multiples bricoles. Cf mon TODO papier

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

6 files changed, 52 insertions, 22 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 63a74b3d07..5fe9264c52 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -51,7 +51,7 @@ let cache r f =
 (*s Renaming issues at toplevel *)
 
 module ToplevelParams = struct
-  let cofix_warning = false
+  let toplevel = true
   let globals () = Idset.empty
   let rename_global r = Names.id_of_string (Global.string_of_global r)
   let pp_type_global = Printer.pr_global
@@ -62,7 +62,7 @@ end
 
 module MonoParams = struct
 
-  let cofix_warning = true
+  let toplevel = false
 
   let globals () = !global_ids
 		     
@@ -98,7 +98,7 @@ end
 
 module ModularParams = struct
 
-  let cofix_warning = true
+  let toplevel = false
 
   let globals () = !global_ids 
 
@@ -172,7 +172,7 @@ let extract_to_file f prm decls =
   in
   let cout = open_out f in
   let ft = Pp_control.with_output_to cout in
-  pP_with ft (hV 0 (preamble prm));
+  if decls <> [] then pP_with ft (hV 0 (preamble prm));
   begin 
     try
       List.iter (fun d -> mSGNL_with ft (pp_decl d)) decls
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 7dd1316c93..35cd8a592e 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -66,7 +66,7 @@ type extraction_params =
     to_appear : global_reference list }
 
 module type Mlpp_param = sig
-  val cofix_warning : bool
+  val toplevel : bool
   val globals : unit -> Idset.t
   val rename_global : global_reference -> identifier
   val pp_type_global : global_reference -> std_ppcmds
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 07e7f25ff9..187df32a49 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -320,6 +320,36 @@ let normalize a =
 	ast_map simplify a 
   in simplify (merge_app a)
 
+(*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
+    the list [id1;...;idn] and the term [t]. *)
+
+let collect_lambda = 
+  let rec collect acc = function
+    | MLlam(id,t) -> collect (id::acc) t
+    | x           -> acc,x
+  in 
+  collect []
+
+
+
+let test_eta l =
+  let rec test n = function 
+    | [] -> true
+    | a :: q -> a = (MLrel n) || (test (succ n) q)
+  in test 1 l 
+
+let optimize_fix a = 
+  if not (optim()) then a else
+    let lams,b = collect_lambda a in 
+    (match a with 
+      | MLfix(_,[|_|],[|c|]) -> a (* TODO *)
+      | MLapp(b,ids) -> 
+	  (match b with 
+	     | MLfix(_,[|_|],[|_|]) when (test_eta ids)-> b
+	     | MLfix(_,[|_|],[|_|]) -> a (* TODO *)
+	     | _ -> a)
+      | _ -> a)
+
 let normalize_decl = function
  | Dglob (id, a) -> Dglob (id, normalize a)
  | d -> d
@@ -494,14 +524,15 @@ let strict_language = function
 let rec optimize prm = function
   | [] -> 
       []
-  | (Dtype _ | Dabbrev _ | Dcustom _) as d :: l -> 
-      d :: (optimize prm l)
-  | Dglob (r, MLprop) as d :: l ->
+  | ( Dabbrev (r,_,Tarity) |
+	Dabbrev(r,_,Tprop) | 
+	  Dglob(r,MLarity) | 
+	    Dglob(r,MLprop) ) as d :: l ->
       if List.mem r prm.to_appear then
 	d :: (optimize prm l) 
       else optimize prm l
   | Dglob (r,t) :: l ->
-      let t = normalize t in
+      let t = optimize_fix (normalize t) in
       let b = expand (strict_language prm.lang) r t in
       let l = if b then 
 	begin
@@ -513,3 +544,7 @@ let rec optimize prm = function
 	Dglob (r,t) :: (optimize prm l)
       else
 	optimize prm l
+  | (Dtype _ | Dabbrev _ | Dcustom _) as d :: l -> 
+      d :: (optimize prm l)
+
+
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index bc5a137640..2c5a586acf 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -41,6 +41,11 @@ val ml_subst : ml_ast -> ml_ast -> ml_ast
 
 val subst_glob_ast : global_reference -> ml_ast -> ml_ast -> ml_ast
 
+(*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
+    the list [id1;...;idn] and the term [t]. *)
+
+val collect_lambda : ml_ast -> identifier list * ml_ast
+
 (*s Some transformations of ML terms. [normalize] and [normalize_decl] reduce
     all beta redexes (when the argument does not occur, it is just
     thrown away; when it occurs exactly once it is substituted; otherwise
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index a2d79fa664..1a7d151fb3 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -91,16 +91,6 @@ let push_vars ids (db,avoid) =
 
 let get_db_name n (db,_) = List.nth db (pred n)
 
-(*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
-    the list [id1;...;idn] and the term [t]. *)
-
-let collect_lambda = 
-  let rec collect acc = function
-    | MLlam(id,t) -> collect (id::acc) t
-    | x           -> acc,x
-  in 
-  collect []
-
 (*s Ocaml renaming issues. *)
 
 let keywords =     
@@ -334,9 +324,10 @@ let warning_coinductive r =
 
 let pp_decl = function
   | Dtype ([], _) -> 
-      [< >]
+      if P.toplevel then hOV 0 [< 'sTR " prop (* Logic inductive *)"; 'fNL >]
+      else [< >] 
   | Dtype ((_,r,_)::_ as i, cofix) -> 
-      if cofix && P.cofix_warning then if_verbose warning_coinductive r; 
+      if cofix && (not P.toplevel) then if_verbose warning_coinductive r; 
       hOV 0 (pp_inductive i)
   | Dabbrev (r, l, t) ->
       hOV 0 [< 'sTR "type"; 'sPC; pp_parameters l; 
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 2b00192309..b982adcdc6 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -35,7 +35,6 @@ type env = identifier list * Idset.t
 val rename_vars: Idset.t -> identifier list -> env
 val push_vars : identifier list -> env -> identifier list * env
 val get_db_name : int -> env -> identifier
-val collect_lambda : ml_ast -> identifier list * ml_ast
 
 val keywords : Idset.t