From ab85be0ab41251ece3b583c3ff38f08f546f6414 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 8 Aug 2013 18:52:29 +0000 Subject: Vernac classification streamlined (handles VERNAC EXTEND) The warning output by vernacextend when the classifier is missing is the documentation of this commit: Warning: Vernac entry "Foo" misses a classifier. A classifier is a function that returns an expression of type vernac_classification (see Vernacexpr). You can: - Use '... EXTEND Foo CLASSIFIED AS QUERY ...' if the new vernacular command does not alter the system state; - Use '... EXTEND Foo CLASSIFIED AS SIDEFF ...' if the new vernacular command alters the system state but not the parser nor it starts a proof or ends one; - Use '... EXTEND Foo CLASSIFIED BY f ...' to specify a global function f. The function f will be called passing "Foo" as the only argument; - Add a specific classifier in each clause using the syntax: '[...] => [ f ] -> [...]'. Specific classifiers have precedence over global classifiers. Only one classifier is called. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16680 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/decl_mode/g_decl_mode.ml4 | 20 +++++++++----------- plugins/extraction/g_extraction.ml4 | 32 ++++++++++++++++---------------- plugins/firstorder/g_ground.ml4 | 4 ++-- plugins/funind/g_indfun.ml4 | 36 +++++++++++++++++++++++------------- plugins/setoid_ring/newring.ml4 | 4 ++-- plugins/xml/xmlentries.ml4 | 2 +- 6 files changed, 53 insertions(+), 45 deletions(-) (limited to 'plugins') diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 072737dab..f79f71712 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -16,6 +16,7 @@ open Tok open Decl_expr open Names open Pcoq +open Vernacexpr open Pcoq.Constr open Pcoq.Tactic @@ -114,11 +115,13 @@ let wit_proof_instr = let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr +let classify_proof_instr _ = VtProofStep, VtLater + (* We use the VERNAC EXTEND facility with a custom non-terminal to populate [proof_mode] with a new toplevel interpreter. The "-" indicates that the rule does not start with a distinguished string. *) -VERNAC proof_mode EXTEND ProofInstr +VERNAC proof_mode EXTEND ProofInstr CLASSIFIED BY classify_proof_instr [ - proof_instr(instr) ] -> [ vernac_proof_instr instr ] END @@ -163,10 +166,13 @@ let _ = } (* Two new vernacular commands *) -VERNAC COMMAND EXTEND DeclProof +let classify_decl _ = VtProofStep, VtNow + +VERNAC COMMAND EXTEND DeclProof CLASSIFIED BY classify_decl [ "proof" ] -> [ vernac_decl_proof () ] END -VERNAC COMMAND EXTEND DeclReturn +VERNAC COMMAND EXTEND DeclReturn CLASSIFIED BY classify_decl + [ "return" ] -> [ vernac_return () ] END @@ -396,11 +402,3 @@ GLOBAL: proof_instr; [[ e=emphasis;i=bare_proof_instr;"." -> {emph=e;instr=i}]] ; END;; - -open Vernacexpr - -let () = - Vernac_classifier.declare_vernac_classifier "decl_mode" (function - | VernacExtend (("DeclProof"|"DeclReturn"), _) -> VtProofStep, VtNow - | VernacExtend ("ProofInstr", _) -> VtProofStep, VtLater - | _ -> VtUnknown, VtNow) diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 5295e2cf9..b0b8217b6 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -51,7 +51,7 @@ END (* Extraction commands *) -VERNAC COMMAND EXTEND Extraction +VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY (* Extraction in the Coq toplevel *) | [ "Extraction" global(x) ] -> [ simple_extraction x ] | [ "Recursive" "Extraction" ne_global_list(l) ] -> [ full_extraction None l ] @@ -61,85 +61,85 @@ VERNAC COMMAND EXTEND Extraction -> [ full_extraction (Some f) l ] END -VERNAC COMMAND EXTEND SeparateExtraction +VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY (* Same, with content splitted in several files *) | [ "Separate" "Extraction" ne_global_list(l) ] -> [ separate_extraction l ] END (* Modular extraction (one Coq library = one ML module) *) -VERNAC COMMAND EXTEND ExtractionLibrary +VERNAC COMMAND EXTEND ExtractionLibrary CLASSIFIED AS QUERY | [ "Extraction" "Library" ident(m) ] -> [ extraction_library false m ] END -VERNAC COMMAND EXTEND RecursiveExtractionLibrary +VERNAC COMMAND EXTEND RecursiveExtractionLibrary CLASSIFIED AS QUERY | [ "Recursive" "Extraction" "Library" ident(m) ] -> [ extraction_library true m ] END (* Target Language *) -VERNAC COMMAND EXTEND ExtractionLanguage +VERNAC COMMAND EXTEND ExtractionLanguage CLASSIFIED AS SIDEFF | [ "Extraction" "Language" language(l) ] -> [ extraction_language l ] END -VERNAC COMMAND EXTEND ExtractionInline +VERNAC COMMAND EXTEND ExtractionInline CLASSIFIED AS SIDEFF (* Custom inlining directives *) | [ "Extraction" "Inline" ne_global_list(l) ] -> [ extraction_inline true l ] END -VERNAC COMMAND EXTEND ExtractionNoInline +VERNAC COMMAND EXTEND ExtractionNoInline CLASSIFIED AS SIDEFF | [ "Extraction" "NoInline" ne_global_list(l) ] -> [ extraction_inline false l ] END -VERNAC COMMAND EXTEND PrintExtractionInline +VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY | [ "Print" "Extraction" "Inline" ] -> [ msg_info (print_extraction_inline ()) ] END -VERNAC COMMAND EXTEND ResetExtractionInline +VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF | [ "Reset" "Extraction" "Inline" ] -> [ reset_extraction_inline () ] END -VERNAC COMMAND EXTEND ExtractionImplicit +VERNAC COMMAND EXTEND ExtractionImplicit CLASSIFIED AS SIDEFF (* 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 +VERNAC COMMAND EXTEND ExtractionBlacklist CLASSIFIED AS SIDEFF (* Force Extraction to not use some filenames *) | [ "Extraction" "Blacklist" ne_ident_list(l) ] -> [ extraction_blacklist l ] END -VERNAC COMMAND EXTEND PrintExtractionBlacklist +VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY | [ "Print" "Extraction" "Blacklist" ] -> [ msg_info (print_extraction_blacklist ()) ] END -VERNAC COMMAND EXTEND ResetExtractionBlacklist +VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF | [ "Reset" "Extraction" "Blacklist" ] -> [ reset_extraction_blacklist () ] END (* Overriding of a Coq object by an ML one *) -VERNAC COMMAND EXTEND ExtractionConstant +VERNAC COMMAND EXTEND ExtractionConstant CLASSIFIED AS SIDEFF | [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ] -> [ extract_constant_inline false x idl y ] END -VERNAC COMMAND EXTEND ExtractionInlinedConstant +VERNAC COMMAND EXTEND ExtractionInlinedConstant CLASSIFIED AS SIDEFF | [ "Extract" "Inlined" "Constant" global(x) "=>" mlname(y) ] -> [ extract_constant_inline true x [] y ] END -VERNAC COMMAND EXTEND ExtractionInductive +VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF | [ "Extract" "Inductive" global(x) "=>" mlname(id) "[" mlname_list(idl) "]" string_opt(o) ] -> [ extract_inductive x id idl o ] diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index bdea8b1a9..84060dc9d 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -53,14 +53,14 @@ let _= let (set_default_solver, default_solver, print_default_solver) = Tactic_option.declare_tactic_option ~default:(<:tactic>) "Firstorder default solver" -VERNAC COMMAND EXTEND Firstorder_Set_Solver +VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [ set_default_solver (Locality.make_section_locality (Locality.LocalityFixme.consume ())) (Tacintern.glob_tactic t) ] END -VERNAC COMMAND EXTEND Firstorder_Print_Solver +VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY | [ "Print" "Firstorder" "Solver" ] -> [ Pp.msg_info (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ] diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 7ab9488de..7e229fbd2 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -155,12 +155,21 @@ type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexp let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) = Genarg.create_arg None "function_rec_definition_loc" -VERNAC COMMAND EXTEND Function - ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] -> - [ - do_generate_principle false (List.map snd recsl); - ] +(* TASSI: n'importe quoi ! *) +VERNAC COMMAND EXTEND Function + ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] + => [ let hard = List.exists (function + | _,((_,(_,(CMeasureRec _|CWfRec _)),_,_,_),_) -> true + | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in + match + Vernac_classifier.classify_vernac + (Vernacexpr.VernacFixpoint(None, List.map snd recsl)) + with + | Vernacexpr.VtSideff ids, _ when hard -> + Vernacexpr.VtStartProof ("Classic", ids), Vernacexpr.VtLater + | x -> x ] + -> [ do_generate_principle false (List.map snd recsl) ] END let pr_fun_scheme_arg (princ_name,fun_name,s) = @@ -191,7 +200,9 @@ let warning_error names e = VERNAC COMMAND EXTEND NewFunctionalScheme - ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] -> + ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] + => [ Vernacexpr.VtSideff(List.map pi1 fas), Vernacexpr.VtLater ] + -> [ begin try @@ -225,14 +236,13 @@ END (***** debug only ***) VERNAC COMMAND EXTEND NewFunctionalCase - ["Functional" "Case" fun_scheme_arg(fas) ] -> - [ - Functional_principles_types.build_case_scheme fas - ] + ["Functional" "Case" fun_scheme_arg(fas) ] + => [ Vernacexpr.VtSideff[pi1 fas], Vernacexpr.VtLater ] + -> [ Functional_principles_types.build_case_scheme fas ] END (***** debug only ***) -VERNAC COMMAND EXTEND GenerateGraph +VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY ["Generate" "graph" "for" reference(c)] -> [ make_graph (Nametab.global c) ] END @@ -449,11 +459,11 @@ TACTIC EXTEND poseq [ poseq x c ] END -VERNAC COMMAND EXTEND Showindinfo +VERNAC COMMAND EXTEND Showindinfo CLASSIFIED AS QUERY [ "showindinfo" ident(x) ] -> [ Merge.showind x ] END -VERNAC COMMAND EXTEND MergeFunind +VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")" "with" "(" ident(id2) ne_ident_list(cl2) ")" "using" ident(id) ] -> [ diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index be661587a..7e4fc7277 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -768,7 +768,7 @@ let process_ring_mods l = let k = match !kind with Some k -> ic_coeff_spec k | None -> Abstract in (k, !set, !cst_tac, !pre, !post, !power, !sign, !div) -VERNAC COMMAND EXTEND AddSetoidRing +VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] -> [ let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in add_theory id (ic t) set k cst (pre,post) power sign div] @@ -1095,7 +1095,7 @@ let process_field_mods l = let k = match !kind with Some k -> ic_coeff_spec k | None -> Abstract in (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div) -VERNAC COMMAND EXTEND AddSetoidField +VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF | [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> [ let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div] diff --git a/plugins/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4 index 5ca6e155b..8cf3a0bdc 100644 --- a/plugins/xml/xmlentries.ml4 +++ b/plugins/xml/xmlentries.ml4 @@ -25,7 +25,7 @@ END (* Print XML and Show XML *) -VERNAC COMMAND EXTEND Xml +VERNAC COMMAND EXTEND Xml CLASSIFIED AS QUERY | [ "Print" "XML" filename(fn) global(qid) ] -> [ Xmlcommand.print_ref qid fn ] | [ "Show" "XML" filename(fn) "Proof" ] -> [ Xmlcommand.show fn ] -- cgit v1.2.3