diff options
Diffstat (limited to 'plugins/ssrmatching/g_ssrmatching.ml4')
-rw-r--r-- | plugins/ssrmatching/g_ssrmatching.ml4 | 101 |
1 files changed, 101 insertions, 0 deletions
diff --git a/plugins/ssrmatching/g_ssrmatching.ml4 b/plugins/ssrmatching/g_ssrmatching.ml4 new file mode 100644 index 00000000..746c368a --- /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 ;; |