Split the Ssrmatching module between code and grammar rules.

Fixes #7857.

6 files changed, 160 insertions, 99 deletions

diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 347a1e4e2..6b183dab1 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -962,6 +962,7 @@ END
 (* the default simpl and unfold tactics would erase blindly.               *)
 
 open Ssrmatching_plugin.Ssrmatching
+open Ssrmatching_plugin.G_ssrmatching
 
 let pr_wgen = function 
   | (clr, Some((id,k),None)) -> spc() ++ pr_clear mt clr ++ str k ++ pr_hoi id
diff --git a/plugins/ssrmatching/g_ssrmatching.ml4 b/plugins/ssrmatching/g_ssrmatching.ml4
new file mode 100644
index 000000000..746c368aa
--- /dev/null
+++ b/plugins/ssrmatching/g_ssrmatching.ml4
@@ -0,0 +1,101 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Ltac_plugin
+open Genarg
+open Pcoq
+open Pcoq.Constr
+open Ssrmatching
+open Ssrmatching.Internal
+
+(* Defining grammar rules with "xx" in it automatically declares keywords too,
+ * we thus save the lexer to restore it at the end of the file *)
+let frozen_lexer = CLexer.get_keyword_state () ;;
+
+DECLARE PLUGIN "ssrmatching_plugin"
+
+let pr_rpattern _ _ _ = pr_rpattern
+
+ARGUMENT EXTEND rpattern
+  TYPED AS rpatternty
+  PRINTED BY pr_rpattern
+  INTERPRETED BY interp_rpattern
+  GLOBALIZED BY glob_rpattern
+  SUBSTITUTED BY subst_rpattern
+  | [ lconstr(c) ] -> [ mk_rpattern (T (mk_lterm c None)) ]
+  | [ "in" lconstr(c) ] -> [ mk_rpattern (In_T (mk_lterm c None)) ]
+  | [ lconstr(x) "in" lconstr(c) ] ->
+    [ mk_rpattern (X_In_T (mk_lterm x None, mk_lterm c None)) ]
+  | [ "in" lconstr(x) "in" lconstr(c) ] ->
+    [ mk_rpattern (In_X_In_T (mk_lterm x None, mk_lterm c None)) ]
+  | [ lconstr(e) "in" lconstr(x) "in" lconstr(c) ] ->
+    [ mk_rpattern (E_In_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) ]
+  | [ lconstr(e) "as" lconstr(x) "in" lconstr(c) ] ->
+    [ mk_rpattern (E_As_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None)) ]
+END
+
+let pr_ssrterm _ _ _ = pr_ssrterm
+
+ARGUMENT EXTEND cpattern
+     PRINTED BY pr_ssrterm
+     INTERPRETED BY interp_ssrterm
+     GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm
+     RAW_PRINTED BY pr_ssrterm
+     GLOB_PRINTED BY pr_ssrterm
+| [ "Qed" constr(c) ] -> [ mk_lterm c None ]
+END
+
+let input_ssrtermkind strm = match Util.stream_nth 0 strm with
+  | Tok.KEYWORD "(" -> '('
+  | Tok.KEYWORD "@" -> '@'
+  | _ -> ' '
+let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
+
+GEXTEND 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
+    else pattern ]];
+END
+
+ARGUMENT EXTEND lcpattern
+     TYPED AS cpattern
+     PRINTED BY pr_ssrterm
+     INTERPRETED BY interp_ssrterm
+     GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm
+     RAW_PRINTED BY pr_ssrterm
+     GLOB_PRINTED BY pr_ssrterm
+| [ "Qed" lconstr(c) ] -> [ mk_lterm c None ]
+END
+
+GEXTEND 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
+    else pattern ]];
+END
+
+ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY pr_rpattern
+| [ rpattern(pat) ] -> [ pat ]
+END
+
+TACTIC EXTEND ssrinstoftpat
+| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof arg) ]
+END
+
+(* We wipe out all the keywords generated by the grammar rules we defined. *)
+(* The user is supposed to Require Import ssreflect or Require ssreflect   *)
+(* and Import ssreflect.SsrSyntax to obtain these keywords and as a         *)
+(* consequence the extended ssreflect grammar.                             *)
+let () = CLexer.set_keyword_state frozen_lexer ;;
diff --git a/plugins/ssrmatching/g_ssrmatching.mli b/plugins/ssrmatching/g_ssrmatching.mli
new file mode 100644
index 000000000..bb5161a0e
--- /dev/null
+++ b/plugins/ssrmatching/g_ssrmatching.mli
@@ -0,0 +1,17 @@
+(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
+(* Distributed under the terms of CeCILL-B.                                  *)
+
+open Genarg
+open Ssrmatching
+
+(** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *)
+val cpattern         : cpattern Pcoq.Gram.entry
+val wit_cpattern     : cpattern uniform_genarg_type
+
+(** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *)
+val lcpattern         : cpattern Pcoq.Gram.entry
+val wit_lcpattern     : cpattern uniform_genarg_type
+
+(** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *)
+val rpattern         : rpattern Pcoq.Gram.entry
+val wit_rpattern     : rpattern uniform_genarg_type
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml
index 9d9b1b2e8..05eda14e9 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -10,10 +10,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-(* Defining grammar rules with "xx" in it automatically declares keywords too,
- * we thus save the lexer to restore it at the end of the file *)
-let frozen_lexer = CLexer.get_keyword_state () ;;
-
 open Ltac_plugin
 open Names
 open Pp
@@ -22,8 +18,6 @@ open Stdarg
 open Term
 module CoqConstr = Constr
 open CoqConstr
-open Pcoq
-open Pcoq.Constr
 open Vars
 open Libnames
 open Tactics
@@ -46,8 +40,6 @@ open Evar_kinds
 open Constrexpr
 open Constrexpr_ops
 
-DECLARE PLUGIN "ssrmatching_plugin"
-
 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
@@ -907,7 +899,6 @@ let pr_pattern_aux pr_constr = function
 let pp_pattern (sigma, p) =
   pr_pattern_aux (fun t -> pr_constr_pat (EConstr.Unsafe.to_constr (pi3 (nf_open_term sigma sigma (EConstr.of_constr t))))) p
 let pr_cpattern = pr_term
-let pr_rpattern _ _ _ = pr_pattern
 
 let wit_rpatternty = add_genarg "rpatternty" pr_pattern
 
@@ -987,27 +978,7 @@ let interp_rpattern s = function
   | 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)
 
