Slepice

Prototype type-inference engine for LF via proof-relevant resolution.

Prerequisites

The following tools need to be available before building slepice:

• Ocaml development environment
• Coq
• Ott version 0.25 (https://github.com/ott-lang/ott)

Optionally (for slepice_wrapper):

• Elpi (https://github.com/LPCIC/elpi)

A local copy of ott and elpi can be installed by running the configure script.

Documentation further requires latex distribution available with latex-extra and xcolor packages.

Installation

The command make builds the slepice binary. The command make doc builds documentation in the doc/ subdirectory.

Usage

usage: slepice <options> -sig <filename> -term <filenamen> [ -o <basename> ]

  -sig <filename>         Input signature
  -term <filename>        Input term
  -o <basename>           Output files basename
  -print-sig <false>      Print parsed signature
  -print-term <false>     Print parsed term
  -print <false>          Print parsed signature and term
  -help                   Display this list of options
  --help                  Display this list of options

The binary either displays the generated logic program and goal or, when a basename is provided, it generates files basename.prog and basename.g with the generated program and the generated goal respectively.

Documentation

The directory doc/ contains html documentation generated from Coq and the file slepice.pdf that contains an overview of Ott grammar.

Examples

The example fromJust:

fromJust.sig            signature
fromJust-tc.sig         fully elaborated example for type checking

Run the following command to see output of slepice:

./slepice \
    -sig examples/fromJust.sig \
    -term examples/fromJust.tt

Run the following command to see a solution resolved by ELPI

./slepice_wraper \
    examples/fromJust.sig \
    examples/fromJust.tt