Module Cells

Require Import Coqlib.
Require Import Maps Maps2 TreeAl MemChunkTree.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import Cminor.
Require Import Memory.
Require Export DLib.
Require Export LatticeSignatures.
Require Import AbMemSignature.

Inductive cell : Type :=
  | V (p:reg)
  | M (b:block) (i:Z) (chunk:memory_chunk).

Module Cell <: TYPE_EQ.

  Definition s := cell.
  Definition t := (reg + Z * Z * memory_chunk)%type.

  Definition t_of_s (x:s) : t :=
    match x with
      | V p => inl _ p
      | M b i c => inr _ (b, i, c)
    end.

  Definition s_of_t (x: t) : s :=
    match x with
      | inl p => V p
      | inr (b,i,c) => M b i c
    end.

  Lemma inj : forall x : s, s_of_t (t_of_s x) = x.
  Lemma surj: forall x : t, t_of_s (s_of_t x) = x.
  Definition eq: forall (x y: s), {x = y} + {x <> y}.

End Cell.

Module M1 <: TREE with Definition elt := (Z * Z)%type :=
  MakeProdTree(ZTree)(ZTree).
Module M2 <: TREE with Definition elt := (Z * Z * memory_chunk)%type :=
  MakeProdTree(M1)(MemChunkTree.MemChunkTree).
Module M3 <: TREE with Definition elt := (reg + Z * Z * memory_chunk)%type :=
  SumTree(PTree)(M2).

Module CTree <: TREE with Definition elt := cell := BijTree(Cell)(M3).

Module CTreeDom := WPFun CTree.

Definition read (m:memory) (c:cell) : option val :=
  match c with
    | V x => PTree.get x m#1
    | M b ofs chunk => Mem.load chunk m#2 b ofs
  end.

Set Implicit Arguments.

Inductive pexpr (var:Type) : Type :=
  | PEvar : var -> pexpr var
  | PEconst : constant -> pexpr var
  | PEunop : unary_operation -> pexpr var -> pexpr var
  | PEbinop : binary_operation -> pexpr var -> pexpr var -> pexpr var
  | PEcond : pexpr var -> pexpr var -> pexpr var -> pexpr var
  .

Section EVAL.
  Variable var: Type.
  Variable ge: CFG.genv.
  Variable sp: val.
  Variable ρ: var -> val.

  Inductive eval_pexpr: pexpr var -> val -> Prop :=
  | eval_PEvar: forall c v,
    ρ c = v ->
    eval_pexpr (PEvar c) v
  | eval_PEconst: forall cst v,
    eval_constant ge sp cst = Some v ->
    eval_pexpr (PEconst _ cst) v
  | eval_PEunop: forall op a1 v1 v,
    eval_pexpr a1 v1 ->
    eval_unop op v1 = Some v ->
    eval_pexpr (PEunop op a1) v
  | eval_PEbinop: forall op a1 a2 v1 v2 v m,
    eval_pexpr a1 v1 ->
    eval_pexpr a2 v2 ->
    eval_binop op v1 v2 m = Some v ->
    eval_pexpr (PEbinop op a1 a2) v
  | eval_PEcond b l r k res:
    eval_pexpr b k ->
    (Val.bool_of_val k true -> eval_pexpr l res) ->
    (Val.bool_of_val k false -> eval_pexpr r res) ->
    (Val.bool_of_val k true \/ Val.bool_of_val k false) ->
    eval_pexpr (PEcond b l r) res
  .

End EVAL.

