diff options
Diffstat (limited to 'plugins/extraction/g_extraction.ml4')
| -rw-r--r-- | plugins/extraction/g_extraction.ml4 | 38 |
1 files changed, 27 insertions, 11 deletions
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 19fda4ae..93909f3e 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -1,24 +1,24 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) +open Pcoq.Prim DECLARE PLUGIN "extraction_plugin" (* ML names *) +open Ltac_plugin open Genarg open Stdarg -open Constrarg -open Pcoq.Prim open Pp open Names -open Nameops open Table open Extract_env @@ -33,7 +33,7 @@ END let pr_int_or_id _ _ _ = function | ArgInt i -> int i - | ArgId id -> pr_id id + | ArgId id -> Id.print id ARGUMENT EXTEND int_or_id PRINTED BY pr_int_or_id @@ -42,14 +42,20 @@ ARGUMENT EXTEND int_or_id END let pr_language = function - | Ocaml -> str "Ocaml" + | 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" ] -> [ Ocaml ] +| [ "Ocaml" ] -> [ let _ = warn_deprecated_ocaml_spelling () in Ocaml ] +| [ "OCaml" ] -> [ Ocaml ] | [ "Haskell" ] -> [ Haskell ] | [ "Scheme" ] -> [ Scheme ] | [ "JSON" ] -> [ JSON ] @@ -65,6 +71,10 @@ VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY (* 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 @@ -150,3 +160,9 @@ VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF 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 |