projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
ajout d'un compteur pour compter le nombre de noeuds évalués
[tatoo.git]
/
src
/
finiteCofinite.ml
diff --git
a/src/finiteCofinite.ml
b/src/finiteCofinite.ml
index
8d3c3ee
..
9963e1f
100644
(file)
--- a/
src/finiteCofinite.ml
+++ b/
src/finiteCofinite.ml
@@
-13,16
+13,12
@@
(* *)
(***********************************************************************)
(* *)
(***********************************************************************)
-(*
- Time-stamp: <Last modified on 2013-01-30 19:09:01 CET by Kim Nguyen>
-*)
-
INCLUDE "utils.ml"
INCLUDE "utils.ml"
-include
Sigs.FINITECOFINITE
+include
FiniteCofinite_sig
module type HConsBuilder =
module type HConsBuilder =
- functor (H :
Sigs.AUX
.HashedType) -> Hcons.S with type data = H.t
+ functor (H :
Common_sig
.HashedType) -> Hcons.S with type data = H.t
module Builder (HCB : HConsBuilder) (E : Ptset.S) :
S with type elt = E.elt and type set = E.t =
module Builder (HCB : HConsBuilder) (E : Ptset.S) :
S with type elt = E.elt and type set = E.t =
@@
-34,9
+30,9
@@
struct
type t = node
let equal a b =
match a, b with
type t = node
let equal a b =
match a, b with
- Finite
(s1), Finite (s2)
- | CoFinite
(s1), CoFinite (s2)
-> E.equal s1 s2
- | _ -> false
+ Finite
s1, Finite s2
+ | CoFinite
s1, CoFinite s2
-> E.equal s1 s2
+ |
(Finite _| CoFinite _),
_ -> false
let hash = function
| Finite s -> HASHINT2 (PRIME1, E.hash s)
let hash = function
| Finite s -> HASHINT2 (PRIME1, E.hash s)
@@
-48,20
+44,21
@@
struct
let finite x = make (Finite x)
let cofinite x = make (CoFinite x)
let finite x = make (Finite x)
let cofinite x = make (CoFinite x)
- let is_empty
= function
- |
{ node = Finite s } when E.is_empty s -> true
- |
_
-> false
+ let is_empty
t = match t.node with
+ |
Finite s -> E.is_empty s
+ |
CoFinite _
-> false
- let is_any
= function
- |
{ node = CoFinite s } when E.is_empty s -> true
- |
_
-> false
+ let is_any
t = match t.node with
+ |
CoFinite s -> E.is_empty s
+ |
Finite _
-> false
let is_finite t = match t.node with
let is_finite t = match t.node with
- | Finite _ -> true | _ -> false
+ | Finite _ -> true
+ | CoFinite _ -> false
let kind t = match t.node with
| Finite _ -> `Finite
let kind t = match t.node with
| Finite _ -> `Finite
- |
_
-> `Cofinite
+ |
CoFinite _
-> `Cofinite
let mem x t = match t.node with
| Finite s -> E.mem x s
let mem x t = match t.node with
| Finite s -> E.mem x s
@@
-124,26
+121,34
@@
struct
let rec next_finite_cofinite facc cacc = function
| [] -> finite facc, cofinite (E.diff cacc facc)
let rec next_finite_cofinite facc cacc = function
| [] -> finite facc, cofinite (E.diff cacc facc)
- | { node = Finite s } ::r ->
+ | { node = Finite s
; _
} ::r ->
next_finite_cofinite (E.union s facc) cacc r
next_finite_cofinite (E.union s facc) cacc r
- | { node = CoFinite _ } ::r when E.is_empty cacc ->
+ | { node = CoFinite _
; _
} ::r when E.is_empty cacc ->
next_finite_cofinite facc cacc r
next_finite_cofinite facc cacc r
- | { node = CoFinite s } ::r ->
+ | { node = CoFinite s
; _
} ::r ->
next_finite_cofinite facc (E.inter cacc s) r
in
let rec first_cofinite facc = function
| [] -> empty,empty
next_finite_cofinite facc (E.inter cacc s) r
in
let rec first_cofinite facc = function
| [] -> empty,empty
- | { node = Finite s } :: r-> first_cofinite (E.union s facc) r
- | { node = CoFinite s } :: r -> next_finite_cofinite facc s r
+ | { node = Finite s
; _
} :: r-> first_cofinite (E.union s facc) r
+ | { node = CoFinite s
; _
} :: r -> next_finite_cofinite facc s r
in
first_cofinite E.empty l
in
first_cofinite E.empty l
- let exn =
Sigs.FINITECOFINITE
.InfiniteSet
+ let exn =
FiniteCofinite_sig
.InfiniteSet
let fold f t a = match t.node with
| Finite s -> E.fold f s a
| CoFinite _ -> raise exn
let fold f t a = match t.node with
| Finite s -> E.fold f s a
| CoFinite _ -> raise exn
+ let fold_left f t a = match t.node with
+ | Finite s -> E.fold_left f s a
+ | CoFinite _ -> raise exn
+
+ let fold_right f t a = match t.node with
+ | Finite s -> E.fold_right f s a
+ | CoFinite _ -> raise exn
+
let iter f t = match t.node with
| Finite t -> E.iter f t
| CoFinite _ -> raise exn
let iter f t = match t.node with
| Finite t -> E.iter f t
| CoFinite _ -> raise exn
@@
-177,42
+182,40
@@
struct
let choose t = match t.node with
Finite s -> E.choose s
let choose t = match t.node with
Finite s -> E.choose s
- | _ -> raise exn
+ |
CoFinite
_ -> raise exn
let is_singleton t = match t.node with
| Finite s -> E.is_singleton s
let is_singleton t = match t.node with
| Finite s -> E.is_singleton s
- | _ -> false
+ |
CoFinite
_ -> false
let intersect s t = match s.node, t.node with
| Finite s, Finite t -> E.intersect s t
| CoFinite s, Finite t -> not (E.subset t s)
| Finite s, CoFinite t -> not (E.subset s t)
let intersect s t = match s.node, t.node with
| Finite s, Finite t -> E.intersect s t
| CoFinite s, Finite t -> not (E.subset t s)
| Finite s, CoFinite t -> not (E.subset s t)
- | CoFinite
s, CoFinite t
-> true
+ | CoFinite
_ , CoFinite _
-> true
let split x s = match s.node with
| Finite s ->
let s1, b, s2 = E.split x s in
finite s1, b, finite s2
let split x s = match s.node with
| Finite s ->
let s1, b, s2 = E.split x s in
finite s1, b, finite s2
- | _ -> raise exn
+ |
CoFinite
_ -> raise exn
let min_elt s = match s.node with
| Finite s -> E.min_elt s
let min_elt s = match s.node with
| Finite s -> E.min_elt s
- | _ -> raise exn
+ |
CoFinite
_ -> raise exn
let max_elt s = match s.node with
| Finite s -> E.min_elt s
let max_elt s = match s.node with
| Finite s -> E.min_elt s
- | _ -> raise exn
+ |
CoFinite
_ -> raise exn
- let positive t =
- match t.node with
- | Finite x -> x
- | _ -> E.empty
+ let positive t = match t.node with
+ | Finite x -> x
+ | CoFinite _ -> E.empty
- let negative t =
- match t.node with
- | CoFinite x -> x
- | _ -> E.empty
+ let negative t = match t.node with
+ | CoFinite x -> x
+ | Finite _ -> E.empty
let inj_positive t = finite t
let inj_negative t = cofinite t
let inj_positive t = finite t
let inj_negative t = cofinite t