ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante dummy

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

12 files changed, 87 insertions, 47 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 9cca520ac..3540e9b2a 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -216,6 +216,11 @@ let extract_to_file f prm decls =
     Idset.remove prm.mod_name (decl_get_modules decls)
   else Idset.empty
   in 
+  let print_dummy = match lang() with 
+    | Ocaml -> decl_search MLdummy' decls
+    | Haskell -> (decl_search MLdummy decls) || (decl_search MLdummy' decls)
+    | _ -> assert false 
+  in 
   cons_cofix := Refset.empty;
   current_module := prm.mod_name;
   Hashtbl.clear renamings;
@@ -231,7 +236,7 @@ let extract_to_file f prm decls =
   if not prm.modular then 
     List.iter (fun r -> pp_with ft (pp_singleton_ind r)) 
       (List.filter decl_is_singleton prm.to_appear); 
-  pp_with ft (preamble prm used_modules);
+  pp_with ft (preamble prm used_modules print_dummy);
   begin 
     try
       List.iter (fun d -> msgnl_with ft (pp_decl d)) decls
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index ef9646b97..d02f9fb32 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -157,7 +157,7 @@ and visit_ast m eenv a =
     | MLfix (_,_,l) -> Array.iter visit l
     | MLcast (a,t) -> visit a; visit_type m eenv t
     | MLmagic a -> visit a
-    | MLrel _ | MLdummy | MLexn _ -> ()
+    | MLrel _ | MLdummy | MLdummy' | MLexn _ -> ()
   in
   visit a
 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 2c6fb88f6..d3dd78dd5 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -48,7 +48,7 @@ open Nametab
 
 type info = Logic | Info
 
-type arity = Arity | NotArity
+type arity = Arity | Flexible | Default
 
 type flag = info * arity
 
@@ -123,13 +123,20 @@ let _ = declare_summary "Extraction tables"
 	    init_function = (fun () -> ());
 	    survive_section = true }
 
-(*S Error messages. *)
+(*S Warning & Error messages. *)
 
-let axiom_message sp =
+let axiom_error_message sp =
   errorlabstrm "axiom_message"
     (str "You must specify an extraction for axiom" ++ spc () ++ 
        pr_sp sp ++ spc () ++ str "first.")
 
+let axiom_warning_message sp = 
+  Options.if_verbose warn 
+    (str "This extraction depends on logical axiom" ++ spc () ++ 
+     pr_sp sp ++ str "." ++ spc() ++ 
+     str "Having false logical axiom in the environment when extracting" ++ 
+     spc () ++ str "may lead to incorrect or non-terminating ML terms.")
+    
 let section_message () = 
   errorlabstrm "section_message"
     (str "You can't extract within a section. Close it and try again.")
@@ -147,11 +154,12 @@ let is_axiom sp = (Global.lookup_constant sp).const_body = None
 (*s [flag_of_type] transforms a type [t] into a [flag]. 
   Really important function. *)
 
-let flag_of_type env t = match find_conclusion env t with
+let flag_of_type env t = match find_conclusion env none t with
   | Sort (Prop Null) -> (Logic,Arity)
   | Sort _ -> (Info,Arity)
-  | _ -> if (sort_of env t) = InProp then (Logic,NotArity)
-    else (Info,NotArity)
+  | (Case _ | Fix _ | CoFix _) -> 
+      if (sort_of env t) = InProp then (Logic,Flexible) else (Info,Default)
+  | _ -> if (sort_of env t) = InProp then (Logic,Default) else (Info,Default)
 
 (*s [is_default] is a particular case of the last function. *)
 
@@ -554,8 +562,10 @@ and extract_constr_to_term env c =
 (* Same, but With Type (wt). *)
 
 and extract_constr_to_term_wt env c t = 
