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
ecUFind.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
open EcUtils
(* -------------------------------------------------------------------- *)
module type Item = sig
type t
val equal : t -> t -> bool
val compare: t -> t -> int
end
(* -------------------------------------------------------------------- *)
module type Data = sig
type data
type effects
val default : data
val isvoid : data -> bool
val noeffects : effects
val union : data -> data -> data * effects
end
(* -------------------------------------------------------------------- *)
module type S = sig
type item
type data
type effects
type t
val initial: t
val find : item -> t -> item
val same : item -> item -> t -> bool
val data : item -> t -> data
val set : item -> data -> t -> t
val isset : item -> t -> bool
val union : item -> item -> t -> t * effects
val domain: t -> item list
val closed: t -> bool
val opened: t -> int
end
(* -------------------------------------------------------------------- *)
module Make (I : Item) (D : Data) = struct
type item = I.t
type data = D.data
type effects = D.effects
type link =
| Root of int * data
| Link of item
module M = Map.Make(I)
type t = {
mutable forest: link M.t;
(*---*) nvoids: int;
}
(* ------------------------------------------------------------------ *)
let initial = { forest = M.empty; nvoids = 0; }
(* ------------------------------------------------------------------ *)
let xfind =
let rec follow (pitem : item) (item : item) (uf : t) =
match oget (M.find_opt item uf.forest) with
| Root (w, data) -> (item, w, Some data)
| Link nitem ->
let (nitem, _, _) as aout = follow item nitem uf in
uf.forest <- M.add pitem (Link nitem) uf.forest;
aout
in
fun (item : item) (uf : t) ->
match M.find_opt item uf.forest with
| None -> (item, 0, None)
| Some (Root (w, data)) -> (item, w, Some data)
| Some (Link next) -> follow item next uf
(* ------------------------------------------------------------------ *)
let find (item : item) (uf : t) =
let (item, _, _) = xfind item uf in item
(* ------------------------------------------------------------------ *)
let same (item1 : item) (item2 : item) (uf : t) =
I.equal (find item1 uf) (find item2 uf)
(* ------------------------------------------------------------------ *)
let data (item : item) (uf : t) =
let (_, _, data) = xfind item uf in odfl D.default data
(* ------------------------------------------------------------------ *)
let set (item : item) (data : data) (uf : t) =
let (item, w, olddata) = xfind item uf in
{ forest = M.add item (Root (w, data)) uf.forest;
nvoids = uf.nvoids
- (odfl 0 (olddata |> omap (int_of_bool |- D.isvoid)))
+ (int_of_bool (D.isvoid data)); }
(* ------------------------------------------------------------------ *)
let isset (item : item) (uf : t) =
M.mem item uf.forest
(* ------------------------------------------------------------------ *)
let union (item1 : item) (item2 : item) (uf : t) =
let (item1, w1, data1) = xfind item1 uf
and (item2, w2, data2) = xfind item2 uf in
if I.equal item1 item2 then
(uf, D.noeffects)
else
let (data, effects) = D.union (odfl D.default data1) (odfl D.default data2) in
let root = Root (w1 + w2, data) in
let (link1, link2) =
if w1 >= w2
then (root, Link item1)
else (Link item2, root)
in
let uf =
{ forest = M.add item1 link1 (M.add item2 link2 uf.forest);
nvoids = uf.nvoids
- (odfl 0 (data1 |> omap (int_of_bool |- D.isvoid)) +
odfl 0 (data2 |> omap (int_of_bool |- D.isvoid)))
+ (int_of_bool (D.isvoid data)); }
in
(uf, effects)
(* ------------------------------------------------------------------ *)
let domain (uf : t) =
M.keys uf.forest
(* ------------------------------------------------------------------ *)
let closed (uf : t) =
uf.nvoids = 0
(* ------------------------------------------------------------------ *)
let opened (uf : t) =
uf.nvoids
end
(* -------------------------------------------------------------------- *)
module type US = sig
type item
type t
val initial : t
val find : item -> t -> item
val union : item -> item -> t -> t
val same : item -> item -> t ->bool
end
(* -------------------------------------------------------------------- *)
module UMake (I : Item) = struct
module D
: Data with type data = unit and type effects = unit
= struct
type data = unit
type effects = unit
let default : data =
()
let isvoid (_ : data) =
false
let noeffects : effects =
()
let union () () =
((), ())
end
module UF = Make(I)(D)
type item = I.t
type data = D.data
type effects = D.effects
type t = UF.t
let initial = UF.initial
let find (x : item) (uf : t) =
UF.find x uf
let union (x1 : item) (x2 : item) (uf : t) =
fst (UF.union x1 x2 uf)
let same (x1 : item) (x2 : item) (uf : t) =
UF.same x1 x2 uf
end