New handling of obligations.

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

11 files changed, 219 insertions, 95 deletions

diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index b1694d7c2..449e0abe1 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -4,7 +4,7 @@ Notation "'fun' { x : A | P } => Q" :=
   (fun x:{x:A|P} => Q)
   (at level 200, x ident, right associativity).
 
-Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Notation "( x & y )" := (@exist _ _ x y) : core_scope.
 
 Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
 intros.
@@ -44,3 +44,4 @@ end.
 
 Ltac destruct_exists := repeat (destruct_one_pair) .
 
+Extraction Inline proj1_sig.
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 678655186..9c11569ef 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -65,13 +65,52 @@ let subst_evars evs n t =
 	       | ((_, Some _, _) :: tlh), (_ :: tla) ->
 		   aux tlh tla acc
 	       | [], [] -> acc
-	       | _, _ -> failwith "subst_evars: invalid argument"
+	       | _, _ -> acc (* failwith "subst_evars: invalid argument" *)
 	   in aux hyps (Array.to_list args) [] 
 	 in
 	   mkApp (ex, Array.of_list args))
     | _ -> map_constr_with_binders succ substrec depth c
   in 
     substrec 0 t
+
+let subst_evar_constr evs n t = 
+  let evar_info id = 
+    let rec aux i = function
+	(k, n, h, v) :: tl -> 
+	  if k = id then (n, h, v) else aux (succ i) tl
+      | [] -> raise Not_found
+    in 
+    let (c, hyps, v) = aux 0 evs in
+      c, hyps
+  in
+  let rec substrec depth c = match kind_of_term c with
+    | Evar (k, args) ->
+	(let ex, hyps = 
+	   try evar_info k
+	   with Not_found -> 
+	     anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
+	 in
+	   (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
+		       int (List.length hyps) ++ str " hypotheses"); 	      with _ -> () );
+	   (* Evar arguments are created in inverse order, 
+	      and we must not apply to defined ones (i.e. LetIn's)
+	   *)
+	 let args =
+	   let rec aux hyps args acc =
+	     match hyps, args with
+		 ((_, None, _) :: tlh), (c :: tla) -> 
+		   aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc)
+	       | ((_, Some _, _) :: tlh), (_ :: tla) ->
+		   aux tlh tla acc
+	       | [], [] -> acc
+	       | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
+	   in aux hyps (Array.to_list args) [] 
+	 in
+	   mkApp (ex, Array.of_list args))
+    | _ -> map_constr_with_binders succ substrec depth c
+  in 
+    substrec 0 t
+
       
 (** Substitute variable references in t using De Bruijn indices, 
   where n binders were passed through. *)
@@ -152,6 +191,74 @@ let eterm_term evm t tycon =
      with _ -> ());
     t'', tycon, evar_names
 
