relay_expr.rst 27 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
..  Licensed to the Apache Software Foundation (ASF) under one
    or more contributor license agreements.  See the NOTICE file
    distributed with this work for additional information
    regarding copyright ownership.  The ASF licenses this file
    to you under the Apache License, Version 2.0 (the
    "License"); you may not use this file except in compliance
    with the License.  You may obtain a copy of the License at

..    http://www.apache.org/licenses/LICENSE-2.0

..  Unless required by applicable law or agreed to in writing,
    software distributed under the License is distributed on an
    "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
    KIND, either express or implied.  See the License for the
    specific language governing permissions and limitations
    under the License.

18 19 20 21 22 23 24 25 26 27 28
====================
Expressions in Relay
====================

The Relay IR is a pure, expression-oriented language. The below sections
describe the different expressions in Relay and give details of their semantics.

Dataflow and Control Fragments
==============================

For the purposes of comparing Relay to traditional computational graph-based IRs, it
29
can be useful to consider Relay expressions in terms of dataflow and control fragments.
30
Each portion of a Relay program containing expressions that only affect the dataflow can
31
be viewed as a traditional computation graph when writing and expressing transformations.
32 33 34 35

The dataflow fragment covers the set of Relay expressions that do not involve
control flow. That is, any portion of a program containing only the following
constructs corresponds to a pure computation graph:
36

37 38 39 40
- `Variables`_
- Tuple `Construction`_ and `Projection`_
- `Let Bindings`_
- `Graph Bindings`_
41
- Calls to `Operators`_ and `ADT Constructors`_
42 43 44 45

Control flow expressions allow the graph topology to change
based on the value of previously executed expressions. The control
fragment in Relay includes the following constructs:
46

47
- `If-Then-Else`_ Expressions
48
- `ADT Matching`_ Expressions
49 50 51
- Recursive Calls in Functions

From the point of view of a computation graph, a function is a subgraph and a function call inlines the subgraph, substituting its arguments for the free variables in the subgraph with corresponding names.
52 53
Thus, if a function's body uses only dataflow constructs,
a call to that function is in the dataflow fragment; conversely, if the
54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72
function's body contains control flow, a call to that function is not part of the dataflow fragment.

Variables
=========

Inspired by LLVM, Relay explicitly distinguishes between local and
global variables both in the AST and in the text format. In the text format,
global and local variables are distinguished by prefixes, or *sigils*.
Global variables are prefixed with :code:`@` and local variables with :code:`%`.

This explicit distinction makes certain optimizations easier to implement.
For example, inlining a global definition requires no analysis: simply
substituting the definition suffices.

Global Variable
~~~~~~~~~~~~~~~~~~

Global identifiers are prefixed by the :code:`@` sigil, such as ":code:`@global`".
A global identifier always references a globally visible definition contained in the
73
globally visible environment, known as the `module <Module and Global Functions_>`__.
74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
Global identifiers must be unique.

See :py:class:`~tvm.relay.expr.GlobalVar` for its implementation
and documentation.

Local Variable
~~~~~~~~~~~~~~

Local identifiers are prefixed by the :code:`%` sigil,
such as ":code:`%local`". A local identifier always references
a function argument or a variable bound in a :code:`let` expression,
and will be scoped to the function where it appears or the :code:`let`
expression where it is bound, respectively.

In the below code segment, notice that :code:`%a` is defined twice. This is
permitted, as in most functional languages; in the scope of the second
:code:`let` expression, the name :code:`%a` is "shadowed," meaning all
91
references to :code:`%a` in the inner scope refer to the later definition, while
92 93 94
references to :code:`%a` in the outer scope continue to refer to
the first one.

95
.. code-block::
96 97 98 99 100

    let %a = 1;
    let %b = 2 * %a;  // %b = 2
    let %a = %a + %a; // %a = 2. %a is shadowed
    %a + %b           // has value 2 + 2 = 4
101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122

(Note that in Relay's implementation, each definition of a local variable
creates a new :py:class:`~tvm.relay.expr.Var`, so a shadowed local variable,
despite having the same name as one in an outer scope, will be a different
object. This allows for comparing local variables by pointer identity with the
knowledge that the same local variable object corresponds to a different binding site.)

See :py:class:`~tvm.relay.expr.Var` for its implementation
and documentation.

Functions
=========

Functions in Relay act similarly to procedures or functions in
other programming languages and serve to generalize the concept
of a named subgraph.