-  if is_default env t then extract_term_wt env c t 
-  else dummy_lams MLdummy (List.length (fst (splay_prod env none t)))
+  match flag_of_type env t with 
+    | (Info, Default) -> extract_term_wt env c t
+    | (Logic, Flexible) -> MLdummy'
+    | _ -> dummy_lams MLdummy (List.length (fst (splay_prod env none t)))
 
 (*S Extraction of a constr. *)
 
@@ -572,8 +582,8 @@ and extract_constr_wt env c t =
 	let ctx = ctx_from_sign s in 
 	let mlt = extract_type_arity env c ctx (List.length s) in 
 	Emltype (mlt, s, vl)
-    | (Logic, NotArity) -> Emlterm MLdummy
-    | (Info, NotArity) -> Emlterm (extract_term_wt env c t)
+    | (Logic, _) -> Emlterm MLdummy
+    | (Info, _) -> Emlterm (extract_term_wt env c t)
 	  
 (*S Extraction of a constant. *)
 		
@@ -584,11 +594,13 @@ and extract_constant sp =
     let cb = Global.lookup_constant sp in
     let typ = cb.const_type in
     match cb.const_body with
-      | None ->
+      | None -> (* A logical axiom is risky, an informative one is fatal. *) 
           (match flag_of_type env typ with
-             | (Info,_) -> axiom_message sp (* We really need some code here *)
-             | (Logic,NotArity) -> Emlterm MLdummy (* Axiom? I don't mind! *)
-             | (Logic,Arity) -> Emltype (Tdummy,[],[]))  (* Idem *)
+             | (Info,_) -> axiom_error_message sp 
+             | (Logic,Arity) -> axiom_warning_message sp; 
+		 Emltype (Tdummy,[],[])
+	     | (Logic,_) -> axiom_warning_message sp;
+		 Emlterm MLdummy)
       | Some body ->
 	  let e = match extract_constr_wt env body typ with 
 	    | Emlterm MLdummy as e -> e
@@ -666,7 +678,7 @@ and extract_mib sp =
 	      let n = List.length s in 
 	      let db,ctx = 
 		if si=[] then Intmap.empty,[]
-		else match find_conclusion params_env t with 
+		else match find_conclusion params_env none t with 
 		  | App (f, args) -> 
 		      (*i assert (kind_of_term f = Ind ip); i*)
 		      let db = parse_ind_args si args in 
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 7f6b88d94..9cabd01be 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -27,19 +27,23 @@ let keywords =
   List.fold_right (fun s -> Idset.add (id_of_string s))
   [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
     "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance"; 
-    "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_";
+    "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__";
     "as"; "qualified"; "hiding" ; "unit" ]
   Idset.empty
 
-let preamble prm used_modules =
+let preamble prm used_modules print_dummy =
   let m = String.capitalize (string_of_id prm.mod_name)   in 
   str "module " ++ str m ++ str " where" ++ fnl () ++ fnl() ++ 
-  str "import Unit" ++ fnl() ++ 
   str "import qualified Prelude" ++ fnl() ++
   Idset.fold 
     (fun m s -> 
        s ++ str "import qualified " ++ pr_id (uppercase_id m) ++ fnl())
     used_modules (mt ()) ++ fnl()
+  ++
+  (if print_dummy then 
+     str "__ = Prelude.error \"Logical or arity value used\"" 
+     ++ fnl () ++ fnl()
+   else mt())
 
 let pp_abst = function
   | [] -> (mt ())