+let rec take n l = 
+  if n = 0 then [] else List.hd l :: take (pred n) (List.tl l)    
+
+let trunc_named_context n ctx = 
+  let len = List.length ctx in
+    take (len - n) ctx
+  
+let eterm_obligations name nclen evm t tycon = 
+  (* 'Serialize' the evars, we assume that the types of the existentials
+     refer to previous existentials in the list only *)
+  let evl = to_list evm in
+  trace (str "Eterm, transformed to list");
+  let evts = 
+    (* Remove existential variables in types and build the corresponding products *)
+    fold_right 
+      (fun (id, ev) l ->
+	 trace (str "Eterm: " ++ str "treating evar: " ++ int id);
+	 let hyps = Environ.named_context_of_val ev.evar_hyps in
+	 let hyps = trunc_named_context nclen hyps in
+	   trace (str "Named context is: " ++ Printer.pr_named_context (Global.env ()) hyps);
+	 let evtyp = etype_of_evar l ev hyps in
+	   trace (str "Evar's type is: " ++ Termops.print_constr_env (Global.env ()) evtyp);
+	 let y' = (id, hyps, evtyp) in
+	   y' :: l) 
+      evl []
+  in 
+  let evar_names = 
+    let i = ref 0 in
+      List.map (fun (id, h, c) -> incr i; 
+		  (id, id_of_string (string_of_id name ^ "_obligation_" ^ string_of_int !i), h, c)) evts
+  in
+  let t' = (* Substitute evar refs in the term by De Bruijn indices *)
+    subst_evar_constr (List.map (fun (id, n, h, c) -> id, mkVar n, h, c) evar_names) 0 t 
+  in
+  let _, evars =
+    fold_right
+      (fun (_, n, h, c) (acc, l) ->
+	 let evt = Termops.it_mkProd_wo_LetIn c acc in
+	   ((Name n, None, c) :: acc, (n, evt) :: l))
+      evar_names ([], [])
+  in
+    (try 
+       trace (str "Term given to eterm" ++ spc () ++
+		Termops.print_constr_env (Global.env ()) t);
+       trace (str "Term constructed in eterm" ++ spc () ++
+		Termops.print_constr_env (Global.env ()) t');
+       ignore(iter
+		(fun (n, typ) ->
+		   trace (str "Evar :" ++ spc () ++ str (string_of_id n) ++
+			    Termops.print_constr_env (Global.env ()) typ))
+		evars);
+     with _ -> ());
+    let subst_closure l = 
+      let l' = List.map2 (fun (id, _, h, c) cst -> (id, cst, h, c)) evar_names l in
+      let _, l'' = 
+	List.fold_right 
+	  (fun (id, cst, h, c) (acc, res) ->
+	     let cst' = applist (cst, List.rev acc) in
+	       (cst' :: acc, (id, cst', h, c) :: res))
+	  l' ([], [])
+      in
+      let t' = subst_evar_constr l'' 0 t in
+	trace (str "Term constructed in eterm" ++ spc () ++
+		 Termops.print_constr_env (Global.env ()) t');
+	t'
+    in
+      subst_closure, evars
+
 let mkMetas n = 
   let rec aux i acc = 
     if i > 0 then aux (pred i) (Evarutil.mk_new_meta () :: acc)
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index d6f058ebd..dec9efa8b 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -17,4 +17,7 @@ val mkMetas : int -> constr list
 
 val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list
 
+val eterm_obligations : identifier -> int -> evar_map -> constr -> types option -> 
+  (constr list -> constr) * (identifier * types) list
+
 val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index cd26e817c..ff3bcb82e 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -40,16 +40,31 @@ end
 
 open SubtacGram 
 open Util
+open Pcoq
+
+let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
 
 GEXTEND Gram
-  GLOBAL: subtac_gallina_loc;
+  GLOBAL: subtac_gallina_loc Constr.binder_let Constr.binder;
  
   subtac_gallina_loc:
     [ [ g = Vernac.gallina -> loc, g ] ]
     ;
-       
+
+  Constr.binder_let:
+    [ [ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> 
+	  let typ = mkAppC (sigref, [mkLambdaC ([id], t, c)]) in
+	    LocalRawAssum ([id], typ)
+    ] ];
+
+  Constr.binder:
+    [ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" ->
+	  let typ = mkAppC (sigref, [mkLambdaC ([id], c, p)]) in
+	    ([id], typ) ] ];
+
   END
 
+
 type ('a,'b) gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a, 'b) Genarg.abstract_argument_type
 
 let (wit_subtac_gallina_loc : (Genarg.tlevel, Proof_type.tactic) gallina_loc_argtype),
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index d1ac74b24..f2e7a999c 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -156,19 +156,19 @@ let subtac (loc, command) =
     match command with
 	VernacDefinition (defkind, (locid, id), expr, hook) -> 
 	    (match expr with
-		 ProveBody (bl, c) -> 
-		   let evm, c, ctyp = Subtac_pretyping.subtac_process env isevars id bl c None in
-		     trace (str "Starting proof");
-		     Command.start_proof id goal_kind c hook;
-		     trace (str "Started proof");	     
+		 ProveBody (bl, c) -> Subtac_pretyping.subtac_proof env isevars id bl c None
+(* 		   let evm, c, ctyp =  in *)
+(* 		     trace (str "Starting proof"); *)
+(* 		     Command.start_proof id goal_kind c hook; *)
+(* 		     trace (str "Started proof");	      *)
 		     
 	       | DefineBody (bl, _, c, tycon) -> 
-		   let evm, c, ctyp = Subtac_pretyping.subtac_process env isevars id bl c tycon in
-		   let tac = Eterm.etermtac (evm, c) in 
-		     trace (str "Starting proof");
-		     Command.start_proof id goal_kind ctyp hook;
-		     trace (str "Started proof");
-		     Pfedit.by tac)
+		   Subtac_pretyping.subtac_proof env isevars id bl c tycon
+		     (* let tac = Eterm.etermtac (evm, c) in  *)
+		     (* 		     trace (str "Starting proof"); *)
+		     (* 		     Command.start_proof id goal_kind ctyp hook; *)
+		     (* 		     trace (str "Started proof"); *)
+		     (* 		     Pfedit.by tac) *))
       | VernacFixpoint (l, b) -> 
 	  let _ = trace (str "Building fixpoint") in
 	    ignore(Subtac_command.build_recursive l b)
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index c173d7724..d664fe5c2 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -43,6 +43,7 @@ open Notation
 module SPretyping = Subtac_pretyping.Pretyping
 open Subtac_utils
 open Pretyping