-let interp_rpattern ist gl t = Tacmach.project gl, interp_rpattern ist t
-
-ARGUMENT EXTEND rpattern
-  TYPED AS rpatternty
-  PRINTED BY pr_rpattern
-  INTERPRETED BY interp_rpattern
-  GLOBALIZED BY glob_rpattern
-  SUBSTITUTED BY subst_rpattern
-  | [ lconstr(c) ] -> [ T (mk_lterm c None) ]
-  | [ "in" lconstr(c) ] -> [ In_T (mk_lterm c None) ]
-  | [ lconstr(x) "in" lconstr(c) ] -> 
-    [ X_In_T (mk_lterm x None, mk_lterm c None) ]
-  | [ "in" lconstr(x) "in" lconstr(c) ] -> 
-    [ In_X_In_T (mk_lterm x None, mk_lterm c None) ]
-  | [ lconstr(e) "in" lconstr(x) "in" lconstr(c) ] -> 
-    [ E_In_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None) ]
-  | [ lconstr(e) "as" lconstr(x) "in" lconstr(c) ] -> 
-    [ E_As_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None) ]
-END
-
-
+let interp_rpattern0 ist gl t = Tacmach.project gl, interp_rpattern ist t
 
 type cpattern = char * glob_constr_and_expr * Geninterp.interp_sign option
 let tag_of_cpattern = pi1
@@ -1051,52 +1022,9 @@ let interp_wit wit ist gl x =
 let interp_open_constr ist gl gc =
   interp_wit wit_open_constr ist gl gc
 let pf_intern_term gl (_, c, ist) = glob_constr ist (pf_env gl) (project gl) c
-let pr_ssrterm _ _ _ = pr_term
-let input_ssrtermkind strm = match stream_nth 0 strm with
-  | Tok.KEYWORD "(" -> '('
-  | Tok.KEYWORD "@" -> '@'
-  | _ -> ' '
-let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
 let interp_ssrterm ist gl t = Tacmach.project gl, interp_ssrterm ist t
 
-ARGUMENT EXTEND cpattern
-     PRINTED BY pr_ssrterm
-     INTERPRETED BY interp_ssrterm
-     GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm
-     RAW_PRINTED BY pr_ssrterm
-     GLOB_PRINTED BY pr_ssrterm
-| [ "Qed" constr(c) ] -> [ mk_lterm c None ]
-END
-
-GEXTEND Gram
-  GLOBAL: cpattern;
-  cpattern: [[ k = ssrtermkind; c = constr ->
-    let pattern = mk_term k c None in
-    if loc_ofCG pattern <> Some !@loc && k = '('
-    then mk_term 'x' c None
-    else pattern ]];
-END
-
-ARGUMENT EXTEND lcpattern
-     TYPED AS cpattern
-     PRINTED BY pr_ssrterm
-     INTERPRETED BY interp_ssrterm
-     GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm
-     RAW_PRINTED BY pr_ssrterm
-     GLOB_PRINTED BY pr_ssrterm
-| [ "Qed" lconstr(c) ] -> [ mk_lterm c None ]
-END
-
-GEXTEND Gram
-  GLOBAL: lcpattern;
-  lcpattern: [[ k = ssrtermkind; c = lconstr ->
-    let pattern = mk_term k c None in
-    if loc_ofCG pattern <> Some !@loc && k = '('
-    then mk_term 'x' c None
-    else pattern ]];
-END
-
 let interp_term gl = function
   | (_, c, Some ist) ->
       on_snd EConstr.Unsafe.to_constr (interp_open_constr ist gl c)
