aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_global.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof_global.ml')
-rw-r--r--proofs/proof_global.ml257
1 files changed, 120 insertions, 137 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index ed985f292..0c0aac715 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -17,6 +17,7 @@
open Util
open Pp
open Names
+open Util
(*** Proof Modes ***)
@@ -59,32 +60,31 @@ let _ =
(*** Proof Global Environment ***)
-(* local shorthand *)
-type nproof = Id.t*Proof.proof
-
(* Extra info on proofs. *)
type lemma_possible_guards = int list list
-type proof_info = {
- strength : Decl_kinds.goal_kind ;
- compute_guard : lemma_possible_guards;
- hook : unit Tacexpr.declaration_hook ;
- mode : proof_mode
+
+type pstate = {
+ pid : Id.t;
+ endline_tactic : unit Proofview.tactic;
+ section_vars : Context.section_context option;
+ proof : Proof.proof;
+ strength : Decl_kinds.goal_kind;
+ compute_guard : lemma_possible_guards;
+ hook : unit Tacexpr.declaration_hook;
+ mode : proof_mode;
}
-(* Invariant: the domain of proof_info is current_proof.*)
-(* The head of [!current_proof] is the actual current proof, the other ones are
+(* The head of [!pstates] is the actual current proof, the other ones are
to be resumed when the current proof is closed or aborted. *)
-let current_proof = ref ([]:nproof list)
-let proof_info = ref (Id.Map.empty : proof_info Id.Map.t)
+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 !current_proof with
- | (id,_)::_ ->
- let { mode = m } = Id.Map.find id !proof_info in
+ match !pstates with
+ | { mode = m } :: _ ->
!current_proof_mode.reset ();
current_proof_mode := m;
!current_proof_mode.set ()
@@ -103,7 +103,7 @@ let _ = Errors.register_handler begin function
end
let extract id l =
let rec aux = function
- | ((id',_) as np)::l when Id.equal id id' -> (np,l)
+ | ({pid = id' } as np)::l when Id.equal id id' -> (np,l)
| np::l -> let (np', l) = aux l in (np' , np::l)
| [] -> raise NoSuchProof
in
@@ -121,10 +121,6 @@ let extract_top l =
match !l with
| np::l' -> l := l' ; update_proof_mode (); np
| [] -> raise NoCurrentProof
-let find_top l =
- match !l with
- | np::_ -> np
- | [] -> raise NoCurrentProof
(* combinators for the proof_info map *)
let add id info m =
@@ -135,13 +131,28 @@ let remove id m =
(*** Proof Global manipulation ***)
let get_all_proof_names () =
- List.map fst !current_proof
+ List.map (function { pid = id } -> id) !pstates
-let give_me_the_proof () =
- snd (find_top current_proof)
+let cur_pstate () =
+ match !pstates with
+ | np::_ -> np
+ | [] -> raise NoCurrentProof
-let get_current_proof_name () =
- fst (find_top current_proof)
+let give_me_the_proof () = (cur_pstate ()).proof
+let get_current_proof_name () = (cur_pstate ()).pid
+
+let with_current_proof f =
+ match !pstates with
+ | [] -> raise NoCurrentProof
+ | p :: rest ->
+ let p = { p with proof = f p.endline_tactic p.proof } in
+ pstates := p :: rest
+
+(* Sets the tactic to be used when a tactic line is closed with [...] *)
+let set_endline_tactic tac =
+ match !pstates with
+ | [] -> raise NoCurrentProof
+ | p :: rest -> pstates := { p with endline_tactic = tac } :: rest
(* spiwack: it might be considered to move error messages away.
Or else to remove special exceptions from Proof_global.
@@ -155,7 +166,7 @@ let msg_proofs () =
| l -> (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
(pr_sequence Nameops.pr_id l) ++ str".")
-let there_is_a_proof () = not (List.is_empty !current_proof)
+let there_is_a_proof () = not (List.is_empty !pstates)
let there_are_pending_proofs () = there_is_a_proof ()
let check_no_pending_proof () =
if not (there_are_pending_proofs ()) then
@@ -167,51 +178,40 @@ let check_no_pending_proof () =
end
let discard_gen id =
- ignore (extract id current_proof);
- remove id proof_info
+ pstates := List.filter (fun { pid = id' } -> id <> id') !pstates
let discard (loc,id) =
- try
- discard_gen id
- with NoSuchProof ->
+ let n = List.length !pstates in
+ discard_gen id;
+ if List.length !pstates = n then
Errors.user_err_loc
(loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ())
let discard_current () =
- let (id,_) = extract_top current_proof in
- remove id proof_info
+ if !pstates = [] then raise NoCurrentProof else pstates := List.tl !pstates
-let discard_all () =
- current_proof := [];
- proof_info := Id.Map.empty
+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. *)
-(* Core component.
- No undo handling.
- Applies to proof [id], and proof mode [m]. *)
let set_proof_mode m id =
- let info = Id.Map.find id !proof_info in
- let info = { info with mode = m } in
- proof_info := Id.Map.add id info !proof_info;
+ pstates :=
+ List.map (function { pid = id' } as p ->
+ if Id.equal id' id then { p with mode = m } else p) !pstates;
update_proof_mode ()
-(* Complete function.
- Handles undo.
- Applies to current proof, and proof mode name [mn]. *)
+
let set_proof_mode mn =
- let m = find_proof_mode mn in
- let id = get_current_proof_name () in
- let pr = give_me_the_proof () in
- Proof.add_undo begin let curr = !current_proof_mode in fun () ->
- set_proof_mode curr id ; update_proof_mode ()
- end pr ;
- set_proof_mode m id
+ set_proof_mode (find_proof_mode mn) (get_current_proof_name ())
+
+let activate_proof_mode mode = (find_proof_mode mode).set ()
+let disactivate_proof_mode mode = (find_proof_mode mode).reset ()
exception AlreadyExists
let _ = Errors.register_handler begin function
| AlreadyExists -> Errors.error "Already editing something of that name."
| _ -> raise Errors.Unhandled
end
+
(* [start_proof s str env t hook tac] starts a proof of name [s] and
conclusion [t]; [hook] is optionally a function to be applied at
proof end (e.g. to declare the built constructions as a coercion
@@ -220,84 +220,67 @@ end
proof of mutually dependent theorems).
It raises exception [ProofInProgress] if there is a proof being
currently edited. *)
-let start_proof id str goals ?(compute_guard=[]) hook =
- begin
- List.iter begin fun (id_ex,_) ->
- if Names.Id.equal id id_ex then raise AlreadyExists
- end !current_proof
- end;
- let p = Proof.start goals in
- add id { strength=str ;
- compute_guard=compute_guard ;
- hook=hook ;
- mode = ! default_proof_mode } proof_info ;
- push (id,p) current_proof
-
-(* arnaud: à enlever *)
-let run_tactic tac =
- let p = give_me_the_proof () in
- let env = Global.env () in
- Proof.run_tactic env tac p
-(* Sets the tactic to be used when a tactic line is closed with [...] *)
-let set_endline_tactic tac =
- let p = give_me_the_proof () in
- Proof.set_endline_tactic tac p
+let start_proof id str goals ?(compute_guard=[]) hook =
+ let initial_state = {
+ pid = id;
+ proof = Proof.start goals;
+ endline_tactic = Proofview.tclUNIT ();
+ section_vars = None;
+ strength = str;
+ compute_guard = compute_guard;
+ hook = hook;
+ mode = ! default_proof_mode } in
+ push initial_state pstates
+
+let get_used_variables () = (cur_pstate ()).section_vars
let set_used_variables l =
- let p = give_me_the_proof () in
let env = Global.env () in
let ids = List.fold_right Id.Set.add l Id.Set.empty in
let ctx = Environ.keep_hyps env ids in
- Proof.set_used_variables ctx p
-
-let get_used_variables () =
- Proof.get_used_variables (give_me_the_proof ())
-
-let with_end_tac tac =
- let p = give_me_the_proof () in
- Proof.with_end_tac p tac
-
+ match !pstates with
+ | [] -> raise NoCurrentProof
+ | p :: rest ->
+ if p.section_vars <> None then
+ Errors.error "Used section variables can be declared only once";
+ pstates := { p with section_vars = Some ctx} :: rest
+
+let get_open_goals () =
+ let gl, gll, _ = Proof.proof (cur_pstate ()).proof in
+ List.length gl +
+ List.fold_left (+) 0
+ (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll)
+
+type closed_proof =
+ Names.Id.t *
+ (Entries.definition_entry list * lemma_possible_guards *
+ Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
+
+let close_proof ~now ?(fix_exn = fun x -> x) ps side_eff =
+ let { pid; section_vars; compute_guard; strength; hook; proof } = ps in
+ let entries = List.map (fun (c, t) -> { Entries.
+ const_entry_body = Future.chain side_eff (fun () ->
+ try Proof.return (cur_pstate ()).proof c with
+ | Proof.UnfinishedProof ->
+ raise (fix_exn(Errors.UserError("last tactic before Qed",
+ str"Attempt to save an incomplete proof")))
+ | Proof.HasUnresolvedEvar ->
+ raise (fix_exn(Errors.UserError("last tactic before Qed",
+ str"Attempt to save a proof with existential " ++
+ str"variables still non-instantiated"))));
+ const_entry_secctx = section_vars;
+ const_entry_type = Some t;
+ const_entry_inline_code = false;
+ const_entry_opaque = true }) (Proof.initial_goals proof) in
+ if now then
+ List.iter (fun x -> ignore(Future.join x.Entries.const_entry_body)) entries;
+ (pid, (entries, compute_guard, strength, hook))
+
+let close_future_proof ~fix_exn proof =
+ close_proof ~now:false ~fix_exn (cur_pstate ()) proof
let close_proof () =
- (* spiwack: for now close_proof doesn't actually discard the proof, it is done
- by [Command.save]. *)
- try
- let id = get_current_proof_name () in
- let p = give_me_the_proof () in
- let proofs_and_types = Proof.return p in
- let section_vars = Proof.get_used_variables p in
- let entries = List.map
- (fun (c,t) -> { Entries.const_entry_body = c;
- const_entry_secctx = section_vars;
- const_entry_type = Some t;
- const_entry_opaque = true;
- const_entry_inline_code = false })
- proofs_and_types
- in
- let { compute_guard=cg ; strength=str ; hook=hook } =
- Id.Map.find id !proof_info
- in
- (id, (entries,cg,str,hook))
- with
- | Proof.UnfinishedProof ->
- Errors.error "Attempt to save an incomplete proof"
- | Proof.HasUnresolvedEvar ->
- Errors.error "Attempt to save a proof with existential variables still non-instantiated"
-
-
-(**********************************************************)
-(* *)
-(* Utility functions *)
-(* *)
-(**********************************************************)
-
-let maximal_unfocus k p =
- begin try while Proof.no_focused_goal p do
- Proof.unfocus k p
- done
- with Proof.FullyUnfocused | Proof.CannotUnfocusThisWay -> ()
- end
-
+ close_proof ~now:true (cur_pstate ()) (Future.from_val())
(**********************************************************)
(* *)
@@ -317,7 +300,7 @@ module Bullet = struct
type behavior = {
name : string;
- put : Proof.proof -> t -> unit
+ put : Proof.proof -> t -> Proof.proof
}
let behaviors = Hashtbl.create 4
@@ -326,7 +309,7 @@ module Bullet = struct
(*** initial modes ***)
let none = {
name = "None";
- put = fun _ _ -> ()
+ put = fun x _ -> x
}
let _ = register_behavior none
@@ -356,8 +339,8 @@ module Bullet = struct
let pop pr =
match get_bullets pr with
| b::_ ->
- Proof.unfocus bullet_kind pr;
- (*returns*) b
+ let pr = Proof.unfocus bullet_kind pr () in
+ pr, b
| _ -> assert false
let push b pr =
@@ -365,10 +348,10 @@ module Bullet = struct
let put p bul =
if has_bullet bul p then
- Proof.transaction p begin fun () ->
- while not (bullet_eq bul (pop p)) do () done;
- push bul p
- end
+ let rec aux p =
+ let p, b = pop p in
+ if not (bullet_eq bul b) then aux p else p in
+ push bul (aux p)
else
push bul p
@@ -403,11 +386,11 @@ end
module V82 = struct
let get_current_initial_conclusions () =
- let p = give_me_the_proof () in
- let id = get_current_proof_name () in
- let { strength=str ; hook=hook } =
- Id.Map.find id !proof_info
- in
- (id,(Proof.V82.get_initial_conclusions p, str, hook))
+ let { pid; strength; hook; proof } = cur_pstate () in
+ pid, (List.map snd (Proof.initial_goals proof), strength, hook)
end
+type state = pstate list
+let freeze () = !pstates
+let unfreeze s = pstates := s; update_proof_mode ()
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 16:33:36 +0000