correction du eta_expanse

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

2 files changed, 32 insertions, 36 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 5fc7afbcb..8f70b560f 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -247,17 +247,6 @@ let rec abstract_n n a =
   if n = 0 then a else MLlam (anonymous, ml_lift 1 (abstract_n (n-1) a))
 
 
-(*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. *)
 
@@ -337,23 +326,17 @@ let rec extract_type env c =
 
 and extract_type_rec env c vl args = 
   (* We accumulate the context, arguments and generated variables list *)
-  try 
-    if sort_of env (applist (c, args)) = InProp 
-    then Tprop
-    else extract_type_rec_info env c vl args
-  with   
-      Anomaly _ -> 
-	let t = type_of env (applist (c, args)) in
-	(* Since [t] is an arity, there is two non-informative case: 
-	   [t] is an arity of sort [Prop], or 
-	   [c] has a non-informative head symbol *)
-	match get_arity env t with 
-	  | None -> 
-	      assert false (* Cf. precondition. *)
-	  | Some InProp ->
-	      Tprop 
-	  | Some _ -> extract_type_rec_info env c vl args
- 
+  let t = type_of env (applist (c, args)) in
+    (* Since [t] is an arity, there is two non-informative case: 
+       [t] is an arity of sort [Prop], or 
+       [c] has a non-informative head symbol *)
+    match get_arity env t with 
+      | None -> 
+	  assert false (* Cf. precondition. *)
+      | Some InProp ->
+	  Tprop 
+      | Some _ -> extract_type_rec_info env c vl args
+	    
 and extract_type_rec_info env c vl args = 
   match (kind_of_term (whd_betaiotalet env none c)) with
     | IsSort _ ->
@@ -739,10 +722,23 @@ and extract_constant sp =
              | (Logic,Arity) -> Emltype (Miniml.Tarity,[],[]))  (* Idem *)
       | Some body ->
           let e = extract_constr_with_type env [] body typ in
-          let e = eta_expanse e (extract_type env typ) in
+          let e = eta_expanse e typ in
           constant_table := Gmap.add sp e !constant_table;
           e
 
+(*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). *)
+
+and eta_expanse ec typ = match ec with 
+  | Emlterm (MLlam _) -> ec
+  | Emlterm a -> 
+      (match extract_type (Global.env()) typ with 
+	 | Tmltype (Tarr _, _, _) -> 
+	     Emlterm (MLlam (anonymous, MLapp (a, [MLrel 1])))
+	 | _ -> ec)
+  | _ -> ec 
+
 (*s Extraction of an inductive. *)
     
 and extract_inductive ((sp,_) as i) =
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index 9c421a27c..d59a149e5 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -94,7 +94,7 @@ Extraction horibilis.
 
 Inductive predicate : Type := 
   | Atom : Prop -> predicate
-  | And  : predicate -> predicate -> predicate.
+  | EAnd  : predicate -> predicate -> predicate.
 
 Extraction predicate.
 
@@ -153,7 +153,7 @@ Extraction PropSet.
 Definition natbool := [b:bool]if b then nat else bool.
 Extraction natbool.
 
-Definition zerotrue := [b:bool]<natbool>if b then 0 else true.
+Definition zerotrue := [b:bool]<natbool>if b then O else true.
 Extraction zerotrue.
 
 Definition natProp := [b:bool]<[_:bool]Type>if b then nat else Prop.
@@ -163,7 +163,7 @@ Definition natTrue := [b:bool]<[_:bool]Type>if b then nat else True.
 Definition zeroTrue := [b:bool]<natProp>if b then O else True.
 Extraction zeroTrue.
 
-Definition natTrue := [b:bool]<[_:bool]Type>if b then nat else True.
+Definition natTrue2 := [b:bool]<[_:bool]Type>if b then nat else True.
 
 Definition zeroprop := [b:bool]<natTrue>if b then O else I.
 Extraction zeroprop.
@@ -181,7 +181,7 @@ Extraction
 
 (* still ok via optim beta -> let *)
 
-Extraction [id':(X:Type)X->X](pair ? ? (id' nat O) (id' bool true)
+Extraction [id':(X:Type)X->X](pair ? ? (id' nat O) (id' bool true)).
 
 (* problem: fun f -> (f 0, f true) not legal in ocaml *)
 (* solution: fun f -> (f 0, Obj.magic f true) *)
@@ -191,13 +191,13 @@ Extraction [id':(X:Type)X->X](pair ? ? (id' nat O) (id' bool true)
 Definition funPropSet:= 
  [b:bool]<[_:bool]Type>if b then (X:Prop)X->X else (X:Set)X->X.
 
-Definition funPropSet2:=
- [b:bool](X:if b then Prop else Set)X->X.
+(* Definition funPropSet2:=
+ [b:bool](X:if b then Prop else Set)X->X. *)
 
 Definition idpropset := 
  [b:bool]<funPropSet>if b then [X:Prop][x:X]x else [X:Set][x:X]x.
 
-Definition proprop := [b:bool]((idpropset b) (natTrue b) (zeroprop b)).
+(* Definition proprop := [b:bool]((idpropset b) (natTrue b) (zeroprop b)). *)
 
 Definition funProp := [b:bool][x:True]<natTrue>if b then O else x.