diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 92 |
1 files changed, 45 insertions, 47 deletions
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 858a75698a..962730d8dc 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -68,6 +68,25 @@ DECLARE PLUGIN "ssreflect_plugin" { +let ssrtac_name name = { + mltac_plugin = "ssreflect_plugin"; + mltac_tactic = "ssr" ^ name; +} + +let ssrtac_entry name = { + mltac_name = ssrtac_name name; + mltac_index = 0; +} + +let register_ssrtac name f = + Tacenv.register_ml_tactic (ssrtac_name name) [|f|] + +let cast_arg wit v = Taccoerce.Value.cast (Genarg.topwit wit) v + +} + +{ + (* 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 () ;; @@ -366,7 +385,6 @@ open Pltac ARGUMENT EXTEND ssrindex PRINTED BY { pr_ssrindex } INTERPRETED BY { interp_index } -| [ int_or_var(i) ] -> { mk_index ~loc i } END @@ -504,7 +522,6 @@ ARGUMENT EXTEND ssrterm GLOBALIZED BY { glob_ssrterm } SUBSTITUTED BY { subst_ssrterm } RAW_PRINTED BY { pr_ssrterm } GLOB_PRINTED BY { pr_ssrterm } -| [ "YouShouldNotTypeThis" constr(c) ] -> { mk_lterm c } END GRAMMAR EXTEND Gram @@ -551,7 +568,6 @@ let pr_ssrbwdview _ _ _ = pr_view ARGUMENT EXTEND ssrbwdview TYPED AS ssrterm list PRINTED BY { pr_ssrbwdview } -| [ "YouShouldNotTypeThis" ] -> { [] } END (* Pcoq *) @@ -575,7 +591,6 @@ let pr_ssrfwdview _ _ _ = pr_view2 ARGUMENT EXTEND ssrfwdview TYPED AS ast_closure_term list PRINTED BY { pr_ssrfwdview } -| [ "YouShouldNotTypeThis" ] -> { [] } END (* Pcoq *) @@ -743,7 +758,6 @@ let test_ident_no_do = } ARGUMENT EXTEND ident_no_do PRINTED BY { fun _ _ _ -> Names.Id.print } -| [ "YouShouldNotTypeThis" ident(id) ] -> { id } END @@ -838,7 +852,6 @@ let _test_nobinder = Pcoq.Entry.of_parser "test_nobinder" (reject_binder false 0 } ARGUMENT EXTEND ssrcpat TYPED AS ssripatrep PRINTED BY { pr_ssripat } - | [ "YouShouldNotTypeThis" ssriorpat(x) ] -> { IPatCase(Regular x) } END (* Pcoq *) @@ -966,17 +979,19 @@ let pr_ssrintrosarg env sigma _ _ prt (tac, ipats) = ARGUMENT EXTEND ssrintrosarg TYPED AS (tactic * ssrintros) PRINTED BY { pr_ssrintrosarg env sigma } -| [ "YouShouldNotTypeThis" ssrtacarg(arg) ssrintros_ne(ipats) ] -> { arg, ipats } -END - -TACTIC EXTEND ssrtclintros -| [ "YouShouldNotTypeThis" ssrintrosarg(arg) ] -> - { let tac, intros = arg in - ssrevaltac ist tac <*> tclIPATssr intros } END { +let () = register_ssrtac "tclintros" begin fun args ist -> match args with +| [arg] -> + let arg = cast_arg wit_ssrintrosarg arg in + let tac, intros = arg in + ssrevaltac ist tac <*> tclIPATssr intros +| _ -> assert false +end + + (** Defined identifier *) let pr_ssrfwdid id = pr_spc () ++ pr_id id @@ -1689,28 +1704,10 @@ let _ = add_internal_name (is_tagged perm_tag) (** Tactical extensions. *) -(* The TACTIC EXTEND facility can't be used for defining new user *) -(* tacticals, because: *) -(* - the concrete syntax must start with a fixed string *) -(* We use the following workaround: *) -(* - We use the (unparsable) "YouShouldNotTypeThis" token for tacticals that *) -(* don't start with a token, then redefine the grammar and *) -(* printer using GEXTEND and set_pr_ssrtac, respectively. *) - { type ssrargfmt = ArgSsr of string | ArgSep of string -let ssrtac_name name = { - mltac_plugin = "ssreflect_plugin"; - mltac_tactic = "ssr" ^ name; -} - -let ssrtac_entry name n = { - mltac_name = ssrtac_name name; - mltac_index = n; -} - let set_pr_ssrtac name prec afmt = (* FIXME *) () (* let fmt = List.map (function | ArgSep s -> Egramml.GramTerminal s @@ -1718,8 +1715,7 @@ let set_pr_ssrtac name prec afmt = (* FIXME *) () (* | ArgCoq at -> Egramml.GramTerminal "COQ_ARG") afmt in let tacname = ssrtac_name name in () *) -let ssrtac_atom ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name 0, args)) -let ssrtac_expr ?loc name args = ssrtac_atom ?loc name args +let ssrtac_expr ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name, args)) let tclintros_expr ?loc tac ipats = let args = [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in @@ -1802,15 +1798,15 @@ END (** The "do" tactical. ********************************************************) -(* -type ssrdoarg = ((ssrindex * ssrmmod) * ssrhint) * ssrclauses -*) -TACTIC EXTEND ssrtcldo -| [ "YouShouldNotTypeThis" "do" ssrdoarg(arg) ] -> { V82.tactic (ssrdotac ist arg) } -END - { +let () = register_ssrtac "tcldo" begin fun args ist -> match args with +| [arg] -> + let arg = cast_arg wit_ssrdoarg arg in + V82.tactic (ssrdotac ist arg) +| _ -> assert false +end + let _ = set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"] let ssrdotac_expr ?loc n m tac clauses = @@ -1849,13 +1845,17 @@ let pr_ssrseqdir _ _ _ = function ARGUMENT EXTEND ssrseqdir TYPED AS ssrdir PRINTED BY { pr_ssrseqdir } END -TACTIC EXTEND ssrtclseq -| [ "YouShouldNotTypeThis" ssrtclarg(tac) ssrseqdir(dir) ssrseqarg(arg) ] -> - { V82.tactic (tclSEQAT ist tac dir arg) } -END - { +let () = register_ssrtac "tclseq" begin fun args ist -> match args with +| [tac; dir; arg] -> + let tac = cast_arg wit_ssrtclarg tac in + let dir = cast_arg wit_ssrseqdir dir in + let arg = cast_arg wit_ssrseqarg arg in + V82.tactic (tclSEQAT ist tac dir arg) +| _ -> assert false +end + let _ = set_pr_ssrtac "tclseq" 5 [ArgSsr "tclarg"; ArgSsr "seqdir"; ArgSsr "seqarg"] let tclseq_expr ?loc tac dir arg = @@ -2228,8 +2228,6 @@ END (** The "congr" tactic *) -(* type ssrcongrarg = open_constr * (int * constr) *) - { let pr_ssrcongrarg _ _ _ ((n, f), dgens) = |