aboutsummaryrefslogtreecommitdiff
path: root/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'ltac')
-rw-r--r--ltac/coretactics.ml45
-rw-r--r--ltac/extraargs.ml414
-rw-r--r--ltac/extraargs.mli5
-rw-r--r--ltac/extratactics.ml440
-rw-r--r--ltac/g_auto.ml436
-rw-r--r--ltac/g_class.ml418
-rw-r--r--ltac/g_rewrite.ml413
-rw-r--r--ltac/profile_ltac.ml4
-rw-r--r--ltac/rewrite.ml42
-rw-r--r--ltac/rewrite.mli3
-rw-r--r--ltac/tacinterp.ml13
-rw-r--r--ltac/tactic_debug.ml5
12 files changed, 162 insertions, 36 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index de4d589eee..6186667584 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -151,7 +151,10 @@ END
TACTIC EXTEND symmetry
[ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ]
-| [ "symmetry" clause_dft_concl(cl) ] -> [ Tactics.intros_symmetry cl ]
+END
+
+TACTIC EXTEND symmetry_in
+| [ "symmetry" "in" in_clause(cl) ] -> [ Tactics.intros_symmetry cl ]
END
(** Split *)
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index c6d72e03e2..0db1cd7bae 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -260,6 +260,20 @@ END
let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c
+let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Ppconstr.pr_lident cl
+let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl
+let in_clause' = Pcoq.Tactic.in_clause
+
+ARGUMENT EXTEND in_clause
+ TYPED AS clause_dft_concl
+ PRINTED BY pr_in_top_clause
+ RAW_TYPED AS clause_dft_concl
+ RAW_PRINTED BY pr_in_clause
+ GLOB_TYPED AS clause_dft_concl
+ GLOB_PRINTED BY pr_in_clause
+| [ in_clause'(cl) ] -> [ cl ]
+END
+
(* spiwack: the print functions are incomplete, but I don't know what they are
used for *)
let pr_r_nat_field natf =
diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli
index 0cf77935c2..b12187e18a 100644
--- a/ltac/extraargs.mli
+++ b/ltac/extraargs.mli
@@ -71,3 +71,8 @@ val pr_by_arg_tac :
val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type
+
+val wit_in_clause :
+ (Id.t Loc.located Locus.clause_expr,
+ Id.t Loc.located Locus.clause_expr,
+ Id.t Locus.clause_expr) Genarg.genarg_type
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index e50b0520bc..d88bcd7eb1 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -38,7 +38,7 @@ DECLARE PLUGIN "extratactics"
let with_delayed_uconstr ist c tac =
let flags = {
Pretyping.use_typeclasses = false;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = Some Pfedit.solve_by_implicit_tactic;
fail_evar = false;
expand_evars = true
@@ -263,7 +263,10 @@ let add_rewrite_hint bases ort t lcsr =
let ctx =
let ctx = UState.context_set ctx in
if poly then ctx
- else (Global.push_context_set false ctx; Univ.ContextSet.empty)
+ else (** This is a global universe context that shouldn't be
+ refreshed at every use of the hint, declare it globally. *)
+ (Declare.declare_universe_context false ctx;
+ Univ.ContextSet.empty)
in
Constrexpr_ops.constr_loc ce, (c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t in
let eqs = List.map f lcsr in
@@ -313,7 +316,8 @@ let project_hint pri l2r r =
in
let ctx = Evd.universe_context_set sigma in
let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
- (pri,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
+ let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in
+ (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
let add_hints_iff l2r lc n bl =
Hints.add_hints true bl
@@ -339,20 +343,21 @@ END
let constr_flags = {
Pretyping.use_typeclasses = true;
- Pretyping.use_unif_heuristics = true;
+ Pretyping.solve_unification_constraints = true;
Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic;
Pretyping.fail_evar = false;
Pretyping.expand_evars = true }
-let refine_tac ist simple c =
+let refine_tac ist simple with_classes c =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
- let flags = constr_flags in
+ let flags =
+ { constr_flags with Pretyping.use_typeclasses = with_classes } in
let expected_type = Pretyping.OfType concl in
let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
let update = { run = fun sigma -> c.delayed env sigma } in
- let refine = Refine.refine ~unsafe:false update in
+ let refine = Refine.refine ~unsafe:true update in
if simple then refine
else refine <*>
Tactics.New.reduce_after_refine <*>
@@ -360,11 +365,28 @@ let refine_tac ist simple c =
end }
TACTIC EXTEND refine
-| [ "refine" uconstr(c) ] -> [ refine_tac ist false c ]
+| [ "refine" uconstr(c) ] ->
+ [ refine_tac ist false true c ]
END
TACTIC EXTEND simple_refine
-| [ "simple" "refine" uconstr(c) ] -> [ refine_tac ist true c ]
+| [ "simple" "refine" uconstr(c) ] ->
+ [ refine_tac ist true true c ]
+END
+
+TACTIC EXTEND notcs_refine
+| [ "notypeclasses" "refine" uconstr(c) ] ->
+ [ refine_tac ist false false c ]
+END
+
+TACTIC EXTEND notcs_simple_refine
+| [ "simple" "notypeclasses" "refine" uconstr(c) ] ->
+ [ refine_tac ist true false c ]
+END
+
+(* Solve unification constraints using heuristics or fail if any remain *)
+TACTIC EXTEND solve_constraints
+[ "solve_constraints" ] -> [ Refine.solve_constraints ]
END
(**********************************************************************)
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index 8bc2ffd654..6a8fa8d698 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -43,18 +43,24 @@ END
let eval_uconstrs ist cs =
let flags = {
Pretyping.use_typeclasses = false;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = Some Pfedit.solve_by_implicit_tactic;
fail_evar = false;
expand_evars = true
} in
List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs
-let pr_auto_using _ _ _ = Pptactic.pr_auto_using (fun _ -> mt ())
+let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr
+let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c)
+let pr_auto_using _ _ _ = Pptactic.pr_auto_using Printer.pr_closed_glob
ARGUMENT EXTEND auto_using
TYPED AS uconstr_list
PRINTED BY pr_auto_using
+ RAW_TYPED AS uconstr_list
+ RAW_PRINTED BY pr_auto_using_raw
+ GLOB_TYPED AS uconstr_list
+ GLOB_PRINTED BY pr_auto_using_glob
| [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ]
| [ ] -> [ [] ]
END
@@ -171,18 +177,32 @@ TACTIC EXTEND convert_concl_no_check
| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x Term.DEFAULTcast ]
END
-let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom
+let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference
+let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global
+let glob_hints_path_atom ist = Hints.glob_hints_path_atom
ARGUMENT EXTEND hints_path_atom
PRINTED BY pr_hints_path_atom
-| [ ne_global_list(g) ] -> [ Hints.PathHints (List.map Nametab.global g) ]
+
+ GLOBALIZED BY glob_hints_path_atom
+
+ RAW_PRINTED BY pr_pre_hints_path_atom
+ GLOB_PRINTED BY pr_hints_path_atom
+| [ ne_global_list(g) ] -> [ Hints.PathHints g ]
| [ "_" ] -> [ Hints.PathAny ]
END
let pr_hints_path prc prx pry c = Hints.pp_hints_path c
-
+let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c
+let glob_hints_path ist = Hints.glob_hints_path
+
ARGUMENT EXTEND hints_path
- PRINTED BY pr_hints_path
+PRINTED BY pr_hints_path
+
+GLOBALIZED BY glob_hints_path
+RAW_PRINTED BY pr_pre_hints_path
+GLOB_PRINTED BY pr_hints_path
+
| [ "(" hints_path(p) ")" ] -> [ p ]
| [ hints_path(p) "*" ] -> [ Hints.PathStar p ]
| [ "emp" ] -> [ Hints.PathEmpty ]
@@ -192,8 +212,6 @@ ARGUMENT EXTEND hints_path
| [ hints_path(p) hints_path(q) ] -> [ Hints.PathSeq (p, q) ]
END
-let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
-
ARGUMENT EXTEND opthints
TYPED AS preident_list_opt
PRINTED BY pr_hintbases
@@ -203,7 +221,7 @@ END
VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [
- let entry = Hints.HintsCutEntry p in
+ let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
(match dbnames with None -> ["core"] | Some l -> l) entry ]
END
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index 18df596eb8..7e26b5d189 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -44,19 +44,33 @@ ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug
| [ ] -> [ false ]
END
+let pr_search_strategy _prc _prlc _prt = function
+ | Some Dfs -> Pp.str "dfs"
+ | Some Bfs -> Pp.str "bfs"
+ | None -> Pp.mt ()
+
+ARGUMENT EXTEND eauto_search_strategy PRINTED BY pr_search_strategy
+| [ "(bfs)" ] -> [ Some Bfs ]
+| [ "(dfs)" ] -> [ Some Dfs ]
+| [ ] -> [ None ]
+END
+
(* true = All transparent, false = Opaque if possible *)
VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) int_opt(depth) ] -> [
+ | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> [
set_typeclasses_debug d;
+ Option.iter set_typeclasses_strategy s;
set_typeclasses_depth depth
]
END
(** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
TACTIC EXTEND typeclasses_eauto
+ | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
+ [ typeclasses_eauto ~strategy:Bfs ~depth:d l ]
| [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
- [ typeclasses_eauto d l ]
+ [ typeclasses_eauto ~depth:d l ]
| [ "typeclasses" "eauto" int_or_var_opt(d) ] -> [
typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] ]
END
diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index 82b79c883d..28078efd64 100644
--- a/ltac/g_rewrite.ml4
+++ b/ltac/g_rewrite.ml4
@@ -63,8 +63,17 @@ let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c
let subst_strategy s str = str
let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
-let pr_raw_strategy _ _ _ (s : raw_strategy) = Pp.str "<strategy>"
-let pr_glob_strategy _ _ _ (s : glob_strategy) = Pp.str "<strategy>"
+let pr_raw_strategy prc prlc _ (s : raw_strategy) =
+ let prr = Pptactic.pr_red_expr (prc, prlc, Pptactic.pr_or_by_notation Libnames.pr_reference, prc) in
+ Rewrite.pr_strategy prc prr s
+let pr_glob_strategy prc prlc _ (s : glob_strategy) =
+ let prr = Pptactic.pr_red_expr
+ (Ppconstr.pr_constr_expr,
+ Ppconstr.pr_lconstr_expr,
+ Pptactic.pr_or_by_notation Libnames.pr_reference,
+ Ppconstr.pr_constr_expr)
+ in
+ Rewrite.pr_strategy prc prr s
ARGUMENT EXTEND rewstrategy
PRINTED BY pr_strategy
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index a91ff98fb9..2514ededb0 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -128,7 +128,7 @@ let to_ltacprof_results xml =
| _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML")
let feedback_results results =
- Feedback.(feedback
+ Feedback.(feedback
(Custom (Loc.dummy_loc, "ltacprof_results", of_ltacprof_results results)))
(* ************** pretty printing ************************************* *)
@@ -218,7 +218,7 @@ let to_string ~filter ?(cutoff=0.0) node =
!global
in
warn_encountered_multi_success_backtracking ();
- let filter s n = filter s && n >= cutoff in
+ let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in
let msg =
h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
fnl () ++
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 69f45e1aeb..44efdd383f 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1700,6 +1700,40 @@ let rec map_strategy (f : 'a -> 'a2) (g : 'b -> 'b2) : ('a,'b) strategy_ast -> (
| StratEval r -> StratEval (g r)
| StratFold c -> StratFold (f c)
+let pr_ustrategy = function
+| Subterms -> str "subterms"
+| Subterm -> str "subterm"
+| Innermost -> str "innermost"
+| Outermost -> str "outermost"
+| Bottomup -> str "bottomup"
+| Topdown -> str "topdown"
+| Progress -> str "progress"
+| Try -> str "try"
+| Any -> str "any"
+| Repeat -> str "repeat"
+
+let paren p = str "(" ++ p ++ str ")"
+
+let rec pr_strategy prc prr = function
+| StratId -> str "id"
+| StratFail -> str "fail"
+| StratRefl -> str "refl"
+| StratUnary (s, str) ->
+ pr_ustrategy s ++ spc () ++ paren (pr_strategy prc prr str)
+| StratBinary (Choice, str1, str2) ->
+ str "choice" ++ spc () ++ paren (pr_strategy prc prr str1) ++ spc () ++
+ paren (pr_strategy prc prr str2)
+| StratBinary (Compose, str1, str2) ->
+ pr_strategy prc prr str1 ++ str ";" ++ spc () ++ pr_strategy prc prr str2
+| StratConstr (c, true) -> prc c
+| StratConstr (c, false) -> str "<-" ++ spc () ++ prc c
+| StratTerms cl -> str "terms" ++ spc () ++ pr_sequence prc cl
+| StratHints (old, id) ->
+ let cmd = if old then "old_hints" else "hints" in
+ str cmd ++ spc () ++ str id
+| StratEval r -> str "eval" ++ spc () ++ prr r
+| StratFold c -> str "fold" ++ spc () ++ prc c
+
let rec strategy_of_ast = function
| StratId -> Strategies.id
| StratFail -> Strategies.fail
@@ -1754,7 +1788,7 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
let anew_instance global binders instance fields =
new_instance (Flags.is_universe_polymorphism ())
binders instance (Some (true, CRecord (Loc.ghost,fields)))
- ~global ~generalize:false ~refine:false None
+ ~global ~generalize:false ~refine:false Hints.empty_hint_info
let declare_instance_refl global binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
@@ -1935,7 +1969,7 @@ let add_morphism_infer glob m n =
Decl_kinds.IsAssumption Decl_kinds.Logical)
in
add_instance (Typeclasses.new_instance
- (Lazy.force PropGlobal.proper_class) None glob
+ (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob
poly (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
else
@@ -1946,7 +1980,7 @@ let add_morphism_infer glob m n =
let hook _ = function
| Globnames.ConstRef cst ->
add_instance (Typeclasses.new_instance
- (Lazy.force PropGlobal.proper_class) None
+ (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
glob poly (ConstRef cst));
declare_projection n instance_id (ConstRef cst)
| _ -> assert false
@@ -1970,7 +2004,7 @@ let add_morphism glob binders m s n =
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
ignore(new_instance ~global:glob poly binders instance
(Some (true, CRecord (Loc.ghost,[])))
- ~generalize:false ~tac ~hook:(declare_projection n instance_id) None)
+ ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
(** Bind to "rewrite" too *)
diff --git a/ltac/rewrite.mli b/ltac/rewrite.mli
index f448c85430..35c4483513 100644
--- a/ltac/rewrite.mli
+++ b/ltac/rewrite.mli
@@ -62,6 +62,9 @@ val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strat
val map_strategy : ('a -> 'b) -> ('c -> 'd) ->
('a, 'c) strategy_ast -> ('b, 'd) strategy_ast
+val pr_strategy : ('a -> Pp.std_ppcmds) -> ('b -> Pp.std_ppcmds) ->
+ ('a, 'b) strategy_ast -> Pp.std_ppcmds
+
(** Entry point for user-level "rewrite_strat" *)
val cl_rewrite_clause_strat : strategy -> Id.t option -> unit Proofview.tactic
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 08e67a0c2f..aa45f1ccf5 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -646,7 +646,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
let constr_flags = {
use_typeclasses = true;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = Some solve_by_implicit_tactic;
fail_evar = true;
expand_evars = true }
@@ -661,21 +661,21 @@ let interp_type = interp_constr_gen IsType
let open_constr_use_classes_flags = {
use_typeclasses = true;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = Some solve_by_implicit_tactic;
fail_evar = false;
expand_evars = true }
let open_constr_no_classes_flags = {
use_typeclasses = false;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = Some solve_by_implicit_tactic;
fail_evar = false;
expand_evars = true }
let pure_open_constr_flags = {
use_typeclasses = false;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = None;
fail_evar = false;
expand_evars = false }
@@ -875,6 +875,9 @@ let rec message_of_value v =
Ftactic.return (pr_closed_glob_env (pf_env gl)
(project gl) c)
end }
+ else if has_type v (topwit wit_var) then
+ let id = out_gen (topwit wit_var) v in
+ Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_id id) end }
else match Value.to_list v with
| Some l ->
Ftactic.List.map message_of_value l >>= fun l ->
@@ -954,7 +957,7 @@ let interp_or_and_intro_pattern_option ist env sigma = function
(match coerce_to_intro_pattern env (Id.Map.find id ist.lfun) with
| IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l)
| _ ->
- raise (CannotCoerceTo "a disjunctive/conjunctive introduction pattern"))
+ user_err_loc (loc,"", str "Cannot coerce to a disjunctive/conjunctive pattern."))
| Some (ArgArg (loc,l)) ->
let sigma,l = interp_or_and_intro_pattern ist env sigma l in
sigma, Some (loc,l)
diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml
index e1c9fed637..5cbddc7f64 100644
--- a/ltac/tactic_debug.ml
+++ b/ltac/tactic_debug.ml
@@ -385,6 +385,8 @@ let skip_extensions trace =
| [] -> [] in
List.rev (aux (List.rev trace))
+let finer_loc loc1 loc2 = Loc.merge loc1 loc2 = loc2
+
let extract_ltac_trace trace eloc =
let trace = skip_extensions trace in
let (loc,c),tail = List.sep_last trace in
@@ -392,11 +394,10 @@ let extract_ltac_trace trace eloc =
(* We entered a user-defined tactic,
we display the trace with location of the call *)
let msg = hov 0 (explain_ltac_call_trace c tail eloc ++ fnl()) in
- Some msg, loc
+ Some msg, if finer_loc eloc loc then eloc else loc
else
(* We entered a primitive tactic, we don't display trace but
report on the finest location *)
- let finer_loc loc1 loc2 = Loc.merge loc1 loc2 = loc2 in
let best_loc =
(* trace is with innermost call coming first *)
let rec aux best_loc = function
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 21:34:01 +0000