conservation des arguments dans Prop (snif)

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

4 files changed, 33 insertions, 15 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index 92f731842..2b50f0026 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -11,5 +11,5 @@ Declare ML Module "mlutil.cmo" "ocaml.cmo" "extraction.cmo" "extract_env.cmo".
 Grammar vernac vernac : ast :=
   extr_constr [ "Extraction" constrarg($c) "." ] -> 
               [(Extraction $c)]
-| extr_list   [ "Extraction" "[" ne_qualidarg_list($l) "]" "." ] ->
+| extr_list   [ "Extraction" "-r" ne_qualidarg_list($l) "." ] ->
               [(ExtractionList ($LIST $l))].
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 1e8d13f76..d3b65e03f 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -241,6 +241,8 @@ let decompose_lam_eta n env c =
     let e = applist (lift dif e, List.rev_map mkRel (interval 1 dif)) in
     (binders, e)
 
+let rec abstract_n n a = 
+  if n = 0 then a else MLlam (anonymous, ml_lift 1 (abstract_n (n-1) a))
 
 (*s Tables to keep the extraction of inductive types and constructors. *)
 
@@ -257,7 +259,7 @@ let add_inductive_extraction i e =
 let lookup_inductive_extraction i = Gmap.find i !inductive_extraction_table
 
 type constructor_extraction_result = 
-  | Cml of ml_type list * signature
+  | Cml of ml_type list * signature * int
   | Cprop
 
 let constructor_extraction_table = 
@@ -427,8 +429,8 @@ and extract_term_with_type env ctx c t =
 	let d' = extract_term env' ctx' d in 
 	(* If [d] was of type an arity, [c] too would be so *)
 	(match v with
-	   | Varity | Vprop -> d'
-	   | Vdefault -> match d' with
+	   | Varity -> d'
+	   | Vprop | Vdefault -> match d' with
 	       | Rmlterm a -> Rmlterm (MLlam (id, a))
 	       | Rprop -> assert false (* Cf. rem. above *))
     | IsRel n ->
@@ -453,11 +455,17 @@ and extract_term_with_type env ctx c t =
     | IsConst (sp,_) ->
 	Rmlterm (MLglob (ConstRef sp))
     | IsMutConstruct (cp,_) ->
-	let s = signature_of_constructor cp in
-	let n =  
-	  List.fold_left (fun n (v,_) -> if v = Vdefault then n+1 else n) 0 s 
+	let (s,n) = signature_of_constructor cp in
+	let ns = List.length s + 1 in
+	let rec abstract rels i = function
+	  | [] -> 
+	      MLcons (ConstructRef cp, List.length rels, List.rev rels)
+	  | (Vdefault,id) :: l -> 
+	      MLlam (id, abstract (MLrel (ns - i) :: rels) (succ i) l)
+	  | (_,id) :: l ->
+	      MLlam (id, abstract rels (succ i) l)
 	in
-	Rmlterm (MLcons (ConstructRef cp,n,[]))
+	Rmlterm (abstract_n n (abstract [] 1 s))
     | IsMutCase ((ni,(ip,cnames,_,_,_)),p,c,br) ->
 	let extract_branch_aux j b = 	  
 	  let (binders,e) = decompose_lam_eta ni.(j) env b in
@@ -474,7 +482,7 @@ and extract_term_with_type env ctx c t =
 	in
 	let extract_branch j b =
 	  let cp = (ip,succ j) in
-	  let s = signature_of_constructor cp in
+	  let (s,_) = signature_of_constructor cp in
 	  assert (List.length s = ni.(j));
 	  (* number of arguments, without parameters *)
 	  let (binders, e') = extract_branch_aux j b in
@@ -531,7 +539,8 @@ and extract_app env ctx (f,tyf,sf) args =
   let mlargs = 
     List.fold_right 
       (fun (v,a) args -> match v with
-	 | (Varity | Vprop), _ -> args
+	 | Varity,_ -> args
+	 | Vprop,_ -> MLprop :: args
 	 | Vdefault,_ ->  
 	     (* We can't trust the tag [Vdefault], we use [extract_constr] *)
 	     match extract_constr env ctx a with 
@@ -592,7 +601,7 @@ and extract_constructor (((sp,_),_) as c) =
 
 and signature_of_constructor cp = match extract_constructor cp with
   | Cprop -> assert false
-  | Cml (_,s) -> s
+  | Cml (_,s,n) -> (s,n)
 
 and extract_mib sp =
   if not (Gmap.mem (sp,0) !inductive_extraction_table) then begin
@@ -613,10 +622,11 @@ and extract_mib sp =
     let fl = 
       array_foldi
 	(fun i ib fl ->
-	   let mis = build_mis ((sp,i),[||]) mib in
+	   let ip = (sp,i) in
+	   let mis = build_mis (ip,[||]) mib in
 	   if mis_sort mis = Prop Null then
 	     (for j = 0 to mis_nconstr mis do
-	       add_constructor_extraction ((sp,i),succ j) Cprop
+		add_constructor_extraction (ip,succ j) Cprop
 	      done;
 	      fl)
 	   else
@@ -630,7 +640,8 @@ and extract_mib sp =
 		    | Tarity | Tprop -> assert false
 		    | Tmltype (mlt, s, f) -> 
 			let l = list_of_ml_arrows mlt in
-			add_constructor_extraction ((sp,i),succ j) (Cml (l,s));
+			let cp = (ip,succ j) in
+			add_constructor_extraction cp (Cml (l,s,nparams));
 			f @ fl)
 	       ib.mind_nf_lc fl)
 	mib.mind_packets []
@@ -652,7 +663,7 @@ and extract_inductive_declaration sp =
     let cp = (ind,succ j) in
     match lookup_constructor_extraction cp with 
       | Cprop -> assert false
-      | Cml (t,_) -> (ConstructRef cp, t)
+      | Cml (t,_,_) -> (ConstructRef cp, t)
   in
   let l = 
     array_foldi
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 16cb33226..a8a3f470b 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -1,6 +1,8 @@
 
 open Miniml
 
+val anonymous : Names.identifier
+
 val occurs : int -> ml_ast -> bool
 
 val ml_lift : int -> ml_ast -> ml_ast
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index 138af0a2e..3d3fb10e7 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -105,6 +105,11 @@ Inductive titi : Set := tata : nat->nat->nat->nat->titi.
 Extraction (tata O).
 Extraction (tata O (S O)).
 
+Inductive eta : Set := eta_c : nat->Prop->nat->Prop->eta.
+Extraction eta_c.
+Extraction (eta_c O).
+Extraction (eta_c O True).
+Extraction (eta_c O True O).
 
 Inductive bidon [A:Prop;B:Type] : Set := tb : (x:A)(y:B)(bidon A B). 
 Definition fbidon := [A,B:Type][f:A->B->(bidon True nat)][x:A][y:B](f x y).