Section convert.
  Variable ge: CFG.genv.
  Variable sp: val.
  Variable m: mem.
  Variable e: env.

  Variable realize : memory_chunk -> expr -> list cell.
  Variable realize_correct : forall chunk a b i,
    eval_expr ge sp e m a (Vptr b i) ->
    In (M b (Int.unsigned i) chunk) (realize chunk a).

  Fixpoint convert (e:expr) : list (pexpr cell) :=
    match e with
      | Evar x => PEvar (V x) :: nil
      | Econst c => PEconst _ c :: nil
      | Eunop o e => map (PEunop o) (convert e)
      | Ebinop o e1 e2 =>
        let e1 := convert e1 in
        let e2 := convert e2 in
        fold_left (fun acc x1 =>
                     fold_left (fun acc x2 => PEbinop o x1 x2 :: acc) e2 acc
                  ) e1 nil
      | Eload chunk e =>
        map (@PEvar cell) (realize chunk e)
      | Econdition b l r =>
        match convert l, convert r with
          | nil, nil => nil
          | L, nil => L
          | nil, R => R
          | L, R =>
            fold_left (fun a r =>
                         fold_left (fun a l =>
                                      fold_left (fun a b => PEcond b l r :: a)
                                                (convert b)
                                                a)
                                   L a)
                      R nil
        end
    end.

  Lemma convert_aux q b B r R l L :
      In q (l::L) ->
      In b B ->
      In (@PEcond cell b q r)
         (fold_left (fun a r =>
                       fold_left (fun a l =>
                                    fold_left (fun a b => PEcond b l r :: a)
                                              B a)
                                 (l::L) a)
                    (r::R) nil).

  Lemma convert_aux' q b B r R l L :
      In q (r::R) ->
      In b B ->
      In (@PEcond cell b l q)
         (fold_left (fun a r =>
                       fold_left (fun a l =>
                                    fold_left (fun a b => PEcond b l r :: a)
                                              B a)
                                 (l::L) a)
                    (r::R) nil).

  Definition compat (m:memory) (ρ:cell -> val) : Prop :=
    forall c v, read m c = Some v -> ρ c = v.

  Opaque fold_left.
  Lemma eval_expr_convert_expr : forall ρ,
    compat (e,m) ρ ->
    forall expr v ,
      eval_expr ge sp e m expr v ->
      exists a, In a (convert expr) /\ eval_pexpr ge sp ρ a v.

  Fixpoint simpl_convert (e:expr) : pexpr cell :=
    match e with
      | Evar x => PEvar (V x)
      | Econst c => PEconst _ c
      | Eunop o e => PEunop o (simpl_convert e)
      | Ebinop o e1 e2 => PEbinop o (simpl_convert e1) (simpl_convert e2)
      | Eload chunk e => PEconst _ (Ointconst Int.zero)
      | Econdition b r l => PEcond (simpl_convert b) (simpl_convert r) (simpl_convert l)
    end.

  Fixpoint wf_simpl_expr (e:expr) : bool :=
    match e with
      | Evar x => true
      | Econst c => true
      | Eunop o e => wf_simpl_expr e
      | Ebinop o e1 e2 => wf_simpl_expr e1 && wf_simpl_expr e2
      | Eload chunk e => false
      | Econdition b r l => wf_simpl_expr b && wf_simpl_expr r && wf_simpl_expr l
    end.

  Lemma eval_expr_simpl_convert_expr : forall ρ,
    compat (e,m) ρ ->
    forall expr v ,
      eval_expr ge sp e m expr v ->
      wf_simpl_expr expr = true ->
      eval_pexpr ge sp ρ (simpl_convert expr) v.


End convert.

Module Cell2Val.
Unset Elimination Schemes.
Record adom {t:Type}: Type := {
  val_adom: Adom.adom t val;
  eval_constant: constant -> t;
  eval_unop : unary_operation -> t -> t;
  eval_binop : binary_operation -> t -> t -> t;
  eval_cond : t -> t+⊥ -> t+⊥ -> t+⊥;
  
  eval_constant_correct: forall (ge:CFG.genv) sp c v,
    Cminor.eval_constant ge (Vptr sp Int.zero) c = Some v ->
    γ (eval_constant c) v;
  eval_unop_correct : forall op arg x v,
    Cminor.eval_unop op arg = Some v ->
    γ x arg ->
    γ (eval_unop op x) v;
  eval_binop_correct : forall op arg1 arg2 x1 x2 m v,
    Cminor.eval_binop op arg1 arg2 m = Some v ->
    γ x1 arg1 ->
    γ x2 arg2 ->
    γ (eval_binop op x1 x2) v
; eval_cond_correct b l r B bv :
    γ b B ->
    Val.bool_of_val B bv ->
    forall K,
      γ (if bv then l else r) K ->
      γ (eval_cond b l r) K
}.

Module Eval (T:TREE).

  Module TDom := WPFun T.

  Section val_adom.
    Context {t:Type}.
    Variable a: @adom t.
    
    Fixpoint eval_expr (ab:@TDom.t t) (e:pexpr T.elt) : t+⊥ :=
      match e with
        | PEvar c => TDom.get (val_adom a) ab c
        | PEconst cst => NotBot (eval_constant a cst)
        | PEunop op e => botlift_fun1 (eval_unop a op) (eval_expr ab e)
        | PEbinop op e1 e2 =>
          botlift_fun2 (eval_binop a op) (eval_expr ab e1) (eval_expr ab e2)
        | PEcond b r l =>
          match eval_expr ab b with
            | Bot => Bot
            | NotBot b => eval_cond a b (eval_expr ab r) (eval_expr ab l)
          end
      end.
    
    Instance val_adom_inst : Adom.adom t val := val_adom a.
    Instance val_adom_bot_inst : Adom.adom (t+⊥) val :=
      lift_bot val_adom_inst.
    Instance tree_adom : Adom.adom TDom.t (T.elt->val) :=
      TDom.makebot (val_adom a).

    Lemma eval_expr_correct: forall (ge:CFG.genv) sp (ab:@TDom.t t) ρ e v,
      γ ab ρ ->
      eval_pexpr ge (Vptr sp Int.zero) ρ e v ->
      γ (eval_expr ab e) v.

  End val_adom.
End Eval.

End Cell2Val.