aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/cctac.ml90
-rw-r--r--plugins/cc/cctac.mli2
-rw-r--r--plugins/ltac/extratactics.mlg4
-rw-r--r--plugins/ltac/pltac.ml2
-rw-r--r--plugins/ltac/pltac.mli1
-rw-r--r--plugins/ltac/rewrite.ml35
-rw-r--r--plugins/ltac/taccoerce.ml12
-rw-r--r--plugins/ssr/ssrast.mli6
-rw-r--r--plugins/ssr/ssrbwd.ml13
-rw-r--r--plugins/ssr/ssrcommon.ml14
-rw-r--r--plugins/ssr/ssrequality.ml4
-rw-r--r--plugins/ssr/ssrfwd.ml4
-rw-r--r--plugins/ssr/ssripats.ml2
-rw-r--r--plugins/ssr/ssrparser.mlg22
-rw-r--r--plugins/ssr/ssrprinters.ml14
-rw-r--r--plugins/ssr/ssrprinters.mli5
-rw-r--r--plugins/ssrmatching/g_ssrmatching.mlg14
-rw-r--r--plugins/ssrmatching/ssrmatching.ml169
-rw-r--r--plugins/ssrmatching/ssrmatching.mli26
19 files changed, 216 insertions, 223 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 23a7b89d2c..499c9684b2 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -429,55 +429,55 @@ let cc_tactic depth additionnal_terms =
match sol with
None -> Tacticals.New.tclFAIL 0 (str "congruence failed")
| Some reason ->
- debug (fun () -> Pp.str "Goal solved, generating proof ...");
- match reason with
- Discrimination (i,ipac,j,jpac) ->
- let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in
- let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
- discriminate_tac cstr p
- | Incomplete ->
- let open Glob_term in
- let env = Proofview.Goal.env gl in
- let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
- let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in
- let pr_missing (c, missing) =
- let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
- let holes = List.init missing (fun _ -> hole) in
- Printer.pr_glob_constr_env env sigma (DAst.make @@ GApp (c, holes))
- in
- let msg = Pp.(str "Goal is solvable by congruence but some arguments are missing."
- ++ fnl () ++
- str " Try " ++
- hov 8
- begin
- str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(")
- pr_missing terms_to_complete ++ str ")\","
- end ++
- str " replacing metavariables by arbitrary terms.") in
- Tacticals.New.tclFAIL 0 msg
- | Contradiction dis ->
- let env = Proofview.Goal.env gl in
- let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in
- let ta=term uf dis.lhs and tb=term uf dis.rhs in
- match dis.rule with
- Goal -> proof_tac p
- | Hyp id -> refute_tac (EConstr.of_constr id) ta tb p
- | HeqG id ->
- let id = EConstr.of_constr id in
- convert_to_goal_tac id ta tb p
- | HeqnH (ida,idb) ->
- let ida = EConstr.of_constr ida in
- let idb = EConstr.of_constr idb in
- convert_to_hyp_tac ida ta idb tb p
+ debug (fun () -> Pp.str "Goal solved, generating proof ...");
+ match reason with
+ Discrimination (i,ipac,j,jpac) ->
+ let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in
+ let cstr=(get_constructor_info uf ipac.cnode).ci_constr in
+ discriminate_tac cstr p
+ | Incomplete ->
+ let open Glob_term in
+ let env = Proofview.Goal.env gl in
+ let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
+ let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in
+ let pr_missing (c, missing) =
+ let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
+ let holes = List.init missing (fun _ -> hole) in
+ Printer.pr_glob_constr_env env sigma (DAst.make @@ GApp (c, holes))
+ in
+ let msg = Pp.(str "Goal is solvable by congruence but some arguments are missing."
+ ++ fnl () ++
+ str " Try " ++
+ hov 8
+ begin
+ str "\"congruence with (" ++
+ prlist_with_sep
+ (fun () -> str ")" ++ spc () ++ str "(")
+ pr_missing terms_to_complete ++
+ str ")\","
+ end ++
+ fnl() ++ str " replacing metavariables by arbitrary terms")
+ in
+ Tacticals.New.tclFAIL 0 msg
+ | Contradiction dis ->
+ let env = Proofview.Goal.env gl in
+ let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in
+ let ta=term uf dis.lhs and tb=term uf dis.rhs in
+ match dis.rule with
+ Goal -> proof_tac p
+ | Hyp id -> refute_tac (EConstr.of_constr id) ta tb p
+ | HeqG id ->
+ let id = EConstr.of_constr id in
+ convert_to_goal_tac id ta tb p
+ | HeqnH (ida,idb) ->
+ let ida = EConstr.of_constr ida in
+ let idb = EConstr.of_constr idb in
+ convert_to_hyp_tac ida ta idb tb p
end
-let cc_fail =
- Tacticals.New.tclZEROMSG (Pp.str "congruence failed.")
let congruence_tac depth l =
- Tacticals.New.tclORELSE
- (Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l))
- cc_fail
+ Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l)
(* Beware: reflexivity = constructor 1 = apply refl_equal
might be slow now, let's rather do something equivalent
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index 52fc3acb6f..79c7d2c676 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -14,8 +14,6 @@ val proof_tac: Ccproof.proof -> unit Proofview.tactic
val cc_tactic : int -> constr list -> unit Proofview.tactic
-val cc_fail : unit Proofview.tactic
-
val congruence_tac : int -> constr list -> unit Proofview.tactic
val f_equal : unit Proofview.tactic
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 0b5d36b845..4a2c298caa 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -608,7 +608,7 @@ END
{
let subst_var_with_hole occ tid t =
- let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in
+ let occref = if occ > 0 then ref occ else Locusops.error_invalid_occurrence [occ] in
let locref = ref 0 in
let rec substrec x = match DAst.get x with
| GVar id ->
@@ -628,7 +628,7 @@ let subst_var_with_hole occ tid t =
| _ -> map_glob_constr_left_to_right substrec x in
let t' = substrec t
in
- if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t'
+ if !occref > 0 then Locusops.error_invalid_occurrence [occ] else t'
let subst_hole_with_term occ tc t =
let locref = ref 0 in
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 80c13a3698..196a68e67c 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -47,6 +47,8 @@ let binder_tactic = Entry.create "binder_tactic"
let tactic = Entry.create "tactic"
(* Main entry for quotations *)
+let tactic_eoi = eoi_entry tactic
+
let () =
let open Stdarg in
let open Tacarg in
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 73bce84d18..c0bf6b9f76 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -40,3 +40,4 @@ val tactic_expr : raw_tactic_expr Entry.t
[@@deprecated "Deprecated in 8.13; use 'ltac_expr' instead"]
val binder_tactic : raw_tactic_expr Entry.t
val tactic : raw_tactic_expr Entry.t
+val tactic_eoi : raw_tactic_expr Entry.t
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 77162ce89a..59533eb3e3 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -855,26 +855,20 @@ let coerce env cstr res =
let res = { res with rew_evars = evars } in
apply_constraint env res.rew_car rel prf cstr res
-let apply_rule unify loccs : int pure_strategy =
- let (nowhere_except_in,occs) = convert_occs loccs in
- let is_occ occ =
- if nowhere_except_in
- then List.mem occ occs
- else not (List.mem occ occs)
- in
- { strategy = fun { state = occ ; env ;
+let apply_rule unify : occurrences_count pure_strategy =
+ { strategy = fun { state = occs ; env ;
term1 = t ; ty1 = ty ; cstr ; evars } ->
let unif = if isEvar (goalevars evars) t then None else unify env evars t in
match unif with
- | None -> (occ, Fail)
+ | None -> (occs, Fail)
| Some rew ->
- let occ = succ occ in
- if not (is_occ occ) then (occ, Fail)
- else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity)
+ let b, occs = update_occurrence_counter occs in
+ if not b then (occs, Fail)
+ else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occs, Identity)
else
let res = { rew with rew_car = ty } in
let res = Success (coerce env cstr res) in
- (occ, res)
+ (occs, res)
}
let apply_lemma l2r flags oc by loccs : strategy = { strategy =
@@ -890,9 +884,10 @@ let apply_lemma l2r flags oc by loccs : strategy = { strategy =
| None -> None
| Some rew -> Some rew
in
- let _, res = (apply_rule unify loccs).strategy { input with
- state = 0 ;
+ let loccs, res = (apply_rule unify).strategy { input with
+ state = initialize_occurrence_counter loccs ;
evars } in
+ check_used_occurrences loccs;
(), res
}
@@ -1423,12 +1418,13 @@ let rewrite_with l2r flags c occs : strategy = { strategy =
let (sigma, rew) = refresh_hypinfo env sigma c in
unify_eqn rew l2r flags env (sigma, cstrs) None t
in
- let app = apply_rule unify occs in
+ let app = apply_rule unify in
let strat =
Strategies.fix (fun aux ->
Strategies.choice app (subterm true default_flags aux))
in
- let _, res = strat.strategy { input with state = 0 } in
+ let occs, res = strat.strategy { input with state = initialize_occurrence_counter occs } in
+ check_used_occurrences occs;
((), res)
}
@@ -2076,11 +2072,12 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals =
Proofview.Goal.enter begin fun gl ->
let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in
let unify env evars t = unify_abs res l2r sort env evars t in
- let app = apply_rule unify occs in
+ let app = apply_rule unify in
let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in
let substrat = Strategies.fix recstrat in
let strat = { strategy = fun ({ state = () } as input) ->
- let _, res = substrat.strategy { input with state = 0 } in
+ let occs, res = substrat.strategy { input with state = initialize_occurrence_counter occs } in
+ check_used_occurrences occs;
(), res
}
in
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 4c1fe6417e..9abdc2ddbe 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -429,7 +429,15 @@ let pr_value env v =
| TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)
-let error_ltac_variable ?loc id env v s =
- CErrors.user_err ?loc (str "Ltac variable " ++ Id.print id ++
+exception CoercionError of Id.t * (Environ.env * Evd.evar_map) option * Val.t * string
+
+let () = CErrors.register_handler begin function
+| CoercionError (id, env, v, s) ->
+ Some (str "Ltac variable " ++ Id.print id ++
strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
strbrk "which cannot be coerced to " ++ str s ++ str".")
+| _ -> None
+end
+
+let error_ltac_variable ?loc id env v s =
+ Loc.raise ?loc (CoercionError (id, env, v, s))
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index f6a741f468..5fbabd7ca1 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -46,7 +46,11 @@ type ssrclear = ssrhyps
type ssrdocc = ssrclear option * ssrocc
(* OLD ssr terms *)
-type ssrtermkind = char (* FIXME, make algebraic *)
+(* terms are pre constr, the kind is a parsing/printing flag to distinguish
+ * between x, @x and (x). It affects automatic clear and let-in preservation. *)
+(* FIXME *)
+(* Cpattern is a temporary flag that becomes InParens ASAP. *)
+type ssrtermkind = Ssrmatching_plugin.Ssrmatching.ssrtermkind
type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr
(* NEW ssr term *)
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 61643c2aa3..37eba7d399 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -19,30 +19,21 @@ open Ssrmatching_plugin
open Ssrmatching
open Ssrast
-open Ssrprinters
open Ssrcommon
-let char_to_kind = function
- | '(' -> xInParens
- | '@' -> xWithAt
- | ' ' -> xNoFlag
- | 'x' -> xCpattern
- | _ -> assert false
-
(** Backward chaining tactics: apply, exact, congr. *)
(** The "apply" tactic *)
let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) =
(* ppdebug(lazy(str"sigma@interp_agen=" ++ pr_evar_map None (project gl))); *)
- let k = char_to_kind k in
let rc = pf_intern_term ist gl c in
let rcs' = rc :: rcs in
match goclr with
| None -> clr, rcs'
| Some ghyps ->
let clr' = snd (interp_hyps ist gl ghyps) @ clr in
- if k <> xNoFlag then clr', rcs' else
+ if k <> NoFlag then clr', rcs' else
let loc = rc.CAst.loc in
match DAst.get rc with
| GVar id when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs'
@@ -132,7 +123,7 @@ let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:
let vtac gv i gl' = refine_interp_apply_view i ist gl' gv in
let ggenl, tclGENTAC =
if gviews <> [] && ggenl <> [] then
- let ggenl= List.map (fun (x,g) -> x, cpattern_of_term g ist) (List.hd ggenl) in
+ let ggenl= List.map (fun (x,(k,p)) -> x, {kind=k; pattern=p; interpretation= Some ist}) (List.hd ggenl) in
[], Tacticals.tclTHEN (Proofview.V82.of_tactic (genstac (ggenl,[])))
else ggenl, Tacticals.tclTHEN Tacticals.tclIDTAC in
tclGENTAC (fun gl ->
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index cd219838d5..4d57abb465 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -290,7 +290,7 @@ let interp_hyps ist gl ghyps =
(* Old terms *)
let mk_term k c = k, (mkRHole, Some c)
-let mk_lterm c = mk_term xNoFlag c
+let mk_lterm c = mk_term NoFlag c
(* New terms *)
@@ -318,9 +318,9 @@ let interp_ast_closure_term (ist : Geninterp.interp_sign) (gl : 'goal Evd.sigma)
let ssrterm_of_ast_closure_term { body; annotation } =
let c = match annotation with
- | `Parens -> xInParens
- | `At -> xWithAt
- | _ -> xNoFlag in
+ | `Parens -> InParens
+ | `At -> WithAt
+ | _ -> NoFlag in
mk_term c body
let ssrdgens_of_parsed_dgens = function
@@ -926,7 +926,7 @@ let pf_interp_ty ?(resolve_typeclasses=false) env sigma0 ist ty =
CProdN (abs, force_type t)
| CLetIn (n, v, oty, t) -> incr n_binders; CLetIn (n, v, oty, force_type t)
| _ -> (mkCCast ty (mkCType None)).v)) ty in
- mk_term ' ' (force_type ty) in
+ mk_term NoFlag (force_type ty) in
let strip_cast (sigma, t) =
let open EConstr in
let rec aux t = match kind_of_type sigma t with
@@ -1099,7 +1099,7 @@ let hyp_of_var sigma v = SsrHyp (Loc.tag @@ EConstr.destVar sigma v)
let interp_clr sigma = function
| Some clr, (k, c)
- when (k = xNoFlag || k = xWithAt) && is_pf_var sigma c ->
+ when (k = NoFlag || k = WithAt) && is_pf_var sigma c ->
hyp_of_var sigma c :: clr
| Some clr, _ -> clr
| None, _ -> []
@@ -1167,7 +1167,7 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) =
let cl = EConstr.of_constr cl in
let clr = interp_clr sigma (oclr, (tag_of_cpattern t, c)) in
if not(occur_existential sigma c) then
- if tag_of_cpattern t = xWithAt then
+ if tag_of_cpattern t = WithAt then
if not (EConstr.isVar sigma c) then
errorstrm (str "@ can be used with variables only")
else match Tacmach.pf_get_hyp gl (EConstr.destVar sigma c) with
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index fdfba48024..aeb6b3cf85 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -232,7 +232,7 @@ let rec get_evalref env sigma c = match EConstr.kind sigma c with
(* Strip a pattern generated by a prenex implicit to its constant. *)
let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with
- | App (f, a) when kt = xNoFlag && Array.for_all (EConstr.isEvar sigma) a && EConstr.isConst sigma f ->
+ | App (f, a) when kt = NoFlag && Array.for_all (EConstr.isEvar sigma) a && EConstr.isConst sigma f ->
(sigma, f), true
| Const _ | Var _ -> p, true
| Proj _ -> p, true
@@ -736,7 +736,7 @@ let unlocktac ist args =
Ssrcommon.tacMK_SSR_CONST "locked" >>= fun locked ->
Ssrcommon.tacMK_SSR_CONST "master_key" >>= fun key ->
let ktacs = [
- (Proofview.tclEVARMAP >>= fun sigma -> unfoldtac None None (sigma, locked) xInParens);
+ (Proofview.tclEVARMAP >>= fun sigma -> unfoldtac None None (sigma, locked) InParens);
Ssrelim.casetac key (fun ?seed:_ k -> k)
] in
Tacticals.New.tclTHENLIST (List.map utac args @ ktacs)
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 4961138190..f2c7f495b3 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -143,8 +143,8 @@ let havetac ist
let gl, _ = pf_e_type_of gl idty in
pf_unify_HO gl args_id.(2) abstract_key in
Tacticals.tclTHENFIRST (Proofview.V82.of_tactic itac_mkabs) (fun gl ->
- let mkt t = mk_term xNoFlag t in
- let mkl t = (xNoFlag, (t, None)) in
+ let mkt t = mk_term NoFlag t in
+ let mkl t = (NoFlag, (t, None)) in
let interp gl rtc t = pf_abs_ssrterm ~resolve_typeclasses:rtc ist gl t in
let interp_ty gl rtc t =
let a,b,_,u = pf_interp_ty ~resolve_typeclasses:rtc (pf_env gl) (project gl) ist t in a,b,u in
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 46f90a7ee1..1e940b5ad3 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -741,7 +741,7 @@ let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin
[A.. -> Ind] and opens new goals for [A..] as well as for the branches
of [Ind], see the [~to_ind] argument *)
if not(Termops.occur_existential sigma c) then
- if Ssrmatching.tag_of_cpattern t = Ssrprinters.xWithAt then
+ if Ssrmatching.tag_of_cpattern t = Ssrmatching.WithAt then
if not (EConstr.isVar sigma c) then
Ssrcommon.errorstrm Pp.(str "@ can be used with variables only")
else match Context.Named.lookup (EConstr.destVar sigma c) hyps with
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index f06b460ee9..935cef58b9 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -38,6 +38,8 @@ open Constrexpr_ops
open Proofview
open Proofview.Notations
+open Ssrmatching_plugin.Ssrmatching
+
open Ssrprinters
open Ssrcommon
open Ssrtacticals
@@ -455,9 +457,9 @@ END
(* Old kinds of terms *)
let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
- | Tok.KEYWORD "(" -> xInParens
- | Tok.KEYWORD "@" -> xWithAt
- | _ -> xNoFlag
+ | Tok.KEYWORD "(" -> InParens
+ | Tok.KEYWORD "@" -> WithAt
+ | _ -> NoFlag
let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
@@ -554,9 +556,9 @@ END
GRAMMAR EXTEND Gram
GLOBAL: ssrbwdview;
ssrbwdview: [
- [ test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr -> { [mk_term xNoFlag c] }
+ [ test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr -> { [mk_term NoFlag c] }
| test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr; w = ssrbwdview -> {
- (mk_term xNoFlag c) :: w } ]];
+ (mk_term NoFlag c) :: w } ]];
END
(* New Views *)
@@ -2201,10 +2203,10 @@ let pr_ssrcongrarg _ _ _ ((n, f), dgens) =
ARGUMENT EXTEND ssrcongrarg TYPED AS ((int * ssrterm) * ssrdgens)
PRINTED BY { pr_ssrcongrarg }
-| [ natural(n) constr(c) ssrdgens(dgens) ] -> { (n, mk_term xNoFlag c), dgens }
-| [ natural(n) constr(c) ] -> { (n, mk_term xNoFlag c),([[]],[]) }
-| [ constr(c) ssrdgens(dgens) ] -> { (0, mk_term xNoFlag c), dgens }
-| [ constr(c) ] -> { (0, mk_term xNoFlag c), ([[]],[]) }
+| [ natural(n) constr(c) ssrdgens(dgens) ] -> { (n, mk_term NoFlag c), dgens }
+| [ natural(n) constr(c) ] -> { (n, mk_term NoFlag c),([[]],[]) }
+| [ constr(c) ssrdgens(dgens) ] -> { (0, mk_term NoFlag c), dgens }
+| [ constr(c) ] -> { (0, mk_term NoFlag c), ([[]],[]) }
END
@@ -2260,7 +2262,7 @@ let pr_rule = function
let pr_ssrrule _ _ _ = pr_rule
-let noruleterm loc = mk_term xNoFlag (mkCProp loc)
+let noruleterm loc = mk_term NoFlag (mkCProp loc)
}
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 95c8024e89..6ed68094dc 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -28,16 +28,6 @@ let pp_concat hd ?(sep=str", ") = function [] -> hd | x :: xs ->
let pp_term gl t =
let t = Reductionops.nf_evar (project gl) t in pr_econstr_env (pf_env gl) (project gl) t
-(* FIXME *)
-(* terms are pre constr, the kind is parsing/printing flag to distinguish
- * between x, @x and (x). It affects automatic clear and let-in preservation.
- * Cpattern is a temporary flag that becomes InParens ASAP. *)
-(* type ssrtermkind = InParens | WithAt | NoFlag | Cpattern *)
-let xInParens = '('
-let xWithAt = '@'
-let xNoFlag = ' '
-let xCpattern = 'x'
-
(* Term printing utilities functions for deciding bracketing. *)
let pr_paren prx x = hov 1 (str "(" ++ prx x ++ str ")")
(* String lexing utilities *)
@@ -45,10 +35,10 @@ let skip_wschars s =
let rec loop i = match s.[i] with '\n'..' ' -> loop (i + 1) | _ -> i in loop
(* We also guard characters that might interfere with the ssreflect *)
(* tactic syntax. *)
-let guard_term ch1 s i = match s.[i] with
+let guard_term kind s i = match s.[i] with
| '(' -> false
| '{' | '/' | '=' -> true
- | _ -> ch1 = xInParens
+ | _ -> kind = Ssrmatching_plugin.Ssrmatching.InParens
(* We also guard characters that might interfere with the ssreflect *)
(* tactic syntax. *)
diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli
index 87eb05b667..21fb28038a 100644
--- a/plugins/ssr/ssrprinters.mli
+++ b/plugins/ssr/ssrprinters.mli
@@ -24,11 +24,6 @@ val pp_concat :
Pp.t ->
?sep:Pp.t -> Pp.t list -> Pp.t
-val xInParens : ssrtermkind
-val xWithAt : ssrtermkind
-val xNoFlag : ssrtermkind
-val xCpattern : ssrtermkind
-
val pr_clear : (unit -> Pp.t) -> ssrclear -> Pp.t
val pr_clear_ne : ssrclear -> Pp.t
val pr_dir : ssrdir -> Pp.t
diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg
index 2252435658..7022949ab6 100644
--- a/plugins/ssrmatching/g_ssrmatching.mlg
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -67,9 +67,9 @@ END
{
let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
- | Tok.KEYWORD "(" -> '('
- | Tok.KEYWORD "@" -> '@'
- | _ -> ' '
+ | Tok.KEYWORD "(" -> InParens
+ | Tok.KEYWORD "@" -> WithAt
+ | _ -> NoFlag
let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
}
@@ -78,8 +78,8 @@ GRAMMAR EXTEND Gram
GLOBAL: cpattern;
cpattern: [[ k = ssrtermkind; c = constr -> {
let pattern = mk_term k c None in
- if loc_of_cpattern pattern <> Some loc && k = '('
- then mk_term 'x' c None
+ if loc_of_cpattern pattern <> Some loc && k = InParens
+ then mk_term Cpattern c None
else pattern } ]];
END
@@ -97,8 +97,8 @@ GRAMMAR EXTEND Gram
GLOBAL: lcpattern;
lcpattern: [[ k = ssrtermkind; c = lconstr -> {
let pattern = mk_term k c None in
- if loc_of_cpattern pattern <> Some loc && k = '('
- then mk_term 'x' c None
+ if loc_of_cpattern pattern <> Some loc && k = InParens
+ then mk_term Cpattern c None
else pattern } ]];
END
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index ea014250ca..2a21049c6e 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -37,6 +37,8 @@ open Evar_kinds
open Constrexpr
open Constrexpr_ops
+type ssrtermkind = | InParens | WithAt | NoFlag | Cpattern
+
let errorstrm = CErrors.user_err ~hdr:"ssrmatching"
let loc_error loc msg = CErrors.user_err ?loc ~hdr:msg (str msg)
let ppnl = Feedback.msg_info
@@ -78,10 +80,10 @@ let skip_wschars s =
let rec loop i = match s.[i] with '\n'..' ' -> loop (i + 1) | _ -> i in loop
(* We also guard characters that might interfere with the ssreflect *)
(* tactic syntax. *)
-let guard_term ch1 s i = match s.[i] with
+let guard_term kind s i = match s.[i] with
| '(' -> false
| '{' | '/' | '=' -> true
- | _ -> ch1 = '('
+ | _ -> kind = InParens
(* The call 'guard s i' should return true if the contents of s *)
(* starting at i need bracketing to avoid ambiguities. *)
let pr_guarded guard prc c =
@@ -102,14 +104,6 @@ let prl_glob_constr_and_expr env sigma = function
let pr_glob_constr_and_expr env sigma = function
| _, Some c -> pr_constr_expr env sigma c
| c, None -> pr_glob_constr c
-let pr_term (k, c, _) =
- let env = Global.env () in
- let sigma = Evd.from_env env in
- pr_guarded (guard_term k) (pr_glob_constr_and_expr env sigma) c
-let prl_term (k, c, _) =
- let env = Global.env () in
- let sigma = Evd.from_env env in
- pr_guarded (guard_term k) (prl_glob_constr_and_expr env sigma) c
(** Adding a new uninterpreted generic argument type *)
let add_genarg tag pr =
@@ -153,28 +147,6 @@ let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args)
let mkRCast rc rt = DAst.make @@ GCast (rc, dC rt)
let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t)
-(* ssrterm conbinators *)
-let combineCG t1 t2 f g =
- let mk_ist i1 i2 = match i1, i2 with
- | None, Some i -> Some i
- | Some i, None -> Some i
- | None, None -> None
- | Some i, Some j when i == j -> Some i
- | _ -> CErrors.anomaly (Pp.str "combineCG: different ist") in
- match t1, t2 with
- | (x, (t1, None), i1), (_, (t2, None), i2) ->
- x, (g t1 t2, None), mk_ist i1 i2
- | (x, (_, Some t1), i1), (_, (_, Some t2), i2) ->
- x, (mkRHole, Some (f t1 t2)), mk_ist i1 i2
- | _, (_, (_, None), _) -> CErrors.anomaly (str"have: mixed C-G constr.")
- | _ -> CErrors.anomaly (str"have: mixed G-C constr.")
-let loc_ofCG = function
- | (_, (s, None), _) -> Glob_ops.loc_of_glob_constr s
- | (_, (_, Some s), _) -> Constrexpr_ops.constr_loc s
-
-let mk_term k c ist = k, (mkRHole, Some c), ist
-let mk_lterm = mk_term ' '
-
let nf_evar sigma c =
EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c))
@@ -803,25 +775,15 @@ type ('ident, 'term) ssrpattern =
| E_In_X_In_T of 'term * 'ident * 'term
| E_As_X_In_T of 'term * 'ident * 'term
-let pr_pattern = function
- | T t -> prl_term t
- | In_T t -> str "in " ++ prl_term t
- | X_In_T (x,t) -> prl_term x ++ str " in " ++ prl_term t
- | In_X_In_T (x,t) -> str "in " ++ prl_term x ++ str " in " ++ prl_term t
+let pr_pattern pr_ident pr_term = function
+ | T t -> pr_term t
+ | In_T t -> str "in " ++ pr_term t
+ | X_In_T (x,t) -> pr_ident x ++ str " in " ++ pr_term t
+ | In_X_In_T (x,t) -> str "in " ++ pr_ident x ++ str " in " ++ pr_term t
| E_In_X_In_T (e,x,t) ->
- prl_term e ++ str " in " ++ prl_term x ++ str " in " ++ prl_term t
+ pr_term e ++ str " in " ++ pr_ident x ++ str " in " ++ pr_term t
| E_As_X_In_T (e,x,t) ->
- prl_term e ++ str " as " ++ prl_term x ++ str " in " ++ prl_term t
-
-let pr_pattern_w_ids = function
- | T t -> prl_term t
- | In_T t -> str "in " ++ prl_term t
- | X_In_T (x,t) -> pr_id x ++ str " in " ++ prl_term t
- | In_X_In_T (x,t) -> str "in " ++ pr_id x ++ str " in " ++ prl_term t
- | E_In_X_In_T (e,x,t) ->
- prl_term e ++ str " in " ++ pr_id x ++ str " in " ++ prl_term t
- | E_As_X_In_T (e,x,t) ->
- prl_term e ++ str " as " ++ pr_id x ++ str " in " ++ prl_term t
+ pr_term e ++ str " as " ++ pr_ident x ++ str " in " ++ pr_term t
let pr_pattern_aux pr_constr = function
| T t -> pr_constr t
@@ -834,16 +796,53 @@ let pr_pattern_aux pr_constr = function
pr_constr e ++ str " as " ++ pr_constr x ++ str " in " ++ pr_constr t
let pp_pattern env (sigma, p) =
pr_pattern_aux (fun t -> pr_econstr_pat env sigma (pi3 (nf_open_term sigma sigma (EConstr.of_constr t)))) p
+
+type cpattern =
+ { kind : ssrtermkind
+ ; pattern : Genintern.glob_constr_and_expr
+ ; interpretation : Geninterp.interp_sign option }
+
+let pr_term {kind; pattern; _} =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ pr_guarded (guard_term kind) (pr_glob_constr_and_expr env sigma) pattern
+let prl_term {kind; pattern; _} =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ pr_guarded (guard_term kind) (prl_glob_constr_and_expr env sigma) pattern
+
let pr_cpattern = pr_term
-let wit_rpatternty = add_genarg "rpatternty" (fun env sigma -> pr_pattern)
+let pr_pattern_w_ids = pr_pattern pr_id prl_term
+
+let mk_term k c ist = {kind=k; pattern=(mkRHole, Some c); interpretation=ist}
+let mk_lterm = mk_term NoFlag
let glob_ssrterm gs = function
- | k, (_, Some c), None ->
- let x = Tacintern.intern_constr gs c in
- k, (fst x, Some c), None
+ | {kind; pattern=(_, Some c); interpretation=None} ->
+ let x = Tacintern.intern_constr gs c in
+ {kind; pattern=(fst x, Some c); interpretation=None}
| ct -> ct
+(* ssrterm conbinators *)
+let combineCG t1 t2 f g =
+ let mk_ist i1 i2 = match i1, i2 with
+ | None, Some i -> Some i
+ | Some i, None -> Some i
+ | None, None -> None
+ | Some i, Some j when i == j -> Some i
+ | _ -> CErrors.anomaly (Pp.str "combineCG: different ist") in
+ match t1, t2 with
+ | {kind=x; pattern=(t1, None); interpretation=i1}, {pattern=(t2, None); interpretation=i2} ->
+ {kind=x; pattern=(g t1 t2, None); interpretation = mk_ist i1 i2}
+ | {kind=x; pattern=(_, Some t1); interpretation=i1}, {pattern=(_, Some t2); interpretation=i2} ->
+ {kind=x; pattern=(mkRHole, Some (f t1 t2)); interpretation = mk_ist i1 i2}
+ | _, {pattern=(_, None); _} -> CErrors.anomaly (str"have: mixed C-G constr.")
+ | _ -> CErrors.anomaly (str"have: mixed G-C constr.")
+let loc_ofCG = function
+ | {pattern = (s, None); _} -> Glob_ops.loc_of_glob_constr s
+ | {pattern = (_, Some s); _} -> Constrexpr_ops.constr_loc s
+
(* This piece of code asserts the following notations are reserved *)
(* Reserved Notation "( a 'in' b )" (at level 0). *)
(* Reserved Notation "( a 'as' b )" (at level 0). *)
@@ -851,19 +850,19 @@ let glob_ssrterm gs = function
(* Reserved Notation "( a 'as' b 'in' c )" (at level 0). *)
let glob_cpattern gs p =
pp(lazy(str"globbing pattern: " ++ pr_term p));
- let glob x = pi2 (glob_ssrterm gs (mk_lterm x None)) in
+ let glob x = (glob_ssrterm gs (mk_lterm x None)).pattern in
let encode k s l =
let name = Name (Id.of_string ("_ssrpat_" ^ s)) in
- k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None), None in
+ {kind=k; pattern=(mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None); interpretation=None} in
let bind_in t1 t2 =
let mkCHole = mkCHole ~loc:None in let n = Name (destCVar t1) in
fst (glob (mkCCast mkCHole (mkCLambda n mkCHole t2))) in
let check_var t2 = if not (isCVar t2) then
loc_error (constr_loc t2) "Only identifiers are allowed here" in
match p with
- | _, (_, None), _ as x -> x
- | k, (v, Some t), _ as orig ->
- if k = 'x' then glob_ssrterm gs ('(', (v, Some t), None) else
+ | {pattern = (_, None); _} as x -> x
+ | {kind=k; pattern=(v, Some t); _} as orig ->
+ if k = Cpattern then glob_ssrterm gs {kind=InParens; pattern=(v, Some t); interpretation=None} else
match t.CAst.v with
| CNotation(_,(InConstrEntry,"( _ in _ )"), ([t1; t2], [], [], [])) ->
(try match glob t1, glob t2 with
@@ -891,8 +890,8 @@ let glob_rpattern s p =
| E_In_X_In_T(e,x,t) -> E_In_X_In_T (glob_ssrterm s e,x,glob_ssrterm s t)
| E_As_X_In_T(e,x,t) -> E_As_X_In_T (glob_ssrterm s e,x,glob_ssrterm s t)
-let subst_ssrterm s (k, c, ist) =
- k, Tacsubst.subst_glob_constr_and_expr s c, ist
+let subst_ssrterm s {kind; pattern; interpretation} =
+ {kind; pattern=Tacsubst.subst_glob_constr_and_expr s pattern; interpretation}
let subst_rpattern s = function
| T t -> T (subst_ssrterm s t)
@@ -902,7 +901,7 @@ let subst_rpattern s = function
| E_In_X_In_T(e,x,t) -> E_In_X_In_T (subst_ssrterm s e,x,subst_ssrterm s t)
| E_As_X_In_T(e,x,t) -> E_As_X_In_T (subst_ssrterm s e,x,subst_ssrterm s t)
-let interp_ssrterm ist (k,t,_) = k, t, Some ist
+let interp_ssrterm ist {kind; pattern; _} = {kind; pattern; interpretation = Some ist}
let interp_rpattern s = function
| T t -> T (interp_ssrterm s t)
@@ -910,23 +909,24 @@ let interp_rpattern s = function
| X_In_T(x,t) -> X_In_T (interp_ssrterm s x,interp_ssrterm s t)
| In_X_In_T(x,t) -> In_X_In_T (interp_ssrterm s x,interp_ssrterm s t)
| E_In_X_In_T(e,x,t) ->
- E_In_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t)
+ E_In_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t)
| E_As_X_In_T(e,x,t) ->
- E_As_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t)
+ E_As_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t)
let interp_rpattern0 ist gl t = Tacmach.project gl, interp_rpattern ist t
-type cpattern = char * Genintern.glob_constr_and_expr * Geninterp.interp_sign option
-let tag_of_cpattern = pi1
+let tag_of_cpattern p = p.kind
let loc_of_cpattern = loc_ofCG
-let cpattern_of_term (c, t) ist = c, t, Some ist
type occ = (bool * int list) option
type rpattern = (cpattern, cpattern) ssrpattern
+let pr_rpattern = pr_pattern pr_cpattern pr_cpattern
+
+let wit_rpatternty = add_genarg "rpatternty" (fun env sigma -> pr_pattern pr_cpattern pr_cpattern)
type pattern = Evd.evar_map * (constr, constr) ssrpattern
-let id_of_cpattern (_, (c1, c2), _) =
+let id_of_cpattern {pattern = (c1, c2); _} =
let open CAst in
match DAst.get c1, c2 with
| _, Some { v = CRef (qid, _) } when qualid_is_ident qid ->
@@ -941,12 +941,12 @@ let id_of_Cterm t = match id_of_cpattern t with
let interp_open_constr ist env sigma gc =
Tacinterp.interp_open_constr ist env sigma gc
-let pf_intern_term env sigma (_, c, ist) = glob_constr ist env sigma c
+let pf_intern_term env sigma {pattern = c; interpretation = ist; _} = glob_constr ist env sigma c
let interp_ssrterm ist gl t = Tacmach.project gl, interp_ssrterm ist t
let interp_term env sigma = function
- | (_, c, Some ist) ->
+ | {pattern = c; interpretation = Some ist; _} ->
on_snd EConstr.Unsafe.to_constr (interp_open_constr ist env sigma c)
| _ -> errorstrm (str"interpreting a term with no ist")
@@ -974,17 +974,17 @@ let pr_ist { lfun= lfun } =
*)
let interp_pattern ?wit_ssrpatternarg env sigma0 red redty =
- pp(lazy(str"interpreting: " ++ pr_pattern red));
+ pp(lazy(str"interpreting: " ++ pr_rpattern red));
let xInT x y = X_In_T(x,y) and inXInT x y = In_X_In_T(x,y) in
let inT x = In_T x and eInXInT e x t = E_In_X_In_T(e,x,t) in
let eAsXInT e x t = E_As_X_In_T(e,x,t) in
- let mkG ?(k=' ') x ist = k,(x,None), ist in
- let ist_of (_,_,ist) = ist in
- let decode (_,_,ist as t) ?reccall f g =
+ let mkG ?(k=NoFlag) x ist = {kind = k; pattern = (x,None); interpretation = ist } in
+ let ist_of x = x.interpretation in
+ let decode ({interpretation=ist; _} as t) ?reccall f g =
try match DAst.get (pf_intern_term env sigma0 t) with
| GCast(t,CastConv c) when isGHole t && isGLambda c->
let (x, c) = destGLambda c in
- f x (' ',(c,None),ist)
+ f x {kind = NoFlag; pattern = (c,None); interpretation = ist}
| GVar id
when Option.has_some ist && let ist = Option.get ist in
Id.Map.mem id ist.lfun &&
@@ -1027,7 +1027,7 @@ let interp_pattern ?wit_ssrpatternarg env sigma0 red redty =
sigma new_evars in
sigma in
let red = let rec decode_red = function
- | T(k,(t,None),ist) ->
+ | T {kind=k; pattern=(t,None); interpretation=ist} ->
begin match DAst.get t with
| GCast (c,CastConv t)
when isGHole c &&
@@ -1058,7 +1058,7 @@ let interp_pattern ?wit_ssrpatternarg env sigma0 red redty =
let red =
match redty with
| None -> red
- | Some (ty, ist) -> let ty = ' ', ty, Some ist in
+ | Some (ty, ist) -> let ty = {kind=NoFlag; pattern=ty; interpretation = Some ist} in
match red with
| T t -> T (combineCG t ty (mkCCast ?loc:(loc_ofCG t)) mkRCast)
| X_In_T (x,t) ->
@@ -1072,9 +1072,12 @@ let interp_pattern ?wit_ssrpatternarg env sigma0 red redty =
E_As_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t)
| red -> red in
pp(lazy(str"typed as: " ++ pr_pattern_w_ids red));
- let mkXLetIn ?loc x (a,(g,c),ist) = match c with
- | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b)), ist
- | None -> a,(DAst.make ?loc @@ GLetIn (x, DAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None), ist in
+ let mkXLetIn ?loc x {kind; pattern=(g,c); interpretation} = match c with
+ | Some b -> {kind; pattern=(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b)); interpretation}
+ | None -> { kind
+ ; pattern = DAst.make ?loc @@ GLetIn
+ (x, DAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None
+ ; interpretation} in
match red with
| T t -> let sigma, t = interp_term env sigma0 t in sigma, T t
| In_T t -> let sigma, t = interp_term env sigma0 t in sigma, In_T t
@@ -1255,16 +1258,16 @@ let pf_fill_occ_term gl occ t =
cl, t
let cpattern_of_id id =
- ' ', (DAst.make @@ GRef (GlobRef.VarRef id, None), None), Some Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty })
+ { kind= NoFlag
+ ; pattern = DAst.make @@ GRef (GlobRef.VarRef id, None), None
+ ; interpretation = Some Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty })}
-let is_wildcard ((_, (l, r), _) : cpattern) : bool = match DAst.get l, r with
+let is_wildcard ({pattern = (l, r); _} : cpattern) : bool = match DAst.get l, r with
| _, Some { CAst.v = CHole _ } | GHole _, None -> true
| _ -> false
(* "ssrpattern" *)
-let pr_rpattern = pr_pattern
-
let pf_merge_uc uc gl =
re_sig (sig_it gl) (Evd.merge_universe_context (project gl) uc)
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 17b47227cb..2b90cef039 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -20,17 +20,16 @@ open Genintern
(** Pattern parsing *)
+type ssrtermkind = | InParens | WithAt | NoFlag | Cpattern
+
(** The type of context patterns, the patterns of the [set] tactic and
[:] tactical. These are patterns that identify a precise subterm. *)
-type cpattern
+type cpattern =
+ { kind : ssrtermkind
+ ; pattern : Genintern.glob_constr_and_expr
+ ; interpretation : Geninterp.interp_sign option }
val pr_cpattern : cpattern -> Pp.t
-(** The type of rewrite patterns, the patterns of the [rewrite] tactic.
- These patterns also include patterns that identify all the subterms
- of a context (i.e. "in" prefix) *)
-type rpattern
-val pr_rpattern : rpattern -> Pp.t
-
(** Pattern interpretation and matching *)
exception NoMatch
@@ -48,6 +47,12 @@ type ('ident, 'term) ssrpattern =
type pattern = evar_map * (constr, constr) ssrpattern
val pp_pattern : env -> pattern -> Pp.t
+(** The type of rewrite patterns, the patterns of the [rewrite] tactic.
+ These patterns also include patterns that identify all the subterms
+ of a context (i.e. "in" prefix) *)
+type rpattern = (cpattern, cpattern) ssrpattern
+val pr_rpattern : rpattern -> Pp.t
+
(** Extracts the redex and applies to it the substitution part of the pattern.
@raise Anomaly if called on [In_T] or [In_X_In_T] *)
val redex_of_pattern :
@@ -193,9 +198,6 @@ val pf_fill_occ_term : goal sigma -> occ -> evar_map * EConstr.t -> EConstr.t *
val fill_occ_term : Environ.env -> Evd.evar_map -> EConstr.t -> occ -> evar_map * EConstr.t -> EConstr.t * EConstr.t
-(* It may be handy to inject a simple term into the first form of cpattern *)
-val cpattern_of_term : char * glob_constr_and_expr -> Geninterp.interp_sign -> cpattern
-
(** Helpers to make stateful closures. Example: a [find_P] function may be
called many times, but the pattern instantiation phase is performed only the
first time. The corresponding [conclude] has to return the instantiated
@@ -219,7 +221,7 @@ val pf_unify_HO : goal sigma -> EConstr.constr -> EConstr.constr -> goal sigma
(** Some more low level functions needed to implement the full SSR language
on top of the former APIs *)
-val tag_of_cpattern : cpattern -> char
+val tag_of_cpattern : cpattern -> ssrtermkind
val loc_of_cpattern : cpattern -> Loc.t option
val id_of_pattern : pattern -> Names.Id.t option
val is_wildcard : cpattern -> bool
@@ -245,7 +247,7 @@ sig
val pr_rpattern : rpattern -> Pp.t
val mk_rpattern : (cpattern, cpattern) ssrpattern -> rpattern
val mk_lterm : Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern
- val mk_term : char -> Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern
+ val mk_term : ssrtermkind -> Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern
val glob_cpattern : Genintern.glob_sign -> cpattern -> cpattern
val subst_ssrterm : Mod_subst.substitution -> cpattern -> cpattern
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 12:47:37 +0000