Add the ability to give a specific tactic to solve each obligation in

Program. No syntax to do it yet.


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

6 files changed, 63 insertions, 40 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 6e522d499..00a69bba7 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -14,6 +14,7 @@ open List
 open Pp
 open Util
 open Subtac_utils
+open Proof_type
 
 let trace s = 
   if !Flags.debug then (msgnl s; msgerr s)
@@ -25,10 +26,11 @@ let succfix (depth, fixrels) =
 type oblinfo =
   { ev_name: int * identifier;
     ev_hyps: named_context;
-    ev_status : obligation_definition_status;
+    ev_status: obligation_definition_status;
     ev_chop: int option;
     ev_loc: Util.loc;
     ev_typ: types;
+    ev_tac: Tacexpr.raw_tactic_expr option;
     ev_deps: Intset.t }
     
 (** Substitute evar references in t using De Bruijn indices, 
@@ -186,9 +188,16 @@ let eterm_obligations env name isevars evm fs ?status t ty =
 	   | Some s -> s, None
 	   | None -> Define true, None
 	 in
+	 let tac = match ev.evar_extra with 
+	   | Some t -> 
+	       if Dyn.tag t = "tactic" then 
+		 Some (Tacinterp.globTacticIn (Tacinterp.tactic_out t))
+	       else None
+	   | None -> None
+	 in
 	 let info = { ev_name = (n, nstr);
 		      ev_hyps = hyps; ev_status = status; ev_chop = chop;
-		      ev_loc = loc; ev_typ = evtyp ; ev_deps = deps }
+		      ev_loc = loc; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
 	 in (id, info) :: l) 
       evn []
   in 
@@ -199,12 +208,12 @@ let eterm_obligations env name isevars evm fs ?status t ty =
   let evars = 
     List.map (fun (_, info) ->
       let { ev_name = (_, name); ev_status = status;
-	    ev_loc = loc; ev_typ = typ; ev_deps = deps } = info
+	    ev_loc = loc; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
       in
       let status = match status with
 	| Define true when Idset.mem name transparent -> Define false
 	| _ -> status
-      in name, typ, loc, status, deps) evts
+      in name, typ, loc, status, deps, tac) evts
   in Array.of_list (List.rev evars), t', ty
 
 let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index a2010c901..413823ffe 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -13,18 +13,20 @@ open Term
 open Evd
 open Names
 open Util
+open Tacinterp
 
 val mkMetas : int -> constr list
 
 val evar_dependencies : evar_map -> int -> Intset.t
 val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * Intset.t) list
-
+  
 (* env, id, evars, number of function prototypes to try to clear from
    evars contexts, object and type *)
 val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> 
   ?status:obligation_definition_status -> constr -> types -> 
