Module IdealIntervalsNonrel

Require Import Utf8.
Require Import IdealExpr.
Require Import AbIdealNonrel.
Require Import ZArith.
Require Import Coqlib.
Require Import ZIntervals FloatIntervals FloatIntervalsBackward.
Require Import FloatIntervalsForward IdealIntervals.
Require Import ZCongruences_defs.
Require Import Integers.
Require Import AdomLib.
Require Import AbIdealEnv IdealBoxDomain ShareTree Util FastArith.

Existing Instance FloatIntervals.gamma.

Definition forward_binop (op:i_binary_operation) (x y:iitv+⊤) : iitv+⊤+⊥ :=
  do x <-
    match op return match op with IOadd => _ | _ => _ end+⊥ with
    | IOadd | IOsub | IOmul | IOdiv | IOmod | IOand | IOor
    | IOxor | IOshl | IOshr | IOcmp _ => in_z x
    | IOaddf | IOsubf | IOmulf | IOdivf | IOcmpf _ => in_f x
    end;
  do y <-
    match op return match op with IOadd => _ | _ => _ end+⊥ with
    | IOadd | IOsub | IOmul | IOdiv | IOmod | IOand | IOor
    | IOxor | IOshl | IOshr | IOcmp _ => in_z y
    | IOaddf | IOsubf | IOmulf | IOdivf | IOcmpf _ => in_f y
    end;
  (match op return match op with IOadd => _ | _ => _ end ->
                  match op with IOadd => _ | _ => _ end -> _ with
  | IOadd => fun x y =>
    match x, y with
    | Just (ZITV mx Mx), Just (ZITV my My) =>
      ret (Just (Az (ZITV (Zfastadd mx my) (Zfastadd Mx My))))
    | _, _ => ret All
    end
  | IOsub => fun x y =>
    match x, y with
    | Just (ZITV mx Mx), Just (ZITV my My) =>
      ret (Just (Az (ZITV (Zfastsub mx My) (Zfastsub Mx my))))
    | _, _ => ret All
    end
  | IOmul => fun x y => fmap (fmap Az) (forward_mult x y)
  | IOdiv => fun x y => fmap (fmap Az) (forward_div x y)
  | IOmod => fun x y => fmap (fmap Az) (forward_mod x y)

  | IOand => fun x y => fmap (fmap Az) (forward_land x y)
  | IOor => fun x y => fmap (fmap Az) (forward_lor x y)
  | IOxor => fun x y => fmap (fmap Az) (forward_lxor x y)
  | IOshl => fun x y => fmap (fmap Az) (forward_shl x y)
  | IOshr => fun x y => fmap (fmap Az) (forward_shr x y)

  | IOcmp c => fun x y =>
    let hasOne := is_bot (backward_cmp_l c x y) in
    let hasZero := is_bot (backward_cmp_l (negate_comparison c) x y) in
    match hasOne, hasZero with
    | false, false => NotBot (Just (Az (ZITV F0 F1)))
    | true, false => NotBot (Just (Az (ZITV F0 F0)))
    | false, true => NotBot (Just (Az (ZITV F1 F1)))
    | true, true => Bot
    end
  | IOcmpf c => fun x y =>
    let hasOne := is_bot (backward_cmpf_l c x y true ⊓ NotBot x) in
    let hasZero := is_bot (backward_cmpf_l c x y false ⊓ NotBot x) in
    match hasOne, hasZero with
      | false, false => NotBot (Just (Az (ZITV F0 F1)))
      | true, false => NotBot (Just (Az (ZITV F0 F0)))
      | false, true => NotBot (Just (Az (ZITV F1 F1)))
      | true, true => Bot
    end

  | IOaddf => fun x y => fmap (fmap Af) (forward_fadd x y)
  | IOsubf => fun x y => fmap (fmap Af) (forward_fsub x y)
  | IOmulf => fun x y => fmap (fmap Af) (forward_fmult x y)
  | IOdivf => fun x y => fmap (fmap Af) (forward_fdiv x y)
  end x y:iitv+⊤+⊥).

Lemma forward_binop_correct:
  ∀ op,
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y y_ab, y ∈ γ y_ab ->
  eval_ibinop op x y ⊆ γ (forward_binop op x_ab y_ab).

