search

meta-logic / sml-to-coq

A tool that translates SML code to Coq
GNU General Public License v3.0
6 stars 0 forks source link

readme

sml-to-coq

A tool that translates SML code to Coq

Installation

Sml-to-coq uses:

Clone the project:

 $ git clone --recurse-submodules https://github.com/meta-logic/sml-to-coq.git

Building the Coq Basis Library

Since most SML programs will make use of some part of SML's basis library, we have implemented Coq equivalents to them.

To compile the Coq Basis Library:

  1. From the top level directory, go to coqBasisLib/libs
  2. Then run: $ make

Using the tool

At the top level directory, run:

 $ sml -m sources.cm

Generator

The main function for generating the Coq code is Generator.generate() in generator.sml. It generates a .v file from the passed .sml file.

generate(inputFile, outputFile): string * string -> unit
For example:
Generator.generate("smlCode.sml", "gallinaCode.v");

Generates the file galllinaCode.v from the file smlCode.sml . The file galllinaCode.v will be located at the top level directory.

To run gallinaCode.v using coqide:

  1. From the top level go to coqBasisLib/libs
  2. Then run: $ coqide
  3. From coqide's GUI open gallinaCode.v
  4. Run the file

Convertor

The main function for translating SML code is Convertor.convert() in convertor.sml. It takes as a parameter a .sml file path to the SML program to be translated, and returns the corresponding Gallina AST. 

Convertor.convert(inputFile): string -> Gallina.sentence list
For example:
Convertor.convert("smlCode.sml"):

Returns Gallina's AST of the sml code in smlCode.sml, and also it prints it.

Important Directories