Module Imandra_surface.Check_cache

type cached_result =
| R_error of {
loc : Imandra_util.Iloc.t option;
kind : Imandra_util.Error.kind;
msg : string;
}
| R_verified_result of Event.cached_verify_result
| R_validate_fun_termination of {
is_rec : bool;
measured : string list;
}
| R_modular_decomp of Modular_decomposition.serialized
| R_custom of string
type id_with_ctx = {
id : Imandra_util.Chash.t;
theory : Imandra_util.Chash.t;
config : Imandra_util.Chash.t;
}
type key =
| K_nil
| K_verify of id_with_ctx
| K_validate of id_with_ctx
| K_custom of string
type entry = {
e_result : cached_result;
e_cap : Imandra_util.Console.Capture.t;
e_top_res : Top_result.t list;
}
type pair = key * entry
val ser_cached_result : cached_result Imandra_util.Serialize.t
type t
val make : get:(key -> entry option) -> set:(key -> entry -> bool) -> ?⁠mem:(key -> bool) -> clear:(unit -> unit) -> ?⁠sync:(unit -> unit) -> unit -> t
val dummy : t
val in_memory : ?⁠ttl:int -> ?⁠save_as:string -> ?⁠size:int -> unit -> t

Saves entries in memory.

parameter save_as

if set, init and save from the given file

parameter ttl

if set, entries not used in ttl seconds will be removed

module Key : sig ... end
module K_tbl : CCHashtbl.S with type K_tbl.key = key
module Entry : sig ... end
val cur_is_dummy : unit -> bool
val get : ?⁠c:t -> key -> entry option
val set : ?⁠c:t -> key -> entry -> unit
val mem : ?⁠c:t -> key -> bool
val set_ : ?⁠c:t -> key -> entry -> bool
val clear : ?⁠c:t -> unit -> unit
val sync : ?⁠c:t -> unit -> unit
val stack : t -> t -> t

stack c1 c2 produces a new cache that looks entries in c1 first, then in c2 if needed. New entries are stored in c1.

The expected usage is that c1 is a local cache, and c2 is a network cache

module State : sig ... end