@@ -152,14 +156,10 @@ let rec pp_expr par env args =
 	(* An [MLexn] may be applied, but I don't really care. *)
 	(open_par par ++ str "Prelude.error" ++ spc () ++ 
 	 qs s ++ close_par par)
-    | MLdummy ->
-	str "unit" (* An [MLdummy] may be applied, but I don't really care. *)
-    | MLcast (a,t) ->
-	(open_par true ++ pp_expr false env args a ++ spc () ++ str "::" ++ 
-	 spc () ++ pp_type false [] t ++ close_par true)
-    | MLmagic a ->
-	(open_par true ++ str "Obj.magic" ++ spc () ++ 
-	 pp_expr false env args a ++ close_par true)
+    | MLdummy | MLdummy' ->
+	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
+    | MLcast (a,t) -> pp_expr par env args a
+    | MLmagic a ->  pp_expr par env args a
 
 and pp_pat env pv = 
   let pp_one_pat (name,ids,t) =
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 78cabaca9..5d744be2a 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -15,6 +15,6 @@ open Miniml
 
 val keywords : Idset.t
 
-val preamble : extraction_params -> Idset.t -> std_ppcmds
+val preamble : extraction_params -> Idset.t -> bool -> std_ppcmds
 
 module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index e49f4fa68..67669f8e4 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -43,6 +43,7 @@ type ml_ast =
   | MLfix   of int * identifier array * ml_ast array
   | MLexn   of string
   | MLdummy
+  | MLdummy' 
   | MLcast  of ml_ast * ml_type
   | MLmagic of ml_ast
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index d4941008a..804416a6d 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -30,7 +30,6 @@ exception Impossible
 
 let anonymous = id_of_string "x"
 let dummy_name = id_of_string "_"
-let flex_name = id_of_string "flex"
 
 let id_of_name = function
   | Anonymous -> anonymous
@@ -70,7 +69,7 @@ let ast_iter_rel f =
     | MLcons (_,l) ->  List.iter (iter n) l
     | MLcast (a,_) -> iter n a
     | MLmagic a -> iter n a
-    | MLglob _ | MLexn _ | MLdummy -> ()
+    | MLglob _ | MLexn _ | MLdummy | MLdummy' -> ()
   in iter 0 
 
 (*s Map over asts. *)
@@ -86,7 +85,7 @@ let ast_map f = function
   | MLcons (c,l) -> MLcons (c, List.map f l)
   | MLcast (a,t) -> MLcast (f a, t)
   | MLmagic a -> MLmagic (f a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLdummy' as a -> a
 
 (*s Map over asts, with binding depth as parameter. *)
 
@@ -102,7 +101,7 @@ let ast_map_lift f n = function
   | MLcons (c,l) -> MLcons (c, List.map (f n) l)
   | MLcast (a,t) -> MLcast (f n a, t)
   | MLmagic a -> MLmagic (f n a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a	
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLdummy' as a -> a	
 
 (*s Iter over asts. *) 
 
@@ -117,7 +116,20 @@ let ast_iter f = function
   | MLcons (c,l) -> List.iter f l
   | MLcast (a,t) -> f a
   | MLmagic a -> f a
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> ()
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLdummy' as a -> ()
+
+(*S Searching occurrences of a particular term (no lifting done). *)
+
+let rec ast_search t a = 
+  if t = a then raise Found else ast_iter (ast_search t) a
+
+let decl_search t l = 
+  let one_decl = function 
+    | Dglob (_,a) -> ast_search t a
+    | Dfix (_,c) -> Array.iter (ast_search t) c
+    | _ -> () 
+  in 
+  try List.iter one_decl l; false with Found -> true
 
 (*S Operations concerning De Bruijn indices. *)
 
@@ -379,7 +391,7 @@ let iota_gen br =
   in iota 0 
 
 let is_atomic = function 
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLdummy' -> true
   | _ -> false
 
 (*S The main simplification function. *)
@@ -427,7 +439,7 @@ and simpl_app o a = function
 	     let a' = List.map (ml_lift k) a in
       	     (n, l, simpl o (MLapp (t,a')))) br 
       in simpl o (MLcase (e,br')) 
-  | (MLdummy | MLexn _) as e -> e 
+  | (MLdummy | MLdummy' | MLexn _) as e -> e 
 	(* We just discard arguments in those cases. *)
   | f -> MLapp (f,a)
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index b4e3d819a..7a6dfb121 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -18,7 +18,6 @@ open Nametab
 
 val anonymous : identifier
 val dummy_name : identifier
-val flex_name : identifier
 val id_of_name : name -> identifier
 
 (*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
@@ -45,8 +44,6 @@ val sp_of_r : global_reference -> section_path
 
 val type_mem_sp : section_path -> ml_type -> bool
 
-(*TODO val get_tvars : ml_type -> identifier list *)
-
 (*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]. *)
@@ -59,6 +56,8 @@ val ml_lift : int -> ml_ast -> ml_ast
 
 val ml_subst : ml_ast -> ml_ast -> ml_ast
 
+val decl_search : ml_ast -> ml_decl list -> bool
+
 (*s Some transformations of ML terms. [normalize] simplify
     all beta redexes (when the argument does not occur, it is just
     thrown away; when it occurs exactly once it is substituted; otherwise
@@ -77,3 +76,8 @@ val optimize :
 
 val kill_some_lams : 
   bool list -> identifier list * ml_ast -> identifier list * ml_ast
+
+
+
+
+
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 36b567203..1df26acc8 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -119,14 +119,19 @@ let keywords =
     "module"; "mutable"; "new"; "object"; "of"; "open"; "or";
     "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
     "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
-    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ] 
+    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] 
   Idset.empty
 
-let preamble _ used_modules = 
+let preamble _ used_modules print_dummy = 
   Idset.fold (fun m s -> s ++ str "open " ++ pr_id (uppercase_id m) ++ fnl())
     used_modules (mt ())
   ++ 
-  (if Idset.is_empty used_modules  then mt () else fnl ()) 
+  (if Idset.is_empty used_modules  then mt () else fnl ())
+  ++
+  (if print_dummy then 
+     str "let (__:unit) = let rec f _ = Obj.magic f in Obj.magic f" 
+     ++ fnl () ++ fnl()
+   else mt ())
 
 (*s The pretty-printing functor. *)
 
@@ -144,7 +149,8 @@ let empty_env () = [], P.globals()
 
 let rec pp_type par vl t =
   let rec pp_rec par = function
-    | Tvar i -> (try pp_tvar (List.nth vl (pred i)) with _ -> (str "'a" ++ int i))
+    | Tvar i -> (try pp_tvar (List.nth vl (pred i)) 
+		 with _ -> (str "'a" ++ int i))
     | Tapp l ->
 	(match collapse_type_app l with
 	   | [] -> assert false
@@ -259,6 +265,8 @@ let rec pp_expr par env args =
 	 str ("(* "^s^" *)") ++ close_par par)
     | MLdummy ->
 	str "()" (* An [MLdummy] may be applied, but I don't really care. *)
+    | MLdummy' -> 
+	str "__" (* idem *)
     | MLcast (a,t) ->
 	(open_par true ++ pp_expr false env args a ++ spc () ++ str ":" ++ 
 	 spc () ++ pp_type false [] t ++ close_par true)
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 1bfd13b11..2a9170bb0 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -41,7 +41,7 @@ val get_db_name : int -> env -> identifier
 
 val keywords : Idset.t
 
-val preamble : extraction_params -> Idset.t -> std_ppcmds
+val preamble : extraction_params -> Idset.t -> bool -> std_ppcmds
 
 (*s Production of Ocaml syntax. We export both a functor to be used for 
     extraction in the Coq toplevel and a function to extract some 
diff --git a/contrib/extraction/test/Makefile.haskell b/contrib/extraction/test/Makefile.haskell
index ddc6ab4fb..347e99887 100644
--- a/contrib/extraction/test/Makefile.haskell
+++ b/contrib/extraction/test/Makefile.haskell
@@ -31,7 +31,7 @@ O:= $(patsubst %.hs,%.o,$(HS))
 #	General rules 
 #
 
-all: v2hs hs Unit.o $(O)
+all: v2hs hs $(O)
 
 hs: $(HS)
 
diff --git a/contrib/extraction/test/Unit.hs b/contrib/extraction/test/Unit.hs
deleted file mode 100644
index 5d104e181..000000000
--- a/contrib/extraction/test/Unit.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-module Unit where
-unit = ()