Progress in new wf def typing.

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

3 files changed, 89 insertions, 8 deletions

diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index db10cb2a1b..b1694d7c22 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -34,3 +34,13 @@ induction t.
  simpl ; auto.
 Qed.
 
+Ltac destruct_one_pair :=
+ match goal with
+ | [H : (ex _) |- _] => destruct H
+ | [H : (ex2 _) |- _] => destruct H
+ | [H : (sig _) |- _] => destruct H
+ | [H : (_ /\ _) |- _] => destruct H
+end.
+
+Ltac destruct_exists := repeat (destruct_one_pair) .
+
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 10c5f580b2..247336386d 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -222,7 +222,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r notation boxed =
   let projection = 
     mkApp (proj, [| argtyp ;
 		    (mkLambda (Name argid', argtyp,
-			       (mkApp (wf_rel, [|mkRel 1; mkRel 2|])))) ;
+			       (mkApp (wf_rel, [|mkRel 1; mkRel 3|])))) ;
 		    mkRel 1
 		 |])
   in
@@ -277,16 +277,54 @@ let build_wellfounded (recname, n, bl,arityc,body) r notation boxed =
   let fullctyp = Evarutil.nf_isevar !isevars typ in
   let _ = try trace (str "After evar normalization: " ++ spc () ++
 		 str "Coq term: " ++ my_print_constr env fullcoqc ++ spc ()
-		 ++ str "Coq type: " ++ my_print_constr env fullctyp) 
+		     ++ str "Coq type: " ++ my_print_constr env fullctyp) 
      with _ -> () 
   in
   let evm = non_instanciated_map env isevars in
   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in
-  let tac = Eterm.etermtac (evm, fullcoqc) in 
-    trace (str "Starting proof of goal: " ++ my_print_constr env fullctyp);
-    Command.start_proof recname goal_kind fullctyp (fun _ _ -> ());
-    trace (str "Started proof");
-    Pfedit.by tac
+  let evars_def, evars_typ, evars = Eterm.eterm_term evm fullcoqc (Some fullctyp) in 	
+  let evars_typ = out_some evars_typ in
+  let evars_sum =
+    if evars = [] then None
+    else (
+      (try trace (str "Building evars sum for : ");
+	 List.iter
+	   (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t))
+	   evars;
+       with _ -> ());
+      let sum = Subtac_utils.build_dependent_sum evars in
+	(try trace (str "Evars sum: " ++ my_print_constr env (snd sum));
+	   trace (str "Evars type: " ++ my_print_constr env evars_typ);
+	 with _ -> ());
+	Some sum)
+  in
+    match evars_sum with
+      | Some (sum_tac, sumg) -> 
+	  let proofid = id_of_string (string_of_id recname ^ "_evars_proof") in
+	    Command.start_proof proofid goal_kind sumg
+	      (fun _ gr -> 
+		 let constant = match gr with Libnames.ConstRef c -> c
+		   | _ -> assert(false)
+		 in
+		 let def = mkConst constant in
+		 let args = Subtac_utils.destruct_ex def sumg in
+		 let args = 
+		   List.map (fun c -> 
+			       try Reductionops.whd_betadeltaiota (Global.env ()) Evd.empty c
+			       with Not_found ->
+				 trace (str "Not_found while reducing " ++
+					my_print_constr (Global.env ()) c);
+				 c
+			    ) args		  
+		 in
+		 let _, newdef = decompose_lam_n (List.length args) evars_def in
+		 let constr = Term.substl (List.rev args) newdef in
+		   debug 1 (str "Applied existentials : " ++ my_print_constr env constr));
+	    trace (str "Started existentials proof");
+	    Pfedit.by sum_tac;
+	    trace (str "Applied sum tac")
+      | None -> ()
+
     
 let build_mutrec l boxed =
   let sigma = Evd.empty
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 31fea63d5c..0d3ebe1869 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -167,7 +167,7 @@ let build_dependent_sum l =
       (n, t) :: tl ->
 	let t' = mkLambda (Name n, t, typ) in
 	  trace (spc () ++ str ("treating evar " ^ string_of_id n));
-	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) t)
+	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) t)	    	     
 	   with _ -> ());
 	let tac' = 
 	  tclTHENS (assert_tac true (Name n) t) 
@@ -186,6 +186,39 @@ let build_dependent_sum l =
 	(_, hd) :: tl -> aux (intros, hd) tl
       | [] -> raise (Invalid_argument "build_dependent_sum")
 
+let id x = x
+
+let build_dependent_sum l =
+  let rec aux names conttac conttype = function
+      (n, t) :: ((_ :: _) as tl) ->
+	let hyptype = substl names t in
+	  trace (spc () ++ str ("treating evar " ^ string_of_id n));
+	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
+	   with _ -> ());
+	let tac = assert_tac true (Name n) hyptype in
+	let conttac = 
+	  (fun cont -> 
+	     conttac
+	     (tclTHENS tac
+		([intros;
+		  (tclTHENSEQ 
+		     [constructor_tac (Some 1) 1 
+			(Rawterm.ImplicitBindings [mkVar n]);
+		      cont]);
+		 ])))
+	in
+	let conttype = 
+	  (fun typ -> 
+	     let tex = mkLambda (Name n, t, typ) in
+	       conttype
+		 (mkApp (Lazy.force ex_ind, [| t; tex |])))
+	in
+	  aux (mkVar n :: names) conttac conttype tl
+    | (n, t) :: [] -> 
+	(conttac intros, conttype t)
+    | [] -> raise (Invalid_argument "build_dependent_sum")
+  in aux [] id id (List.rev l)       
+	  
 open Proof_type
 open Tacexpr