Commit 94c4a59b authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

notes de cours de la seance 6 : modules, records, extraction

parent 6b935db0
Require Import List.
Import ListNotations.
(** * Partie 1 : Modules *)
(** Exemple de "module type". On parle aussi de signature, ou
d'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.
(** Exemple d'implémentation de cette signature.
Avec "<:" à la ligne ci-dessous, Coq vérifie que les
définitions de Bar sont compatibles avec Foo.
Mais Bar n'est pas restreinte ensuite.
*)
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)
end.
(* Note: l'implémentation peut contenir des éléments en plus que Foo. *)
Definition truc := 1 + 2.
Definition length := @List.length.
End Bar.
Print Bar.t.
Compute (Bar.cons _ 1 Bar.empty).
(** Si on met ":" au lieu de "<:" dans la définition d'un
module, les détails internes ne sont plus visibles ensuite,
il ne reste que les infos fournis par Foo. En particulier,
plus de calculs possibles.
*)
Module RestrictedBar : Foo := Bar.
Print RestrictedBar.t.
Compute (RestrictedBar.cons _ 1 (RestrictedBar.empty _)).
(** Un "functeur" (functor en anglais) est un module paramétré
par un autre module.
*)
(** Exemple: à partir de [Foo], on peut proposer des fonctions
[head] et [tail] *)
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.
(** Pour l'instant ceci ne crée pas de nouvelles fonctions concrètes. *)
Fail Print HeadTail.head.
(** Mais on peut s'en servir de manière générique sur toute implémentation
de [Foo]. *)
Module BarHdTl := HeadTail(Bar).
Print BarHdTl.head.
Compute BarHdTl.head [1;2].
(** On peut même étendre un module, via une notion d'inclusion. *)
Module Bar2.
Include Bar.
Include HeadTail(Bar).
End Bar2.
(** Syntaxe plus légère pour la même chose: *)
Module Bar3 := Bar <+ HeadTail.
(** Autre exemple de foncteur: à partir d'un premier module
satisfaisant l'interface [Foo], on peut en bâtir un autre
pour lequel la fonction [length] sera en temps constant.
Pour cela, on stocke cette taille, c'est un exemple typique
de compromis entre temps et espace. *)
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))
end.
Definition length A (l:t A) := snd l.
End FastLength.
(** Un dernier exemple de foncteur: utilisation de la stdlib
de Coq pour fabriquer des ensembles finis efficaces. *)
Require Import Arith MSets MSetAVL.
(** L'interface des ensembles finis: *)
Print MSetInterface.S.
(** Un foncteur fabriquant une telle structure d'ensemble fini: *)
Print MSetAVL.Make.
(** Ce qu'il faut pour pouvoir utiliser ce foncteur: *)
Print Orders.OrderedType.
(** Hormis les parties specifications et preuves, il s'agit
essentiellement de fournir une fonction [compare]... *)
Print comparison.
(** Il se trouve que le module [Nat] fourni par [Arith] contient
déjà tout ce qu'il faut, ce qu'on peut vérifier ainsi: *)
Module Nat' <: Orders.OrderedType := Nat.
(** Fabrication d'un module d'ensembles finis d'entiers naturels *)
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.
(** * Partie 2 : Records *)
(** Il s'agit d'une syntaxe particulière pour des types inductifs
à un seul constructeur. *)
(** Jusqu'ici, on pouvait utiliser le type des paires Coq *)
Definition truc := (1,true).
(** Ou définir un type ad-hoc via [Inductive], pas limité
à deux arguments. *)
Inductive montruc :=
| Truc : nat -> bool -> (nat -> nat) -> montruc.
Check (Truc 1 true pred).
(** Autre possibilité : *)
Record monrecord :=
{ position : nat;
flag : bool;
next : nat -> nat;
}.
Print monrecord.
Check Build_monrecord. (** constructeur, au nom engendré par Coq *)
(** Principal intérêt : chaque champs est nommé, idéalement
avec un nom significatif, plus besoin de se souvenir de
l'ordre des choses. *)
(** On peut bâtir une valeur record comme ceci : *)
Definition exemple_record :=
{| position := 1; flag := true; next := pred |}.
(** Ou bien utiliser le nom de constructeur que Coq a généré
pour nous : [Build_monrecord]. *)
Definition exemple_record' := Build_monrecord 1 true pred.
(** On peut aussi donner nous-même le nom du constructeur *)
Record monrecord' := Make_monrecord' { foo : nat; bar : bool}.
(** Syntaxe de projection [r.(...)] pour accéder à un champ: *)
Compute exemple_record.(flag).
(** Une extension des records non présentée ici faute de temps :
les "type classes" *)
(** * Partie 3 : Extraction *)
(** L'extraction Coq est un traducteur de code Coq vers OCaml ou
Haskell. Cela permet d'intégrer du code Coq (idéalement spécifié
et certifié en Coq) dans des programmes plus larges, permettant
par exemple des entrées/sorties, ou toute autre chose non
directement faisable en Coq. *)
(** Les garanties théoriques de l'extraction :
- si une fonction extraite est lancée en OCaml ou en Haskell
sur des valeurs qui auraient pu être exprimées en Coq, alors
le calcul se déroulera jusqu un résultat compatible avec
le résultat qu'on aurait eu en Coq. Les seules erreurs possibles
lors du calcul sont celles liées à un épuisement des ressources
de la machine (out-of-memory, stack overflow, etc).
Informellement, cela signifie que les propriétés que l'on a prouvé
sur le code Coq continuent à être valide sur le code obtenu par
extraction.
Attention, le résultat précédent ne tient que si le code Coq
d'origine n'utilisait pas d'axiomes incohérents. La présence
d'axiomes incohérents peut amener à du code extrait qui boucle,
ou bien même qui crashe (!).
Attention également aux arguments qu'on donne à une fonction
extraite. En OCaml (ou Haskell), il est possible par exemple de
définir une donnée cyclique [let rec maliste = 1 :: maliste].
Si on donne cette donnée en argument à la fonction extraite
de [List.length], on obtient un calcul infini et l'extraction
n'y est pour rien. Ceci signifie juste que [maliste] n'est pas
une valeur "qui aurait pu être exprimé en Coq".
*)
(** L'extraction en pratique : pour le fragment de Coq qu'on a vu
jusqu maintenant, l'extraction est principalement un ajustement
de la syntaxe. Par contre:
- En cas de présence de portions de preuves dans le coq Coq,
l'extraction va enlever ces preuves.
- Et si les types Coq ne sont pas traduisibles dans le langage
cible, on contourne les limitations du typage cible en utilisant
des approximations des types et des primitives "unsafe" du
langage cible ([Obj.magic] en OCaml, [unsafeCoerce] en Haskell).
*)
(** Exemple *)
Fixpoint fact n :=
match n with
| 0 => 1
| S n => (S n) * fact n
end.
Compute fact 8.
Require Extraction.
(** Extraction non-recursive : juste une fonction *)
Extraction fact.
(** On obtient:
let rec fact = function
| O -> S O
| S n0 -> mul (S n0) (fact n0)
*)
(** La même en Haskell *)
Extraction Language Haskell.
Recursive Extraction fact.
Extraction Language OCaml.
(** fact et ses dépendences (y compris types) *)
Recursive Extraction fact.
(** On obtient:
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)
*)
(** Le code issue d'un [Recursive Extraction] peut normalement être
copié-collé dans un fichier OCaml ou directement dans un "toplevel"
OCaml. D'habitude, il est plus pratique de laisser Coq écrire
un fichier extrait pour nous: *)
Extraction "fact.ml" fact.
(** On peut ensuite soit charger ce fichier dans un toplevel,
via la directive [#use "fact.ml";;], soit intégrer ce fichier
dans un programme et le compiler. *)
(** Exemple de session en OCaml après cette extraction:
#use "fact.ml";;
(* attention, pas de jolie syntaxe par défaut ici *)
fact (S (S (S (S (S (S (S O)))))));;
(* on peut écrire des fonctions de conversions entre int et nat ... *)
let rec n2i = function O -> 0 | S n -> 1+n2i n;;
let rec i2n = function 0 -> O | n -> S (i2n (n-1));;
(* ... puis "enrober" la fonction extraite pour en faire une int->int *)
let ocaml_fact n = n2i (fact (i2n n));;
let _ = ocaml_fact 8;; (* 40320 *)
let _ = ocaml_fact 9;; (* stack overflow *)
*)
(** Concernant le "stack overflow" ci-dessus : un calcul inefficace
en Coq ne devient pas miraculeusement efficace après extraction...
Pour calculer plus sérieusement avec des gros nombres, utilisons
plutôt le type Coq [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.ml" Nfact.
(** Exemple de session en OCaml après cette extraction:
#use "nfact.ml";;
(* fonctions de conversions entre positive et int puis entre n et 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 *)
*)
(** Notez que le résultat obtenu pour [!30] est plus petit que celui
pour [!20], ce qui ne devrait pas être le cas. En fait, on a dépassé
les capacités du type OCaml [int], pour lequel [max_int = 2^62-1].
L'extraction n'y est pour rien, le résultat de [nfact (i2n 30)] est
bien correct, c'est la conversion vers [int] ensuite qui n'est exacte
qu un "modulo" près. Ici il faudrait utiliser pour l'affichage
des entiers OCaml en précision arbitraire (cf [Big_int] ou
bibliothèque OCaml [zarith]). Ou le type [Integer] en Haskell. *)
(** Exemple d'extraction utilisant des types Coq non expressibles en
OCaml: On reprend la séance sur les types dépendants. *)
Fixpoint narity n :=
match n with
| 0 => nat
| S n => nat -> narity n
end.
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)
end.
Definition narity_sum n : narity n :=
match n with
| 0 => 0
| S n => narity_S_sum n
end.
Compute narity_sum 4 5 1 2 3 : nat. (* 5 + 1 + 2 + 3 = 11 *)
Recursive Extraction narity_sum. (* quelques [Obj.magic] ... *)
(** Autre exemple : reprendre le code des vecteurs et l'extraire.
On obtient alors après extraction un type [vect] très proche
des listes standards, avec juste un entier en plus dans le
constructeur [Vcons], qu'on peut éventuellement enlever
(cf. la commande expérimentale [Extraction Implicit]).
Et [Vcast] devient juste une identité. *)
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