Skip to content

GitLab

why3
why3
Commit 09cd77de authored by François Bobot's avatar François Bobot
Browse files
Options

stdlib : inline the signature of Set in the module Map 

in order to cope with a "two view" syndrom in util.ml/.mli

Perhaps another solution exists
parent ded85826
Hide whitespace changes
Inline Side-by-side
Showing with 199 additions and 172 deletions
src/core/decl.mli
View file @ 09cd77de
......@@ -62,8 +62,8 @@ type prsymbol = private {
pr_name : ident;
}
module Spr : Set.S with type elt = prsymbol
module Mpr : Map.S with type key = prsymbol
module Spr : Mpr.Set
module Hpr : Hashtbl.S with type key = prsymbol
module Wpr : Hashweak.S with type key = prsymbol
......@@ -100,8 +100,8 @@ and decl_node =
| Dind of ind_decl list (* inductive predicates *)
| Dprop of prop_decl (* axiom / lemma / goal *)
module Sdecl : Set.S with type elt = decl
module Mdecl : Map.S with type key = decl
module Sdecl : Mdecl.Set
module Wdecl : Hashweak.S with type key = decl
val d_equal : decl -> decl -> bool
......
src/core/ident.mli
View file @ 09cd77de
......@@ -42,7 +42,7 @@ and origin =
| Fresh
module Mid : Map.S with type key = ident
module Sid : Mid.SetS
module Sid : Mid.Set
module Hid : Hashtbl.S with type key = ident
val id_equal : ident -> ident -> bool
......
src/core/term.mli
View file @ 09cd77de
......@@ -31,8 +31,8 @@ type vsymbol = private {
vs_ty : ty;
}
module Svs : Set.S with type elt = vsymbol
module Mvs : Map.S with type key = vsymbol
module Svs : Mvs.Set
module Hvs : Hashtbl.S with type key = vsymbol
val vs_equal : vsymbol -> vsymbol -> bool
......@@ -48,8 +48,8 @@ type lsymbol = private {
ls_value : ty option;
}
module Sls : Set.S with type elt = lsymbol
module Mls : Map.S with type key = lsymbol
module Sls : Mls.Set
module Hls : Hashtbl.S with type key = lsymbol
module Wls : Hashweak.S with type key = lsymbol
......@@ -176,12 +176,12 @@ and expr =
and trigger = expr list
module Sterm : Set.S with type elt = term
module Mterm : Map.S with type key = term
module Sterm : Mterm.Set
module Hterm : Hashtbl.S with type key = term
module Sfmla : Set.S with type elt = fmla
module Mfmla : Map.S with type key = fmla
module Sfmla : Mfmla.Set
module Hfmla : Hashtbl.S with type key = fmla
val t_equal : term -> term -> bool
......
src/core/theory.mli
View file @ 09cd77de
......@@ -26,8 +26,8 @@ open Ty
open Term
open Decl
module Snm : Set.S with type elt = string
module Mnm : Map.S with type key = string
module Snm : Mnm.Set
type namespace = private {
ns_ts : tysymbol Mnm.t; (* type symbols *)
......@@ -64,8 +64,8 @@ type meta = private {
meta_tag : int;
}
module Smeta : Set.S with type elt = meta
module Mmeta : Map.S with type key = meta
module Smeta : Mmeta.Set
module Hmeta : Hashtbl.S with type key = meta
val meta_equal : meta -> meta -> bool
......@@ -99,8 +99,8 @@ and tdecl_node = private
| Clone of theory * tysymbol Mts.t * lsymbol Mls.t * prsymbol Mpr.t
| Meta of meta * meta_arg list
module Stdecl : Set.S with type elt = tdecl
module Mtdecl : Map.S with type key = tdecl
module Stdecl : Mtdecl.Set
module Htdecl : Hashtbl.S with type key = tdecl
val td_equal : tdecl -> tdecl -> bool
......
src/core/ty.mli
View file @ 09cd77de
......@@ -26,8 +26,8 @@ type tvsymbol = private {
tv_name : ident;
}
module Stv : Set.S with type elt = tvsymbol
module Mtv : Map.S with type key = tvsymbol
module Stv : Mtv.Set
module Htv : Hashtbl.S with type key = tvsymbol
val tv_equal : tvsymbol -> tvsymbol -> bool
......@@ -53,13 +53,13 @@ and ty_node = private
| Tyvar of tvsymbol
| Tyapp of tysymbol * ty list
module Sts : Set.S with type elt = tysymbol
module Mts : Map.S with type key = tysymbol
module Sts : Mts.Set
module Hts : Hashtbl.S with type key = tysymbol
module Wts : Hashweak.S with type key = tysymbol
module Sty : Set.S with type elt = ty
module Mty : Map.S with type key = ty
module Sty : Mty.Set
module Hty : Hashtbl.S with type key = ty
module Wty : Hashweak.S with type key = ty
......
src/util/stdlib.ml
View file @ 09cd77de
......@@ -21,38 +21,6 @@ module type OrderedType =
val compare: t -> t -> int
end
module type SetS =
sig
type elt
type t
val empty: t
val is_empty: t -> bool
val mem: elt -> t -> bool
val add: elt -> t -> t
val singleton: elt -> t
val remove: elt -> t -> t
val merge: (elt -> bool -> bool -> bool) -> t -> t -> t
val compare: t -> t -> int
val equal: t -> t -> bool
val subset: t -> t -> bool
val iter: (elt -> unit) -> t -> unit
val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all: (elt -> bool) -> t -> bool
val exists: (elt -> bool) -> t -> bool
val filter: (elt -> bool) -> t -> t
val partition: (elt -> bool) -> t -> t * t
val cardinal: t -> int
val elements: t -> elt list
val min_elt: t -> elt
val max_elt: t -> elt
val choose: t -> elt
val split: elt -> t -> t * bool * t
val change : elt -> (bool -> bool) -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
end
module type S =
sig
type key
......@@ -92,9 +60,40 @@ module type S =
val find_default : key -> 'a -> 'a t -> 'a
val mapi_fold:
(key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
module type SetS = SetS with type elt = key and type t = unit t
module Set : SetS
module type Set =
sig
type elt = key
type set = unit t
type t = set
val empty: t
val is_empty: t -> bool
val mem: elt -> t -> bool
val add: elt -> t -> t
val singleton: elt -> t
val remove: elt -> t -> t
val merge: (elt -> bool -> bool -> bool) -> t -> t -> t
val compare: t -> t -> int
val equal: t -> t -> bool
val subset: t -> t -> bool
val iter: (elt -> unit) -> t -> unit
val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all: (elt -> bool) -> t -> bool
val exists: (elt -> bool) -> t -> bool
val filter: (elt -> bool) -> t -> t
val partition: (elt -> bool) -> t -> t * t
val cardinal: t -> int
val elements: t -> elt list
val min_elt: t -> elt
val max_elt: t -> elt
val choose: t -> elt
val split: elt -> t -> t * bool * t
val change : elt -> (bool -> bool) -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
end
module Set : Set
end
......@@ -470,7 +469,38 @@ module Make(Ord: OrderedType) = struct
let acc,r' = mapi_fold f r acc in
acc,Node(l', v, d', r', h)
module type SetS = SetS with type elt = key and type t = unit t
module type Set =
sig
type elt = key
type set = unit t
type t = set
val empty: t
val is_empty: t -> bool
val mem: elt -> t -> bool
val add: elt -> t -> t
val singleton: elt -> t
val remove: elt -> t -> t
val merge: (elt -> bool -> bool -> bool) -> t -> t -> t
val compare: t -> t -> int
val equal: t -> t -> bool
val subset: t -> t -> bool
val iter: (elt -> unit) -> t -> unit
val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all: (elt -> bool) -> t -> bool
val exists: (elt -> bool) -> t -> bool
val filter: (elt -> bool) -> t -> t
val partition: (elt -> bool) -> t -> t * t
val cardinal: t -> int
val elements: t -> elt list
val min_elt: t -> elt
val max_elt: t -> elt
val choose: t -> elt
val split: elt -> t -> t * bool * t
val change : elt -> (bool -> bool) -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
end
module Set =
struct
......
src/util/stdlib.mli
View file @ 09cd77de
......@@ -40,120 +40,6 @@ module type OrderedType =
end
(** Input signature of the functor {!Map.Make}. *)
module type SetS =
sig
type elt
type t
(** The type of sets of type [elt]. *)
val empty: t
(** The empty set. *)
val is_empty: t -> bool
(** Test whether a set is empty or not. *)
val mem: elt -> t -> bool
(** [mem x s] returns [true] if [s] contains [x],
and [false] otherwise. *)
val add: elt -> t -> t
(** [add x s] returns a set containing the same elements as
[s], plus [x]. *)
val singleton: elt -> t
(** [singleton x] returns the one-element set that contains [x]. *)
val remove: elt -> t -> t
(** [remove x s] returns a set containing the same elements as [s],
except for [x]. *)
val merge: (elt -> bool -> bool -> bool) -> t -> t -> t
(** [merge f s1 s2] computes a set whose elts is a subset of elts
of [s1] and of [s2]. The presence of each such element is
determined with the function [f]. *)
val compare: t -> t -> int
(** Total ordering between sets. *)
val equal: t -> t -> bool
(** [equal s1 s2] tests whether the sets [s1] and [s2] are equal. *)
val subset: t -> t -> bool
(** [subset s1 s2] tests whether the set [s1] is a subset of [s2]. *)
val iter: (elt -> unit) -> t -> unit
(** [iter f s] applies [f] to all elements of [s].
The elements are passed to [f] in increasing order with respect
to the ordering over the type of the elts. *)
val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
(** [fold f s a] computes [(f eN ... (f e1 a)...)],
where [e1 ... eN] are the element of [s] in increasing order. *)
val for_all: (elt -> bool) -> t -> bool
(** [for_all p s] checks if all the elements of [s] satisfy
the predicate [p]. *)
val exists: (elt -> bool) -> t -> bool
(** [exists p s] checks if at least one element of [s] satisfies
the predicate [p]. *)
val filter: (elt -> bool) -> t -> t
(** [filter p s] returns the set with all the elements of [s]
that satisfy predicate [p]. *)
val partition: (elt -> bool) -> t -> t * t
(** [partition p s] returns a pair of sets [(s1, s2)], where
[s1] contains all the elements of [s] that satisfy the
predicate [p], and [s2] is the map with all the elements of
[s] that do not satisfy [p]. *)
val cardinal: t -> int
(** Return the number of elements in a set. *)
val elements: t -> elt list
(** Return the list of all elements of the given set.
The returned list is sorted in increasing order. *)
val min_elt: t -> elt
(** Return the smallest element of the given set or raise
[Not_found] if the set is empty. *)
val max_elt: t -> elt
(** Return the largest element of the given set or raise
[Not_found] if the set is empty. *)
val choose: t -> elt
(** Return one element of the given set, or raise [Not_found] if
the set is empty. Which element is chosen is unspecified,
but equal elements will be chosen for equal sets. *)
val split: elt -> t -> t * bool * t
(** [split x s] returns a triple [(l, mem, r)], where
[l] is the set with all the elements of [s] that are
strictly less than [x];
[r] is the set with all the elements of [s] that are
strictly greater than [x];
[mem] is [true] if [x] belongs to [s] and [false] otherwise. *)
val change : elt -> (bool -> bool) -> t -> t
(** [change x f s] returns a set containing the same elements as
[s], except [x] which is added to [s] if [f (mem x s)] returns
[true] and removed otherwise. *)
val union : t -> t -> t
(** [union f s1 s2] computes the union of two sets *)
val inter : t -> t -> t
(** [inter f s1 s2] computes the intersection of two sets *)
val diff : t -> t -> t
(** [diss f s1 s2] computes the difference of two sets *)
end
module type S =
sig
type key
......@@ -342,11 +228,122 @@ module type S =
val mapi_fold:
(key -> 'a -> 'acc -> 'acc * 'b)-> 'a t -> 'acc -> 'acc * 'b t
(** fold and map at the same time *)
(** fold and map at the same time *)
module type Set =
sig
type elt = key
type set = unit t
type t = set
(** The type of sets of type [elt]. *)
val empty: t
(** The empty set. *)
val is_empty: t -> bool
(** Test whether a set is empty or not. *)
val mem: elt -> t -> bool
(** [mem x s] returns [true] if [s] contains [x],
and [false] otherwise. *)
val add: elt -> t -> t
(** [add x s] returns a set containing the same elements as
[s], plus [x]. *)
val singleton: elt -> t
(** [singleton x] returns the one-element set that contains [x]. *)
val remove: elt -> t -> t
(** [remove x s] returns a set containing the same elements as [s],
except for [x]. *)
val merge: (elt -> bool -> bool -> bool) -> t -> t -> t
(** [merge f s1 s2] computes a set whose elts is a subset of elts
of [s1] and of [s2]. The presence of each such element is
determined with the function [f]. *)
val compare: t -> t -> int
(** Total ordering between sets. *)
val equal: t -> t -> bool
(** [equal s1 s2] tests whether the sets [s1] and [s2] are equal. *)
val subset: t -> t -> bool
(** [subset s1 s2] tests whether the set [s1] is a subset of [s2]. *)
val iter: (elt -> unit) -> t -> unit
(** [iter f s] applies [f] to all elements of [s].
The elements are passed to [f] in increasing order with respect
to the ordering over the type of the elts. *)
val fold: (elt -> 'a -> 'a) -> t -> 'a -> 'a
(** [fold f s a] computes [(f eN ... (f e1 a)...)],
where [e1 ... eN] are the element of [s] in increasing order. *)
val for_all: (elt -> bool) -> t -> bool
(** [for_all p s] checks if all the elements of [s] satisfy
the predicate [p]. *)
val exists: (elt -> bool) -> t -> bool
(** [exists p s] checks if at least one element of [s] satisfies
the predicate [p]. *)
val filter: (elt -> bool) -> t -> t
(** [filter p s] returns the set with all the elements of [s]
that satisfy predicate [p]. *)
val partition: (elt -> bool) -> t -> t * t
(** [partition p s] returns a pair of sets [(s1, s2)], where
[s1] contains all the elements of [s] that satisfy the
predicate [p], and [s2] is the map with all the elements of
[s] that do not satisfy [p]. *)
val cardinal: t -> int
(** Return the number of elements in a set. *)
val elements: t -> elt list
(** Return the list of all elements of the given set.
The returned list is sorted in increasing order. *)
val min_elt: t -> elt
(** Return the smallest element of the given set or raise
[Not_found] if the set is empty. *)
val max_elt: t -> elt
(** Return the largest element of the given set or raise
[Not_found] if the set is empty. *)
val choose: t -> elt
(** Return one element of the given set, or raise [Not_found] if
the set is empty. Which element is chosen is unspecified,
but equal elements will be chosen for equal sets. *)
val split: elt -> t -> t * bool * t
(** [split x s] returns a triple [(l, mem, r)], where
[l] is the set with all the elements of [s] that are
strictly less than [x];
[r] is the set with all the elements of [s] that are
strictly greater than [x];
[mem] is [true] if [x] belongs to [s] and [false] otherwise. *)
val change : elt -> (bool -> bool) -> t -> t
(** [change x f s] returns a set containing the same elements as
[s], except [x] which is added to [s] if [f (mem x s)] returns
[true] and removed otherwise. *)
val union : t -> t -> t
(** [union f s1 s2] computes the union of two sets *)
val inter : t -> t -> t
(** [inter f s1 s2] computes the intersection of two sets *)
val diff : t -> t -> t
(** [diss f s1 s2] computes the difference of two sets *)
module type SetS = SetS with type elt = key and type t = unit t
end
module Set : SetS
module Set : Set
end
......
src/util/util.ml
View file @ 09cd77de
......@@ -115,11 +115,11 @@ let ffalse _ = false
module Int = struct type t = int let compare = Pervasives.compare end
module Sint = Set.Make(Int)
module Mint = Map.Make(Int)
module Sint = Mint.Set
module Sstr = Set.Make(String)
module Mstr = Map.Make(String)
module Sstr = Mstr.Set
(* Set, Map, Hashtbl on structures with a unique tag *)
......
src/util/util.mli
View file @ 09cd77de
......@@ -90,11 +90,11 @@ val ttrue : 'a -> bool
(* Set and Map on ints and strings *)
module Sint : Set.S with type elt = int
module Mint : Map.S with type key = int
module Sint : Mint.Set
module Sstr : Set.S with type elt = string
module Mstr : Map.S with type key = string
module Sstr : Mstr.Set
val memo_int : int -> (int -> 'a) -> int -> 'a
......@@ -120,14 +120,14 @@ module OrderedHashList (X : Tagged) : OrderedHash with type t = X.t list
module StructMake (X : Tagged) :
sig
module M : Map.S with type key = X.t
module S : M.SetS
module S : M.Set with type elt = X.t
module H : Hashtbl.S with type key = X.t
end
module WeakStructMake (X : Hashweak.Weakey) :
sig
module M : Map.S with type key = X.t
module S : M.SetS
module S : M.Set
module H : Hashtbl.S with type key = X.t
module W : Hashweak.S with type key = X.t
end
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment