diff options
author | 2010-07-21 09:46:51 +0200 | |
---|---|---|
committer | 2010-07-21 09:46:51 +0200 | |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /contrib/extraction/g_extraction.ml4 | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'contrib/extraction/g_extraction.ml4')
-rw-r--r-- | contrib/extraction/g_extraction.ml4 | 123 |
1 files changed, 0 insertions, 123 deletions
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4 deleted file mode 100644 index 345cb307..00000000 --- a/contrib/extraction/g_extraction.ml4 +++ /dev/null @@ -1,123 +0,0 @@ -(************************************************************************) -(* 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 |