|
|
|---|
|
|
|
|---|
Fixtype of Syntheto expressions.
This is a tagged union type, introduced by fty::deftagsum.
There are literals, variables, if-then-else expressions (non-strict), and function calls. These all correspond to ACL2 translated terms.
The type list argument in the function call is non-empty for certain built-in Syntheto functions, which are polymorphic. Examples are functions that operate on sequences. The type list consists of actual type arguments for the function's formal type parameters: that is, it describes the (monomorphic) instance of the function used in the call. This will be useful also if and when we extend Syntheto with more general polymorphic user-defined types and functions.
We have variants when-then-else and unless-then-else of if-then-else: when-then-else is just like if-then-else, but it may be syntactically represented as an early exit in concrete syntax; unless-then-else is just liked a flipped if-then-else, but it may be syntactically represented as an early exit in concrete syntax. In ACL2, these are available as ``bindings'' in b*, but they are not really bindings as such, so we do not represent them as bindings.
We have a more general form of ACL2's let bindings, which can either bind a single variable to a single-valued expression, or multiple variables to a multi-valued expression. The latter is like mv-let, or an mv binder in b*.
We also have conditional expressions, consisting of sequences of branches, where a branch consists of a condition expression and an expression that computes the value when the condition holds. These correspond to cond in ACL2.
In addition, there are unary and binary expressions. These are like function calls, but syntactically they use operators that are not identifiers and have an infix notation in the case of binary expressions.
We have expressions to build multi-valued expressions, corresponding to ACL2's mv. And we have expressions to obtain single-valued components of multi-valued expressions, via numeric indices, corresponding to ACL2's mv-nth.
There are also expressions to construct values of product types. There are expressions to obtain the value of a field of a product type. There are also expressions to ``update a value of a product type'' by returning a copied value with some of its fields changed.
There are similar expressions for values of sum types. They include the name of an alternative, which ``selects'' the type product. Note, however, that there are no anonymous product types in Syntheto: the summands of a sum type are anonymous product types in a sense, but they are not actual Syntheto types. This is similar to how fty::deftagsum works. In addition, there are expressions to test whether a value of a sum type belongs to a named alternative.