blob: 4980333b5d4025116a6a5589246b79173120974f (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
type t = {
system : States.state; (* summary + libstack *)
proof : Proof_global.t; (* proof state *)
shallow : bool (* is the state trimmed down (libstack) *)
}
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 = update_cache s_proof (Proof_global.freeze ~marshallable);
shallow = marshallable = `Shallow }
let unfreeze_interp_state { system; proof } =
do_if_not_cached s_cache States.unfreeze system;
do_if_not_cached s_proof Proof_global.unfreeze proof
|
