Module AbNumDomain

Require Import
  Coqlib Utf8
  Integers DLib
  LatticeSignatures
  AbEnvironment
  IntervalDomain.

Set Implicit Arguments.

Ltac bot :=
  repeat match goal with |- context[match ?a with Bot => _ | NotBot _ => _ end] => case_eq a end.

Definition lift_unop (op: int → int) (A: ℘ int) : ℘ int :=
  fun i => ∃ j, A j ∧ i = (op j).

Definition lift_binop (op: int → int → int) (A B: ℘ int) : ℘ int :=
  fun i => ∃ a, ∃ b, A a ∧ B b ∧ i = (op a b).


Unset Elimination Schemes.
Class num_dom (t:Type) : Type :=
{ as_adom :> adom t int

; meet: t → t+⊥ → t+⊥

; const: int → t
; booleans: t
; range: t → sign_flag → Interval.itv+⊥

; neg: t → t+⊥
; not: t → t+⊥
; notbool: t → t+⊥
; boolval: t → t+⊥

; add: t → t → t+⊥
; sub: t → t → t+⊥
; mul: t → t → t+⊥
; divs: t → t → t+⊥
; shl: t → t → t+⊥

; and: t → t → t+⊥
; or: t → t → t+⊥
; xor: t → t → t+⊥

; is_in_itv: int → int → t → bool

; backward_boolval: t → t → t+⊥
; backward_notbool: t → t → t+⊥
; backward_neg: t → t → t+⊥
; backward_not: t → t → t+⊥

; backward_add: t → t → t → t+⊥ * t+⊥
; backward_sub: t → t → t → t+⊥ * t+⊥
; backward_cmp: comparison → t → t → t → t+⊥ * t+⊥
; backward_cmpu: comparison → t → t → t → t+⊥ * t+⊥
; backward_and: t → t → t → list (t+⊥ * t+⊥)
; backward_or: t → t → t → list (t+⊥ * t+⊥)
}.

Definition backward_unop_correct (t:Type) `{adom t int}
           (aop: t → t → t+⊥)
           (op : int → int) : Prop :=
  ∀ x y : t,
  ∀ i : int,
    γ x i →
    γ y (op i) →
    γ (aop x y) i.

Definition backward_binop_correct (t:Type) `{adom t int}
           (aop: t → t → t → t+⊥ * t+⊥)
           (op : int → int → int) : Prop :=
  ∀ x y z : t,
  ∀ i j : int,
    γ x i →
    γ y j →
    γ z (op i j) →
    let '(u,v) := aop x y z in
    γ u i ∧ γ v j.

