Revision e12e2c2f2d80489ea5981a51f4362c947b05079d authored by Pierre-Yves Strub on 14 October 2019, 08:38:48 UTC, committed by Pierre-Yves Strub on 14 October 2019, 08:39:46 UTC
- call by value reduction strategy. - user defined reduction rules. Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> Co-authored-by: Benjamin Gregoire <benjamin.gregoire@inria.fr>
1 parent 651df3f
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)
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...