projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Add a tiny XML file to help debug automata behaviour.
[tatoo.git]
/
src
/
finiteCofinite.ml
diff --git
a/src/finiteCofinite.ml
b/src/finiteCofinite.ml
index
1c8e6ef
..
9963e1f
100644
(file)
--- a/
src/finiteCofinite.ml
+++ b/
src/finiteCofinite.ml
@@
-12,16
+12,13
@@
(* ../LICENSE. *)
(* *)
(***********************************************************************)
(* ../LICENSE. *)
(* *)
(***********************************************************************)
+
INCLUDE "utils.ml"
INCLUDE "utils.ml"
-module type S =
- sig
- include Sigs.FiniteCofiniteSet
- include Hcons.S with type t := t
- end
+include FiniteCofinite_sig
module type HConsBuilder =
module type HConsBuilder =
- functor (H :
Sigs
.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 =
@@
-33,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)
@@
-47,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
@@
-123,93
+121,101
@@
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 = FiniteCofinite_sig.InfiniteSet
+
let fold f t a = match t.node with
| Finite s -> E.fold f s a
let fold f t a = match t.node with
| Finite s -> E.fold f s a
- | CoFinite _ -> raise Sigs.InfiniteSet
+ | 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
let iter f t = match t.node with
| Finite t -> E.iter f t
- | CoFinite _ -> raise
Sigs.InfiniteSet
+ | CoFinite _ -> raise
exn
let for_all f t = match t.node with
| Finite s -> E.for_all f s
let for_all f t = match t.node with
| Finite s -> E.for_all f s
- | CoFinite _ -> raise
Sigs.InfiniteSet
+ | CoFinite _ -> raise
exn
let exists f t = match t.node with
| Finite s -> E.exists f s
let exists f t = match t.node with
| Finite s -> E.exists f s
- | CoFinite _ -> raise
Sigs.InfiniteSet
+ | CoFinite _ -> raise
exn
let filter f t = match t.node with
| Finite s -> finite (E.filter f s)
let filter f t = match t.node with
| Finite s -> finite (E.filter f s)
- | CoFinite _ -> raise
Sigs.InfiniteSet
+ | CoFinite _ -> raise
exn
let partition f t = match t.node with
| Finite s -> let a,b = E.partition f s in finite a,finite b
let partition f t = match t.node with
| Finite s -> let a,b = E.partition f s in finite a,finite b
- | CoFinite _ -> raise
Sigs.InfiniteSet
+ | CoFinite _ -> raise
exn
let cardinal t = match t.node with
| Finite s -> E.cardinal s
let cardinal t = match t.node with
| Finite s -> E.cardinal s
- | CoFinite _ -> raise
Sigs.InfiniteSet
+ | CoFinite _ -> raise
exn
let elements t = match t.node with
| Finite s -> E.elements s
let elements t = match t.node with
| Finite s -> E.elements s
- | CoFinite _ -> raise
Sigs.InfiniteSet
+ | CoFinite _ -> raise
exn
let from_list l =
finite (List.fold_left (fun x a -> E.add a x ) E.empty l)
let choose t = match t.node with
Finite s -> E.choose s
let from_list l =
finite (List.fold_left (fun x a -> E.add a x ) E.empty l)
let choose t = match t.node with
Finite s -> E.choose s
- |
_ -> raise Sigs.InfiniteSet
+ |
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 Sigs.InfiniteSet
+ |
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 Sigs.InfiniteSet
+ |
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 Sigs.InfiniteSet
+ |
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