Definition forward_unop (op:i_unary_operation) (x:iitv+⊤) : iitv+⊤+⊥ :=
  do x <-
    match op return match op with IOneg => _ | _ => _ end+⊥ with
    | IOneg | IOnot | IOfloatofz | IOsingleofz => in_z x
    | IOnegf | IOabsf | IOsingleoffloat | IOzoffloat => in_f x
    end;
  ret (match op return match op with IOneg => _ | _ => _ end -> _ with
          | IOneg => fun x => fmap Az (forward_neg x)
          | IOnot => fun x => fmap Az (forward_lnot x)
          | IOnegf => fun x => fmap Af (forward_fneg x)
          | IOabsf => fun x => fmap Af (forward_fabs x)
          | IOsingleoffloat => fun x => fmap Af (forward_singleoffloat x)
          | IOfloatofz => fun x => fmap Af (forward_floatofz x)
          | IOsingleofz => fun x => fmap Af (forward_singleofz x)
          | IOzoffloat => fun x => fmap Az (forward_zoffloat x)
          end x).

Lemma forward_unop_correct:
  ∀ op,
  ∀ x x_ab, x ∈ γ x_ab ->
  eval_iunop op x ⊆ γ (forward_unop op x_ab).

Definition backward_binop (op:i_binary_operation) (res x y:iitv+⊤) : (iitv+⊤*iitv+⊤)+⊥ :=
  do x <-
    match op return match op with IOadd => _ | _ => _ end+⊥ with
    | IOadd | IOsub | IOmul | IOdiv | IOmod | IOand | IOor
    | IOxor | IOshl | IOshr | IOcmp _ => in_z x
    | IOaddf | IOsubf | IOmulf | IOdivf | IOcmpf _ => in_f x
    end;
  do y <-
    match op return match op with IOadd => _ | _ => _ end+⊥ with
    | IOadd | IOsub | IOmul | IOdiv | IOmod | IOand | IOor
    | IOxor | IOshl | IOshr | IOcmp _ => in_z y
    | IOaddf | IOsubf | IOmulf | IOdivf | IOcmpf _ => in_f y
    end;
  do res <-
    match op return match op with IOadd => _ | _ => _ end+⊥ with
    | IOadd | IOsub | IOmul | IOdiv | IOmod | IOand | IOor
    | IOxor | IOshl | IOshr | IOcmp _ | IOcmpf _ => in_z res
    | IOaddf | IOsubf | IOmulf | IOdivf => in_f res
    end;
  match op return match op with IOadd => _ | _ => _ end ->
                  match op with IOadd => _ | _ => _ end ->
                  match op with IOadd => _ | _ => _ end -> _ with
  | IOadd => fun x y res =>
    let x' :=
      match y, res with
        | Just (ZITV my My), Just (ZITV mres Mres) =>
          Just (ZITV (Zfastsub mres My) (Zfastsub Mres my))
        | _, _ => All
      end
    in
    let y' :=
      match x, res with
        | Just (ZITV mx Mx), Just (ZITV mres Mres) =>
          Just (ZITV (Zfastsub mres Mx) (Zfastsub Mres mx))
        | _, _ => All
      end
    in
    ret (fmap Az x', fmap Az y')
  | IOsub => fun x y res =>
    let x' :=
      match y, res with
        | Just (ZITV my My), Just (ZITV mres Mres) =>
          Just (ZITV (Zfastadd mres my) (Zfastadd Mres My))
        | _, _ => All
      end
    in
    let y' :=
      match x, res with
        | Just (ZITV mx Mx), Just (ZITV mres Mres) =>
          Just (ZITV (Zfastsub mx Mres) (Zfastsub Mx mres))
        | _, _ => All
      end
    in
    ret (fmap Az x', fmap Az y')
  | IOmul => fun x y res =>
    do x' <- backward_mul_l res x y;
    do y' <- backward_mul_l res y x;
    ret (fmap Az x', fmap Az y')
  | IOcmp c => fun x y res =>
    match res with
    | Just (ZITV m M) =>
      match (Zfastleb m F1 && Zfastleb F1 M)%bool,
            (Zfastleb m F0 && Zfastleb F0 M)%bool with
      | true, true => NotBot (fmap Az x, fmap Az y)
      | true, false =>
        do x' <- backward_cmp_l c x y;
        do y' <- backward_cmp_l (swap_comparison c) y x;
        ret (fmap Az x', fmap Az y')
      | false, true =>
        do x' <- backward_cmp_l (negate_comparison c) x y;
        do y' <- backward_cmp_l (swap_comparison (negate_comparison c)) y x;
        ret (fmap Az x', fmap Az y')
      | false, false => Bot
      end
    | All =>
      ret (fmap Az x, fmap Az y)
    end
  | IOor => fun x y res =>
    do (x', y') <- backward_or res x y;
    ret (fmap Az x', fmap Az y')
  | IOdiv | IOmod | IOand | IOxor | IOshl | IOshr => fun _ _ _ =>
    ret (All, All)
  | IOaddf => fun x y res =>
    do x' <- backward_addf_l res y;
    do y' <- backward_addf_r res x;
    ret (fmap Af x', fmap Af y')
  | IOsubf => fun x y res =>
    do x' <- backward_subf_l res y;
    do y' <- backward_subf_r res x;
    ret (fmap Af x', fmap Af y')
  | IOmulf | IOdivf => fun _ _ _ =>
    ret (All, All)
  | IOcmpf c => fun x y res =>
    match res with
    | Just (ZITV m M) =>
      match (Zfastleb m F1 && Zfastleb F1 M)%bool,
            (Zfastleb m F0 && Zfastleb F0 M)%bool with
      | true, true => ret (fmap Af x, fmap Af y)
      | true, false =>
        do x' <- backward_cmpf_l c x y true;
        do y' <- backward_cmpf_l (swap_comparison c) y x true;
        ret (fmap Af x', fmap Af y')
      | false, true =>
        do x' <- backward_cmpf_l c x y false;
        do y' <- backward_cmpf_l (swap_comparison c) y x false;
        ret (fmap Af x', fmap Af y')
      | false, false => Bot
      end
    | All =>
      ret (fmap Af x, fmap Af y)
    end
  end x y res.

