From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- tactics/auto.ml | 417 ++++++++++++++++---------------- tactics/auto.mli | 54 ++--- tactics/class_tactics.ml4 | 37 ++- tactics/dhyp.ml | 359 --------------------------- tactics/dhyp.mli | 28 --- tactics/eauto.ml4 | 146 +++++++---- tactics/eauto.mli | 4 +- tactics/extraargs.ml4 | 35 +-- tactics/extraargs.mli | 2 + tactics/extratactics.ml4 | 18 +- tactics/refine.ml | 2 +- tactics/rewrite.ml4 | 22 +- tactics/tacinterp.ml | 605 ++++++++++++++++++++++++++++++---------------- tactics/tacinterp.mli | 14 +- tactics/tacticals.ml | 1 - tactics/tacticals.mli | 1 - tactics/tactics.ml | 10 +- tactics/tactics.mllib | 1 - 18 files changed, 821 insertions(+), 935 deletions(-) delete mode 100644 tactics/dhyp.ml delete mode 100644 tactics/dhyp.mli (limited to 'tactics') 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 *) -(* - SORT= - - 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 pri . - - and - - Hint DConcl pri . - - 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:). - -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:). - -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:). - -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 *) -(* 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 "" -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 -- cgit v1.2.3