diff options
| -rw-r--r-- | dev/shim/dune | 8 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 75 | ||||
| -rw-r--r-- | test-suite/misc/universes/dune | 3 |
3 files changed, 51 insertions, 35 deletions
diff --git a/dev/shim/dune b/dev/shim/dune index e307848292..84b2e642e8 100644 --- a/dev/shim/dune +++ b/dev/shim/dune @@ -4,7 +4,7 @@ %{bin:coqtop} %{project_root}/theories/Init/Prelude.vo) (action - (with-outputs-to coqtop-prelude + (with-stdout-to coqtop-prelude (progn (echo "#!/usr/bin/env bash\n") (bash "echo \"$(pwd)/%{bin:coqtop} -coqlib $(pwd)/%{project_root}\" \\$@") @@ -16,7 +16,7 @@ %{bin:coqc} %{project_root}/theories/Init/Prelude.vo) (action - (with-outputs-to coqc-prelude + (with-stdout-to coqc-prelude (progn (echo "#!/usr/bin/env bash\n") (bash "echo \"$(pwd)/%{bin:coqc} -coqlib $(pwd)/%{project_root}\" \\$@") @@ -29,7 +29,7 @@ %{lib:coq.kernel:../../stublibs/dllbyterun_stubs.so} %{project_root}/theories/Init/Prelude.vo) (action - (with-outputs-to %{targets} + (with-stdout-to %{targets} (progn (echo "#!/usr/bin/env bash\n") (bash "echo \"$(pwd)/%{bin:coqtop.byte} -coqlib $(pwd)/%{project_root}\" \\$@") @@ -45,7 +45,7 @@ %{project_root}/coqide-server.install %{project_root}/coqide.install) (action - (with-outputs-to coqide-prelude + (with-stdout-to coqide-prelude (progn (echo "#!/usr/bin/env bash\n") (bash "echo \"$(pwd)/%{bin:coqide} -coqlib $(pwd)/%{project_root}\" \\$@") diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 858a75698a..c09250ade5 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 () ;; @@ -969,14 +988,17 @@ ARGUMENT EXTEND ssrintrosarg TYPED AS (tactic * ssrintros) | [ "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 @@ -1701,16 +1723,6 @@ let _ = add_internal_name (is_tagged perm_tag) 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 +1730,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 +1813,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 +1860,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 = diff --git a/test-suite/misc/universes/dune b/test-suite/misc/universes/dune index 0772f95604..c0d925deb5 100644 --- a/test-suite/misc/universes/dune +++ b/test-suite/misc/universes/dune @@ -1,8 +1,9 @@ (rule (targets all_stdlib.v) (deps + build_all_stdlib.sh (source_tree ../../../theories) (source_tree ../../../plugins)) (action - (with-outputs-to all_stdlib.v + (with-stdout-to all_stdlib.v (bash "./build_all_stdlib.sh")))) |