aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernacstate.ml
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