🐓 September 28, 2019
In order to make coq-of-ocaml usable on a maximum of OCaml programs, we should handle mutually recursive types. We show how we import these types to Coq and the main differences between the two languages. As a result, more OCaml programming patterns should be supported by coq-of-ocaml.
We develop coq-of-ocaml at 🐙 Nomadic Labs with the aim to formally verify OCaml programs, and in particular the implementation of the crypto-currency Tezos. If you want to use this tool for your own projects, please do not hesitate to look at our website or contact us!
Take the following mutually recursive definition of a tree in OCaml:
type 'a tree = Tree of 'a node list
and 'a node =
| Leaf of 'a leaf
| Node of 'a tree
and 'content leaf = string * 'content
By applying coq-of-ocaml on this code we get:
Reserved Notation "'leaf".
Inductive tree (a : Type) : Type :=
| Tree : (list (node a)) -> tree a
with node (a : Type) : Type :=
| Leaf : ('leaf a) -> node a
| Node : (tree a) -> node a
where "'leaf" := (fun (content : Type) => string * content).
Definition leaf := 'leaf.
Arguments Tree {_}.
Arguments Leaf {_}.
Arguments Node {_}.
We transform algebraic data types to Coq’s inductive types. We use a notation to implement the type synonym leaf. This is a trick because Coq only supports inductive types in mutual definitions. See the documentation on notations for more information. We rename the leaf type parameter 'content instead of 'a to avoid a name collision in Coq. The type parameters of the constructors are set implicit with the command Arguments to keep the behavior of OCaml.
We handle type ... and ... definitions with algebraic data types (including GADTs, “Generalized Algebraic Data Types”) and type synonyms. We do not handle abstract types. For records in mutual definitions, one can use a type synonym to a more generic record. For example:
type expression =
| Number of int
| Operation of operation
and operation = {
name : string;
parameters : expression list }
can be rewritten as:
type 'a operation_skeleton = {
name : string;
parameters : 'a list }
type expression =
| Number of int
| Operation of operation
and operation = expression operation_skeleton
in order to be imported into Coq.
In Coq, there is a distinction between type variables on the left (type parameters) and on the right of the : (type indices):
Inductive t (A1 A2 ... : Type) : forall (B1 B2 ... : Type), Type :=
| Constr1 : ... -> t A1 A2 ... C1 C2 ...
| ...
The variables Ai do not behave the same as the variables Bi. Type parameters have the constraint of being the same for each constructor. When used, they simplify the typing of the pattern matching. Typically, in GADTs, type variables are type indices while in non-generalized algebraic data types they are type parameters. In mutually recursive inductive types there is one more constraint: the type parameters must be the same for each type. We consider a type variable to be a parameter if it appears with the same name in each OCaml constructor and in the type definition. For example:
type ('a, 'b) arith =
| Int : 'a * int -> ('a, int) arith
| Eq : 'a * ('a, int) arith * ('a, int) arith -> ('a, bool) arith
| Plus : 'a * ('a, int) arith * ('a, int) arith -> ('a, int) arith
is imported to:
Inductive arith (a : Type) : forall (b : Type), Type :=
| Int : a -> Z -> arith a Z
| Eq : a -> (arith a Z) -> (arith a Z) -> arith a bool
| Plus : a -> (arith a Z) -> (arith a Z) -> arith a Z.
Arguments Int {_}.
Arguments Eq {_}.
Arguments Plus {_}.
Here we transform 'a to a type parameter and 'b to a type index.
Many OCaml programs define all types as mutually recursive by default. In Coq this is usually very difficult as:
In practice, I would recommend to find a way to avoid mutually recursive types when possible. For cases they are used, I hope this import mechanism to be useful.
blog comments powered by Disqus