aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/tacextend.ml459
-rw-r--r--grammar/vernacextend.ml492
-rw-r--r--intf/vernacexpr.mli3
-rw-r--r--parsing/g_obligations.ml428
-rw-r--r--plugins/decl_mode/g_decl_mode.ml420
-rw-r--r--plugins/extraction/g_extraction.ml432
-rw-r--r--plugins/firstorder/g_ground.ml44
-rw-r--r--plugins/funind/g_indfun.ml436
-rw-r--r--plugins/setoid_ring/newring.ml44
-rw-r--r--plugins/xml/xmlentries.ml42
-rw-r--r--tactics/class_tactics.ml46
-rw-r--r--tactics/eauto.ml42
-rw-r--r--tactics/extratactics.ml442
-rw-r--r--tactics/rewrite.ml430
-rw-r--r--toplevel/stm.ml42
-rw-r--r--toplevel/toplevel.mllib2
-rw-r--r--toplevel/vernac_classifier.ml94
-rw-r--r--toplevel/vernac_classifier.mli14
-rw-r--r--toplevel/whelp.ml47
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<None>> l
- | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT;
+ declare_command loc s c <:expr<None>> l
+ | "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; c = OPT classification;
OPT "|"; l = LIST1 rule SEP "|";
"END" ->
- declare_command loc s <:expr<Some $lid:nt$>> l ] ]
+ declare_command loc s c <:expr<Some $lid:nt$>> 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<auto with *>>) "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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-26 12:23:35 +0000