-  (identifier * types * loc * obligation_definition_status * Intset.t) array * constr * types
-    (* Obl. name, type as product, location of the original evar, 
+  (identifier * types * loc * obligation_definition_status * Intset.t * 
+      Tacexpr.raw_tactic_expr option) array * constr * types
+    (* Obl. name, type as product, location of the original evar, associated tactic,
        status and dependencies as indexes into the array *)
 
 val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 5cd9151f0..c1e168da1 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -112,25 +112,25 @@ END
 
 VERNAC COMMAND EXTEND Subtac_Solve_Obligation
 | [ "Solve" "Obligation" integer(num) "of" ident(name) "using" tactic(t) ] -> 
-    [ Subtac_obligations.try_solve_obligation num (Some name) (Tacinterp.interp t) ]
+    [ Subtac_obligations.try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ]
 | [ "Solve" "Obligation" integer(num) "using" tactic(t) ] -> 
-    [ Subtac_obligations.try_solve_obligation num None (Tacinterp.interp t) ]
+    [ Subtac_obligations.try_solve_obligation num None (Some (Tacinterp.interp t)) ]
       END
 
 VERNAC COMMAND EXTEND Subtac_Solve_Obligations
 | [ "Solve" "Obligations" "of" ident(name) "using" tactic(t) ] -> 
-    [ Subtac_obligations.try_solve_obligations (Some name) (Tacinterp.interp t) ]
+    [ Subtac_obligations.try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ]
 | [ "Solve" "Obligations" "using" tactic(t) ] -> 
-    [ Subtac_obligations.try_solve_obligations None (Tacinterp.interp t) ]
+    [ Subtac_obligations.try_solve_obligations None (Some (Tacinterp.interp t)) ]
 | [ "Solve" "Obligations" ] -> 
-    [ Subtac_obligations.try_solve_obligations None (Subtac_obligations.default_tactic ()) ]
+    [ Subtac_obligations.try_solve_obligations None None ]
       END
 
 VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations
 | [ "Solve" "All" "Obligations" "using" tactic(t) ] -> 
-    [ Subtac_obligations.solve_all_obligations (Tacinterp.interp t) ]
+    [ Subtac_obligations.solve_all_obligations (Some (Tacinterp.interp t)) ]
 | [ "Solve" "All" "Obligations" ] -> 
-    [ Subtac_obligations.solve_all_obligations (Subtac_obligations.default_tactic ()) ]
+    [ Subtac_obligations.solve_all_obligations None ]
       END
 
 VERNAC COMMAND EXTEND Subtac_Admit_Obligations
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index ce75299de..cc1e2dde2 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -15,6 +15,7 @@ open Decl_kinds
 open Util
 open Evd
 open Declare
+open Proof_type
 
 type definition_hook = global_reference -> unit
 
@@ -28,8 +29,9 @@ let explain_no_obligations = function
     Some ident -> str "No obligations for program " ++ str (string_of_id ident)
   | None -> str "No obligations remaining"
 
-type obligation_info = (Names.identifier * Term.types * loc * obligation_definition_status * Intset.t) array
-
+type obligation_info = (Names.identifier * Term.types * loc * obligation_definition_status * Intset.t
+			 * Tacexpr.raw_tactic_expr option) array
+  
 type obligation =
     { obl_name : identifier;
       obl_type : types;
@@ -37,6 +39,7 @@ type obligation =
       obl_body : constr option;
       obl_status : obligation_definition_status;
       obl_deps : Intset.t;
+      obl_tac : Tacexpr.raw_tactic_expr option;
     }
 
 type obligations = (obligation array * int)
@@ -284,11 +287,11 @@ let red = Reductionops.nf_betaiota
 let init_prog_info n b t deps fixkind notations obls impls kind hook =
   let obls' = 
     Array.mapi
-      (fun i (n, t, l, o, d) ->
+      (fun i (n, t, l, o, d, tac) ->
 	 debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d));
          { obl_name = n ; obl_body = None; 
 	   obl_location = l; obl_type = red t; obl_status = o;
-	   obl_deps = d })
+	   obl_deps = d; obl_tac = tac })
       obls
   in
     { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
@@ -416,7 +419,7 @@ let rec solve_obligation prg num =
 		  match update_obls prg obls (pred rem) with
 		  | Remain n when n > 0 ->
 		      if has_dependencies obls num then
-			ignore(auto_solve_obligations (Some prg.prg_name))
+			ignore(auto_solve_obligations (Some prg.prg_name) None)
 		  | _ -> ());
 	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
 		      Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
