Module IdealIntervals

Require Import Utf8 Util FastArith.
Require Import ShareTree.
Require Import ZArith.
Require Import Coqlib ToString.
Require Import ZIntervals FloatIntervals.
Require Import AdomLib.
Require Import IdealExpr.

Inductive iitv :=
| Az : zitv -> iitv
| Af : fitv -> iitv.

Instance iditv_leb : leb_op iitv := fun x y =>
  match x, y return _ with
  | Az x, Az y => x ⊑ y
  | Af x, Af y => x ⊑ y
  | Af _, Az _ | Az _, Af _ => false
  end.

Program Instance iditv_join : join_op iitv (iitv+⊤) := fun x y =>
  match x, y with
  | Az x', Az y' =>
    let res := x' ⊔ y' in
    Just (ifeq x' == res then x else
            ifeq y' == res then y else Az res)
  | Af x', Af y' =>
    let res := x' ⊔ y' in
    Just (ifeq x' == res then x else
            ifeq y' == res then y else Af res)
  | Af _, Az _ | Az _, Af _ => All
  end.

Instance iditv_meet : meet_op iitv (iitv+⊥) := fun x y =>
  match x, y with
  | Az x, Az y => fmap Az (x ⊓ y)
  | Af x, Af y => fmap Af (x ⊓ y)
  | Af _, Az _ | Az _, Af _ => Bot
  end.

Program Definition iditv_widen x y :=
  match x, y with
  | Az x', Az y' =>
    do res <- widen_zitv x' y';
    ret (ifeq x' == res then x else
           ifeq y' == res then y else Az res)
  | Af x', Af y' =>
    let res := fitv_widen x' y' in
    ret (ifeq x' == res then x else
           ifeq y' == res then y else Af res)
  | Af _, Az _ | Az _, Af _ => All
  end.

Instance itv_num_gamma : gamma_op iitv ideal_num := fun v x =>
  match v, x with
  | Az v, INz x => (x:Z) ∈ γ v
  | Af v, INf x => x ∈ γ v
  | _, _ => False
  end.

Instance iditv_leb_correct : leb_op_correct iitv ideal_num.

Instance iditv_join_correct : join_op_correct iitv (iitv+⊤) ideal_num.

Instance iditv_meet_correct : meet_op_correct iitv (iitv+⊥) ideal_num.

Lemma widen_incr:
  ∀ ab1 ab2, γ ab1 ⊆ γ (iditv_widen ab1 ab2).

Definition in_z v : zitv+⊤+⊥ :=
  match v with
  | Just (Az v) => NotBot (Just v)
  | Just (Af v) => Bot
  | All => NotBot All
  end.

Lemma in_z_correct:
  ∀ ab x, INz x ∈ γ ab -> (x:Z) ∈ γ (in_z ab).

Hint Resolve in_z_correct.

Definition in_f v : fitv+⊤+⊥ :=
  match v with
  | Just (Af v) => NotBot (Just v)
  | Just (Az v) => Bot
  | All => NotBot All
  end.

Lemma in_f_correct:
  ∀ ab x, INf x ∈ γ ab -> x ∈ γ (in_f ab).

Hint Resolve in_f_correct.

Definition singleton (itv:iitv) : option ideal_num :=
  match itv with
  | Az (ZITV a b) => if Zfastleb b a then Some (INz a) else None
  | Af (FITV a b) =>
    if FloatLib.Fleb b a then
      match a with
      | Fappli_IEEE.B754_zero _ => None
      | _ => Some (INf a)
      end
    else None
  end.

Lemma singleton_correct:
  ∀ itv x r, x ∈ γ itv -> singleton itv = Some r -> x = r.

Instance IitvToString : ToString iitv := λ i,
  match i with
  | Az j => to_string j
  | Af j => to_string j
  end.