reparation du cas des arguments de type qui sont des arités + patch dummy applied

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

3 files changed, 19 insertions, 6 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index ad0f6053d..e6acb73ab 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -313,6 +313,10 @@ let parse_ind_args si args =
 
 let rec extract_type env c args ctx = 
   match kind_of_term (whd_betaiotazeta c) with
+    | Lambda (_,_,d) -> 
+	(match args with 
+	   | [] -> assert false (* This lambda must be reductible. *)
+	   | a :: args -> extract_type env (subst1 a d) args ctx)
     | Sort _ ->
 	Tdummy 
     | Prod (n,t,d) ->
@@ -362,7 +366,11 @@ let rec extract_type env c args ctx =
 and extract_type_app env (r,s) args ctx =
   let ml_args = 
     List.fold_right 
-      (fun (b,t) a -> if b then (extract_type env t [] ctx) :: a else a)
+      (fun (b,c) a -> if not b then a 
+       else 
+	 let p = List.length (fst (splay_prod env none (type_of env c))) in
+	 let ctx = iterate (fun l -> 0 :: l) p ctx in
+	 (extract_type_arity env c ctx p) :: a)
       (List.combine s args) []
   in Tapp ((Tglob r) :: ml_args)
 
@@ -554,7 +562,8 @@ 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 MLdummy
+  if is_default env t then extract_term_wt env c t 
+  else dummy_lams MLdummy (List.length (fst (splay_prod env none t)))
 
 (*S Extraction of a constr. *)
 
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 31066b0e5..d48fde802 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -40,3 +40,5 @@ val decl_is_logical_ind : global_reference -> bool
   a singleton inductive. *)
 
 val decl_is_singleton : global_reference -> bool
+
+val extract_type : env -> constr -> constr list -> int list -> ml_type
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index e024fb909..ef7d80e0c 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -323,7 +323,7 @@ Definition idpropset :=
 
 Definition funProp := [b:bool][x:True]<natTrue>if b then O else x.
 
-(*s prop and arity can be applied.... *)
+(*s prop and arity can be applied.... -> fixed ? *)
 
 Definition f : (X:Type)(nat->X)->(X->bool)->bool := 
  [X:Type;x:nat->X;y:X->bool](y (x O)).
@@ -336,13 +336,13 @@ Definition f_prop := (f (O=O) [_](refl_equal ? O) [_]true).
 Extraction NoInline f.
 Extraction f_prop.
 (* let f_prop =
-  f () (fun _ -> True)
+  f (fun _ -> ()) (fun _ -> True)
 *)
 
 Definition f_arity := (f Set [_:nat]nat [_:Set]true).
 Extraction f_arity.
 (* let f_arity =
-  f () (fun _ -> True)
+  f (fun _ -> ()) (fun _ -> True)
 *)
 
 Definition f_normal := (f nat [x]x [x](Cases x of O => true | _ => false end)).
@@ -383,6 +383,8 @@ let oups h0 = match h0 with
   | Cons0 (n, l) -> n
 *)
 
+(* Dependant type over Type *)
 
-
+Extraction (sigT Set [a:Set](option a)).
+(* (unit, Obj.t option) sigT *)