aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/09263-maximedenes-parsing-state.sh12
-rw-r--r--ide/idetop.ml13
-rw-r--r--lib/stateid.ml2
-rw-r--r--lib/stateid.mli1
-rw-r--r--parsing/pcoq.ml1
-rw-r--r--parsing/pcoq.mli14
-rw-r--r--plugins/derive/g_derive.mlg2
-rw-r--r--plugins/funind/g_indfun.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg11
-rw-r--r--plugins/ltac/g_obligations.mlg2
-rw-r--r--plugins/ltac/g_rewrite.mlg4
-rw-r--r--proofs/proof_global.ml92
-rw-r--r--proofs/proof_global.mli45
-rw-r--r--stm/stm.ml483
-rw-r--r--stm/stm.mli13
-rw-r--r--stm/vernac_classifier.ml26
-rw-r--r--toplevel/coqloop.ml23
-rw-r--r--toplevel/g_toplevel.mlg18
-rw-r--r--toplevel/vernac.ml74
-rw-r--r--vernac/lemmas.ml2
-rw-r--r--vernac/pvernac.ml38
-rw-r--r--vernac/pvernac.mli28
-rw-r--r--vernac/vernacentries.ml43
-rw-r--r--vernac/vernacentries.mli5
-rw-r--r--vernac/vernacextend.ml6
-rw-r--r--vernac/vernacextend.mli6
-rw-r--r--vernac/vernacstate.ml32
-rw-r--r--vernac/vernacstate.mli17
28 files changed, 527 insertions, 488 deletions
diff --git a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh
new file mode 100644
index 0000000000..ebd1b524da
--- /dev/null
+++ b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "9263" ] || [ "$CI_BRANCH" = "parsing-state" ]; then
+
+ mtac2_CI_REF=proof-mode
+ mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2
+
+ ltac2_CI_REF=proof-mode
+ ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+ equations_CI_REF=proof-mode
+ equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+fi
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 716a942d5c..f91aa569d4 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -83,7 +83,10 @@ let set_doc doc = ide_doc := Some doc
let add ((s,eid),(sid,verbose)) =
let doc = get_doc () in
let pa = Pcoq.Parsable.make (Stream.of_string s) in
- let loc_ast = Stm.parse_sentence ~doc sid pa in
+ match Stm.parse_sentence ~doc sid ~entry:Pvernac.main_entry pa with
+ | None -> assert false (* s is not an empty string *)
+ | Some (loc, ast) ->
+ let loc_ast = CAst.make ~loc ast in
let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in
set_doc doc;
let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
@@ -121,10 +124,10 @@ let query (route, (s,id)) =
let annotate phrase =
let doc = get_doc () in
- let {CAst.loc;v=ast} =
- let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
- Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa
- in
+ let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
+ match Stm.parse_sentence ~doc (Stm.get_current_state ~doc) ~entry:Pvernac.main_entry pa with
+ | None -> Richpp.richpp_of_pp 78 (Pp.mt ())
+ | Some (_, ast) ->
(* XXX: Width should be a parameter of annotate... *)
Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)
diff --git a/lib/stateid.ml b/lib/stateid.ml
index 5485c4bf19..8f45f3605d 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -27,6 +27,8 @@ let get exn = Exninfo.get exn state_id_info
let equal = Int.equal
let compare = Int.compare
+let print id = Pp.int id
+
module Self = struct
type t = int
let compare = compare
diff --git a/lib/stateid.mli b/lib/stateid.mli
index 5d4b71a354..f6ce7ddc40 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -20,6 +20,7 @@ val initial : t
val dummy : t
val fresh : unit -> t
val to_string : t -> string
+val print : t -> Pp.t
val of_int : int -> t
val to_int : t -> int
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 19ae97da77..759e60fbca 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -439,7 +439,6 @@ module Module =
let module_expr = Entry.create "module_expr"
let module_type = Entry.create "module_type"
end
-
let epsilon_value f e =
let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in
let ext = [None, None, [r]] in
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 352857d4cd..3203a25b46 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -41,6 +41,16 @@ end
- static rules explicitly defined in files g_*.ml4
- static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and
VERNAC EXTEND (see e.g. file extratactics.ml4)
+
+ Note that parsing a Coq document is in essence stateful: the parser
+ needs to recognize commands that start proofs and use a different
+ parsing entry point for them.
+
+ We thus provide two different interfaces: the "raw" parsing
+ interface, in the style of camlp5, which provides more flexibility,
+ and a more specialize "parse_vernac" one, which will indeed adjust
+ the state as needed.
+
*)
(** Dynamic extension of rules
@@ -269,3 +279,7 @@ type any_entry = AnyEntry : 'a Entry.t -> any_entry
val register_grammars_by_name : string -> any_entry list -> unit
val find_grammars_by_name : string -> any_entry list
+
+(** Parsing state handling *)
+val freeze : marshallable:bool -> frozen_t
+val unfreeze : frozen_t -> unit
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg
index df4b647642..0cdf8fb5d8 100644
--- a/plugins/derive/g_derive.mlg
+++ b/plugins/derive/g_derive.mlg
@@ -18,7 +18,7 @@ DECLARE PLUGIN "derive_plugin"
{
-let classify_derive_command _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
+let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]),VtLater)
}
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 8f0440a2a4..c4f8843e51 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -186,7 +186,7 @@ VERNAC COMMAND EXTEND Function
(Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
with
| Vernacextend.VtSideff ids, _ when hard ->
- Vernacextend.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
+ Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater)
| x -> x }
-> { do_generate_principle false (List.map snd recsl) }
END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index d9b19c1ae6..4c24f51b1e 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -58,15 +58,8 @@ let new_entry name =
let toplevel_selector = new_entry "vernac:toplevel_selector"
let tacdef_body = new_entry "tactic:tacdef_body"
-(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
- proof editing and changes nothing else). Then sets it as the default proof mode. *)
-let _ =
- let mode = {
- Proof_global.name = "Classic";
- set = (fun () -> Pvernac.set_command_entry tactic_mode);
- reset = (fun () -> Pvernac.(set_command_entry noedit_mode));
- } in
- Proof_global.register_proof_mode mode
+(* Registers [tactic_mode] as a parser for proof editing *)
+let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode
(* Hack to parse "[ id" without dropping [ *)
let test_bracket_ident =
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 1ea6ff84d4..cdee012a82 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -83,7 +83,7 @@ open Obligations
let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
-let classify_obbl _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
+let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
}
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 31fb1c9abf..db8d1b20d8 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -285,13 +285,13 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
add_morphism_infer atts m n;
}
| #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
- => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater }
+ => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
-> {
add_morphism atts [] m s n;
}
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
"with" "signature" lconstr(s) "as" ident(n) ]
- => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater }
+ => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
-> {
add_morphism atts binders m s n;
}
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 4cc73f419e..9ee9e7ae2c 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -22,51 +22,6 @@ open Names
module NamedDecl = Context.Named.Declaration
-(*** Proof Modes ***)
-
-(* Type of proof modes :
- - A function [set] to set it *from standard mode*
- - A function [reset] to reset the *standard mode* from it *)
-type proof_mode_name = string
-type proof_mode = {
- name : proof_mode_name ;
- set : unit -> unit ;
- reset : unit -> unit
-}
-
-let proof_modes = Hashtbl.create 6
-let find_proof_mode n =
- try Hashtbl.find proof_modes n
- with Not_found ->
- CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." n))
-
-let register_proof_mode ({name = n} as m) =
- Hashtbl.add proof_modes n (CEphemeron.create m)
-
-(* initial mode: standard mode *)
-let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) }
-let _ = register_proof_mode standard
-
-(* Default proof mode, to be set at the beginning of proofs. *)
-let default_proof_mode = ref (find_proof_mode "No")
-
-let get_default_proof_mode_name () =
- (CEphemeron.default !default_proof_mode standard).name
-
-let proof_mode_opt_name = ["Default";"Proof";"Mode"]
-let () =
- Goptions.(declare_string_option {
- optdepr = false;
- optname = "default proof mode" ;
- optkey = proof_mode_opt_name ;
- optread = begin fun () ->
- (CEphemeron.default !default_proof_mode standard).name
- end;
- optwrite = begin fun n ->
- default_proof_mode := find_proof_mode n
- end
- })
-
(*** Proof Global Environment ***)
(* Extra info on proofs. *)
@@ -95,7 +50,6 @@ type pstate = {
endline_tactic : Genarg.glob_generic_argument option;
section_vars : Constr.named_context option;
proof : Proof.t;
- mode : proof_mode CEphemeron.key;
universe_decl: UState.universe_decl;
strength : Decl_kinds.goal_kind;
}
@@ -109,23 +63,8 @@ let apply_terminator f = f
to be resumed when the current proof is closed or aborted. *)
let pstates = ref ([] : pstate list)
-(* Current proof_mode, for bookkeeping *)
-let current_proof_mode = ref !default_proof_mode
-
-(* combinators for proof modes *)
-let update_proof_mode () =
- match !pstates with
- | { mode = m } :: _ ->
- CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
- current_proof_mode := m;
- CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ())
- | _ ->
- CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
- current_proof_mode := find_proof_mode "No"
-
(* combinators for the current_proof lists *)
-let push a l = l := a::!l;
- update_proof_mode ()
+let push a l = l := a::!l
exception NoSuchProof
let () = CErrors.register_handler begin function
@@ -221,25 +160,8 @@ let discard {CAst.loc;v=id} =
let discard_current () =
if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates
-
let discard_all () = pstates := []
-(* [set_proof_mode] sets the proof mode to be used after it's called. It is
- typically called by the Proof Mode command. *)
-let set_proof_mode m id =
- pstates := List.map
- (fun ps -> if pf_name_eq id ps then { ps with mode = m } else ps)
- !pstates;
- update_proof_mode ()
-
-let set_proof_mode mn =
- set_proof_mode (find_proof_mode mn) (get_current_proof_name ())
-
-let activate_proof_mode mode =
- CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ())
-let disactivate_current_proof_mode () =
- CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ())
-
(** [start_proof sigma id pl str goals terminator] starts a proof of name
[id] with goals [goals] (a list of pairs of environment and
conclusion); [str] describes what kind of theorem/definition this
@@ -254,9 +176,8 @@ let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator
proof = Proof.start ~name ~poly:(pi2 kind) sigma goals;
endline_tactic = None;
section_vars = None;
- mode = find_proof_mode "No";
- universe_decl = pl;
- strength = kind } in
+ strength = kind;
+ universe_decl = pl } in
push initial_state pstates
let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator =
@@ -265,9 +186,8 @@ let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals termina
proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals;
endline_tactic = None;
section_vars = None;
- mode = find_proof_mode "No";
- universe_decl = pl;
- strength = kind } in
+ strength = kind;
+ universe_decl = pl } in
push initial_state pstates
let get_used_variables () = (cur_pstate ()).section_vars
@@ -478,7 +398,7 @@ end
let freeze ~marshallable =
if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.")
else !pstates
-let unfreeze s = pstates := s; update_proof_mode ()
+let unfreeze s = pstates := s
let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof
let copy_terminators ~src ~tgt =
assert(List.length src = List.length tgt);
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index e762f3b7dc..40920f51a3 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -13,7 +13,6 @@
environment. *)
type t
-
val there_are_pending_proofs : unit -> bool
val check_no_pending_proof : unit -> unit
@@ -139,47 +138,3 @@ val freeze : marshallable:bool -> t
val unfreeze : t -> unit
val proof_of_state : t -> Proof.t
val copy_terminators : src:t -> tgt:t -> t
-
-
-(**********************************************************)
-(* Proof Mode API *)
-(* The current Proof Mode API is deprecated and a new one *)
-(* will be (hopefully) defined in 8.8 *)
-(**********************************************************)
-
-(** Type of proof modes :
- - A name
- - A function [set] to set it *from standard mode*
- - A function [reset] to reset the *standard mode* from it
-
-*)
-type proof_mode_name = string
-type proof_mode = {
- name : proof_mode_name ;
- set : unit -> unit ;
- reset : unit -> unit
-}
-
-(** Registers a new proof mode which can then be adressed by name
- in [set_default_proof_mode].
- One mode is already registered - the standard mode - named "No",
- It corresponds to Coq default setting are they are set when coqtop starts. *)
-val register_proof_mode : proof_mode -> unit
-(* Can't make this deprecated due to limitations of camlp5 *)
-(* [@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] *)
-
-val proof_mode_opt_name : string list
-
-val get_default_proof_mode_name : unit -> proof_mode_name
-[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
-
-(** [set_proof_mode] sets the proof mode to be used after it's called. It is
- typically called by the Proof Mode command. *)
-val set_proof_mode : proof_mode_name -> unit
-[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
-
-val activate_proof_mode : proof_mode_name -> unit
-[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
-
-val disactivate_current_proof_mode : unit -> unit
-[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "]
diff --git a/stm/stm.ml b/stm/stm.ml
index 8ed7f2c866..dfe5581ed5 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -126,8 +126,6 @@ type aast = {
}
let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr_vernac expr)
-let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
-
(* Commands piercing opaque *)
let may_pierce_opaque = function
| VernacPrint _
@@ -146,13 +144,13 @@ let update_global_env () =
module Vcs_ = Vcs.Make(Stateid.Self)
type future_proof = Proof_global.closed_proof_output Future.computation
-type proof_mode = string
+
type depth = int
type branch_type =
[ `Master
- | `Proof of proof_mode * depth
+ | `Proof of depth
| `Edit of
- proof_mode * Stateid.t * Stateid.t * Vernacextend.vernac_qed_type * Vcs_.Branch.t ]
+ Stateid.t * Stateid.t * Vernacextend.vernac_qed_type * Vcs_.Branch.t ]
(* TODO 8.7 : split commands and tactics, since this type is too messy now *)
type cmd_t = {
ctac : bool; (* is a tactic *)
@@ -203,10 +201,10 @@ let summary_pstate = Evarutil.meta_counter_summary_tag,
Obligations.program_tcc_summary_tag
type cached_state =
- | Empty
- | Error of Exninfo.iexn
- | Valid of Vernacstate.t
-
+ | EmptyState
+ | ParsingState of Vernacstate.Parser.state
+ | FullState of Vernacstate.t
+ | ErrorState of Vernacstate.Parser.state option * Exninfo.iexn
type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info
type backup = { mine : branch; others : branch list }
@@ -214,10 +212,16 @@ type 'vcs state_info = { (* TODO: Make this record private to VCS *)
mutable n_reached : int; (* debug cache: how many times was computed *)
mutable n_goals : int; (* open goals: indentation *)
mutable state : cached_state; (* state value *)
+ mutable proof_mode : Pvernac.proof_mode option;
mutable vcs_backup : 'vcs option * backup option;
}
-let default_info () =
- { n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None }
+let default_info proof_mode =
+ {
+ n_reached = 0; n_goals = 0;
+ state = EmptyState;
+ proof_mode;
+ vcs_backup = (None,None);
+ }
module DynBlockData : Dyn.S = Dyn.Make ()
@@ -256,15 +260,15 @@ end = struct (* {{{ *)
List.fold_left max 0
(CList.map_filter
(function
- | { Vcs_.kind = `Proof (_,n) } -> Some n
+ | { Vcs_.kind = `Proof n } -> Some n
| { Vcs_.kind = `Edit _ } -> Some 1
| _ -> None)
(List.map (Vcs_.get_branch vcs) (Vcs_.branches vcs)))
let find_proof_at_depth vcs pl =
try List.find (function
- | _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl
- | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth.")
+ | _, { Vcs_.kind = `Proof n } -> Int.equal n pl
+ | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth")
| _ -> false)
(List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs))
with Not_found -> failwith "find_proof_at_depth"
@@ -326,7 +330,7 @@ module VCS : sig
type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t
- val init : stm_doc_type -> id -> doc
+ val init : stm_doc_type -> id -> Vernacstate.Parser.state -> doc
(* val get_type : unit -> stm_doc_type *)
val set_ldir : Names.DirPath.t -> unit
val get_ldir : unit -> Names.DirPath.t
@@ -339,7 +343,7 @@ module VCS : sig
val branches : unit -> Branch.t list
val get_branch : Branch.t -> branch_type branch_info
val get_branch_pos : Branch.t -> id
- val new_node : ?id:Stateid.t -> unit -> id
+ val new_node : ?id:Stateid.t -> Pvernac.proof_mode option -> unit -> id
val merge : id -> ours:transaction -> ?into:Branch.t -> Branch.t -> unit
val rewrite_merge : id -> ours:transaction -> at:id -> Branch.t -> unit
val delete_branch : Branch.t -> unit
@@ -356,6 +360,10 @@ module VCS : sig
val goals : id -> int -> unit
val set_state : id -> cached_state -> unit
val get_state : id -> cached_state
+ val set_parsing_state : id -> Vernacstate.Parser.state -> unit
+ val get_parsing_state : id -> Vernacstate.Parser.state option
+ val get_proof_mode : id -> Pvernac.proof_mode option
+ val set_proof_mode : id -> Pvernac.proof_mode option -> unit
(* cuts from start -> stop, raising Expired if some nodes are not there *)
val slice : block_start:id -> block_stop:id -> vcs
@@ -369,7 +377,8 @@ module VCS : sig
val proof_nesting : unit -> int
val checkout_shallowest_proof_branch : unit -> unit
- val propagate_sideff : action:seff_t -> unit
+ val propagate_sideff : action:seff_t -> Stateid.t list
+ val propagate_qed : unit -> unit
val gc : unit -> unit
@@ -411,11 +420,11 @@ end = struct (* {{{ *)
| Qed { qast } -> Pp.string_of_ppcmds (pr_ast qast) in
let is_green id =
match get_info vcs id with
- | Some { state = Valid _ } -> true
+ | Some { state = FullState _ } -> true
| _ -> false in
let is_red id =
match get_info vcs id with
- | Some { state = Error _ } -> true
+ | Some { state = ErrorState _ } -> true
| _ -> false in
let head = current_branch vcs in
let heads =
@@ -517,10 +526,11 @@ end = struct (* {{{ *)
let doc_type = ref (Interactive (TopLogical (Names.DirPath.make [])))
let ldir = ref Names.DirPath.empty
- let init dt id =
+ let init dt id ps =
doc_type := dt;
vcs := empty id;
- vcs := set_info !vcs id (default_info ());
+ let info = { (default_info None) with state = ParsingState ps } in
+ vcs := set_info !vcs id info;
dummy_doc
let set_ldir ld =
@@ -545,9 +555,9 @@ end = struct (* {{{ *)
let branches () = branches !vcs
let get_branch head = get_branch !vcs head
let get_branch_pos head = (get_branch head).pos
- let new_node ?(id=Stateid.fresh ()) () =
+ let new_node ?(id=Stateid.fresh ()) proof_mode () =
assert(Vcs_.get_info !vcs id = None);
- vcs := set_info !vcs id (default_info ());
+ vcs := set_info !vcs id (default_info proof_mode);
id
let merge id ~ours ?into branch =
vcs := merge !vcs id ~ours ~theirs:Noop ?into branch
@@ -569,9 +579,39 @@ end = struct (* {{{ *)
| Some x -> x
| None -> raise Vcs_aux.Expired
let set_state id s =
- (get_info id).state <- s;
- if async_proofs_is_master !cur_opt then Hooks.(call state_ready ~doc:dummy_doc (* XXX should be taken in input *) id)
+ let info = get_info id in
+ info.state <- s;
+ let is_full_state_valid = match s with
+ | FullState _ -> true
+ | EmptyState | ErrorState _ | ParsingState _ -> false
+ in
+ if async_proofs_is_master !cur_opt && is_full_state_valid then
+ Hooks.(call state_ready ~doc:dummy_doc (* XXX should be taken in input *) id)
+
let get_state id = (get_info id).state
+
+ let get_parsing_state id =
+ stm_pperr_endline (fun () -> str "retrieve parsing state state " ++ str (Stateid.to_string id) ++ str " }}}");
+ match (get_info id).state with
+ | FullState s -> Some s.Vernacstate.parsing
+ | ParsingState s -> Some s
+ | ErrorState (s,_) -> s
+ | EmptyState -> None
+
+ let set_parsing_state id ps =
+ let info = get_info id in
+ let new_state =
+ match info.state with
+ | FullState s -> assert false
+ | ParsingState s -> assert false
+ | ErrorState _ -> assert false
+ | EmptyState -> ParsingState ps
+ in
+ info.state <- new_state
+
+ let get_proof_mode id = (get_info id).proof_mode
+ let set_proof_mode id pm = (get_info id).proof_mode <- pm
+
let reached id =
let info = get_info id in
info.n_reached <- info.n_reached + 1
@@ -582,28 +622,33 @@ end = struct (* {{{ *)
let checkout_shallowest_proof_branch () =
if List.mem edit_branch (Vcs_.branches !vcs) then begin
- checkout edit_branch;
- match get_branch edit_branch with
- | { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
- | _ -> assert false
+ checkout edit_branch
end else
let pl = proof_nesting () in
try
- let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with
- | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
- checkout branch;
- stm_prerr_endline (fun () -> "mode:" ^ mode);
- Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
+ let branch = fst @@ Vcs_aux.find_proof_at_depth !vcs pl in
+ checkout branch
with Failure _ ->
- checkout Branch.master;
- Proof_global.disactivate_current_proof_mode () [@ocaml.warning "-3"]
+ checkout Branch.master
(* copies the transaction on every open branch *)
let propagate_sideff ~action =
+ List.map (fun b ->
+ checkout b;
+ let proof_mode = get_proof_mode @@ get_branch_pos b in
+ let id = new_node proof_mode () in
+ merge id ~ours:(Sideff action) ~into:b Branch.master;
+ id)
+ (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ()))
+
+ let propagate_qed () =
List.iter (fun b ->
checkout b;
- let id = new_node () in
- merge id ~ours:(Sideff action) ~into:b Branch.master)
+ let proof_mode = get_proof_mode @@ get_branch_pos b in
+ let id = new_node proof_mode () in
+ let parsing = Option.get @@ get_parsing_state (get_branch_pos b) in
+ merge id ~ours:(Sideff CherryPickEnv) ~into:b Branch.master;
+ set_parsing_state id parsing)
(List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ()))
let visit id = Vcs_aux.visit !vcs id
@@ -625,10 +670,12 @@ end = struct (* {{{ *)
let slice ~block_start ~block_stop =
let l = nodes_in_slice ~block_start ~block_stop in
let copy_info v id =
+ let info = get_info id in
Vcs_.set_info v id
- { (get_info id) with state = Empty; vcs_backup = None,None } in
+ { info with state = EmptyState;
+ vcs_backup = None,None } in
let make_shallow = function
- | Valid st -> Valid (Vernacstate.make_shallow st)
+ | FullState st -> FullState (Vernacstate.make_shallow st)
| x -> x
in
let copy_info_w_state v id =
@@ -651,12 +698,14 @@ end = struct (* {{{ *)
let v = copy_info v id in
v) l v in
(* Stm should have reached the beginning of proof *)
- assert (match (get_info block_start).state with Valid _ -> true | _ -> false);
+ assert (match get_state block_start
+ with FullState _ -> true | _ -> false);
(* We put in the new dag the most recent state known to master *)
let rec fill id =
- match (get_info id).state with
- | Empty | Error _ -> fill (Vcs_aux.visit v id).next
- | Valid _ -> copy_info_w_state v id in
+ match get_state id with
+ | EmptyState | ErrorState _ | ParsingState _ -> fill (Vcs_aux.visit v id).next
+ | FullState _ -> copy_info_w_state v id
+ in
let v = fill block_stop in
(* We put in the new dag the first state (since Qed shall run on it,
* see check_task_aux) *)
@@ -753,13 +802,12 @@ end = struct (* {{{ *)
end (* }}} *)
let state_of_id ~doc id =
- try match (VCS.get_info id).state with
- | Valid s -> `Valid (Some s)
- | Error (e,_) -> `Error e
- | Empty -> `Valid None
+ try match VCS.get_state id with
+ | FullState s -> `Valid (Some s)
+ | ErrorState (_,(e,_)) -> `Error e
+ | EmptyState | ParsingState _ -> `Valid None
with VCS.Expired -> `Expired
-
(****** A cache: fills in the nodes of the VCS document with their value ******)
module State : sig
@@ -782,6 +830,7 @@ module State : sig
val fix_exn_ref : (Exninfo.iexn -> Exninfo.iexn) ref
val install_cached : Stateid.t -> unit
+ (* val install_parsing_state : Stateid.t -> unit *)
val is_cached : ?cache:bool -> Stateid.t -> bool
val is_cached_and_valid : ?cache:bool -> Stateid.t -> bool
@@ -804,10 +853,6 @@ module State : sig
val register_root_state : unit -> unit
val restore_root_state : unit -> unit
- (* Only for internal use to catch problems in parse_sentence, should
- be removed in the state handling refactoring. *)
- val cur_id : Stateid.t ref
-
val purify : ('a -> 'b) -> 'a -> 'b
end = struct (* {{{ *)
@@ -824,6 +869,8 @@ end = struct (* {{{ *)
Vernacstate.unfreeze_interp_state st.vernac_state;
cur_id := st.id
+ let invalidate_cur_state () = cur_id := Stateid.dummy
+
type proof_part =
Proof_global.t *
int * (* Evarutil.meta_counter_summary_tag *)
@@ -842,49 +889,58 @@ end = struct (* {{{ *)
Summary.project_from_summary st Util.(pi3 summary_pstate)
let cache_state ~marshallable id =
- VCS.set_state id (Valid (Vernacstate.freeze_interp_state ~marshallable))
+ VCS.set_state id (FullState (Vernacstate.freeze_interp_state ~marshallable))
- let freeze_invalid id iexn = VCS.set_state id (Error iexn)
+ let freeze_invalid id iexn =
+ let ps = VCS.get_parsing_state id in
+ VCS.set_state id (ErrorState (ps,iexn))
let is_cached ?(cache=false) id only_valid =
if Stateid.equal id !cur_id then
try match VCS.get_info id with
- | { state = Empty } when cache -> cache_state ~marshallable:false id; true
+ | ({ state = EmptyState } | { state = ParsingState _ }) when cache -> cache_state ~marshallable:false id; true
| _ -> true
with VCS.Expired -> false
else
- try match VCS.get_info id with
- | { state = Empty } -> false
- | { state = Valid _ } -> true
- | { state = Error _ } -> not only_valid
+ try match VCS.get_state id with
+ | EmptyState | ParsingState _ -> false
+ | FullState _ -> true
+ | ErrorState _ -> not only_valid
with VCS.Expired -> false
let is_cached_and_valid ?cache id = is_cached ?cache id true
let is_cached ?cache id = is_cached ?cache id false
let install_cached id =
- match VCS.get_info id with
- | { state = Valid s } ->
+ match VCS.get_state id with
+ | FullState s ->
Vernacstate.unfreeze_interp_state s;
cur_id := id
- | { state = Error ie } ->
+ | ErrorState (_,ie) ->
Exninfo.iraise ie
- | _ ->
- (* coqc has a 1 slot cache and only for valid states *)
- if not (VCS.is_interactive ()) && Stateid.equal id !cur_id then ()
- else anomaly Pp.(str "installing a non cached state.")
+ | EmptyState | ParsingState _ ->
+ (* coqc has a 1 slot cache and only for valid states *)
+ if (VCS.is_interactive ()) || not (Stateid.equal id !cur_id) then
+ anomaly Pp.(str "installing a non cached state.")
+
+ (*
+ let install_parsing_state id =
+ if not (Stateid.equal id !cur_id) then begin
+ Vernacstate.Parser.install @@ VCS.get_parsing_state id
+ end
+ *)
let get_cached id =
- try match VCS.get_info id with
- | { state = Valid s } -> s
+ try match VCS.get_state id with
+ | FullState s -> s
| _ -> anomaly Pp.(str "not a cached state.")
with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).")
let assign id what =
let open Vernacstate in
- if VCS.get_state id <> Empty then () else
+ if VCS.get_state id <> EmptyState then () else
try match what with
| `Full s ->
let s =
@@ -896,7 +952,7 @@ end = struct (* {{{ *)
~src:(get_cached prev).proof ~tgt:s.proof }
else s
with VCS.Expired -> s in
- VCS.set_state id (Valid s)
+ VCS.set_state id (FullState s)
| `ProofOnly(ontop,(pstate,c1,c2,c3)) ->
if is_cached_and_valid ontop then
let s = get_cached ontop in
@@ -912,7 +968,7 @@ end = struct (* {{{ *)
st
end
} in
- VCS.set_state id (Valid s)
+ VCS.set_state id (FullState s)
with VCS.Expired -> ()
let exn_on id ~valid (e, info) =
@@ -958,7 +1014,7 @@ end = struct (* {{{ *)
with e ->
let (e, info) = CErrors.push e in
let good_id = !cur_id in
- cur_id := Stateid.dummy;
+ invalidate_cur_state ();
VCS.reached id;
let ie =
match Stateid.get info, safe_id with
@@ -1130,7 +1186,7 @@ module Backtrack : sig
val branches_of : Stateid.t -> backup
(* Returns the state that the command should backtract to *)
- val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t * vernac_when
+ val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t
val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
end = struct (* {{{ *)
@@ -1205,30 +1261,30 @@ end = struct (* {{{ *)
try
match Vernacprop.under_control v with
| VernacResetInitial ->
- Stateid.initial, VtNow
+ Stateid.initial
| VernacResetName {CAst.v=name} ->
- let id = VCS.get_branch_pos (VCS.current_branch ()) in
+ let id = VCS.cur_tip () in
(try
let oid =
fold_until (fun b (id,_,label,_,_) ->
if b then `Stop id else `Cont (List.mem name label))
false id in
- oid, VtNow
+ oid
with Not_found ->
- id, VtNow)
+ id)
| VernacBack n ->
- let id = VCS.get_branch_pos (VCS.current_branch ()) in
+ let id = VCS.cur_tip () in
let oid = fold_until (fun n (id,_,_,_,_) ->
if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
- oid, VtNow
+ oid
| VernacUndo n ->
- let id = VCS.get_branch_pos (VCS.current_branch ()) in
+ let id = VCS.cur_tip () in
let oid = fold_until back_tactic n id in
- oid, VtLater
+ oid
| VernacUndoTo _
| VernacRestart as e ->
let m = match e with VernacUndoTo m -> m | _ -> 0 in
- let id = VCS.get_branch_pos (VCS.current_branch ()) in
+ let id = VCS.cur_tip () in
let vcs =
match (VCS.get_info id).vcs_backup with
| None, _ -> anomaly Pp.(str"Backtrack: tip with no vcs_backup.")
@@ -1241,15 +1297,15 @@ end = struct (* {{{ *)
0 id in
let oid = fold_until (fun n (id,_,_,_,_) ->
if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
- oid, VtLater
+ oid
| VernacAbortAll ->
- let id = VCS.get_branch_pos (VCS.current_branch ()) in
+ let id = VCS.cur_tip () in
let oid = fold_until (fun () (id,vcs,_,_,_) ->
match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
() id in
- oid, VtLater
+ oid
| VernacBackTo id ->
- Stateid.of_int id, VtNow
+ Stateid.of_int id
| _ -> anomaly Pp.(str "incorrect VtMeta classification")
with
| Not_found ->
@@ -2331,8 +2387,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
(Proofview.Goal.goal gl) goals_to_admit then
Proofview.give_up else Proofview.tclUNIT ()
end in
- match (VCS.get_info base_state).state with
- | Valid { Vernacstate.proof } ->
+ match VCS.get_state base_state with
+ | FullState { Vernacstate.proof } ->
Proof_global.unfreeze proof;
Proof_global.with_current_proof (fun _ p ->
feedback ~id:id Feedback.AddedAxiom;
@@ -2469,7 +2525,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
VCS.create_proof_task_box nodes ~qed:id ~block_start;
begin match brinfo, qed.fproof with
| { VCS.kind = `Edit _ }, None -> assert false
- | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) ->
+ | { VCS.kind = `Edit (_,_, okeep, _) }, Some (ofp, cancel) ->
assert(redefine_qed = true);
if okeep <> keep then
msg_warning(strbrk("The command closing the proof changed. "
@@ -2655,7 +2711,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
(* We must reset the whole state before creating a document! *)
State.restore_root_state ();
- let doc = VCS.init doc_type Stateid.initial in
+ let doc = VCS.init doc_type Stateid.initial (Vernacstate.Parser.init ()) in
(* Set load path; important, this has to happen before we declare
the library below as [Declaremods/Library] will infer the module
@@ -2723,16 +2779,8 @@ let observe ~doc id =
let finish ~doc =
let head = VCS.current_branch () in
- let doc =observe ~doc (VCS.get_branch_pos head) in
- VCS.print ();
- (* EJGA: Setting here the proof state looks really wrong, and it
- hides true bugs cf bug #5363. Also, what happens with observe? *)
- (* Some commands may by side effect change the proof mode *)
- (match VCS.get_branch head with
- | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
- | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]
- | _ -> ()
- ); doc
+ let doc = observe ~doc (VCS.get_branch_pos head) in
+ VCS.print (); doc
let wait ~doc =
let doc = observe ~doc (VCS.get_branch_pos VCS.Branch.master) in
@@ -2809,12 +2857,14 @@ let merge_proof_branch ~valid ?id qast keep brname =
match brinfo with
| { VCS.kind = `Proof _ } ->
VCS.checkout VCS.Branch.master;
- let id = VCS.new_node ?id () in
+ let id = VCS.new_node ?id None () in
+ let parsing = Option.get @@ VCS.get_parsing_state (VCS.cur_tip ()) in
VCS.merge id ~ours:(Qed (qed None)) brname;
+ VCS.set_parsing_state id parsing;
VCS.delete_branch brname;
- VCS.propagate_sideff ~action:CherryPickEnv;
+ VCS.propagate_qed ();
`Ok
- | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } ->
+ | { VCS.kind = `Edit (qed_id, master_id, _,_) } ->
let ofp =
match VCS.visit qed_id with
| { step = `Qed ({ fproof }, _) } -> fproof
@@ -2846,25 +2896,32 @@ let snapshot_vio ~doc ldir long_f_dot_vo =
let reset_task_queue = Slaves.reset_task_queue
(* Document building *)
-let process_back_meta_command ~newtip ~head oid aast w =
- let id = VCS.new_node ~id:newtip () in
- let { mine; others } = Backtrack.branches_of oid in
+
+(* We process a meta command found in the document *)
+let process_back_meta_command ~newtip ~head oid aast =
let valid = VCS.get_branch_pos head in
+ let old_parsing = Option.get @@ VCS.get_parsing_state oid in
+
+ (* Merge in and discard all the branches currently open that were not open in `oid` *)
+ let { mine; others } = Backtrack.branches_of oid in
List.iter (fun branch ->
if not (List.mem_assoc branch (mine::others)) then
ignore(merge_proof_branch ~valid aast VtDrop branch))
(VCS.branches ());
+
+ (* We add a node on top of every branch, to represent state aliasing *)
VCS.checkout_shallowest_proof_branch ();
let head = VCS.current_branch () in
List.iter (fun b ->
- if not(VCS.Branch.equal b head) then begin
- VCS.checkout b;
- VCS.commit (VCS.new_node ()) (Alias (oid,aast));
- end)
+ VCS.checkout b;
+ let id = if (VCS.Branch.equal b head) then Some newtip else None in
+ let proof_mode = VCS.get_proof_mode @@ VCS.cur_tip () in
+ let id = VCS.new_node ?id proof_mode () in
+ VCS.commit id (Alias (oid,aast));
+ VCS.set_parsing_state id old_parsing)
(VCS.branches ());
VCS.checkout_shallowest_proof_branch ();
- VCS.commit id (Alias (oid,aast));
- Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
+ Backtrack.record (); `Ok
let get_allow_nested_proofs =
Goptions.declare_bool_option_and_ref
@@ -2873,6 +2930,7 @@ let get_allow_nested_proofs =
~key:Vernac_classifier.stm_allow_nested_proofs_option_name
~value:false
+(** [process_transaction] adds a node in the document *)
let process_transaction ~doc ?(newtip=Stateid.fresh ())
({ verbose; loc; expr } as x) c =
stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
@@ -2880,18 +2938,21 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
try
let head = VCS.current_branch () in
VCS.checkout head;
+ let head_parsing =
+ Option.get @@ VCS.(get_parsing_state (get_branch_pos head)) in
+ let proof_mode = VCS.(get_proof_mode (get_branch_pos head)) in
let rc = begin
stm_prerr_endline (fun () ->
" classified as: " ^ Vernac_classifier.string_of_vernac_classification c);
match c with
(* Meta *)
| VtMeta, _ ->
- let id, w = Backtrack.undo_vernac_classifier expr ~doc in
- process_back_meta_command ~newtip ~head id x w
+ let id = Backtrack.undo_vernac_classifier expr ~doc in
+ process_back_meta_command ~newtip ~head id x
(* Query *)
| VtQuery, w ->
- let id = VCS.new_node ~id:newtip () in
+ let id = VCS.new_node ~id:newtip proof_mode () in
let queue =
if VCS.is_vio_doc () &&
VCS.((get_branch head).kind = `Master) &&
@@ -2899,10 +2960,11 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
then `SkipQueue
else `MainQueue in
VCS.commit id (mkTransCmd x [] false queue);
- Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
+ VCS.set_parsing_state id head_parsing;
+ Backtrack.record (); assert (w == VtLater); `Ok
(* Proof *)
- | VtStartProof (mode, guarantee, names), w ->
+ | VtStartProof (guarantee, names), w ->
if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then
"Nested proofs are not allowed unless you turn option Nested Proofs Allowed on."
@@ -2912,39 +2974,22 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
|> Exninfo.iraise
else
- let id = VCS.new_node ~id:newtip () in
+ let proof_mode = Some (Vernacentries.get_default_proof_mode ()) in
+ let id = VCS.new_node ~id:newtip proof_mode () in
let bname = VCS.mk_branch_name x in
VCS.checkout VCS.Branch.master;
if VCS.Branch.equal head VCS.Branch.master then begin
VCS.commit id (Fork (x, bname, guarantee, names));
- VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1))
+ VCS.branch bname (`Proof (VCS.proof_nesting () + 1))
end else begin
- VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1));
+ VCS.branch bname (`Proof (VCS.proof_nesting () + 1));
VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head
end;
- Proof_global.activate_proof_mode mode [@ocaml.warning "-3"];
- Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
- | VtProofMode _, VtLater ->
- anomaly(str"VtProofMode must be executed VtNow.")
- | VtProofMode mode, VtNow ->
- let id = VCS.new_node ~id:newtip () in
- VCS.commit id (mkTransCmd x [] false `MainQueue);
- List.iter
- (fun bn -> match VCS.get_branch bn with
- | { VCS.root; kind = `Master; pos } -> ()
- | { VCS.root; kind = `Proof(_,d); pos } ->
- VCS.delete_branch bn;
- VCS.branch ~root ~pos bn (`Proof(mode,d))
- | { VCS.root; kind = `Edit(_,f,q,k,ob); pos } ->
- VCS.delete_branch bn;
- VCS.branch ~root ~pos bn (`Edit(mode,f,q,k,ob)))
- (VCS.branches ());
- VCS.checkout_shallowest_proof_branch ();
- Backtrack.record ();
- ignore(finish ~doc:dummy_doc);
- `Ok
+ VCS.set_parsing_state id head_parsing;
+ Backtrack.record (); assert (w == VtLater); `Ok
+
| VtProofStep { parallel; proof_block_detection = cblock }, w ->
- let id = VCS.new_node ~id:newtip () in
+ let id = VCS.new_node ~id:newtip proof_mode () in
let queue =
match parallel with
| `Yes(solve,abstract) -> `TacQueue (solve, abstract, ref false)
@@ -2954,21 +2999,25 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
If/when and UI will make something useful with this piece of info,
detection should occur here.
detect_proof_block id cblock; *)
- Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
+ VCS.set_parsing_state id head_parsing;
+ Backtrack.record (); assert (w == VtLater); `Ok
+
| VtQed keep, w ->
let valid = VCS.get_branch_pos head in
- let rc = merge_proof_branch ~valid ~id:newtip x keep head in
+ let rc =
+ merge_proof_branch ~valid ~id:newtip x keep head in
VCS.checkout_shallowest_proof_branch ();
- Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc);
+ Backtrack.record (); assert (w == VtLater);
rc
(* Side effect in a (still open) proof is replayed on all branches*)
| VtSideff l, w ->
- let id = VCS.new_node ~id:newtip () in
- begin match (VCS.get_branch head).VCS.kind with
- | `Edit _ -> VCS.commit id (mkTransCmd x l true `MainQueue);
- | `Master -> VCS.commit id (mkTransCmd x l false `MainQueue);
- | `Proof _ ->
+ let id = VCS.new_node ~id:newtip proof_mode () in
+ let new_ids =
+ match (VCS.get_branch head).VCS.kind with
+ | `Edit _ -> VCS.commit id (mkTransCmd x l true `MainQueue); []
+ | `Master -> VCS.commit id (mkTransCmd x l false `MainQueue); []
+ | `Proof _ ->
VCS.checkout VCS.Branch.master;
VCS.commit id (mkTransCmd x l true `MainQueue);
(* We can't replay a Definition since universes may be differently
@@ -2976,10 +3025,27 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
let action = match Vernacprop.under_control x.expr with
| VernacDefinition(_, _, DefineBody _) -> CherryPickEnv
| _ -> ReplayCommand x in
- VCS.propagate_sideff ~action;
- end;
+ VCS.propagate_sideff ~action
+ in
VCS.checkout_shallowest_proof_branch ();
- Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
+ Backtrack.record ();
+ let parsing_state =
+ begin match w with
+ | VtNow ->
+ (* We need to execute to get the new parsing state *)
+ ignore(finish ~doc:dummy_doc);
+ let parsing = Vernacstate.Parser.cur_state () in
+ (* If execution has not been put in cache, we need to save the parsing state *)
+ if (VCS.get_info id).state == EmptyState then VCS.set_parsing_state id parsing;
+ parsing
+ | VtLater -> VCS.set_parsing_state id head_parsing; head_parsing
+ end
+ in
+ (* We save the parsing state on non-master branches *)
+ List.iter (fun id ->
+ if (VCS.get_info id).state == EmptyState then
+ VCS.set_parsing_state id parsing_state) new_ids;
+ `Ok
(* Unknown: we execute it, check for open goals and propagate sideeff *)
| VtUnknown, VtNow ->
@@ -2991,7 +3057,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
|> State.exn_on ~valid:Stateid.dummy Stateid.dummy
|> Exninfo.iraise
else
- let id = VCS.new_node ~id:newtip () in
+ let id = VCS.new_node ~id:newtip proof_mode () in
let head_id = VCS.get_branch_pos head in
let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *)
let step () =
@@ -3009,9 +3075,8 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
| VernacInstance (_,_ , None, _) -> GuaranteesOpacity
| _ -> Doesn'tGuaranteeOpacity in
VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[]));
- let proof_mode = default_proof_mode () in
- VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1));
- Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
+ VCS.set_proof_mode id (Some (Vernacentries.get_default_proof_mode ()));
+ VCS.branch bname (`Proof (VCS.proof_nesting () + 1));
end else begin
begin match (VCS.get_branch head).VCS.kind with
| `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
@@ -3019,7 +3084,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
| `Proof _ ->
VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
(* We hope it can be replayed, but we can't really know *)
- VCS.propagate_sideff ~action:(ReplayCommand x);
+ ignore(VCS.propagate_sideff ~action:(ReplayCommand x));
end;
VCS.checkout_shallowest_proof_branch ();
end in
@@ -3028,6 +3093,17 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
| VtUnknown, VtLater ->
anomaly(str"classifier: VtUnknown must imply VtNow.")
+
+ | VtProofMode pm, VtNow ->
+ let proof_mode = Pvernac.lookup_proof_mode pm in
+ let id = VCS.new_node ~id:newtip proof_mode () in
+ VCS.commit id (mkTransCmd x [] false `MainQueue);
+ VCS.set_parsing_state id head_parsing;
+ Backtrack.record (); `Ok
+
+ | VtProofMode _, VtLater ->
+ anomaly(str"classifier: VtProofMode must imply VtNow.")
+
end in
let pr_rc rc = match rc with
| `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"])
@@ -3051,45 +3127,10 @@ let get_ast ~doc id =
let stop_worker n = Slaves.cancel_worker n
-(* We must parse on top of a state id, it should be something like:
-
- - get parsing information for that state.
- - feed the parsable / parser with the right parsing information.
- - call the parser
-
- Now, the invariant in ensured by the callers, but this is a bit
- problematic.
-*)
-exception End_of_input
-
-let parse_sentence ~doc sid pa =
- (* XXX: Should this restore the previous state?
- Using reach here to try to really get to the
- proper state makes the error resilience code fail *)
- (* Reach.known_state ~cache:`Yes sid; *)
- let cur_tip = VCS.cur_tip () in
- let real_tip = !State.cur_id in
- if not (Stateid.equal sid cur_tip) then
- user_err ~hdr:"Stm.parse_sentence"
- (str "Currently, the parsing api only supports parsing at the tip of the document." ++ fnl () ++
- str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++
- str " but the current tip is: " ++ str (Stateid.to_string cur_tip)) ;
- if not (Stateid.equal sid real_tip) && !Flags.debug && !stm_debug then
- Feedback.msg_debug
- (str "Warning, the real tip doesn't match the current tip." ++
- str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++
- str " but the real tip is: " ++ str (Stateid.to_string real_tip) ++ fnl () ++
- str "This is usually due to use of Stm.observe to evaluate a state different than the tip. " ++
- str "All is good if not parsing changes occur between the two states, however if they do, a problem might occur.");
- Flags.with_option Flags.we_are_parsing (fun () ->
- try
- match Pcoq.Entry.parse Pvernac.main_entry pa with
- | None -> raise End_of_input
- | Some (loc, cmd) -> CAst.make ~loc cmd
- with e when CErrors.noncritical e ->
- let (e, info) = CErrors.push e in
- Exninfo.iraise (e, info))
- ()
+let parse_sentence ~doc sid ~entry pa =
+ let ps = Option.get @@ VCS.get_parsing_state sid in
+ let proof_mode = VCS.get_proof_mode sid in
+ Vernacstate.Parser.parse ps (entry proof_mode) pa
(* You may need to know the len + indentation of previous command to compute
* the indentation of the current one.
@@ -3153,20 +3194,20 @@ let query ~doc ~at ~route s =
State.purify (fun s ->
if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc)
else Reach.known_state ~doc ~cache:true at;
- try
- while true do
- let { CAst.loc; v=ast } = parse_sentence ~doc at s in
- let indentation, strlen = compute_indentation ?loc at in
- let st = State.get_cached at in
- let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
- ignore(stm_vernac_interp ~route at st aast)
- done;
- with
- | End_of_input -> ()
- | exn ->
- let iexn = CErrors.push exn in
- Exninfo.iraise iexn
- )
+ let rec loop () =
+ match parse_sentence ~doc at ~entry:Pvernac.main_entry s with
+ | None -> ()
+ | Some (loc, ast) ->
+ let indentation, strlen = compute_indentation ~loc at in
+ let st = State.get_cached at in
+ let aast = {
+ verbose = true; indentation; strlen;
+ loc = Some loc; expr = ast } in
+ ignore(stm_vernac_interp ~route at st aast);
+ loop ()
+ in
+ loop ()
+ )
s
let edit_at ~doc id =
@@ -3204,21 +3245,21 @@ let edit_at ~doc id =
| { step = `Sideff (ReplayCommand _,id) } -> id
| { step = `Sideff _ } -> tip
| { next } -> master_for_br root next in
- let reopen_branch start at_id mode qed_id tip old_branch =
+ let reopen_branch start at_id qed_id tip old_branch =
let master_id, cancel_switch, keep =
(* Hum, this should be the real start_id in the cluster and not next *)
match VCS.visit qed_id with
| { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep
| _ -> anomaly (str "ProofTask not ending with Qed.") in
VCS.branch ~root:master_id ~pos:id
- VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch));
+ VCS.edit_branch (`Edit (qed_id, master_id, keep, old_branch));
VCS.delete_boxes_of id;
cancel_switch := true;
Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id;
VCS.checkout_shallowest_proof_branch ();
`Focus { stop = qed_id; start = master_id; tip } in
let no_edit = function
- | `Edit (pm, _,_,_,_) -> `Proof(pm,1)
+ | `Edit (_,_,_,_) -> `Proof 1
| x -> x in
let backto id bn =
List.iter VCS.delete_branch (VCS.branches ());
@@ -3244,17 +3285,17 @@ let edit_at ~doc id =
let focused = List.exists ((=) VCS.edit_branch) (VCS.branches ()) in
let branch_info =
match snd (VCS.get_info id).vcs_backup with
- | Some{ mine = bn, { VCS.kind = `Proof(m,_) }} -> Some(m,bn)
- | Some{ mine = _, { VCS.kind = `Edit(m,_,_,_,bn) }} -> Some (m,bn)
+ | Some{ mine = bn, { VCS.kind = `Proof _ }} -> Some bn
+ | Some{ mine = _, { VCS.kind = `Edit(_,_,_,bn) }} -> Some bn
| _ -> None in
match focused, VCS.proof_task_box_of id, branch_info with
| _, Some _, None -> assert false
- | false, Some { qed = qed_id ; lemma = start }, Some(mode,bn) ->
+ | false, Some { qed = qed_id ; lemma = start }, Some bn ->
let tip = VCS.cur_tip () in
if has_failed qed_id && is_pure qed_id && not !cur_opt.async_proofs_never_reopen_branch
- then reopen_branch start id mode qed_id tip bn
+ then reopen_branch start id qed_id tip bn
else backto id (Some bn)
- | true, Some { qed = qed_id }, Some(mode,bn) ->
+ | true, Some { qed = qed_id }, Some bn ->
if on_cur_branch id then begin
assert false
end else if is_ancestor_of_cur_branch id then begin
@@ -3273,7 +3314,7 @@ let edit_at ~doc id =
end else begin
anomaly(str"Cannot leave an `Edit branch open.")
end
- | false, None, Some(_,bn) -> backto id (Some bn)
+ | false, None, Some bn -> backto id (Some bn)
| false, None, None -> backto id None
in
VCS.print ();
diff --git a/stm/stm.mli b/stm/stm.mli
index b6071fa56b..821ab59a43 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -93,16 +93,17 @@ val init_core : unit -> unit
(** [new_doc opt] Creates a new document with options [opt] *)
val new_doc : stm_init_options -> doc * Stateid.t
-(** [parse_sentence sid pa] Reads a sentence from [pa] with parsing
- state [sid] Returns [End_of_input] if the stream ends *)
-val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Parsable.t ->
- Vernacexpr.vernac_control CAst.t
+(** [parse_sentence sid entry pa] Reads a sentence from [pa] with parsing state
+ [sid] and non terminal [entry]. [entry] receives in input the current proof
+ mode. [sid] should be associated with a valid parsing state (which may not
+ be the case if an error was raised at parsing time). *)
+val parse_sentence :
+ doc:doc -> Stateid.t ->
+ entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.Parsable.t -> 'a
(* Reminder: A parsable [pa] is constructed using
[Pcoq.Parsable.t stream], where [stream : char Stream.t]. *)
-exception End_of_input
-
(* [add ~ontop ?newtip verbose cmd] adds a new command [cmd] ontop of
the state [ontop].
The [ontop] parameter just asserts that the GUI is on
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 09f531ce13..710ddb5571 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -15,8 +15,6 @@ open CAst
open Vernacextend
open Vernacexpr
-let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
-
let string_of_parallel = function
| `Yes (solve,abs) ->
"par" ^ if solve then "solve" else "" ^ if abs then "abs" else ""
@@ -32,9 +30,9 @@ let string_of_vernac_type = function
| VtProofStep { parallel; proof_block_detection } ->
"ProofStep " ^ string_of_parallel parallel ^
Option.default "" proof_block_detection
- | VtProofMode s -> "ProofMode " ^ s
| VtQuery -> "Query"
| VtMeta -> "Meta "
+ | VtProofMode _ -> "Proof Mode"
let string_of_vernac_when = function
| VtLater -> "Later"
@@ -57,7 +55,7 @@ let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"]
let options_affecting_stm_scheduling =
[ Attributes.universe_polymorphism_option_name;
stm_allow_nested_proofs_option_name;
- Proof_global.proof_mode_opt_name;
+ Vernacentries.proof_mode_opt_name;
]
let classify_vernac e =
@@ -97,15 +95,15 @@ let classify_vernac e =
| VernacSetOption (_, ["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
(* StartProof *)
| VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) ->
- VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
+ VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
| VernacDefinition (_,({v=i},_),ProveBody _) ->
let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
- VtStartProof(default_proof_mode (),guarantee, idents_of_name i), VtLater
+ VtStartProof(guarantee, idents_of_name i), VtLater
| VernacStartTheoremProof (_,l) ->
let ids = List.map (fun (({v=i}, _), _) -> i) l in
let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
- VtStartProof (default_proof_mode (),guarantee,ids), VtLater
+ VtStartProof (guarantee,ids), VtLater
| VernacFixpoint (discharge,l) ->
let guarantee =
if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
@@ -115,7 +113,7 @@ let classify_vernac e =
List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
- then VtStartProof (default_proof_mode (),guarantee,ids), VtLater
+ then VtStartProof (guarantee,ids), VtLater
else VtSideff ids, VtLater
| VernacCoFixpoint (discharge,l) ->
let guarantee =
@@ -126,7 +124,7 @@ let classify_vernac e =
List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
- then VtStartProof (default_proof_mode (),guarantee,ids), VtLater
+ then VtStartProof (guarantee,ids), VtLater
else VtSideff ids, VtLater
(* Sideff: apply to all open branches. usually run on master only *)
| VernacAssumption (_,_,l) ->
@@ -184,8 +182,8 @@ let classify_vernac e =
| VernacSyntacticDefinition _
| VernacRequire _ | VernacImport _ | VernacInclude _
| VernacDeclareMLModule _
- | VernacContext _ (* TASSI: unsure *)
- | VernacProofMode _ -> VtSideff [], VtNow
+ | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow
+ | VernacProofMode pm -> VtProofMode pm, VtNow
(* These are ambiguous *)
| VernacInstance _ -> VtUnknown, VtNow
(* Stm will install a new classifier to handle these *)
@@ -211,10 +209,10 @@ let classify_vernac e =
| VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
(match static_control_classifier e with
| ( VtQuery | VtProofStep _ | VtSideff _
- | VtProofMode _ | VtMeta), _ as x -> x
+ | VtMeta), _ as x -> x
| VtQed _, _ ->
VtProofStep { parallel = `No; proof_block_detection = None },
- VtNow
- | (VtStartProof _ | VtUnknown), _ -> VtQuery, VtLater)
+ VtLater
+ | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater)
in
static_control_classifier e
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index e58b9ccac7..cdbe444e5b 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -243,7 +243,7 @@ let set_prompt prompt =
let parse_to_dot =
let rec dot st = match Stream.next st with
| Tok.KEYWORD ("."|"...") -> ()
- | Tok.EOI -> raise Stm.End_of_input
+ | Tok.EOI -> ()
| _ -> dot st
in
Pcoq.Entry.of_parser "Coqtoplevel.dot" dot
@@ -257,12 +257,12 @@ let rec discard_to_dot () =
Pcoq.Entry.parse parse_to_dot top_buffer.tokens
with
| Gramlib.Plexing.Error _ | CLexer.Error.E _ -> discard_to_dot ()
- | Stm.End_of_input -> raise Stm.End_of_input
| e when CErrors.noncritical e -> ()
let read_sentence ~state input =
(* XXX: careful with ignoring the state Eugene!*)
- try G_toplevel.parse_toplevel input
+ let open Vernac.State in
+ try Stm.parse_sentence ~doc:state.doc state.sid ~entry:G_toplevel.vernac_toplevel input
with reraise ->
let reraise = CErrors.push reraise in
discard_to_dot ();
@@ -366,7 +366,6 @@ let top_goal_print ~doc c oldp newp =
let msg = CErrors.iprint (e, info) in
TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer
-(* Careful to keep this loop tail-rec *)
let rec vernac_loop ~state =
let open CAst in
let open Vernac.State in
@@ -379,26 +378,30 @@ let rec vernac_loop ~state =
try
let input = top_buffer.tokens in
match read_sentence ~state input with
- | {v=VernacBacktrack(bid,_,_)} ->
+ | Some { v = VernacBacktrack(bid,_,_) } ->
let bid = Stateid.of_int bid in
let doc, res = Stm.edit_at ~doc:state.doc bid in
assert (res = `NewTip);
let state = { state with doc; sid = bid } in
vernac_loop ~state
- | {v=VernacQuit} ->
+ | Some { v = VernacQuit } ->
exit 0
- | {v=VernacDrop} ->
+
+ | Some { v = VernacDrop } ->
if Mltop.is_ocaml_top()
then (drop_last_doc := Some state; state)
else (Feedback.msg_warning (str "There is no ML toplevel."); vernac_loop ~state)
- | {v=VernacControl c; loc} ->
+
+ | Some { v = VernacControl c; loc } ->
let nstate = Vernac.process_expr ~state (make ?loc c) in
top_goal_print ~doc:state.doc c state.proof nstate.proof;
vernac_loop ~state:nstate
+
+ | None ->
+ top_stderr (fnl ()); exit 0
+
with
- | Stm.End_of_input ->
- top_stderr (fnl ()); exit 0
(* Exception printing should be done by the feedback listener,
however this is not yet ready so we rely on the exception for
now. *)
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index 5aba3d6b0b..7f1cca277e 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -21,7 +21,7 @@ type vernac_toplevel =
| VernacControl of vernac_control
module Toplevel_ : sig
- val vernac_toplevel : vernac_toplevel CAst.t Entry.t
+ val vernac_toplevel : vernac_toplevel CAst.t option Entry.t
end = struct
let gec_vernac s = Entry.create ("toplevel:" ^ s)
let vernac_toplevel = gec_vernac "vernac_toplevel"
@@ -34,14 +34,14 @@ open Toplevel_
GRAMMAR EXTEND Gram
GLOBAL: vernac_toplevel;
vernac_toplevel: FIRST
- [ [ IDENT "Drop"; "." -> { CAst.make VernacDrop }
- | IDENT "Quit"; "." -> { CAst.make VernacQuit }
+ [ [ IDENT "Drop"; "." -> { Some (CAst.make VernacDrop) }
+ | IDENT "Quit"; "." -> { Some (CAst.make VernacQuit) }
| IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." ->
- { CAst.make (VernacBacktrack (n,m,p)) }
- | cmd = Pvernac.main_entry ->
+ { Some (CAst.make (VernacBacktrack (n,m,p))) }
+ | cmd = Pvernac.Vernac_.main_entry ->
{ match cmd with
- | None -> raise Stm.End_of_input
- | Some (loc,c) -> CAst.make ~loc (VernacControl c) }
+ | None -> None
+ | Some (loc,c) -> Some (CAst.make ~loc (VernacControl c)) }
]
]
;
@@ -49,6 +49,8 @@ END
{
-let parse_toplevel pa = Pcoq.Entry.parse vernac_toplevel pa
+let vernac_toplevel pm =
+ Pvernac.Unsafe.set_tactic_entry pm;
+ vernac_toplevel
}
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index d8465aac27..45ca658857 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -68,10 +68,8 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) =
if ntip <> `NewTip then
anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!");
- (* Due to bug #5363 we cannot use observe here as we should,
- it otherwise reveals bugs *)
- (* Stm.observe nsid; *)
- let ndoc = if check then Stm.finish ~doc else doc in
+ (* Force the command *)
+ let ndoc = if check then Stm.observe ~doc nsid else doc in
let new_proof = Proof_global.give_me_the_proof_opt () in
{ state with doc = ndoc; sid = nsid; proof = new_proof; }
with reraise ->
@@ -92,51 +90,37 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
let in_echo = if echo then Some (open_utf8_file_in file) else None in
let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in
- let in_pa = Pcoq.Parsable.make ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
- let rstate = ref state in
- (* For beautify, list of parsed sids *)
- let rids = ref [] in
+ let in_pa =
+ Pcoq.Parsable.make ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
let open State in
- try
- (* we go out of the following infinite loop when a End_of_input is
- * raised, which means that we raised the end of the file being loaded *)
- while true do
- let { CAst.loc; _ } as ast =
- Stm.parse_sentence ~doc:!rstate.doc !rstate.sid in_pa
- (* If an error in parsing occurs, we propagate the exception
- so the caller of load_vernac will take care of it. However,
- in the future it could be possible that we want to handle
- all the errors as feedback events, thus in this case we
- should relay the exception here for convenience. A
- possibility is shown below, however we may want to refactor
- this code:
-
- try Stm.parse_sentence !rsid in_pa
- with
- | any when not is_end_of_input any ->
- let (e, info) = CErrors.push any in
- let loc = Loc.get_loc info in
- let msg = CErrors.iprint (e, info) in
- Feedback.msg_error ?loc msg;
- iraise (e, info)
- *)
- in
- (* Printing of vernacs *)
- Option.iter (vernac_echo ?loc) in_echo;
-
- checknav_simple ast;
- let state = Flags.silently (interp_vernac ~check ~interactive ~state:!rstate) ast in
- rids := state.sid :: !rids;
- rstate := state;
- done;
- input_cleanup ();
- !rstate, !rids, Pcoq.Parsable.comment_state in_pa
+
+ (* ids = For beautify, list of parsed sids *)
+ let rec loop state ids =
+ match
+ Stm.parse_sentence
+ ~doc:state.doc ~entry:Pvernac.main_entry state.sid in_pa
+ with
+ | None ->
+ input_cleanup ();
+ state, ids, Pcoq.Parsable.comment_state in_pa
+ | Some (loc, ast) ->
+ let ast = CAst.make ~loc ast in
+
+ (* Printing of AST for -compile-verbose *)
+ Option.iter (vernac_echo ~loc) in_echo;
+
+ checknav_simple ast;
+
+ let state =
+ Flags.silently (interp_vernac ~check ~interactive ~state) ast in
+
+ loop state (state.sid :: ids)
+ in
+ try loop state []
with any -> (* whatever the exception *)
let (e, info) = CErrors.push any in
input_cleanup ();
- match e with
- | Stm.End_of_input -> !rstate, !rids, Pcoq.Parsable.comment_state in_pa
- | reraise -> iraise (e, info)
+ iraise (e, info)
let process_expr ~state loc_ast =
checknav_deep loc_ast;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 8f155adb8a..0dfbba0e83 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -340,7 +340,7 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c
| None -> standard_proof_terminator ?hook compute_guard
| Some terminator -> terminator ?hook compute_guard
in
- let sign =
+ let sign =
match sign with
| Some sign -> sign
| None -> initialize_named_context_for_proof ()
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index a647b2ef73..0e46df2320 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -12,6 +12,27 @@ open Pcoq
let uvernac = create_universe "vernac"
+type proof_mode = string
+
+(* Tactic parsing modes *)
+let register_proof_mode, find_proof_mode, lookup_proof_mode =
+ let proof_mode : (string, Vernacexpr.vernac_expr Entry.t) Hashtbl.t =
+ Hashtbl.create 19 in
+ let register_proof_mode ename e = Hashtbl.add proof_mode ename e; ename in
+ let find_proof_mode ename =
+ try Hashtbl.find proof_mode ename
+ with Not_found ->
+ CErrors.anomaly Pp.(str "proof mode not found: " ++ str ename) in
+ let lookup_proof_mode name =
+ if Hashtbl.mem proof_mode name then Some name
+ else None
+ in
+ register_proof_mode, find_proof_mode, lookup_proof_mode
+
+let proof_mode_to_string name = name
+
+let command_entry_ref = ref None
+
module Vernac_ =
struct
let gec_vernac s = Entry.create ("vernac:" ^ s)
@@ -39,17 +60,24 @@ module Vernac_ =
] in
Pcoq.grammar_extend main_entry None (None, [None, None, rule])
- let command_entry_ref = ref noedit_mode
+ let select_tactic_entry spec =
+ match spec with
+ | None -> noedit_mode
+ | Some ename -> find_proof_mode ename
+
let command_entry =
Pcoq.Entry.of_parser "command_entry"
- (fun strm -> Pcoq.Entry.parse_token_stream !command_entry_ref strm)
+ (fun strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm)
end
-let main_entry = Vernac_.main_entry
+module Unsafe = struct
+ let set_tactic_entry oname = command_entry_ref := oname
+end
-let set_command_entry e = Vernac_.command_entry_ref := e
-let get_command_entry () = !Vernac_.command_entry_ref
+let main_entry proof_mode =
+ Unsafe.set_tactic_entry proof_mode;
+ Vernac_.main_entry
let () =
register_grammar Genredexpr.wit_red_expr (Vernac_.red_expr);
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index b2f8f71462..fa251281dc 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -14,6 +14,8 @@ open Vernacexpr
val uvernac : gram_universe
+type proof_mode
+
module Vernac_ :
sig
val gallina : vernac_expr Entry.t
@@ -24,13 +26,31 @@ module Vernac_ :
val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
val noedit_mode : vernac_expr Entry.t
val command_entry : vernac_expr Entry.t
+ val main_entry : (Loc.t * vernac_control) option Entry.t
val red_expr : raw_red_expr Entry.t
val hint_info : Hints.hint_info_expr Entry.t
end
+(* To be removed when the parser is made functional wrt the tactic
+ * non terminal *)
+module Unsafe : sig
+ (* To let third party grammar entries reuse Vernac_ and
+ * do something with the proof mode *)
+ val set_tactic_entry : proof_mode option -> unit
+end
+
(** The main entry: reads an optional vernac command *)
-val main_entry : (Loc.t * vernac_control) option Entry.t
+val main_entry : proof_mode option -> (Loc.t * vernac_control) option Entry.t
+
+(** Grammar entry for tactics: proof mode(s).
+ By default Coq's grammar has an empty entry (non-terminal) for
+ tactics. A plugin can register its non-terminal by providing a name
+ and a grammar entry.
+
+ For example the Ltac plugin register the "Classic" grammar
+ entry for parsing its tactics.
+ *)
-(** Handling of the proof mode entry *)
-val get_command_entry : unit -> vernac_expr Entry.t
-val set_command_entry : vernac_expr Entry.t -> unit
+val register_proof_mode : string -> Vernacexpr.vernac_expr Entry.t -> proof_mode
+val lookup_proof_mode : string -> proof_mode option
+val proof_mode_to_string : proof_mode -> string
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 26859cd2cf..996fe320f9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -489,6 +489,28 @@ let vernac_notation ~module_local =
let vernac_custom_entry ~module_local s =
Metasyntax.declare_custom_entry module_local s
+(* Default proof mode, to be set at the beginning of proofs for
+ programs that cannot be statically classified. *)
+let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode)
+let get_default_proof_mode () = !default_proof_mode
+
+let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode
+let set_default_proof_mode_opt name =
+ default_proof_mode :=
+ match Pvernac.lookup_proof_mode name with
+ | Some pm -> pm
+ | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name))
+
+let proof_mode_opt_name = ["Default";"Proof";"Mode"]
+let () =
+ Goptions.declare_string_option Goptions.{
+ optdepr = false;
+ optname = "default proof mode" ;
+ optkey = proof_mode_opt_name;
+ optread = get_default_proof_mode_opt;
+ optwrite = set_default_proof_mode_opt;
+ }
+
(***********)
(* Gallina *)
@@ -2115,13 +2137,9 @@ exception End_of_input
let vernac_load interp fname =
if Proof_global.there_are_pending_proofs () then
CErrors.user_err Pp.(str "Load is not supported inside proofs.");
- let interp x =
- let proof_mode = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] in
- Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"];
- interp x in
- let parse_sentence = Flags.with_option Flags.we_are_parsing
+ let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing
(fun po ->
- match Pcoq.Entry.parse Pvernac.main_entry po with
+ match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with
| Some x -> x
| None -> raise End_of_input) in
let fname =
@@ -2132,7 +2150,15 @@ let vernac_load interp fname =
let in_chan = open_utf8_file_in longfname in
Pcoq.Parsable.make ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
begin
- try while true do interp (snd (parse_sentence input)) done
+ try while true do
+ let proof_mode =
+ if Proof_global.there_are_pending_proofs () then
+ Some (get_default_proof_mode ())
+ else
+ None
+ in
+ interp (snd (parse_sentence proof_mode input));
+ done
with End_of_input -> ()
end;
(* If Load left a proof open, we fail too. *)
@@ -2312,8 +2338,7 @@ let interp ?proof ~atts ~st c =
Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings);
Option.iter vernac_set_end_tac tac;
Option.iter vernac_set_used_variables using
- | VernacProofMode mn -> unsupported_attributes atts;
- Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
+ | VernacProofMode mn -> unsupported_attributes atts; ()
(* Extensions *)
| VernacExtend (opn,args) ->
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 8d8d7cfcf0..4fbd3849b0 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -10,6 +10,11 @@
val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit
+(** Default proof mode set by `start_proof` *)
+val get_default_proof_mode : unit -> Pvernac.proof_mode
+
+val proof_mode_opt_name : string list
+
(** Vernacular entries *)
val vernac_require :
Libnames.qualid option -> bool option -> Libnames.qualid list -> unit
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 05687afd8b..f5cf3401d0 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -29,15 +29,15 @@ type vernac_type =
parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
proof_block_detection : proof_block_name option
}
- (* To be removed *)
- | VtProofMode of string
(* Queries are commands assumed to be "pure", that is to say, they
don't modify the interpretation state. *)
| VtQuery
+ (* Commands that change the current proof mode *)
+ | VtProofMode of string
(* To be removed *)
| VtMeta
| VtUnknown
-and vernac_start = string * opacity_guarantee * Names.Id.t list
+and vernac_start = opacity_guarantee * Names.Id.t list
and vernac_sideff_type = Names.Id.t list
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 0d43eb1ee8..118907c31b 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -45,15 +45,15 @@ type vernac_type =
parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
proof_block_detection : proof_block_name option
}
- (* To be removed *)
- | VtProofMode of string
(* Queries are commands assumed to be "pure", that is to say, they
don't modify the interpretation state. *)
| VtQuery
+ (* Commands that change the current proof mode *)
+ | VtProofMode of string
(* To be removed *)
| VtMeta
| VtUnknown
-and vernac_start = string * opacity_guarantee * Names.Id.t list
+and vernac_start = opacity_guarantee * Names.Id.t list
and vernac_sideff_type = Names.Id.t list
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 61540024ef..c691dc8559 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -8,10 +8,30 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+module Parser = struct
+
+ type state = Pcoq.frozen_t
+
+ let init () = Pcoq.freeze ~marshallable:false
+
+ let cur_state () = Pcoq.freeze ~marshallable:false
+
+ let parse ps entry pa =
+ Pcoq.unfreeze ps;
+ Flags.with_option Flags.we_are_parsing (fun () ->
+ try Pcoq.Entry.parse entry pa
+ with e when CErrors.noncritical e ->
+ let (e, info) = CErrors.push e in
+ Exninfo.iraise (e, info))
+ ()
+
+end
+
type t = {
- system : States.state; (* summary + libstack *)
- proof : Proof_global.t; (* proof state *)
- shallow : bool (* is the state trimmed down (libstack) *)
+ parsing: Parser.state;
+ system : States.state; (* summary + libstack *)
+ proof : Proof_global.t; (* proof state *)
+ shallow : bool; (* is the state trimmed down (libstack) *)
}
let s_cache = ref None
@@ -37,11 +57,13 @@ let freeze_interp_state ~marshallable =
{ system = update_cache s_cache (States.freeze ~marshallable);
proof = update_cache s_proof (Proof_global.freeze ~marshallable);
shallow = false;
+ parsing = Parser.cur_state ();
}
-let unfreeze_interp_state { system; proof } =
+let unfreeze_interp_state { system; proof; parsing } =
do_if_not_cached s_cache States.unfreeze system;
- do_if_not_cached s_proof Proof_global.unfreeze proof
+ do_if_not_cached s_proof Proof_global.unfreeze proof;
+ Pcoq.unfreeze parsing
let make_shallow st =
let lib = States.lib_of_state st.system in
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index ed20cb935a..581c23386a 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -8,10 +8,21 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+module Parser : sig
+ type state
+
+ val init : unit -> state
+ val cur_state : unit -> state
+
+ val parse : state -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a
+
+end
+
type t = {
- system : States.state; (* summary + libstack *)
- proof : Proof_global.t; (* proof state *)
- shallow : bool (* is the state trimmed down (libstack) *)
+ parsing: Parser.state;
+ system : States.state; (* summary + libstack *)
+ proof : Proof_global.t; (* proof state *)
+ shallow : bool; (* is the state trimmed down (libstack) *)
}
val freeze_interp_state : marshallable:bool -> t
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:31:01 +0000