+open Subtac_obligations
 
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
@@ -175,20 +176,18 @@ let rec gen_rels = function
     0 -> []
   | n -> mkRel n :: gen_rels (pred n)
 
-let id_of_name = function
-    Anonymous -> raise (Invalid_argument "id_of_name")
-  | Name n -> n
-
- 
 let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let sigma = Evd.empty in
   let isevars = ref (Evd.create_evar_defs sigma) in
   let env = Global.env() in 
   let pr c = my_print_constr env c in
   let prr = Printer.pr_rel_context env in
+  let prn = Printer.pr_named_context env in
   let pr_rel env = Printer.pr_rel_context env in
+  let nc = named_context env in
+  let nc_len = named_context_length nc in
   let _ = 
-    try debug 2 (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ 
+    try debug 2 (str "In named context: " ++ prn (named_context env) ++ str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ 
 		 Ppconstr.pr_binders bl ++ str " : " ++ 
 		 Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
 		 Ppconstr.pr_constr_expr body)
@@ -305,39 +304,22 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   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 evars_def, evars_typ, evars = Eterm.eterm_term evm fullcoqc (Some fullctyp) in 	
-  let evars_typ = out_some evars_typ in
-  (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_tac, sumg) = Subtac_utils.build_dependent_sum evars in
-  (try trace (str "Evars sum: " ++ my_print_constr env sumg);
-     trace (str "Evars type: " ++ my_print_constr env evars_typ);
-   with _ -> ());
-  let proofid = id_of_string (string_of_id recname ^ "_evars_proof") in
-    Command.start_proof proofid goal_proof_kind sumg
-      (fun strength gr -> 
-	 debug 2 (str "Proof finished");
-	 let def = constr_of_global gr in
-	 let args = Subtac_utils.destruct_ex def sumg in
-	 let _, newdef = decompose_lam_n (List.length args) evars_def in
-	 let constr = Term.substl (List.rev args) newdef in
-	   debug 2 (str "Applied existentials : " ++ my_print_constr env constr);
-	   let ce = 
-	     { const_entry_body = constr;
-	       const_entry_type = Some fullctyp;
-	       const_entry_opaque = false;
-	       const_entry_boxed = boxed} 
-	   in
-	   let _constant = Declare.declare_constant 
-			    recname (DefinitionEntry ce,IsDefinition Definition)
-	   in
-	     definition_message recname);
-    trace (str "Started existentials proof");
-    Pfedit.by sum_tac;
-    trace (str "Applied sum tac")  
+  let evars_def, evars = Eterm.eterm_obligations recname nc_len evm fullcoqc (Some fullctyp) in
+    (try trace (str "Generated obligations : ");
+       List.iter
+	 (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t))
+	 evars;
+     with _ -> ());    
+    let prog = 
+      {  prg_name = recname;
+	 prg_body = evars_def;
+	 prg_type = fullctyp;
+	 prg_obligations = obligations_of_evars evars;
+      }
+    in
+      trace (str "Adding to obligations list");
+      Subtac_obligations.add_entry recname prog;
+      trace (str "Added to obligations list")
 
 let build_mutrec l boxed = 
   let sigma = Evd.empty
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 5cea7e8af..ede753711 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -9,19 +9,19 @@ open Summary
 open Libobject
 open Entries
 open Decl_kinds