Lemma backward_binop_correct:
  ∀ op x x_ab, x ∈ γ x_ab ->
  ∀ y y_ab, y ∈ γ y_ab ->
  ∀ res res_ab, res ∈ γ res_ab ->
    eval_ibinop op x y res ->
    (x, y) ∈ γ (backward_binop op res_ab x_ab y_ab).

Definition backward_unop (op:i_unary_operation) (res x:iitv+⊤) : iitv+⊤+⊥ :=
  do res <-
    match op return match op with IOneg => _ | _ => _ end+⊥ with
    | IOneg | IOnot | IOzoffloat => in_z res
    | IOnegf | IOabsf | IOsingleoffloat | IOfloatofz | IOsingleofz => in_f res
    end;
  match op return match op with IOneg => _ | _ => _ end -> _ with
  | IOneg => fun res =>
    NotBot (fmap Az (forward_neg res))
  | IOnot => fun res =>
    NotBot (fmap Az (forward_lnot res))
  | IOnegf => fun res =>
    NotBot (fmap Af (forward_fneg res))
  | IOabsf => fun res =>
    fmap (fmap Af) (backward_absf res)
  | IOsingleoffloat => fun res =>
    fmap (fmap Af) (backward_singleoffloat res)
  | IOzoffloat => fun res =>
    NotBot (fmap Af (backward_zoffloat res))
  | IOfloatofz => fun res =>
    do x <- in_z x;
    fmap (fmap Az) (backward_floatofz res x)
  | IOsingleofz => fun res =>
    do x <- in_z x;
    fmap (fmap Az) (backward_singleofz res x)
  end res.

Lemma backward_unop_correct:
  ∀ op,
    ∀ x x_ab, x ∈ γ x_ab ->
    ∀ res res_ab, res ∈ γ res_ab ->
      eval_iunop op x res ->
      x ∈ γ (backward_unop op res_ab x_ab).

Definition extract_msgs (x:var) v : messages_chan :=
  match singleton v with
  | Some v => Broadcasted_msg (Known_value_msg x v)::nil
  | None => Itv_msg x v::nil
  end.

Lemma extract_msgs_correct:
  ∀ x v ρ,
    γ v (ρ x) → γ (extract_msgs x v) ρ.

Definition enrich_query_chan fev (chan:query_chan) : query_chan :=
  {| get_var_ty := chan.(get_var_ty);
     get_itv expr :=
       do ab <- fev expr;
       do ab' <- chan.(get_itv) expr;
       match ab with
       | All => NotBot ab'
       | Just (Az i1) => do i2 <- in_z ab'; fmap (fmap Az) (Just i1 ⊓ i2)
       | Just (Af i1) => do i2 <- in_f ab'; fmap (fmap Af) (Just i1 ⊓ i2)
       end;
     get_congr := chan.(get_congr);
     get_eq_expr := chan.(get_eq_expr);
     linearize_expr := chan.(linearize_expr) |}.

