rollback sur les commandes Extract Constant/Inductive; nettoyage et documentation code

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1528 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 119 insertions, 43 deletions

diff --git a/contrib/extraction/TODO b/contrib/extraction/TODO
index 58f655b482..c2d8f44584 100644
--- a/contrib/extraction/TODO
+++ b/contrib/extraction/TODO
@@ -7,4 +7,3 @@
 
  5. Syntaxe Haskell
 
- 6. Reset sur les commandes Extract Constant/Inductive
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 7eddb932c6..57a6abc870 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -1,3 +1,12 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
 
 open Pp
 open Util
@@ -86,7 +95,10 @@ let extract_env rl =
   List.iter (visit_reference eenv) rl;
   List.rev eenv.to_extract
 
-(*s Registration of vernac commands for extraction. *)
+(*s Extraction in the Coq toplevel. We display the extracted term in
+    Ocaml syntax and we use the Coq printers for globals. The
+    vernacular command is \verb!Extraction! [term]. Whenever [term] is
+    a global, its definition is displayed. *)
 
 module ToplevelParams = struct
   let rename_global r = Names.id_of_string (Global.string_of_global r)
@@ -120,6 +132,10 @@ let _ =
 		      | Eprop -> message "prop")
        | _ -> assert false)
 
+(*s Recursive extraction in the Coq toplevel. The vernacular command is
+    \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env]
+    to get the saturated environment to extract. *)
+
 let no_such_reference q =
   errorlabstrm "reference_of_varg" 
     [< Nametab.pr_qualid q; 'sTR ": no such reference" >]
@@ -139,6 +155,10 @@ let _ =
        let rl' = decl_of_vargl vl in
        List.iter (fun d -> mSGNL (Pp.pp_decl d)) rl')
 
+(*s Extraction to a file (necessarily recursive). 
+    The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn].
+    We just call [extract_to_file] on the saturated environment. *)
+
 let _ = 
   vinterp_add "ExtractionFile"
     (function 
@@ -146,7 +166,10 @@ let _ =
 	   (fun () -> Ocaml.extract_to_file f false (decl_of_vargl vl))
        | _ -> assert false)
 
-(*s Extraction of a module. *)
+(*s Extraction of a module. The vernacular command is \verb!Extraction Module!
+    [M]. We build the environment to extract by traversing the segment of
+    module [M]. We just keep constants and inductives, and we remove
+    those having an ML extraction. *)
 
 let extract_module m =
   let seg = Library.module_segment (Some m) in
@@ -159,6 +182,10 @@ let extract_module m =
     | _ -> failwith "caught"
   in
   let rl = Util.map_succeed get_reference seg in
+  let rl = 
+    let mlset = ml_extractions () in 
+    List.filter (fun r -> not (Refset.mem r mlset)) rl 
+  in
   List.map extract_declaration rl
 
 let _ = 
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
index ba083df77a..710e801d12 100644
--- a/contrib/extraction/extract_env.mli
+++ b/contrib/extraction/extract_env.mli
@@ -1,3 +1,12 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
 
 (*s This module declares the extraction commands. *)
 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 2788fa8113..1e8b8248f2 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -595,7 +595,7 @@ and extract_constr_with_type env ctx c t =
 	     | Tarity -> Emltype (Miniml.Tarity, [], [])
 	     | Tmltype (t, sign, fl) -> Emltype (t, sign, fl))
       | (Info, NotArity) -> 
