aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ssr/ssrast.mli6
-rw-r--r--plugins/ssr/ssrbwd.ml11
-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.ml18
-rw-r--r--plugins/ssrmatching/ssrmatching.mli10
12 files changed, 55 insertions, 69 deletions
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..0f10183426 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'
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..8f3b66b55c 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 =
@@ -173,7 +175,7 @@ let loc_ofCG = function
| (_, (_, Some s), _) -> Constrexpr_ops.constr_loc s
let mk_term k c ist = k, (mkRHole, Some c), ist
-let mk_lterm = mk_term ' '
+let mk_lterm = mk_term NoFlag
let nf_evar sigma c =
EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c))
@@ -863,7 +865,7 @@ let glob_cpattern gs p =
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
+ if k = Cpattern then glob_ssrterm gs (InParens, (v, Some t), None) else
match t.CAst.v with
| CNotation(_,(InConstrEntry,"( _ in _ )"), ([t1; t2], [], [], [])) ->
(try match glob t1, glob t2 with
@@ -916,7 +918,7 @@ let interp_rpattern s = function
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
+type cpattern = ssrtermkind * Genintern.glob_constr_and_expr * Geninterp.interp_sign option
let tag_of_cpattern = pi1
let loc_of_cpattern = loc_ofCG
let cpattern_of_term (c, t) ist = c, t, Some ist
@@ -978,13 +980,13 @@ let interp_pattern ?wit_ssrpatternarg env sigma0 red redty =
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 mkG ?(k=NoFlag) x ist = k, (x,None), ist in
let ist_of (_,_,ist) = ist in
let decode (_,_,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 (NoFlag,(c,None),ist)
| GVar id
when Option.has_some ist && let ist = Option.get ist in
Id.Map.mem id ist.lfun &&
@@ -1255,7 +1257,7 @@ 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 })
+ NoFlag, (DAst.make @@ GRef (GlobRef.VarRef id, None), None), 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
| _, Some { CAst.v = CHole _ } | GHole _, None -> true
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 1573998f6f..e68187555b 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -20,9 +20,11 @@ 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 = char * Genintern.glob_constr_and_expr * Geninterp.interp_sign option
+type cpattern = ssrtermkind * Genintern.glob_constr_and_expr * Geninterp.interp_sign option
val pr_cpattern : cpattern -> Pp.t
(** Pattern interpretation and matching *)
@@ -194,7 +196,7 @@ 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
+val cpattern_of_term : ssrtermkind * 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
@@ -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-01-31 12:16:22 +0000