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.mli
(* --------------------------------------------------------------------
* 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
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
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)
: S with type item = I.t
and type data = D.data
and type effects = D.effects
(* -------------------------------------------------------------------- *)
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) : US with type item = I.t