Creation of a leaf, testing whether an MMX program is a leaf and converting a leaf to a literal.

Creation of a compound tree, testing whether an MMX program is a compound tree, obtaining the arity of a compound tree and accessing a child of a compound tree.

Commodity accessors for the determination of all components of a compound tree (postfix .components), of all arguments of a primitive or function call (postfix .args), of all but its last arguments (postfix .initial), and its last argument (postfix .args).

Given vectors what = [w1, …, wn] and by = [b1, …, bn] of the same length n, return the syntactic substitution of each wi by bi in p.

These modifiers alter the semantics of a declaration decl. In the cases of $forall and $exists, the parameter ql contains a list of signifiers (see below) over which we quantify. In the case of $assume, the parameter hyps contains a list of hypothesis.

Declaration of a macro. The left-hand side is either a literal or an expression var (a1,…,an), where var, a1, …, an are all literals. The right-hand side contains the replacement.

Forward declaration of a variable var of type tp. To do: check whether var should be a literal.

Syntactic construction of a signifier (or typed variable) “var: tp”, for use in combination with $define, $assign, $lambda, $in, $Forall, $Exists. etc. To do: check whether var should be a literal (exception: typed bodies of lambda expressions).

Declaration of a constant resp. a mutable variable. The left-hand side lhs is a typed variable of the form “var: tp” and the right-hand side rhs contains the (initial) value. In the case of an initialization using $define inside a constructor, the left-hand side is a literal.

Declaration of a category, class or module. The name can be of the form Comp (a1, …, an) in the case of compound categories, types or modules, where each of the arguments ai is a signifier.

Checks whether a program is a variable declaration or a forward declaration.

Predicates corresponding to $forall, $exists, $assume, $intern, $extern, $method, $constructor, $constant, $mutable, $private, $public, $macro, $header, $of, $define, $assign, $category, $class and $module.

Find the variable of a variable declaration or signifier.

Find the variable and type of a signifier, a forward declaration, or of the left hand side of a variable declaration.

Find the left-hand side and the right-hand side of a (possibly forward) declaration. The right hand side of a forward declaration is the symbolic constant mmx$forward.

Sequential block of instructions. In the case of mmx$begin, the block may also contain local declarations. When using $BEGIN, it is assumed that the local declarations have already been processed. To do: is the $BEGIN primitive really necessary?

Conditional instructions or expressions.

Fundamental boolean operations

Looping construct, where mods is a list of looping modulators, as described below.

Elementary looping modulators. The $for modulator contains a variable declaration, or an instruction to be executed once before the loop, or an expression of the form “sf in gen”, where gen is a generator. The $while and $until modulators allow for the execution as long as resp. until a certain condition is satisfied. The $step modulator executes an instruction each time we complete one cycle of the loop.

Allows the construction of “sf in gen” as needed by one of the variants of the $for looping modulator. Here sf is a signifier of the form “var: tp” and gen a generator.

Construct for breaking or continuing a loop.

Construction of a lambda expression with arguments args and a typed body tbody. Each of the arguments and the typed body should be signifiers.

Returning the result of a lambda expression.

Constructors for exception handling. The $try construct attempts to execute body. If an error is raised using the $raise construct, then we attempt to handle it using one of the handlers. On failure, the error is reraised outside the $try block.

Predicates corresponding to mmx$begin, $BEGIN, $if, $not, $or, $not, $loop, $for, $while, $step, $in, $break, $continue, $lambda, $return, $try and $raise.

Find the arguments, the (non typed) body and the return type of a lambda expression.

The type Structure is used for the generation of the trivial category. The type Any is used internally as a quantifier for Forall and Exist types.

In the case of $Forall and $Exists, the first argument ql constains a list of quantifiers and the second argument tp a quantified type. Each of the arguments ql should be a signifier.

Special constants and keywords.

Standard hypothesis for use with $assume.

Special functions.

Read and write acces to a field of the instance inst of a class.

Assuming that we are inside a class, this construct indicates that the function lamb is a method of the class. During the compilation, a special “method environment” is attached to the class environment, which allows other methods to be accessed through short names.

Assuming that we are inside a class, this construct indicates that body is the body of a constructor. Such a body is a succession of statements of the form var == val, where var is an intern class field and val its initial value.

Declares a new type tp to be equivalent to equiv.

The first routine $PENALTY explicitly attaches a penalty pen to an object x; if x has type T, then the result has type Penalty (pen, T). The second routine removes the penalty from an object x of type Penalty (pen, T). To do: to be verified.

The first routine $EXPLICIT converts an object x of type T to an object of type Explicit T. The second routine $UNEXPLICIT performs the inverse conversion. To do: to be verified.

Template construction and template instantiation.

Abstraction and concretization.

Low level cast of expr to Void. In particular, $as_void (expr) is used as an equivalent for expr :> $Void in the implementation of :>.