Commit f32a3339 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

seance 6 (english version)

parent cfb708ae
(** * Session 6 : more modules, records, extraction *)
Require Import List.
Import ListNotations.
(** * Part 1 : Modules *)
(** Example of "Module Type", also known as a signature, or
an interface. *)
Module Type Foo.
Parameter t : Type -> Type.
Parameter empty : forall A, t A.
Parameter cons : forall A, A -> t A -> t A.
Parameter decons : forall A, t A -> option (A * t A).
Parameter length : forall A, t A -> nat.
End Foo.
(** Example of an implementation of this signature.
With the "<:" syntax below, Coq checks that the definitions
in module Bar are compatibles with Foo.
But Bar is left unrestricted afterwards.
Module Bar <: Foo.
Definition t := list.
Definition empty {A} : list A := [].
Definition cons := @List.cons.
Definition decons {A} (l:list A) :=
match l with
| [] => None
| x::l => Some (x,l)
(* Note: the implementation can contain extra stuff not mentionned in Foo. *)
Definition truc := 1 + 2.
Definition length := @List.length.
End Bar.
Print Bar.t.
Compute (Bar.cons _ 1 Bar.empty).
(** Now, if we use the syntax ":" below instead of "<:" in the definition
of a module, all internal details will be masked afterwards, hidden
by Foo, and only the information given by Foo will be available.
In particular, this will prevent here any computation, since
the body of the definitions will be inaccessible.
So in Coq this ":" is usually far too restrictive, unlike in
languages like OCaml.
Module RestrictedBar : Foo := Bar.
Print RestrictedBar.t.
Compute (RestrictedBar.cons _ 1 (RestrictedBar.empty _)).
(** A "functeur" ("foncteur" in French) is a module parametrized
by another module.
(** Example: starting from [Foo], one may propose some [head] and
[tail] functions. *)
Module HeadTail (M:Foo).
Definition head {A} : M.t A -> option A :=
fun l => match M.decons _ l with None => None | Some (x,l') => Some x end.
Definition tail {A} : M.t A -> option (M.t A) :=
fun l => match M.decons _ l with None => None | Some (x,l') => Some l' end.
End HeadTail.
(** For now, this does not create any new concrete functions. *)
Fail Print HeadTail.head.
(** But we can use this in a generic way on any implementation of Foo. *)
Module BarHdTl := HeadTail(Bar).
Print BarHdTl.head.
Compute BarHdTl.head [1;2].
(** We can even extend a module, via a notion of inclusion. *)
Module Bar2.
Include Bar.
Include HeadTail(Bar).
End Bar2.
(** Lighter syntax for the same thing: *)
Module Bar3 := Bar <+ HeadTail.
(** Another example of functor: starting from a first module
satisfying interface Foo, we could build another one for which
the [length] function is working in constant time.
For that we store somewhere this size, and update it after
all operations. That's a typical example of time vs. space tradeoff.
Module FastLength (M:Foo) <: Foo.
Definition t A := (M.t A * nat)%type.
Definition empty A := (M.empty A, 0).
Definition cons A x (l:t A) :=
let (l,n) := l in
(M.cons A x l, S n).
Definition decons A (l:t A) :=
let (l,n) := l in
match M.decons A l with
| None => None
| Some (x,l) => Some (x,(l,pred n))
Definition length A (l:t A) := snd l.
End FastLength.
(** A last example of functor: using the Coq standard library
for building efficient finite sets. *)
Require Import Arith MSets MSetRBT.
(** The interface of finite sets: *)
Print MSetInterface.S.
(** A functor building such a structure of finite sets: *)
Print MSetRBT.Make.
(** What we need for instantiating this functor: *)
Print Orders.OrderedType.
(** Except for a few logical predicates and a few proofs, this interface
mainly asks for a type [t] and a ternary comparison function named
[compare]... *)
Print comparison.
(** Moreover the [Nat] module provided by the library [Arith]
already contains all that (just like for [N] or [Z] modules
for efficient binary numbers). Let's check this inclusion
(also called module subtyping) : *)
Module Nat' <: Orders.OrderedType := Nat.
(** So now we can build a module of finite sets of numbers. *)
Module NatSet := MSetAVL.Make(Nat).
Print NatSet.
Definition test := NatSet.add 7 (NatSet.add 8 NatSet.empty).
Compute NatSet.mem 7 test.
Compute NatSet.elements test.
(** Note that NatSet.elt is now a alias for nat. *)
Print NatSet.elt.
(** And the type NatSet.t is not abstract as it could (and should)
be in other languages, once again due to ":" being too restrictive
in Coq. But looking into the implementation details of this type
is not recommended (but not a secret either, it's a binary tree
with some proof of invariants attached to it *)
(** * Part 2 : Records *)
(** This is a particular syntax for inductive types with only
one constructor. *)
(** Up to now, we could use the type of Coq pairs, possibly nested ... *)
Definition truc := (1,true,pred). (* actually ((1,true),pred) *)
(** ... or define an ad-hoc type via [Inductive], whose constructor(s)
may have any number of arguments we see fit. *)
Inductive something :=
| Thing : nat -> bool -> (nat -> nat) -> something.
Check (Thing 1 true pred).
(** Another possibility, use a Record : *)
Record myrecord :=
{ position : nat;
flag : bool;
next : nat -> nat;
Print myrecord.
Check Build_myrecord. (** constructor, with a name generated by Coq *)
(** Main interest : each field is named, hopefully with a significant
name, no need to remember the order of the arguments. *)
(** One may build a record value like this : *)
Definition example_record :=
{| position := 1; flag := true; next := pred |}.
(** In this case, the order of fields is arbitrary *)
Check {| flag := true; next := pred; position := 1 |}.
(** It is also possible to use the constructor in a usual way.
Here the Coq-generated name is [Build_myrecord]. *)
Definition example_record' := Build_myrecord 1 true pred.
(** We could also pick our own constructor name when defining the
record type *)
Record myrecord' := Make_myrecord' { foo : nat; bar : bool}.
(** For accessing a specific field, the syntax of a projection is [r.(...)] *)
Compute example_record.(flag).
(** Coq Records has been extended in a notion called "type classes".
We won't detail them here, for more on that, see for instance:
(** * Part 3 : Extraction *)
(** The Coq extraction is an automated code translator from Coq to
OCaml or Haskell. It allows to integrate Coq code (ideally,
a code that we have specified and proved correct in Coq) into
larger, more realistic programs. For instance, this way we can
benefit from input/output parts, or any other notions that cannot
be done directly in Coq. *)
(** The main theoretical guarantee provided by the Coq extraction :
- If a extracted function is launched in OCaml or Haskell
on values that could have been expressed in Coq, then the
computation will produce a result compatible with the result
we would have had in Coq. The only possible erreurs during
this computation are exhaustion of machine resources
(out-of-memory, stack overflow, etc).
Informally, this means that any property proved on our Coq code
will continue to be valid on the code obtained by extraction.
Beware : the previous result only holds if the initial Coq code
does not depend on incoherent axioms. Otherwise, incoherent axioms
may lead to extracted code that loops forever, or even crashes !
Another caveat : the target language may provide values that
have no Coq counterparts. For instance, in OCaml (or Haskell), it
is possible to define a cyclic data [let rec mylist = 1 :: mylist].
If one gives this value as argument to the extracted version of
[List.length], the computation will never stop, and the extraction
correctness is not to blaim. Simply, [mylist] is clearly not
a "value that could have been expressed in Coq".
(** Extraction in practice. On the programming fragment of Coq, the
one we have almost exlusively considered up to now, the extraction
is mainly preforming syntactic adjustments. But:
- If the Coq code contains proof parts, the extraction removes them,
since they are sorts of assertions, and do not influence the
computation results. We say that they have no computational
- All types are also erased from extracted values, since them have
no computational content either (you cannot "match" on a type).
Moreover the target languages separate strictly between the
worlds of types and the world of values (no pairs such as
[(int,int)] in OCaml, for instance).
- Types are normally translated into types in the target language,
but this is not always possible since Coq types are way richer.
In case a Coq type has not counterpart in the target language,
we overcome this limitation by type approximations and
use of "unsage" primitives of the target language ([Obj.magic]
in OCaml, [unsafeCoerce] in Haskell).
(** Example *)
Fixpoint fact n :=
match n with
| 0 => 1
| S n => (S n) * fact n
Compute fact 8.
Require Extraction.
(** Simpliest extraction : just one definition at a time.
No recursive dependency analysis. *)
Extraction fact.
(** Here we obtain:
let rec fact = function
| O -> S O
| S n0 -> mul (S n0) (fact n0)
(** Or in Haskell: *)
Extraction Language Haskell.
Extraction fact.
Extraction Language OCaml.
(** More interesting : extracting fact and all its dependencies
(including type definition). This way we get a standalone
code fragment in OCaml (resp. Haskell). *)
Recursive Extraction fact.
(** We obtain:
type nat =
| O
| S of nat
(** val add : nat -> nat -> nat **)
let rec add n m =
match n with
| O -> m
| S p -> S (add p m)
(** val mul : nat -> nat -> nat **)
let rec mul n m =
match n with
| O -> O
| S p -> add m (mul p m)
(** val fact : nat -> nat **)
let rec fact = function
| O -> S O
| S n0 -> mul (S n0) (fact n0)
(** The code produced by [Recursive Extraction] could normally be
used unmodified in an OCaml file or sent directly to an OCaml
"toplevel". Or we could let Coq write this extracted code to
a file for us: *)
Extraction "" fact.
(** This file can then be either loaded in a toplevel, via the
command [#use "";;], or be integrated in a larger program
and be compiled and run. *)
(** Example of OCaml session after this extraction:
#use "";;
(* No nice notation for numbers here *)
fact (S (S (S (S (S (S (S O)))))));;
(* One may write conversion functions between int and (extracted) nat ... *)
let rec n2i = function O -> 0 | S n -> 1+n2i n;;
let rec i2n = function 0 -> O | n -> S (i2n (n-1));;
(* ... then "wrap" the extracted function to obtain a int->int function *)
let ocaml_fact n = n2i (fact (i2n n));;
let _ = ocaml_fact 8;; (* 40320 *)
let _ = ocaml_fact 9;; (* stack overflow *)
(** Why a "stack overflow" above ? An inefficient computation in Coq
will not become efficient by miracle after extraction...
For serious computation with big numbers, rather use Coq type [N]
Require Import NArith.
Check N.peano_rect.
Definition Nfact n : N :=
(N.peano_rect _ 1 (fun n p => (N.succ n) * p) n)%N.
Compute Nfact 8.
Extraction "" Nfact.
(** Example of OCaml session after this extraction :
#use "";;
(* Conversion functions between positive and int, then between n and int *)
let rec p2i = function XH -> 1 | XO p -> 2* (p2i p) | XI p -> 2*(p2i p)+1;;
let n2i = function N0 -> 0 | Npos p -> p2i p;;
let rec i2p i =
if i <= 1 then XH
else if i mod 2 = 0 then XO (i2p (i/2))
else XI (i2p (i/2));;
let i2n = function 0 -> N0 | n -> Npos (i2p n);;
let _ = n2i (nfact (i2n 10));; (* 3628800 *)
let _ = n2i (nfact (i2n 20));; (* 2432902008176640000 *)
let _ = n2i (nfact (i2n 30));; (* 458793068007522304 *)
(** Note that the result for [!30] is smaller than the one for [!20],
which should not be the case. In fact, the OCaml type [int] is
bounded : usually [max_int = 2^62-1].
The extracted code is fine, the result of [nfact (i2n 30)] is
indeed correct, but the conversion [n2i] toward [int] produces a
result which is accurate only up to some "modulo". Various solutions
exists to leverage this issue, for instance use some OCaml library
of arbritrary precision numbers (old [bignum] library, or the recent
[zarith] one). Or use the type [Integer] in Haskell. *)
(** Example of an extraction involving types that cannot be expressed
in OCaml : an excerpt of the session of dependent types. *)
Fixpoint narity n :=
match n with
| 0 => nat
| S n => nat -> narity n
Compute narity 5.
Fixpoint narity_S_sum n : narity (S n) :=
match n with
| 0 => fun a => a
| S n => fun a b => narity_S_sum n (a+b)
Definition narity_sum n : narity n :=
match n with
| 0 => 0
| S n => narity_S_sum n
Compute narity_sum 4 5 1 2 3 : nat. (* 5 + 1 + 2 + 3 = 11 *)
Recursive Extraction narity_sum. (* Some [Obj.magic] ... *)
(** Another example : consider again the type of Coq vectors and
extract it. This way, we obtain an OCaml type [vect] which is
very close to regular lists, with just an extra number in it
in constructor [Vcons], remnant of the size annotation.
This last remnant of a dependent type may be removed via the
use of an experimental command named [Extraction Implicit].
And [Vcast] is extracted into an identity function. *)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment