Require Import CSet Le.

Require Import Plus Util AllInRel Map.
Require Import Val Var Env EnvTy IL Annotation Sim Fresh Liveness Status MoreExp.

Set Implicit Arguments.

Definition pmov := list (list var × list var).

Definition pmov_source_set (p:pmov) : set var
  := fold_right (fun p s ⇒ s \ of_list (fst p) ∪ of_list (snd p)) ∅ p.

Section Parallel_Move.
  Variable X:Type.
  Context `{OrderedType X}.

  Fixpoint upd_list p M : env X :=
    match p with
      | nil ⇒ M
      | (l1, l2) :: p´ ⇒ upd_list p´ (M[ l1 <-- lookup_list M l2])
    end.

  Fixpoint par_move (E E´: var → var) (Z : params) (Y : params)
    : var → var :=
    match Z, Y with
      | nil, nil ⇒ E
      | y::Z´, a :: Y´ ⇒
        (fun x ⇒ if [ x = y ] then E´ a else par_move E E´ Z´ Y´ x)
      | _, _ ⇒ E
    end.

  Fixpoint par_list p M :=
    match p with
      | nil ⇒ M
      | (l1, l2) :: p´ ⇒ par_list p´ (par_move M M l1 l2)
    end.

Section Translate.

  Definition check_pmove (vars : set var) (p1 p2 : pmov) :=
    let M1 := par_list p1 (fun x ⇒ x) in
    let M2 := par_list p2 (fun x ⇒ x) in
      for_all
        (fun x ⇒ if [M1 x = M2 x] then true else false) vars.
  Hint Unfold check_pmove.

  Lemma par_move_eq (M1 M2 MC:env X) f fC Z Y
    : (∀ y : var, MC y = M1 (fC y))
    → (∀ y : var, M2 y = M1 (f y))
    → ∀ y : var, M2 [ Z <-- (lookup_list MC Y) ] y = (M1 (par_move f fC Z Y y)).

  Lemma symb_eval p (M1 M2 : env X) f
    : (∀ y, M2 y = (M1 (f y)))
    → ∀ x, upd_list p M2 x = (M1 (par_list p f x)).

  Corollary symb_eval_id : ∀ p (M : env X) x,
    upd_list p M x = (M (par_list p (fun x ⇒ x) x)).

  Lemma check_pmove_correct {vars} {p1} {p2}
    (COK:check_pmove vars p1 p2) (M : env X)
    : agree_on eq vars (upd_list p1 M) (upd_list p2 M).

  Definition check_source_set (p1 p2 : pmov) :=
    if [ pmov_source_set p1 ⊆ pmov_source_set p2 ] then true else false.

  Lemma check_source_set_correct p1 l1 l2
    (COK:check_source_set p1 ((l1,l2)::nil)) (M : onv X)
    (Src:∀ x : var, x \In of_list l2 → M x ≠ ⎣⎦)
    : ∀ x : var, x \In pmov_source_set p1 → M x ≠ ⎣⎦.

  End Translate.

End Parallel_Move.

Section GlueCode.
  Function list_to_stmt (p : list (list var × list var)) (s : stmt) {struct p} : stmt :=
    match p with
      | nil ⇒ s
      | (x :: nil, y:: nil) :: p´ ⇒ stmtLet x (var_to_exp y) (list_to_stmt p´ s)
      | _ ⇒ s
    end.

  Lemma list_to_stmt_correct p s :
    (∀ ass, List.In ass p → ∃ x, ∃ y, ass = (x :: nil, y :: nil)) →
    ∀ M,
    (∀ x, x ∈ pmov_source_set p → M x ≠ None) →
    ∀ K, star2 I.step (K, M, list_to_stmt p s) nil (K, upd_list p M, s).

  Hypothesis parallel_move : var → list var → list var → (list(list var × list var)).

  Definition linearize_parallel_assignment (vars:set var) (l1 l2:list var) :=
    parallel_move (least_fresh vars) l1 l2.

  Function check_is_simple_ass (p : list(list var × list var)) {struct p} : bool :=
    match p with
      | nil ⇒ true
      | (_ :: nil, _ :: nil):: p´ ⇒ check_is_simple_ass p´
      | _ ⇒ false
    end.

  Lemma check_is_simple_ass_correct (p : list (list var × list var)) :
    check_is_simple_ass p →
    ∀ ass, List.In ass p → ∃ x, ∃ y, ass = (x :: nil, y :: nil).

  Definition validate_parallel_assignment vars p l1 l2 :=
    check_is_simple_ass p
    ∧ check_pmove vars p ((l1, l2) :: nil)
    ∧ check_source_set p ((l1, l2) :: nil).

  Lemma validate_parallel_assignment_correct vars p l1 l2
    (VOK:validate_parallel_assignment vars p l1 l2)
    : ∀ M K cont (Src:∀ x : var, x \In of_list l2 → M x ≠ ⎣⎦), ∃ M´,
        star2 I.step (K, M, list_to_stmt p cont) nil (K, M´, cont) ∧
        agree_on eq vars M´ (M[ l1 <-- lookup_list M l2]).

  Definition compile_parallel_assignment
    (vars:set var) (l1 l2 : list var) (s : stmt) : status stmt :=
    let p := linearize_parallel_assignment vars l1 l2 in
    if [validate_parallel_assignment vars p l1 l2] then
      Success (list_to_stmt p s) else
        Error "compile parallel assignment failed".

  Lemma compile_parallel_assignment_correct
    : ∀ vars l1 l2 s s´,
      compile_parallel_assignment vars l1 l2 s = Success s´ →
      ∀ M K (Src:∀ x : var, x \In (of_list l2) → M x ≠ ⎣⎦), ∃ M´,
        star2 I.step (K, M, s´) nil (K, M´, s) ∧
        agree_on eq vars M´ (M[ l1 <-- lookup_list M l2]).

End GlueCode.

Section Implementation.
  Hypothesis parallel_move : var → list var → list var → (list(list var × list var)).

Fixpoint onlyVars (Y:args) : status params :=
  match Y with
    | nil ⇒ Success nil
    | (Var x)::Y ⇒ sdo Y´ <- onlyVars Y; Success (x::Y´)
    | _ ⇒ Error "onlyVars: argument list contains expressions"
  end.

Lemma onlyVars_defined (E:onv var) Y Y´ v
  : onlyVars Y = Success Y´
    → omap (exp_eval E) Y = Some v
    → ∀ x, x ∈ of_list Y´ → E x ≠ None.

Lemma onlyVars_lookup (E:onv var) Y Y´ v
  : onlyVars Y = Success Y´
    → omap (exp_eval E) Y = Some v
    → lookup_list E Y´ = List.map Some v.

Fixpoint lower DL s (an:ann (set var))
  : status stmt :=
  match s, an with
    | stmtLet x e s, ann1 lv ans ⇒
      sdo sl <- lower DL s ans;
        Success (stmtLet x e sl)
    | stmtIf x s t, ann2 lv ans ant ⇒
      sdo sl <- lower DL s ans;
        sdo tl <- lower DL t ant;
            Success (stmtIf x sl tl)
    | stmtApp l Y, ann0 lv ⇒
       sdo Lve <- option2status (nth_error DL (counted l)) "lower: No annotation for function";
        sdo Y <- onlyVars Y;
        let ´(lv´, Z) := Lve in
        compile_parallel_assignment parallel_move lv´ Z Y (stmtApp l nil)

    | stmtReturn x, ann0 lv ⇒ Success (stmtReturn x)
    | stmtExtern x f Y s, ann1 _ ans ⇒
      sdo sl <- lower DL s ans;
        Success (stmtExtern x f Y sl)
    | stmtFun Z s t, ann2 lv ans ant ⇒
      let DL´ := (getAnn ans,Z) in
      sdo s´ <- lower (DL´ :: DL)%list s ans;
        sdo t´ <- lower (DL´ :: DL)%list t ant;
        Success (stmtFun nil s´ t´)
    | s, _ ⇒ Error "lower: Annotation mismatch"
  end.

Inductive approx
: list (set var × list var) → I.block → I.block → Prop :=
  approxI Lv s Z lv s´
  (al:ann (set var))
  (LS:live_sound Imperative ((lv,Z)::Lv) s al)
  (AL:(of_list Z) ⊆ lv)
  (EQ:getAnn al \ of_list Z ⊆ lv)
  (spm:lower ((lv,Z)::Lv) s al = Success s´)
  : approx ((lv,Z)::Lv) (I.blockI Z s) (I.blockI nil s´).

Inductive pmSim : I.state → I.state → Prop :=
  pmSimI Lv s (E E´:onv val) L L´ s´
  (al: ann (set var))
  (LS:live_sound Imperative Lv s al)
  (pmlowerOk:lower Lv s al = Success s´)
  (LA:AIR3 approx Lv L L´)
  (EEQ:agree_on eq (getAnn al) E E´)
  : pmSim (L,E,s) (L´, E´, s´).

Lemma pmSim_sim σ1 σ2
: pmSim σ1 σ2 → sim σ1 σ2.

End Implementation.