Module IdealExpr

Require Import Utf8 Coqlib ToString DebugCminor Util TreeAl.
Require Import Integers Floats FastArith.
Require Import AdomLib Hash ShareTree.
Require Import ZIntervals Cells.

Inductive var :=
| Real: cell -> var
| Ghost: positive -> var.

Module var_EQ : TYPE_EQ
  with Definition s := var
  with Definition t := (cell + positive)%type.

  Definition s := var.
  Definition t := (cell + positive)%type.

  Definition t_of_s (x:s) : t :=
    match x with
    | Real x => inl x
    | Ghost x => inr x
    end.

  Definition s_of_t (x:t) : s :=
    match x with
    | inl x => Real x
    | inr x => Ghost x
    end.

  Lemma s_of_t_of_s : forall x : s, s_of_t (t_of_s x) = x.

  Lemma t_of_s_of_t: forall x : t, t_of_s (s_of_t x) = x.

  Instance eq : EqDec s.
End var_EQ.

Instance hash_var : hashable var :=
  fun h x =>
    match x with
    | Real x => hash (MIX h F0) x
    | Ghost x => hash (MIX h F1) x
    end.

Instance ToString_var : ToString cell -> ToString var :=
  fun _ x =>
    match x with
    | Real x => to_string x
    | Ghost x => ("$" ++ to_string x ++ "$")%string
    end.

Module STPT := SumShareTree(ACTree)(PShareTree).
Module T := BijShareTree(var_EQ)(STPT).
Instance var_eq : EqDec var := T.elt_eq.

Inductive ideal_num :=
| INf : float -> ideal_num
| INz : Zfast -> ideal_num.

Inductive ideal_num_ty : Type :=
| INTz | INTf.

Inductive ideal_num_ty_gamma : gamma_op ideal_num_ty ideal_num :=
| INTSz : forall i, ideal_num_ty_gamma INTz (INz i)
| INTSf : forall f, ideal_num_ty_gamma INTf (INf f).
Existing Instance ideal_num_ty_gamma.

Inductive i_binary_operation : Type :=
| IOadd | IOsub | IOmul | IOdiv | IOmod
| IOand | IOor | IOxor | IOshl | IOshr
| IOcmp : comparison -> i_binary_operation
| IOaddf | IOsubf | IOmulf | IOdivf
| IOcmpf : comparison -> i_binary_operation.

Inductive i_unary_operation :=
| IOneg | IOnot
| IOnegf | IOabsf
| IOsingleoffloat | IOfloatofz | IOsingleofz | IOzoffloat.

Inductive iexpr : Type :=
| IEvar : ideal_num_ty -> var -> iexpr
| IEconst : ideal_num -> iexpr
| IEZitv : zitv -> iexpr
| IEunop : i_unary_operation -> iexpr -> iexpr
| IEbinop : i_binary_operation -> iexpr -> iexpr -> iexpr.

Inductive ite_iexpr : Type :=
| Leaf : iexpr -> ite_iexpr
| Ite : iexpr -> ite_iexpr -> ite_iexpr -> ite_iexpr.

