Introduction to FreeSpec.Exec

The present document remains a draft and must be considered as such.

Coq notably provides a nice purely functional language with dependent type called Gallina to write specifications, and facilities (including a tactic language called Ltac) to reason about their correctness. Unfortunately, Gallina has long and infamously been known as “the language with no hello world.” Although Coq has a nice feature called program extraction to turn Gallina specifications into executable Ocaml programs, it has remained cumbersome to use. The result of this situation is the small amount of “Coq flagship projects” (eg. CompCert).

FreeSpec.Exec, an extensible plugin provided by the FreeSpec framework, is an attempt to improve this situation by making it easy to execute Gallina specifications with side effects with coqc only. There is no need to deal with extraction-related burden anymore.

For instance, here is how you write a hello world program in Coq using FreeSpec.Exec.

Require Import FreeSpec.Program.
Require Import FreeSpec.Stdlib.Console.

Definition hello {ix} `{Use Console.i ix}
  : Program ix unit :=
  Console.echo "Hello, world!".

Exec hello.

And executing this program is simply a matter of calling coqc.

$ coqc hello.v
Hello, world!

Getting Started

FreeSpec.Exec remains in an early stage of development. While the core of the plugin already works as intended, too few useful interfaces are supported at the moment.

Fortunately, because FreeSpec.Exec is extensible, you can already start experimenting with it by defining your own interfaces.

Extending FreeSpec.Exec

FreeSpec.Exec is extensible, meaning it is easy for Coq developers to define their interfaces, implement primitive semantics in dedicated OCaml plugins, and enjoy coqc being able to execute programs written thanks to these primitives.

Defining Effectful Semantics

In FreeSpec, primitives are modeled with Coq terms, and in FreeSpec.Exec, an effectful_semantic of a given primitive is an OCaml function which computes a result given the list of arguments of a particular primitive.

In FreeSpec.Exec, effectful_semantic is defined in OCaml as follows:

type effectful_semantic =
  Constr.constr list -> Constr.constr

… where the Constr.constr type (as defined in the Coq source in the kernel/constr.ml file) allows for describing (and manipulating) Coq terms. Hopefully, you should not have to learn how Coq works under the hood and Constr.constr in particular, as FreeSpec.Exec intends to provide facilities to fill the gap between Coq and OCaml world.

Coq	OCaml	to OCaml	from OCaml
Z	int	int_of_coqz	int_to_coqz
bool	bool	bool_of_coqbool	bool_to_coqbool
ascii	char	char_of_coqascii	char_to_coqascii
string	bytes	bytes_of_coqascii	bytes_to_coqstr
string	string		string_to_coqstr
unit			coqtt

Let’s have a look with a concrete example. FreeSpec comes with a simple package called FreeSpec.Stdlib.Console whose purpose is to provide simple primitives to read from the standard input and write to the standard output.

The interface in FreeSpec.Stdlib.Console is defined as follows:

Module Console.
  Inductive i: Type -> Type :=
  | Scan: i string
  | Echo: string -> i unit.
End Console.

Scan of type Console.i unit is intended to be a primitive to read one line from the standard input, while Echo s of type Echo unit is inteded to be the primitive to write the string s into the standard output.

In FreeSpec.Stdlib.Console, the effectful semantic of scan is implemented as follows:

let scan = function
  | [] -> string_to_coqstr (read_line ())
  | _ -> assert false

We convert the result of read_line () (of OCaml type string) into a Constr.constr value using string_to_coqstr. Because scan does not have any parameter, we raise an error if a non-empty list is passed to us as input. In such a case, this means there is a bug in FreeSpec.Exec, or that the Coq definition of Scan as been changed.

The effectful_semantic of Echo is not harder to write:

let echo = function
  | [str] -> print_bytes (bytes_of_coqstr str);
             coqtt
  | _ -> assert false

We convert the Coq term passed as an argument of Echo using bytes_of_coqstr, then we send it to the standard output using print_bytes. We then return a Coq term (tt) whose Constr.constr representation in OCaml is coqtt.

Registering with FreeSpec.Exec

Now that we have defined effectful semantics for the primitives of Console.i, we have everything we need to emulate in OCaml the missing piece of Program evaluation, that is a function of type:

forall {A: Type}, Console.i A -> A

The next and last step is to let FreeSpec.Exec know about these semantics (“to register our effectful_semantics”).

The Extends module provides a function to that end:

val register_interface :
 (* The path of the module within the interface type
    lives. *)
    string list
 (* A list to map each constructor of this interface
    to an effectfull semantic. *)
 -> (string * effectful_semantic) list
 -> unit

The type signature of register_interface is pretty self-explanatory.

let _ =
  register_interface
    ["FreeSpec"; "Stdlib"; "Console"; "Console"]
    [("Scan", scan); ("Echo", echo)]

Conclusion

FreeSpec.Exec provides a novel approach to turn Gallina into a real programming language. It currently lacks a comprehensive library of primitives, but it is extensible so that you do not have to wait for us to start testing it.