Module PExpr

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

Set Implicit Arguments.
Local Open Scope string_scope.

Inductive constant :=
| Ointconst : int → constant
| Ofloatconst : float → constant
| Osingleconst : float32 → constant
| Olongconst : int64 → constant
| Oaddrsymbol : ident → int → constant. (* address of a global *)

Inductive typ := VI | VP | VIP | VL | VF | VS.

Instance typEqDec : EqDec typ.

Instance gamma_typ : gamma_op typ val :=
  fun ab v =>
    match ab, v with
      | VI, Vint _
      | VP, Vptr _ _
      | VIP, (Vint _ | Vptr _ _)
      | VL, Vlong _
      | VF, Vfloat _
      | VS, Vsingle _ => True
      | _, _ => False
    end.
Arguments gamma_typ !x !y.

Lemma gamma_typ_inv ty v :
  γ ty v →
  match ty with
  | VI => ∃ i, v = Vint i
  | VP => ∃ b i, v = Vptr b i
  | VIP => (∃ i, v = Vint i) ∨ (∃ b i, v = Vptr b i)
  | VL => ∃ i, v = Vlong i
  | VF => ∃ f, v = Vfloat f
  | VS => ∃ s, v = Vsingle s
  end.

Lemma gamma_typ_inv' ty v :
  γ ty v →
  match v with
  | Vundef => False
  | Vint _ => ty = VI ∨ ty = VIP
  | Vlong _ => ty = VL
  | Vfloat _ => ty = VF
  | Vsingle _ => ty = VS
  | Vptr _ _ => ty = VP ∨ ty = VIP
  end.

Instance toString : ToString typ :=
  (λ x, match x with VI => "int" | VP => "ptr" | VIP => "intorptr"
                  | VL => "long" | VF => "float" | VS => "single" end)%string.

Definition type_of_constant (c: constant) (t: typ) : Prop :=
    match c with
    | Ointconst _ => t = VI
    | Ofloatconst _ => t = VF
    | Osingleconst _ => t = VS
    | Olongconst _ => t = VL
    | Oaddrsymbol _ _ => t = VP
  end.

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

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

Inductive pexpr (var:Type) : Type :=
| PEvar : var -> typ -> pexpr var
| PElocal: ident -> pexpr var (* address of a local variable *)
| PEconst (c: constant) (t: typ) `(type_of_constant c t)
| PEunop (u: unary_operation) (pe: pexpr var) (t: typ) `(t = type_of_unop u)
| PEbinop (b: binary_operation) (pe1 pe2: pexpr var) (t: typ) `(type_of_binop b t).

Fixpoint pe_free_var {var} (pe: pexpr var) : ℘(var) :=
  match pe with
  | PEvar v _ => eq v
  | PElocal _
  | PEconst _ _ _ => ∅
  | PEunop _ pe' _ _ => pe_free_var pe'
  | PEbinop _ pe₁ pe₂ _ _ => pe_free_var pe₁ ∪ pe_free_var pe₂
  end.

Instance string_of_constant : ToString constant :=
  λ cst,
  match cst with
  | Ointconst i => to_string i
  | Ofloatconst f => to_string f
  | Osingleconst s => to_string s
  | Olongconst l => to_string l
  | Oaddrsymbol s ofs => to_string (s, ofs)
  end.

Fixpoint string_of_pexpr {A} `{ToString A} (e: pexpr A) {struct e} : string :=
  match e with
  | PEvar v ty => to_string v ++ "@" ++ to_string ty
  | PElocal i => "&" ++ to_string i
  | PEconst c ty _ => to_string c ++ "@" ++ to_string ty
  | PEunop op l ty _ => string_of_unop op ++ string_of_pexpr l ++ "@" ++ to_string ty
  | PEbinop op l r ty _ => "(" ++ string_of_pexpr l ++ string_of_binop op ++ string_of_pexpr r ++ ")" ++ "@" ++ to_string ty
  end.