Section eval_iexpr.
  Variable ρ: var -> ideal_num.

  Inductive eval_ibinop : i_binary_operation -> ideal_num -> ideal_num -> ideal_num -> Prop :=
  | eval_ibinop_IOadd : forall i1 i2:Z,
    eval_ibinop IOadd (INz i1) (INz i2) (INz (i1+i2))
  | eval_ibinop_IOsub : forall i1 i2:Z,
    eval_ibinop IOsub (INz i1) (INz i2) (INz (i1-i2))
  | eval_ibinop_IOmul : forall i1 i2:Z,
    eval_ibinop IOmul (INz i1) (INz i2) (INz (i1*i2))
  | eval_ibinop_IOdiv : forall i1 i2:Z,
    i2 <> 0%Z ->
    eval_ibinop IOdiv (INz i1) (INz i2) (INz (Z.quot i1 i2))
  | eval_ibinop_IOmod : forall i1 i2:Z,
    i2 <> 0%Z ->
    eval_ibinop IOmod (INz i1) (INz i2) (INz (Z.rem i1 i2))
  | eval_ibinop_IOand : forall i1 i2:Z,
    eval_ibinop IOand (INz i1) (INz i2) (INz (Z.land i1 i2))
  | eval_ibinop_IOor : forall i1 i2:Z,
    eval_ibinop IOor (INz i1) (INz i2) (INz (Z.lor i1 i2))
  | eval_ibinop_IOxor : forall i1 i2:Z,
    eval_ibinop IOxor (INz i1) (INz i2) (INz (Z.lxor i1 i2))
  | eval_ibinop_IOshl : forall i1 i2:Z,
    eval_ibinop IOshl (INz i1) (INz i2) (INz (Z.shiftl i1 i2))
  | eval_ibinop_IOshr : forall i1 i2:Z,
    eval_ibinop IOshr (INz i1) (INz i2) (INz (Z.shiftr i1 i2))
  | eval_ibinop_IOcmp : forall c (i1 i2:Z),
    eval_ibinop (IOcmp c) (INz i1) (INz i2)
                (INz (if (ZIntervals.Zcmp c i1 i2) then F1 else F0))
  | eval_ibinop_IOaddf : forall f1 f2,
    eval_ibinop IOaddf (INf f1) (INf f2) (INf (Float.add f1 f2))
  | eval_ibinop_IOsubf : forall f1 f2,
    eval_ibinop IOsubf (INf f1) (INf f2) (INf (Float.sub f1 f2))
  | eval_ibinop_IOmulf : forall f1 f2,
    eval_ibinop IOmulf (INf f1) (INf f2) (INf (Float.mul f1 f2))
  | eval_ibinop_IOdivf : forall f1 f2,
    eval_ibinop IOdivf (INf f1) (INf f2) (INf (Float.div f1 f2))
  | eval_ibinop_IOcmpf : forall c f1 f2,
    eval_ibinop (IOcmpf c) (INf f1) (INf f2)
                (INz (if (Float.cmp c f1 f2) then F1 else F0)).

  Inductive eval_iunop : i_unary_operation -> ideal_num -> ideal_num -> Prop :=
  | eval_iunop_IOneg : forall i:Z,
    eval_iunop IOneg (INz i) (INz (-i))
  | eval_iunop_IOnot : forall i:Z,
    eval_iunop IOnot (INz i) (INz (Z.lnot i))
  | eval_iunop_IOnegf : forall f,
    eval_iunop IOnegf (INf f) (INf (Float.neg f))
  | eval_iunop_IOabsf : forall f,
    eval_iunop IOabsf (INf f) (INf (Float.abs f))
  | eval_iunop_IOzoffloat : forall f (i:Z),
    Fappli_IEEE_extra.ZofB f = Some i ->
    eval_iunop IOzoffloat (INf f) (INz i)
  | eval_iunop_IOfloatofz : forall i:Z,
    eval_iunop IOfloatofz (INz i)
          (INf (Fappli_IEEE_extra.BofZ 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) i))
  | eval_iunop_IOsingleofz : forall i:Z,
    eval_iunop IOsingleofz (INz i)
               (INf (Float.of_single (Fappli_IEEE_extra.BofZ 24 128 (@eq_refl _ Lt) (@eq_refl _ Lt) i)))
  | eval_iunop_IOsingleoffloat : forall f,
    eval_iunop IOsingleoffloat (INf f) (INf (Float.of_single (Float.to_single f))).

  Inductive eval_iexpr: iexpr -> ideal_num -> Prop :=
  | eval_IEvar: forall id i ty,
    ρ id = i ->
    i ∈ γ ty ->
    eval_iexpr (IEvar ty id) i
  | eval_IEconst: forall n,
    eval_iexpr (IEconst n) n
  | eval_IEZitv: forall itv (x:Z),
    x ∈ γ itv ->
    eval_iexpr (IEZitv itv) (INz x)
  | eval_IEunop: forall op a n r,
    eval_iexpr a n ->
    eval_iunop op n r->
    eval_iexpr (IEunop op a) r
  | eval_IEbinop: forall op a1 a2 n1 n2 n,
    eval_iexpr a1 n1 ->
    eval_iexpr a2 n2 ->
    eval_ibinop op n1 n2 n ->
    eval_iexpr (IEbinop op a1 a2) n.

  Inductive eval_ite_iexpr: ite_iexpr -> ideal_num -> Prop :=
  | eval_Leaf : forall e v,
    eval_iexpr e v ->
    eval_ite_iexpr (Leaf e) v
  | eval_Ite_0 : forall c et ef v,
    eval_iexpr c (INz 0) ->
    eval_ite_iexpr ef v ->
    eval_ite_iexpr (Ite c et ef) v
  | eval_Ite_1 : forall c et ef v,
    eval_iexpr c (INz 1) ->
    eval_ite_iexpr et v ->
    eval_ite_iexpr (Ite c et ef) v.

