https://github.com/EasyCrypt/easycrypt
Tip revision: 846710a2a656834065e745d19416ebdc83158f55 authored by Benjamin Gregoire on 14 July 2019, 06:50:07 UTC
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Tip revision: 846710a
ecMaps.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 EcUtils
(* -------------------------------------------------------------------- *)
module Map = struct
module type OrderedType = Why3.Extmap.OrderedType
module type S = sig
include Why3.Extmap.S
val odup : ('a -> key) -> 'a list -> ('a * 'a) option
val to_stream : 'a t -> (key * 'a) Stream.t
end
module Make(O : OrderedType) : S with type key = O.t = struct
include Why3.Extmap.Make(O)
let odup (type a) (f : a -> key) (xs : a list) =
let module E = struct exception Found of a * a end in
try
List.fold_left
(fun sm x ->
let key = f x in
match find_opt key sm with
| Some y -> raise (E.Found (y, x))
| None -> add (f x) x sm)
empty xs
|> ignore; None
with E.Found (x, y) -> Some (x, y)
let to_stream (m : 'a t) =
let next =
let enum = ref (start_enum m) in
fun (_ : int) ->
let aout = val_enum !enum in
enum := next_enum !enum;
aout
in
Stream.from next
end
module MakeBase(M : S) : Why3.Extmap.S
with type key = M.key
and type 'a t = 'a M.t
and type 'a enumeration = 'a M.enumeration
=
struct include M end
end
module Set = struct
module type OrderedType = Why3.Extset.OrderedType
module type S = sig
include Why3.Extset.S
val big_union : t list -> t
val map : (elt -> elt) -> t -> t
val undup : elt list -> elt list
end
module MakeOfMap(M : Why3.Extmap.S) : S with module M = M = struct
include Why3.Extset.MakeOfMap(M)
let big_union (xs : t list) : t =
List.fold_left union empty xs
let map f s =
fold (fun k s -> add (f k) s) s empty
let undup =
let rec doit seen acc s =
match s with
| [] -> List.rev acc
| x :: s ->
if mem x seen then
doit seen acc s
else
doit (add x seen) (x :: acc) s
in fun (s : elt list) -> doit empty [] s
end
module Make(Ord : OrderedType) = MakeOfMap(Map.Make(Ord))
end
module EHashtbl = struct
module type S = sig
include Why3.Exthtbl.S
val memo_rec : int -> ((key -> 'a) -> key -> 'a) -> key -> 'a
end
module Make(T : Why3.Wstdlib.OrderedHashedType) = struct
include Why3.Exthtbl.Make(T)
let memo_rec size f =
let h = create size in
let rec aux x =
try find h x with Not_found -> let r = f aux x in add h x r; r in
aux
end
end
(* -------------------------------------------------------------------- *)
module MakeMSH (X : Why3.Wstdlib.TaggedType) : sig
module M : Map.S with type key = X.t
module S : Set.S with module M = Map.MakeBase(M)
module H : EHashtbl.S with type key = X.t
end = struct
module T = Why3.Wstdlib.OrderedHashed(X)
module M = Map.Make(T)
module S = Set.MakeOfMap(M)
module H = EHashtbl.Make(T)
end
(* --------------------------------------------------------------------*)
module Int = struct
type t = int
let compare = (Pervasives.compare : t -> t -> int)
let equal = ((=) : t -> t -> bool)
let hash = (fun (x : t) -> x)
end
module Mint = Map.Make(Int)
module Sint = Set.MakeOfMap(Mint)
module Hint = EHashtbl.Make(Int)
(* --------------------------------------------------------------------*)
module DInt = struct
type t = int * int
let compare = (Pervasives.compare : t -> t -> int)
let equal = ((=) : t -> t -> bool)
let hash = (fun (x : t) -> Hashtbl.hash x)
end
module Mdint = Map.Make(DInt)
module Sdint = Set.MakeOfMap(Mdint)
module Hdint = EHashtbl.Make(DInt)
(* --------------------------------------------------------------------*)
module Mstr = Map.Make(String)
module Sstr = Set.MakeOfMap(Mstr)