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/extraction/g_extraction.ml4 | 1 - 1 file changed, 1 deletion(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 93909f3e64..370d3c248f 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -15,7 +15,6 @@ DECLARE PLUGIN "extraction_plugin" (* ML names *) open Ltac_plugin -open Genarg open Stdarg open Pp open Names -- 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/extraction/g_extraction.ml4 | 167 -------------------------------- plugins/extraction/g_extraction.mlg | 183 ++++++++++++++++++++++++++++++++++++ 2 files changed, 183 insertions(+), 167 deletions(-) delete mode 100644 plugins/extraction/g_extraction.ml4 create mode 100644 plugins/extraction/g_extraction.mlg (limited to 'plugins/extraction') diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 deleted file mode 100644 index 370d3c248f..0000000000 --- a/plugins/extraction/g_extraction.ml4 +++ /dev/null @@ -1,167 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* [ id ] -| [ string(s) ] -> [ s ] -END - -let pr_int_or_id _ _ _ = function - | ArgInt i -> int i - | ArgId id -> Id.print id - -ARGUMENT EXTEND int_or_id - PRINTED BY pr_int_or_id -| [ preident(id) ] -> [ ArgId (Id.of_string id) ] -| [ integer(i) ] -> [ ArgInt i ] -END - -let pr_language = function - | Ocaml -> str "OCaml" - | Haskell -> str "Haskell" - | Scheme -> str "Scheme" - | JSON -> str "JSON" - -let warn_deprecated_ocaml_spelling = - CWarnings.create ~name:"deprecated-ocaml-spelling" ~category:"deprecated" - (fun () -> - strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\".")) - -VERNAC ARGUMENT EXTEND language -PRINTED BY pr_language -| [ "Ocaml" ] -> [ let _ = warn_deprecated_ocaml_spelling () in Ocaml ] -| [ "OCaml" ] -> [ Ocaml ] -| [ "Haskell" ] -> [ Haskell ] -| [ "Scheme" ] -> [ Scheme ] -| [ "JSON" ] -> [ JSON ] -END - -(* Extraction commands *) - -VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY -(* Extraction in the Coq toplevel *) -| [ "Extraction" global(x) ] -> [ simple_extraction x ] -| [ "Recursive" "Extraction" ne_global_list(l) ] -> [ full_extraction None l ] - -(* Monolithic extraction to a file *) -| [ "Extraction" string(f) ne_global_list(l) ] - -> [ full_extraction (Some f) l ] - -(* Extraction to a temporary file and OCaml compilation *) -| [ "Extraction" "TestCompile" ne_global_list(l) ] - -> [ extract_and_compile l ] -END - -VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY -(* Same, with content splitted in several files *) -| [ "Separate" "Extraction" ne_global_list(l) ] - -> [ separate_extraction l ] -END - -(* Modular extraction (one Coq library = one ML module) *) -VERNAC COMMAND EXTEND ExtractionLibrary CLASSIFIED AS QUERY -| [ "Extraction" "Library" ident(m) ] - -> [ extraction_library false m ] -END - -VERNAC COMMAND EXTEND RecursiveExtractionLibrary CLASSIFIED AS QUERY -| [ "Recursive" "Extraction" "Library" ident(m) ] - -> [ extraction_library true m ] -END - -(* Target Language *) -VERNAC COMMAND EXTEND ExtractionLanguage CLASSIFIED AS SIDEFF -| [ "Extraction" "Language" language(l) ] - -> [ extraction_language l ] -END - -VERNAC COMMAND EXTEND ExtractionInline CLASSIFIED AS SIDEFF -(* Custom inlining directives *) -| [ "Extraction" "Inline" ne_global_list(l) ] - -> [ extraction_inline true l ] -END - -VERNAC COMMAND EXTEND ExtractionNoInline CLASSIFIED AS SIDEFF -| [ "Extraction" "NoInline" ne_global_list(l) ] - -> [ extraction_inline false l ] -END - -VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY -| [ "Print" "Extraction" "Inline" ] - -> [Feedback. msg_info (print_extraction_inline ()) ] -END - -VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF -| [ "Reset" "Extraction" "Inline" ] - -> [ reset_extraction_inline () ] -END - -VERNAC COMMAND EXTEND ExtractionImplicit CLASSIFIED AS SIDEFF -(* Custom implicit arguments of some csts/inds/constructors *) -| [ "Extraction" "Implicit" global(r) "[" int_or_id_list(l) "]" ] - -> [ extraction_implicit r l ] -END - -VERNAC COMMAND EXTEND ExtractionBlacklist CLASSIFIED AS SIDEFF -(* Force Extraction to not use some filenames *) -| [ "Extraction" "Blacklist" ne_ident_list(l) ] - -> [ extraction_blacklist l ] -END - -VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY -| [ "Print" "Extraction" "Blacklist" ] - -> [ Feedback.msg_info (print_extraction_blacklist ()) ] -END - -VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF -| [ "Reset" "Extraction" "Blacklist" ] - -> [ reset_extraction_blacklist () ] -END - - -(* Overriding of a Coq object by an ML one *) -VERNAC COMMAND EXTEND ExtractionConstant CLASSIFIED AS SIDEFF -| [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ] - -> [ extract_constant_inline false x idl y ] -END - -VERNAC COMMAND EXTEND ExtractionInlinedConstant CLASSIFIED AS SIDEFF -| [ "Extract" "Inlined" "Constant" global(x) "=>" mlname(y) ] - -> [ extract_constant_inline true x [] y ] -END - -VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF -| [ "Extract" "Inductive" global(x) "=>" - mlname(id) "[" mlname_list(idl) "]" string_opt(o) ] - -> [ extract_inductive x id idl o ] -END -(* Show the extraction of the current proof *) - -VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY -| [ "Show" "Extraction" ] - -> [ show_extraction () ] -END diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg new file mode 100644 index 0000000000..1445dffefa --- /dev/null +++ b/plugins/extraction/g_extraction.mlg @@ -0,0 +1,183 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* { id } +| [ string(s) ] -> { s } +END + +{ + +let pr_int_or_id _ _ _ = function + | ArgInt i -> int i + | ArgId id -> Id.print id + +} + +ARGUMENT EXTEND int_or_id + PRINTED BY { pr_int_or_id } +| [ preident(id) ] -> { ArgId (Id.of_string id) } +| [ integer(i) ] -> { ArgInt i } +END + +{ + +let pr_language = function + | Ocaml -> str "OCaml" + | Haskell -> str "Haskell" + | Scheme -> str "Scheme" + | JSON -> str "JSON" + +let warn_deprecated_ocaml_spelling = + CWarnings.create ~name:"deprecated-ocaml-spelling" ~category:"deprecated" + (fun () -> + strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\".")) + +} + +VERNAC ARGUMENT EXTEND language +PRINTED BY { pr_language } +| [ "Ocaml" ] -> { let _ = warn_deprecated_ocaml_spelling () in Ocaml } +| [ "OCaml" ] -> { Ocaml } +| [ "Haskell" ] -> { Haskell } +| [ "Scheme" ] -> { Scheme } +| [ "JSON" ] -> { JSON } +END + +(* Extraction commands *) + +VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY +(* Extraction in the Coq toplevel *) +| [ "Extraction" global(x) ] -> { simple_extraction x } +| [ "Recursive" "Extraction" ne_global_list(l) ] -> { full_extraction None l } + +(* Monolithic extraction to a file *) +| [ "Extraction" string(f) ne_global_list(l) ] + -> { full_extraction (Some f) l } + +(* Extraction to a temporary file and OCaml compilation *) +| [ "Extraction" "TestCompile" ne_global_list(l) ] + -> { extract_and_compile l } +END + +VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY +(* Same, with content splitted in several files *) +| [ "Separate" "Extraction" ne_global_list(l) ] + -> { separate_extraction l } +END + +(* Modular extraction (one Coq library = one ML module) *) +VERNAC COMMAND EXTEND ExtractionLibrary CLASSIFIED AS QUERY +| [ "Extraction" "Library" ident(m) ] + -> { extraction_library false m } +END + +VERNAC COMMAND EXTEND RecursiveExtractionLibrary CLASSIFIED AS QUERY +| [ "Recursive" "Extraction" "Library" ident(m) ] + -> { extraction_library true m } +END + +(* Target Language *) +VERNAC COMMAND EXTEND ExtractionLanguage CLASSIFIED AS SIDEFF +| [ "Extraction" "Language" language(l) ] + -> { extraction_language l } +END + +VERNAC COMMAND EXTEND ExtractionInline CLASSIFIED AS SIDEFF +(* Custom inlining directives *) +| [ "Extraction" "Inline" ne_global_list(l) ] + -> { extraction_inline true l } +END + +VERNAC COMMAND EXTEND ExtractionNoInline CLASSIFIED AS SIDEFF +| [ "Extraction" "NoInline" ne_global_list(l) ] + -> { extraction_inline false l } +END + +VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY +| [ "Print" "Extraction" "Inline" ] + -> {Feedback. msg_info (print_extraction_inline ()) } +END + +VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF +| [ "Reset" "Extraction" "Inline" ] + -> { reset_extraction_inline () } +END + +VERNAC COMMAND EXTEND ExtractionImplicit CLASSIFIED AS SIDEFF +(* Custom implicit arguments of some csts/inds/constructors *) +| [ "Extraction" "Implicit" global(r) "[" int_or_id_list(l) "]" ] + -> { extraction_implicit r l } +END + +VERNAC COMMAND EXTEND ExtractionBlacklist CLASSIFIED AS SIDEFF +(* Force Extraction to not use some filenames *) +| [ "Extraction" "Blacklist" ne_ident_list(l) ] + -> { extraction_blacklist l } +END + +VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY +| [ "Print" "Extraction" "Blacklist" ] + -> { Feedback.msg_info (print_extraction_blacklist ()) } +END + +VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF +| [ "Reset" "Extraction" "Blacklist" ] + -> { reset_extraction_blacklist () } +END + + +(* Overriding of a Coq object by an ML one *) +VERNAC COMMAND EXTEND ExtractionConstant CLASSIFIED AS SIDEFF +| [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ] + -> { extract_constant_inline false x idl y } +END + +VERNAC COMMAND EXTEND ExtractionInlinedConstant CLASSIFIED AS SIDEFF +| [ "Extract" "Inlined" "Constant" global(x) "=>" mlname(y) ] + -> { extract_constant_inline true x [] y } +END + +VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF +| [ "Extract" "Inductive" global(x) "=>" + mlname(id) "[" mlname_list(idl) "]" string_opt(o) ] + -> { extract_inductive x id idl o } +END +(* Show the extraction of the current proof *) + +VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY +| [ "Show" "Extraction" ] + -> { show_extraction () } +END -- cgit v1.2.3