End eval_iexpr.

Definition iexpr_ty e : ideal_num_ty :=
  match e with
  | IEvar ty _ => ty
  | IEconst (INz _) => INTz
  | IEconst (INf _) => INTf
  | IEZitv _ => INTz
  | IEunop (IOneg | IOnot | IOzoffloat) _ => INTz
  | IEunop (IOnegf | IOabsf | IOsingleoffloat | IOfloatofz | IOsingleofz) _ => INTf
  | IEbinop (IOadd | IOsub | IOmul | IOdiv | IOmod | IOand | IOor | IOxor |
             IOshl | IOshr | IOcmp _ | IOcmpf _) _ _ => INTz
  | IEbinop (IOaddf | IOsubf | IOmulf | IOdivf) _ _ => INTf
  end.

Lemma iexpr_ty_correct:
  forall n e ρ, eval_iexpr ρ e n -> γ (iexpr_ty e) n.

Instance iexpr_eq : EqDec var -> EqDec iexpr.

Fixpoint iexpr_sz (e:iexpr) : Z :=
  match e with
  | IEvar _ _ | IEconst _ | IEZitv _ => 1
  | IEunop _ e => iexpr_sz e+1
  | IEbinop _ e1 e2 => iexpr_sz e1+iexpr_sz e2+1
  end.

Fixpoint ite_iexpr_sz (e:ite_iexpr) : Z :=
  match e with
  | Leaf e => iexpr_sz e
  | Ite c e1 e2 => iexpr_sz c+ite_iexpr_sz e1+ite_iexpr_sz e2+1
  end.

Fixpoint iexpr_det (e:iexpr) :=
  match e with
  | IEvar _ _ | IEconst _ => true
  | IEZitv _ => false
  | IEunop _ e => iexpr_det e
  | IEbinop _ e1 e2 => iexpr_det e1 && iexpr_det e2
  end.

Lemma iexpr_det_ok:
  forall ρ e n, eval_iexpr ρ e n ->
    forall m, eval_iexpr ρ e m ->
    iexpr_det e = true ->
    n = m.

Local Open Scope N.

