reorganisation des recherches de ref dans ml_decl

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

3 files changed, 95 insertions, 6 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index e5505877a2..9d1808a76d 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -20,7 +20,7 @@ open Extraction
 open Mlutil
 open Common
 
-
+(*
 
 let mp_of_kn kn = 
   let mp,_,l = repr_kn kn in MPdot (mp,l) 
@@ -64,7 +64,51 @@ type visit = { mutable kn : KNset.t; mutable mp : MPset.t }
 let in_kn kn v = KNset.mem kn v.kn
 let in_mp mp v = MPset.mem mp v.mp
 
-(* let rec extract_msb mp all v = function 
+let rec visit_type m eenv t =
+  let rec visit = function
+    | Tglob (r,l) -> visit_reference m eenv r; List.iter visit l  
+    | Tarr (t1,t2) -> visit t1; visit t2
+    | Tvar _ | Tdummy | Tunknown | Tcustom _ -> ()
+    | Tmeta _ | Tvar' _ -> assert false 
+  in
+  visit t
+    
+and visit_ast m eenv a =
+  let rec visit = function
+    | MLglob r -> visit_reference m eenv r
+    | MLapp (a,l) -> visit a; List.iter visit l
+    | MLlam (_,a) -> visit a
+    | MLletin (_,a,b) -> visit a; visit b
+    | MLcons (r,l) -> visit_reference m eenv r; List.iter visit l
+    | MLcase (a,br) -> 
+	visit a; 
+	Array.iter (fun (r,_,a) -> visit_reference m eenv r; visit a) br
+    | MLfix (_,_,l) -> Array.iter visit l
+    | MLcast (a,t) -> visit a; visit_type m eenv t
+    | MLmagic a -> visit a
+    | MLrel _ | MLdummy | MLexn _ | MLcustom _ -> ()
+  in
+  visit a
+
+and visit_inductive m eenv inds =
+  let visit_constructor (_,tl) = List.iter (visit_type m eenv) tl in
+  let visit_ind (_,_,cl) = List.iter visit_constructor cl in
+  List.iter visit_ind inds
+
+and visit_decl m eenv = function
+  | Dind (inds,_) -> visit_inductive m eenv inds
+  | Dtype (_,_,t) -> visit_type m eenv t
+  | Dterm (_,a,t) -> visit_ast m eenv a; visit_type m eenv t
+  | Dfix (_,c,t) -> 
+      Array.iter (visit_ast m eenv) c;
+      Array.iter (visit_type m eenv) t
+  | _ -> ()
+
+
+let rec get_structure_elem_references = function 
+  | SEind ml_ind -> 
+      
+let rec extract_msb mp all v = function 
   | [] -> [] 
   | (l,seb) -> 
       let ml_msb = extract_msb v in 
@@ -73,7 +117,7 @@ let in_mp mp v = MPset.mem mp v.mp
 	    let kn = std_kn mp l in 
 	    if all || in_kn kn v then 
 	      let ml_se = extraction_constant_body kn cb in 
-	      search_visit ml_se v; 
+	      get_structure_elem_references ml_se v; 
 	      ml_se :: ml_msb
 	    else ml_msb
 	| SEBmind mib ->
@@ -93,9 +137,8 @@ let in_mp mp v = MPset.mem mp v.mp
 	    if all || in_kn kn v then 
 	      SEmodtype (extraction_mtb (MPdot (mp,l)) true v m) :: ml_msb
 	    else msb
-*)
 
-(*
+
 let mono_environment kn_set = 
   let add_mp kn mpset = KNset.union (sub_modpath (modpath kn)) mpset
   let kn_to_visit = ref kn_set 
@@ -106,7 +149,8 @@ let mono_environment kn_set =
 
 
   let top = toplevel_structure_body ()
-*)	      
+
+*)
 
 (*s Auxiliary functions dealing with modules. *)
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index d4c8ba1907..07df294b51 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -1183,7 +1183,47 @@ and optimize_Dfix prm (r,t,typ) b l =
 	  else optimize prm l 
     | _ -> raise Impossible
 
+(* Apply some fonctions upon all references in 
+   [ml_type], [ml_ast], [ml_decl]. *)
 
+type do_ref = global_reference -> unit
+
+let type_iter_references do_type t = 
+  let rec iter = function 
+    | Tglob (r,l) -> do_type r; List.iter iter l 
+    | Tarr (a,b) -> iter a; iter b 
+    | _ -> () 
+  in iter t
+
+let ast_iter_references do_term do_cons do_type a = 
+  let rec iter a = 
+    ast_iter iter a;
+    match a with 
+      | MLglob r -> do_term r
+      | MLcons (r,_) -> do_cons r
+      | MLcase (_,v) as a -> Array.iter (fun (r,_,_) -> do_cons r) v
+      | MLcast (_,t) -> type_iter_references do_type t 
+      | _ -> ()
+  in iter a
+
+let decl_iter_references do_term do_cons do_type = 
+  let type_iter = type_iter_references do_type 
+  and ast_iter = ast_iter_references do_term do_cons do_type in 
+  let cons_iter (r,l) = do_cons r; List.iter type_iter l in 
+  let ind_iter (_,r,l) = 
+    do_type r; 
+    (try List.iter do_term (find_proj ((kn_of_r r),0)) 
+     with Not_found -> ()); 
+    List.iter cons_iter l 
+  in 
+  function 
+    | Dind (l,_) -> List.iter ind_iter l 
+    | Dtype (r,_,t) -> do_type r; type_iter t 
+    | Dterm (r,a,t) -> do_term r; ast_iter a; type_iter t
+    | Dfix(rv,c,t) -> 	
+	Array.iter do_term rv; Array.iter ast_iter c; Array.iter type_iter t
+    | DcustomTerm (r,_) -> do_term r
+    | DcustomType (r,_) -> do_type r
 
 
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 023fcf95ef..c061a53699 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -118,6 +118,11 @@ val case_expunge :
 val term_expunge : 
   bool list -> identifier list * ml_ast -> ml_ast
 
+type do_ref = global_reference -> unit 
+
+val type_iter_references : do_ref -> ml_type -> unit
+val ast_iter_references : do_ref -> do_ref -> do_ref -> ml_ast -> unit
+val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit