cofix; axiomes; eta-expansions pour variables de types mal generalisees (en cours)

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

2 files changed, 35 insertions, 12 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 616591048..c99d270ca 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -110,6 +110,13 @@ module Pp = Ocaml.Make(ToplevelParams)
 
 open Vernacinterp
 
+let extract_reference r =
+  mSGNL 
+    (if is_ml_extraction r then
+       [< 'sTR "User defined extraction:"; 'sPC; 'sTR (find_ml_extraction r) >]
+     else
+       Pp.pp_decl (extract_declaration r))
+
 let _ = 
   vinterp_add "Extraction"
     (function 
@@ -118,12 +125,9 @@ let _ =
 	      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.pp_decl (extract_declaration (ConstRef sp)))
-		| IsMutInd (ind,_) ->
-		    mSGNL (Pp.pp_decl (extract_declaration (IndRef ind)))
-		| IsMutConstruct (cs,_) ->
-		    mSGNL (Pp.pp_decl (extract_declaration (ConstructRef cs)))
+		| IsConst (sp,_) -> extract_reference (ConstRef sp)
+		| IsMutInd (ind,_) -> extract_reference (IndRef ind)
+		| IsMutConstruct (cs,_) -> extract_reference (ConstructRef cs)
 		(* Otherwise, output the ML type or expression *)
 		| _ ->
 		    match extract_constr (Global.env()) [] c with
@@ -196,7 +200,7 @@ let extract_module m =
   let get_reference = function
     | sp, Leaf o ->
 	(match Libobject.object_tag o with
-	   | "CONSTANT" -> ConstRef sp
+	   | "CONSTANT" | "PARAMETER" -> ConstRef sp
 	   | "INDUCTIVE" -> IndRef (sp,0)
 	   | _ -> failwith "caught")
     | _ -> failwith "caught"
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 0a0ec8029..dafd0747a 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -244,6 +244,23 @@ let decompose_lam_eta n env c =
 let rec abstract_n n a = 
   if n = 0 then a else MLlam (anonymous, ml_lift 1 (abstract_n (n-1) a))
 
+let dest_fix_cofix = function
+  | IsFix ((_,i),(ti,fi,ci)) -> (false,i,ti,fi,ci)
+  | IsCoFix (i,(ti,fi,ci)) -> (true,i,ti,fi,ci)
+  | _ -> assert false
+
+(*s Eta-expansion to bypass ML type inference limitations (due to possible
+    polymorphic references, the ML type system does not generalize all
+    type variables that could be generalized). *)
+
+let eta_expanse ec = function 
+  | Tmltype (Tarr _, _, _) ->
+      (match ec with
+	 | Emlterm (MLlam _) -> ec
+	 | Emlterm a -> Emlterm (MLlam (anonymous, MLapp (a, [MLrel 1])))
+	 | _ -> ec)
+  | _ -> ec
+
 (*s Error message when extraction ends on an axiom. *)
 
 let axiom_message sp =
@@ -371,7 +388,7 @@ and extract_type_rec_info env vl c args =
 	   |Iprop -> assert false
 		 (* Cf. initial tests *))
     | IsMutCase _ 
-    | IsFix _ ->
+    | IsFix _ | IsCoFix _ ->
 	let id = next_ident_away flexible_name vl in
 	Tmltype (Tvar id, [], id :: vl)
 	  (* CIC type without counterpart in ML: we generate a 
@@ -554,7 +571,8 @@ and extract_term_info_with_type env ctx c t =
 	     | Rprop -> (* Logical singleton elimination *)
 		 assert (Array.length br = 1);
 		 snd (extract_branch_aux 0 br.(0)))
-      | IsFix ((_,i),(ti,fi,ci)) ->
+      | IsFix _ | IsCoFix _ as c ->
+          let (cofix,i,ti,fi,ci) = dest_fix_cofix c in
 	  let n = Array.length ti in
 	  let (env', ctx') = fix_environment env ctx fi ti in
 	  let extract_fix_body c t =
@@ -578,8 +596,7 @@ and extract_term_info_with_type env ctx c t =
 		 extract_term_info env' (false :: ctx) c2)
       | IsCast (c, _) ->
 	  extract_term_info_with_type env ctx c t
-      | IsMutInd _ | IsProd _ | IsSort _ | IsVar _ 
-      | IsMeta _ | IsEvar _ | IsCoFix _ ->
+      | IsMutInd _ | IsProd _ | IsSort _ | IsVar _ | IsMeta _ | IsEvar _ ->
 	  assert false 
 	    
 and extract_app env ctx (f,tyf,sf) args =
@@ -656,7 +673,9 @@ and extract_constant sp =
       | Some c -> c 
       | None -> axiom_message sp
     in
-    let e = extract_constr_with_type (Global.env()) [] body typ in
+    let env = Global.env() in
+    let e = extract_constr_with_type env [] body typ in
+    let e = eta_expanse e (extract_type env typ) in
     constant_table := Gmap.add sp e !constant_table;
     e