Definition backward_binop_list_correct (t:Type) `{adom t int}
           (aop: t → t → t → list (t+⊥ * t+⊥))
           (op : int → int → int) : Prop :=
  ∀ x y z : t,
  ∀ i j : int,
    γ x i →
    γ y j →
    γ z (op i j) →
    ∃ ab, In ab (aop x y z) ∧
    γ (fst ab) i ∧ γ (snd ab) j.

Class num_dom_correct t (D: num_dom t) : Prop :=
{ meet_correct: ∀ x y, (γ x) ∩ (γ y) ⊆ γ (meet x y)
; const_correct: ∀ n: int, γ (const n) n
; booleans_correct0: γ booleans Int.zero
; booleans_correct1: γ booleans Int.one
; range_correct: ∀ x:t, γ x ⊆ ints_in_range (range x)
; neg_correct: ∀ x: t, lift_unop Int.neg (γ x) ⊆ γ (neg x)
; not_correct: ∀ x: t, lift_unop Int.not (γ x) ⊆ γ (not x)
; notbool_correct: ∀ x: t, ∀ i, γ x i → γ (notbool x) (Interval.of_bool (Int.eq i Int.zero))
; boolval_correct: ∀ x: t, ∀ i, γ x i → γ (boolval x) (Interval.of_bool (negb (Int.eq i Int.zero)))
; add_correct: ∀ x y: t, lift_binop Int.add (γ x) (γ y) ⊆ γ (add x y)
; sub_correct: ∀ x y: t, lift_binop Int.sub (γ x) (γ y) ⊆ γ (sub x y)
; mul_correct: ∀ x y: t, lift_binop Int.mul (γ x) (γ y) ⊆ γ (mul x y)
; divs_correct: ∀ x y: t, lift_binop Int.divs (γ x) (γ y) ⊆ γ (divs x y)
; shl_correct: ∀ x y: t, lift_binop Int.shl (γ x) (γ y) ⊆ γ (shl x y)
; and_correct: ∀ x y: t, lift_binop Int.and (γ x) (γ y) ⊆ γ (and x y)
; or_correct: ∀ x y: t, lift_binop Int.or (γ x) (γ y) ⊆ γ (or x y)
; xor_correct: ∀ x y: t, lift_binop Int.xor (γ x) (γ y) ⊆ γ (xor x y)

; is_in_itv_correct (m M:int) : ∀ x: t, is_in_itv m M x = true →
    ∀ i, γ x i → Int.lt M i = false ∧ Int.lt i m = false

; backward_boolval_correct: backward_unop_correct (t:=t) backward_boolval
    (fun i => (Interval.of_bool (negb (Int.eq i Int.zero))))
; backward_notbool_correct: backward_unop_correct (t:=t) backward_notbool
    (fun i => (Interval.of_bool (Int.eq i Int.zero)))
; backward_neg_correct: backward_unop_correct (t:=t) backward_neg Int.neg
; backward_not_correct: backward_unop_correct (t:=t) backward_not Int.not

; backward_add_correct: backward_binop_correct (t:=t) backward_add Int.add
; backward_sub_correct: backward_binop_correct (t:=t) backward_sub Int.sub
; backward_cmp_correct: ∀ c, backward_binop_correct (t:=t) (backward_cmp c)
    (fun i j => (Interval.of_bool (Int.cmp c i j)))
; backward_cmpu_correct: ∀ c, backward_binop_correct (t:=t) (backward_cmpu c)
    (fun i j => (Interval.of_bool (Int.cmpu c i j)))

; backward_and_correct: backward_binop_list_correct (t:=t) backward_and Int.and
; backward_or_correct: backward_binop_list_correct (t:=t) backward_or Int.or
}.

Class reduction A B : Type := { ρ: A+⊥ → B+⊥ → (A * B)+⊥ }.
Class reduction_correct A B t (Ha:adom A t) (Hb:adom B t) `{reduction A B} : Prop :=
{ reduction_spec a b:
    γ a ∩ γ b ⊆
    match ρ a b with
      | Bot => ∅
      | NotBot (u,v) => γ u ∩ γ v
    end
}.

Definition botbind {A B} (f: A → B+⊥) (a: A+⊥) : B+⊥ :=
  match a with
    | Bot => Bot
    | NotBot x => f x
  end.

Definition red_prod_unop {A B} ρ (opa: A → A+⊥) (opb: B → B+⊥) : A*B → (A*B)+⊥ :=
  fun x => match x with (a,b) => ρ (opa a) (opb b) end.

Definition botbind2 {A B C} (f: A → B → C+⊥) (a: A+⊥) (b: B+⊥) : C+⊥ :=
  match a, b with
    | Bot, _
    | _, Bot => Bot
    | NotBot x, NotBot y => f x y
  end.

Definition red_prod_binop {A B} ρ (opa: A → A → A+⊥) (opb: B → B → B+⊥)
  : (A*B) → (A*B) → (A*B)+⊥ :=
  fun x y => match x,y with (a,b), (c,d) =>
                            ρ (opa a c) (opb b d)
             end.

Definition red_prod_backop_bin {A B} ρ (opa: A → A → A → A+⊥ * A+⊥) (opb: B → B → B → B+⊥ * B+⊥)
  : (A*B) → (A*B) → (A*B) → (A*B)+⊥ * (A*B)+⊥ :=
  fun x y z => match x,y,z with
               | (a,b), (c,d), (e,f) =>
                 let '(a',c') := opa a c e in
                 let '(b',d') := opb b d f in
                 (ρ a' b', ρ c' d')
             end.

