Skip to content

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

License

Notifications You must be signed in to change notification settings

ranjitjhala/sprite-lang

Repository files navigation

SPRITE

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

Install

1. Get Z3

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

2. Clone the repository

$ git clone [email protected]:ranjitjhala/sprite-lang.git
$ cd sprite-lang

3. Build

Using stack

$ stack build

or

$ cabal v2-build

Run on a single file

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

The 8 indicates the language-level -- see below.

Horn VC

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

Languages

  • [*] 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)

About

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

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published