@@ -445,6 +448,14 @@ and solve_obligation_by_tac prg obls i tac =
 	(try
 	    if deps_remaining obls obl.obl_deps = [] then
 	     let obl = subst_deps_obl obls obl in
+	     let tac = 
+	       match tac with
+	       | Some t -> t
+	       | None -> 
+		   match obl.obl_tac with
+		   | Some t -> Tacinterp.interp t
+		   | None -> !default_tactic
+	     in
 	     let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
 	       obls.(i) <- declare_obligation obl t;
 	       true
@@ -481,13 +492,13 @@ and try_solve_obligation n prg tac =
   let obls' = Array.copy obls in
     if solve_obligation_by_tac prg obls' n tac then
       ignore(update_obls prg obls' (pred rem));
-    
+
 and try_solve_obligations n tac = 
   try ignore (solve_obligations n tac) with NoObligations _ -> ()
 
-and auto_solve_obligations n : progress =
+and auto_solve_obligations n tac : progress =
   Flags.if_verbose msgnl (str "Solving obligations automatically...");
-  try solve_obligations n !default_tactic with NoObligations _ -> Dependent
+  try solve_prg_obligations (get_prog_err n) tac with NoObligations _ -> Dependent
       
 open Pp
 let show_obligations ?(msg=true) n =
@@ -501,7 +512,8 @@ let show_obligations ?(msg=true) n =
 		   | None -> 
 		       if !showed > 0 then (
 			 decr showed;
-			 msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ 
+			 msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
+				   str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ 
 				   hov 1 (my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())))
 		   | Some _ -> ())
       obls
@@ -509,7 +521,8 @@ let show_obligations ?(msg=true) n =
 let show_term n =
   let prg = get_prog_err n in
   let n = prg.prg_name in
-    msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++ my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
+    msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++
+	      my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ my_print_constr (Global.env ()) prg.prg_body)
 
 let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun x -> ()) obls =
@@ -525,11 +538,7 @@ let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
     let len = Array.length obls in
     let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
       from_prg := ProgMap.add n prg !from_prg; 
-      let res =
-	match tactic with
-	| None -> auto_solve_obligations (Some n) 
-	| Some tac -> solve_obligations (Some n) tac
-      in
+      let res = auto_solve_obligations (Some n) tactic in
 	match res with
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	| _ -> res)
@@ -547,11 +556,7 @@ let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) notations f
       List.fold_left (fun finished x -> 
 	if finished then finished 
 	else
-	  let res =
-	    match tactic with
-	    | None -> auto_solve_obligations (Some x) 
-	    | Some tac -> solve_obligations (Some x) tac
-	  in
+	  let res = auto_solve_obligations (Some x) tactic in
 	    match res with
 	    | Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true
 	    | _ -> false) 
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 355ca7cd7..60c0a4139 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -2,9 +2,13 @@ open Names
 open Util
 open Libnames
 open Evd
+open Proof_type
 
-type obligation_info = (identifier * Term.types * loc * obligation_definition_status * Intset.t) array
-    (* ident, type, location, opaque or transparent, expand or define dependencies *)
+type obligation_info = 
+  (identifier * Term.types * loc * 
+      obligation_definition_status * Intset.t * Tacexpr.raw_tactic_expr option) array
+    (* ident, type, location, (opaque or transparent, expand or define),
+       dependencies, tactic to solve it *)
 
 type progress = (* Resolution status of a program *)
     | Remain of int  (* n obligations remaining *)
@@ -39,14 +43,14 @@ val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr op
 
 val next_obligation : Names.identifier option -> unit
 
-val solve_obligations : Names.identifier option -> Proof_type.tactic -> progress
+val solve_obligations : Names.identifier option -> Proof_type.tactic option -> progress
 (* Number of remaining obligations to be solved for this program *)
 
-val solve_all_obligations : Proof_type.tactic -> unit 
+val solve_all_obligations : Proof_type.tactic option -> unit 
 
-val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic -> unit
+val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic option -> unit
 
-val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit
+val try_solve_obligations : Names.identifier option -> Proof_type.tactic option -> unit
 
 val show_obligations : ?msg:bool -> Names.identifier option -> unit
 
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 0d41db8a4..6faae3adc 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -48,6 +48,9 @@ and interp_sign =
 val constr_of_id : Environ.env -> identifier -> constr
 
 (* To embed several objects in Coqast.t *)
+val tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t
+val tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr)
+  
 val tacticIn : (interp_sign -> raw_tactic_expr) -> raw_tactic_expr
 val globTacticIn : (interp_sign -> glob_tactic_expr) -> raw_tactic_expr
 val valueIn : value -> raw_tactic_arg