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/g_rewrite.ml413
-rw-r--r--ltac/profile_ltac.ml8
-rw-r--r--ltac/profile_ltac_tactics.ml42
-rw-r--r--ltac/rewrite.ml34
-rw-r--r--ltac/rewrite.mli3
8 files changed, 76 insertions, 8 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/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 102918e5e5..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 () ++
@@ -401,11 +401,11 @@ let print_results ~cutoff =
print_results_filter ~cutoff ~filter:(fun _ -> true)
let print_results_tactic tactic =
- print_results_filter ~cutoff:0.0 ~filter:(fun s ->
+ print_results_filter ~cutoff:!Flags.profile_ltac_cutoff ~filter:(fun s ->
String.(equal tactic (sub (s ^ ".") 0 (min (1+length s) (length tactic)))))
let do_print_results_at_close () =
- if get_profiling () then print_results ~cutoff:0.0
+ if get_profiling () then print_results ~cutoff:!Flags.profile_ltac_cutoff
let _ = Declaremods.append_end_library_hook do_print_results_at_close
diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4
index 9083bda60a..8cb76d81c5 100644
--- a/ltac/profile_ltac_tactics.ml4
+++ b/ltac/profile_ltac_tactics.ml4
@@ -31,7 +31,7 @@ VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF
END
VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
-| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:0.0 ]
+| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:!Flags.profile_ltac_cutoff ]
| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ]
END
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 69f45e1aeb..4d7c5d0e4b 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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 18:08:23 +0000