Purely functional IO for Coq

Hello World in Coq

```coq From SimpleIO Require Import SimpleIO. From Coq Require Import String.

[local] Open Scope string_scope.

Definition main : IO unit := print_endline "Hello, world!".

RunIO main. ```

The coq-simple-io library provides tools to implement IO programs directly in Coq, in a similar style to Haskell.

• IO monad
• Bindings to OCaml standard library
• RunIO command for running programs

Facilities for formal verification are not included. There is no canonical way to describe the effects of the arbitrary foreign constructs that this library allows, so this library commits to none.

A possible workflow is to generalize your program to any monad with a certain interface, specialize it to a mathematical monad (e.g., state, or free monad) for formal verification, and to IO for execution. coqffi provides a toolchain for generating such interfaces from OCaml interfaces.

Installation

From OPAM

opam install coq-simple-io

From this repository as a local package

```

Clone this repository

git clone https://github.com/Lysxia/coq-simple-io

Register it with opam (the last argument is the path to the repo)

opam pin add coq-simple-io ./coq-simple-io ```

Documentation

The documentation of the latest released version is available on website at https://lysxia.github.io/coq-simple-io/toc.html

Consult the OCaml user manual for detailed description of extracted code.

Interface

To use this library:

```coq Require Import SimpleIO.SimpleIO.

(* And to use the monadic notations: *) Import IO.Notations. Local Open Scope io_scope.

(* Equivalent notations can be found ext-lib, using its [Monad] type class. *) ```

Combinators for IO actions.

```coq Parameter IO : Type -> Type.

Module IO.

Parameter ret : forall {a}, a -> IO a. Parameter bind : forall {a b}, IO a -> (a -> IO b) -> IO b. Parameter fix_io : forall {a b}, ((a -> IO b) -> (a -> IO b)) -> a -> IO b. (* etc. *)

Module Notations. Notation "c >>= f" := (bind c f) Notation "f =<< c" := (bind c f) Notation "x <- c1 ;; c2" := (bind c1 (fun x => c2)) Notation "e1 ;; e2" := (_ <- e1%io ;; e2%io)%io Notation delay io := (delay_io (fun _ => io)). End Notations.

End IO. ```

Define IO actions

The IO type extracts to the following definition in OCaml:

ocaml (* Implicitly [forall r, (a -> r) -> r]. *) type 'a coq_IO = ('a -> Obj.t) -> Obj.t

So an effectful function f : t -> u -> v in OCaml can be wrapped as a Coq function f : t -> u -> IO v in the following way:

coq Parameter f : t -> u -> IO v. Extract Constant f => "fun a b k -> k (f a b)".

Basically, add an extra parameter k and apply it to the OCaml function call.

This boilerplate can also be generated from OCaml interfaces using coqffi.

Run

The RunIO command extracts and runs an action of type IO unit.

```coq Definition main : IO unit := print_endline "Hello, world!".

RunIO main. ```

Run as a command-line script

You can run a .v file from the command line with coqc. To forward stdin and stdout to your RunIO scripts, set the option RunIO IOMode Forward.

```coq From SimpleIO Require Import SimpleIO. Import IO.Notations.

RunIO IOMode Forward.

Definition cat : IO unit := _ <- catcheof (IO.fixio (fun f _ => input <- readline ;; printendline input ;; f tt :> IO unit) tt) ;; IO.ret tt.

RunIO cat. ```

Configuration

```coq (* Open MyModule at the top of the extracted code *) RunIO Open "MyModule".

(* Build with ocamlfind (default) *) RunIO Builder Ocamlfind.

(* Build with dune, specifying a dune file. *) RunIO Builder Dune "dune".

(* Build with ocamlbuild. It must be installed separately.

 opam install ocamlbuild

*) RunIO Builder Ocamlbuild.

(* RunIO Builder can also take extra arguments for the build command in a string. *) RunIO Builder Ocamlfind "-rectypes".

(* Include my-package when compiling (only for builders Ocamlfind and Ocamlbuild; Dune is configured via the dune file). *) RunIO Package "my-package".

(* Copy my-directory to the build location so it will be visible to ocamlbuild or dune. *) RunIO Include "my-directory".

(* Enable or disable automatic detection of common dependencies (on by default): - zarith for bigint representation of integers - coq-core.kernel for Uint63 *) RunIO Smart On. RunIO Smart Off. ```

New RunIO options may be added in the future. To avoid risks of future collisions with the main RunIO command, use names with a lower case initial (like RunIO main), or put the action name in parentheses (like RunIO (Builder) to run the IO action Builder).

Library organization

The source code can be found under src/.

• SimpleIO.SimpleIO: Reexports default modules.

Default modules

The following modules are imported with SimpleIO.SimpleIO.

• SimpleIO.IO_Monad: Definition of IO and basic combinators.
• SimpleIO.IO_Stdlib: Wrappers around Stdlib from OCaml's standard library.
• SimpleIO.IO_StdlibAxioms: Basic theory for pure Stdlib functions.
• SimpleIO.IO_Exceptions: Catch common exceptions.
• SimpleIO.IO_RawChar: Utilities that rely on ExtrOcamlString.
• SimpleIO.IO_String: Operations on OCaml strings.

Auxiliary modules

The following module can be imported separately. They correspond to modules from the OCaml standard library.

• SimpleIO.IO_Bytes: Mutable byte sequences.
• SimpleIO.IO_Random: Pseudo-random number generators (PRNG).
• SimpleIO.IO_Float: Floating-point arithmetic.
• SimpleIO.IO_Unix: Interface to the Unix system.
• SimpleIO.IO_Sys: System interface.

Unsafe modules

• SimpleIO.IO_Unsafe: Unsafe operations.
• SimpleIO.IO_UnsafeNat: Pervasives functions adapted to nat (unsafety because of overflow and underflow).

Related

• coqffi
• Ynot
• Coq.io