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.

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

Inductive pexpr (var:Type) : Type :=
| PEvar : var -> typ -> pexpr var
| PElocal: ident -> pexpr var (* address of a local variable *)
| PEconst : option constant -> typ -> pexpr var (* None is /any/ value *)
| PEunop : unary_operation -> pexpr var -> typ -> pexpr var
| PEbinop : binary_operation -> pexpr var -> pexpr var -> typ -> pexpr var.

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 None ty => "?" ++ "@" ++ to_string ty
  | PEconst (Some 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,
    pexpr_eval_constant cst = v ->
    (v = Vundef \/ v ∈ γ ty) ->
    eval_pexpr (PEconst _ (Some cst) ty) v
  | eval_PEconst_none: forall v ty,
    v ≠ Vundef →
    v ∈ γ ty ->
    eval_pexpr (PEconst _ None ty) v
  | eval_PEunop: forall op a1 v1 v ty,
    eval_pexpr a1 v1 ->
    eval_unop op v1 = Some v ->
    (v = Vundef \/ v ∈ γ ty) ->
    eval_pexpr (PEunop op a1 ty) v
  | eval_PEbinop: forall op a1 a2 v1 v2 v 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) 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_Some_inv cst ty v :
    eval_pexpr (PEconst _ (Some cst) ty) v →
    v = pexpr_eval_constant cst ∧ (v = Vundef ∨ v ∈ γ ty).

  Lemma eval_pexpr_const_None_inv ty v :
    eval_pexpr (PEconst _ None ty) v →
    v ≠ Vundef.

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

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

  Lemma eval_pexpr_binop_inv op u₁ u₂ ty v :
    eval_pexpr (PEbinop op u₁ u₂ ty) 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 _ None _) _ |- _ => apply eval_pexpr_const_None_inv in H
  | H : eval_pexpr _ _ _ _ (PEconst _ (Some _) _) _ |- _ => apply eval_pexpr_const_Some_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).