diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/extraction/g_extraction.ml4 | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/extraction/g_extraction.ml4')
-rw-r--r-- | plugins/extraction/g_extraction.ml4 | 142 |
1 files changed, 142 insertions, 0 deletions
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 new file mode 100644 index 00000000..18828241 --- /dev/null +++ b/plugins/extraction/g_extraction.ml4 @@ -0,0 +1,142 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(* ML names *) + +open Vernacexpr +open Pcoq +open Genarg +open Pp +open Names +open Nameops +open Table +open Extract_env + +let pr_mlname _ _ _ s = spc () ++ qs s + +ARGUMENT EXTEND mlname + TYPED AS string + PRINTED BY pr_mlname +| [ preident(id) ] -> [ id ] +| [ string(s) ] -> [ s ] +END + +let pr_int_or_id _ _ _ = function + | ArgInt i -> int i + | ArgId id -> pr_id id + +ARGUMENT EXTEND int_or_id + TYPED AS 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" + +VERNAC ARGUMENT EXTEND language +PRINTED BY pr_language +| [ "Ocaml" ] -> [ Ocaml ] +| [ "Haskell" ] -> [ Haskell ] +| [ "Scheme" ] -> [ Scheme ] +END + +(* Extraction commands *) + +VERNAC COMMAND EXTEND Extraction +(* 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 ] +END + +(* Modular extraction (one Coq library = one ML module) *) +VERNAC COMMAND EXTEND ExtractionLibrary +| [ "Extraction" "Library" ident(m) ] + -> [ extraction_library false m ] +END + +VERNAC COMMAND EXTEND RecursiveExtractionLibrary +| [ "Recursive" "Extraction" "Library" ident(m) ] + -> [ extraction_library true m ] +END + +(* Target Language *) +VERNAC COMMAND EXTEND ExtractionLanguage +| [ "Extraction" "Language" language(l) ] + -> [ extraction_language l ] +END + +VERNAC COMMAND EXTEND ExtractionInline +(* Custom inlining directives *) +| [ "Extraction" "Inline" ne_global_list(l) ] + -> [ extraction_inline true l ] +END + +VERNAC COMMAND EXTEND ExtractionNoInline +| [ "Extraction" "NoInline" ne_global_list(l) ] + -> [ extraction_inline false l ] +END + +VERNAC COMMAND EXTEND PrintExtractionInline +| [ "Print" "Extraction" "Inline" ] + -> [ print_extraction_inline () ] +END + +VERNAC COMMAND EXTEND ResetExtractionInline +| [ "Reset" "Extraction" "Inline" ] + -> [ reset_extraction_inline () ] +END + +VERNAC COMMAND EXTEND ExtractionImplicit +(* 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 +(* Force Extraction to not use some filenames *) +| [ "Extraction" "Blacklist" ne_ident_list(l) ] + -> [ extraction_blacklist l ] +END + +VERNAC COMMAND EXTEND PrintExtractionBlacklist +| [ "Print" "Extraction" "Blacklist" ] + -> [ print_extraction_blacklist () ] +END + +VERNAC COMMAND EXTEND ResetExtractionBlacklist +| [ "Reset" "Extraction" "Blacklist" ] + -> [ reset_extraction_blacklist () ] +END + + +(* Overriding of a Coq object by an ML one *) +VERNAC COMMAND EXTEND ExtractionConstant +| [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ] + -> [ extract_constant_inline false x idl y ] +END + +VERNAC COMMAND EXTEND ExtractionInlinedConstant +| [ "Extract" "Inlined" "Constant" global(x) "=>" mlname(y) ] + -> [ extract_constant_inline true x [] y ] +END + +VERNAC COMMAND EXTEND ExtractionInductive +| [ "Extract" "Inductive" global(x) "=>" + mlname(id) "[" mlname_list(idl) "]" string_opt(o) ] + -> [ extract_inductive x id idl o ] +END |