Library IntSet

Require Import
  Coqlib Utf8 String PrintPos ToString
  Maps TreeAl
  LatticeSignatures AdomLib

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 :=
    (fun acc iZTree.set (proj i) tt acc)

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 :=
    (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 :=
    (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 :=
  ("{ " ++
        (fun s i _string_of_z i ++ "; " ++ s)

Returns the minimal and maximal elements. None if empty.
Definition min_max (interp: Z Z) (x: int_set) : option (Z × Z) :=
    (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

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

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
    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

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.

Lemma int_set_adom : adom fint_set int int_set_wl fs_gamma.

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')

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 (singleton

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'))

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'))

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 |}

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 |}

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

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