| --------------------------- MODULE TLAPlus2Grammar --------------------------- | |
| EXTENDS Naturals, Sequences, BNFGrammars | |
| CommaList(L) == L & (tok(",") & L)^* | |
| AtLeast4(s) == Tok({s \o s \o s} & {s}^+) | |
| ReservedWord == | |
| { "ASSUME", "ELSE", "LOCAL", "UNION", | |
| "ASSUMPTION", "ENABLED", "MODULE", "VARIABLE", | |
| "AXIOM", "EXCEPT", "OTHER", "VARIABLES", |
| (* A variable identifier of the lambda language [term]. *) | |
| type var = string [@@deriving eq] | |
| (* The lambda language; direct style. *) | |
| type term = | |
| | Var of var | |
| | Fix of (var * var list * term) list * term | |
| | Appl of term * term list | |
| | Record of term list | |
| | Select of term * int |
| type cps_var = | |
| (* Taken from the lambda term during CPS conversion. *) | |
| | CLamVar of string | |
| (* Generated uniquely during CPS conversion. *) | |
| | CGenVar of int | |
| type cps_term = | |
| | CFix of (cps_var * cps_var list * cps_term) list * cps_term | |
| | CAppl of cps_var * cps_var list | |
| | CRecord of cps_var list * binder |
Every once in a while I investigate low-level backend options for PL-s, although so far I haven't actually written any such backend for my projects. Recently I've been looking at precise garbage collection in popular backends, and I've been (like on previous occasions) annoyed by limitations and compromises.
I was compelled to think about a system which accommodates precise relocating GC as much as possible. In one extreme configuration, described in this note, there
| (* | |
| A formalization of first-order logic, theories and their models. | |
| As an example we formalize the language of ZF set theory and a a small fragment of ZF. | |
| *) | |
| (* A signature is given by function symbols, relation symbols, and their arities. *) | |
| Structure Signature := | |
| { funSym : Type (* names of function symbols *) | |
| ; funArity : funSym -> Type (* arities of function symbols *) | |
| ; relSym : Type (* names of relation symbols *) |