extraction recursive d'un morceau d'environnement

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

7 files changed, 228 insertions, 78 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index 5bf303fbb..92f731842 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -6,7 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Declare ML Module "mlutil.cmo" "ocaml.cmo" "extraction.cmo".
+Declare ML Module "mlutil.cmo" "ocaml.cmo" "extraction.cmo" "extract_env.cmo".
 
 Grammar vernac vernac : ast :=
-  extr_constr [ "Extraction" constrarg($c) "." ] -> [(Extraction $c)].
+  extr_constr [ "Extraction" constrarg($c) "." ] -> 
+              [(Extraction $c)]
+| extr_list   [ "Extraction" "[" ne_qualidarg_list($l) "]" "." ] ->
+              [(ExtractionList ($LIST $l))].
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
new file mode 100644
index 000000000..4fc2dc79f
--- /dev/null
+++ b/contrib/extraction/extract_env.ml
@@ -0,0 +1,172 @@
+
+open Pp
+open Term
+open Miniml
+open Mlutil
+open Extraction
+
+(*s Topological sort of global CIC references. 
+    We introduce graphs of global references; a graph is a map
+    from edges to the set of their immediate successors. *)
+
+module Refmap = 
+  Map.Make(struct type t = global_reference let compare = compare end)
+
+module Refset = 
+  Set.Make(struct type t = global_reference let compare = compare end)
+
+type graph = Refset.t Refmap.t
+
+let empty = Refmap.empty
+
+let add_arc x y g =
+  let s = try Refmap.find x g with Not_found -> Refset.empty in
+  let g' = Refmap.add x (Refset.add y s) g in
+  if not (Refmap.mem y g') then Refmap.add y Refset.empty g' else g'
+
+exception Found of global_reference
+
+let maximum g =
+  try 
+    Refmap.iter (fun x s -> if s = Refset.empty then raise (Found x)) g;
+    assert false
+  with Found m -> 
+    m
+
+let remove m g =
+  let g' = 
+    Refmap.fold (fun x s -> Refmap.add x (Refset.remove m s)) g Refmap.empty
+  in
+  Refmap.remove m g'
+
+let sorted g =
+  let rec sorted_aux acc g =
+    if g = Refmap.empty then
+      acc
+    else
+      let max = maximum g in
+      sorted_aux (max :: acc) (remove max g)
+  in
+  sorted_aux [] g
+
+(*s Computation of the global references appearing in an AST of a 
+    declaration. *)
+
+let globals_of_type t =
+  let rec collect s = function
+    | Tglob r -> Refset.add r s
+    | Tapp l -> List.fold_left collect s l
+    | Tarr (t1,t2) -> collect (collect s t1) t2
+    | Tvar _ | Tprop | Tarity -> s
+  in
+  collect Refset.empty t
+
+let globals_of_ast a =
+  let rec collect s = function
+    | MLglob r -> Refset.add r s
+    | MLapp (a,l) -> List.fold_left collect (collect s a) l
+    | MLlam (_,a) -> collect s a
+    | MLletin (_,a,b) -> collect (collect s a) b
+    | MLcons (r,_,l) -> List.fold_left collect (Refset.add r s) l
+    | MLcase (a,br) -> 
+	Array.fold_left 
+	  (fun s (r,_,a) -> collect (Refset.add r s) a) (collect s a) br
+    | MLfix (_,_,l) -> List.fold_left collect s l
+    | MLcast (a,t) -> Refset.union (collect s a) (globals_of_type t)
+    | MLmagic a -> collect s a
+    | MLrel _ | MLprop | MLarity | MLexn _ -> s
+  in
+  collect Refset.empty a
+
+let globals_of_inductive inds =
+  let globals_of_constructor ie (r,tl) =
+    List.fold_left 
+      (fun (i,e) t -> Refset.add r i, Refset.union (globals_of_type t) e) ie tl
+  in
+  let globals_of_ind (i,e) (_,r,cl) = 
+    List.fold_left globals_of_constructor (Refset.add r i, e) cl
+  in
+  let (i,e) = List.fold_left globals_of_ind (Refset.empty,Refset.empty) inds in
+  Refset.diff e i
+
+let globals_of_decl = function
+  | Dtype inds ->
+      globals_of_inductive inds
+  | Dabbrev (r,_,t) ->
+      Refset.remove r (globals_of_type t)
+  | Dglob (r,a) ->
+      Refset.remove r (globals_of_ast a)
+
+(*s Recursive extraction of a piece of environment. *)
+
+let add_dependency r r' g = 
+  let normalize = function
+    | ConstructRef (ip,_) -> IndRef ip
+    | r -> r
+  in
+  add_arc (normalize r') (normalize r) g
+
+let extract_env rl =
+  let rec extract graph seen todo = 
+    if Refset.equal todo Refset.empty then
+      sorted graph
+    else 
+      let r = Refset.choose todo in
+      let todo' = Refset.remove r todo in
+      if Refset.mem r seen then
+	extract graph seen todo'
+      else
+	let d = extract_declaration r in
+	let deps = globals_of_decl d in
+	let graph' = Refset.fold (add_dependency r) deps graph in
+	extract graph' (Refset.add r seen) (Refset.union todo' deps)
+  in
+  extract empty Refset.empty (List.fold_right Refset.add rl Refset.empty)
+
+
+(*s Registration of vernac commands for extraction. *)
+
+module ToplevelParams = struct
+  let pp_type_global = Printer.pr_global
+  let pp_global = Printer.pr_global
+end
+
+module Pp = Ocaml.Make(ToplevelParams)
+
+let pp_ast a = Pp.pp_ast (uncurrify_ast a)
+let pp_decl d = Pp.pp_decl (uncurrify_decl d)
+
+open Vernacinterp
+
+let _ = 
+  vinterp_add "Extraction"
+    (function 
+       | [VARG_CONSTR ast] ->
+	   (fun () -> 
+	      let c = Astterm.interp_constr Evd.empty (Global.env()) ast in
+	      match kind_of_term c with
+		(* If it is a global reference, then output the declaration *)
+		| IsConst (sp,_) -> 
+		    mSGNL (pp_decl (extract_declaration (ConstRef sp)))
+		| IsMutInd (ind,_) ->
+		    mSGNL (pp_decl (extract_declaration (IndRef ind)))
+		| IsMutConstruct (cs,_) ->
+		    mSGNL (pp_decl (extract_declaration (ConstructRef cs)))
+		(* Otherwise, output the ML type or expression *)
+		| _ ->
+		    match extract_constr (Global.env()) [] c with
+		      | Emltype (t,_,_) -> mSGNL (Pp.pp_type t)
+		      | Emlterm a -> mSGNL (pp_ast a)
+		      | Eprop -> message "prop")
+       | _ -> assert false)
+
+let reference_of_varg = function
+  | VARG_QUALID q -> Nametab.locate q
+  | _ -> assert false
+
+let _ = 
+  vinterp_add "ExtractionList"
+    (fun vl () ->
+       let rl = List.map reference_of_varg vl in
+       let rl' = extract_env rl in
+       List.iter (fun r -> mSGNL (pp_decl (extract_declaration r))) rl')
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
new file mode 100644
index 000000000..041bb44ca
--- /dev/null
+++ b/contrib/extraction/extract_env.mli
@@ -0,0 +1,4 @@
+
+open Term
+
+val extract_env : global_reference list -> global_reference list
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 7ae999ea3..1e8d13f76 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -259,7 +259,7 @@ let lookup_inductive_extraction i = Gmap.find i !inductive_extraction_table
 type constructor_extraction_result = 
   | Cml of ml_type list * signature
   | Cprop
-   
+
 let constructor_extraction_table = 
   ref (Gmap.empty : (constructor_path, constructor_extraction_result) Gmap.t)
 
@@ -473,7 +473,8 @@ and extract_term_with_type env ctx c t =
 	  in (binders,e')
 	in
 	let extract_branch j b =
-	  let s = signature_of_constructor (ip,succ j) in
+	  let cp = (ip,succ j) in
+	  let s = signature_of_constructor cp in
 	  assert (List.length s = ni.(j));
 	  (* number of arguments, without parameters *)
 	  let (binders, e') = extract_branch_aux j b in
@@ -483,7 +484,7 @@ and extract_term_with_type env ctx c t =
 		 if v = Vdefault then (id_of_name n :: acc) else acc)
 	      (List.combine s binders) []
 	  in
-	  (cnames.(j), ids, e')
+	  (ConstructRef cp, ids, e')
 	in
 	(* [c] has an  inductive type, not an arity type *)
 	(match extract_term env ctx c with
@@ -647,21 +648,23 @@ and extract_mib sp =
 and extract_inductive_declaration sp =
   extract_mib sp;
   let mib = Global.lookup_mind sp in
-  let one_constructor ind j id = 
-    match lookup_constructor_extraction (ind,succ j) with 
+  let one_constructor ind j _ = 
+    let cp = (ind,succ j) in
+    match lookup_constructor_extraction cp with 
       | Cprop -> assert false
-      | Cml (t,_) -> (id, t)
+      | Cml (t,_) -> (ConstructRef cp, t)
   in
   let l = 
     array_foldi
-      (fun i ip acc -> 
-	 match lookup_inductive_extraction (sp,i) with
+      (fun i packet acc -> 
+	 let ip = (sp,i) in
+	 match lookup_inductive_extraction ip with
 	   | Iprop -> acc
 	   | Iml (s,fl) -> 
 	       (params_of_sign s @ fl, 
-		ip.mind_typename, 
+		IndRef ip, 
 		Array.to_list 
-		  (Array.mapi (one_constructor (sp,i)) ip.mind_consnames))
+		  (Array.mapi (one_constructor ip) packet.mind_consnames))
 	       :: acc )
 	 mib.mind_packets [] 
   in
@@ -669,50 +672,12 @@ and extract_inductive_declaration sp =
 
 (*s ML declaration from a reference. *)
 
-let extract_declaration = function
+let extract_declaration r = match r with
   | ConstRef sp -> 
-      let id = basename sp in (* FIXME *)
       (match extract_constant sp with
-	 | Emltype (mlt, s, fl) -> Dabbrev (id, params_of_sign s @ fl, mlt)
-	 | Emlterm t -> Dglob (id, t)
-	 | Eprop -> Dglob (id, MLprop))
+	 | Emltype (mlt, s, fl) -> Dabbrev (r, params_of_sign s @ fl, mlt)
+	 | Emlterm t -> Dglob (r, t)
+	 | Eprop -> Dglob (r, MLprop))
   | IndRef (sp,_) -> extract_inductive_declaration sp
   | ConstructRef ((sp,_),_) -> extract_inductive_declaration sp
   | VarRef _ -> assert false
-
-(*s Registration of vernac commands for extraction. *)
-
-module ToplevelParams = struct
-  let pp_type_global = Printer.pr_global
-  let pp_global = Printer.pr_global
-end
-
-module Pp = Ocaml.Make(ToplevelParams)
-
-let pp_ast a = Pp.pp_ast (uncurrify_ast a)
-let pp_decl d = Pp.pp_decl (uncurrify_decl d)
-
-open Vernacinterp
-
-let _ = 
-  vinterp_add "Extraction"
-    (function 
-       | [VARG_CONSTR ast] ->
-	   (fun () -> 
-	      let c = Astterm.interp_constr Evd.empty (Global.env()) ast in
-	      match kind_of_term c with
-		(* If it is a global reference, then output the declaration *)
-		| IsConst (sp,_) -> 
-		    mSGNL (pp_decl (extract_declaration (ConstRef sp)))
-		| IsMutInd (ind,_) ->
-		    mSGNL (pp_decl (extract_declaration (IndRef ind)))
-		| IsMutConstruct (cs,_) ->
-		    mSGNL (pp_decl (extract_declaration (ConstructRef cs)))
-		(* Otherwise, output the ML type or expression *)
-		| _ ->
-		    match extract_constr (Global.env()) [] c with
-		      | Emltype (t,_,_) -> mSGNL (Pp.pp_type t)
-		      | Emlterm a -> mSGNL (pp_ast a)
-		      | Eprop -> message "prop")
-       | _ -> assert false)
-
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 66993d488..bb11adaab 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -26,7 +26,8 @@ type ml_type =
       
 (*s ML inductive types. *)
 
-type ml_ind = identifier list * identifier * (identifier * ml_type list) list
+type ml_ind = 
+  identifier list * global_reference * (global_reference * ml_type list) list
 
 (*s ML terms. *)
 
@@ -37,7 +38,7 @@ type ml_ast =
   | MLletin of identifier * ml_ast * ml_ast
   | MLglob  of global_reference
   | MLcons  of global_reference * int * ml_ast list
-  | MLcase  of ml_ast * (identifier * identifier list * ml_ast) array
+  | MLcase  of ml_ast * (global_reference * identifier list * ml_ast) array
   | MLfix   of int * (identifier list) * (ml_ast list)
   | MLexn   of identifier
   | MLprop
@@ -49,8 +50,8 @@ type ml_ast =
 
 type ml_decl = 
   | Dtype   of ml_ind list
-  | Dabbrev of identifier * (identifier list) * ml_type
-  | Dglob   of identifier * ml_ast
+  | Dabbrev of global_reference * (identifier list) * ml_type
+  | Dglob   of global_reference * ml_ast
 
 (*s Pretty-printing of MiniML in a given concrete syntax is parameterized
     by a function [pp_global] that pretty-prints global references. 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 9d66a820c..09683eb77 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -2,8 +2,8 @@
 open Util
 open Miniml
 
-(* [occurs : int -> ml_ast -> bool]
-   [occurs k M] returns true if (Rel k) occurs in M. *)
+(*s [occurs : int -> ml_ast -> bool]
+    [occurs k M] returns true if (Rel k) occurs in M. *)
 
 let rec occurs k = function
   | MLrel i          -> i=k
@@ -21,14 +21,14 @@ let rec occurs k = function
 and occurs_list k l =
   List.exists (fun t -> occurs k t) l
 
-(* map over ML asts *)
+(*s map over ML asts *)
 
 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)
-  | MLcase (a,eqv) -> (MLcase (f a, Array.map (ast_map_eqn f) eqv))
+  | 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)
   | MLmagic a -> MLmagic (f a)
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index e7d77904c..ee501ba2f 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -42,7 +42,9 @@ let pp_boxed_tuple f = function
       	    hOV 0 [< prlist_with_sep (fun () -> [< 'sTR ","; 'sPC >]) f l;
 		     'sTR ")" >] >]
 
-let space_if = function true -> [< 'sPC >] | false -> [< >]
+let space_if = function true -> [< 'sTR " " >] | false -> [< >]
+
+let sec_space_if = function true -> [< 'sPC >] | false -> [< >]
 
 (* collect_lambda MLlam(id1,...MLlam(idn,t)...) = [id1;...;idn],t *)
 
@@ -85,7 +87,8 @@ let pp_type t =
 	   | [] -> assert false
 	   | [t] -> pp_rec par t
 	   | t::l -> [< open_par par; pp_tuple (pp_rec false) l; 
-			space_if (l <>[]); pp_rec false t; close_par par >])
+			sec_space_if (l <>[]); 
+			pp_rec false t; close_par par >])
     | Tarr (t1,t2) ->
 	[< open_par par; pp_rec true t1; 'sPC; 'sTR "->"; 'sPC; 
 	   pp_rec false t2; close_par par >]
@@ -170,7 +173,7 @@ and pp_pat env pv =
       | MLcase _ -> true
       | _        -> false 
     in
-    hOV 2 [< pr_id name;
+    hOV 2 [< P.pp_global name;
 	     begin match ids with 
 	       | [] -> [< >]
 	       | _  -> [< 'sTR " "; pp_boxed_tuple pr_id ids >]
@@ -185,7 +188,7 @@ and pp_fix par env in_p (j,fid,bl) args =
      v 0 [< 'sTR "let rec " ;
 	    prlist_with_sep
       	      (fun () -> [< 'fNL; 'sTR "and " >])
-	      (fun (fi,ti) -> pp_function env' fi ti)
+	      (fun (fi,ti) -> pp_function env' (pr_id fi) ti)
 	      (List.combine fid bl) ;
 	    'fNL ;
 	    if in_p then 
@@ -209,16 +212,16 @@ and pp_function env f t =
   match t' with 
     | MLcase(MLrel 1,pv) ->
 	if is_function pv then
-	  [< pr_id f; pr_binding (List.rev (List.tl bl)) ;
+	  [< f; pr_binding (List.rev (List.tl bl)) ;
        	     'sTR " = function"; 'fNL;
 	     v 0 [< 'sTR "  "; pp_pat (bl @ env) pv >] >]
 	else
-          [< pr_id f; pr_binding (List.rev bl); 
+          [< f; pr_binding (List.rev bl); 
              'sTR " = match ";
 	     pr_id (List.hd bl); 'sTR " with"; 'fNL;
 	     v 0 [< 'sTR "  "; pp_pat (bl @ env) pv >] >]
 	  
-    | _ -> [< pr_id f; pr_binding (List.rev bl);
+    | _ -> [< f; pr_binding (List.rev bl);
 	      'sTR " ="; 'fNL; 'sTR "  ";
 	      hOV 2 (pp_expr false (bl @ env) [] t') >]
 	
@@ -231,14 +234,14 @@ let pp_parameters l =
 
 let pp_one_inductive (pl,name,cl) =
   let pp_constructor (id,l) =
-    [< pr_id id;
+    [< P.pp_global id;
        match l with
          | [] -> [< >] 
 	 | _  -> [< 'sTR " of " ;
       	       	    prlist_with_sep 
 		      (fun () -> [< 'sPC ; 'sTR "* " >]) pp_type l >] >] 
   in
-  [< pp_parameters pl; pr_id name; 'sTR " ="; 'fNL; 
+  [< pp_parameters pl; P.pp_global name; 'sTR " ="; 'fNL;
      v 0 [< 'sTR "    ";
 	    prlist_with_sep (fun () -> [< 'fNL; 'sTR "  | " >])
                             (fun c -> hOV 2 (pp_constructor c)) cl >] >]
@@ -252,21 +255,23 @@ let pp_inductive il =
      'fNL >]
 
 let pp_decl = function
+  | Dtype [] -> 
+      [< >]
   | Dtype i -> 
       hOV 0 (pp_inductive i)
-  | Dabbrev (id, l, t) ->
+  | Dabbrev (r, l, t) ->
       hOV 0 [< 'sTR "type"; 'sPC; pp_parameters l; 
-	       pr_id id; 'sPC; 'sTR "="; 'sPC; pp_type t >]
-  | Dglob (id, MLfix (n,idl,l)) ->
+	       P.pp_type_global r; 'sPC; 'sTR "="; 'sPC; pp_type t; 'fNL >]
+  | Dglob (r, MLfix (n,idl,l)) ->
       let id' = List.nth idl n in
-      if id = id' then
+      if true then (* TODO id = id' *)
 	[<  hOV 2 (pp_fix false [] false (n,idl,l) []) >]
       else
-	[< 'sTR "let "; pr_id id; 'sTR " ="; 'fNL;
+	[< 'sTR "let "; P.pp_global r; 'sTR " ="; 'fNL;
 	   v 0 [< 'sTR "  "; 
 		  hOV 2 (pp_fix false [] true (n,idl,l) []); 'fNL >] >]
-  | Dglob (id, a) ->
-      hOV 0 [< 'sTR "let "; pp_function [] id a >]
+  | Dglob (r, a) ->
+      hOV 0 [< 'sTR "let "; pp_function [] (P.pp_global r) a; 'fNL >]
 
 end