Functions are first class in Relay, which means they are expressions just like variables, constants, and tuples.
Additionally, functions in Relay are higher-order, which means that a function can be passed as an argument to a
function or returned by a function, as function expressions evaluate to closures (see the `Closures`_ subsection),
which are values like tensors and tuples.

Zhi committed
123
See :py:class:`~tvm.relay.function.Function` for the definition and documentation of function nodes.
124 125 126 127 128 129 130 131

Syntax
~~~~~~

A definition minimally consists of the keyword :code:`fn`, an empty set of
parameters, and a body expression (:py:class:`~tvm.relay.expr.Expr`)
contained by curly braces.

132
.. code-block::
133 134 135 136 137 138

    fn() { body }

A definition may contain any number of parameters. For example, a
simple function that invokes the :code:`add` operator:

139
.. code-block::
140 141 142 143 144 145 146 147 148 149

    fn(%x, %y) { add(%x, %y) }

Notice that within the function's body, the parameters are local
variables, just like those bound in a :code:`let` expression.

One may also annotate explicit types on functions.
For example, we can restrict the above function to only work
on certain types:

150
.. code-block::
151 152 153 154 155 156 157

    fn(%x : Tensor[(10, 10), float32], %y : Tensor[(10, 10), float32])
               -> Tensor[(10, 10), float32] {
        add(%x, %y)
    }

The above function only takes arguments of type :code:`Tensor[(10, 10), float32]` and returns a value of
158
type :code:`Tensor[(10, 10), float32]`. A function parameter is just a local
159 160 161 162 163 164 165 166 167 168
variable (:py:class:`~tvm.relay.expr.LocalVar`) optionally annotated with a type, written as :code:`%x : T`.

When the type information is omitted, Relay attempts to infer the most general type
for the users. This property is known as generalization: for a definition without
explicit annotations, Relay attempts to assign the most general type to the
parameters and return type based on the function body and call sites.

A recursive function expression can be defined using a :code:`let` binding,
as here:

169
.. code-block::
170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191

    let %fact = fn(%x : Tensor[(10, 10), float32]) -> Tensor[(10, 10), float32] {
        if (%x == Constant(0, (10, 10), float32)) {
            Constant(1, (10, 10), float32)
        } else {
            %x * %fact(%x - Constant(1, (10, 10), float32))
        }
    };
    %fact(Constant(10, (10, 10), float32))

Closures
~~~~~~~~

