diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-20 01:22:58 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-20 01:22:58 +0000 |
commit | 7d220f8b61649646692983872626d6a8042446a9 (patch) | |
tree | fefceb2c59cf155c55fffa25ad08bec629de523e /plugins/extraction/g_extraction.ml4 | |
parent | ad1fea78e3c23c903b2256d614756012d5f05d87 (diff) |
Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/g_extraction.ml4')
-rw-r--r-- | plugins/extraction/g_extraction.ml4 | 123 |
1 files changed, 123 insertions, 0 deletions
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 new file mode 100644 index 000000000..2b561616b --- /dev/null +++ b/plugins/extraction/g_extraction.ml4 @@ -0,0 +1,123 @@ +(************************************************************************) +(* 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 + +let pr_mlname _ _ _ s = spc () ++ qs s + +ARGUMENT EXTEND mlname + TYPED AS string + PRINTED BY pr_mlname +| [ preident(id) ] -> [ id ] +| [ string(s) ] -> [ s ] +END + +open Table +open Extract_env + +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 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) "]" ] + -> [ extract_inductive x (id,idl) ] +END |