aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/proofBlockDelimiter.ml4
-rw-r--r--stm/stm.ml117
-rw-r--r--stm/vernac_classifier.ml2
3 files changed, 47 insertions, 76 deletions
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 2ff76e69f8..3d892fa5ca 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -49,8 +49,8 @@ let is_focused_goal_simple ~doc id =
match state_of_id ~doc id with
| `Expired | `Error _ | `Valid None -> `Not
| `Valid (Some { Vernacstate.lemmas }) ->
- Option.cata (Vernacstate.LemmaStack.with_top_pstate ~f:(fun proof ->
- let proof = Declare.Proof.get_proof proof in
+ Option.cata (Vernacstate.LemmaStack.with_top ~f:(fun proof ->
+ let proof = Declare.Proof.get proof in
let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in
let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
if List.for_all (fun x -> simple_goal sigma x rest) focused
diff --git a/stm/stm.ml b/stm/stm.ml
index b72cee7a9d..3b7921f638 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -147,7 +147,7 @@ let update_global_env () =
PG_compat.update_global_env ()
module Vcs_ = Vcs.Make(Stateid.Self)
-type future_proof = Declare.closed_proof_output Future.computation
+type future_proof = Declare.Proof.closed_proof_output Future.computation
type depth = int
type branch_type =
@@ -199,16 +199,11 @@ let mkTransTac cast cblock cqueue =
let mkTransCmd cast cids ceff cqueue =
Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff }
-(* Parts of the system state that are morally part of the proof state *)
-let summary_pstate = Evarutil.meta_counter_summary_tag,
- Evd.evar_counter_summary_tag,
- Declare.Obls.State.prg_tag
-
type cached_state =
| EmptyState
- | ParsingState of Vernacstate.Parser.state
+ | ParsingState of Vernacstate.Parser.t
| FullState of Vernacstate.t
- | ErrorState of Vernacstate.Parser.state option * Exninfo.iexn
+ | ErrorState of Vernacstate.Parser.t option * Exninfo.iexn
type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info
type backup = { mine : branch; others : branch list }
@@ -334,7 +329,7 @@ module VCS : sig
type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t
- val init : stm_doc_type -> id -> Vernacstate.Parser.state -> doc
+ val init : stm_doc_type -> id -> Vernacstate.Parser.t -> doc
(* val get_type : unit -> stm_doc_type *)
val set_ldir : Names.DirPath.t -> unit
val get_ldir : unit -> Names.DirPath.t
@@ -364,8 +359,8 @@ 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 set_parsing_state : id -> Vernacstate.Parser.t -> unit
+ val get_parsing_state : id -> Vernacstate.Parser.t option
val get_proof_mode : id -> Pvernac.proof_mode option
(* cuts from start -> stop, raising Expired if some nodes are not there *)
@@ -678,7 +673,7 @@ end = struct (* {{{ *)
{ info with state = EmptyState;
vcs_backup = None,None } in
let make_shallow = function
- | FullState st -> FullState (Vernacstate.make_shallow st)
+ | FullState st -> FullState (Vernacstate.Stm.make_shallow st)
| x -> x
in
let copy_info_w_state v id =
@@ -870,22 +865,13 @@ end = struct (* {{{ *)
let invalidate_cur_state () = cur_id := Stateid.dummy
- type proof_part =
- Vernacstate.LemmaStack.t option *
- int * (* Evarutil.meta_counter_summary_tag *)
- int * (* Evd.evar_counter_summary_tag *)
- Declare.Obls.State.t
+ type proof_part = Vernacstate.Stm.pstate
type partial_state =
[ `Full of Vernacstate.t
| `ProofOnly of Stateid.t * proof_part ]
- let proof_part_of_frozen { Vernacstate.lemmas; system } =
- let st = States.summary_of_state system in
- lemmas,
- Summary.project_from_summary st Util.(pi1 summary_pstate),
- Summary.project_from_summary st Util.(pi2 summary_pstate),
- Summary.project_from_summary st Util.(pi3 summary_pstate)
+ let proof_part_of_frozen st = Vernacstate.Stm.pstate st
let cache_state ~marshallable id =
VCS.set_state id (FullState (Vernacstate.freeze_interp_state ~marshallable))
@@ -952,21 +938,10 @@ end = struct (* {{{ *)
else s
with VCS.Expired -> s in
VCS.set_state id (FullState s)
- | `ProofOnly(ontop,(pstate,c1,c2,c3)) ->
+ | `ProofOnly(ontop,pstate) ->
if is_cached_and_valid ontop then
let s = get_cached ontop in
- let s = { s with lemmas =
- PG_compat.copy_terminators ~src:s.lemmas ~tgt:pstate } in
- let s = { s with system =
- States.replace_summary s.system
- begin
- let st = States.summary_of_state s.system in
- let st = Summary.modify_summary st Util.(pi1 summary_pstate) c1 in
- let st = Summary.modify_summary st Util.(pi2 summary_pstate) c2 in
- let st = Summary.modify_summary st Util.(pi3 summary_pstate) c3 in
- st
- end
- } in
+ let s = Vernacstate.Stm.set_pstate s pstate in
VCS.set_state id (FullState s)
with VCS.Expired -> ()
@@ -978,12 +953,7 @@ end = struct (* {{{ *)
execution_error ?loc id (iprint (e, info));
(e, Stateid.add info ~valid id)
- let same_env { Vernacstate.system = s1 } { Vernacstate.system = s2 } =
- let s1 = States.summary_of_state s1 in
- let e1 = Summary.project_from_summary s1 Global.global_env_summary_tag in
- let s2 = States.summary_of_state s2 in
- let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in
- e1 == e2
+ let same_env = Vernacstate.Stm.same_env
(* [define] puts the system in state [id] calling [f ()] *)
(* [safe_id] is the last known valid state before execution *)
@@ -1047,9 +1017,9 @@ end = struct (* {{{ *)
end (* }}} *)
(* Wrapper for the proof-closing special path for Qed *)
-let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc ~control pending : Vernacstate.t =
+let stm_qed_delay_proof ?route ~proof ~pinfo ~id ~st ~loc ~control pending : Vernacstate.t =
set_id_for_feedback ?route dummy_doc id;
- Vernacinterp.interp_qed_delayed_proof ~proof ~info ~st ~control (CAst.make ?loc pending)
+ Vernacinterp.interp_qed_delayed_proof ~proof ~pinfo ~st ~control (CAst.make ?loc pending)
(* Wrapper for Vernacentries.interp to set the feedback id *)
(* It is currently called 19 times, this number should be certainly
@@ -1157,7 +1127,8 @@ end = struct (* {{{ *)
let get_proof ~doc id =
match state_of_id ~doc id with
- | `Valid (Some vstate) -> Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:Declare.Proof.get_proof) vstate.Vernacstate.lemmas
+ | `Valid (Some vstate) ->
+ Option.map (Vernacstate.LemmaStack.with_top ~f:Declare.Proof.get) vstate.Vernacstate.lemmas
| _ -> None
let undo_vernac_classifier v ~doc =
@@ -1351,7 +1322,7 @@ module rec ProofTask : sig
t_stop : Stateid.t;
t_drop : bool;
t_states : competence;
- t_assign : Declare.closed_proof_output Future.assignment -> unit;
+ t_assign : Declare.Proof.closed_proof_output Future.assignment -> unit;
t_loc : Loc.t option;
t_uuid : Future.UUID.t;
t_name : string }
@@ -1374,7 +1345,7 @@ module rec ProofTask : sig
?loc:Loc.t ->
drop_pt:bool ->
Stateid.t * Stateid.t -> Stateid.t ->
- Declare.closed_proof_output Future.computation
+ Declare.Proof.closed_proof_output Future.computation
(* If set, only tasks overlapping with this list are processed *)
val set_perspective : Stateid.t list -> unit
@@ -1390,7 +1361,7 @@ end = struct (* {{{ *)
t_stop : Stateid.t;
t_drop : bool;
t_states : competence;
- t_assign : Declare.closed_proof_output Future.assignment -> unit;
+ t_assign : Declare.Proof.closed_proof_output Future.assignment -> unit;
t_loc : Loc.t option;
t_uuid : Future.UUID.t;
t_name : string }
@@ -1412,7 +1383,7 @@ end = struct (* {{{ *)
e_safe_states : Stateid.t list }
type response =
- | RespBuiltProof of Declare.closed_proof_output * float
+ | RespBuiltProof of Declare.Proof.closed_proof_output * float
| RespError of error
| RespStates of (Stateid.t * State.partial_state) list
@@ -1522,11 +1493,12 @@ end = struct (* {{{ *)
PG_compat.close_future_proof ~feedback_id:stop (Future.from_val proof) in
let st = Vernacstate.freeze_interp_state ~marshallable:false in
- let opaque = Declare.Opaque in
+ let opaque = Opaque in
try
let _pstate =
+ let pinfo = Declare.Proof.Proof_info.default () in
stm_qed_delay_proof ~st ~id:stop
- ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None)) in
+ ~proof:pobject ~pinfo ~loc ~control:[] (Proved (opaque,None)) in
()
with exn ->
(* If [stm_qed_delay_proof] fails above we need to use the
@@ -1666,13 +1638,13 @@ end = struct (* {{{ *)
let _proof = PG_compat.return_partial_proof () in
`OK_ADMITTED
else begin
- let opaque = Declare.Opaque in
+ let opaque = Opaque in
(* The original terminator, a hook, has not been saved in the .vio*)
let proof, _info =
PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true in
- let info = Lemmas.Info.make () in
+ let pinfo = Declare.Proof.Proof_info.default () in
(* We jump at the beginning since the kernel handles side effects by also
* looking at the ones that happen to be present in the current env *)
@@ -1685,9 +1657,9 @@ end = struct (* {{{ *)
*)
(* STATE We use the state resulting from reaching start. *)
let st = Vernacstate.freeze_interp_state ~marshallable:false in
- ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc ~control:[] (Proved (opaque,None)));
+ ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~pinfo ~loc ~control:[] (Proved (opaque,None)));
(* Is this name the same than the one in scope? *)
- let name = Declare.get_po_name proof in
+ let name = Declare.Proof.get_po_name proof in
`OK name
end
with e ->
@@ -1932,8 +1904,7 @@ end = struct (* {{{ *)
List.for_all (Context.Named.Declaration.for_all is_ground)
Evd.(evar_context g))
then
- CErrors.user_err ~hdr:"STM" Pp.(strbrk("the par: goal selector supports ground "^
- "goals only"))
+ CErrors.user_err ~hdr:"STM" Pp.(strbrk("The par: goal selector does not support goals with existential variables"))
else begin
let (i, ast) = r_ast in
PG_compat.map_proof (fun p -> Proof.focus focus_cond () i p);
@@ -1950,10 +1921,15 @@ end = struct (* {{{ *)
| Evd.Evar_empty -> RespNoProgress
| Evd.Evar_defined t ->
let t = Evarutil.nf_evar sigma t in
- if Evarutil.is_ground_term sigma t then
+ let evars = Evarutil.undefined_evars_of_term sigma t in
+ if Evar.Set.is_empty evars then
let t = EConstr.Unsafe.to_constr t in
RespBuiltSubProof (t, Evd.evar_universe_context sigma)
- else CErrors.user_err ~hdr:"STM" Pp.(str"The solution is not ground")
+ else
+ CErrors.user_err ~hdr:"STM"
+ Pp.(str"The par: selector requires a tactic that makes no progress or fully" ++
+ str" solves the goal and leaves no unresolved existential variables. The following" ++
+ str" existentials remain unsolved: " ++ prlist (Termops.pr_existential_key sigma) (Evar.Set.elements evars))
end) ()
with e when CErrors.noncritical e -> RespError (CErrors.print e)
@@ -2157,7 +2133,7 @@ let collect_proof keep cur hd brkind id =
| id :: _ -> Names.Id.to_string id in
let loc = (snd cur).expr.CAst.loc in
let is_defined_expr = function
- | VernacEndProof (Proved (Declare.Transparent,_)) -> true
+ | VernacEndProof (Proved (Transparent,_)) -> true
| _ -> false in
let is_defined = function
| _, { expr = e } -> is_defined_expr e.CAst.v.expr
@@ -2367,21 +2343,16 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
(* ugly functions to process nested lemmas, i.e. hard to reproduce
* side effects *)
- let cherry_pick_non_pstate () =
- let st = Summary.freeze_summaries ~marshallable:false in
- let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in
- let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in
- let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in
- st, Lib.freeze () in
-
let inject_non_pstate (s,l) =
Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env ()
in
+
let rec pure_cherry_pick_non_pstate safe_id id =
State.purify (fun id ->
stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
reach ~safe_id id;
- cherry_pick_non_pstate ())
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ Vernacstate.Stm.non_pstate st)
id
(* traverses the dag backward from nodes being already calculated *)
@@ -2492,13 +2463,13 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
| VtKeepDefined ->
CErrors.anomaly (Pp.str "Cannot delegate transparent proofs, this is a bug in the STM.")
in
- let proof, info =
+ let proof, pinfo =
PG_compat.close_future_proof ~feedback_id:id fp in
if not delegate then ignore(Future.compute fp);
reach view.next;
let st = Vernacstate.freeze_interp_state ~marshallable:false in
let control, pe = extract_pe x in
- ignore(stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe);
+ ignore(stm_qed_delay_proof ~id ~st ~proof ~pinfo ~loc ~control pe);
feedback ~id:id Incomplete
| { VCS.kind = `Master }, _ -> assert false
end;
@@ -2522,7 +2493,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
| VtKeep VtKeepAxiom ->
qed.fproof <- Some (None, ref false); None
| VtKeep opaque ->
- let opaque = let open Declare in match opaque with
+ let opaque = match opaque with
| VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent
| VtKeepAxiom -> assert false
in
@@ -2537,9 +2508,9 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
let st = Vernacstate.freeze_interp_state ~marshallable:false in
let _st = match proof with
| None -> stm_vernac_interp id st x
- | Some (proof, info) ->
+ | Some (proof, pinfo) ->
let control, pe = extract_pe x in
- stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe
+ stm_qed_delay_proof ~id ~st ~proof ~pinfo ~loc ~control pe
in
let wall_clock3 = Unix.gettimeofday () in
Aux_file.record_in_aux_at ?loc:x.expr.CAst.loc "proof_check_time"
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index cf127648b4..a957f7354f 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -37,7 +37,7 @@ let string_of_vernac_classification = function
| VtMeta -> "Meta "
| VtProofMode _ -> "Proof Mode"
-let vtkeep_of_opaque = let open Declare in function
+let vtkeep_of_opaque = function
| Opaque -> VtKeepOpaque
| Transparent -> VtKeepDefined
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 21:43:04 +0000