diff options
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/g_ssrmatching.ml4 | 101 | ||||
| -rw-r--r-- | plugins/ssrmatching/g_ssrmatching.mli | 17 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml (renamed from plugins/ssrmatching/ssrmatching.ml4) | 105 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 34 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching_plugin.mlpack | 1 |
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 |