Module TypesDomain

Require Import Coqlib Utf8.
Require Import Globalenvs.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import AST.
Require Import ToString.
Require Import Util.
Require Import AdomLib.
Require Import Cminor.
Require Import PExpr.

Module AbTy.


  Definition t := PExpr.typ.

  Instance ty_leb : leb_op t := fun x y =>
    match x, y with
      | VI, VI
      | VP, VP
      | VIP, VIP
      | VL, VL
      | VF, VF
      | VS, VS
      | (VI | VP), VIP => true
      | _, _ => false
    end.

  Instance ty_join : join_op t (t+⊤) := fun x y =>
    match x, y with
      | VI, VI => Just VI
      | VP, VP => Just VP
      | (VIP|VP), (VIP|VI)
      | (VIP|VI), VP | VI, VIP => Just VIP
      | VL, VL => Just VL
      | VF, VF => Just VF
      | VS, VS => Just VS
      | _, _ => All
    end.

  Definition ty_widen := ty_join.

  Instance ty_leb_correct : leb_op_correct t val.

  Instance ty_join_correct : join_op_correct t (t+⊤) val.

  Definition eval_constant (cst: constant) : t :=
    match cst with
      | Ointconst n => VI
      | Ofloatconst n => VF
      | Osingleconst n => VS
      | Olongconst n => VL
      | Oaddrsymbol s ofs => VP
    end.

  Definition eval_unop (op: unary_operation) (arg: t) : t :=
    match op with
      | Ocast8unsigned | Ocast8signed | Ocast16unsigned | Ocast16signed
      | Onegint | Onotint | Ointoffloat | Ointuoffloat | Ointofsingle
      | Ointuofsingle | Ointoflong => VI
      | Onegf | Oabsf | Ofloatofsingle | Ofloatofint | Ofloatofintu
      | Ofloatoflong | Ofloatoflongu => VF
      | Onegl | Onotl | Olongofint | Olongofintu | Olongoffloat
      | Olonguoffloat | Olongofsingle | Olonguofsingle => VL
      | Onegfs | Oabsfs | Osingleoffloat | Osingleofint | Osingleofintu
      | Osingleoflong | Osingleoflongu => VS
  end.

  Definition eval_binop (op: binary_operation) (arg1 arg2: t): t :=
    match op with
    | Oadd =>
      match arg1, arg2 with
      | VP, VI
      | VI, VP => VP
      | VI, VI => VI
      | _, _ => VIP
      end
    | Osub =>
      match arg1, arg2 with
      | VP, VI => VP
      | VP, VP
      | VI, VI => VI
      | _, _ => VIP
      end
    | Omul | Odiv | Odivu | Omod | Omodu | Oand | Oor | Oxor | Oshl
    | Oshr | Oshru | Ocmp _ | Ocmpu _ | Ocmpf _ | Ocmpfs _ | Ocmpl _ | Ocmplu _ => VI
    | Oaddf | Osubf | Omulf | Odivf => VF
    | Oaddfs | Osubfs | Omulfs | Odivfs => VS
    | Oaddl | Osubl | Omull | Odivl | Odivlu | Omodl | Omodlu | Oandl
    | Oorl | Oxorl | Oshll | Oshrl | Oshrlu => VL
    end.

  Lemma eval_constant_correct F V : forall (ge: Genv.t F V) c v,
    pexpr_eval_constant ge c = v ->
    v ≠ Vundef →
    γ (eval_constant c) v.

  Lemma eval_unop_correct : forall op arg x v,
    Cminor.eval_unop op arg = Some v ->
    v ≠ Vundef →
    γ x arg ->
    γ (eval_unop op x) v.

  Lemma gamma_Vint_inv {x : t} {i} : γ x (Vint i) →
    x = VI ∨ x = VIP.

  Lemma gamma_VI_inv {v} :
    γ VI v → ∃ i, v = Vint i.

  Lemma gamma_Vptr_inv {x : t} {b i} : γ x (Vptr b i) →
    x = VP ∨ x = VIP.

  Lemma gamma_VP_inv {v} :
    γ VP v → ∃ b i, v = Vptr b i.

  Lemma gamma_VIP_inv {v} :
    γ VIP v → (∃ b i, v = Vptr b i) ∨ (∃ i, v = Vint i).

  Lemma gamma_Vfloat_inv {x : t} {f} : γ x (Vfloat f) → x = VF.

  Lemma gamma_Vsingle_inv {x : t} {f} : γ x (Vsingle f) → x = VS.

  Lemma gamma_VF_inv {v} :
    v ∈ γ VF → ∃ f, v = Vfloat f.

  Lemma gamma_VS_inv {v} :
    v ∈ γ VS → ∃ f, v = Vsingle f.

  Lemma gamma_Vlong_inv {x : t} {l} : γ x (Vlong l) → x = VL.

  Lemma gamma_VL_inv {v} :
    v ∈ γ VL → ∃ l, v = Vlong l.

  Lemma gamma_Vundef_inv {x: t} : γ x Vundef → False.

  Ltac gamma_inv :=
    repeat
      match goal with
      | H : gamma_typ ?a ?b |- _ => change (γ a b) in H
      | H : γ _ (Vint _) |- _ => apply gamma_Vint_inv in H
      | H : γ VI _ |- _ => apply gamma_VI_inv in H
      | H : γ _ (Vptr _ _) |- _ => apply gamma_Vptr_inv in H
      | H : γ VP _ |- _ => apply gamma_VP_inv in H
      | H : γ VIP _ |- _ => apply gamma_VIP_inv in H
      | H : γ _ (Vfloat _) |- _ => apply gamma_Vfloat_inv in H
      | H : γ VF _ |- _ => apply gamma_VF_inv in H
      | H : γ _ (Vsingle _) |- _ => apply gamma_Vsingle_inv in H
      | H : γ VS _ |- _ => apply gamma_VS_inv in H
      | H : γ _ (Vlong _) |- _ => apply gamma_Vlong_inv in H
      | H : γ VL _ |- _ => apply gamma_VL_inv in H
      | H : γ _ Vundef |- _ => apply gamma_Vundef_inv in H
      end.

  Lemma if_opt {A: Type} (b: bool) (a a': A) :
    (if b then Some a else None) = Some a' →
    a = a' ∧ b = true.

  Lemma eval_binop_correct : forall op arg1 arg2 x1 x2 m v,
    Cminor.eval_binop op arg1 arg2 m = Some v ->
    v ≠ Vundef →
    γ x1 arg1 ->
    γ x2 arg2 ->
    γ (eval_binop op x1 x2) v.

End AbTy.