aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssrmatching
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-27 21:34:39 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-30 09:57:05 +0200
commit9e26743cf40cdfd85317d2826ee05373d8670082 (patch)
tree3cb2eccd00e151b28c67c7a4f36db128faa2ea37 /plugins/ssrmatching
parente25d69f5d47f7ad6584bf54ea48e42fd482c95e0 (diff)
Split the Ssrmatching module between code and grammar rules.
Fixes #7857.
Diffstat (limited to 'plugins/ssrmatching')
-rw-r--r--plugins/ssrmatching/g_ssrmatching.ml4101
-rw-r--r--plugins/ssrmatching/g_ssrmatching.mli17
-rw-r--r--plugins/ssrmatching/ssrmatching.ml (renamed from plugins/ssrmatching/ssrmatching.ml4)105
-rw-r--r--plugins/ssrmatching/ssrmatching.mli34
-rw-r--r--plugins/ssrmatching/ssrmatching_plugin.mlpack1
5 files changed, 159 insertions, 99 deletions
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