@@ -1416,10 +1344,6 @@ let is_wildcard ((_, (l, r), _) : cpattern) : bool = match DAst.get l, r with
 
 (* "ssrpattern" *)
 
-ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY pr_rpattern
-| [ rpattern(pat) ] -> [ pat ]
-END
-
 let pr_rpattern = pr_pattern
   
 let pf_merge_uc uc gl =
@@ -1428,6 +1352,9 @@ let pf_merge_uc uc gl =
 let pf_unsafe_merge_uc uc gl =
   re_sig (sig_it gl) (Evd.set_universe_context (project gl) uc)
 
+(** All the pattern types reuse the same dynamic toplevel tag *)
+let wit_ssrpatternarg = wit_rpatternty
+
 let interp_rpattern = interp_rpattern ~wit_ssrpatternarg
 
 let ssrpatterntac _ist arg gl =
@@ -1479,14 +1406,20 @@ let ssrinstancesof arg gl =
     done; raise NoMatch
   with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl
 
-TACTIC EXTEND ssrinstoftpat
-| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof arg) ]
-END
-
-(* We wipe out all the keywords generated by the grammar rules we defined. *)
-(* The user is supposed to Require Import ssreflect or Require ssreflect   *)
-(* and Import ssreflect.SsrSyntax to obtain these keywords and as a         *)
-(* consequence the extended ssreflect grammar.                             *)
-let () = CLexer.set_keyword_state frozen_lexer ;;
+module Internal =
+struct
+  let wit_rpatternty = wit_rpatternty
+  let glob_rpattern = glob_rpattern
+  let subst_rpattern = subst_rpattern
+  let interp_rpattern = interp_rpattern0
+  let pr_rpattern = pr_rpattern
+  let mk_rpattern x = x
+  let mk_lterm = mk_lterm
+  let mk_term = mk_term
+  let glob_cpattern = glob_cpattern
+  let subst_ssrterm = subst_ssrterm
+  let interp_ssrterm = interp_ssrterm
+  let pr_ssrterm = pr_term
+end
 
 (* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index c55081e0f..f478d48ea 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -2,7 +2,6 @@
 (* Distributed under the terms of CeCILL-B.                                  *)
 
 open Goal
-open Genarg
 open Environ
 open Evd
 open Constr
@@ -19,24 +18,12 @@ open Tacexpr
 type cpattern
 val pr_cpattern : cpattern -> Pp.t
 
-(** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *)
-val cpattern         : cpattern Pcoq.Gram.entry
-val wit_cpattern     : cpattern uniform_genarg_type
-
-(** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *)
-val lcpattern         : cpattern Pcoq.Gram.entry
-val wit_lcpattern     : cpattern uniform_genarg_type
-
 (** 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
 
-(** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *)
-val rpattern         : rpattern Pcoq.Gram.entry
-val wit_rpattern     : rpattern uniform_genarg_type
-
 (** Pattern interpretation and matching *)
 
 exception NoMatch
@@ -238,4 +225,25 @@ val debug : bool -> unit
  * "Unset SsrMatchingProfiling" to get timings *)
 val profile : bool -> unit
 
+val ssrinstancesof : cpattern -> Tacmach.tactic
+
+(** Functions used for grammar extensions. Do not use. *)
+
+module Internal :
+sig
+  val wit_rpatternty : (rpattern, rpattern, rpattern) Genarg.genarg_type
+  val glob_rpattern : Genintern.glob_sign -> rpattern -> rpattern
+  val subst_rpattern : Mod_subst.substitution -> rpattern -> rpattern
+  val interp_rpattern : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> rpattern -> Evd.evar_map * rpattern
+  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 glob_cpattern : Genintern.glob_sign -> cpattern -> cpattern
+  val subst_ssrterm : Mod_subst.substitution -> cpattern -> cpattern
+  val interp_ssrterm : Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> cpattern -> Evd.evar_map * cpattern
+  val pr_ssrterm : cpattern -> Pp.t
+end
+
 (* eof *)
diff --git a/plugins/ssrmatching/ssrmatching_plugin.mlpack b/plugins/ssrmatching/ssrmatching_plugin.mlpack
index 5fb1f1567..02c75f14e 100644
--- a/plugins/ssrmatching/ssrmatching_plugin.mlpack
+++ b/plugins/ssrmatching/ssrmatching_plugin.mlpack
@@ -1 +1,2 @@
 Ssrmatching
+G_ssrmatching