From 43d381ab20035f64ce2edea8639fcd9e1d0453bc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 25 May 2020 14:09:30 +0200 Subject: [declare] Move proof information to declare. At this point the record in lemmas was just a stub; next commit will stop exposing the internals of mutual information, and pave the way for the refactoring of `Info.t` handling in the Declare interface. --- stm/proofBlockDelimiter.ml | 4 ++-- stm/stm.ml | 7 ++++--- 2 files changed, 6 insertions(+), 5 deletions(-) (limited to 'stm') 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 943c83ecd3..7aaa359149 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1157,7 +1157,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 = @@ -1526,7 +1527,7 @@ end = struct (* {{{ *) try let _pstate = stm_qed_delay_proof ~st ~id:stop - ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None)) in + ~proof:pobject ~info:(Declare.Info.make ()) ~loc ~control:[] (Proved (opaque,None)) in () with exn -> (* If [stm_qed_delay_proof] fails above we need to use the @@ -1672,7 +1673,7 @@ end = struct (* {{{ *) let proof, _info = PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true in - let info = Lemmas.Info.make () in + let info = Declare.Info.make () 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 *) -- cgit v1.2.3 From a6d663c85d71b3cce007af23419e8030b8c5ac88 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 25 May 2020 14:57:44 +0200 Subject: [declare] [api] Removal of duplicated type aliases. --- stm/stm.ml | 8 ++++---- stm/vernac_classifier.ml | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 7aaa359149..800115ce42 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1523,7 +1523,7 @@ 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 = stm_qed_delay_proof ~st ~id:stop @@ -1667,7 +1667,7 @@ 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 = @@ -2162,7 +2162,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 @@ -2527,7 +2527,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 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 -- cgit v1.2.3 From ea8b9e060dfba9cc8706677e29c26dabaaa87551 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 22 Jun 2020 20:42:39 +0200 Subject: [declare] Improve organization of proof/constant information. We unify information about constants so it is shared among all the paths [interactive, NI, obligations]. IMHO the current setup looks pretty good, with information split into a per-constant record `CInfo.t` and variables affecting mutual definitions at once, which live in `Info.t`. Main information outside our `Info` record is `opaque`, which is provided at different moments in several cases. There are a few nits regarding interactive proofs, which will go away in the next commits. --- stm/stm.ml | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 800115ce42..7af0ace215 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1047,9 +1047,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 @@ -1526,8 +1526,9 @@ end = struct (* {{{ *) 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:(Declare.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 @@ -1673,7 +1674,7 @@ end = struct (* {{{ *) let proof, _info = PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true in - let info = Declare.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 *) @@ -1686,7 +1687,7 @@ 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 `OK name @@ -2497,13 +2498,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; @@ -2542,9 +2543,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" -- cgit v1.2.3 From bf31fad28992a67b66d859655f030e619b69705e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 23 Jun 2020 21:48:23 +0200 Subject: [declare] Improve logical code order Now that the interface has mostly stabilized, we move code around to respect internal dependency order. This will allow us to start sharing more code in the 4 principal cases, and also paves the way for the full merging of obligations and the removal of the Proof_ending type in favor of stronger type abstraction. --- stm/stm.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 7af0ace215..652d064b83 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 = @@ -1352,7 +1352,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 } @@ -1375,7 +1375,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 @@ -1391,7 +1391,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 } @@ -1413,7 +1413,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 @@ -1689,7 +1689,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state ~marshallable:false in 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 -> -- cgit v1.2.3