Instance PExprToString A `{ToString A} : ToString (pexpr A) := string_of_pexpr.

Section EVAL.
  Variable var: Type.
  Variables F V: Type.
  Variable ge: Genv.t F V.
  Variable m: Mem.mem.
  Variable ρ: var → val.
  Variable e: ident → option block.

  Definition pexpr_eval_constant (cst: constant) : val :=
    match cst with
    | Ointconst n => Vint n
    | Ofloatconst n => Vfloat n
    | Osingleconst n => Vsingle n
    | Olongconst n => Vlong n
    | Oaddrsymbol s ofs =>
      match Genv.find_symbol ge s with
      | Some b => Vptr b ofs
      | None => Vundef
      end
    end.

  Inductive eval_pexpr: pexpr var -> val -> Prop :=
  | eval_PEvar: forall c v ty,
    ρ c = v ->
    (v = Vundef \/ v ∈ γ ty) ->
    eval_pexpr (PEvar c ty) v
  | eval_PElocal: forall i b,
    e(i) = Some b ->
    eval_pexpr (PElocal _ i) (Vptr b Int.zero)
  | eval_PEconst_some: forall cst v ty Hty,
    pexpr_eval_constant cst = v ->
    (v = Vundef \/ v ∈ γ ty) ->
    eval_pexpr (PEconst _ cst ty Hty) v
  | eval_PEunop: forall op a1 v1 v ty (Hty: ty = type_of_unop op),
    eval_pexpr a1 v1 ->
    eval_unop op v1 = Some v ->
    (v = Vundef \/ v ∈ γ ty) ->
    eval_pexpr (PEunop op a1 Hty) v
  | eval_PEbinop: forall op a1 a2 v1 v2 v ty (Hty: type_of_binop op ty),
    eval_pexpr a1 v1 ->
    eval_pexpr a2 v2 ->
    eval_binop op v1 v2 m = Some v ->
    (v = Vundef \/ v ∈ γ ty) ->
    eval_pexpr (PEbinop op a1 a2 ty Hty) v.

  Lemma eval_pexpr_var_inv c ty v :
    eval_pexpr (PEvar c ty) v →
    ρ c = v ∧ (v = Vundef ∨ v ∈ γ ty).

  Lemma eval_pexpr_local_inv i v :
    eval_pexpr (PElocal _ i) v →
    ∃ b, e(i) = Some b ∧ v = Vptr b Int.zero.

  Lemma eval_pexpr_const_inv cst ty Hty v :
    eval_pexpr (PEconst _ cst ty Hty) v →
    v = pexpr_eval_constant cst ∧ (v = Vundef ∨ v ∈ γ ty).

  Lemma eval_pexpr_unop_inv op u ty (Hty: ty = type_of_unop op) v :
    eval_pexpr (PEunop op u Hty) v →
    ∃ v', eval_pexpr u v' ∧ eval_unop op v' = Some v ∧ (v = Vundef ∨ v ∈ γ ty).

  Lemma eval_pexpr_unop_ptr op u ty (Hty: ty = type_of_unop op) b i :
    ¬ (eval_pexpr (PEunop op u Hty) (Vptr b i)).

  Lemma eval_pexpr_binop_inv op u₁ u₂ ty (Hty: type_of_binop op ty) v :
    eval_pexpr (PEbinop op u₁ u₂ ty Hty) v →
    ∃ v₁ v₂, eval_pexpr u₁ v₁ ∧ eval_pexpr u₂ v₂ ∧ eval_binop op v₁ v₂ m = Some v ∧ (v = Vundef ∨ v ∈ γ ty).

End EVAL.

Ltac eval_pexpr_inv :=
  repeat match goal with
  | H : eval_pexpr _ _ _ _ (PEvar _ _) _ |- _ => apply eval_pexpr_var_inv in H
  | H : eval_pexpr _ _ _ _ (PElocal _ _) _ |- _ => apply eval_pexpr_local_inv in H; hsplit
  | H : eval_pexpr _ _ _ _ (PEconst _ _ _ _) _ |- _ => apply eval_pexpr_const_inv in H
  | H : eval_pexpr _ _ _ _ (PEunop _ _ _) _ |- _ => apply eval_pexpr_unop_inv in H; hsplit
  | H : eval_pexpr _ _ _ _ (PEbinop _ _ _ _ _) _ |- _ => apply eval_pexpr_binop_inv in H; hsplit
  end.

Definition pexpr_get_ty var (e:pexpr var) : typ :=
  match e with
    | PEvar _ ab => ab
    | PElocal _ => VP
    | PEconst _ ab _ => ab
    | PEunop _ _ ab _ => ab
    | PEbinop _ _ _ ab _ => ab
  end.

Lemma pexpr_get_ty_ok var:
  ∀ F V (ge:Genv.t F V) mem ρ ε e v,
    eval_pexpr (var:=var) ge mem ρ ε e v ->
    v ≠ Vundef ->
    v ∈ γ (pexpr_get_ty e).