Grisette: Symbolic Compilation as a Functional Programming Library
summary
Grisette is a Haskell library that compiles programs symbolically by evaluating all paths and merging states into a normal form that avoids pairwise exclusive guards; its ordered-guards representation plus hierarchical, sorted unions shrinks constraint terms and speeds solving — the paper reports about 5-fold smaller constraints and >2× faster solving versus prior tools. It is purely functional, statically typed, supports memoization and monadic integration, uses SBV backends, ships BSD‑3 on GitHub, and demos synthesis (finds x+3).
AI-written summary · about
chapters (11)
- 0:00Start
- 3:50Reusable symbolic compilers
- 6:29Reusable symbolic compiler as a library
- 7:36Design goals
- 8:05An example program
- 8:46MEG (Mutually Exclusive Guards)
- 9:59Sources of duplications in MEG vs. ORG
- 11:56Merging complex types in ORG
- 13:38Evaluation settings
- 17:47Discussion 1: Stateful programming with Grisette
- 19:56A minimal synthesizer