-	  (match extract_term env ctx c with 
+	  (match extract_term_with_type env ctx c t with 
 	     | Rmlterm a -> Emlterm a
 	     | Rprop -> Eprop)
  	    
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 8bc026dae3..de77687fbe 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -1,29 +1,42 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
 
 open Pp
 open Names
 open Term
 open Declarations
+open Libobject
+open Lib
 open Util
 open Miniml
 
-(*s [occurs : int -> ml_ast -> bool]
-    [occurs k M] returns true if (Rel k) occurs in M. *)
+(*s Dummy names. *)
+
+let anonymous = id_of_string "x"
+let prop_name = id_of_string "_"
+
+(*s [occurs k t] returns true if [(Rel k)] occurs in [t]. *)
 
 let rec occurs k = function
-  | MLrel i          -> i=k
-  | MLapp(t,argl)    -> (occurs k t) or (occurs_list k argl)
-  | MLlam(_,t)       -> occurs (k+1) t
+  | MLrel i -> i = k
+  | MLapp(t,argl) -> (occurs k t) || (occurs_list k argl)
+  | MLlam(_,t) -> occurs (k + 1) t
   | MLcons(_,_,argl) -> occurs_list k argl
-  | MLcase(t,pv)     -> 
-      (occurs k t) or
-      (List.exists (fun (k',t') -> occurs (k+k') t')
-      	 (array_map_to_list (fun (_,l,t') -> 
-      	       	           let k' = List.length l in (k',t')) pv))
-  | MLfix(_,l,cl)  -> let k' = List.length l in occurs_list (k+k') cl
-  | _                -> false
+  | MLcase(t,pv) -> 
+      (occurs k t) ||
+      (array_exists
+	 (fun (_,l,t') -> let k' = List.length l in occurs (k + k') t') pv)
+  | MLfix(_,l,cl) -> let k' = List.length l in occurs_list (k + k') cl
+  | _ -> false
 
-and occurs_list k l =
-  List.exists (fun t -> occurs k t) l
+and occurs_list k l = List.exists (occurs k) l
 
 (*s map over ML asts *)
 
@@ -31,7 +44,7 @@ let rec ast_map f = function
   | MLapp (a,al) -> MLapp (f a, List.map f al)
   | MLlam (id,a) -> MLlam (id, f a)
   | MLletin (id,a,b) -> MLletin (id, f a, f b)
-  | MLcons (c,n,al)  -> MLcons (c, n, List.map f al)
+  | MLcons (c,n,al) -> MLcons (c, n, List.map f al)
   | MLcase (a,eqv) -> MLcase (f a, Array.map (ast_map_eqn f) eqv)
   | MLfix (fi,ids,al) -> MLfix (fi, ids, List.map f al)
   | MLcast (a,t) -> MLcast (f a, t)
@@ -40,8 +53,10 @@ let rec ast_map f = function
 
 and ast_map_eqn f (c,ids,a) = (c,ids,f a)
 
-(*s Lifting on terms [ml_lift : int -> ml_ast -> ml_ast]
-    [ml_lift k M] lifts the binding depth of [M] across [k] bindings. *)
+(*s Lifting on terms.
+    [ml_lift k t] lifts the binding depth of [t] across [k] bindings. 
+    We use a generalization [ml_lift k n t] lifting the vars
+    of [t] under [n] bindings. *)
 
 let ml_liftn k n c = 
   let rec liftrec n = function
@@ -64,7 +79,9 @@ let ml_lift k c = ml_liftn k 1 c
 
 let ml_pop c = ml_lift (-1) c
 
-(*s substitution *)
+(*s Substitution. [ml_subst e t] substitutes [e] for [Rel 1] in [t]. 
+    It uses a generalization [subst] substituting [m] for [Rel n]. 
+    Lifting (of one binder) is done at the same time. *)
 
 let rec ml_subst v =
   let rec subst n m = function
@@ -81,8 +98,7 @@ let rec ml_subst v =
 	MLcase (subst n m t,
 		Array.map (fun (id,ids,t) ->
 			     let k = List.length ids in
-      	       		     (id,ids,subst (n+k) (ml_lift k m) t))
-		  pv)
+      	       		     (id,ids,subst (n+k) (ml_lift k m) t)) pv)
     | MLfix (i,ids,cl) -> 
 	MLfix (i,ids, 
 	       let k = List.length ids in
@@ -91,19 +107,19 @@ let rec ml_subst v =
   in 
   subst 1 v
 
-(*s Number of occurences of [Rel 1] in [a] *)
+(*s Number of occurences of [Rel 1] in [a]. *)
 
 let nb_occur a =
   let cpt = ref 0 in
   let rec count n = function
     | MLrel i -> if i = n then incr cpt
-    | MLlam (id,t) -> count (n+1) t
-    | MLletin (id,a,b) -> count n a; count (n+1) b
+    | MLlam (id,t) -> count (n + 1) t
+    | MLletin (id,a,b) -> count n a; count (n + 1) b
     | MLcase (t,pv) ->
 	count n t;
-	Array.iter (fun (_,l,t) -> let k = List.length l in count (n+k) t) pv
+	Array.iter (fun (_,l,t) -> let k = List.length l in count (n + k) t) pv
     | MLfix (_,ids,cl) -> 
-	let k = List.length ids in List.iter (count (n+k)) cl
+	let k = List.length ids in List.iter (count (n + k)) cl
     | MLapp (a,l) -> count n a; List.iter (count n) l
     | MLcons (_,_,l) ->  List.iter (count n) l
     | MLmagic a -> count n a
@@ -136,7 +152,7 @@ let betared_decl = function
  | Dglob (id, a) -> Dglob (id, betared_ast a)
  | d -> d
 
-(*s [uncurrify] uncurrifies the applications of constructors *)
+(*s [uncurrify] uncurrifies the applications of constructors. *)
 
 let rec is_constructor_app = function
   | MLcons _ -> true
@@ -151,9 +167,6 @@ let rec decomp_app = function
   | _ ->
       assert false
 
-let anonymous = Names.id_of_string "x"
-let prop_name = Names.id_of_string "_"
-
 let rec n_lam n a =
   if n = 0 then a else MLlam (anonymous, n_lam (pred n) a)
 
@@ -181,6 +194,7 @@ let uncurrify_decl = function
  | Dglob (id, a) -> Dglob (id, uncurrify_ast a)
  | d -> d
 
+
 (*s Table for direct ML extractions. *)
 
 module Refset = 
@@ -189,7 +203,9 @@ module Refset =
 module Refmap = 
   Map.Make(struct type t = global_reference let compare = compare end)
 
-let extractions = ref (Refmap.empty, Refset.empty)
+let empty_extractions = (Refmap.empty, Refset.empty)
+
+let extractions = ref empty_extractions
 
 let ml_extractions () = snd !extractions
 
@@ -201,15 +217,23 @@ let is_ml_extraction r = Refset.mem r (snd !extractions)
 
 let find_ml_extraction r = Refmap.find r (fst !extractions)
 
-(*s Registration for rollback. *)
+(*s Registration of operations for rollback. *)
+
+let (in_ml_extraction,_) = 
+  declare_object ("ML extractions",
+		  { cache_function = (fun (_,(r,s)) -> add_ml_extraction r s);
+		    load_function = (fun (_,(r,s)) -> add_ml_extraction r s);
+		    open_function = (fun _ -> ());
+		    export_function = (fun x -> Some x) })
+
+(*s Registration of the table for rollback. *)
 
 open Summary
 
 let _ = declare_summary "ML extractions"
 	  { freeze_function = (fun () -> !extractions);
 	    unfreeze_function = ((:=) extractions);
-	    init_function = 
-	      (fun () -> extractions := (Refmap.empty, Refset.empty));
+	    init_function = (fun () -> extractions := empty_extractions);
 	    survive_section = true }
 
 (*s Grammar entries. *)
@@ -234,7 +258,7 @@ let reference_of_varg = function
 
 let extract_constant r s = match r with
   | ConstRef _ -> 
-      add_ml_extraction r s
+      add_anonymous_leaf (in_ml_extraction (r,s))
   | _ -> 
       errorlabstrm "extract_constant"
 	[< Printer.pr_global r; 'sPC; 'sTR "is not a constant" >]
@@ -251,13 +275,15 @@ let _ =
 
 let extract_inductive r (id2,l2) = match r with
   | IndRef ((sp,i) as ip) ->
-      add_ml_extraction r id2;
       let mib = Global.lookup_mind sp in
       let n = Array.length mib.mind_packets.(i).mind_consnames in
       if n <> List.length l2 then
 	error "not the right number of constructors";
+      add_anonymous_leaf (in_ml_extraction (r,id2));
       list_iter_i
-	(fun j s -> add_ml_extraction (ConstructRef (ip,succ j)) s) l2
+	(fun j s -> 
+	   add_anonymous_leaf 
+	     (in_ml_extraction (ConstructRef (ip,succ j),s))) l2
   | _ -> 
       errorlabstrm "extract_inductive"
 	[< Printer.pr_global r; 'sPC; 'sTR "is not an inductive type" >]
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 7b7a20dd28..92b210dacd 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -1,3 +1,12 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
 
 open Names
 open Term
@@ -9,22 +18,28 @@ open Miniml
 val anonymous : identifier
 val prop_name : identifier
 
-(*s Utility functions over ML terms. *)
+(*s Utility functions over ML terms. [occurs n t] checks whether [Rel
+    n] occurs (freely) in [t]. [ml_lift] is de Bruijn
+    lifting. [ml_subst e t] substitutes [e] for [Rel 1] in [t]. *)
 
 val occurs : int -> ml_ast -> bool
 
 val ml_lift : int -> ml_ast -> ml_ast
 
-(* [ml_subst e t] substitutes [e] for [Rel 1] in [t] *)
 val ml_subst : ml_ast -> ml_ast -> ml_ast
 
+(*s Some transformations of ML terms. [betared_ast] and [betared_ecl] reduce
+    all beta redexes (when the argument does not occur, it is just
+    thrown away; when it occurs exactly once it is substituted; otherwise
+    a let in redex is created for clarity) *)
+
 val betared_ast : ml_ast -> ml_ast
 val betared_decl : ml_decl -> ml_decl
 
 val uncurrify_ast : ml_ast -> ml_ast
 val uncurrify_decl : ml_decl -> ml_decl
 
-(*s Table for the extraction to ML values. *)
+(*s Table for direct extractions to ML values. *)
 
 module Refset : Set.S with type elt = global_reference