Context
Fixtype of contexts.
This is a product type introduced by fty::defprod.
Fields
- tops — toplevel-list
- types — identifier-list
- functions — function-header-list
- variables — variable-context
- obligation-vars — typed-variable-list
- obligation-hyps — obligation-hyp-list
A context consists of the following components:
- A sequence of top-level constructs
processed so far by the static semantics.
This starts with the empty sequence,
and is extended one top-level construct after the other.
In Syntheto, order matters:
things are introduced in order, bottom-up;
there are no forward references allowed,
unless they are within explicit mutual recursion constructs.
- A list of the type names whose definitions are being checked.
This is non-empty only when checking
a type definition
(in which case it contains the name of the type being defined)
or a type recursion
(in which case it contains the names of the types being defined).
This component is necessary to accept recursive type definitions.
- A list of the function headers whose definitions are being checked.
This is non-empty only when checking
a function definition
(in which case it contains the header of the function being defined)
or a function recursion
(in which case it contains the headers of the functions being defined).
This component is necessary to accept recursive function definitions.
- A variable context for the variables encountered so far and their types,
when checking an expression.
This is non-empty only if we are checking an expression.
- A list of the typed variables
at the top level of the expression being checked.
These variables are used in the generated proof obligations,
where only the top-level variables count,
because the non-top-level variables, i.e. the let-bound variables,
are collected in the obligation hypotheses instead (see next item).
This list is non-empty only if we are checking an expression.
- A list of the obligation hypotheses collected
at the current position in the Syntheto code.
See obligation-hyp.
This list is non-empty only if we are checking an expression.
Subtopics
- Contextp
- Recognizer for context structures.
- Context-fix
- Fixing function for context structures.
- Make-context
- Basic constructor macro for context structures.
- Context-equiv
- Basic equivalence relation for context structures.
- Context->obligation-vars
- Get the obligation-vars field from a context.
- Context->obligation-hyps
- Get the obligation-hyps field from a context.
- Context->functions
- Get the functions field from a context.
- Change-context
- Modifying constructor for context structures.
- Context->variables
- Get the variables field from a context.
- Context->types
- Get the types field from a context.
- Context->tops
- Get the tops field from a context.
