suite et fin (?) de haskell: gestion des modules, mise en place du'un test

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

1 files changed, 17 insertions, 5 deletions

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index dd21564ce5..d516bb3694 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -178,6 +178,21 @@ let ast_map_lift f n = function
   | MLmagic a -> MLmagic (f n a)
   | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity as a -> a	
 
+(* Iter over asts. *) 
+
+let ast_iter_case f (c,ids,a) = f a
+
+let ast_iter f = function
+  | MLlam (i,a) -> f a
+  | MLletin (i,a,b) -> f a; f b
+  | MLcase (a,v) -> f a; Array.iter (ast_iter_case f) v
+  | MLfix (i,ids,v) -> Array.iter f v
+  | MLapp (a,l) -> f a; List.iter f l
+  | MLcons (c,l) -> List.iter f l
+  | MLcast (a,t) -> f a
+  | MLmagic a -> f a
+  | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity as a -> ()
+
 (*s [occurs k t] returns true if [(Rel k)] occurs in [t]. *)
 
 let occurs k t = 
@@ -763,10 +778,7 @@ let add_ml_decls prm decls =
   let l = List.map (fun (r,s)-> Dcustom (r,s)) l in 
   (List.rev l @ decls)
 
-let strict_language = function
-  | "ocaml" -> true
-  | "haskell" -> false
-  | _ -> assert false
+let strict_language = (=) Ocaml
 
 let rec empty_ind = function 
   | [] -> [],[]
@@ -804,7 +816,7 @@ let rec optim prm = function
 	  List.map (subst_glob_decl r t) l
 	end
       else l in 
-      if (not b || prm.mod_name <> None || List.mem r prm.to_appear) then 
+      if (not b || prm.modular || List.mem r prm.to_appear) then 
  	  let t = optimize_fix t in
 	  Dglob (r,t) :: (optim prm l)
       else