blob: 6eb618ad0aa31feb65a65c1cf374851eeee91788 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (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 = {
parsing : Parser.state;
system : States.state; (* summary + libstack *)
proof : Proof_global.t option; (* proof state *)
shallow : bool (* is the state trimmed down (libstack) *)
}
let pstate st = Option.map Proof_global.get_current_pstate st.proof
let s_cache = ref None
let s_proof = ref None
let invalidate_cache () =
s_cache := None;
s_proof := None
let update_cache rf v =
rf := Some v; v
let do_if_not_cached rf f v =
match !rf with
| None ->
rf := Some v; f v
| Some vc when vc != v ->
rf := Some v; f v
| Some _ ->
()
let freeze_interp_state ~marshallable =
{ system = update_cache s_cache (States.freeze ~marshallable);
proof = !s_proof;
shallow = false;
parsing = Parser.cur_state ();
}
let unfreeze_interp_state { system; proof; parsing } =
do_if_not_cached s_cache States.unfreeze system;
s_proof := proof;
Pcoq.unfreeze parsing
let make_shallow st =
let lib = States.lib_of_state st.system in
{ st with
system = States.replace_lib st.system @@ Lib.drop_objects lib;
shallow = true;
}
(* Compatibility module *)
module Proof_global = struct
let get () = !s_proof
let set x = s_proof := x
let freeze ~marshallable:_ = get ()
let unfreeze x = s_proof := Some x
exception NoCurrentProof
let () =
CErrors.register_handler begin function
| NoCurrentProof ->
CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).")
| _ -> raise CErrors.Unhandled
end
open Proof_global
let cc f = match !s_proof with
| None -> raise NoCurrentProof
| Some x -> f x
let cc1 f = cc (fun p -> f (Proof_global.get_current_pstate p))
let dd f = match !s_proof with
| None -> raise NoCurrentProof
| Some x -> s_proof := Some (f x)
let dd1 f = dd (fun p -> Proof_global.modify_current_pstate f p)
let there_are_pending_proofs () = !s_proof <> None
let get_open_goals () = cc1 get_open_goals
let set_terminator x = dd1 (set_terminator x)
let give_me_the_proof_opt () = Option.map (fun p -> give_me_the_proof (Proof_global.get_current_pstate p)) !s_proof
let give_me_the_proof () = cc1 give_me_the_proof
let get_current_proof_name () = cc1 get_current_proof_name
let simple_with_current_proof f =
dd (simple_with_current_proof f)
let with_current_proof f =
let pf, res = cc (with_current_proof f) in
s_proof := Some pf; res
let install_state s = s_proof := Some s
let return_proof ?allow_partial () =
cc1 (return_proof ?allow_partial)
let close_future_proof ~opaque ~feedback_id pf =
cc1 (fun st -> close_future_proof ~opaque ~feedback_id st pf)
let close_proof ~opaque ~keep_body_ucst_separate f =
cc1 (close_proof ~opaque ~keep_body_ucst_separate f)
let discard_all () = s_proof := None
let update_global_env () = dd1 update_global_env
let get_current_context () = cc1 Pfedit.get_current_context
let get_all_proof_names () =
try cc get_all_proof_names
with NoCurrentProof -> []
let copy_terminators ~src ~tgt =
match src, tgt with
| None, None -> None
| Some _ , None -> None
| None, Some x -> Some x
| Some src, Some tgt -> Some (copy_terminators ~src ~tgt)
end
|