A function expression evaluates to a closure. Closures
are values that are represented as a pair of a local environment
(storing the values for all variables defined outside the scope
of the function's body) and the function itself.

For example, in the below example, the final result will be
a tensor of zero values because the closure for :code:`%f` stores the value of
:code:`%x` at the pointer where :code:`%f` was defined.

192
.. code-block::
193 194 195 196 197 198 199 200 201 202 203 204 205 206 207

    let %g = fn() {
      let %x = Constant(0, (10, 10), float32);
      // %x is a free variable in the below function
      fn(%y) { %y * %x }
    };
    // the %x in %g's body is not in scope anymore
    // %f is a closure where %x maps to Constant(0, (10, 10), float32)
    let %f = %g();
    let %x = Constant(1, (10, 10), float32);
    %f(%x) // evaluates to Constant(0, (10, 10), float32)

Polymorphism and Type Relations
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

208
*Note: type parameter syntax is not yet supported in the text format.*
209 210 211 212 213 214 215 216 217 218

A function may also be given a set of type parameters, which can be
substituted for specific types at call sites. Functions with
type parameters are *type polymorphic*; their return type or the types
of arguments they will accept can vary based on the type arguments
given at call sites.

Type parameters are classified by *kind* and can
only appear in parts of the type signature where their kind is appropriate
(e.g., type parameters of kind :code:`Shape` can only appear where a shape
219
would be expected in a tensor type); for a full discussion,
220
see :ref:`the documentation on type parameters <type-parameter>`.
221 222 223 224

For example, one can define a polymorphic identity function for
any Relay type as follows:

225
.. code-block::
226

227 228 229 230 231 232 233
    fn<t : Type>(%x : t) -> t {
        %x
    }

The below definition is also polymorphic, but restricts its
arguments to tensor types:

234
.. code-block::
235

236 237 238 239 240 241
    fn<s : Shape, bt : BaseType>(%x : Tensor[s, bt]) {
        %x
    }

Notice that the return type is omitted and will be inferred.

242
*Note: "where" syntax is not yet supported in the text format.*
243 244 245 246

A function may also be subject to one or more type relations, such as in
the following:

247
.. code-block::
248 249 250 251 252 253 254 255 256 257 258 259 260 261

    fn(%x, %y) where Broadcast { add(%x, %y) }

In the above definition, the types of :code:`%x` and :code:`%y` and the return type
are subject to the :code:`Broadcast` relation, meaning all three must be tensors
and their shapes follow the elementwise broadcast relation. As with
operators, the definitions of relations are not transparent to Relay
and they are instead implemented externally in either C++ or Python.

As in the case of :code:`Broadcast`, relations are used to express complicated
constraints on types (especially tensor shapes).
All function relations must hold at all call sites;
type checking is thus treated as a constraint-solving problem.
For more detail on type relations and their implementations,
262
please see :ref:`their section in the documentation on Relay's type system <type-relation>`.
263 264 265 266 267 268 269

Operators
=========

An operator is a primitive operation, such as :code:`add` or :code:`conv2d`, not defined in the Relay
language. Operators are declared in the global operator
registry in C++. Many common operators are backed by TVM's
270
Tensor Operator Inventory (`TOPI <https://github.com/apache/incubator-tvm/tree/master/topi>`__).
271 272 273 274 275 276 277 278 279 280

To register an operator a user must provide an implementation
of the operator, its type, and any other desired metadata.
The operator registry is a column-based store where
operators are keys, so any metadata (which might be referenced
by optimization passes) may be registered as a new column.

From the perspective of Relay's type system, an operator is a function,
so operators may be called like any other function and have function
types. In particular, operator types are registered using a single
281
type relation (see :ref:`the documentation on type relations <type-relation>`), typically a relation
282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299
specialized to that operator. For example, the :code:`add` operator
is registered with the :code:`Broadcast` relation, indicating that the
arguments of :code:`add` must be tensors and that the return type
is a tensor whose shape depends on those of its arguments.

Operators are rendered without a sigil (e.g :code:`conv2d`, :code:`flatten`)
when pretty-printing Relay programs.
Operators are explicitly contained in the program and are uniquely
identifiable by pointer.

Note that common arithmetic operators such as :code:`add` and :code:`multiply`
may be written using the corresponding arithmetic operators in the text format
(e.g., :code:`+` or :code:`*`) as syntactic sugar.

See :py:class:`~tvm.relay.op.Op` for the definition and documentation
of operator nodes, demonstrating the infrastructure for registering
operator metadata. The other files in :py:class:`~tvm.relay.op` give
handles for generating a call to various pre-registered operators.
300
The :ref:`tutorial on adding operators to Relay <relay-add-op>` shows how to add further
301 302
operators into the language.

303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338
ADT Constructors
================

Algebraic data types (ADTs) in Relay are described in detail in a
:ref:`separate overview<adt-overview>` and their integration into
the type system is described :ref:`here<adt-typing>`.

In this section, we will simply note that ADT constructors are given
a function type and should be used inside call nodes like a function
or operator. An ADT constructor is defined by giving the name of
the ADT it constructs (a global type variable) and the types of the
expected arguments for the constructor.

If the ADT definition includes type variables, those type variables
may appear in the constructor. Constructors cannot include any other
type variables.

Let us suppose that :code:`D` is an ADT that takes type parameters
:code:`a` and :code:`b`. If :code:`C1` is a constructor for :code:`D`
and expects two arguments, one of type :code:`a` and one of type :code:`b`, then
:code:`C1` has the following type signature:
:code:`fun<a, b>(a, b) -> D[a, b]`. (See either the ADT overview
or the discussion of ADT typing for an explanation of the type call
in the return type.)
If another constructor for :code:`D`, :code:`C2`, takes no arguments,
then it has the following type signature: :code:`fun<a, b>() -> D[a, b]`;
the type parameters will always appear in the return type.

Once called, a constructor produces an ADT instance, which is a
container that stores the values of the arguments to the constructor
as well as the name ("tag") of the constructor. The tag will be used
for deconstructing the instances and retrieving the values when
`ADT Matching`_.

See :py:class:`~tvm.relay.adt.Constructor` for the definition and documentation.

339 340 341 342 343 344 345 346 347 348 349
Call
====

Expressions with function types in Relay are "callable,"
meaning that they can be invoked via a function call. These consist of
any expression that evaluates to a closure (i.e., function expressions
or global functions) and Relay operators.

The syntax of calls follows that used in C-like languages, demonstrated in the
example below:

350
.. code-block::
351 352 353 354 355 356

   let %c = 1;
   let %f = fn(%x : Tensor[(), float32], %y : Tensor[(), float32]) { %x + %y + %c };
   %f(10, 11)

When a closure is called (see `Closures`_),
357
the closure's body is evaluated in the stored environment
358 359 360 361 362 363 364
(i.e., using the stored values for free variables) with
local variable bindings added for each argument; the final value
obtained by evaluating the body is the call's return value.
Thus, in the above example, the call evaluates to 22.
In the case of operators, the implementation is opaque to Relay,
so the result is left up to the registered TVM implementation.

365
*Note: type parameters are not yet supported in the text format.*
366 367 368 369 370 371 372

A type-polymorphic function can also include type arguments at a call
site. The type arguments are substituted for type parameters when
type checking. If a function is type-polymorphic and type arguments are not
given, type inference will attempt to infer type arguments if possible.
The following code gives examples of explicit and inferred type arguments:

373
.. code-block::
374 375 376 377 378 379 380 381 382

    // %f : fn<a : Type, b : Type, c : Type>(a, b) -> c
    let %x1 = %f<Tensor[(), bool], Tensor[(), bool], Tensor[(), bool)]>(True, False);
    // %x1 is of type Tensor[(), bool]
    let %x2 : () = %f(%x1, %x1)
    // the type arguments in the second call are inferred to be <Tensor[(), bool], Tensor[(), bool], ()>

