# Library IntSet

Require Import
Coqlib Utf8 String PrintPos ToString
Integers
Maps TreeAl
IntervalDomain.

Module P := Tree_Properties( ZTree ).

Definition int_set : Type := ZTree.t unit.
Definition proj (i: int) : Z := Int.unsigned i.

Notation "x ∈ S" := (ZTree.get x S = Some tt): int_set_scope.

Local Open Scope int_set_scope.

Definition Mem (x: int) (S: int_set) := (proj x) S.

Definition mem x S : { x S } + { ¬ x S }.

Notation "x ∈? S" := (mem x S) (at level 19): int_set_scope.

Definition empty : int_set := ZTree.empty _.

Definition forallb (f: Z bool) (s: int_set) : bool :=
P.for_all s (fun x _f x).

Lemma forallb_forall {f x r} :
forallb f r = true x r f x = true.

Definition of_list' (l: list int) : int_set int_set :=
List.fold_left
(fun acc iZTree.set (proj i) tt acc)
l.

Definition of_list (l: list int) : int_set :=
of_list' l (ZTree.empty _).

Lemma of_list'_iff : l acc i, List.In i l (proj i) acc (proj i) (of_list' l acc).

Lemma of_list_iff : l i, List.In i l (proj i) (of_list l).

Definition fold {A} (f: A int A) : int_set A A :=
ZTree.fold (fun x y (_:unit) ⇒ f x (Int.repr y)).

Definition as_list (m: int_set) : list int :=
fold (λ l i, i :: l) m nil.

Lemma as_list_iff : m i, List.In i (as_list m) j, j m Int.repr j = i.

Definition fs_size (x: int_set) : N :=
ZTree.fold (fun n _ _Nsucc n) x N0.

Definition int_set_LE (x y: int_set) :=
i : Z, i x i y.

Definition int_set_LE_dec (x y: int_set) : { int_set_LE x y } + { ¬ int_set_LE x y }.

Definition is_empty (x: int_set) : bool :=
int_set_LE_dec x (ZTree.empty _).

Lemma is_empty_correct (x: int_set) :
is_empty x = true
y, ¬ y x.

Definition singleton (i: int) : int_set := ZTree.set (proj i) tt (ZTree.empty _).

Definition union (x y: int_set) : int_set :=
ZTree.combine
(fun l r
match l, r with
| None, NoneNone
| Some tt, _
| _, Some ttSome tt
end) x y.

Lemma union_comm (x y: int_set) : union x y = union y x.

Lemma union_in_l (x y: int_set) :
i: Z, i x i union x y.

Lemma union_in_r (x y: int_set) :
i: Z, i y i union x y.

Definition intersection (x y: int_set) : int_set :=
ZTree.combine
(fun l r
match l, r with
| Some tt, Some ttSome tt
| _, _None
end) x y.

Lemma intersection_correct (x y: int_set) :
i : Z, i x i y i intersection x y.

Lemma intersection_exact (x y: int_set) :
i : Z, i intersection x y i x i y.

Instance toString : ToString int_set :=
{ to_string x :=
("{ " ++
ZTree.fold
(fun s i _string_of_z i ++ "; " ++ s)
x
"}"
)%string
}.

Returns the minimal and maximal elements. None if empty.
Definition min_max (interp: Z Z) (x: int_set) : option (Z × Z) :=
ZTree.fold
(fun m k _
match m with
| NoneSome (k,k)
| Some (l, r)
let k' := interp k in
let l' := interp l in
let r' := interp r in
if Z_le_gt_dec k' l' then Some (k, r)
else if Z_le_gt_dec r' k' then Some (l, k)
else m
end)
x
None.

Lemma min_max_spec (interp: Z Z) (x: int_set) :
match min_max interp x with
| Noneis_empty x = true
| Some (l,r)l x r x i, i x interp l interp i interp r
end.

Definition fint_set : Type := int_set+⊤.

Definition fempty : fint_set := Just (ZTree.empty _).

Definition fs_widen (old new: int_set) : fint_set :=
if int_set_LE_dec new old
then Just old
else
let j : int_set := union old new in
if N.leb 10%N (fs_size j)
then All
else Just j.

Instance fs_gamma : gamma_op fint_set int := fun x
match x with
| Allfun _True
| Just sfun iproj i s
end.

Lemma fempty_gamma i : ¬ fs_gamma fempty i.

Definition int_set_pl : pre_lattice int_set :=
{| pl_leb x y := int_set_LE_dec x y
; pl_join x y := Just (union x y)
; pl_widen x y := fs_widen x y
|}.

Instance int_set_wl : weak_lattice fint_set :=
weak_lattice_of_pre_lattice int_set_pl.

Definition fs_reduce (x: int_set) : fint_set+⊥ :=
if is_empty x
then Bot
else NotBot (Just x).

Definition fs_meet (x y: fint_set) : fint_set+⊥ :=
match x, y with
| All, _NotBot y
| _, AllNotBot x
| Just x', Just y'fs_reduce (intersection x' y')
end.

Lemma fs_meet_sound : x y: fint_set, (γ x) (γ y) γ (fs_meet x y).

Lemma fs_meet_glb : x y: fint_set, γ (fs_meet x y) (γ x) (γ y).

Definition fs_const : int fint_set := @Just _ singleton.

Definition fs_booleans : fint_set :=
Just (union (singleton Int.zero) (singleton Int.one)).

Definition map (f: Z Z) (s: int_set) : int_set :=
ZTree.fold (fun m k _ZTree.set (f k) tt m) s (ZTree.empty unit).

Lemma map_in f (s: int_set) : x, x s f x map f s.

Definition fs_unop (op: int int) : fint_set fint_set+⊥ :=
fun x
match x with
| AllNotBot x
| Just x'NotBot (Just (map (fun iproj (op (Int.repr i))) x'))
end.

Definition map2 (f: Z Z Z) (l r: int_set) : int_set :=
ZTree.fold (fun m i _
ZTree.fold (fun m j _ZTree.set (f i j) tt m) r m ) l (ZTree.empty unit).

Lemma map2_in f (l r: int_set) : x y, x l y r f x y map2 f l r.

Definition fs_binop (op: int int int) (x: fint_set) (y: fint_set) : fint_set+⊥ :=
match x, y with
| All, _
| _, AllNotBot All
| Just x', Just y'NotBot (Just (map2 (fun a bproj (op (Int.repr a) (Int.repr b))) x' y'))
end.

Definition int_set_unsigned_range (x: int_set) :=
match min_max (fun ii) x with
| NoneBot
| Some (l,r)NotBot {| Interval.min := l; Interval.max := r |}
end.

Definition int_set_signed_range (x: int_set) :=
let interp := Int.signed Int.repr in
match min_max interp x with
| NoneBot
| Some (l,r)NotBot {| Interval.min := interp l; Interval.max := interp r |}
end.

Definition fs_range (x: fint_set) :=
match x with
| Allfun sNotBot (match s with SignedInterval.top | UnsignedInterval.utop end)
| Just x'fun s
match s with
| Signedint_set_signed_range x'
| Unsignedint_set_unsigned_range x'
end
end.

Definition fs_is_in_itv (l r: int) (x: fint_set) : bool :=
match x with
| Allfalse
| Just x'forallb (fun inegb (Int.lt r (Int.repr i)) && negb (Int.lt (Int.repr i) l)) x'
end.