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
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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 () -> Pcoq.Entry.parse entry pa)
()
end
module LemmaStack = struct
type t = Lemmas.t * Lemmas.t list
let map f (pf, pfl) = (f pf, List.map f pfl)
let map_top_pstate ~f (pf, pfl) = (Lemmas.pf_map f pf, pfl)
let pop (ps, p) = match p with
| [] -> ps, None
| pp :: p -> ps, Some (pp, p)
let with_top (p, _) ~f = f p
let with_top_pstate (p, _) ~f = Lemmas.pf_fold f p
let push ontop a =
match ontop with
| None -> a , []
| Some (l,ls) -> a, (l :: ls)
let get_all_proof_names (pf : t) =
let prj x = Lemmas.pf_fold Declare.Proof.get_proof x in
let (pn, pns) = map Proof.(function pf -> (data (prj pf)).name) pf in
pn :: pns
let copy_info src tgt =
Lemmas.pf_map (fun _ -> Lemmas.pf_fold (fun x -> x) tgt) src
let copy_info ~src ~tgt =
let (ps, psl), (ts,tsl) = src, tgt in
copy_info ps ts,
List.map2 (fun op p -> copy_info op p) psl tsl
end
type t = {
parsing : Parser.state;
system : States.state; (* summary + libstack *)
lemmas : LemmaStack.t option; (* proofs of lemmas currently opened *)
shallow : bool (* is the state trimmed down (libstack) *)
}
let s_cache = ref None
let s_lemmas = ref None
let invalidate_cache () =
s_cache := None;
s_lemmas := 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);
lemmas = !s_lemmas;
shallow = false;
parsing = Parser.cur_state ();
}
let unfreeze_interp_state { system; lemmas; parsing } =
do_if_not_cached s_cache States.unfreeze system;
s_lemmas := lemmas;
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 Declare = struct
let get () = !s_lemmas
let set x = s_lemmas := x
let get_pstate () =
Option.map (LemmaStack.with_top ~f:(Lemmas.pf_fold (fun x -> x))) !s_lemmas
let freeze ~marshallable:_ = get ()
let unfreeze x = s_lemmas := Some x
exception NoCurrentProof
let () =
CErrors.register_handler begin function
| NoCurrentProof ->
Some (Pp.(str "No focused proof (No proof-editing in progress)."))
| _ -> None
end
open Lemmas
open Declare
let cc f = match !s_lemmas with
| None -> raise NoCurrentProof
| Some x -> LemmaStack.with_top_pstate ~f x
let cc_lemma f = match !s_lemmas with
| None -> raise NoCurrentProof
| Some x -> LemmaStack.with_top ~f x
let cc_stack f = match !s_lemmas with
| None -> raise NoCurrentProof
| Some x -> f x
let dd f = match !s_lemmas with
| None -> raise NoCurrentProof
| Some x -> s_lemmas := Some (LemmaStack.map_top_pstate ~f x)
let there_are_pending_proofs () = !s_lemmas <> None
let get_open_goals () = cc Proof.get_open_goals
let give_me_the_proof_opt () = Option.map (LemmaStack.with_top_pstate ~f:Proof.get_proof) !s_lemmas
let give_me_the_proof () = cc Proof.get_proof
let get_current_proof_name () = cc Proof.get_proof_name
let map_proof f = dd (Proof.map_proof f)
let with_current_proof f =
match !s_lemmas with
| None -> raise NoCurrentProof
| Some stack ->
let pf, res = LemmaStack.with_top_pstate stack ~f:(Proof.map_fold_proof_endline f) in
let stack = LemmaStack.map_top_pstate stack ~f:(fun _ -> pf) in
s_lemmas := Some stack;
res
type closed_proof = Declare.proof_object * Lemmas.Info.t
let return_proof () = cc return_proof
let return_partial_proof () = cc return_partial_proof
let close_future_proof ~feedback_id pf =
cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~feedback_id st pf) pt,
Lemmas.Internal.get_info pt)
let close_proof ~opaque ~keep_body_ucst_separate =
cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate)) pt,
Lemmas.Internal.get_info pt)
let discard_all () = s_lemmas := None
let update_global_env () = dd (Proof.update_global_env)
let get_current_context () = cc Declare.get_current_context
let get_all_proof_names () =
try cc_stack LemmaStack.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 (LemmaStack.copy_info ~src ~tgt)
end
|