Note that all type relations in the function type must hold at each
call site. Specifically, this means that the relation will be checked
383
against the specific types of the arguments at a given call site. This
384 385 386 387 388 389 390 391 392
is also a form of polymorphism, since there may be multiple valid
assignments of argument types and a return type so long as the relation
is satisfied.

For example, if we have a function :code:`%f` that takes tensor arguments
and has the :code:`Broadcast` relation, then there are many different
shapes that the arguments in the below call could have that would satisfy
the type annotation:

393
.. code-block::
394 395 396 397 398 399

   let %x : Tensor[(100, 100, 100), float32] = %f(%a, %b);
   %x

See :py:class:`~tvm.relay.expr.Call` for its definition and documentation.

400 401
.. _module-description:

402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418
Module and Global Functions
===========================

Relay keeps a global data structure known as a "module" (often called an "environment" in other
functional programming languages) to keep track of the definitions of global functions.
In particular, the module keeps a globally accessible mapping of global variables to the
function expressions they denote. The utility of the module is that it allows global functions
to recursively refer to themselves or any other global function (e.g., as in mutual recursion).

Note Relay's module is analogous to data structures for keeping track of subgraphs in computation
graph-based IRs.

Global functions in Relay behave identically to the function expressions defined in `Functions`_,
but have syntactic sugar in the text format to enter their definitions into the module. Namely,
a global function definition includes a global identifier and is allowed to recursively refer to
that identifier in the body, as in the following example:

419
.. code-block::
420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457

   def @ackermann(%m : Tensor[(), int32], %n : Tensor[(), int32]) -> Tensor[(), int32] {
       if (%m == 0) {
           %n + 1
       } else if (%m > 0 && %n == 0) {
           @ackermann(%m - 1, 1)
       } else {
           @ackermann(%m - 1, @ackermann(%m, %n - 1))
       }
   }

This definition would result in a module entry mapping the identifier :code:`@ackermann` to a function expression
with the parameters, return type, and body above. Any reference to the identifier :code:`@ackermann` elsewhere in the
code could then look up the identifier in the module and replace the function definition as needed.

See :py:class:`~tvm.relay.Module` for the definition and documentation of a module.

Constant
========

This node represents a constant tensor value
(see :py:mod:`~tvm.relay.Value` for more details).
A constant is represented as a :py:class:`~tvm.NDArray`,
allowing Relay to utilize TVM operators for constant evaluation.

This node can also represent scalar constants, since
scalars are tensors with a shape of :code:`()`. In the text format, numerical
and boolean literals are thus syntactic sugar for constants encoding a
tensor type with a rank-zero shape.

See :py:class:`~tvm.relay.expr.Constant` for its definition and documentation.

Tuples
======

