The Coq source of this tutorial is available here.
Make sure that you added the Coq repository:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-cybele
Here is our first program:
Require Import Cybele. Require Import String. Import Monad. Definition hello := print_string (sig := Sig.empty) "Hello world!".
It prints a message in the Cybele monad. If we check its type:
M Sig.empty unit. So we return a value of type
unit in the monad. The
Sig.empty tells we are using no memory. We run it:
Compute run hello 0.
The message is written in the output trace.
We write the return operation
ret. For the bind, we postfix common constructs by a
Compute run (sig := Sig.empty) ( let! x := ret 12 in do! print_string "Twelve: " in print x) 0.
let! does the bind. The
do! sequences two instructions. We see that
It is nice to run programs in the Cybele monad. But we ultimately want to extract their results to proofs in order to write decision procedures. Here comes the
Lemma easy: True. cybele (ret (sig := Sig.empty) I). Defined.
It extracts from an expression of type
M sig A a value of type
A (if the computation successes). For this example the proof of
True is trivially
I. In order to save space, the proof is implemented by reflexivity:
proof_by_reflection (ret I) ... eq_refl. The proofs holds the full monadic expression which is executed at type-checking time.
We do not need to prove termination to write recursive functions:
Require Import Arith.Div2. Definition log2: nat -> M Sig.empty nat := fix_ (fun log2 n => match n with | 0 | 1 => ret 0 | _ => let! r := log2 (div2 n) in ret (r + 1) end).
The general fixpoint operator is
dependent_fix in a dependently typed form. We compute the logarithm in base two without giving the induction principle for recursive calls on
div2. But if we evaluate directly:
Compute run (log2 256) 0.
"Not terminated". We need to feed in the maximal number of steps allowed, let us say 100 for safety:
Compute run (log2 256) 100.
Now we get
8. We could even write non-terminating programs:
Definition infinite: unit -> M Sig.empty unit := fix_ (fun infinite _ => infinite tt).
We often need to write partial functions, especially in the case of decision procedures which work only on valid inputs. If we rewrite the logarithm function to handle the zero case:
Definition log2_error: nat -> M Sig.empty nat := fix_ (fun log2_error n => match n with | 0 => error "Log of zero." | 1 => ret 0 | _ => let! r := log2 (div2 n) in ret (r + 1) end).
we get an exception running it on zero. It is possible to catch them with the
Compute run (try! log2_error 0 with _=> ret 0) 100.Finally, we can lift option types to the monad using
Compute run (sig := Sig.empty) (extract_some (Some 23)) 0.
The temporary memory is the main memory system, allowing to use references. Due to the type-system of Coq we need to type this dynamically allocated memory. The programmer gives a signature, the list of types which will be allocated in the memory. If we only need a natural number:
Require Import List. Import ListNotations. Definition sig := Sig.Make nil [nat: Type].
We manipulate references with a syntax similar to OCaml:
Definition twenty := let! r := tmp_ref sig 0 12 in let! v := !r in do! r :=! v + 8 in !r.
computes the value
20. Allocation is done with
tmp_ref sig 0 12, the index
0 being an index in the signature referring to the type
nat. Dereferencings and assignments are done with
If we try to allocate another
nat reference we get an error:
Definition two_refs := let! r1 := tmp_ref sig 0 12 in let! r2 := tmp_ref sig 0 14 in !r1.returns
"The reference is already allocated". This is because there can be only one allocation per element of the signature. They are two solutions for our program. We can extend the signature if we know we will allocate only two references:
Definition sig_couple := Sig.Make nil [nat: Type; nat: Type]. Definition two_refs_couple := let! r1 := tmp_ref sig_couple 0 12 in let! r2 := tmp_ref sig_couple 1 14 in !r1.Or we can use an extensible container such as a list:
Definition sig_list := Sig.Make nil [list nat: Type]. Definition two_refs_list := let! l := tmp_ref sig_list 0 [12; 14] in let! l_value := !l in extract_some (nth_error l_value 0).
It may be viewed as a limitation to have fixed number of allocations, but in practice it was always possible for us to overcome that using references to containers.
Complex results can be pre-computed efficiently by the OCaml back-end. The program is executed twice, first in OCaml (the code is generated using the extraction mechanism) and then in Coq, using results given by the first execution.
The communication between the two is done through the input memory. It has the same behavior as the temporary memory, except that its final value after the first execution is saved and given as an initial memory value to Coq. The idea is that OCaml will write in it while Coq will read it. To encode these two behaviors, there is the
select f g operator. It executes
f in Coq but
g in OCaml.