https://github.com/EasyCrypt/easycrypt
Tip revision: d5830863b50a5b59e77c7b3b888a1d3de33875d5 authored by Antoine Séré on 01 March 2021, 09:56:16 UTC
CRT prooved modulo some easy admits
CRT prooved modulo some easy admits
Tip revision: d583086
ecGState.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
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 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