A PLT Redex-inspired language of operational semantics with an automatic "abstracting abstract machines" transformation.
The code is heavily commented with design decisions, descriptions of abstractions and rationale. The following tags have significance:
TODO[?]: A point in the code where an addition is necessary/suggested (respectively) for later commits.
FIXME[?]: A piece of code that is absolutely broken or needs re-evaluation later (respectively).
XXX: Discusses caveats to a design decision, or a less sure "FIXME?"
INVARIANT: Description of a property that should hold invariably.
ASSUMPTION: Like an invariant, but based more on user interaction than program behavior.
UNCHECKED ASSUMPTION: An unproven/poorly justified proposition about user interaction.
OPT: Description of how some piece of code/data structure was optimized.
OPT-OP: An unimplemented idea for an optimization opportunity.
NOTE: A decidedly tricky piece of code follows. This note is a careful explanation.
- abstract counting for better equality matching [1]
- "address spaces" divvy items amongst as many stores that get automatically added.
- Addresses can be marked for pointer equality, or for equality to automatically dereference.
- Addresses introduced by the AAM transformation are the latter kind, in the 'AAM address space.
- finite functions (dictionaries) and sets are natively supported. The burden of ensuring associativity/commutivity of meta-functions on these data is left to the user.
- pattern support for sets and maps
- build an escape hatch for smarter lattices.
- widening for control flow
- automatic garbage collection in "weak maps." Addresses of different spaces can occur in mapped objects.
- add a new "binding" form like When, only non-local. Failure leads to trying the next major rule.
- Synthesize a better alloc skeleton with more user guidance/annotations.
- Drop distinction between terms and expressions. Variant constructors and meta-functions inhabit same namespace.
- Add annotation for trusted termination of meta-functions so the memo table isn't necessary.
- Smarter abstraction of maps so that the CEK machine is automatically transformed into the CESK^*_t machine.
- Arrow expanders (--> position in reduction-relation is expanded)
- Hygienic macros in expressions
- Predicative parametric polymorphism
- a compiler to output specialized Racket code implementing an input language's semantics. Take alloc syntax and partially evaluate?
- a higher-level language with binding specifications, synthesized substitution and contextual matching that compiles to a closure-based semantics and reified continuations.
[1] Might and Shivers ICFP 2006 "Improving flow analyses via ΓCFA: Abstract garbage collection and counting"