/morpheus

The code repo for tool morpheus

Primary LanguageOCaml

Morpheus

A Refinement Typed Parser Combinator DSL.

Dependencies:

  1. OCaml (Version >= 4.03)
  2. Z3
  3. OCamlLex

To build:

cd <project-root>
./build.sh <path-to-testfile>/testfile.native

This generates a testfile.native in the /outputs directory

To run:

./outputs/testfile.native <path-to-testfile>/testfile.spec

Example

./build.sh tests/unit/unit1.native 
./outputs/unit1.native tests/unit/unit1.spec

Directory Structure

  • Type/Specification Language : /speclang/specLang.ml
  • Program/Term Language : /synlang/lambdasyn.ml
  • Typing Rules : /typechecking/syntypechecker.ml
  • Unit and other tests : /tests/unit/
  • Morpheus benchmarks : /benchmarks/safeparse/
  • Verification Conditions : /typechecking/verificationC.ml
  • VCtoZ3 Encoding : /vcencode/vcencode.ml