From dba567555fed9c88887b463a975c3d7e0852ebd3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 11 Oct 2018 19:17:47 +0200 Subject: Plug ARGUMENT EXTEND into the argument extension API. --- plugins/ssrmatching/g_ssrmatching.ml4 | 1 - 1 file changed, 1 deletion(-) (limited to 'plugins/ssrmatching') diff --git a/plugins/ssrmatching/g_ssrmatching.ml4 b/plugins/ssrmatching/g_ssrmatching.ml4 index 746c368aa9..9e1f992f38 100644 --- a/plugins/ssrmatching/g_ssrmatching.ml4 +++ b/plugins/ssrmatching/g_ssrmatching.ml4 @@ -9,7 +9,6 @@ (************************************************************************) open Ltac_plugin -open Genarg open Pcoq open Pcoq.Constr open Ssrmatching -- cgit v1.2.3 From 4da233a9685cd193a84def037ec18a27c9225dce Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 12 Oct 2018 09:22:56 +0200 Subject: Port remaining EXTEND ml4 files to coqpp. Almost all of ml4 were removed in the process. The only remaining files are in the test-suite and probably need a bit of fiddling with coq_makefile, and there only two really remaning ml4 files containing code. --- plugins/ssrmatching/g_ssrmatching.ml4 | 100 ---------------------------- plugins/ssrmatching/g_ssrmatching.mlg | 120 ++++++++++++++++++++++++++++++++++ 2 files changed, 120 insertions(+), 100 deletions(-) delete mode 100644 plugins/ssrmatching/g_ssrmatching.ml4 create mode 100644 plugins/ssrmatching/g_ssrmatching.mlg (limited to 'plugins/ssrmatching') diff --git a/plugins/ssrmatching/g_ssrmatching.ml4 b/plugins/ssrmatching/g_ssrmatching.ml4 deleted file mode 100644 index 9e1f992f38..0000000000 --- a/plugins/ssrmatching/g_ssrmatching.ml4 +++ /dev/null @@ -1,100 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* [ 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.mlg b/plugins/ssrmatching/g_ssrmatching.mlg new file mode 100644 index 0000000000..3f0794fdd4 --- /dev/null +++ b/plugins/ssrmatching/g_ssrmatching.mlg @@ -0,0 +1,120 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* { 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 + +} + +GRAMMAR EXTEND 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 + +GRAMMAR EXTEND 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 ;; + +} -- cgit v1.2.3