Construction
~~~~~~~~~~~~

458
The tuple node builds a finite (that is, of statically known size) sequence of heterogeneous data.
459 460 461
These tuples match Python's closely, and their fixed length allows for efficient projection of their
members.

462
.. code-block::
463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478

   fn(%a : Tensor[(10, 10), float32], %b : float32, %c : Tensor[(100, 100), float32]) {
       let %tup = (%a, %b);     // type: (Tensor[(10, 10), float32], float32)
       ((%tup.0 + %tup.1), %c)  // type: (Tensor[(10, 10), float32], Tensor[(100, 100), float32])
   }

See :py:class:`~tvm.relay.expr.Tuple` for its definition and documentation.

Projection
~~~~~~~~~~

A tuple must be indexed by an integer constant in order to extract a
particular member of the tuple. Projections are 0-indexed.

For example, the below projection evaluates to :code:`%b`:

479
.. code-block::
480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496

   (%a, %b, %c).1

See :py:class:`~tvm.relay.expr.TupleGetItem` for its definition and documentation.

Let Bindings
============

A :code:`let` binding is an immutable local variable binding,
allowing the user to bind an expression to a name.

A :code:`let` binding contains a local variable,
an optional type annotation, a value, and a body expression
that may reference the bound identifier. If a type annotation
on the bound variable is omitted, Relay attempts to infer the
most general type permitted for the variable.

497
The bound variable in a :code:`let` expression is only in scope
498 499
in its body, except when the variable defines a function expression.
When a :code:`let` expression creates a function, the variable is also
500
in scope in its value to allow for recursively defined functions
501 502 503 504 505 506 507
(see the previous subsection).

The value of a :code:`let` binding is the value of the final expression
after evaluating the bindings it depends on. For example, in the
following example the entire expression evaluates to a tensor
of shape :code:`(10, 10)` where all elements are 2:

508
.. code-block::
509 510 511 512 513 514 515 516 517 518 519 520

   let %x : Tensor[(10, 10), float32] = Constant(1, (10, 10), float32);
   %x + %x

A sequence of :code:`let` bindings can be considered as a dataflow graph,
where the bindings are a series of sub-graphs connected
by bound variables. Since these binding sequences are
pure, a pair of bindings where neither depends on the other can be safely reordered.
For example, the first and second :code:`let` bindings below
may be evaluated in either order because neither has a dataflow
dependency on the other:

521
.. code-block::
522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543

   let %x = %a + %b;
   let %y = %c + %d;
   %x * %y

See :py:class:`~tvm.relay.expr.Let` for its definition and documentation.

Graph Bindings
==============

A :code:`let` binding creates a named variable that is bound to the given value
and scoped to the subsequent expression. By contrast, a graph binding allows for
explicitly constructing dataflow graphs in a Relay program by binding an expression
(graph node) directly to a temporary variable, which is not scoped. Each reference
to the variable corresponds to an edge in the dataflow graph. This has the
semantics of substituting the expression wherever the variable appears, even though
the graph node will only be evaluated once by the compiled program.

These bindings allow for a style of programming that corresponds to that already
employed by NNVM and other dataflow graph-based input formats. The fact that the variables
are not scoped offers some flexibility in evaluation order compared to :code:`let`
bindings, though this can also introduce some ambiguity in programs (the
544
:ref:`developer introduction to the Relay IR<relay-dev-intro>` includes more detailed discussion
545 546
of this nuance).

547
*Note: Graph bindings are not currently parsed by the text format.*
548 549 550 551

In Relay's text format, a graph binding can be written as below (note the lack of a
:code:`let` keyword and a semicolon):

552
.. code-block::
553 554 555 556 557 558 559 560 561 562 563

   %1 = %a + %b
   %2 = %1 + %1
   %2 * %2

Unlike a let binding, a graph binding is not represented as an AST node in Relay, but rather as a meta-variable referencing its AST node value.
For example, a program like the above could be constructed in Relay's
Python front-end by setting *Python variables* equal to the corresponding Relay AST node and
using the variables repeatedly, as below (a C++ program using the corresponding API bindings
could accomplish the same thing):

564
.. code-block::
565 566 567 568 569 570 571 572 573

   sum1 = relay.add(a, b)
   sum2 = relay.add(sum1, sum1)
   relay.multiply(sum2, sum2)

