summaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml417
-rw-r--r--tactics/auto.mli54
-rw-r--r--tactics/class_tactics.ml437
-rw-r--r--tactics/dhyp.ml359
-rw-r--r--tactics/dhyp.mli28
-rw-r--r--tactics/eauto.ml4146
-rw-r--r--tactics/eauto.mli4
-rw-r--r--tactics/extraargs.ml435
-rw-r--r--tactics/extraargs.mli2
-rw-r--r--tactics/extratactics.ml418
-rw-r--r--tactics/refine.ml2
-rw-r--r--tactics/rewrite.ml422
-rw-r--r--tactics/tacinterp.ml605
-rw-r--r--tactics/tacinterp.mli14
-rw-r--r--tactics/tacticals.ml1
-rw-r--r--tactics/tacticals.mli1
-rw-r--r--tactics/tactics.ml10
-rw-r--r--tactics/tactics.mllib1
18 files changed, 821 insertions, 935 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 93ca89f4..8a0de08b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -786,8 +786,6 @@ type hints_entry =
| HintsTransparencyEntry of evaluable_global_reference list * bool
| HintsExternEntry of
int * (patvar list * constr_pattern) option * glob_tactic_expr
- | HintsDestructEntry of identifier * int * (bool,unit) location *
- (patvar list * constr_pattern) * glob_tactic_expr
let h = id_of_string "H"
@@ -858,9 +856,6 @@ let interp_hints h =
let pat = Option.map fp patcom in
let tacexp = !forward_intern_tac (match pat with None -> [] | Some (l, _) -> l) tacexp in
HintsExternEntry (pri, pat, tacexp)
- | HintsDestruct(na,pri,loc,pat,code) ->
- let (l,_ as pat) = fp pat in
- HintsDestructEntry (na,pri,loc,pat,!forward_intern_tac l code)
let add_hints local dbnames0 h =
if List.mem "nocore" dbnames0 then
@@ -876,10 +871,6 @@ let add_hints local dbnames0 h =
add_transparency lhints b local dbnames
| HintsExternEntry (pri, pat, tacexp) ->
add_externs pri pat tacexp local dbnames
- | HintsDestructEntry (na,pri,loc,pat,code) ->
- if dbnames0<>[] then
- warn (str"Database selection not implemented for destruct hints");
- Dhyp.add_destructor_hint local na loc pat pri code
(**************************************************************************)
(* Functions for printing the hints *)
@@ -887,14 +878,14 @@ let add_hints local dbnames0 h =
let pr_autotactic =
function
- | Res_pf (c,clenv) -> (str"apply " ++ pr_lconstr c)
- | ERes_pf (c,clenv) -> (str"eapply " ++ pr_lconstr c)
- | Give_exact c -> (str"exact " ++ pr_lconstr c)
+ | Res_pf (c,clenv) -> (str"apply " ++ pr_constr c)
+ | ERes_pf (c,clenv) -> (str"eapply " ++ pr_constr c)
+ | Give_exact c -> (str"exact " ++ pr_constr c)
| Res_pf_THEN_trivial_fail (c,clenv) ->
- (str"apply " ++ pr_lconstr c ++ str" ; trivial")
+ (str"apply " ++ pr_constr c ++ str" ; trivial")
| Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c)
| Extern tac ->
- (str "(external) " ++ Pptactic.pr_glob_tactic (Global.env()) tac)
+ (str "(*external*) " ++ Pptactic.pr_glob_tactic (Global.env()) tac)
let pr_hint (id, v) =
(pr_autotactic v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
@@ -1107,6 +1098,131 @@ let conclPattern concl pat tac gl =
with PatternMatchingFailure -> error "conclPattern" in
!forward_interp_tactic constr_bindings tac gl
+(***********************************************************)
+(** A debugging / verbosity framework for trivial and auto *)
+(***********************************************************)
+
+(** The following options allow to trigger debugging/verbosity
+ without having to adapt the scripts.
+ Note: if Debug and Info are both activated, Debug take precedence. *)
+
+let global_debug_trivial = ref false
+let global_debug_auto = ref false
+let global_info_trivial = ref false
+let global_info_auto = ref false
+
+let add_option ls refe =
+ let _ = Goptions.declare_bool_option
+ { Goptions.optsync = true;
+ Goptions.optdepr = false;
+ Goptions.optname = String.concat " " ls;
+ Goptions.optkey = ls;
+ Goptions.optread = (fun () -> !refe);
+ Goptions.optwrite = (:=) refe }
+ in ()
+
+let _ =
+ add_option ["Debug";"Trivial"] global_debug_trivial;
+ add_option ["Debug";"Auto"] global_debug_auto;
+ add_option ["Info";"Trivial"] global_info_trivial;
+ add_option ["Info";"Auto"] global_info_auto
+
+let no_dbg () = (Off,0,ref [])
+
+let mk_trivial_dbg debug =
+ let d =
+ if debug = Debug || !global_debug_trivial then Debug
+ else if debug = Info || !global_info_trivial then Info
+ else Off
+ in (d,0,ref [])
+
+(** Note : we start the debug depth of auto at 1 to distinguish it
+ for trivial (whose depth is 0). *)
+
+let mk_auto_dbg debug =
+ let d =
+ if debug = Debug || !global_debug_auto then Debug
+ else if debug = Info || !global_info_auto then Info
+ else Off
+ in (d,1,ref [])
+
+let incr_dbg = function (dbg,depth,trace) -> (dbg,depth+1,trace)
+
+(** A tracing tactic for debug/info trivial/auto *)
+
+let tclLOG (dbg,depth,trace) pp tac =
+ match dbg with
+ | Off -> tac
+ | Debug ->
+ (* For "debug (trivial/auto)", we directly output messages *)
+ let s = String.make depth '*' in
+ begin fun gl ->
+ try
+ let out = tac gl in
+ msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
+ out
+ with e ->
+ msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
+ raise e
+ end
+ | Info ->
+ (* For "info (trivial/auto)", we store a log trace *)
+ begin fun gl ->
+ try
+ let out = tac gl in
+ trace := (depth, Some pp) :: !trace;
+ out
+ with e ->
+ trace := (depth, None) :: !trace;
+ raise e
+ end
+
+(** For info, from the linear trace information, we reconstitute the part
+ of the proof tree we're interested in. The last executed tactic
+ comes first in the trace (and it should be a successful one).
+ [depth] is the root depth of the tree fragment we're visiting.
+ [keep] means we're in a successful tree fragment (the very last
+ tactic has been successful). *)
+
+let rec cleanup_info_trace depth acc = function
+ | [] -> acc
+ | (d,Some pp) :: l -> cleanup_info_trace d ((d,pp)::acc) l
+ | l -> cleanup_info_trace depth acc (erase_subtree depth l)
+
+and erase_subtree depth = function
+ | [] -> []
+ | (d,_) :: l -> if d = depth then l else erase_subtree depth l
+
+let pr_info_atom (d,pp) =
+ msg_debug (str (String.make d ' ') ++ pp () ++ str ".")
+
+let pr_info_trace = function
+ | (Info,_,{contents=(d,Some pp)::l}) ->
+ List.iter pr_info_atom (cleanup_info_trace d [(d,pp)] l)
+ | _ -> ()
+
+let pr_info_nop = function
+ | (Info,_,_) -> msg_debug (str "idtac.")
+ | _ -> ()
+
+let pr_dbg_header = function
+ | (Off,_,_) -> ()
+ | (Debug,0,_) -> msg_debug (str "(* debug trivial : *)")
+ | (Debug,_,_) -> msg_debug (str "(* debug auto : *)")
+ | (Info,0,_) -> msg_debug (str "(* info trivial : *)")
+ | (Info,_,_) -> msg_debug (str "(* info auto : *)")
+
+let tclTRY_dbg d tac =
+ tclORELSE0
+ (fun gl ->
+ pr_dbg_header d;
+ let out = tac gl in
+ pr_info_trace d;
+ out)
+ (fun gl ->
+ pr_info_nop d;
+ tclIDTAC gl)
+
(**************************************************************************)
(* The Trivial tactic *)
(**************************************************************************)
@@ -1130,17 +1246,20 @@ let exists_evaluable_reference env = function
| EvalConstRef _ -> true
| EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false
-let rec trivial_fail_db mod_delta db_list local_db gl =
+let dbg_intro dbg = tclLOG dbg (fun () -> str "intro") intro
+let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption
+
+let rec trivial_fail_db dbg mod_delta db_list local_db gl =
let intro_tac =
- tclTHEN intro
+ tclTHEN (dbg_intro dbg)
(fun g'->
let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
- in trivial_fail_db mod_delta db_list (Hint_db.add_list hintl local_db) g')
+ in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db) g')
in
tclFIRST
- (assumption::intro_tac::
- (List.map (fun tac -> tclCOMPLETE tac)
- (trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl
+ ((dbg_assumption dbg)::intro_tac::
+ (List.map tclCOMPLETE
+ (trivial_resolve dbg mod_delta db_list local_db (pf_concl gl)))) gl
and my_find_search_nodelta db_list local_db hdc concl =
List.map (fun hint -> (None,hint))
@@ -1181,7 +1300,7 @@ and my_find_search_delta db_list local_db hdc concl =
in List.map (fun x -> (Some flags,x)) l)
(local_db::db_list)
-and tac_of_hint db_list local_db concl (flags, ({pat=p; code=t})) =
+and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t})) =
let tactic =
match t with
| Res_pf (c,cl) -> unify_resolve_gen flags (c,cl)
@@ -1190,23 +1309,26 @@ and tac_of_hint db_list local_db concl (flags, ({pat=p; code=t})) =
| Res_pf_THEN_trivial_fail (c,cl) ->
tclTHEN
(unify_resolve_gen flags (c,cl))
- (trivial_fail_db (flags <> None) db_list local_db)
- | Unfold_nth c ->
+ (* With "(debug) trivial", we shouldn't end here, and
+ with "debug auto" we don't display the details of inner trivial *)
+ (trivial_fail_db (no_dbg ()) (flags <> None) db_list local_db)
+ | Unfold_nth c ->
(fun gl ->
if exists_evaluable_reference (pf_env gl) c then
tclPROGRESS (h_reduce (Unfold [all_occurrences_expr,c]) onConcl) gl
else tclFAIL 0 (str"Unbound reference") gl)
| Extern tacast -> conclPattern concl p tacast
- in tactic
+ in
+ tclLOG dbg (fun () -> pr_autotactic t) tactic
-and trivial_resolve mod_delta db_list local_db cl =
+and trivial_resolve dbg mod_delta db_list local_db cl =
try
let head =
try let hdconstr,_ = head_constr_bound cl in
Some (head_of_constr_reference hdconstr)
with Bound -> None
in
- List.map (tac_of_hint db_list local_db cl)
+ List.map (tac_of_hint dbg db_list local_db cl)
(priority
(my_find_search mod_delta db_list local_db head cl))
with Not_found -> []
@@ -1223,255 +1345,126 @@ let make_db_list dbnames =
in
List.map lookup dbnames
-let trivial lems dbnames gl =
+let trivial ?(debug=Off) lems dbnames gl =
let db_list = make_db_list dbnames in
- tclTRY (trivial_fail_db false db_list (make_local_hint_db false lems gl)) gl
+ let d = mk_trivial_dbg debug in
+ tclTRY_dbg d
+ (trivial_fail_db d false db_list (make_local_hint_db false lems gl)) gl
-let full_trivial lems gl =
+let full_trivial ?(debug=Off) lems gl =
let dbnames = Hintdbmap.dom !searchtable in
let dbnames = list_remove "v62" dbnames in
let db_list = List.map (fun x -> searchtable_map x) dbnames in
- tclTRY (trivial_fail_db false db_list (make_local_hint_db false lems gl)) gl
+ let d = mk_trivial_dbg debug in
+ tclTRY_dbg d
+ (trivial_fail_db d false db_list (make_local_hint_db false lems gl)) gl
-let gen_trivial lems = function
- | None -> full_trivial lems
- | Some l -> trivial lems l
+let gen_trivial ?(debug=Off) lems = function
+ | None -> full_trivial ~debug lems
+ | Some l -> trivial ~debug lems l
-let h_trivial lems l =
- Refiner.abstract_tactic (TacTrivial (List.map snd lems,l))
- (gen_trivial lems l)
+let h_trivial ?(debug=Off) lems l =
+ Refiner.abstract_tactic (TacTrivial (debug,List.map snd lems,l))
+ (gen_trivial ~debug lems l)
(**************************************************************************)
(* The classical Auto tactic *)
(**************************************************************************)
-let possible_resolve mod_delta db_list local_db cl =
+let possible_resolve dbg mod_delta db_list local_db cl =
try
let head =
try let hdconstr,_ = head_constr_bound cl in
Some (head_of_constr_reference hdconstr)
with Bound -> None
in
- List.map (tac_of_hint db_list local_db cl)
+ List.map (tac_of_hint dbg db_list local_db cl)
(my_find_search mod_delta db_list local_db head cl)
with Not_found -> []
-let decomp_unary_term_then (id,_,typc) kont1 kont2 gl =
+let dbg_case dbg id =
+ tclLOG dbg (fun () -> str "case " ++ pr_id id) (simplest_case (mkVar id))
+
+let decomp_unary_term_then dbg (id,_,typc) kont1 kont2 gl =
try
let ccl = applist (head_constr typc) in
match Hipattern.match_with_conjunction ccl with
| Some (_,args) ->
- tclTHEN (simplest_case (mkVar id)) (kont1 (List.length args)) gl
+ tclTHEN (dbg_case dbg id) (kont1 (List.length args)) gl
| None ->
kont2 gl
with UserError _ -> kont2 gl
-let decomp_empty_term (id,_,typc) gl =
+let decomp_empty_term dbg (id,_,typc) gl =
if Hipattern.is_empty_type typc then
- simplest_case (mkVar id) gl
+ dbg_case dbg id gl
else
errorlabstrm "Auto.decomp_empty_term" (str "Not an empty type.")
let extend_local_db gl decl db =
Hint_db.add_list (make_resolve_hyp (pf_env gl) (project gl) decl) db
-(* Try to decompose hypothesis [decl] into atomic components of a
- conjunction with maximum depth [p] (or solve the goal from an
- empty type) then call the continuation tactic with hint db extended
- with the obtained not-further-decomposable hypotheses *)
-
-let rec decomp_and_register_decl p kont (id,_,_ as decl) db gl =
- if p = 0 then
- kont (extend_local_db gl decl db) gl
- else
- tclORELSE0
- (decomp_empty_term decl)
- (decomp_unary_term_then decl (intros_decomp (p-1) kont [] db)
- (kont (extend_local_db gl decl db))) gl
-
-(* Introduce [n] hypotheses, then decompose then with maximum depth [p] and
- call the continuation tactic [kont] with the hint db extended
- with the so-obtained not-further-decomposable hypotheses *)
-
-and intros_decomp p kont decls db n =
- if n = 0 then
- decomp_and_register_decls p kont decls db
- else
- tclTHEN intro (onLastDecl (fun d ->
- (intros_decomp p kont (d::decls) db (n-1))))
-
-(* Decompose hypotheses [hyps] with maximum depth [p] and
- call the continuation tactic [kont] with the hint db extended
- with the so-obtained not-further-decomposable hypotheses *)
-
-and decomp_and_register_decls p kont decls =
- List.fold_left (decomp_and_register_decl p) kont decls
+(* Introduce an hypothesis, then call the continuation tactic [kont]
+ with the hint db extended with the so-obtained hypothesis *)
+let intro_register dbg kont db =
+ tclTHEN (dbg_intro dbg)
+ (onLastDecl (fun decl gl -> kont (extend_local_db gl decl db) gl))
-(* decomp is an natural number giving an indication on decomposition
- of conjunction in hypotheses, 0 corresponds to no decomposition *)
(* n is the max depth of search *)
(* local_db contains the local Hypotheses *)
exception Uplift of tactic list
-let search_gen p n mod_delta db_list local_db =
- let rec search n local_db =
+let search d n mod_delta db_list local_db =
+ let rec search d n local_db =
if n=0 then (fun gl -> error "BOUND 2") else
- tclORELSE0 assumption
- (tclORELSE0 (intros_decomp p (search n) [] local_db 1)
- (fun gl -> tclFIRST
- (List.map (fun ntac -> tclTHEN ntac (search (n-1) local_db))
- (possible_resolve mod_delta db_list local_db (pf_concl gl))) gl))
+ tclORELSE0 (dbg_assumption d)
+ (tclORELSE0 (intro_register d (search d n) local_db)
+ (fun gl ->
+ let d' = incr_dbg d in
+ tclFIRST
+ (List.map
+ (fun ntac -> tclTHEN ntac (search d' (n-1) local_db))
+ (possible_resolve d mod_delta db_list local_db (pf_concl gl))) gl))
in
- search n local_db
-
-let search = search_gen 0
+ search d n local_db
let default_search_depth = ref 5
-let delta_auto mod_delta n lems dbnames gl =
+let delta_auto ?(debug=Off) mod_delta n lems dbnames gl =
let db_list = make_db_list dbnames in
- tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl)) gl
+ let d = mk_auto_dbg debug in
+ tclTRY_dbg d
+ (search d n mod_delta db_list (make_local_hint_db false lems gl)) gl
-let auto = delta_auto false
+let auto ?(debug=Off) n = delta_auto ~debug false n
-let new_auto = delta_auto true
+let new_auto ?(debug=Off) n = delta_auto ~debug true n
let default_auto = auto !default_search_depth [] []
-let delta_full_auto mod_delta n lems gl =
+let delta_full_auto ?(debug=Off) mod_delta n lems gl =
let dbnames = Hintdbmap.dom !searchtable in
let dbnames = list_remove "v62" dbnames in
let db_list = List.map (fun x -> searchtable_map x) dbnames in
- tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl)) gl
+ let d = mk_auto_dbg debug in
+ tclTRY_dbg d
+ (search d n mod_delta db_list (make_local_hint_db false lems gl)) gl
-let full_auto = delta_full_auto false
-let new_full_auto = delta_full_auto true
+let full_auto ?(debug=Off) n = delta_full_auto ~debug false n
+let new_full_auto ?(debug=Off) n = delta_full_auto ~debug true n
let default_full_auto gl = full_auto !default_search_depth [] gl
-let gen_auto n lems dbnames =
+let gen_auto ?(debug=Off) n lems dbnames =
let n = match n with None -> !default_search_depth | Some n -> n in
match dbnames with
- | None -> full_auto n lems
- | Some l -> auto n lems l
+ | None -> full_auto ~debug n lems
+ | Some l -> auto ~debug n lems l
let inj_or_var = Option.map (fun n -> ArgArg n)
-let h_auto n lems l =
- Refiner.abstract_tactic (TacAuto (inj_or_var n,List.map snd lems,l))
- (gen_auto n lems l)
-
-(**************************************************************************)
-(* The "destructing Auto" from Eduardo *)
-(**************************************************************************)
-
-(* Depth of search after decomposition of hypothesis, by default
- one look for an immediate solution *)
-let default_search_decomp = ref 20
-
-let destruct_auto p lems n gl =
- decomp_and_register_decls p (fun local_db gl ->
- search_gen p n false (List.map searchtable_map ["core";"extcore"])
- (add_hint_lemmas false lems local_db gl) gl)
- (pf_hyps gl)
- (Hint_db.empty empty_transparent_state false)
- gl
-
-let dautomatic des_opt lems n = tclTRY (destruct_auto des_opt lems n)
-
-let dauto (n,p) lems =
- let p = match p with Some p -> p | None -> !default_search_decomp in
- let n = match n with Some n -> n | None -> !default_search_depth in
- dautomatic p lems n
-
-let default_dauto = dauto (None,None) []
-
-let h_dauto (n,p) lems =
- Refiner.abstract_tactic (TacDAuto (inj_or_var n,p,List.map snd lems))
- (dauto (n,p) lems)
-
-(***************************************)
-(*** A new formulation of Auto *********)
-(***************************************)
-
-let make_resolve_any_hyp env sigma (id,_,ty) =
- let ents =
- map_succeed
- (fun f -> f (mkVar id,ty))
- [make_exact_entry sigma None; make_apply_entry env sigma (true,true,false) None]
- in
- ents
-
-type autoArguments =
- | UsingTDB
- | Destructing
-
-let compileAutoArg contac = function
- | Destructing ->
- (function g ->
- let ctx = pf_hyps g in
- tclFIRST
- (List.map
- (fun (id,_,typ) ->
- let cl = (strip_prod_assum typ) in
- if Hipattern.is_conjunction cl
- then
- tclTHENSEQ [simplest_elim (mkVar id); clear [id]; contac]
- else
- tclFAIL 0 (pr_id id ++ str" is not a conjunction"))
- ctx) g)
- | UsingTDB ->
- (tclTHEN
- (Tacticals.tryAllHypsAndConcl
- (function
- | Some id -> Dhyp.h_destructHyp false id
- | None -> Dhyp.h_destructConcl))
- contac)
-
-let compileAutoArgList contac = List.map (compileAutoArg contac)
-
-let rec super_search n db_list local_db argl gl =
- if n = 0 then error "BOUND 2";
- tclFIRST
- (assumption
- ::
- tclTHEN intro
- (fun g ->
- let hintl = pf_apply make_resolve_any_hyp g (pf_last_hyp g) in
- super_search n db_list (Hint_db.add_list hintl local_db)
- argl g)
- ::
- List.map (fun ntac ->
- tclTHEN ntac
- (super_search (n-1) db_list local_db argl))
- (possible_resolve false db_list local_db (pf_concl gl))
- @
- compileAutoArgList (super_search (n-1) db_list local_db argl) argl) gl
-
-let search_superauto n to_add argl g =
- let sigma =
- List.fold_right
- (fun (id,c) -> add_named_decl (id, None, pf_type_of g c))
- to_add empty_named_context in
- let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in
- let db = Hint_db.add_list db0 (make_local_hint_db false [] g) in
- super_search n [Hintdbmap.find "core" !searchtable] db argl g
-
-let superauto n to_add argl =
- tclTRY (tclCOMPLETE (search_superauto n to_add argl))
-
-let interp_to_add gl r =
- let r = locate_global_with_alias (qualid_of_reference r) in
- let id = basename_of_global r in
- (next_ident_away id (pf_ids_of_hyps gl), constr_of_global r)
-
-let gen_superauto nopt l a b gl =
- let n = match nopt with Some n -> n | None -> !default_search_depth in
- let al = (if a then [Destructing] else [])@(if b then [UsingTDB] else []) in
- superauto n (List.map (interp_to_add gl) l) al gl
-
-let h_superauto no l a b =
- Refiner.abstract_tactic (TacSuperAuto (no,l,a,b)) (gen_superauto no l a b)
-
+let h_auto ?(debug=Off) n lems l =
+ Refiner.abstract_tactic (TacAuto (debug,inj_or_var n,List.map snd lems,l))
+ (gen_auto ~debug n lems l)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 521c5ed2..87786e5b 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -102,8 +102,6 @@ type hints_entry =
| HintsTransparencyEntry of evaluable_global_reference list * bool
| HintsExternEntry of
int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr
- | HintsDestructEntry of identifier * int * (bool,unit) Tacexpr.location *
- (patvar list * constr_pattern) * Tacexpr.glob_tactic_expr
val searchtable_map : hint_db_name -> hint_db
@@ -220,59 +218,51 @@ val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -
val make_db_list : hint_db_name list -> hint_db list
-val auto : int -> open_constr list -> hint_db_name list -> tactic
+val auto : ?debug:Tacexpr.debug ->
+ int -> open_constr list -> hint_db_name list -> tactic
(** Auto with more delta. *)
-val new_auto : int -> open_constr list -> hint_db_name list -> tactic
+val new_auto : ?debug:Tacexpr.debug ->
+ int -> open_constr list -> hint_db_name list -> tactic
(** auto with default search depth and with the hint database "core" *)
val default_auto : tactic
(** auto with all hint databases except the "v62" compatibility database *)
-val full_auto : int -> open_constr list -> tactic
+val full_auto : ?debug:Tacexpr.debug ->
+ int -> open_constr list -> tactic
(** auto with all hint databases except the "v62" compatibility database
and doing delta *)
-val new_full_auto : int -> open_constr list -> tactic
+val new_full_auto : ?debug:Tacexpr.debug ->
+ int -> open_constr list -> tactic
(** auto with default search depth and with all hint databases
except the "v62" compatibility database *)
val default_full_auto : tactic
(** The generic form of auto (second arg [None] means all bases) *)
-val gen_auto : int option -> open_constr list -> hint_db_name list option -> tactic
+val gen_auto : ?debug:Tacexpr.debug ->
+ int option -> open_constr list -> hint_db_name list option -> tactic
(** The hidden version of auto *)
-val h_auto : int option -> open_constr list -> hint_db_name list option -> tactic
+val h_auto : ?debug:Tacexpr.debug ->
+ int option -> open_constr list -> hint_db_name list option -> tactic
(** Trivial *)
-val trivial : open_constr list -> hint_db_name list -> tactic
-val gen_trivial : open_constr list -> hint_db_name list option -> tactic
-val full_trivial : open_constr list -> tactic
-val h_trivial : open_constr list -> hint_db_name list option -> tactic
-val pr_autotactic : 'a auto_tactic -> Pp.std_ppcmds
-
-(** {6 The following is not yet up to date -- Papageno. } *)
-
-(** DAuto *)
-val dauto : int option * int option -> open_constr list -> tactic
-val default_search_decomp : int ref
-val default_dauto : tactic
-
-val h_dauto : int option * int option -> open_constr list -> tactic
+val trivial : ?debug:Tacexpr.debug ->
+ open_constr list -> hint_db_name list -> tactic
+val gen_trivial : ?debug:Tacexpr.debug ->
+ open_constr list -> hint_db_name list option -> tactic
+val full_trivial : ?debug:Tacexpr.debug ->
+ open_constr list -> tactic
+val h_trivial : ?debug:Tacexpr.debug ->
+ open_constr list -> hint_db_name list option -> tactic
-(** SuperAuto *)
-
-type autoArguments =
- | UsingTDB
- | Destructing
-
-(*
-val superauto : int -> (identifier * constr) list -> autoArguments list -> tactic
-*)
+val pr_autotactic : 'a auto_tactic -> Pp.std_ppcmds
-val h_superauto : int option -> reference list -> bool -> bool -> tactic
+(** Hook for changing the initialization of auto *)
val add_auto_init : (unit -> unit) -> unit
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 42df244d..e063124d 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -634,6 +634,23 @@ let has_undefined p oevd evd =
snd (p oevd ev evi))
evd false
+(** Revert the resolvability status of evars after resolution,
+ potentially unprotecting some evars that were set unresolvable
+ just for this call to resolution. *)
+
+let revert_resolvability oevd evd =
+ Evd.fold_undefined
+ (fun ev evi evm ->
+ try
+ if not (Typeclasses.is_resolvable evi) then
+ let evi' = Evd.find_undefined oevd ev in
+ if Typeclasses.is_resolvable evi' then
+ Evd.add evm ev (Typeclasses.mark_resolvable evi)
+ else evm
+ else evm
+ with Not_found -> evm)
+ evd evd
+
(** If [do_split] is [true], we try to separate the problem in
several components and then solve them separately *)
@@ -644,7 +661,7 @@ let resolve_all_evars debug m env p oevd do_split fail =
let in_comp comp ev = if do_split then Intset.mem ev comp else true
in
let rec docomp evd = function
- | [] -> evd
+ | [] -> revert_resolvability oevd evd
| comp :: comps ->
let p = select_and_update_evars p oevd (in_comp comp) in
try
@@ -659,24 +676,20 @@ let resolve_all_evars debug m env p oevd do_split fail =
docomp evd comps
in docomp oevd split
-let initial_select_evars onlyargs =
- if onlyargs then
- (fun evd ev evi ->
- Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd))
- && Typeclasses.is_class_evar evd evi)
- else
- (fun evd ev evi -> Typeclasses.is_class_evar evd evi)
+let initial_select_evars filter evd ev evi =
+ filter (snd evi.Evd.evar_source) &&
+ Typeclasses.is_class_evar evd evi
-let resolve_typeclass_evars debug m env evd onlyargs split fail =
+let resolve_typeclass_evars debug m env evd filter split fail =
let evd =
try Evarconv.consider_remaining_unif_problems
~ts:(Typeclasses.classes_transparent_state ()) env evd
with _ -> evd
in
- resolve_all_evars debug m env (initial_select_evars onlyargs) evd split fail
+ resolve_all_evars debug m env (initial_select_evars filter) evd split fail
-let solve_inst debug depth env evd onlyargs split fail =
- resolve_typeclass_evars debug depth env evd onlyargs split fail
+let solve_inst debug depth env evd filter split fail =
+ resolve_typeclass_evars debug depth env evd filter split fail
let _ =
Typeclasses.solve_instanciations_problem :=
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
deleted file mode 100644
index fd924707..00000000
--- a/tactics/dhyp.ml
+++ /dev/null
@@ -1,359 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* Chet's comments about this tactic :
-
- Programmable destruction of hypotheses and conclusions.
-
- The idea here is that we are going to store patterns. These
- patterns look like:
-
- TYP=<pattern>
- SORT=<pattern>
-
- and from these patterns, we will be able to decide which tactic to
- execute.
-
- For hypotheses, we have a vector of 4 patterns:
-
- HYP[TYP] HYP[SORT] CONCL[TYP] CONCL[SORT]
-
- and for conclusions, we have 2:
-
- CONCL[TYP] CONCL[SORT]
-
- If the user doesn't supply some of these, they are just replaced
- with empties.
-
- The process of matching goes like this:
-
- We use a discrimination net to look for matches between the pattern
- for HYP[TOP] (CONCL[TOP]) and the type of the chosen hypothesis.
- Then, we use this to look for the right tactic to apply, by
- matching the rest of the slots. Each match is tried, and if there
- is more than one, this fact is reported, and the one with the
- lowest priority is taken. The priority is a parameter of the
- tactic input.
-
- The tactic input is an expression to hand to the
- tactic-interpreter, and its priority.
-
- For most tactics, the priority should be the number of subgoals
- generated.
-
- Matching is compatible with second-order matching of sopattern.
-
- SYNTAX:
-
- Hint DHyp <hyp-pattern> pri <tac-pattern>.
-
- and
-
- Hint DConcl <concl-pattern> pri <tac-pattern>.
-
- The bindings at the end allow us to transfer information from the
- patterns on terms into the patterns on tactics in a safe way - we
- will perform second-order normalization and conversion to an AST
- before substitution into the tactic-expression.
-
- WARNING: The binding mechanism is NOT intended to facilitate the
- transfer of large amounts of information from the terms to the
- tactic. This should be done in a special-purpose tactic.
-
- *)
-
-(*
-
-Example : The tactic "if there is a hypothesis saying that the
-successor of some number is smaller than zero, then invert such
-hypothesis" is defined in this way:
-
-Require DHyp.
-Hint Destruct Hypothesis less_than_zero (le (S ?) O) 1
- (:tactic:<Inversion $0>).
-
-Then, the tactic is used like this:
-
-Goal (le (S O) O) -> False.
-Intro H.
-DHyp H.
-Qed.
-
-The name "$0" refers to the matching hypothesis --in this case the
-hypothesis H.
-
-Similarly for the conclusion :
-
-Hint Destruct Conclusion equal_zero (? = ?) 1 (:tactic:<Reflexivity>).
-
-Goal (plus O O)=O.
-DConcl.
-Qed.
-
-The "Discardable" option clears the hypothesis after using it.
-
-Require DHyp.
-Hint Destruct Discardable Hypothesis less_than_zero (le (S ?) O) 1
- (:tactic:<Inversion $0>).
-
-Goal (n:nat)(le (S n) O) -> False.
-Intros n H.
-DHyp H.
-Qed.
--- Eduardo (9/3/97 )
-
-*)
-
-open Pp
-open Util
-open Names
-open Term
-open Environ
-open Reduction
-open Proof_type
-open Glob_term
-open Tacmach
-open Refiner
-open Tactics
-open Clenv
-open Tactics
-open Tacticals
-open Libobject
-open Library
-open Pattern
-open Matching
-open Pcoq
-open Tacexpr
-open Termops
-open Libnames
-
-(* two patterns - one for the type, and one for the type of the type *)
-type destructor_pattern = {
- d_typ: constr_pattern;
- d_sort: constr_pattern }
-
-let subst_destructor_pattern subst { d_typ = t; d_sort = s } =
- { d_typ = subst_pattern subst t; d_sort = subst_pattern subst s }
-
-(* hypothesis patterns might need to do matching on the conclusion, too.
- * conclusion-patterns only need to do matching on the hypothesis *)
-type located_destructor_pattern =
- (* discardable, pattern for hyp, pattern for concl *)
- (bool * destructor_pattern * destructor_pattern,
- (* pattern for concl *)
- destructor_pattern) location
-
-let subst_located_destructor_pattern subst = function
- | HypLocation (b,d,d') ->
- HypLocation
- (b,subst_destructor_pattern subst d, subst_destructor_pattern subst d')
- | ConclLocation d ->
- ConclLocation (subst_destructor_pattern subst d)
-
-
-type destructor_data = {
- d_pat : located_destructor_pattern;
- d_pri : int;
- d_code : identifier option * glob_tactic_expr (* should be of phylum tactic *)
-}
-
-module Dest_data = struct
- type t = destructor_data
- let compare = Pervasives.compare
- end
-
-module Nbterm_net = Nbtermdn.Make(Dest_data)
-
-type t = identifier Nbterm_net.t
-type frozen_t = identifier Nbterm_net.frozen_t
-
-let tactab = (Nbterm_net.create () : t)
-
-let lookup pat = Nbterm_net.lookup tactab pat
-
-
-let init () = Nbterm_net.empty tactab
-
-let freeze () = Nbterm_net.freeze tactab
-let unfreeze fs = Nbterm_net.unfreeze fs tactab
-
-let add (na,dd) =
- let pat = match dd.d_pat with
- | HypLocation(_,p,_) -> p.d_typ
- | ConclLocation p -> p.d_typ
- in
- if Nbterm_net.in_dn tactab na then begin
- msgnl (str "Warning [Overriding Destructor Entry " ++
- str (string_of_id na) ++ str"]");
- Nbterm_net.remap tactab na (pat,dd)
- end else
- Nbterm_net.add tactab (na,(pat,dd))
-
-let _ =
- Summary.declare_summary "destruct-hyp-concl"
- { Summary.freeze_function = freeze;
- Summary.unfreeze_function = unfreeze;
- Summary.init_function = init }
-
-let forward_subst_tactic =
- ref (fun _ -> failwith "subst_tactic is not installed for DHyp")
-
-let cache_dd (_,(_,na,dd)) =
- try
- add (na,dd)
- with _ ->
- anomalylabstrm "Dhyp.add"
- (str"The code which adds destructor hints broke;" ++ spc () ++
- str"this is not supposed to happen")
-
-let classify_dd (local,_,_ as o) =
- if local then Dispose else Substitute o
-
-let subst_dd (subst,(local,na,dd)) =
- (local,na,
- { d_pat = subst_located_destructor_pattern subst dd.d_pat;
- d_pri = dd.d_pri;
- d_code = !forward_subst_tactic subst dd.d_code })
-
-let inDD : bool * identifier * destructor_data -> obj =
- declare_object {(default_object "DESTRUCT-HYP-CONCL-DATA") with
- cache_function = cache_dd;
- open_function = (fun i o -> if i=1 then cache_dd o);
- subst_function = subst_dd;
- classify_function = classify_dd }
-
-let catch_all_sort_pattern = PMeta(Some (id_of_string "SORT"))
-let catch_all_type_pattern = PMeta(Some (id_of_string "TYPE"))
-
-let add_destructor_hint local na loc (_,pat) pri code =
- let code =
- begin match loc, code with
- | HypLocation _, TacFun ([id],body) -> (id,body)
- | ConclLocation _, _ -> (None, code)
- | _ ->
- errorlabstrm "add_destructor_hint"
- (str "The tactic should be a function of the hypothesis name.") end
- in
- let pat = match loc with
- | HypLocation b ->
- HypLocation
- (b,{d_typ=pat;d_sort=catch_all_sort_pattern},
- {d_typ=catch_all_type_pattern;d_sort=catch_all_sort_pattern})
- | ConclLocation () ->
- ConclLocation({d_typ=pat;d_sort=catch_all_sort_pattern}) in
- Lib.add_anonymous_leaf
- (inDD (local,na,{ d_pat = pat; d_pri=pri; d_code=code }))
-
-let match_dpat dp cls gls =
- let onconcl = cls.concl_occs <> no_occurrences_expr in
- match (cls,dp) with
- | ({onhyps=lo},HypLocation(_,hypd,concld)) when not onconcl ->
- let hl = match lo with
- Some l -> l
- | None -> List.map (fun id -> ((all_occurrences_expr,id),InHyp))
- (pf_ids_of_hyps gls) in
- if not
- (List.for_all
- (fun ((_,id),hl) ->
- let cltyp = pf_get_hyp_typ gls id in
- let cl = pf_concl gls in
- (hl=InHyp) &
- (is_matching hypd.d_typ cltyp) &
- (is_matching hypd.d_sort (pf_type_of gls cltyp)) &
- (is_matching concld.d_typ cl) &
- (is_matching concld.d_sort (pf_type_of gls cl)))
- hl)
- then error "No match."
- | ({onhyps=Some[]},ConclLocation concld) when onconcl ->
- let cl = pf_concl gls in
- if not
- ((is_matching concld.d_typ cl) &
- (is_matching concld.d_sort (pf_type_of gls cl)))
- then error "No match."
- | _ -> error "ApplyDestructor"
-
-let forward_interp_tactic =
- ref (fun _ -> failwith "interp_tactic is not installed for DHyp")
-
-let set_extern_interp f = forward_interp_tactic := f
-
-let applyDestructor cls discard dd gls =
- match_dpat dd.d_pat cls gls;
- let cll = simple_clause_of cls gls in
- let tacl =
- List.map (fun cl ->
- match cl, dd.d_code with
- | Some id, (Some x, tac) ->
- let arg =
- ConstrMayEval(ConstrTerm (GRef(dummy_loc,VarRef id),None)) in
- TacLetIn (false, [(dummy_loc, x), arg], tac)
- | None, (None, tac) -> tac
- | _, (Some _,_) -> error "Destructor expects an hypothesis."
- | _, (None,_) -> error "Destructor is for conclusion.")
- cll in
- let discard_0 =
- List.map (fun cl ->
- match (cl,dd.d_pat) with
- | (Some id,HypLocation(discardable,_,_)) ->
- if discard & discardable then thin [id] else tclIDTAC
- | (None,ConclLocation _) -> tclIDTAC
- | _ -> error "ApplyDestructor" ) cll in
- tclTHEN (tclMAP !forward_interp_tactic tacl) (tclTHENLIST discard_0) gls
-
-
-(* [DHyp id gls]
-
- will take an identifier, get its type, look it up in the
- discrimination net, get the destructors stored there, and then try
- them in order of priority. *)
-
-let destructHyp discard id gls =
- let hyptyp = pf_get_hyp_typ gls id in
- let ddl = List.map snd (lookup hyptyp) in
- let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in
- tclFIRST (List.map (applyDestructor (onHyp id) discard) sorted_ddl) gls
-
-let dHyp id gls = destructHyp false id gls
-
-let h_destructHyp b id =
- abstract_tactic (TacDestructHyp (b,(dummy_loc,id))) (destructHyp b id)
-
-(* [DConcl gls]
-
- will take a goal, get its concl, look it up in the
- discrimination net, get the destructors stored there, and then try
- them in order of priority. *)
-
-let dConcl gls =
- let ddl = List.map snd (lookup (pf_concl gls)) in
- let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in
- tclFIRST (List.map (applyDestructor onConcl false) sorted_ddl) gls
-
-let h_destructConcl = abstract_tactic TacDestructConcl dConcl
-
-let rec search n =
- if n=0 then error "Search has reached zero.";
- tclFIRST
- [intros;
- assumption;
- (tclTHEN
- (Tacticals.tryAllHypsAndConcl
- (function
- | Some id -> (dHyp id)
- | None -> dConcl ))
- (search (n-1)))]
-
-let auto_tdb n = tclTRY (tclCOMPLETE (search n))
-
-let search_depth_tdb = ref(5)
-
-let depth_tdb = function
- | None -> !search_depth_tdb
- | Some n -> n
-
-let h_auto_tdb n = abstract_tactic (TacAutoTDB n) (auto_tdb (depth_tdb n))
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
deleted file mode 100644
index 1bdeed6a..00000000
--- a/tactics/dhyp.mli
+++ /dev/null
@@ -1,28 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Names
-open Tacmach
-open Tacexpr
-
-(** Programmable destruction of hypotheses and conclusions. *)
-
-val set_extern_interp : (glob_tactic_expr -> tactic) -> unit
-
-(*
-val dHyp : identifier -> tactic
-val dConcl : tactic
-*)
-val h_destructHyp : bool -> identifier -> tactic
-val h_destructConcl : tactic
-val h_auto_tdb : int option -> tactic
-
-val add_destructor_hint :
- Vernacexpr.locality_flag -> identifier -> (bool,unit) Tacexpr.location ->
- Glob_term.patvar list * Pattern.constr_pattern -> int ->
- glob_tactic_expr -> unit
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 9966fb77..a8ce4254 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -27,6 +27,7 @@ open Clenv
open Auto
open Glob_term
open Hiddentac
+open Tacexpr
let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state }
@@ -171,7 +172,14 @@ type search_state = {
tacres : goal list sigma;
last_tactic : std_ppcmds Lazy.t;
dblist : Auto.hint_db list;
- localdb : Auto.hint_db list }
+ localdb : Auto.hint_db list;
+ prev : prev_search_state
+}
+
+and prev_search_state = (* for info eauto *)
+ | Unknown
+ | Init
+ | State of search_state
module SearchProblem = struct
@@ -211,6 +219,7 @@ module SearchProblem = struct
if s.depth = 0 then
[]
else
+ let ps = if s.prev = Unknown then Unknown else State s in
let lg = s.tacres in
let nbgl = List.length (sig_it lg) in
assert (nbgl > 0);
@@ -225,7 +234,8 @@ module SearchProblem = struct
in
List.map (fun (res,pp) -> { depth = s.depth; tacres = res;
last_tactic = pp; dblist = s.dblist;
- localdb = List.tl s.localdb }) l
+ localdb = List.tl s.localdb;
+ prev = ps}) l
in
let intro_tac =
List.map
@@ -237,7 +247,7 @@ module SearchProblem = struct
let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
{ depth = s.depth; tacres = res;
last_tactic = pp; dblist = s.dblist;
- localdb = ldb :: List.tl s.localdb })
+ localdb = ldb :: List.tl s.localdb; prev = ps })
(filter_tactics s.tacres [Tactics.intro,lazy (str "intro")])
in
let rec_tacs =
@@ -248,73 +258,122 @@ module SearchProblem = struct
(fun (lgls as res, pp) ->
let nbgl' = List.length (sig_it lgls) in
if nbgl' < nbgl then
- { depth = s.depth; tacres = res; last_tactic = pp;
+ { depth = s.depth; tacres = res; last_tactic = pp; prev = ps;
dblist = s.dblist; localdb = List.tl s.localdb }
else
{ depth = pred s.depth; tacres = res;
- dblist = s.dblist; last_tactic = pp;
+ dblist = s.dblist; last_tactic = pp; prev = ps;
localdb =
list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
l
in
List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
- let pp s =
- msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++
- (Lazy.force s.last_tactic) ++ str "\n"))
+ let pp s = hov 0 (str " depth=" ++ int s.depth ++ spc () ++
+ (Lazy.force s.last_tactic))
end
module Search = Explore.Make(SearchProblem)
-let make_initial_state n gl dblist localdb =
+(** Utilities for debug eauto / info eauto *)
+
+let global_debug_eauto = ref false
+let global_info_eauto = ref false
+
+let _ =
+ Goptions.declare_bool_option
+ { Goptions.optsync = true;
+ Goptions.optdepr = false;
+ Goptions.optname = "Debug Eauto";
+ Goptions.optkey = ["Debug";"Eauto"];
+ Goptions.optread = (fun () -> !global_debug_eauto);
+ Goptions.optwrite = (:=) global_debug_eauto }
+
+let _ =
+ Goptions.declare_bool_option
+ { Goptions.optsync = true;
+ Goptions.optdepr = false;
+ Goptions.optname = "Info Eauto";
+ Goptions.optkey = ["Info";"Eauto"];
+ Goptions.optread = (fun () -> !global_info_eauto);
+ Goptions.optwrite = (:=) global_info_eauto }
+
+let mk_eauto_dbg d =
+ if d = Debug || !global_debug_eauto then Debug
+ else if d = Info || !global_info_eauto then Info
+ else Off
+
+let pr_info_nop = function
+ | Info -> msg_debug (str "idtac.")
+ | _ -> ()
+
+let pr_dbg_header = function
+ | Off -> ()
+ | Debug -> msg_debug (str "(* debug eauto : *)")
+ | Info -> msg_debug (str "(* info eauto : *)")
+
+let pr_info dbg s =
+ if dbg <> Info then ()
+ else
+ let rec loop s =
+ match s.prev with
+ | Unknown | Init -> s.depth
+ | State sp ->
+ let mindepth = loop sp in
+ let indent = String.make (mindepth - sp.depth) ' ' in
+ msg_debug (str indent ++ Lazy.force s.last_tactic ++ str ".");
+ mindepth
+ in
+ ignore (loop s)
+
+(** Eauto main code *)
+
+let make_initial_state dbg n gl dblist localdb =
{ depth = n;
tacres = tclIDTAC gl;
last_tactic = lazy (mt());
dblist = dblist;
- localdb = [localdb] }
-
-let e_depth_search debug p db_list local_db gl =
- try
- let tac = if debug then Search.debug_depth_first else Search.depth_first in
- let s = tac (make_initial_state p gl db_list local_db) in
- s.tacres
- with Not_found -> error "eauto: depth first search failed."
-
-let e_breadth_search debug n db_list local_db gl =
- try
- let tac =
- if debug then Search.debug_breadth_first else Search.breadth_first
- in
- let s = tac (make_initial_state n gl db_list local_db) in
- s.tacres
- with Not_found -> error "eauto: breadth first search failed."
+ localdb = [localdb];
+ prev = if dbg=Info then Init else Unknown;
+ }
let e_search_auto debug (in_depth,p) lems db_list gl =
let local_db = make_local_hint_db ~ts:full_transparent_state true lems gl in
- if in_depth then
- e_depth_search debug p db_list local_db gl
- else
- e_breadth_search debug p db_list local_db gl
+ let d = mk_eauto_dbg debug in
+ let tac = match in_depth,d with
+ | (true,Debug) -> Search.debug_depth_first
+ | (true,_) -> Search.depth_first
+ | (false,Debug) -> Search.debug_breadth_first
+ | (false,_) -> Search.breadth_first
+ in
+ try
+ pr_dbg_header d;
+ let s = tac (make_initial_state d p gl db_list local_db) in
+ pr_info d s;
+ s.tacres
+ with Not_found ->
+ pr_info_nop d;
+ error "eauto: search failed"
open Evd
-let eauto_with_bases debug np lems db_list =
+let eauto_with_bases ?(debug=Off) np lems db_list =
tclTRY (e_search_auto debug np lems db_list)
-let eauto debug np lems dbnames =
+let eauto ?(debug=Off) np lems dbnames =
let db_list = make_db_list dbnames in
tclTRY (e_search_auto debug np lems db_list)
-let full_eauto debug n lems gl =
+let full_eauto ?(debug=Off) n lems gl =
let dbnames = current_db_names () in
let dbnames = list_remove "v62" dbnames in
let db_list = List.map searchtable_map dbnames in
tclTRY (e_search_auto debug n lems db_list) gl
-let gen_eauto d np lems = function
- | None -> full_eauto d np lems
- | Some l -> eauto d np lems l
+let gen_eauto ?(debug=Off) np lems = function
+ | None -> full_eauto ~debug np lems
+ | Some l -> eauto ~debug np lems l
let make_depth = function
| None -> !default_search_depth
@@ -362,7 +421,7 @@ END
TACTIC EXTEND eauto
| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
- [ gen_eauto false (make_dimension n p) lems db ]
+ [ gen_eauto (make_dimension n p) lems db ]
END
TACTIC EXTEND new_eauto
@@ -370,20 +429,25 @@ TACTIC EXTEND new_eauto
hintbases(db) ] ->
[ match db with
| None -> new_full_auto (make_depth n) lems
- | Some l ->
- new_auto (make_depth n) lems l ]
+ | Some l -> new_auto (make_depth n) lems l ]
END
TACTIC EXTEND debug_eauto
| [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
- [ gen_eauto true (make_dimension n p) lems db ]
+ [ gen_eauto ~debug:Debug (make_dimension n p) lems db ]
+END
+
+TACTIC EXTEND info_eauto
+| [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
+ hintbases(db) ] ->
+ [ gen_eauto ~debug:Info (make_dimension n p) lems db ]
END
TACTIC EXTEND dfs_eauto
| [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
- [ gen_eauto false (true, make_depth p) lems db ]
+ [ gen_eauto (true, make_depth p) lems db ]
END
let cons a l = a :: l
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 68ec42f4..5e656139 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -27,11 +27,11 @@ val registered_e_assumption : tactic
val e_give_exact : ?flags:Unification.unify_flags -> constr -> tactic
-val gen_eauto : bool -> bool * int -> open_constr list ->
+val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> open_constr list ->
hint_db_name list option -> tactic
val eauto_with_bases :
- bool ->
+ ?debug:Tacexpr.debug ->
bool * int ->
open_constr list -> Auto.hint_db list -> Proof_type.tactic
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 6a13ac2a..58f07a1b 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -33,23 +33,9 @@ END
let pr_orient = pr_orient () () ()
-let pr_int_list_full _prc _prlc _prt l =
- let rec aux = function
- | i :: l -> Pp.int i ++ Pp.spc () ++ aux l
- | [] -> Pp.mt()
- in aux l
-ARGUMENT EXTEND int_nelist
- PRINTED BY pr_int_list_full
- RAW_TYPED AS int list
- RAW_PRINTED BY pr_int_list_full
- GLOB_TYPED AS int list
- GLOB_PRINTED BY pr_int_list_full
-| [ integer(x) int_nelist(l) ] -> [x::l]
-| [ integer(x) ] -> [ [x] ]
-END
-
-let pr_int_list = pr_int_list_full () () ()
+let pr_int_list = Util.pr_sequence Pp.int
+let pr_int_list_full _prc _prlc _prt l = pr_int_list l
open Glob_term
@@ -72,6 +58,8 @@ let interp_occs ist gl l =
| ArgVar (_,id as locid) ->
(try int_list_of_VList (List.assoc id ist.lfun)
with Not_found | CannotCoerceTo _ -> [interp_int ist locid])
+let interp_occs ist gl l =
+ Tacmach.project gl , interp_occs ist gl l
let glob_occs ist l = l
@@ -93,7 +81,7 @@ ARGUMENT EXTEND occurrences
GLOB_TYPED AS occurrences_or_var
GLOB_PRINTED BY pr_occurrences
-| [ int_nelist(l) ] -> [ ArgArg l ]
+| [ ne_integer_list(l) ] -> [ ArgArg l ]
| [ var(id) ] -> [ ArgVar id ]
END
@@ -103,7 +91,7 @@ let pr_gen prc _prlc _prtac c = prc c
let pr_globc _prc _prlc _prtac (_,glob) = Printer.pr_glob_constr glob
-let interp_glob ist gl (t,_) = (ist,t)
+let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t)
let glob_glob = Tacinterp.intern_constr
@@ -150,6 +138,9 @@ let interp_place ist gl = function
ConclLocation () -> ConclLocation ()
| HypLocation (id,hl) -> HypLocation (interp_hyp ist gl id,hl)
+let interp_place ist gl p =
+ Tacmach.project gl , interp_place ist gl p
+
let subst_place subst pl = pl
ARGUMENT EXTEND hloc
@@ -287,13 +278,13 @@ let glob_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause (fun x -> x)
(* spiwack argument for the commands of the retroknowledge *)
let (wit_r_nat_field, globwit_r_nat_field, rawwit_r_nat_field) =
- Genarg.create_arg "r_nat_field"
+ Genarg.create_arg None "r_nat_field"
let (wit_r_n_field, globwit_r_n_field, rawwit_r_n_field) =
- Genarg.create_arg "r_n_field"
+ Genarg.create_arg None "r_n_field"
let (wit_r_int31_field, globwit_r_int31_field, rawwit_r_int31_field) =
- Genarg.create_arg "r_int31_field"
+ Genarg.create_arg None "r_int31_field"
let (wit_r_field, globwit_r_field, rawwit_r_field) =
- Genarg.create_arg "r_field"
+ Genarg.create_arg None "r_field"
(* spiwack: the print functions are incomplete, but I don't know what they are
used for *)
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 2abca40e..6f466490 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -15,6 +15,7 @@ open Termops
open Glob_term
val rawwit_orient : bool raw_abstract_argument_type
+val globwit_orient : bool glob_abstract_argument_type
val wit_orient : bool typed_abstract_argument_type
val orient : bool Pcoq.Gram.entry
val pr_orient : bool -> Pp.std_ppcmds
@@ -39,6 +40,7 @@ val hloc : loc_place Pcoq.Gram.entry
val pr_hloc : loc_place -> Pp.std_ppcmds
val in_arg_hyp: (Names.identifier Util.located list option * bool) Pcoq.Gram.entry
+val globwit_in_arg_hyp : (Names.identifier Util.located list option * bool) glob_abstract_argument_type
val rawwit_in_arg_hyp : (Names.identifier Util.located list option * bool) raw_abstract_argument_type
val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type
val raw_in_arg_hyp_to_clause : (Names.identifier Util.located list option * bool) -> Tacticals.clause
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index da35edbe..507a1205 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -23,9 +23,13 @@ open Equality
open Compat
(**********************************************************************)
-(* replace, discriminate, injection, simplify_eq *)
+(* admit, replace, discriminate, injection, simplify_eq *)
(* cutrewrite, dependent rewrite *)
+TACTIC EXTEND admit
+ [ "admit" ] -> [ admit_as_an_axiom ]
+END
+
let replace_in_clause_maybe_by (sigma1,c1) c2 in_hyp tac =
Refiner.tclWITHHOLES false
(replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp))
@@ -761,3 +765,15 @@ TACTIC EXTEND is_hyp
| Var _ -> tclIDTAC
| _ -> tclFAIL 0 (str "Not a variable or hypothesis") ]
END
+
+
+(* Command to grab the evars left unresolved at the end of a proof. *)
+(* spiwack: I put it in extratactics because it is somewhat tied with
+ the semantics of the LCF-style tactics, hence with the classic tactic
+ mode. *)
+VERNAC COMMAND EXTEND GrabEvars
+[ "Grab" "Existential" "Variables" ] ->
+ [ let p = Proof_global.give_me_the_proof () in
+ Proof.V82.grab_evars p;
+ Flags.if_verbose (fun () -> Pp.msg (Printer.pr_open_subgoals ())) () ]
+END
diff --git a/tactics/refine.ml b/tactics/refine.ml
index e7f3998a..653d005c 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -388,7 +388,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
let refine (evd,c) gl =
let sigma = project gl in
- let evd = Typeclasses.resolve_typeclasses ~onlyargs:true (pf_env gl) evd in
+ let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals (pf_env gl) evd in
let c = Evarutil.nf_evar evd c in
let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in
(* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index d297969d..120a76ae 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -257,7 +257,7 @@ let decompose_applied_relation env sigma flags orig (c,l) left2right =
let ctype = Typing.type_of env sigma c' in
let find_rel ty =
let eqclause = Clenv.make_clenv_binding_env_apply env sigma None (c',ty) l in
- let (equiv, args) = decompose_app_rel env sigma (Clenv.clenv_type eqclause) in
+ let (equiv, args) = decompose_app_rel env eqclause.evd (Clenv.clenv_type eqclause) in
let c1 = args.(0) and c2 = args.(1) in
let ty1, ty2 =
Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2
@@ -1343,7 +1343,7 @@ type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bi
let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = Printer.pr_glob_constr (fst (fst (snd ge)))
let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = Printer.pr_glob_constr (fst (fst ge))
let pr_constr_expr_with_bindings prc _ _ (ge : constr_expr_with_bindings) = prc (fst ge)
-let interp_glob_constr_with_bindings ist gl c = (ist, c)
+let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c)
let glob_glob_constr_with_bindings ist l = Tacinterp.intern_constr_with_bindings ist l
let subst_glob_constr_with_bindings s c = subst_glob_with_bindings s c
@@ -1365,7 +1365,7 @@ ARGUMENT EXTEND glob_constr_with_bindings
END
let _ =
- (Genarg.create_arg "strategy" :
+ (Genarg.create_arg None "strategy" :
((strategy, Genarg.tlevel) Genarg.abstract_argument_type *
(strategy, Genarg.glevel) Genarg.abstract_argument_type *
(strategy, Genarg.rlevel) Genarg.abstract_argument_type))
@@ -1374,7 +1374,7 @@ let _ =
let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
-let interp_strategy ist gl c = c
+let interp_strategy ist gl c = project gl , c
let glob_strategy ist l = l
let subst_strategy evm l = l
@@ -1405,10 +1405,11 @@ ARGUMENT EXTEND rewstrategy TYPED AS strategy
| [ "choice" rewstrategy(h) rewstrategy(h') ] -> [ Strategies.choice h h' ]
| [ "old_hints" preident(h) ] -> [ Strategies.old_hints h ]
| [ "hints" preident(h) ] -> [ Strategies.hints h ]
- | [ "terms" constr_list(h) ] -> [ fun env avoid t ty cstr evars ->
+ | [ "terms" constr_list(h) ] -> [ fun env avoid t ty cstr evars ->
Strategies.lemmas rewrite_unif_flags (interp_constr_list env (goalevars evars) h) env avoid t ty cstr evars ]
- | [ "eval" red_expr(r) ] -> [ fun env avoid t ty cstr evars ->
- Strategies.reduce (Tacinterp.interp_redexp env (goalevars evars) r) env avoid t ty cstr evars ]
+ | [ "eval" red_expr(r) ] -> [ fun env avoid t ty cstr evars ->
+ let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in
+ Strategies.reduce r_interp env avoid t ty cstr (sigma,cstrevars evars) ]
| [ "fold" constr(c) ] -> [ Strategies.fold c ]
END
@@ -1425,6 +1426,8 @@ let clsubstitute o c =
| Some id when is_tac id -> tclIDTAC
| _ -> cl_rewrite_clause c o all_occurrences cl)
+open Extraargs
+
TACTIC EXTEND substitute
| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ]
END
@@ -1536,7 +1539,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
type 'a binders_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
let _, _, rawwit_binders =
- (Genarg.create_arg "binders" :
+ (Genarg.create_arg None "binders" :
Genarg.tlevel binders_argtype *
Genarg.glevel binders_argtype *
Genarg.rlevel binders_argtype)
@@ -1867,7 +1870,8 @@ let setoid_proof gl ty fn fallback =
let env = pf_env gl in
try
let rel, args = decompose_app_rel env (project gl) (pf_concl gl) in
- let evm, car = project gl, pf_type_of gl args.(0) in
+ let evm = project gl in
+ let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
fn env evm car rel gl
with e ->
try fallback gl
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a41cd6e7..3efff8fa 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -175,8 +175,8 @@ let _ =
"intros", TacIntroPattern [];
"assumption", TacAssumption;
"cofix", TacCofix None;
- "trivial", TacTrivial ([],None);
- "auto", TacAuto(None,[],None);
+ "trivial", TacTrivial (Off,[],None);
+ "auto", TacAuto(Off,None,[],None);
"left", TacLeft(false,NoBindings);
"eleft", TacLeft(true,NoBindings);
"right", TacRight(false,NoBindings);
@@ -254,7 +254,7 @@ type glob_sign = {
type interp_genarg_type =
(glob_sign -> raw_generic_argument -> glob_generic_argument) *
(interp_sign -> goal sigma -> glob_generic_argument ->
- typed_generic_argument) *
+ Evd.evar_map * typed_generic_argument) *
(substitution -> glob_generic_argument -> glob_generic_argument)
let extragenargtab =
@@ -713,17 +713,10 @@ let rec intern_atomic lf ist x =
(clause_app (intern_hyp_location ist) cls),b)
(* Automation tactics *)
- | TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l)
- | TacAuto (n,lems,l) ->
- TacAuto (Option.map (intern_or_var ist) n,
+ | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (intern_constr ist) lems,l)
+ | TacAuto (d,n,lems,l) ->
+ TacAuto (d,Option.map (intern_or_var ist) n,
List.map (intern_constr ist) lems,l)
- | TacAutoTDB n -> TacAutoTDB n
- | TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id)
- | TacDestructConcl -> TacDestructConcl
- | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
- | TacDAuto (n,p,lems) ->
- TacDAuto (Option.map (intern_or_var ist) n,p,
- List.map (intern_constr ist) lems)
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) ->
@@ -1256,7 +1249,8 @@ let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma
in
let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in
let evdc =
- catch_error trace (understand_ltac expand_evar sigma env vars kind) c in
+ catch_error trace
+ (understand_ltac ~resolve_classes:use_classes expand_evar sigma env vars kind) c in
let (evd,c) =
if expand_evar then
solve_remaining_evars fail_evar use_classes
@@ -1268,7 +1262,7 @@ let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma
(* Interprets a constr; expects evars to be solved *)
let interp_constr_gen kind ist env sigma c =
- snd (interp_gen kind ist false true true true env sigma c)
+ interp_gen kind ist false true true true env sigma c
let interp_constr = interp_constr_gen (OfType None)
@@ -1278,8 +1272,8 @@ let interp_type = interp_constr_gen IsType
let interp_open_constr_gen kind ist =
interp_gen kind ist false true false false
-let interp_open_constr ccl =
- interp_open_constr_gen (OfType ccl)
+let interp_open_constr ccl ist =
+ interp_gen (OfType ccl) ist false true false (ccl<>None)
let interp_pure_open_constr ist =
interp_gen (OfType None) ist false false false false
@@ -1317,7 +1311,7 @@ let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
sigma, List.flatten l
let interp_constr_list ist env sigma c =
- snd (interp_constr_in_compound_list (fun x -> x) (fun x -> x) (fun ist env sigma c -> (Evd.empty, interp_constr ist env sigma c)) ist env sigma c)
+ interp_constr_in_compound_list (fun x -> x) (fun x -> x) interp_constr ist env sigma c
let interp_open_constr_list =
interp_constr_in_compound_list (fun x -> x) (fun x -> x)
@@ -1339,7 +1333,8 @@ let interp_flag ist env red =
{ red with rConst = List.map (interp_evaluable ist env) red.rConst }
let interp_constr_with_occurrences ist sigma env (occs,c) =
- (interp_occurrences ist occs, interp_constr ist sigma env c)
+ let (sigma,c_interp) = interp_constr ist sigma env c in
+ sigma , (interp_occurrences ist occs, c_interp)
let interp_typed_pattern_with_occurrences ist env sigma (occs,c) =
let sign,p = interp_typed_pattern ist env sigma c in
@@ -1354,36 +1349,48 @@ let interp_constr_with_occurrences_and_name_as_list =
(function ((occs,c),Anonymous) when occs = all_occurrences_expr -> c
| _ -> raise Not_found)
(fun ist env sigma (occ_c,na) ->
- sigma, (interp_constr_with_occurrences ist env sigma occ_c,
+ let (sigma,c_interp) = interp_constr_with_occurrences ist env sigma occ_c in
+ sigma, (c_interp,
interp_fresh_name ist env na))
let interp_red_expr ist sigma env = function
- | Unfold l -> Unfold (List.map (interp_unfold ist env) l)
- | Fold l -> Fold (List.map (interp_constr ist env sigma) l)
- | Cbv f -> Cbv (interp_flag ist env f)
- | Lazy f -> Lazy (interp_flag ist env f)
+ | Unfold l -> sigma , Unfold (List.map (interp_unfold ist env) l)
+ | Fold l ->
+ let (sigma,l_interp) = interp_constr_list ist env sigma l in
+ sigma , Fold l_interp
+ | Cbv f -> sigma , Cbv (interp_flag ist env f)
+ | Lazy f -> sigma , Lazy (interp_flag ist env f)
| Pattern l ->
- Pattern (List.map (interp_constr_with_occurrences ist env sigma) l)
+ let (sigma,l_interp) =
+ List.fold_right begin fun c (sigma,acc) ->
+ let (sigma,c_interp) = interp_constr_with_occurrences ist env sigma c in
+ sigma , c_interp :: acc
+ end l (sigma,[])
+ in
+ sigma , Pattern l_interp
| Simpl o ->
- Simpl(Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
- | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r
+ sigma , Simpl(Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
+ | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> sigma , r
let pf_interp_red_expr ist gl = interp_red_expr ist (project gl) (pf_env gl)
let interp_may_eval f ist gl = function
| ConstrEval (r,c) ->
- let redexp = pf_interp_red_expr ist gl r in
- pf_reduction_of_red_expr gl redexp (f ist gl c)
+ let (sigma,redexp) = pf_interp_red_expr ist gl r in
+ let (sigma,c_interp) = f ist { gl with sigma=sigma } c in
+ sigma , pf_reduction_of_red_expr gl redexp c_interp
| ConstrContext ((loc,s),c) ->
(try
- let ic = f ist gl c
+ let (sigma,ic) = f ist gl c
and ctxt = constr_of_VConstr_context (List.assoc s ist.lfun) in
- subst_meta [special_meta,ic] ctxt
+ sigma , subst_meta [special_meta,ic] ctxt
with
| Not_found ->
user_err_loc (loc, "interp_may_eval",
str "Unbound context identifier" ++ pr_id s ++ str"."))
- | ConstrTypeOf c -> pf_type_of gl (f ist gl c)
+ | ConstrTypeOf c ->
+ let (sigma,c_interp) = f ist gl c in
+ sigma , pf_type_of gl c_interp
| ConstrTerm c ->
try
f ist gl c
@@ -1394,7 +1401,7 @@ let interp_may_eval f ist gl = function
(* Interprets a constr expression possibly to first evaluate *)
let interp_constr_may_eval ist gl c =
- let csr =
+ let (sigma,csr) =
try
interp_may_eval pf_interp_constr ist gl c
with e ->
@@ -1403,7 +1410,7 @@ let interp_constr_may_eval ist gl c =
in
begin
db_constr ist.debug (pf_env gl) csr;
- csr
+ sigma , csr
end
let rec message_of_value gl = function
@@ -1565,7 +1572,7 @@ let interp_induction_arg ist gl arg =
ElimOnIdent (loc,id)
else
let c = (GVar (loc,id),Some (CRef (Ident (loc,id)))) in
- let c = interp_constr ist env sigma c in
+ let (sigma,c) = interp_constr ist env sigma c in
ElimOnConstr (sigma,(c,NoBindings))
(* Associates variables with values and gives the remaining variables and
@@ -1725,7 +1732,12 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps =
(* misc *)
-let mk_constr_value ist gl c = VConstr ([],pf_interp_constr ist gl c)
+let mk_constr_value ist gl c =
+ let (sigma,c_interp) = pf_interp_constr ist gl c in
+ sigma,VConstr ([],c_interp)
+let mk_open_constr_value ist gl c =
+ let (sigma,c_interp) = pf_apply (interp_open_constr None ist) gl c in
+ sigma,VConstr ([],c_interp)
let mk_hyp_value ist gl c = VConstr ([],mkVar (interp_hyp ist gl c))
let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c)
@@ -1739,17 +1751,16 @@ let extend_gl_hyps { it=gl ; sigma=sigma } sign =
(* Interprets an l-tac expression into a value *)
let rec val_interp ist gl (tac:glob_tactic_expr) =
-
let value_interp ist = match tac with
(* Immediate evaluation *)
- | TacFun (it,body) -> VFun (ist.trace,ist.lfun,it,body)
+ | TacFun (it,body) -> project gl , VFun (ist.trace,ist.lfun,it,body)
| TacLetIn (true,l,u) -> interp_letrec ist gl l u
| TacLetIn (false,l,u) -> interp_letin ist gl l u
| TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist gl lz lr lmr
| TacMatch (lz,c,lmr) -> interp_match ist gl lz c lmr
| TacArg (loc,a) -> interp_tacarg ist gl a
(* Delayed evaluation *)
- | t -> VFun (ist.trace,ist.lfun,[],t)
+ | t -> project gl , VFun (ist.trace,ist.lfun,[],t)
in check_for_interrupt ();
match ist.debug with
@@ -1769,7 +1780,9 @@ and eval_tactic ist = function
catch_error (push_trace(loc,call)ist.trace) tac gl
| TacFun _ | TacLetIn _ -> assert false
| TacMatchGoal _ | TacMatch _ -> assert false
- | TacId s -> fun gl -> tclIDTAC_MESSAGE (interp_message_nl ist gl s) gl
+ | TacId s -> fun gl ->
+ let res = tclIDTAC_MESSAGE (interp_message_nl ist gl s) gl in
+ db_breakpoint ist.debug s; res
| TacFail (n,s) -> fun gl -> tclFAIL (interp_int_or_var ist n) (interp_message ist gl s) gl
| TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
| TacAbstract (tac,ido) ->
@@ -1782,14 +1795,6 @@ and eval_tactic ist = function
| TacDo (n,tac) -> tclDO (interp_int_or_var ist n) (interp_tactic ist tac)
| TacTimeout (n,tac) -> tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac)
| TacTry tac -> tclTRY (interp_tactic ist tac)
- | TacInfo tac ->
- let t = (interp_tactic ist tac) in
- tclINFO
- begin
- match tac with
- TacAtom (_,_) -> t
- | _ -> abstract_tactic_expr (TacArg (dloc,Tacexp tac)) t
- end
| TacRepeat tac -> tclREPEAT (interp_tactic ist tac)
| TacOrelse (tac1,tac2) ->
tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2)
@@ -1797,17 +1802,23 @@ and eval_tactic ist = function
| TacSolve l -> tclSOLVE (List.map (interp_tactic ist) l)
| TacComplete tac -> tclCOMPLETE (interp_tactic ist tac)
| TacArg a -> interp_tactic ist (TacArg a)
+ | TacInfo tac ->
+ msg_warning
+ (str "The general \"info\" tactic is currently not working.\n" ++
+ str "Some specific verbose tactics may exist instead, such as\n" ++
+ str "info_trivial, info_auto, info_eauto.");
+ eval_tactic ist tac
and force_vrec ist gl = function
| VRec (lfun,body) -> val_interp {ist with lfun = !lfun} gl body
- | v -> v
+ | v -> project gl , v
and interp_ltac_reference loc' mustbetac ist gl = function
| ArgVar (loc,id) ->
let v = List.assoc id ist.lfun in
- let v = force_vrec ist gl v in
+ let (sigma,v) = force_vrec ist gl v in
let v = propagate_trace ist loc id v in
- if mustbetac then coerce_to_tactic loc id v else v
+ sigma , if mustbetac then coerce_to_tactic loc id v else v
| ArgArg (loc,r) ->
let ids = extract_ids [] ist.lfun in
let loc_info = ((if loc' = dloc then loc else loc'),LtacNameCall r) in
@@ -1816,36 +1827,69 @@ and interp_ltac_reference loc' mustbetac ist gl = function
trace = push_trace loc_info ist.trace } in
val_interp ist gl (lookup r)
-and interp_tacarg ist gl = function
- | TacVoid -> VVoid
- | Reference r -> interp_ltac_reference dloc false ist gl r
- | Integer n -> VInteger n
- | IntroPattern ipat -> VIntroPattern (snd (interp_intro_pattern ist gl ipat))
- | ConstrMayEval c -> VConstr ([],interp_constr_may_eval ist gl c)
- | MetaIdArg (loc,_,id) -> assert false
- | TacCall (loc,r,[]) -> interp_ltac_reference loc true ist gl r
- | TacCall (loc,f,l) ->
- let fv = interp_ltac_reference loc true ist gl f
- and largs = List.map (interp_tacarg ist gl) l in
- List.iter check_is_value largs;
- interp_app loc ist gl fv largs
- | TacExternal (loc,com,req,la) ->
- interp_external loc ist gl com req (List.map (interp_tacarg ist gl) la)
- | TacFreshId l ->
- let id = pf_interp_fresh_id ist gl l in
- VIntroPattern (IntroIdentifier id)
- | Tacexp t -> val_interp ist gl t
- | TacDynamic(_,t) ->
- let tg = (Dyn.tag t) in
- if tg = "tactic" then
- val_interp ist gl (tactic_out t ist)
- else if tg = "value" then
- value_out t
- else if tg = "constr" then
+and interp_tacarg ist gl arg =
+ let evdref = ref (project gl) in
+ let v = match arg with
+ | TacVoid -> VVoid
+ | Reference r ->
+ let (sigma,v) = interp_ltac_reference dloc false ist gl r in
+ evdref := sigma;
+ v
+ | Integer n -> VInteger n
+ | IntroPattern ipat -> VIntroPattern (snd (interp_intro_pattern ist gl ipat))
+ | ConstrMayEval c ->
+ let (sigma,c_interp) = interp_constr_may_eval ist gl c in
+ evdref := sigma;
+ VConstr ([],c_interp)
+ | MetaIdArg (loc,_,id) -> assert false
+ | TacCall (loc,r,[]) ->
+ let (sigma,v) = interp_ltac_reference loc true ist gl r in
+ evdref := sigma;
+ v
+ | TacCall (loc,f,l) ->
+ let (sigma,fv) = interp_ltac_reference loc true ist gl f in
+ let (sigma,largs) =
+ List.fold_right begin fun a (sigma',acc) ->
+ let (sigma', a_interp) = interp_tacarg ist gl a in
+ sigma' , a_interp::acc
+ end l (sigma,[])
+ in
+ List.iter check_is_value largs;
+ let (sigma,v) = interp_app loc ist { gl with sigma=sigma } fv largs in
+ evdref:= sigma;
+ v
+ | TacExternal (loc,com,req,la) ->
+ let (sigma,la_interp) =
+ List.fold_right begin fun a (sigma,acc) ->
+ let (sigma,a_interp) = interp_tacarg ist {gl with sigma=sigma} a in
+ sigma , a_interp::acc
+ end la (project gl,[])
+ in
+ let (sigma,v) = interp_external loc ist { gl with sigma=sigma } com req la_interp in
+ evdref := sigma;
+ v
+ | TacFreshId l ->
+ let id = pf_interp_fresh_id ist gl l in
+ VIntroPattern (IntroIdentifier id)
+ | Tacexp t ->
+ let (sigma,v) = val_interp ist gl t in
+ evdref := sigma;
+ v
+ | TacDynamic(_,t) ->
+ let tg = (Dyn.tag t) in
+ if tg = "tactic" then
+ let (sigma,v) = val_interp ist gl (tactic_out t ist) in
+ evdref := sigma;
+ v
+ else if tg = "value" then
+ value_out t
+ else if tg = "constr" then
VConstr ([],constr_out t)
- else
- anomaly_loc (dloc, "Tacinterp.val_interp",
- (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">"))
+ else
+ anomaly_loc (dloc, "Tacinterp.val_interp",
+ (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">"))
+ in
+ !evdref , v
(* Interprets an application node *)
and interp_app loc ist gl fv largs =
@@ -1859,19 +1903,20 @@ and interp_app loc ist gl fv largs =
(TacFun _|TacLetIn _|TacMatchGoal _|TacMatch _| TacArg _ as body))) ->
let (newlfun,lvar,lval)=head_with_value (var,largs) in
if lvar=[] then
- let v =
+ let (sigma,v) =
try
catch_error trace
(val_interp {ist with lfun=newlfun@olfun; trace=trace} gl) body
with e ->
debugging_exception_step ist false e (fun () -> str "evaluation");
raise e in
+ let gl = { gl with sigma=sigma } in
debugging_step ist
(fun () ->
str"evaluation returns"++fnl()++pr_value (Some (pf_env gl)) v);
- if lval=[] then v else interp_app loc ist gl v lval
+ if lval=[] then sigma,v else interp_app loc ist gl v lval
else
- VFun(trace,newlfun@olfun,lvar,body)
+ project gl , VFun(trace,newlfun@olfun,lvar,body)
| _ ->
user_err_loc (loc, "Tacinterp.interp_app",
(str"Illegal tactic application."))
@@ -1894,10 +1939,12 @@ and tactic_of_value ist vle g =
(* Evaluation with FailError catching *)
and eval_with_fail ist is_lazy goal tac =
try
- (match val_interp ist goal tac with
+ let (sigma,v) = val_interp ist goal tac in
+ sigma ,
+ (match v with
| VFun (trace,lfun,[],t) when not is_lazy ->
let tac = eval_tactic {ist with lfun=lfun; trace=trace} t in
- VRTactic (catch_error trace tac goal)
+ VRTactic (catch_error trace tac { goal with sigma=sigma })
| a -> a)
with
| FailError (0,s) | Loc.Exc_located(_, FailError (0,s))
@@ -1919,10 +1966,15 @@ and interp_letrec ist gl llc u =
(* Interprets the clauses of a LetIn *)
and interp_letin ist gl llc u =
- let lve = list_map_left (fun ((_,id),body) ->
- let v = interp_tacarg ist gl body in check_is_value v; (id,v)) llc in
+ let (sigma,lve) =
+ List.fold_right begin fun ((_,id),body) (sigma,acc) ->
+ let (sigma,v) = interp_tacarg ist { gl with sigma=sigma } body in
+ check_is_value v;
+ sigma, (id,v)::acc
+ end llc (project gl,[])
+ in
let ist = { ist with lfun = lve@ist.lfun } in
- val_interp ist gl u
+ val_interp ist { gl with sigma=sigma } u
(* Interprets the Match Context expressions *)
and interp_match_goal ist goal lz lr lmr =
@@ -2015,80 +2067,103 @@ and interp_external loc ist gl com req la =
(* Interprets extended tactic generic arguments *)
and interp_genarg ist gl x =
- match genarg_tag x with
- | BoolArgType -> in_gen wit_bool (out_gen globwit_bool x)
- | IntArgType -> in_gen wit_int (out_gen globwit_int x)
- | IntOrVarArgType ->
+ let evdref = ref (project gl) in
+ let rec interp_genarg ist gl x =
+ let gl = { gl with sigma = !evdref } in
+ match genarg_tag x with
+ | BoolArgType -> in_gen wit_bool (out_gen globwit_bool x)
+ | IntArgType -> in_gen wit_int (out_gen globwit_int x)
+ | IntOrVarArgType ->
in_gen wit_int_or_var
(ArgArg (interp_int_or_var ist (out_gen globwit_int_or_var x)))
- | StringArgType ->
+ | StringArgType ->
in_gen wit_string (out_gen globwit_string x)
- | PreIdentArgType ->
+ | PreIdentArgType ->
in_gen wit_pre_ident (out_gen globwit_pre_ident x)
- | IntroPatternArgType ->
+ | IntroPatternArgType ->
in_gen wit_intro_pattern
(interp_intro_pattern ist gl (out_gen globwit_intro_pattern x))
- | IdentArgType b ->
+ | IdentArgType b ->
in_gen (wit_ident_gen b)
(pf_interp_fresh_ident ist gl (out_gen (globwit_ident_gen b) x))
- | VarArgType ->
+ | VarArgType ->
in_gen wit_var (interp_hyp ist gl (out_gen globwit_var x))
- | RefArgType ->
+ | RefArgType ->
in_gen wit_ref (pf_interp_reference ist gl (out_gen globwit_ref x))
- | SortArgType ->
+ | SortArgType ->
+ let (sigma,c_interp) =
+ pf_interp_constr ist gl
+ (GSort (dloc,out_gen globwit_sort x), None)
+ in
+ evdref := sigma;
in_gen wit_sort
- (destSort
- (pf_interp_constr ist gl
- (GSort (dloc,out_gen globwit_sort x), None)))
- | ConstrArgType ->
- in_gen wit_constr (pf_interp_constr ist gl (out_gen globwit_constr x))
- | ConstrMayEvalArgType ->
- in_gen wit_constr_may_eval (interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x))
- | QuantHypArgType ->
+ (destSort c_interp)
+ | ConstrArgType ->
+ let (sigma,c_interp) = pf_interp_constr ist gl (out_gen globwit_constr x) in
+ evdref := sigma;
+ in_gen wit_constr c_interp
+ | ConstrMayEvalArgType ->
+ let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x) in
+ evdref := sigma;
+ in_gen wit_constr_may_eval c_interp
+ | QuantHypArgType ->
in_gen wit_quant_hyp
(interp_declared_or_quantified_hypothesis ist gl
- (out_gen globwit_quant_hyp x))
- | RedExprArgType ->
- in_gen wit_red_expr (pf_interp_red_expr ist gl (out_gen globwit_red_expr x))
- | OpenConstrArgType casted ->
+ (out_gen globwit_quant_hyp x))
+ | RedExprArgType ->
+ let (sigma,r_interp) = pf_interp_red_expr ist gl (out_gen globwit_red_expr x) in
+ evdref := sigma;
+ in_gen wit_red_expr r_interp
+ | OpenConstrArgType casted ->
in_gen (wit_open_constr_gen casted)
(interp_open_constr (if casted then Some (pf_concl gl) else None)
- ist (pf_env gl) (project gl)
- (snd (out_gen (globwit_open_constr_gen casted) x)))
- | ConstrWithBindingsArgType ->
+ ist (pf_env gl) (project gl)
+ (snd (out_gen (globwit_open_constr_gen casted) x)))
+ | ConstrWithBindingsArgType ->
in_gen wit_constr_with_bindings
(pack_sigma (interp_constr_with_bindings ist (pf_env gl) (project gl)
- (out_gen globwit_constr_with_bindings x)))
- | BindingsArgType ->
+ (out_gen globwit_constr_with_bindings x)))
+ | BindingsArgType ->
in_gen wit_bindings
(pack_sigma (interp_bindings ist (pf_env gl) (project gl) (out_gen globwit_bindings x)))
- | List0ArgType ConstrArgType -> interp_genarg_constr_list0 ist gl x
- | List1ArgType ConstrArgType -> interp_genarg_constr_list1 ist gl x
- | List0ArgType VarArgType -> interp_genarg_var_list0 ist gl x
- | List1ArgType VarArgType -> interp_genarg_var_list1 ist gl x
- | List0ArgType _ -> app_list0 (interp_genarg ist gl) x
- | List1ArgType _ -> app_list1 (interp_genarg ist gl) x
- | OptArgType _ -> app_opt (interp_genarg ist gl) x
- | PairArgType _ -> app_pair (interp_genarg ist gl) (interp_genarg ist gl) x
- | ExtraArgType s ->
+ | List0ArgType ConstrArgType ->
+ let (sigma,v) = interp_genarg_constr_list0 ist gl x in
+ evdref := sigma;
+ v
+ | List1ArgType ConstrArgType ->
+ let (sigma,v) = interp_genarg_constr_list1 ist gl x in
+ evdref := sigma;
+ v
+ | List0ArgType VarArgType -> interp_genarg_var_list0 ist gl x
+ | List1ArgType VarArgType -> interp_genarg_var_list1 ist gl x
+ | List0ArgType _ -> app_list0 (interp_genarg ist gl) x
+ | List1ArgType _ -> app_list1 (interp_genarg ist gl) x
+ | OptArgType _ -> app_opt (interp_genarg ist gl) x
+ | PairArgType _ -> app_pair (interp_genarg ist gl) (interp_genarg ist gl) x
+ | ExtraArgType s ->
match tactic_genarg_level s with
| Some n ->
(* Special treatment of tactic arguments *)
- in_gen (wit_tactic n)
- (TacArg(dloc,valueIn(VFun(ist.trace,ist.lfun,[],
- out_gen (globwit_tactic n) x))))
+ in_gen (wit_tactic n)
+ (TacArg(dloc,valueIn(VFun(ist.trace,ist.lfun,[],
+ out_gen (globwit_tactic n) x))))
| None ->
- lookup_interp_genarg s ist gl x
+ let (sigma,v) = lookup_interp_genarg s ist gl x in
+ evdref:=sigma;
+ v
+ in
+ let v = interp_genarg ist gl x in
+ !evdref , v
and interp_genarg_constr_list0 ist gl x =
let lc = out_gen (wit_list0 globwit_constr) x in
- let lc = pf_apply (interp_constr_list ist) gl lc in
- in_gen (wit_list0 wit_constr) lc
+ let (sigma,lc) = pf_apply (interp_constr_list ist) gl lc in
+ sigma , in_gen (wit_list0 wit_constr) lc
and interp_genarg_constr_list1 ist gl x =
let lc = out_gen (wit_list1 globwit_constr) x in
- let lc = pf_apply (interp_constr_list ist) gl lc in
- in_gen (wit_list1 wit_constr) lc
+ let (sigma,lc) = pf_apply (interp_constr_list ist) gl lc in
+ sigma , in_gen (wit_list1 wit_constr) lc
and interp_genarg_var_list0 ist gl x =
let lc = out_gen (wit_list0 globwit_var) x in
@@ -2111,10 +2186,10 @@ and interp_match ist g lz constr lmr =
with e when is_match_catchable e ->
match_next_pattern find_next' () in
match_next_pattern (fun () -> match_subterm_gen app c csr) () in
- let rec apply_match ist csr = function
+ let rec apply_match ist sigma csr = let g = { g with sigma=sigma } in function
| (All t)::tl ->
(try eval_with_fail ist lz g t
- with e when is_match_catchable e -> apply_match ist csr tl)
+ with e when is_match_catchable e -> apply_match ist sigma csr tl)
| (Pat ([],Term c,mt))::tl ->
(try
let lmatch =
@@ -2134,31 +2209,31 @@ and interp_match ist g lz constr lmr =
raise e
with e when is_match_catchable e ->
debugging_step ist (fun () -> str "switching to the next rule");
- apply_match ist csr tl)
+ apply_match ist sigma csr tl)
| (Pat ([],Subterm (b,id,c),mt))::tl ->
(try apply_match_subterm b ist (id,c) csr mt
- with PatternMatchingFailure -> apply_match ist csr tl)
+ with PatternMatchingFailure -> apply_match ist sigma csr tl)
| _ ->
errorlabstrm "Tacinterp.apply_match" (str
"No matching clauses for match.") in
- let csr =
+ let (sigma,csr) =
try interp_ltac_constr ist g constr with e ->
debugging_exception_step ist true e
(fun () -> str "evaluation of the matched expression");
raise e in
- let ilr = read_match_rule (fst (extract_ltac_constr_values ist (pf_env g))) ist (pf_env g) (project g) lmr in
+ let ilr = read_match_rule (fst (extract_ltac_constr_values ist (pf_env g))) ist (pf_env g) sigma lmr in
let res =
- try apply_match ist csr ilr with e ->
+ try apply_match ist sigma csr ilr with e ->
debugging_exception_step ist true e (fun () -> str "match expression");
raise e in
debugging_step ist (fun () ->
- str "match expression returns " ++ pr_value (Some (pf_env g)) res);
+ str "match expression returns " ++ pr_value (Some (pf_env g)) (snd res));
res
(* Interprets tactic expressions : returns a "constr" *)
and interp_ltac_constr ist gl e =
- let result =
+ let (sigma, result) =
try val_interp ist gl e with Not_found ->
debugging_step ist (fun () ->
str "evaluation failed for" ++ fnl() ++
@@ -2171,7 +2246,7 @@ and interp_ltac_constr ist gl e =
str " has value " ++ fnl() ++
pr_constr_under_binders_env (pf_env gl) cresult);
if fst cresult <> [] then raise Not_found;
- snd cresult
+ sigma , snd cresult
with Not_found ->
errorlabstrm ""
(str "Must evaluate to a closed term" ++ fnl() ++
@@ -2204,7 +2279,8 @@ and interp_ltac_constr ist gl e =
(* Interprets tactic expressions : returns a "tactic" *)
and interp_tactic ist tac gl =
- tactic_of_value ist (val_interp ist gl tac) gl
+ let (sigma,v) = val_interp ist gl tac in
+ tactic_of_value ist v { gl with sigma=sigma }
(* Interprets a primitive tactic *)
and interp_atomic ist gl tac =
@@ -2219,9 +2295,21 @@ and interp_atomic ist gl tac =
h_intro_move (Option.map (interp_fresh_ident ist env) ido)
(interp_move_location ist gl hto)
| TacAssumption -> h_assumption
- | TacExact c -> h_exact (pf_interp_casted_constr ist gl c)
- | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c)
- | TacVmCastNoCheck c -> h_vm_cast_no_check (pf_interp_constr ist gl c)
+ | TacExact c ->
+ let (sigma,c_interp) = pf_interp_casted_constr ist gl c in
+ tclTHEN
+ (tclEVARS sigma)
+ (h_exact c_interp)
+ | TacExactNoCheck c ->
+ let (sigma,c_interp) = pf_interp_constr ist gl c in
+ tclTHEN
+ (tclEVARS sigma)
+ (h_exact_no_check c_interp)
+ | TacVmCastNoCheck c ->
+ let (sigma,c_interp) = pf_interp_constr ist gl c in
+ tclTHEN
+ (tclEVARS sigma)
+ (h_vm_cast_no_check c_interp)
| TacApply (a,ev,cb,cl) ->
let sigma, l =
list_fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
@@ -2235,56 +2323,89 @@ and interp_atomic ist gl tac =
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
tclWITHHOLES ev (h_elim ev cb) sigma cbo
- | TacElimType c -> h_elim_type (pf_interp_type ist gl c)
+ | TacElimType c ->
+ let (sigma,c_interp) = pf_interp_type ist gl c in
+ tclTHEN
+ (tclEVARS sigma)
+ (h_elim_type c_interp)
| TacCase (ev,cb) ->
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
tclWITHHOLES ev (h_case ev) sigma cb
- | TacCaseType c -> h_case_type (pf_interp_type ist gl c)
+ | TacCaseType c ->
+ let (sigma,c_interp) = pf_interp_type ist gl c in
+ tclTHEN
+ (tclEVARS sigma)
+ (h_case_type c_interp)
| TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist env) idopt) n
| TacMutualFix (b,id,n,l) ->
- let f (id,n,c) = (interp_fresh_ident ist env id,n,pf_interp_type ist gl c)
- in h_mutual_fix b (interp_fresh_ident ist env id) n (List.map f l)
+ let f sigma (id,n,c) =
+ let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
+ sigma , (interp_fresh_ident ist env id,n,c_interp) in
+ let (sigma,l_interp) =
+ List.fold_right begin fun c (sigma,acc) ->
+ let (sigma,c_interp) = f sigma c in
+ sigma , c_interp::acc
+ end l (project gl,[])
+ in
+ tclTHEN
+ (tclEVARS sigma)
+ (h_mutual_fix b (interp_fresh_ident ist env id) n l_interp)
| TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist env) idopt)
| TacMutualCofix (b,id,l) ->
- let f (id,c) = (interp_fresh_ident ist env id,pf_interp_type ist gl c) in
- h_mutual_cofix b (interp_fresh_ident ist env id) (List.map f l)
- | TacCut c -> h_cut (pf_interp_type ist gl c)
+ let f sigma (id,c) =
+ let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
+ sigma , (interp_fresh_ident ist env id,c_interp) in
+ let (sigma,l_interp) =
+ List.fold_right begin fun c (sigma,acc) ->
+ let (sigma,c_interp) = f sigma c in
+ sigma , c_interp::acc
+ end l (project gl,[])
+ in
+ tclTHEN
+ (tclEVARS sigma)
+ (h_mutual_cofix b (interp_fresh_ident ist env id) l_interp)
+ | TacCut c ->
+ let (sigma,c_interp) = pf_interp_type ist gl c in
+ tclTHEN
+ (tclEVARS sigma)
+ (h_cut c_interp)
| TacAssert (t,ipat,c) ->
- let c = (if t=None then interp_constr else interp_type) ist env sigma c in
- abstract_tactic (TacAssert (t,ipat,c))
- (Tactics.forward (Option.map (interp_tactic ist) t)
- (Option.map (interp_intro_pattern ist gl) ipat) c)
+ let (sigma,c) = (if t=None then interp_constr else interp_type) ist env sigma c in
+ tclTHEN
+ (tclEVARS sigma)
+ (abstract_tactic (TacAssert (t,ipat,c))
+ (Tactics.forward (Option.map (interp_tactic ist) t)
+ (Option.map (interp_intro_pattern ist gl) ipat) c))
| TacGeneralize cl ->
let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
tclWITHHOLES false (h_generalize_gen) sigma cl
- | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
+ | TacGeneralizeDep c ->
+ let (sigma,c_interp) = pf_interp_constr ist gl c in
+ tclTHEN
+ (tclEVARS sigma)
+ (h_generalize_dep c_interp)
| TacLetTac (na,c,clp,b) ->
let clp = interp_clause ist gl clp in
if clp = nowhere then
(* We try to fully-typechect the term *)
- h_let_tac b (interp_fresh_name ist env na)
- (pf_interp_constr ist gl c) clp
+ let (sigma,c_interp) = pf_interp_constr ist gl c in
+ tclTHEN
+ (tclEVARS sigma)
+ (h_let_tac b (interp_fresh_name ist env na) c_interp clp)
else
(* We try to keep the pattern structure as much as possible *)
h_let_pat_tac b (interp_fresh_name ist env na)
(interp_pure_open_constr ist env sigma c) clp
(* Automation tactics *)
- | TacTrivial (lems,l) ->
- Auto.h_trivial
+ | TacTrivial (debug,lems,l) ->
+ Auto.h_trivial ~debug
(interp_auto_lemmas ist env sigma lems)
(Option.map (List.map (interp_hint_base ist)) l)
- | TacAuto (n,lems,l) ->
- Auto.h_auto (Option.map (interp_int_or_var ist) n)
+ | TacAuto (debug,n,lems,l) ->
+ Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n)
(interp_auto_lemmas ist env sigma lems)
(Option.map (List.map (interp_hint_base ist)) l)
- | TacAutoTDB n -> Dhyp.h_auto_tdb n
- | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id)
- | TacDestructConcl -> Dhyp.h_destructConcl
- | TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2
- | TacDAuto (n,p,lems) ->
- Auto.h_dauto (Option.map (interp_int_or_var ist) n,p)
- (interp_auto_lemmas ist env sigma lems)
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) ->
@@ -2304,15 +2425,30 @@ and interp_atomic ist gl tac =
let h1 = interp_quantified_hypothesis ist h1 in
let h2 = interp_quantified_hypothesis ist h2 in
Elim.h_double_induction h1 h2
- | TacDecomposeAnd c -> Elim.h_decompose_and (pf_interp_constr ist gl c)
- | TacDecomposeOr c -> Elim.h_decompose_or (pf_interp_constr ist gl c)
+ | TacDecomposeAnd c ->
+ let (sigma,c_interp) = pf_interp_constr ist gl c in
+ tclTHEN
+ (tclEVARS sigma)
+ (Elim.h_decompose_and c_interp)
+ | TacDecomposeOr c ->
+ let (sigma,c_interp) = pf_interp_constr ist gl c in
+ tclTHEN
+ (tclEVARS sigma)
+ (Elim.h_decompose_or c_interp)
| TacDecompose (l,c) ->
let l = List.map (interp_inductive ist) l in
- Elim.h_decompose l (pf_interp_constr ist gl c)
+ let (sigma,c_interp) = pf_interp_constr ist gl c in
+ tclTHEN
+ (tclEVARS sigma)
+ (Elim.h_decompose l c_interp)
| TacSpecialize (n,cb) ->
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
tclWITHHOLES false (h_specialize n) sigma cb
- | TacLApply c -> h_lapply (pf_interp_constr ist gl c)
+ | TacLApply c ->
+ let (sigma,c_interp) = pf_interp_constr ist gl c in
+ tclTHEN
+ (tclEVARS sigma)
+ (h_lapply c_interp)
(* Context management *)
| TacClear (b,l) -> h_clear b (interp_hyp_list ist gl l)
@@ -2344,27 +2480,48 @@ and interp_atomic ist gl tac =
(* Conversion *)
| TacReduce (r,cl) ->
- h_reduce (pf_interp_red_expr ist gl r) (interp_clause ist gl cl)
+ let (sigma,r_interp) = pf_interp_red_expr ist gl r in
+ tclTHEN
+ (tclEVARS sigma)
+ (h_reduce r_interp (interp_clause ist gl cl))
| TacChange (None,c,cl) ->
- h_change None
- (if (cl.onhyps = None or cl.onhyps = Some []) &
+ let (sigma,c_interp) =
+ if (cl.onhyps = None or cl.onhyps = Some []) &
(cl.concl_occs = all_occurrences_expr or
cl.concl_occs = no_occurrences_expr)
then pf_interp_type ist gl c
- else pf_interp_constr ist gl c)
- (interp_clause ist gl cl)
+ else pf_interp_constr ist gl c
+ in
+ tclTHEN
+ (tclEVARS sigma)
+ (h_change None c_interp (interp_clause ist gl cl))
| TacChange (Some op,c,cl) ->
let sign,op = interp_typed_pattern ist env sigma op in
- h_change (Some op)
- (try pf_interp_constr ist (extend_gl_hyps gl sign) c
- with Not_found | Anomaly _ (* Hack *) ->
- errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side."))
- (interp_clause ist gl cl)
+ (* spiwack: (2012/04/18) the evar_map output by pf_interp_constr
+ is dropped as the evar_map taken as input (from
+ extend_gl_hyps) is incorrect. This means that evar
+ instantiated by pf_interp_constr may be lost, there. *)
+ let (_,c_interp) =
+ try pf_interp_constr ist (extend_gl_hyps gl sign) c
+ with Not_found | Anomaly _ (* Hack *) ->
+ errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
+ in
+ tclTHEN
+ (tclEVARS sigma)
+ (h_change (Some op) c_interp (interp_clause ist { gl with sigma=sigma } cl))
(* Equivalence relations *)
| TacReflexivity -> h_reflexivity
| TacSymmetry c -> h_symmetry (interp_clause ist gl c)
- | TacTransitivity c -> h_transitivity (Option.map (pf_interp_constr ist gl) c)
+ | TacTransitivity c ->
+ begin match c with
+ | None -> h_transitivity None
+ | Some c ->
+ let (sigma,c_interp) = pf_interp_constr ist gl c in
+ tclTHEN
+ (tclEVARS sigma)
+ (h_transitivity (Some c_interp))
+ end
(* Equality and inversion *)
| TacRewrite (ev,l,cl,by) ->
@@ -2375,7 +2532,14 @@ and interp_atomic ist gl tac =
Equality.general_multi_multi_rewrite ev l cl
(Option.map (fun by -> tclCOMPLETE (interp_tactic ist by), Equality.Naive) by)
| TacInversion (DepInversion (k,c,ids),hyp) ->
- Inv.dinv k (Option.map (pf_interp_constr ist gl) c)
+ let (sigma,c_interp) =
+ match c with
+ | None -> sigma , None
+ | Some c ->
+ let (sigma,c_interp) = pf_interp_constr ist gl c in
+ sigma , Some c_interp
+ in
+ Inv.dinv k c_interp
(Option.map (interp_intro_pattern ist gl) ids)
(interp_declared_or_quantified_hypothesis ist gl hyp)
| TacInversion (NonDepInversion (k,idl,ids),hyp) ->
@@ -2384,16 +2548,23 @@ and interp_atomic ist gl tac =
(interp_hyp_list ist gl idl)
(interp_declared_or_quantified_hypothesis ist gl hyp)
| TacInversion (InversionUsing (c,idl),hyp) ->
+ let (sigma,c_interp) = pf_interp_constr ist gl c in
Leminv.lemInv_clause (interp_declared_or_quantified_hypothesis ist gl hyp)
- (pf_interp_constr ist gl c)
+ c_interp
(interp_hyp_list ist gl idl)
(* For extensions *)
| TacExtend (loc,opn,l) ->
let tac = lookup_tactic opn in
- let args = List.map (interp_genarg ist gl) l in
+ let (sigma,args) =
+ List.fold_right begin fun a (sigma,acc) ->
+ let (sigma,a_interp) = interp_genarg ist { gl with sigma=sigma } a in
+ sigma , a_interp::acc
+ end l (project gl,[])
+ in
abstract_extended_tactic opn args (tac args)
| TacAlias (loc,s,l,(_,body)) -> fun gl ->
+ let evdref = ref gl.sigma in
let rec f x = match genarg_tag x with
| IntArgType ->
VInteger (out_gen globwit_int x)
@@ -2415,17 +2586,34 @@ and interp_atomic ist gl tac =
| SortArgType ->
VConstr ([],mkSort (interp_sort (out_gen globwit_sort x)))
| ConstrArgType ->
- mk_constr_value ist gl (out_gen globwit_constr x)
+ let (sigma,v) = mk_constr_value ist gl (out_gen globwit_constr x) in
+ evdref := sigma;
+ v
+ | OpenConstrArgType false ->
+ let (sigma,v) = mk_open_constr_value ist gl (snd (out_gen globwit_open_constr x)) in
+ evdref := sigma;
+ v
| ConstrMayEvalArgType ->
- VConstr
- ([],interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x))
+ let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x) in
+ evdref := sigma;
+ VConstr ([],c_interp)
| ExtraArgType s when tactic_genarg_level s <> None ->
(* Special treatment of tactic arguments *)
- val_interp ist gl
+ let (sigma,v) = val_interp ist gl
(out_gen (globwit_tactic (Option.get (tactic_genarg_level s))) x)
+ in
+ evdref := sigma;
+ v
| List0ArgType ConstrArgType ->
let wit = wit_list0 globwit_constr in
- VList (List.map (mk_constr_value ist gl) (out_gen wit x))
+ let (sigma,l_interp) =
+ List.fold_right begin fun c (sigma,acc) ->
+ let (sigma,c_interp) = mk_constr_value ist { gl with sigma=sigma } c in
+ sigma , c_interp::acc
+ end (out_gen wit x) (project gl,[])
+ in
+ evdref := sigma;
+ VList (l_interp)
| List0ArgType VarArgType ->
let wit = wit_list0 globwit_var in
VList (List.map (mk_hyp_value ist gl) (out_gen wit x))
@@ -2445,7 +2633,14 @@ and interp_atomic ist gl tac =
VList (List.map mk_ipat (out_gen wit x))
| List1ArgType ConstrArgType ->
let wit = wit_list1 globwit_constr in
- VList (List.map (mk_constr_value ist gl) (out_gen wit x))
+ let (sigma, l_interp) =
+ List.fold_right begin fun c (sigma,acc) ->
+ let (sigma,c_interp) = mk_constr_value ist { gl with sigma=sigma } c in
+ sigma , c_interp::acc
+ end (out_gen wit x) (project gl,[])
+ in
+ evdref:=sigma;
+ VList l_interp
| List1ArgType VarArgType ->
let wit = wit_list1 globwit_var in
VList (List.map (mk_hyp_value ist gl) (out_gen wit x))
@@ -2469,17 +2664,22 @@ and interp_atomic ist gl tac =
| ExtraArgType _ | BindingsArgType
| OptArgType _ | PairArgType _
| List0ArgType _ | List1ArgType _
- -> error "This generic type is not supported in alias."
+ -> error "This argument type is not supported in tactic notations."
in
let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in
let trace = push_trace (loc,LtacNotationCall s) ist.trace in
+ let gl = { gl with sigma = !evdref } in
interp_tactic { ist with lfun=lfun; trace=trace } body gl
let make_empty_glob_sign () =
{ ltacvars = ([],[]); ltacrecvars = [];
gsigma = Evd.empty; genv = Global.env() }
+let fully_empty_glob_sign =
+ { ltacvars = ([],[]); ltacrecvars = [];
+ gsigma = Evd.empty; genv = Environ.empty_env }
+
(* Initial call for interpretation *)
let interp_tac_gen lfun avoid_ids debug t gl =
interp_tactic { lfun=lfun; avoid_ids=avoid_ids; debug=debug; trace=[] }
@@ -2488,6 +2688,7 @@ let interp_tac_gen lfun avoid_ids debug t gl =
gsigma = project gl; genv = pf_env gl } t) gl
let eval_tactic t gls =
+ db_initialize ();
interp_tactic { lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] }
t gls
@@ -2641,13 +2842,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacLetTac (id,c,clp,b) -> TacLetTac (id,subst_glob_constr subst c,clp,b)
(* Automation tactics *)
- | TacTrivial (lems,l) -> TacTrivial (List.map (subst_glob_constr subst) lems,l)
- | TacAuto (n,lems,l) -> TacAuto (n,List.map (subst_glob_constr subst) lems,l)
- | TacAutoTDB n -> TacAutoTDB n
- | TacDestructHyp (b,id) -> TacDestructHyp(b,id)
- | TacDestructConcl -> TacDestructConcl
- | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
- | TacDAuto (n,p,lems) -> TacDAuto (n,p,List.map (subst_glob_constr subst) lems)
+ | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (subst_glob_constr subst) lems,l)
+ | TacAuto (d,n,lems,l) -> TacAuto (d,n,List.map (subst_glob_constr subst) lems,l)
(* Derived basic tactics *)
| TacSimpleInductionDestruct (isrec,h) as x -> x
@@ -2991,4 +3187,3 @@ let _ = Auto.set_extern_intern_tac
Flags.with_option strict_check
(intern_pure_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])}))
let _ = Auto.set_extern_subst_tactic subst_tactic
-let _ = Dhyp.set_extern_interp eval_tactic
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index d9dc8094..b9fd64f6 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -77,16 +77,18 @@ type glob_sign = {
gsigma : Evd.evar_map;
genv : Environ.env }
+val fully_empty_glob_sign : glob_sign
+
val add_interp_genarg :
string ->
(glob_sign -> raw_generic_argument -> glob_generic_argument) *
(interp_sign -> goal sigma -> glob_generic_argument ->
- typed_generic_argument) *
+ Evd.evar_map * typed_generic_argument) *
(substitution -> glob_generic_argument -> glob_generic_argument)
-> unit
val interp_genarg :
- interp_sign -> goal sigma -> glob_generic_argument -> typed_generic_argument
+ interp_sign -> goal sigma -> glob_generic_argument -> Evd.evar_map * typed_generic_argument
val intern_genarg :
glob_sign -> raw_generic_argument -> glob_generic_argument
@@ -114,14 +116,14 @@ val subst_glob_with_bindings :
substitution -> glob_constr_and_expr Glob_term.with_bindings -> glob_constr_and_expr Glob_term.with_bindings
(** Interprets any expression *)
-val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value
+val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> Evd.evar_map * value
(** Interprets an expression that evaluates to a constr *)
val interp_ltac_constr : interp_sign -> goal sigma -> glob_tactic_expr ->
- constr
+ Evd.evar_map * constr
(** Interprets redexp arguments *)
-val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> red_expr
+val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr
(** Interprets tactic expressions *)
val interp_tac_gen : (identifier * value) list -> identifier list ->
@@ -143,7 +145,7 @@ val eval_tactic : glob_tactic_expr -> tactic
val interp : raw_tactic_expr -> tactic
-val eval_ltac_constr : goal sigma -> raw_tactic_expr -> constr
+val eval_ltac_constr : goal sigma -> raw_tactic_expr -> Evd.evar_map * constr
val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 11625cbd..b82f1fca 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -53,7 +53,6 @@ let tclREPEAT_MAIN = Refiner.tclREPEAT_MAIN
let tclFIRST = Refiner.tclFIRST
let tclSOLVE = Refiner.tclSOLVE
let tclTRY = Refiner.tclTRY
-let tclINFO = Refiner.tclINFO
let tclCOMPLETE = Refiner.tclCOMPLETE
let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
let tclFAIL = Refiner.tclFAIL
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index db9ab0c9..c70c13f7 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -45,7 +45,6 @@ val tclREPEAT_MAIN : tactic -> tactic
val tclFIRST : tactic list -> tactic
val tclSOLVE : tactic list -> tactic
val tclTRY : tactic -> tactic
-val tclINFO : tactic -> tactic
val tclCOMPLETE : tactic -> tactic
val tclAT_LEAST_ONCE : tactic -> tactic
val tclFAIL : int -> std_ppcmds -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 988d9f53..9a2682fd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -546,7 +546,7 @@ let depth_of_quantified_hypothesis red h gl =
str".")
let intros_until_gen red h g =
- tclDO (depth_of_quantified_hypothesis red h g) intro g
+ tclDO (depth_of_quantified_hypothesis red h g) (if red then introf else intro) g
let intros_until_id id = intros_until_gen true (NamedHyp id)
let intros_until_n_gen red n = intros_until_gen red (AnonHyp n)
@@ -2498,11 +2498,17 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id gl =
tclMAP (fun id ->
tclTRY (generalize_dep ~with_let:true (mkVar id))) vars] gl) gl
+let rec compare_upto_variables x y =
+ if (isVar x || isRel x) && (isVar y || isRel y) then true
+ else compare_constr compare_upto_variables x y
+
let specialize_eqs id gl =
let env = pf_env gl in
let ty = pf_get_hyp_typ gl id in
let evars = ref (project gl) in
- let unif env evars c1 c2 = Evarconv.e_conv env evars c2 c1 in
+ let unif env evars c1 c2 =
+ compare_upto_variables c1 c2 && Evarconv.e_conv env evars c1 c2
+ in
let rec aux in_eqs ctx acc ty =
match kind_of_term ty with
| Prod (na, t, b) ->
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 333d6a3a..f1324809 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -10,7 +10,6 @@ Elimschemes
Tactics
Hiddentac
Elim
-Dhyp
Auto
Equality
Contradiction
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-11 14:25:03 +0000