Make ssrtermkind algebraic instead of a char

9 files changed, 32 insertions, 50 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