package coq-of-ocaml

  1. Overview
  2. Docs
Compile a subset of OCaml to Coq

Install

Dune Dependency

Authors

Maintainers

Sources

2.2.1.tar.gz
sha256=3185fe93e13ce05f409307f04f30de4cbbbdd644b85570f2ef629780b57af174
sha512=835ca0b5f464c602317dedf55c15ca7e4d0f99c88fdda925a595632fe8dc63f6c15e6f4a5578bd211d9fab4fae44d7e61235af786e30f8bb1b2454f55faa6269

Description

README

coq-of-ocaml

https://clarus.github.io/coq-of-ocaml/

Start with the file main.ml:

type 'a tree =
  | Leaf of 'a
  | Node of 'a tree * 'a tree

let rec sum tree =
  match tree with
  | Leaf n -> n
  | Node (tree1, tree2) -> sum tree1 + sum tree2

Run:

coq-of-ocaml main.ml

Get a file Main.v:

Require Import OCaml.OCaml.

Local Open Scope Z_scope.
Local Open Scope type_scope.
Import ListNotations.

Inductive tree (a : Set) : Set :=
| Leaf : a -> tree a
| Node : tree a -> tree a -> tree a.

Arguments Leaf {_}.
Arguments Node {_}.

Fixpoint sum (tree : tree Z) : Z :=
  match tree with
  | Leaf n => n
  | Node tree1 tree2 => Z.add (sum tree1) (sum tree2)
  end.

Features

  • core of OCaml (functions, let bindings, pattern-matching,...) ✔️

  • type definitions (records, inductive types, synonyms, mutual types) ✔️

  • modules as namespaces ✔️

  • modules as dependent records (signatures, functors, first-class modules) ✔️

  • projects with complex dependencies using .merlin files ✔️

  • .ml and .mli files ✔️

  • existential types ✔️

  • partial support of GADTs 🌊

  • partial support of polymorphic variants 🌊

  • ignores extensible types ❌

  • ignores side-effects ❌

Even in case of errors we try to generate some Coq code. The generated Coq code should be readable and with a size similar to the OCaml source. One should not hesitate to fix remaining compilation errors, by hand or with a script (name collisions, missing Require,...).

Install

Latest stable version

Using the package manager opam, add the Coq repository:

opam repo add coq-released https://coq.inria.fr/opam/released

and run:

opam install coq-of-ocaml

Current development version

To install the current development version:

opam pin add https://github.com/clarus/coq-of-ocaml.git#master

Manually

Read the coq-of-ocaml.opam file at the root of the project to know the dependencies to install and get the list of commands to build the project.

Usage

coq-of-ocaml compiles the .ml or .mli files using Merlin to understand the dependencies of a project. One first needs to have a compiled project with a working configuration of Merlin. The basic command is:

coq-of-ocaml file.ml

If this does not work as expected, you may specify the path to a .merlin file:

coq-of-ocaml -merlin src/.merlin path/file.ml

You can start to experiment with the test files in tests/ or look at our online examples.

License

MIT © Guillaume Claret.

Dependencies (5)

  1. yojson >= "1.6.0"
  2. smart-print
  3. ocamlfind >= "1.5.2"
  4. ocaml >= "4.09" & < "4.10"
  5. dune >= "1.11" & < "2.8"

Dev Dependencies

None

Used by

None

Conflicts (1)

  1. coq < "8.11"
OCaml

Innovation. Community. Security.