diff options
Diffstat (limited to 'contrib/extraction/g_extraction.ml4')
-rw-r--r-- | contrib/extraction/g_extraction.ml4 | 119 |
1 files changed, 119 insertions, 0 deletions
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4 new file mode 100644 index 00000000..33a6117d --- /dev/null +++ b/contrib/extraction/g_extraction.ml4 @@ -0,0 +1,119 @@ +(************************************************************************) +(* 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 () ++ + (if !Options.v7 && not (Options.do_translate()) then qs s + else Pptacticnew.qsnew s) + +ARGUMENT EXTEND mlname + TYPED AS string + PRINTED BY pr_mlname +| [ preident(id) ] -> [ id ] +| [ string(s) ] -> [ s ] +END + +open Table +open Extract_env + +VERNAC ARGUMENT EXTEND language +| [ "Ocaml" ] -> [ Ocaml ] +| [ "Haskell" ] -> [ Haskell ] +| [ "Scheme" ] -> [ Scheme ] +| [ "Toplevel" ] -> [ Toplevel ] +END + +(* Temporary for translator *) +if !Options.v7 then + let pr_language _ _ = function + | Ocaml -> str " Ocaml" + | Haskell -> str " Haskell" + | Scheme -> str " Scheme" + | Toplevel -> str " Toplevel" + in + let globwit_language = Obj.magic rawwit_language in + let wit_language = Obj.magic rawwit_language in + Pptactic.declare_extra_genarg_pprule true + (rawwit_language, pr_language) + (globwit_language, pr_language) + (wit_language, pr_language); + +(* Extraction commands *) + +VERNAC COMMAND EXTEND Extraction +(* Extraction in the Coq toplevel *) +| [ "Extraction" global(x) ] -> [ extraction x ] +| [ "Recursive" "Extraction" ne_global_list(l) ] -> [ extraction_rec l ] + +(* Monolithic extraction to a file *) +| [ "Extraction" string(f) ne_global_list(l) ] + -> [ extraction_file 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 + +(* 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 |