Require Import Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RationalConstruction Daisy.Infra.RealRationalProps.
Require Import Daisy.Expressions Daisy.IntervalArithQ.

Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
  let (intv, _) := absenv e in
    match e with
    | Var v =>
      let bounds_v := P v in
      andb (Qeq_bool (fst intv) (fst (bounds_v))) (Qeq_bool (snd bounds_v) (snd (intv)))
    | Param v =>
      let bounds_v := P v in
      andb (Qeq_bool (fst intv) (fst (bounds_v))) (Qeq_bool (snd bounds_v) (snd (intv)))
    | Const n =>
      andb (Qleb (fst intv) n) (Qleb n (snd intv))
    | Binop b e1 e2 =>
      let rec := andb (validIntervalbounds e1 absenv P) (validIntervalbounds e2 absenv P) in
      let (iv1,_) := absenv e1 in
      let (iv2,_) := absenv e2 in
      let opres :=
          match b with
          | Plus =>
            let new_iv := addIntv iv1 iv2 in
            isSupersetIntv new_iv intv
          | Sub =>
            let new_iv := subtractIntv iv1 iv2 in
            isSupersetIntv new_iv intv
          | Mult =>
            let new_iv := multIntv iv1 iv2 in
            isSupersetIntv new_iv intv
          | Div => false
          end
      in
      andb rec opres
    end.

(*
Lemma validIntervalbounds_correct (e:exp Q):
  forall (absenv:analysisResult) (P:precond) cenv vR,
  validIntervalbounds e absenv P = true ->
  eval_exp 0%R cenv (toRExp e) vR ->
  contained vR (Q2R (fst (fst(absenv e))), Q2R (snd (fst (absenv e)))).
Proof.
  induction e.
  - intros absenv P cenv vR valid_bounds eval_e.
    unfold validIntervalbounds in valid_bounds.
    destruct (absenv (Var Q n)) as [intv err].
    simpl.
    (* needs that Precond approximates value *)
    admit.
  - intros absenv P cenv vR valid_bounds eval_e.
    unfold validIntervalbounds in valid_bounds.
    destruct (absenv (Param Q n)) as [intv err].
    (* same *)
    admit.
  - intros absenv P cenv vR valid_bounds eval_e.
    unfold validIntervalbounds in valid_bounds.
    destruct (absenv (Const v)) as [intv err].
    simpl.
    apply Is_true_eq_left in valid_bounds.
    apply andb_prop_elim in valid_bounds.
    destruct valid_bounds.
    unfold contained; simpl.
    split.
    + apply Is_true_eq_true in H.
      unfold Qleb in *.
      apply Qle_bool_iff in H.
      admit.
    + admit.
  - destruct b.
    + admit.
    + admit.
    + admit.
    + intros absenv P cenv vR valid_bounds eval_e.
      simpl in valid_bounds.
      destruct (absenv (Binop Div e1 e2));
        destruct (absenv e1);
        destruct (absenv e2).
      apply Is_true_eq_left in valid_bounds.
      apply andb_prop_elim in valid_bounds.
      destruct valid_bounds.
      unfold Is_true in *; simpl in *. contradiction.
Admitted.
 *)

Definition u:nat := 1.
(** 1655/5 = 331; 0,4 = 2/5 **)
Definition cst1:Q := 1657 # 5.

(** Define abbreviations **)
Definition varU:exp Q := Param Q u.
Definition valCst:exp Q := Const cst1.
Definition valCstAddVarU:exp Q := Binop Plus valCst varU.

(** Error values **)
Definition errCst1 :Q := rationalFromNum (36792791036077685#1) 16 14.
Definition errVaru := rationalFromNum (11102230246251565#1) 16 14.
Definition lowerBoundAddUCst:Q := 1157 # 5.
Definition upperBoundAddUCst:Q := 2157 # 5.
Definition errAddUCst := rationalFromNum (9579004256465851#1) 15 14.

(** The added assertion becomes the precondition for us **)
Definition precondition := fun n:nat => (- (100#1),100#1).
Definition absenv := fun e:exp Q => match e with
                                 |Const n => (cst1,cst1,0)
                                 |Binop b e1 e2 => (lowerBoundAddUCst,upperBoundAddUCst,0)
                                 | Param v => (-(100#1),100#1,0)
                                 | _ => (0,0,0)
                                 end.

Eval compute in isSupersetIntv (lowerBoundAddUCst,upperBoundAddUCst) (lowerBoundAddUCst,upperBoundAddUCst).
Eval compute in addIntv (cst1,cst1) (-(100#1),100#1).

Eval compute in validIntervalbounds valCst (fun _ => (cst1,cst1,0)) (fun _ => (cst1,cst1)).
Eval compute in validIntervalbounds varU (fun _ => (- (100#1),100#1,0)) precondition.