Module fungi_lang::eval
[−]
[src]
Fungi: big-step evaluation semantics.
Gives the incremental semantics of Fungi programs, using an external library (Adapton in Rust) to create and maintain the "demanded computation graph" (the DCG), that underpins change propagation.
Design discussion
The Rust types and functions below demonstrate how closely the
IODyn Target AST corresponds to the primitive notions of Adapton,
namely refs and thunks, and their observation/demand
operations, get and force, respectively.
In particular, the semantics of ref and thunk are entirely
encapsulated by the Adapton run-time library, leaving the
dynamics semantics for other expression forms to eval to define.
In this sense, the language built around the ref and thunk
primitives is open-ended.
Given this language choice, as usual, we choose STLC in CBPV, with product and sum types. Other language/semantics design choices in this module are guided by our choice of "CBPV + environment-passing-style", as discussed further in this module's comments.
Val vs RtVal
We distinguish between programmer-written values (Val) and closed, run-time values (RtVal). Environments map variables to (closed) run-time values.
Exp vs TermExp
We distinguish between (open) expressions and (fully evaluated) terminal expressions, which are closed.
Enums
| EvalTyErr |
Dynamic type errors ("stuck cases" for evaluation) |
| ExpTerm |
Terminal expressions (a la CBPV), but in environment-passing style, where lambdas are associatd with closing environments. |
| NameTmVal |
Name Term Values. The value forms (name and lambda) for the Name Term sub-language (STLC + names). |
| RtVal |
Run-time values. Same as ast_tgt::Val, except that (1) there are
no variables ("closed") and (2) unlike values written by user in
their program, run-time values may contain run-time structures,
such as actual thunks and references, a la |
Functions
| close_val |
Given a closing environment and an Tgt-AST value (with zero or more variables) producing a closed, run-time value. |
| close_val_rec |
See |
| engine_name_of_ast_name |
Name conversion. Convert Tgt-AST name into a run-time (adapton library) name. |
| eval |
Big-step evaluation |
| nametm_eval | |
| nametm_eval_rec | |
| nametm_of_nametmval | |
| nametm_subst | |
| nametm_subst_rec | |
| proj_namespace_name |
project/pattern-match the name of namespace, defined as the sub-term M in the following nameterm (lambda) form: |
Type Definitions
| Env |
TODO-Sometime: Prune the environments (using free variables as filters) |
| RtValRec |