Static-semantics
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.
Subtopics
- 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-rem-expression
- Check if a multiplication expression is well-formed.
- Check-mul-expression
- Check if a multiplication expression is well-formed.
- Check-sub-expression
- Check if a subtraction 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-lt-expression
- Check if a less-than expression is well-formed.
- Check-le-expression
- Check if a less-than-or-equal-to expression is well-formed.
- Check-gt-expression
- Check if a greater-than 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-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.
- Check-sum-test-expression
- Check if a sum test expression is statically well-formed.
- Match-field
- Match a source field to some target field.
- Decompose-expression
- Decompose an expression into a list of expressions of given length.
- Match-to-target
- Match the type(s) of an expression to some optional target type(s).
- Check-unary-expression
- Check if a unary expression is statically well-formed.
- Max-supertype
- Maximal supertype of a type.
- Match-type-list
- Match a list of source types to a list of target types.
- 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.
- Check-type-product
- Check if a type product is statically well-formed.
- Match-field-list
- Match a list of source fields to some target fields.
- 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.
- Align-let-vars-values-aux
- Non-trivial-proof-obligation
- Check-type-recursion
- Check if a type recursion is statically well-formed.
- Check-function-specification
- Check if a function specification is statically well-formed.
- Check-toplevel
- Check if a top-level construct 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-branch-list
- Check if a list of branches is statically well-formed.
- Check-function-recursion
- Check if a function recursion 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.
- Check-nonstrict-binary-expression
- Check if a non-strict binary expression is statically well-formed.
- Context-add-variables
- Add some variables to a context.
- 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-type-sum
- Check if a type sum is statically well-formed.
- Check-type
- Check if a type 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-definer
- Check if a type definer is statically well-formed.
- Check-transform
- Check-variable
- Check if a variable is statically well-formed.
- Check-transform-args
- 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-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.
- Context-add-toplevel
- Add a toplevel object to context.
- Ensure-single-type
- Ensure that a list of types is a singleton.
- Max-supertypes
- Check-bind-expression
- Check if a binding expression is statically well-formed.
- Check-type-list
- Check-literal
- Check if a literal 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
- Check-expression
- Check if an expression is statically well-formed.
- *builtin-function-names*
- List of identifiers of the Syntheto built-in functions.
- Function-called-in
