A tutorial-style implementation of liquid/refinement types for a subset of Ocaml/Reason.

1. Get Z3

Download from here and make sure z3 is on your $PATH

2. Clone the repository

git clone git@github.com:ranjitjhala/sprite-lang.git
cd sprite-lang

3. Build

Using stack

stack build

Tested with GHC 8.10.7. If you run into LLVM-related errors, especially on an Apple M1 machine, install llvm@13 using homebrew.

stack exec -- sprite 8 test/L8/pos/listSet.re

The 8 indicates the language level -- see below.

When you run sprite N path/to/file.re the generated Horn-VC is saved in path/to/.liquid/file.re.smt2.

So, for example:

stack exec -- sprite 8 test/L8/pos/listSet.re

will generate a VC in

test/L8/pos/.liquid/listSet.re.smt2

• Lang1: STLC + Annot (refinements 101)
• Lang2: "" + Branches (path-sensitivity)
• Lang3: "" + *-refinements (inference + qual-fixpoint)
• Lang4: "" + T-Poly (type-polymorphism)
• Lang5: "" + Data (datatypes & measures)
• Lang6: "" + R-Poly (refinement-polymorphism)
• Lang7: "" + Termination (metrics + invariants)
• Lang8: "" + Reflection (proofs)