Instance hash_iexpr : hashable iexpr :=
  fix hash_iexpr (h:Nfast) (e:iexpr) :=
  match e with
  | IEvar _ x => hash (MIX h F1) x
  | IEconst (INz a) => hash (MIX h F2) a
  | IEconst (INf x) => hash (MIX h F3) (Fappli_IEEE_bits.bits_of_b64 x:Zfast)
  | IEunop op e =>
    let key :=
      match op with
      | IOneg => F4 | IOnot => F5 | IOnegf => F6
      | IOabsf => F7 | IOsingleoffloat => F8 | IOfloatofz => F9
      | IOsingleofz => F10 | IOzoffloat => F11
      end%N in
    hash_iexpr (MIX h key) e
  | IEbinop op e1 e2 =>
    let key :=
      match op with
      | IOadd => F12 | IOsub => F13 | IOmul => F14
      | IOdiv => F15 | IOmod => F16 | IOand => F17
      | IOor => F18 | IOxor => F19 | IOshl => F20
      | IOshr => F21 | IOcmp Ceq => F22 | IOcmp Cne => F23
      | IOcmp Clt => F24 | IOcmp Cle => F25 | IOcmp Cgt => F26
      | IOcmp Cge => F27 | IOaddf => F28 | IOsubf => F29
      | IOmulf => F30 | IOdivf => F31 | IOcmpf Ceq => F32
      | IOcmpf Cne => F33 | IOcmpf Clt => F34 | IOcmpf Cle => F35
      | IOcmpf Cgt => F36 | IOcmpf Cge => F37
      end%N in
    hash_iexpr (hash_iexpr (MIX h key) e1) e2
  | IEZitv (ZITV a b) => hash (hash (MIX h F38) a) b
  end.

Instance hash_ite_iexpr : hashable ite_iexpr :=
  fix hash_ite_iexpr (h:Nfast) (e:ite_iexpr) :=
  match e with
  | Leaf e => hash h e
  | Ite e1 e2 e3 =>
    hash_ite_iexpr (hash_ite_iexpr (hash (MIX h F39) e1) e2) e3
  end.

Local Open Scope string.

Definition string_of_ideal_num_ty (ty:ideal_num_ty) : string :=
  match ty with
  | INTz => "%z"
  | INTf => "%f"
  end.

Definition string_of_unop (op:i_unary_operation) :=
  match op with
  | IOneg => "-"
  | IOnot => "~"
  | IOnegf => "-."
  | IOabsf => "absf"
  | IOsingleoffloat => "singleoffloat"
  | IOfloatofz => "floatofz"
  | IOsingleofz => "singleofz"
  | IOzoffloat => "zoffloat"
  end.

Definition string_of_binop (op:i_binary_operation) :=
  match op with
  | IOadd => "+"
  | IOsub => "-"
  | IOmul => "*"
  | IOdiv => "/"
  | IOmod => "%"
  | IOand => "&"
  | IOor => "|"
  | IOxor => "^"
  | IOshl => "<<"
  | IOshr => ">>"
  | IOcmp c => string_of_comparison c
  | IOaddf => "+."
  | IOsubf => "-."
  | IOmulf => "*."
  | IOdivf => "/."
  | IOcmpf c => string_of_comparison c
  end.

Fixpoint string_of_iexpr `{ToString var} (e: iexpr) {struct e} : string :=
  match e with
  | IEvar ty v => to_string v ++ string_of_ideal_num_ty ty
  | IEconst (INz z) => to_string z
  | IEconst (INf x) => to_string x
  | IEZitv itv => to_string itv
  | IEunop op e' => string_of_unop op ++ "(" ++ string_of_iexpr e' ++ ")"
  | IEbinop op x y =>
    "(" ++ string_of_iexpr x ++ ")" ++ string_of_binop op ++
        "(" ++ string_of_iexpr y ++ ")"
  end.

Instance IExprToString : ToString var -> ToString iexpr := @string_of_iexpr.

Fixpoint string_of_iteiexpr `{ToString var} (e: ite_iexpr) {struct e} : string :=
  match e with
  | Leaf e => to_string e
  | Ite c et ef => "(" ++ string_of_iexpr c ++ ") ? (" ++
                       string_of_iteiexpr et ++ ") : (" ++
                       string_of_iteiexpr ef ++ ")"
  end.

Instance IteIExprToString : ToString var -> ToString ite_iexpr := @string_of_iteiexpr.

Hint Constructors eval_ibinop.
Hint Constructors eval_iunop.
Hint Constructors eval_iexpr.
Hint Constructors ideal_num_ty_gamma.