Definition red_prod_backop_bin_list {A B} ρ
  (opa: A → A → A → list (A+⊥ * A+⊥)) (opb: B → B → B → list (B+⊥ * B+⊥))
  : (A*B) → (A*B) → (A*B) → list ((A*B)+⊥ * (A*B)+⊥) :=
  fun x y z => match x,y,z with
               | (a,b), (c,d), (e,f) =>
                 let l1 := opa a c e in
                   match opb b d f with
                     | (b',d') :: nil =>
                       map (fun ab:(A+⊥ * A+⊥) => let (a',c') := ab in
                             (ρ a' b', ρ c' d')) l1
                     | _ => (NotBot x, NotBot y) :: nil
                   end
             end.

Definition red_prod_backop_un {A B} ρ (opa: A → A → A+⊥) (opb: B → B → B+⊥)
  : (A*B) → (A*B) → (A*B)+⊥ :=
  fun x y => match x,y with
               | (a,b), (c,d) =>
                 let a' := opa a c in
                 let b' := opb b d in
                 (ρ a' b')
             end.

Definition pair_of_prod {A B} (x: (A*B)+⊥) : A+⊥ * B+⊥ :=
  match x with
    | NotBot (a,b) => (NotBot a, NotBot b)
    | Bot => (Bot, Bot)
  end.

Instance reduced_product_num_dom A B `{Da:num_dom A} `{Db:num_dom B}
         (Ρ: reduction A B)
  : num_dom (A*B) :=
{| as_adom := WProd.make _ _
 ; meet x := botbind (fun y => ρ (meet (fst x) (NotBot (fst y))) (meet (snd x) (NotBot (snd y))))
 ; const n := (const n, const n)
 ; booleans := (booleans, booleans)
 ; range x s := Interval.meet' (range (fst x) s) (range (snd x) s)
 ; neg := red_prod_unop ρ neg neg
 ; not := red_prod_unop ρ not not
 ; notbool := red_prod_unop ρ notbool notbool
 ; boolval := red_prod_unop ρ boolval boolval
 ; add := red_prod_binop ρ add add
 ; sub := red_prod_binop ρ sub sub
 ; mul := red_prod_binop ρ mul mul
 ; divs := red_prod_binop ρ divs divs
 ; shl := red_prod_binop ρ shl shl
 ; and := red_prod_binop ρ and and
 ; or := red_prod_binop ρ or or
 ; xor := red_prod_binop ρ xor xor
 ; is_in_itv m M x := let '(a,b) := x in is_in_itv m M a || is_in_itv m M b

 ; backward_boolval := red_prod_backop_un ρ backward_boolval backward_boolval
 ; backward_notbool := red_prod_backop_un ρ backward_notbool backward_notbool
 ; backward_neg := red_prod_backop_un ρ backward_neg backward_neg
 ; backward_not := red_prod_backop_un ρ backward_not backward_not

 ; backward_add := red_prod_backop_bin ρ backward_add backward_add
 ; backward_sub := red_prod_backop_bin ρ backward_sub backward_sub
 ; backward_cmp := (fun c => red_prod_backop_bin ρ (backward_cmp c) (backward_cmp c))
 ; backward_cmpu := (fun c => red_prod_backop_bin ρ (backward_cmpu c) (backward_cmpu c))
 ; backward_and := red_prod_backop_bin_list ρ backward_and backward_and
 ; backward_or := red_prod_backop_bin_list ρ backward_or backward_or
|}.

Instance reduced_product_num_dom_correct A B `{Da:num_dom A} `{Db:num_dom B}
         (Das: num_dom_correct Da) (Dbs: num_dom_correct Db)
         (Ρ: reduction A B) (Ρs: reduction_correct (@as_adom _ Da) (@as_adom _ Db))
  : num_dom_correct (reduced_product_num_dom A B Ρ).