aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--coqpp/coqpp_ast.mli3
-rw-r--r--coqpp/coqpp_lex.mll1
-rw-r--r--coqpp/coqpp_main.ml72
-rw-r--r--coqpp/coqpp_parse.mly29
-rw-r--r--plugins/derive/g_derive.mlg4
-rw-r--r--plugins/extraction/g_extraction.mlg4
-rw-r--r--plugins/funind/g_indfun.mlg12
-rw-r--r--plugins/ltac/extratactics.mlg8
-rw-r--r--plugins/ltac/g_ltac.mlg6
-rw-r--r--plugins/ltac/g_obligations.mlg14
-rw-r--r--vernac/vernacentries.ml36
-rw-r--r--vernac/vernacentries.mli13
12 files changed, 125 insertions, 77 deletions
diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli
index 81109887ba..4ace6e78d2 100644
--- a/coqpp/coqpp_ast.mli
+++ b/coqpp/coqpp_ast.mli
@@ -103,7 +103,7 @@ type classification =
type vernac_rule = {
vernac_atts : (string * string) list option;
- vernac_state: string option;
+ vernac_state : string option;
vernac_toks : ext_token list;
vernac_class : code option;
vernac_depr : bool;
@@ -114,6 +114,7 @@ type vernac_ext = {
vernacext_name : string;
vernacext_entry : code option;
vernacext_class : classification;
+ vernacext_state : string option;
vernacext_rules : vernac_rule list;
}
diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll
index 81ba8ad98c..9c6b78dc98 100644
--- a/coqpp/coqpp_lex.mll
+++ b/coqpp/coqpp_lex.mll
@@ -103,6 +103,7 @@ rule extend = parse
| "PLUGIN" { PLUGIN }
| "DEPRECATED" { DEPRECATED }
| "CLASSIFIED" { CLASSIFIED }
+| "STATE" { STATE }
| "PRINTED" { PRINTED }
| "TYPED" { TYPED }
| "INTERPRETED" { INTERPRETED }
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 8444f3a58c..ad79599cf4 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -357,41 +357,35 @@ let print_atts_right fmt = function
let nota = match atts with [_] -> "" | _ -> "Attributes.Notations." in
fprintf fmt "(Attributes.parse %s%a atts)" nota aux atts
-let print_body_wrapper fmt r =
- match r.vernac_state with
- | Some "proof_stack" ->
- fprintf fmt "let proof = (%a) ~pstate:st.Vernacstate.proof in { st with Vernacstate.proof }" print_code r.vernac_body
-
- | Some "open_proof" ->
- let push = "Some (Proof_global.push ~ontop:st.Vernacstate.proof pstate)" in
- fprintf fmt "let pstate = (%a) in let proof = %s in { st with Vernacstate.proof }" print_code r.vernac_body push
-
- | Some "maybe_open_proof" ->
- let push = "Proof_global.maybe_push ~ontop:st.Vernacstate.proof pstate" in
- fprintf fmt "let pstate = (%a) in let proof = %s in { st with Vernacstate.proof }" print_code r.vernac_body push
-
- | Some "proof" ->
- fprintf fmt "let proof = Vernacentries.modify_pstate ~pstate:st.Vernacstate.proof (%a) in { st with Vernacstate.proof }" print_code r.vernac_body
-
- | Some "proof_opt_query" ->
- fprintf fmt "let () = (%a) ~pstate:(Vernacstate.pstate st) in st" print_code r.vernac_body
-
- | Some "proof_query" ->
- fprintf fmt "let () = Vernacentries.with_pstate ~pstate:st.Vernacstate.proof (%a) in st" print_code r.vernac_body
-
- | None ->
- fprintf fmt "let () = %a in st" print_code r.vernac_body
-
- | Some x ->
- fatal ("unsupported state specifier: " ^ x)
-
-let print_body_fun fmt r =
- fprintf fmt "let coqpp_body %a%a ~st = @[%a@] in "
- print_binders r.vernac_toks print_atts_left r.vernac_atts print_body_wrapper r
-
-let print_body fmt r =
+let understand_state = function
+ | "proof_stack" -> "VtModifyProofStack", false
+ | "maybe_open_proof" -> "VtMaybeOpenProof", true
+ | "open_proof" -> "VtOpenProof", true
+ | "proof" -> "VtModifyProof", false
+ | "proof_opt_query" -> "VtReadProofOpt", false
+ | "proof_query" -> "VtReadProof", false
+ | s -> fatal ("unsupported state specifier: " ^ s)
+
+let print_body_state state fmt r =
+ let state = match r.vernac_state with Some _ as s -> s | None -> state in
+ match state with
+ | None -> fprintf fmt "Vernacentries.VtDefault (fun () -> %a)" print_code r.vernac_body
+ | Some "CUSTOM" -> print_code fmt r.vernac_body
+ | Some state ->
+ let state, unit_wrap = understand_state state in
+ fprintf fmt "Vernacentries.%s (%s%a)" state (if unit_wrap then "fun () ->" else "")
+ print_code r.vernac_body
+
+let print_body_wrapper state fmt r =
+ fprintf fmt "Vernacentries.interp_functional_vernac (%a)" (print_body_state state) r
+
+let print_body_fun state fmt r =
+ fprintf fmt "let coqpp_body %a%a = @[%a@] in "
+ print_binders r.vernac_toks print_atts_left r.vernac_atts (print_body_wrapper state) r
+
+let print_body state fmt r =
fprintf fmt "@[(%afun %a~atts@ ~st@ -> coqpp_body %a%a ~st)@]"
- print_body_fun r print_binders r.vernac_toks
+ (print_body_fun state) r print_binders r.vernac_toks
print_binders r.vernac_toks print_atts_right r.vernac_atts
let rec print_sig fmt = function
@@ -402,12 +396,12 @@ let rec print_sig fmt = function
fprintf fmt "@[Vernacextend.TyNonTerminal (%a, %a)@]"
print_symbol symb print_sig rem
-let print_rule fmt r =
+let print_rule state fmt r =
fprintf fmt "Vernacextend.TyML (%b, %a, %a, %a)"
- r.vernac_depr print_sig r.vernac_toks print_body r print_rule_classifier r
+ r.vernac_depr print_sig r.vernac_toks (print_body state) r print_rule_classifier r
-let print_rules fmt rules =
- print_list fmt (fun fmt r -> fprintf fmt "(%a)" print_rule r) rules
+let print_rules state fmt rules =
+ print_list fmt (fun fmt r -> fprintf fmt "(%a)" (print_rule state) r) rules
let print_classifier fmt = function
| ClassifDefault -> fprintf fmt ""
@@ -426,7 +420,7 @@ let print_ast fmt ext =
let pr fmt () =
fprintf fmt "Vernacextend.vernac_extend ~command:\"%s\" %a ?entry:%a %a"
ext.vernacext_name print_classifier ext.vernacext_class
- print_entry ext.vernacext_entry print_rules ext.vernacext_rules
+ print_entry ext.vernacext_entry (print_rules ext.vernacext_state) ext.vernacext_rules
in
let () = fprintf fmt "let () = @[%a@]@\n" pr () in
()
diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly
index 43ba990f6a..930a205f85 100644
--- a/coqpp/coqpp_parse.mly
+++ b/coqpp/coqpp_parse.mly
@@ -64,7 +64,7 @@ let parse_user_entry s sep =
%token <int> INT
%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED ARGUMENT
%token RAW_PRINTED GLOB_PRINTED
-%token COMMAND CLASSIFIED PRINTED TYPED INTERPRETED GLOBALIZED SUBSTITUTED BY AS
+%token COMMAND CLASSIFIED STATE PRINTED TYPED INTERPRETED GLOBALIZED SUBSTITUTED BY AS
%token BANGBRACKET HASHBRACKET LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR
%token LPAREN RPAREN COLON SEMICOLON
%token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA
@@ -183,12 +183,13 @@ argtype:
;
vernac_extend:
-| VERNAC vernac_entry EXTEND IDENT vernac_classifier vernac_rules END
+| VERNAC vernac_entry EXTEND IDENT vernac_classifier vernac_state vernac_rules END
{ VernacExt {
vernacext_name = $4;
vernacext_entry = $2;
vernacext_class = $5;
- vernacext_rules = $6;
+ vernacext_state = $6;
+ vernacext_rules = $7;
} }
;
@@ -203,16 +204,21 @@ vernac_classifier:
| CLASSIFIED AS IDENT { ClassifName $3 }
;
+vernac_state:
+| { None }
+| STATE IDENT { Some $2 }
+;
+
vernac_rules:
| vernac_rule { [$1] }
| vernac_rule vernac_rules { $1 :: $2 }
;
vernac_rule:
-| PIPE vernac_attributes_opt vernac_state_opt LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE
+| PIPE vernac_attributes_opt rule_state LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE
{ {
vernac_atts = $2;
- vernac_state= $3;
+ vernac_state = $3;
vernac_toks = $5;
vernac_depr = $7;
vernac_class= $8;
@@ -220,6 +226,11 @@ vernac_rule:
} }
;
+rule_state:
+| { None }
+| BANGBRACKET IDENT RBRACKET { Some $2 }
+;
+
vernac_attributes_opt:
| { None }
| HASHBRACKET vernac_attributes RBRACKET { Some $2 }
@@ -236,14 +247,6 @@ vernac_attribute:
| qualid_or_ident { ($1, $1) }
;
-vernac_state_opt:
-| { None }
-| BANGBRACKET vernac_state RBRACKET { Some $2 }
-;
-
-vernac_state:
-| qualid_or_ident { $1 }
-
rule_deprecation:
| { false }
| DEPRECATED { true }
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg
index d25b8fd01c..526989fdf3 100644
--- a/plugins/derive/g_derive.mlg
+++ b/plugins/derive/g_derive.mlg
@@ -22,7 +22,7 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac
}
-VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command }
-| ![ open_proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
+VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } STATE open_proof
+| [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
{ Derive.(start_deriving f suchthat lemma) }
END
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index 487accbc9b..9ea3fbeaf4 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -177,7 +177,7 @@ VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF
END
(* Show the extraction of the current proof *)
-VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY
-| ![ proof_query ] [ "Show" "Extraction" ]
+VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY STATE proof_query
+| [ "Show" "Extraction" ]
-> { show_extraction }
END
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index cc772e96f3..8c9b1e7ba4 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -176,8 +176,8 @@ let () =
}
(* TASSI: n'importe quoi ! *)
-VERNAC COMMAND EXTEND Function
-| ![ maybe_open_proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
+VERNAC COMMAND EXTEND Function STATE maybe_open_proof
+| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
=> { let hard = List.exists (function
| _,((_,(Some { CAst.v = CMeasureRec _ }
| Some { CAst.v = CWfRec _}),_,_,_),_) -> true
@@ -224,8 +224,8 @@ let warning_error names e =
}
-VERNAC COMMAND EXTEND NewFunctionalScheme
-| ![ maybe_open_proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
+VERNAC COMMAND EXTEND NewFunctionalScheme STATE maybe_open_proof
+| ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
=> { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
->
{ begin
@@ -263,7 +263,7 @@ VERNAC COMMAND EXTEND NewFunctionalCase
END
(***** debug only ***)
-VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
-| ![ maybe_open_proof ] ["Generate" "graph" "for" reference(c)] ->
+VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY STATE maybe_open_proof
+| ["Generate" "graph" "for" reference(c)] ->
{ make_graph (Smartlocate.global_with_alias c) }
END
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 4a2fb425ac..0ded60d9c7 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -931,8 +931,8 @@ END
(* spiwack: I put it in extratactics because it is somewhat tied with
the semantics of the LCF-style tactics, hence with the classic tactic
mode. *)
-VERNAC COMMAND EXTEND GrabEvars
-| ![ proof ] [ "Grab" "Existential" "Variables" ]
+VERNAC COMMAND EXTEND GrabEvars STATE proof
+| [ "Grab" "Existential" "Variables" ]
=> { classify_as_proofstep }
-> { fun ~pstate -> Proof_global.modify_proof (fun p -> Proof.V82.grab_evars p) pstate }
END
@@ -963,8 +963,8 @@ TACTIC EXTEND unshelve
END
(* Command to add every unshelved variables to the focus *)
-VERNAC COMMAND EXTEND Unshelve
-| ![ proof ] [ "Unshelve" ]
+VERNAC COMMAND EXTEND Unshelve STATE proof
+| [ "Unshelve" ]
=> { classify_as_proofstep }
-> { fun ~pstate -> Proof_global.modify_proof (fun p -> Proof.unshelve p) pstate }
END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 9bf5bd1bda..960e5b76f8 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -434,13 +434,13 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false
}
-VERNAC { tactic_mode } EXTEND VernacSolve
-| ![ proof ] [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+VERNAC { tactic_mode } EXTEND VernacSolve STATE proof
+| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
{ classify_as_proofstep } -> {
let g = Option.default (Goal_select.get_default_goal_selector ()) g in
vernac_solve g n t def
}
-| ![ proof ] [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
{
let anon_abstracting_tac = is_anonymous_abstract t in
let solving_tac = is_explicit_terminator t in
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index c01b97c14d..58c8dabd79 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -87,18 +87,18 @@ let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), V
}
-VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl }
-| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
+VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE open_proof
+| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, Some name, Some t) tac }
-| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
+| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
{ obligation (num, Some name, None) tac }
-| ![ open_proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
+| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, None, Some t) tac }
-| ![ open_proof ] [ "Obligation" integer(num) withtac(tac) ] ->
+| [ "Obligation" integer(num) withtac(tac) ] ->
{ obligation (num, None, None) tac }
-| ![ open_proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
+| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
{ next_obligation (Some name) tac }
-| ![ open_proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
+| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
END
VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 34b5e13cd8..e4667e376c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2711,3 +2711,39 @@ let interp ?(verbosely=true) ?proof ~st cmd =
let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in
Vernacstate.invalidate_cache ();
iraise exn
+
+(* mlg helpers *)
+
+type functional_vernac =
+ | VtDefault of (unit -> unit)
+ | VtModifyProofStack of (pstate:Proof_global.t option -> Proof_global.t option)
+ | VtMaybeOpenProof of (unit -> Proof_global.pstate option)
+ | VtOpenProof of (unit -> Proof_global.pstate)
+ | VtModifyProof of (pstate:Proof_global.pstate -> Proof_global.pstate)
+ | VtReadProofOpt of (pstate:Proof_global.pstate option -> unit)
+ | VtReadProof of (pstate:Proof_global.pstate -> unit)
+
+let interp_functional_vernac c ~st =
+ let open Proof_global in
+ let open Vernacstate in
+ match c with
+ | VtDefault f -> f (); st
+ | VtModifyProofStack f ->
+ let proof = f ~pstate:st.proof in { st with proof }
+ | VtMaybeOpenProof f ->
+ let pstate = f () in
+ let proof = maybe_push ~ontop:st.proof pstate in
+ { st with proof }
+ | VtOpenProof f ->
+ let pstate = f () in
+ let proof = Some (push ~ontop:st.proof pstate) in
+ { st with proof }
+ | VtModifyProof f ->
+ let proof = modify_pstate f ~pstate:st.proof in
+ { st with proof }
+ | VtReadProofOpt f ->
+ f ~pstate:(Option.map get_current_pstate st.proof);
+ st
+ | VtReadProof f ->
+ with_pstate ~pstate:st.proof f;
+ st
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 5e6e9fdb0f..9756c1e0bb 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -51,3 +51,16 @@ val modify_pstate : pstate:Proof_global.t option -> (pstate:Proof_global.pstate
(* Flag set when the test-suite is called. Its only effect to display
verbose information for `Fail` *)
val test_mode : bool ref
+
+(** For mlg *)
+
+type functional_vernac =
+ | VtDefault of (unit -> unit)
+ | VtModifyProofStack of (pstate:Proof_global.t option -> Proof_global.t option)
+ | VtMaybeOpenProof of (unit -> Proof_global.pstate option)
+ | VtOpenProof of (unit -> Proof_global.pstate)
+ | VtModifyProof of (pstate:Proof_global.pstate -> Proof_global.pstate)
+ | VtReadProofOpt of (pstate:Proof_global.pstate option -> unit)
+ | VtReadProof of (pstate:Proof_global.pstate -> unit)
+
+val interp_functional_vernac : functional_vernac -> st:Vernacstate.t -> Vernacstate.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:45:25 +0000