For development purposes and to enable certain optimizations, Relay includes passes to
convert between dataflow graphs defined using graph bindings and programs with :code:`let`
bindings in A-normal form, employed by many compiler optimizations from the functional
programming community (see `"A-Normalization: Why and How" by
574
Matt Might <http://matt.might.net/articles/a-normalization/>`__ for an introduction
575 576 577 578 579 580 581 582 583
to A-normal form).

If-Then-Else
============

Relay has a simple if-then-else expression that allows programs to branch
on a single value of type :code:`bool`, i.e., a zero-rank
tensor of booleans (:code:`Tensor[(), bool]`).

584
.. code-block::
585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600

    if (%t == %u) {
        %t
    } else {
        %u
    }

Since if-then-else branches are expressions, they may appear inline
wherever any other expression may be expected, like invocations of
the ternary operator in C-like languages. The if-then-else expression
evaluates to the value of the "then" branch if the condition value
evaluates to :code:`True` and evaluates to the value of the "else" branch if the
condition value evaluates to :code:`False`.

See :py:class:`~tvm.relay.expr.If` for its definition and documentation.

601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628
ADT Matching
============

Instances of algebraic data types (ADTs), as discussed in the
:ref:`ADT overview<adt-overview>`, are containers that store the
arguments passed to the constructor used to create them, tagged by
the constructor name.

Match expressions in Relay allow for retrieving the values stored in
an ADT instance ("deconstructing" it) based on their constructor tag.
A match expression behaves similarly to a C-style :code:`switch` statement,
branching on the different possible constructors for the type of the
value being deconstructed. As the ADT overview details, match
expressions are capable of more general pattern-matching than simply
splitting by constructors: any ADT instance nested inside an instance
(e.g., a list of lists) can be deconstructed at the same time as
the outer instance, while the different fields of the instance can be
bound to variables. (See :ref:`this section<adt-pattern>` for a detailed
description of ADT pattern-matching.)

A match expression is defined using the
input value (an expression) and a list of clauses, each of which
consists of a pattern and an expression. When executed, the *first*
clause whose pattern matches the structure of the queried value is
executed; the clause expression is evaluated and returned.

For example, suppose we have an ADT for natural numbers:

629
.. code-block::
630 631 632 633 634 635 636 637

   data Nat {
     Z : () -> Nat # zero
     S : (Nat) -> Nat # successor (+1) to a nat
   }

Then the following function subtracts one from a passed nat:

638
.. code-block::
639 640 641 642 643 644 645 646 647 648 649

   fn(%v: Nat[]) -> Nat[] {
     match(%v) {
       case Z() { Z() }
       case S(%n) { %n } # the variable %n is bound in the scope of this clause
     }
   }

The following function subtracts two from its argument if it is at least
two and returns the argument otherwise, using a nested constructor pattern:

650
.. code-block::
651 652 653 654 655 656 657 658 659 660 661 662 663

   fn(%v : Nat[]) -> Nat[] {
     match(%v) {
        case S(S(%n)) { %n }
        # wildcard pattern: matches all cases not matched already
        case _ { %v }
     }
   }

As aforementioned, the ordering of match clauses is relevant.
In the below example, the first clause will always match so
those below it can never run:

664
.. code-block::
665 666 667 668 669 670 671 672 673 674 675 676

   fn(%v : Nat[]) -> Nat[] {
     match(%v) {
       case _ { %v }
       case S(S(%n)) { S(%n) }
       case S(%n) { %n }
       case Z() { S(Z()) }
     }
   }

See :py:class:`~tvm.relay.adt.Match` for its definition and documentation.

677 678 679
TempExprs
=========

680
Program transformations (passes) in Relay may require inserting temporary
681 682 683
state into the program AST to guide further transformations. The
:code:`TempExpr` node is provided as a utility to developers for this purpose;
nodes inheriting from :code:`TempExpr` cannot appear directly in user-provided
684 685 686
code but may be inserted in a pass. Any :code:`TempExpr` created in a pass
should ideally be eliminated before the pass is complete, as a
:code:`TempExpr` only stores internal state and has no semantics of its own.
687

688
For an example of :code:`TempExpr` being used in a pass,
689 690 691 692 693
see :code:`src/relay/pass/alter_op_layout.cc`, which uses :code:`TempExpr` nodes
to store information about operator layouts as the pass tries to rearrange operator
calls.

See :py:class:`~tvm.relay.expr.TempExpr` for its definition and documentation.