-
+open Util
 
 type obligation =
     { obl_name : identifier;
       obl_type  : types;
-      obl_body : global_reference option;
+      obl_body : constr option;
     }
 
 type obligations = (obligation array * int)
 
 type program_info = {
   prg_name: identifier;
-  prg_body: constr;
+  prg_body: constr list -> constr;
   prg_type: types;
   prg_obligations: obligations;
 }
@@ -38,11 +38,10 @@ let map_cardinal m =
 exception Found of program_info
 
 let map_first m = 
-  let x = ref None in 
-    try
-      ProgMap.iter (fun _ v -> raise (Found v)) m;
-      assert(false)
-    with Found x -> x
+  try
+    ProgMap.iter (fun _ v -> raise (Found v)) m;
+    assert(false)
+  with Found x -> x
       
 let map_single m = 
   if map_cardinal m = 1 then map_first m
@@ -63,25 +62,6 @@ let _ =
 let add_entry _ e =
   from_prg := ProgMap.add e.prg_name e !from_prg
     
-(* let subst_th (_,subst,th) =  *)
-(*   let c' = subst_mps subst th.ring_carrier in                    *)
-(*   let eq' = subst_mps subst th.ring_req in *)
-(*   let thm1' = subst_mps subst th.ring_lemma1 in *)
-(*   let thm2' = subst_mps subst th.ring_lemma2 in *)
-(*   let tac'= subst_tactic subst th.ring_cst_tac in *)
-(*   if c' == th.ring_carrier && *)
-(*      eq' == th.ring_req && *)
-(*      thm1' == th.ring_lemma1 && *)
-(*      thm2' == th.ring_lemma2 && *)
-(*      tac' == th.ring_cst_tac then th *)
-(*   else *)
-(*     { ring_carrier = c'; *)
-(*       ring_req = eq'; *)
-(*       ring_cst_tac = tac'; *)
-(*       ring_lemma1 = thm1'; *)
-(*       ring_lemma2 = thm2' } *)
-
-
 let (theory_to_obj, obj_to_theory) = 
   let cache_th (name,th) = add_entry name th
   and export_th x = Some x in
@@ -94,8 +74,11 @@ let (theory_to_obj, obj_to_theory) =
       export_function = export_th }
 
 let declare_definition prg = 
+  let obls_constrs = 
+    Array.fold_right (fun x acc -> (out_some x.obl_body) :: acc) (fst prg.prg_obligations) []
+  in
   let ce = 
-    { const_entry_body = prg.prg_body;
+    { const_entry_body = prg.prg_body obls_constrs;
       const_entry_type = Some prg.prg_type;
       const_entry_opaque = false;
       const_entry_boxed = false} 
@@ -107,9 +90,8 @@ let declare_definition prg =
 
 let error s = Util.error s
 
-
-let subtac_obligation (num, name) =
-  let num = pred num in
+let subtac_obligation (user_num, name) =
+  let num = pred user_num in
   let prg_infos = !from_prg in
   let prg = 
     match name with
@@ -125,18 +107,30 @@ let subtac_obligation (num, name) =
 	    None -> 
 	      Command.start_proof obl.obl_name Subtac_utils.goal_proof_kind obl.obl_type
 		(fun strength gr -> 
-		   debug 2 (str "Proof of obligation " ++ int num ++ str " finished");
-		   let rem = snd prg.prg_obligations in
-		     if rem > 0 then (
-		       let obl = { obl with obl_body = Some gr } in
-		       let obls = Array.copy obls in
-			 obls.(num) <- obl;
-			 from_prg := map_replace prg.prg_name { prg with prg_obligations = (obls, rem) } !from_prg)
+		   debug 2 (str "Proof of obligation " ++ int user_num ++ str " finished");		   
+		   let obl = { obl with obl_body = Some (Libnames.constr_of_global gr) } in
+		   let obls = Array.copy obls in
+		   let _ = obls.(num) <- obl in
+		   let prg' = { prg with prg_obligations = (obls, pred rem) } in
+		     if rem > 1 then (
+		       debug 2 (int rem ++ str " obligations remaining");
+		       from_prg := map_replace prg.prg_name prg' !from_prg)
 		     else (
-		       declare_definition prg;
+		       declare_definition prg';
 		       from_prg := ProgMap.remove prg.prg_name !from_prg
 		     ));
-		trace (str "Started obligation " ++ int num ++ str "  proof")
+	      trace (str "Started obligation " ++ int user_num ++ str "  proof")
 	  | Some r -> error "Obligation already solved"
     else error (sprintf "Unknown obligation number %i" (succ num))
       
+      
+let obligations_of_evars evars =
+  let arr = 
+    Array.of_list
+      (List.map
+	 (fun (n, t) ->
+	    { obl_name = n;
+	      obl_type = t;
+	      obl_body = None;
+	    }) evars)
+  in arr, Array.length arr
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index d0240f5a5..6f7aaa5cc 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -151,3 +151,20 @@ let subtac_process env isevars id l c tycon =
   let evm = non_instanciated_map env isevars in
   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in
     evm, fullcoqc, fullctyp
+
+open Subtac_obligations
+
+let subtac_proof env isevars id l c tycon =
+  let nc = named_context env in
+  let nc_len = named_context_length nc in
+  let evm, coqc, coqt = subtac_process env isevars id l c tycon in
+  let evars_def, evars = Eterm.eterm_obligations id nc_len evm coqc (Some coqt) in
+  let prog = 
+    {  prg_name = id;
+       prg_body = evars_def;
+       prg_type = coqt;
+       prg_obligations = obligations_of_evars evars;
+    }
+  in
+    trace (str "Adding to obligations list");
+    add_entry id prog
diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli
index 97e56ecb2..b62a8766a 100644
--- a/contrib/subtac/subtac_pretyping.mli
+++ b/contrib/subtac/subtac_pretyping.mli
@@ -10,3 +10,6 @@ module Pretyping : Pretyping.S
 
 val subtac_process : env -> evar_defs ref -> identifier -> local_binder list ->
   constr_expr -> constr_expr option -> evar_map * constr * types
+
+val subtac_proof : env -> evar_defs ref -> identifier -> local_binder list ->
+  constr_expr -> constr_expr option -> unit
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 702410230..672c86e90 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -80,6 +80,7 @@ open Pp
 let my_print_constr = Termops.print_constr_env
 let my_print_constr_expr = Ppconstr.pr_constr_expr
 let my_print_context = Termops.print_rel_context
+let my_print_named_context = Termops.print_named_context
 let my_print_env = Termops.print_env
 let my_print_rawconstr = Printer.pr_rawconstr_env
 let my_print_evardefs = Evd.pr_evar_defs
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 9eed53e4e..7f3d3640a 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -10,6 +10,7 @@ open Rawterm
 open Util
 open Evarutil
 open Names
+open Sign
 
 val contrib_name : string
 val subtac_dir : string list
@@ -51,6 +52,7 @@ val my_print_constr : env -> constr -> std_ppcmds
 val my_print_constr_expr : constr_expr -> std_ppcmds
 val my_print_evardefs : evar_defs -> std_ppcmds
 val my_print_context : env -> std_ppcmds
+val my_print_named_context : env -> std_ppcmds
 val my_print_env : env -> std_ppcmds
 val my_print_rawconstr : env -> rawconstr -> std_ppcmds
 val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds
@@ -88,7 +90,6 @@ val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->
 val destruct_ex : constr -> constr -> constr list
 
 val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr
-
 val id_of_name : name -> identifier
 
 val definition_message : identifier -> unit