Static semantics of Syntheto.

We formalize the constraints that Syntheto code must satisfy in order to be well-formed and have a formal semantics.

The constraints include type requirements, according to Syntheto's strong typing. Since the Syntheto type system includes predicate subtypes and product/sum type invariants, the static semantics is undecidable, because it may involve general theorem proving. We handle this situation by splitting the static semantics into a decidable and an undecidable part, similar to systems like PVS and Specware. The decidable part handles most of the constraints, generating proof obligations for the undecidable parts. Proof obligations are Syntheto boolean expressions universally quantified over its explicitly typed free variables.

The constraints of the static semantics are checked in the context of variables, types, and other entities that are in scope and can be referenced. We represent the context as an explicit data structure, which is passed to the ACL2 functions that check the constraints and which is updated by some of these functions as more entities come into scope. In addition to the entities mentioned above, since we need to generate proof obligations, the context also includes conditions (boolean expressions) collected as expressions are traversed.

- Check-expression-fns
- Mutually recursive functions for expression checking.
- Subtypep
- Check if a type is a subtype of another type.
- Match-type
- Match a source type to a target type.
- Check-product-update-expression
- Check if a product update expression is statically well-formed.
- Get-builtin-function-in/out/pre-post
- Retrieve the inputs, outputs, precondition, and postcondition of a built-in function.
- Check-sum-update-expression
- Check if a sum update expression is statically well-formed.
- Check-sum-field-expression
- Check if a sum field expression is statically well-formed.
- Check-strict-binary-expression
- Check if a strict binary expression is well-formed.
- Check-lt/le/gt/ge-expression
- Check if an ordering expression is well-formed.
- Check-eq/ne-expression
- Check if an equality or inequality expression is well-formed.
- Check-div/rem-expression
- Check if a division or remainder expression is well-formed.
- Check-add/sub/mul-expression
- Check if an addition, substraction, or multiplication expression is well-formed.
- Align-let-vars-values
- Align bound variables to their expressions.
- Check-iff-expression
- Check if a coimplication expression is well-formed.
- Check-function-definition-top/nontop
- Check if a function definition (at the top level or not) is statically well-formed.
- Check-sum-construct-expression
- Check if a sum construction expression is statically well-formed.
- Check-sub-expression
- Check if a subtraction expression is well-formed.
- Check-rem-expression
- Check if a multiplication expression is well-formed.
- Check-mul-expression
- Check if a multiplication expression is well-formed.
- Check-div-expression
- Check if a division expression is well-formed.
- Check-add-expression
- Check if an addition expression is well-formed.
- Check-ne-expression
- Check if an inequality expression is well-formed.
- Check-le-expression
- Check if a less-than-or-equal-to expression is well-formed.
- Check-ge-expression
- Check if a greater-than-or-equal-to expression is well-formed.
- Check-eq-expression
- Check if an equality expression is well-formed.
- Check-lt-expression
- Check if a less-than expression is well-formed.
- Check-gt-expression
- Check if a greater-than expression is well-formed.
- Check-function-specifier
- Check if a function specifier is statically well-formed.
- Type-result
- Fixtype of type results.
- Check-product-construct-expression
- Check if a product construction expression is statically well-formed.
- Supremum-type
- Supremum (i.e. least upper bound) of two Syntheto types.
- Check-call-expression
- Check if a function call is statically well-formed.
- Check-product-field-expression
- Check if a product field expression is statically well-formed.
- Check-function-definer
- Check if a function definer is statically well-formed.
- Make-subproof-obligations
- Create the obligations for a chain of subtypes.
- Get-function-in/out/pre/post
- Retrieve the inputs, outputs, precondition, and postcondition of a function.
- Match-field
- Match a source field to some target field.
- Decompose-expression
- Decompose an expression into a list of expressions of given length.
- Check-sum-test-expression
- Check if a sum test expression is statically well-formed.
- Match-to-target
- Match the type(s) of an expression to some optional target type(s).
- Match-type-list
- Match a list of source types to a list of target types.
- Check-unary-expression
- Check if a unary expression is statically well-formed.
- Max-supertype
- Maximal supertype of a type.
- Check-minus-expression
- Check if an integer negation expression is well-formed.
- Check-type-definition
- Check if a type definition (at the top level) is statically well-formed.
- Check-not-expression
- Check if a boolean negation expression is well-formed.
- Match-field-list
- Match a list of source fields to some target fields.
- Check-type-product
- Check if a type product is statically well-formed.
- Align-let-vars-values-aux
- Check-type-subset
- Check if a type subset is statically well-formed.
- Check-type-definition-in-recursion
- Check if a type definition in a type recursion is statically well-formed.
- Non-trivial-proof-obligation
- Check-type-recursion
- Check if a type recursion is statically well-formed.
- Check-toplevel
- Check if a top-level construct is statically well-formed.
- Check-function-specification
- Check if a function specification is statically well-formed.
- Supremum-type-list
- Lift
`supremum-type`to lists. - Check-component-expression
- Check if a multi-valued component expression is statically well-formed.
- Check-function-recursion
- Check if a function recursion is statically well-formed.
- Check-branch-list
- Check if a list of branches is statically well-formed.
- Check-function-definition
- Check if a function definition (at the top level) is statically well-formed.
- Binding
- Fixtype of bindings.
- Check-function-header
- Check if a function header is statically well-formed.
- Check-function-definition-list
- Check if a list of function definitions is statically well-formed.
- Check-type-definition-list-in-recursion
- Lift
`check-type-definition-in-recursion`to lists. - Check-theorem
- Check if a theorem is statically well-formed.
- Context-add-variables
- Add some variables to a context.
- Check-nonstrict-binary-expression
- Check if a non-strict binary expression is statically well-formed.
- Decompose-expression-aux
- Check-alternative
- Check if a type sum alternative is statically well-formed.
- Check-multi-expression
- Check if a multi-valued expression is statically well-formed.
- Check-alternative-list
- Lift
`check-alternative`to lists. - Context-add-condition
- Add a condition obligation hypothesis to a context.
- Check-type-sum
- Check if a type sum is statically well-formed.
- Check-type-definer
- Check if a type definer is statically well-formed.
- Check-type
- Check if a type is statically well-formed.
- Check-transform
- Check-toplevel-list
- Check if a list of top-level constructs is statically well-formed.
- Context-add-condition-list
- Add a list of condition obligation-hypotheses to a context, in order.
- Check-variable
- Check if a variable is statically well-formed.
- Check-transform-args
- Check-if/when/unless-expression
- Check if an if/when/unless-then-else expression is statically well-formed.
- Initializers-to-variable-substitution
- Turn a list of initializers into a variable substitution.
- Context-add-binding
- Add a binding obligation hypothesis to a context.
- Check-function-header-list
- Check if a list of function headers is statically well-formed.
- Ensure-single-type
- Ensure that a list of types is a singleton.
- Context-add-toplevel
- Add a toplevel object to context.
- Max-supertypes
- Check-type-list
- Check-literal
- Check if a literal is statically well-formed.
- Check-bind-expression
- Check if a binding expression is statically well-formed.
- Literal-type
- Type of a literal.
- Check-expression-list
- Check if a list of expressions is statically well-formed.
- Variable-context
- Fixtype of variable contexts.
- Check-cond-expression
- Check if a conditional expression is statically well-formed.
- Check-branch
- Check if a branch is statically well-formed.
- Args-without-defaults
- *builtin-function-names*
- List of identifiers of the Syntheto built-in functions.
- Check-expression
- Check if an expression is statically well-formed.
- Function-called-in