easycrypt/src/ecGState.ml at b9887bba357960c4d1ea36877e9ef07404b915fc · EasyCrypt/easycrypt · GitHub

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
(* -------------------------------------------------------------------- *)
open EcMaps

(* -------------------------------------------------------------------- *)
type nid_t    = EcUid.uid
type loglevel = [`Debug | `Info | `Warning | `Critical]

type notifier = {
  nt_id : nid_t;
  nt_cb : loglevel -> string Lazy.t -> unit;
}

type value = [ `Int of int ]

type gstate = {
  mutable gs_flags     : bool Mstr.t;
  mutable gs_values    : value Mstr.t;
  mutable gs_notifiers : notifier list;
  mutable gs_loglevel  : loglevel;
}

(* -------------------------------------------------------------------- *)
let asint ~(default : int) (value : value option) =
  match value with Some (`Int i) -> i | _ -> default

(* -------------------------------------------------------------------- *)
let create () : gstate =
  { gs_flags     = Mstr.empty;
    gs_values    = Mstr.empty;
    gs_notifiers = [];
    gs_loglevel  = `Info; }

(* -------------------------------------------------------------------- *)
let copy (gs : gstate) : gstate =
  { gs_flags     = gs.gs_flags    ;
    gs_values    = gs.gs_values   ;
    gs_notifiers = gs.gs_notifiers;
    gs_loglevel  = gs.gs_loglevel ; }

(* -------------------------------------------------------------------- *)
let from_flags (flags : (string * bool) list) : gstate =
  let gstate = create () in
  { gstate with gs_flags = Mstr.of_list flags; }

(* -------------------------------------------------------------------- *)
let getflag ?(default = false) (name : string) (g : gstate) =
  Mstr.find_def default name g.gs_flags

(* -------------------------------------------------------------------- *)
let setflag (name : string) (value : bool) (g : gstate) =
  g.gs_flags <- Mstr.add name value g.gs_flags

(* -------------------------------------------------------------------- *)
let getvalue (name : string) (g : gstate) =
  Mstr.find_opt name g.gs_values

(* -------------------------------------------------------------------- *)
let setvalue (name : string) (value : value) (g : gstate) =
  g.gs_values <- Mstr.add name value g.gs_values

(* -------------------------------------------------------------------- *)
let old_mem_restr = "old_mem_restr"

let get_old_mem_restr (g : gstate) : bool =
  getflag ~default:false old_mem_restr g

(* -------------------------------------------------------------------- *)
let pp_showtvi = "PP:showtvi"

let get_pp_showtvi (g : gstate) : bool =
  getflag ~default:false pp_showtvi g

(* -------------------------------------------------------------------- *)
let add_notifier (notifier : loglevel -> string Lazy.t -> unit) (gs : gstate) =
  let notifier = { nt_id = EcUid.unique (); nt_cb = notifier; } in
  gs.gs_notifiers <- notifier :: gs.gs_notifiers; notifier.nt_id

(* -------------------------------------------------------------------- *)
let rem_notifier (nid : nid_t) (gs : gstate) =
  gs.gs_notifiers <- List.filter (fun nt -> nt.nt_id = nid) gs.gs_notifiers

(* -------------------------------------------------------------------- *)
let loglevel (gs : gstate) =
  gs.gs_loglevel

(* -------------------------------------------------------------------- *)
let set_loglevel (lvl : loglevel) (gs : gstate) =
  gs.gs_loglevel <- lvl

(* -------------------------------------------------------------------- *)
let int_of_loglevel = function
  | `Debug    -> 0
  | `Info     -> 1
  | `Warning  -> 2
  | `Critical -> 3

let accept_log ~(level:loglevel) ~(wanted:loglevel) =
  int_of_loglevel level <= int_of_loglevel wanted

(* -------------------------------------------------------------------- *)
let string_of_loglevel = function
  | `Debug    -> "debug"
  | `Info     -> "info"
  | `Warning  -> "warning"
  | `Critical -> "critical"

(* -------------------------------------------------------------------- *)
let max_loglevel x1 x2 =
  let i1 = int_of_loglevel x1 in
  let i2 = int_of_loglevel x2 in
  if i1 < i2 then x2 else x1

(* -------------------------------------------------------------------- *)
let notify (lvl : loglevel) (msg : string Lazy.t) (gs : gstate) =
  let do1 (notifier : notifier) =
    try  notifier.nt_cb lvl msg
    with _ -> ()
  in

  if accept_log ~level:gs.gs_loglevel ~wanted:lvl then
    List.iter do1 gs.gs_notifiers