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 --- grammar/tacextend.ml4 | 59 ++++++++++++++++------- grammar/vernacextend.ml4 | 92 +++++++++++++++++++++++++++++------- intf/vernacexpr.mli | 3 +- parsing/g_obligations.ml4 | 28 ++++++----- 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 +- tactics/class_tactics.ml4 | 6 +-- tactics/eauto.ml4 | 2 +- tactics/extratactics.ml4 | 42 ++++++++++------- tactics/rewrite.ml4 | 30 +++++++----- toplevel/stm.ml | 42 ++++++----------- toplevel/toplevel.mllib | 2 +- toplevel/vernac_classifier.ml | 94 +++++++++++++++++++++---------------- toplevel/vernac_classifier.mli | 14 ++++-- toplevel/whelp.ml4 | 7 +-- 19 files changed, 318 insertions(+), 201 deletions(-) diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 6e241cf87..5ea514174 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -36,16 +36,18 @@ let rec make_when loc = function <:expr< Genarg.argument_type_eq (Genarg.genarg_tag $lid:p$) $t$ && $l$ >> | _::l -> make_when loc l -let rec make_let e = function +let rec make_let raw e = function | [] -> <:expr< fun $lid:"ist"$ -> $e$ >> | GramNonTerminal(loc,t,_,Some p)::l -> let loc = of_coqloc loc in let p = Names.Id.to_string p in let loc = CompatLoc.merge loc (MLast.loc_of_expr e) in - let e = make_let e l in - let v = <:expr< Genarg.out_gen $make_topwit loc t$ $lid:p$ >> in + let e = make_let raw e l in + let v = + if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >> + else <:expr< Genarg.out_gen $make_topwit loc t$ $lid:p$ >> in <:expr< let $lid:p$ = $v$ in $e$ >> - | _::l -> make_let e l + | _::l -> make_let raw e l let rec extract_signature = function | [] -> [] @@ -53,21 +55,39 @@ let rec extract_signature = function | _::l -> extract_signature l let check_unicity s l = - let l' = List.map (fun (l,_) -> extract_signature l) l in + let l' = List.map (fun (l,_,_) -> extract_signature l) l in if not (Util.List.distinct l') then Pp.msg_warning (strbrk ("Two distinct rules of tactic entry "^s^" have the same "^ "non-terminals in the same order: put them in distinct tactic entries")) -let make_clause (pt,e) = +let make_clause (pt,_,e) = (make_patt pt, vala (Some (make_when (MLast.loc_of_expr e) pt)), - make_let e pt) + make_let false e pt) let make_fun_clauses loc s l = check_unicity s l; Compat.make_fun loc (List.map make_clause l) +let make_clause_classifier cg s (pt,c,_) = + match c ,cg with + | Some c, _ -> + (make_patt pt, + vala (Some (make_when (MLast.loc_of_expr c) pt)), + make_let true c pt) + | None, Some cg -> + (make_patt pt, + vala (Some (make_when (MLast.loc_of_expr cg) pt)), + <:expr< fun () -> $cg$ $str:s$ >>) + | None, None -> + (make_patt pt, + vala (Some (make_when loc pt)), + <:expr< fun () -> (Vernacexpr.VtProofStep, Vernacexpr.VtLater) >>) + +let make_fun_classifiers loc s c l = + Compat.make_fun loc (List.map (make_clause_classifier c s) l) + let rec make_args = function | [] -> <:expr< [] >> | GramNonTerminal(loc,t,_,Some p)::l -> @@ -89,7 +109,7 @@ let make_prod_item = function $mlexpr_of_prod_entry_key g$ $mlexpr_of_option mlexpr_of_ident sopt$ >> let mlexpr_of_clause = - mlexpr_of_list (fun (a,b) -> mlexpr_of_list make_prod_item a) + mlexpr_of_list (fun (a,_,b) -> mlexpr_of_list make_prod_item a) let rec make_tags loc = function | [] -> <:expr< [] >> @@ -101,7 +121,7 @@ let rec make_tags loc = function <:expr< [ $t$ :: $l$ ] >> | _::l -> make_tags loc l -let make_one_printing_rule se (pt,e) = +let make_one_printing_rule se (pt,_,e) = let level = mlexpr_of_int 0 in (* only level 0 supported here *) let loc = MLast.loc_of_expr e in let prods = mlexpr_of_list mlexpr_terminals_of_grammar_tactic_prod_item_expr pt in @@ -151,11 +171,11 @@ let rec possibly_empty_subentries loc = function let possibly_atomic loc prods = let l = List.map_filter (function - | GramTerminal s :: l, _ -> Some (s,l) + | GramTerminal s :: l, _, _ -> Some (s,l) | _ -> None) prods in possibly_empty_subentries loc (List.factorize_left l) -let declare_tactic loc s cl = +let declare_tactic loc s c cl = let se = mlexpr_of_string s in let pp = make_printing_rule se cl in let gl = mlexpr_of_clause cl in @@ -164,8 +184,10 @@ let declare_tactic loc s cl = (possibly_atomic loc cl) in declare_str_items loc [ <:str_item< do { - try - let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in + try do { + Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$; + Vernac_classifier.declare_vernac_classifier + $se$ $make_fun_classifiers loc s c cl$; List.iter (fun (s,l) -> match l with [ Some l -> @@ -173,7 +195,7 @@ let declare_tactic loc s cl = (Tacexpr.TacAtom($default_loc$, Tacexpr.TacExtend($default_loc$,$se$,l))) | None -> () ]) - $atomic_tactics$ + $atomic_tactics$ } with [ e when Errors.noncritical e -> Pp.msg_warning (Pp.app @@ -190,17 +212,20 @@ EXTEND GLOBAL: str_item; str_item: [ [ "TACTIC"; "EXTEND"; s = tac_name; + c = OPT [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> ]; OPT "|"; l = LIST1 tacrule SEP "|"; "END" -> - declare_tactic loc s l ] ] + declare_tactic loc s c l ] ] ; tacrule: - [ [ "["; l = LIST1 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]" -> + [ [ "["; l = LIST1 tacargs; "]"; + c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> c ]; + "->"; "["; e = Pcaml.expr; "]" -> (match l with | GramNonTerminal _ :: _ -> (* En attendant la syntaxe de tacticielles *) failwith "Tactic syntax must start with an identifier" - | _ -> (l,e)) + | _ -> (l,c,e)) ] ] ; tacargs: diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 7d02a1ba5..0d91c796a 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -28,33 +28,81 @@ let rec make_let e = function | _::l -> make_let e l let check_unicity s l = - let l' = List.map (fun (_,l,_) -> extract_signature l) l in + let l' = List.map (fun (_,l,_,_) -> extract_signature l) l in if not (Util.List.distinct l') then - Pp.msg_warning + msg_warning (strbrk ("Two distinct rules of entry "^s^" have the same "^ "non-terminals in the same order: put them in distinct vernac entries")) -let make_clause (_,pt,e) = +let make_clause (_,pt,_,e) = (make_patt pt, vala (Some (make_when (MLast.loc_of_expr e) pt)), make_let e pt) +(* To avoid warnings *) +let mk_ignore c pt = + let names = CList.map_filter (function + | GramNonTerminal(_,_,_,Some p) -> Some (Names.Id.to_string p) + | _ -> None) pt in + let names = List.map (fun n -> <:expr< $lid:n$ >>) names in + <:expr< do { ignore($list:names$); $c$ } >> + +let make_clause_classifier cg s (_,pt,c,_) = + match c ,cg with + | Some c, _ -> + (make_patt pt, + vala (Some (make_when (MLast.loc_of_expr c) pt)), + make_let (mk_ignore c pt) pt) + | None, Some cg -> + (make_patt pt, + vala (Some (make_when (MLast.loc_of_expr cg) pt)), + <:expr< fun () -> $cg$ $str:s$ >>) + | None, None -> msg_warning + (strbrk("Vernac entry \""^s^"\" misses a classifier. "^ + "A classifier is a function that returns an expression "^ + "of type vernac_classification (see Vernacexpr). You can: ")++ + str"- "++hov 0 ( + strbrk("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^ + "new vernacular command does not alter the system state;"))++fnl()++ + str"- "++hov 0 ( + strbrk("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^ + "new vernacular command alters the system state but not the "^ + "parser nor it starts a proof or ends one;"))++fnl()++ + str"- "++hov 0 ( + strbrk("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^ + "a global function f. The function f will be called passing "^ + "\""^s^"\" as the only argument;")) ++fnl()++ + str"- "++hov 0 ( + strbrk"Add a specific classifier in each clause using the syntax:" + ++fnl()++strbrk("'[...] => [ f ] -> [...]'. "))++fnl()++ + strbrk("Specific classifiers have precedence over global "^ + "classifiers. Only one classifier is called.")++fnl()); + (make_patt pt, + vala (Some (make_when loc pt)), + <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) + let make_fun_clauses loc s l = check_unicity s l; Compat.make_fun loc (List.map make_clause l) +let make_fun_classifiers loc s c l = + Compat.make_fun loc (List.map (make_clause_classifier c s) l) + let mlexpr_of_clause = mlexpr_of_list - (fun (a,b,c) -> mlexpr_of_list make_prod_item + (fun (a,b,_,_) -> mlexpr_of_list make_prod_item (Option.List.cons (Option.map (fun a -> GramTerminal a) a) b)) -let declare_command loc s nt cl = +let declare_command loc s c nt cl = let se = mlexpr_of_string s in let gl = mlexpr_of_clause cl in let funcl = make_fun_clauses loc s cl in + let classl = make_fun_classifiers loc s c cl in declare_str_items loc [ <:str_item< do { - try Vernacinterp.vinterp_add $se$ $funcl$ + try do { + Vernacinterp.vinterp_add $se$ $funcl$; + Vernac_classifier.declare_vernac_classifier $se$ $classl$ } with [ e when Errors.noncritical e -> Pp.msg_warning (Pp.app @@ -69,25 +117,37 @@ open PcamlSig EXTEND GLOBAL: str_item; str_item: - [ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT; + [ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT; c = OPT classification; OPT "|"; l = LIST1 rule SEP "|"; "END" -> - declare_command loc s <:expr> l - | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; + declare_command loc s c <:expr> l + | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; c = OPT classification; OPT "|"; l = LIST1 rule SEP "|"; "END" -> - declare_command loc s <:expr> l ] ] + declare_command loc s c <:expr> l ] ] + ; + classification: + [ [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> + | "CLASSIFIED"; "AS"; "SIDEFF" -> + <:expr< fun _ -> Vernac_classifier.classify_as_sideeff >> + | "CLASSIFIED"; "AS"; "QUERY" -> + <:expr< fun _ -> Vernac_classifier.classify_as_query >> + ] ] ; (* spiwack: comment-by-guessing: it seems that the isolated string (which otherwise could have been another argument) is not passed to the VernacExtend interpreter function to discriminate between the clauses. *) rule: - [ [ "["; s = STRING; l = LIST0 args; "]"; "->"; "["; e = Pcaml.expr; "]" - -> - if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty."); - (Some s,l,<:expr< fun () -> $e$ >>) - | "[" ; "-" ; l = LIST1 args ; "]" ; "->" ; "[" ; e = Pcaml.expr ; "]" -> - (None,l,<:expr< fun () -> $e$ >>) + [ [ "["; s = STRING; l = LIST0 args; "]"; + c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun () -> $c$>> ]; + "->"; "["; e = Pcaml.expr; "]" -> + if String.is_empty s then + Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty."); + (Some s,l,c,<:expr< fun () -> $e$ >>) + | "[" ; "-" ; l = LIST1 args ; "]" ; + c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun () -> $c$>> ]; + "->"; "["; e = Pcaml.expr; "]" -> + (None,l,c,<:expr< fun () -> $e$ >>) ] ] ; args: diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 9a26668cd..5bfea4e34 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -422,7 +422,7 @@ and located_vernac_expr = Loc.t * vernac_expr a query like Check *) type vernac_type = | VtStartProof of vernac_start - | VtSideff + | VtSideff of vernac_sideff_type | VtQed of vernac_qed_type | VtProofStep | VtQuery of vernac_part_of_script @@ -430,6 +430,7 @@ type vernac_type = | VtUnknown and vernac_qed_type = KeepProof | DropProof (* Qed, Admitted/Abort *) and vernac_start = string * Id.t list +and vernac_sideff_type = Id.t list and vernac_is_alias = bool and vernac_part_of_script = bool and vernac_control = diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4 index 95ffd281c..a0d4771f1 100644 --- a/parsing/g_obligations.ml4 +++ b/parsing/g_obligations.ml4 @@ -60,7 +60,9 @@ let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type = open Obligations -VERNAC COMMAND EXTEND Obligations +let classify_obbl _ = Vernacexpr.VtStartProof ("Classic",[]), Vernacexpr.VtLater + +VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl | [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] -> [ obligation (num, Some name, Some t) tac ] | [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> @@ -74,35 +76,35 @@ VERNAC COMMAND EXTEND Obligations | [ "Next" "Obligation" withtac(tac) ] -> [ next_obligation None tac ] END -VERNAC COMMAND EXTEND Solve_Obligation +VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF | [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] -> [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ] | [ "Solve" "Obligation" integer(num) "with" tactic(t) ] -> [ try_solve_obligation num None (Some (Tacinterp.interp t)) ] - END +END -VERNAC COMMAND EXTEND Solve_Obligations +VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF | [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] -> [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ] | [ "Solve" "Obligations" "with" tactic(t) ] -> [ try_solve_obligations None (Some (Tacinterp.interp t)) ] | [ "Solve" "Obligations" ] -> [ try_solve_obligations None None ] - END +END -VERNAC COMMAND EXTEND Solve_All_Obligations +VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF | [ "Solve" "All" "Obligations" "with" tactic(t) ] -> [ solve_all_obligations (Some (Tacinterp.interp t)) ] | [ "Solve" "All" "Obligations" ] -> [ solve_all_obligations None ] - END +END -VERNAC COMMAND EXTEND Admit_Obligations +VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF | [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ] | [ "Admit" "Obligations" ] -> [ admit_obligations None ] - END +END -VERNAC COMMAND EXTEND Set_Solver +VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ set_default_tactic (Locality.make_section_locality (Locality.LocalityFixme.consume ())) @@ -111,17 +113,17 @@ END open Pp -VERNAC COMMAND EXTEND Show_Solver +VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY | [ "Show" "Obligation" "Tactic" ] -> [ msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ] END -VERNAC COMMAND EXTEND Show_Obligations +VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY | [ "Obligations" "of" ident(name) ] -> [ show_obligations (Some name) ] | [ "Obligations" ] -> [ show_obligations None ] END -VERNAC COMMAND EXTEND Show_Preterm +VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY | [ "Preterm" "of" ident(name) ] -> [ msg_info (show_term (Some name)) ] | [ "Preterm" ] -> [ msg_info (show_term None) ] END 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 ] diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 21678c971..646c57d95 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -735,12 +735,12 @@ let set_transparency cl b = let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in Classes.set_typeclass_transparency ev false b) cl -VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings +VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF | [ "Typeclasses" "Transparent" reference_list(cl) ] -> [ set_transparency cl true ] END -VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings +VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF | [ "Typeclasses" "Opaque" reference_list(cl) ] -> [ set_transparency cl false ] END @@ -765,7 +765,7 @@ END (* true = All transparent, false = Opaque if possible *) -VERNAC COMMAND EXTEND Typeclasses_Settings +VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF | [ "Typeclasses" "eauto" ":=" debug(d) depth(depth) ] -> [ set_typeclasses_debug d; set_typeclasses_depth depth diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 713d6f233..6b607c38d 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -600,7 +600,7 @@ ARGUMENT EXTEND opthints | [ ] -> [ None ] END -VERNAC COMMAND EXTEND HintCut +VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ let entry = HintsCutEntry p in Auto.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ())) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index ae617a4d8..a935f6900 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -259,7 +259,9 @@ let add_rewrite_hint bases ort t lcsr = let add_hints base = add_rew_rules base eqs in List.iter add_hints bases -VERNAC COMMAND EXTEND HintRewrite +let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater + +VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY classify_hint [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> [ add_rewrite_hint bl o None l ] | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) @@ -300,14 +302,14 @@ let add_hints_iff l2r lc n bl = Auto.add_hints true bl (Auto.HintsResolveEntry (List.map (project_hint n l2r) lc)) -VERNAC COMMAND EXTEND HintResolveIffLR +VERNAC COMMAND EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ":" preident_list(bl) ] -> [ add_hints_iff true lc n bl ] | [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] -> [ add_hints_iff true lc n ["core"] ] END -VERNAC COMMAND EXTEND HintResolveIffRL +VERNAC COMMAND EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ":" preident_list(bl) ] -> [ add_hints_iff false lc n bl ] @@ -332,17 +334,20 @@ let refine_tac = refine open Inv open Leminv +let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater + VERNAC COMMAND EXTEND DeriveInversionClear - [ "Derive" "Inversion_clear" ident(na) hyp(id) ] + [ "Derive" "Inversion_clear" ident(na) hyp(id) ] => [ seff na ] -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_clear_tac ] -| [ "Derive" "Inversion_clear" natural(n) ident(na) hyp(id) ] +| [ "Derive" "Inversion_clear" natural(n) ident(na) hyp(id) ] => [ seff na ] -> [ inversion_lemma_from_goal n na id Term.prop_sort false inv_clear_tac ] | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ] + => [ seff na ] -> [ add_inversion_lemma_exn na c s false inv_clear_tac ] -| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] +| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ] -> [ add_inversion_lemma_exn na c GProp false inv_clear_tac ] END @@ -350,25 +355,28 @@ open Term VERNAC COMMAND EXTEND DeriveInversion | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ] + => [ seff na ] -> [ add_inversion_lemma_exn na c s false inv_tac ] -| [ "Derive" "Inversion" ident(na) "with" constr(c) ] +| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ] -> [ add_inversion_lemma_exn na c GProp false inv_tac ] -| [ "Derive" "Inversion" ident(na) hyp(id) ] +| [ "Derive" "Inversion" ident(na) hyp(id) ] => [ seff na ] -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_tac ] -| [ "Derive" "Inversion" natural(n) ident(na) hyp(id) ] +| [ "Derive" "Inversion" natural(n) ident(na) hyp(id) ] => [ seff na ] -> [ inversion_lemma_from_goal n na id Term.prop_sort false inv_tac ] END VERNAC COMMAND EXTEND DeriveDependentInversion | [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ] + => [ seff na ] -> [ add_inversion_lemma_exn na c s true dinv_tac ] - END +END VERNAC COMMAND EXTEND DeriveDependentInversionClear | [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ] + => [ seff na ] -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ] END @@ -470,17 +478,17 @@ TACTIC EXTEND stepr | ["stepr" constr(c) ] -> [ step false c tclIDTAC ] END -VERNAC COMMAND EXTEND AddStepl +VERNAC COMMAND EXTEND AddStepl CLASSIFIED AS SIDEFF | [ "Declare" "Left" "Step" constr(t) ] -> [ add_transitivity_lemma true t ] END -VERNAC COMMAND EXTEND AddStepr +VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF | [ "Declare" "Right" "Step" constr(t) ] -> [ add_transitivity_lemma false t ] END -VERNAC COMMAND EXTEND ImplicitTactic +VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF | [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> [ Pfedit.declare_implicit_tactic (Tacinterp.interp tac) ] END @@ -491,7 +499,7 @@ END (**********************************************************************) (*spiwack : Vernac commands for retroknowledge *) -VERNAC COMMAND EXTEND RetroknowledgeRegister +VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] -> [ let tc = Constrintern.interp_constr Evd.empty (Global.env ()) c in let tb = Constrintern.interp_constr Evd.empty (Global.env ()) b in @@ -766,7 +774,7 @@ END;; the semantics of the LCF-style tactics, hence with the classic tactic mode. *) VERNAC COMMAND EXTEND GrabEvars -[ "Grab" "Existential" "Variables" ] -> - [ Proof_global.with_current_proof (fun _ p -> - Proof.V82.grab_evars p) ] +[ "Grab" "Existential" "Variables" ] + => [ Vernacexpr.VtProofStep, Vernacexpr.VtLater ] + -> [ Proof_global.with_current_proof (fun _ p -> Proof.V82.grab_evars p) ] END diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 154cad691..c855486db 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1643,7 +1643,7 @@ let wit_binders = (Genarg.create_arg None "binders" : binders_argtype Genarg.uniform_genarg_type) -VERNAC COMMAND EXTEND AddRelation +VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> [ declare_relation a aeq n (Some lemma1) (Some lemma2) None ] @@ -1655,7 +1655,7 @@ VERNAC COMMAND EXTEND AddRelation [ declare_relation a aeq n None None None ] END -VERNAC COMMAND EXTEND AddRelation2 +VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> [ declare_relation a aeq n None (Some lemma2) None ] @@ -1663,7 +1663,7 @@ VERNAC COMMAND EXTEND AddRelation2 [ declare_relation a aeq n None (Some lemma2) (Some lemma3) ] END -VERNAC COMMAND EXTEND AddRelation3 +VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> [ declare_relation a aeq n (Some lemma1) None (Some lemma3) ] @@ -1676,7 +1676,7 @@ VERNAC COMMAND EXTEND AddRelation3 [ declare_relation a aeq n None None (Some lemma3) ] END -VERNAC COMMAND EXTEND AddParametricRelation +VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> @@ -1689,7 +1689,7 @@ VERNAC COMMAND EXTEND AddParametricRelation [ declare_relation ~binders:b a aeq n None None None ] END -VERNAC COMMAND EXTEND AddParametricRelation2 +VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> [ declare_relation ~binders:b a aeq n None (Some lemma2) None ] @@ -1697,7 +1697,7 @@ VERNAC COMMAND EXTEND AddParametricRelation2 [ declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) ] END -VERNAC COMMAND EXTEND AddParametricRelation3 +VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> [ declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) ] @@ -1846,18 +1846,22 @@ let add_morphism glob binders m s n = ignore(new_instance ~global:glob binders instance (Some (CRecord (Loc.ghost,None,[]))) ~generalize:false ~tac ~hook:(declare_projection n instance_id) None) -VERNAC COMMAND EXTEND AddSetoid1 +VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] a aeq t n ] | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders a aeq t n ] - | [ "Add" "Morphism" constr(m) ":" ident(n) ] -> - [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ] - | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] -> - [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ] + | [ "Add" "Morphism" constr(m) ":" ident(n) ] + (* This command may or may not open a goal *) + => [ Vernacexpr.VtUnknown, Vernacexpr.VtNow ] + -> [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ] + | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] + => [ Vernacexpr.VtStartProof("Classic",[n]), Vernacexpr.VtLater ] + -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ] | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) - "with" "signature" lconstr(s) "as" ident(n) ] -> - [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ] + "with" "signature" lconstr(s) "as" ident(n) ] + => [ Vernacexpr.VtStartProof("Classic",[n]), Vernacexpr.VtLater ] + -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ] END (** Bind to "rewrite" too *) diff --git a/toplevel/stm.ml b/toplevel/stm.ml index c1376079e..218929f23 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -40,8 +40,8 @@ let pr_ast (_, _, v) = pr_vernac v module Vcs_ = Vcs.Make(StateidOrderedType) type branch_type = [ `Master | `Proof of string * int ] -type cmd_t = ast -type fork_t = ast * Vcs_.branch_name * Names.Id.t list +type cmd_t = ast * Id.t list +type fork_t = ast * Vcs_.branch_name * Id.t list type qed_t = ast * vernac_qed_type * (Vcs_.branch_name * branch_type Vcs_.branch_info) type seff_t = ast option @@ -153,7 +153,7 @@ end = struct (* {{{ *) let print_dag vcs () = (* {{{ *) let fname = "stm" in let string_of_transaction = function - | Cmd t | Fork (t, _, _) -> + | Cmd (t, _) | Fork (t, _, _) -> (try string_of_ppcmds (pr_ast t) with _ -> "ERR") | Sideff (Some t) -> sprintf "Sideff(%s)" @@ -446,7 +446,7 @@ let collect_proof cur hd id = let rec collect last accn id = let view = VCS.visit id in match last, view.step with - | _, `Cmd x -> collect (Some (id,x)) (id::accn) view.next + | _, `Cmd (x, _) -> collect (Some (id,x)) (id::accn) view.next | _, `Alias _ -> collect None (id::accn) view.next | Some (parent, (_,_,VernacExactProof _)), `Fork _ -> `NotOptimizable `Immediate @@ -510,7 +510,7 @@ let known_state ~cache id = | DropProof -> reach view.next; Option.iter (interp start) proof_using_ast; - interp id x + interp id (pi1 x, pi2 x, VernacNop) end; Proof_global.discard_all ()) | `NotOptimizable `Immediate -> assert (view.next = eop); @@ -526,7 +526,7 @@ let known_state ~cache id = interp id ~proof x | DropProof -> reach view.next; - interp id x + interp id (pi1 x, pi2 x, VernacNop) end; Proof_global.discard_all ()) | `MaybeOptimizable (start, nodes) -> @@ -594,18 +594,7 @@ end = struct (* {{{ *) if id = initial_state_id || id = dummy_state_id then [] else match VCS.visit id with | { step = `Fork (_,_,l) } -> l - | { step = `Cmd (_,_, VernacFixpoint (_,l)) } -> - List.map (fun (((_,id),_,_,_,_),_) -> id) l - | { step = `Cmd (_,_, VernacCoFixpoint (_,l)) } -> - List.map (fun (((_,id),_,_,_),_) -> id) l - | { step = `Cmd (_,_, VernacAssumption (_,_,l)) } -> - List.flatten (List.map (fun (_,(lid,_)) -> List.map snd lid) l) - | { step = `Cmd (_,_, VernacInductive (_,_,l)) } -> - List.map (fun (((_,(_,id)),_,_,_,_),_) -> id) l - | { step = `Cmd (_,_, (VernacDefinition (_,(_,id),DefineBody _) | - VernacDeclareModuleType ((_,id),_,_,_) | - VernacDeclareModule (_,(_,id),_,_) | - VernacDefineModule (_,(_,id),_,_,_))) } -> [id] + | { step = `Cmd (_,l) } -> l | _ -> [] } history @@ -675,7 +664,7 @@ end (* }}} *) let init () = VCS.init initial_state_id; - declare_vernac_classifier "Stm" Backtrack.undo_vernac_classifier; + set_undo_classifier Backtrack.undo_vernac_classifier; State.define ~cache:true (fun () -> ()) initial_state_id; Backtrack.record () @@ -750,8 +739,7 @@ let process_transaction verbosely (loc, expr) = let bl = Backtrack.branches_of oid in List.iter (fun branch -> if not (List.mem branch bl) then - merge_proof_branch - (false,Loc.ghost,VernacAbortAll) DropProof branch) + merge_proof_branch x DropProof branch) (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); VCS.commit id (Alias oid); @@ -773,7 +761,7 @@ let process_transaction verbosely (loc, expr) = raise(State.exn_on dummy_state_id e)) | VtQuery true, w -> let id = VCS.new_node () in - VCS.commit id (Cmd x); + VCS.commit id (Cmd (x,[])); Backtrack.record (); if w = VtNow then finish () | VtQuery false, VtLater -> anomaly(str"classifier: VtQuery + VtLater must imply part_of_script") @@ -789,7 +777,7 @@ let process_transaction verbosely (loc, expr) = Backtrack.record (); if w = VtNow then finish () | VtProofStep, w -> let id = VCS.new_node () in - VCS.commit id (Cmd x); + VCS.commit id (Cmd (x,[])); Backtrack.record (); if w = VtNow then finish () | VtQed keep, w -> merge_proof_branch x keep head; @@ -797,10 +785,10 @@ let process_transaction verbosely (loc, expr) = Backtrack.record (); if w = VtNow then finish () (* Side effect on all branches *) - | VtSideff, w -> + | VtSideff l, w -> let id = VCS.new_node () in VCS.checkout VCS.master; - VCS.commit id (Cmd x); + VCS.commit id (Cmd (x,l)); VCS.propagate_sideff (Some x); VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w = VtNow then finish () @@ -821,7 +809,7 @@ let process_transaction verbosely (loc, expr) = VCS.commit id (Fork (x,bname,[])); VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1)) end else begin - VCS.commit id (Cmd x); + VCS.commit id (Cmd (x,[])); VCS.propagate_sideff (Some x); VCS.checkout_shallowest_proof_branch (); end in @@ -893,7 +881,7 @@ let get_script prf = | `Qed ((x,_,_), proof) -> find [pi3 x, (VCS.get_info id).n_goals] proof | `Sideff (`Ast (x,id)) -> find ((pi3 x, (VCS.get_info id).n_goals)::acc) id | `Sideff (`Id id) -> find acc id - | `Cmd x -> find ((pi3 x, (VCS.get_info id).n_goals)::acc) view.next + | `Cmd (x,_) -> find ((pi3 x, (VCS.get_info id).n_goals)::acc) view.next | `Alias id -> find acc id | `Fork _ -> find acc view.next in diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index d58df57f2..ab8c89623 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -19,9 +19,9 @@ Ppvernac Vernacinterp Mltop Vernacentries -Whelp Vernac_classifier Stm +Whelp Vernac Ide_slave Toplevel diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml index 46e04d87e..99ee547a8 100644 --- a/toplevel/vernac_classifier.ml +++ b/toplevel/vernac_classifier.ml @@ -16,7 +16,7 @@ let string_of_in_script b = if b then " (inside script)" else "" let string_of_vernac_type = function | VtUnknown -> "Unknown" | VtStartProof _ -> "StartProof" - | VtSideff -> "Sideff" + | VtSideff _ -> "Sideff" | VtQed _ -> "Qed" | VtProofStep -> "ProofStep" | VtQuery b -> "Query" ^ string_of_in_script b @@ -31,10 +31,11 @@ let string_of_vernac_when = function let string_of_vernac_classification (t,w) = string_of_vernac_type t ^ " " ^ string_of_vernac_when w -(* Since the set of vernaculars is extensible, also the classification function - has to be. *) -let classifiers = Summary.ref ~name:"vernac_classifier" [] -let declare_vernac_classifier s (f : vernac_expr -> vernac_classification) = +let classifiers = ref [] +let declare_vernac_classifier + (s : string) + (f : Genarg.raw_generic_argument list -> unit -> vernac_classification) += classifiers := !classifiers @ [s,f] let elide_part_of_script_and_now (a, _) = @@ -43,6 +44,9 @@ let elide_part_of_script_and_now (a, _) = | VtStm (x, _) -> VtStm (x, false), VtNow | x -> x, VtNow +let undo_classifier = ref (fun _ -> assert false) +let set_undo_classifier f = undo_classifier := f + let rec classify_vernac e = let static_classifier e = match e with (* Stm *) @@ -83,24 +87,39 @@ let rec classify_vernac e = | VernacDefinition (_,(_,i),ProveBody _) -> VtStartProof("Classic",[i]), VtLater | VernacStartTheoremProof (_,l,_) -> - let names = + let ids = CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in - VtStartProof ("Classic", names), VtLater + VtStartProof ("Classic", ids), VtLater | VernacGoal _ -> VtStartProof ("Classic",[]), VtLater - | VernacFixpoint (_,l) - when List.exists (fun ((_,_,_,_,p),_) -> p = None) l -> - VtStartProof ("Classic", - List.map (fun (((_,id),_,_,_,_),_) -> id) l), VtLater - | VernacCoFixpoint (_,l) - when List.exists (fun ((_,_,_,p),_) -> p = None) l -> - VtStartProof ("Classic", - List.map (fun (((_,id),_,_,_),_) -> id) l), VtLater + | VernacFixpoint (_,l) -> + let ids, open_proof = + List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) -> + id::l, b || p = None) ([],false) l in + if open_proof then VtStartProof ("Classic",ids), VtLater + else VtSideff ids, VtLater + | VernacCoFixpoint (_,l) -> + let ids, open_proof = + List.fold_left (fun (l,b) (((_,id),_,_,p),_) -> + id::l, b || p = None) ([],false) l in + if open_proof then VtStartProof ("Classic",ids), VtLater + else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) - | VernacAssumption _ - | VernacDefinition (_,_,DefineBody _) - | VernacFixpoint _ | VernacCoFixpoint _ - | VernacInductive _ - | VernacScheme _ | VernacCombinedScheme _ + | VernacAssumption (_,_,l) -> + let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in + VtSideff ids, VtLater + | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater + | VernacInductive (_,_,l) -> + let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with + | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l + | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @ + CList.map_filter (function + | ((_,AssumExpr((_,Names.Name n),_)),_),_ -> Some n + | _ -> None) l) l in + VtSideff (List.flatten ids), VtLater + | VernacScheme l -> + let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in + VtSideff ids, VtLater + | VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater | VernacBeginSection _ | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _ | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ @@ -116,14 +135,15 @@ let rec classify_vernac e = | VernacGlobalCheck _ | VernacDeclareReduction _ | VernacDeclareClass _ | VernacDeclareInstances _ - | VernacComments _ -> VtSideff, VtLater + | VernacRegister _ + | VernacComments _ -> VtSideff [], VtLater (* (Local) Notations have to disappear *) - | VernacEndSegment _ -> VtSideff, VtNow + | VernacEndSegment _ -> VtSideff [], VtNow (* Modules with parameters have to be executed: can import notations *) - | VernacDeclareModule (_,_,bl,_) - | VernacDefineModule (_,_,bl,_,_) - | VernacDeclareModuleType (_,bl,_,_) -> - VtSideff, if bl = [] then VtLater else VtNow + | VernacDeclareModule (_,(_,id),bl,_) + | VernacDefineModule (_,(_,id),bl,_,_) + | VernacDeclareModuleType ((_,id),bl,_,_) -> + VtSideff [id], if bl = [] then VtLater else VtNow (* These commands alter the parser *) | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ | VernacInfix _ | VernacNotation _ | VernacSyntaxExtension _ @@ -133,7 +153,7 @@ let rec classify_vernac e = | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) | VernacProofMode _ - | VernacRequireFrom _ -> VtSideff, VtNow + | VernacRequireFrom _ -> VtSideff [], VtNow (* These are ambiguous *) | VernacInstance _ -> VtUnknown, VtNow (* Stm will install a new classifier to handle these *) @@ -147,19 +167,11 @@ let rec classify_vernac e = | VernacRestoreState _ | VernacWriteState _ -> VtUnknown, VtNow (* Plugins should classify their commands *) - | VernacExtend _ -> VtUnknown, VtNow in - let rec extended_classifier = function - | [] -> static_classifier e - | (name,f)::fs -> - try - match f e with - | VtUnknown, _ -> extended_classifier fs - | x -> x - with e when Errors.noncritical e -> - let e = Errors.push e in - msg_warning(str"Exception raised by classifier: " ++ str name); - raise e - + | VernacExtend (s,l) -> + try List.assoc s !classifiers l () + with Not_found -> anomaly(str"No classifier for"++spc()++str s) in - extended_classifier !classifiers + static_classifier e +let classify_as_query = VtQuery true, VtLater +let classify_as_sideeff = VtSideff [], VtLater diff --git a/toplevel/vernac_classifier.mli b/toplevel/vernac_classifier.mli index 06535d512..d6bc8b886 100644 --- a/toplevel/vernac_classifier.mli +++ b/toplevel/vernac_classifier.mli @@ -8,13 +8,21 @@ open Stateid open Vernacexpr +open Genarg val string_of_vernac_classification : vernac_classification -> string (** What does a vernacular do *) val classify_vernac : vernac_expr -> vernac_classification -(** Install an additional vernacular classifier (that has precedence over - all classifiers already installed) *) +(** Install a vernacular classifier for VernacExtend *) val declare_vernac_classifier : - string -> (vernac_expr -> vernac_classification) -> unit + string -> (raw_generic_argument list -> unit -> vernac_classification) -> unit + +(** Set by Stm *) +val set_undo_classifier : (vernac_expr -> vernac_classification) -> unit + +(** Standard constant classifiers *) +val classify_as_query : vernac_classification +val classify_as_sideeff : vernac_classification + diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 8185e5702..7508ffaab 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -211,14 +211,15 @@ VERNAC ARGUMENT EXTEND whelp_constr_request | [ "Instance" ] -> [ "instance" ] END -VERNAC COMMAND EXTEND Whelp +VERNAC COMMAND EXTEND Whelp CLASSIFIED AS QUERY | [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] | [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] | [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (Smartlocate.global_inductive_with_alias r) ] | [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c] END -VERNAC COMMAND EXTEND WhelpHint +VERNAC COMMAND EXTEND WhelpHint CLASSIFIED AS QUERY | [ "Whelp" "Hint" constr(c) ] -> [ whelp_constr_expr "hint" c ] -| [ "Whelp" "Hint" ] -> [ on_goal (whelp_constr "hint") ] +| [ "Whelp" "Hint" ] => [ Vernacexpr.VtProofStep, Vernacexpr.VtLater ] -> + [ on_goal (whelp_constr "hint") ] END -- cgit v1.2.3