Definition reduce_itv_congr (zc:zcongr) (itv:zitv) : zitv+⊥ :=
  let 'ZITV a b := itv in
  let m := zc.(zc_mod) in
  if Nfastleb m F0 then
    let x := zc.(zc_rem) in meet itv (ZITV x x)
  else if Nfastleb m F1 then NotBot itv
  else
    let b := Zfastsub b (Zfastmod (Zfastsub b zc.(zc_rem)) (Zfast_of_Nfast m)) in
    let a := Zfastadd a (Zfastmod (Zfastsub zc.(zc_rem) a) (Zfast_of_Nfast m)) in
    if Zfastleb a b then NotBot (ZITV a b)
    else Bot.

Lemma reduce_itv_congr_correct:
  ∀ zc itv v,
    v ∈ γ zc -> v ∈ γ itv ->
    v ∈ γ (reduce_itv_congr zc itv).

Definition process_msg fev {AB} bev (msg:message) (abenv:AB*query_chan)
           : (AB*messages_chan)+⊥ :=
  match msg with
  | Congr_msg x zc =>
    do ab <- fev (IEvar INTz x);
    match ab with
    | Just (Az itv0) =>
      do itv <- reduce_itv_congr zc itv0;
      let 'ZITV a b := itv in
      let msgs :=
        if Zfastleb b a then Broadcasted_msg (Known_value_msg x (INz a))::nil
        else if itv0 ⊑ itv then msg::nil
             else msg::Itv_msg x (Az itv)::nil
      in
      do abenv <- bev (IEvar INTz x) (Az itv) abenv;
      NotBot (abenv, msgs)
    | _ => NotBot (fst abenv, msg::nil)
    end
  | Itv_msg x itv =>
    let ty := match itv with Az _ => INTz | Af _ => INTf end in
    do abenv <- bev (IEvar ty x) itv abenv;
    NotBot (abenv, msg::nil)
  | _ => NotBot (fst abenv, msg::nil)
  end.

Lemma process_msg_correct :
  ∀ fev AB (GAB:gamma_op AB (var -> ideal_num)) bev (msg:message) (abenv:AB * query_chan) ρ,

    (∀ e v, eval_iexpr ρ e v -> v ∈ γ (fev e)) ->
    (∀ e v abv ab, eval_iexpr ρ e v -> v ∈ γ abv -> ρ ∈ γ ab -> ρ ∈ γ (bev e abv ab)) ->

    γ msg ρ → γ abenv ρ → γ (process_msg fev bev msg abenv) ρ.

Instance itv_dom : ab_ideal_nonrel iitv :=
  { widen := iditv_widen
  ; const n :=
      match n with
      | INz z => let z:Zfast := z in Just (Az (ZITV z z))
      | INf f => if Fappli_IEEE.is_nan f then All else Just (Af (FITV f f))
      end
  ; z_itv := @Just _ ∘ Az
  ; forward_unop := forward_unop
  ; forward_binop := forward_binop
  ; backward_unop := backward_unop
  ; backward_binop := backward_binop

  ; forward_var fev x ab c := NotBot ab
  ; backward_var fev AB bev var_ref x ab abenv :=
      match ab with
      | Az itv =>
        do zc <- (snd abenv).(get_congr) (IEvar INTz x);
        do itv' <- reduce_itv_congr zc itv;
        do ab <- var_ref (Az itv') (fst abenv);
        match (snd abenv).(get_eq_expr) x with
        | Some (Leaf e) => bev e (Az itv') (ab, snd abenv)
        | _ => NotBot ab
        end
      | _ => var_ref ab (fst abenv)
      end
  ; enrich_query_chan := enrich_query_chan
  ; process_msg := process_msg
  ; assign_msgs := extract_msgs
  ; assume_msgs x v_old v := extract_msgs x v
}.

Instance itv_dom_correct : ab_ideal_nonrel_correct itv_dom _ := {}.

Definition t := @IdealBoxDomain.t iitv.

Instance intervals_ideal_env : ab_ideal_env t (t+⊥) :=
  IdealBoxDomain.ideal_box_domain _ itv_dom_correct.