Qcert.NNRC.Optim.NNRCRewriteUtil

Section NNRCRewriteUtil.



  Context {fruntime:foreign_runtime}.

  Lemma not_in_over_app {A} (x:A) (l1 l2:list A) :
    ¬In x (l1++l2) → ¬In x l1 ∧ ¬In x l2.

  Lemma really_fresh_is_really_fresh {sep} {oldvar} (avoid:list var) (e:nnrc) (x:var) :
    x = really_fresh_in sep oldvar avoid e →
    (¬In x avoid) ∧ (¬In x (nnrc_free_vars e)) ∧ (¬In x (nnrc_bound_vars e)).

  Lemma split_really_fresh_app (x:var) l1 l2 l3 l4 :
    ¬ False ∧
       ¬ In x (l1 ++ l2) ∧
       ¬ In x (l3 ++ l4) →
    ((¬In x l1) ∧ (¬In x l2)) ∧
    ((¬In x l3) ∧ (¬In x l4)).

  Lemma split_really_fresh_app2 (x:var) l1 l2 l3 l4 :
    ¬ False ∧
       ¬ In x (l1 ++ l2) ∧
       ¬ In x (l3 ++ l4) →
    (¬ False ∧ (¬In x l1) ∧ (¬In x l3)) ∧
    (¬ False ∧ (¬In x l2) ∧ (¬In x l4)).

  Lemma dupl_var_ignored {h:list (string×string)} (d1 d2:data) (env:bindings) (v:var) (e:nnrc):
    nnrc_core_eval h ((v,d1) :: (v,d2) :: env) e = nnrc_core_eval h ((v,d1)::env) e.

  Lemma not_or p1 p2:
    ~(p1 ∨ p2) → ¬p1 ∧ ¬p2.

  Lemma remove_in l (x v:var):
    v≠x → ¬ In x (remove equiv_dec v l) →
    ¬ In x l.

  Lemma split_really_fresh_app3 (v x:var) l1 l2 l3 l4 :
    ¬ False ∧
       ¬
       In x (l1 ++ remove equiv_dec v l2) ∧
       ¬ (v = x ∨ In x (l3 ++ l4)) →
    (v ≠ x) ∧ (¬ False ∧ (¬In x l1) ∧ (¬In x l3)) ∧
    (¬ False ∧ (¬In x l2) ∧ (¬In x l4)).

  Lemma nnrc_subst_rename {sep} {oldvar} (e1 e2:nnrc) (x1 x2:var) :
    x2 = really_fresh_in sep oldvar nil e2 →
    nnrc_eq (NNRCLet x1 e1 e2) (NNRCLet x2 e1 (nnrc_subst e2 x1 (NNRCVar x2))).

  Inductive var_use :=
  | NotUsed
  | UsedOnce
  | UsedMany.

  Definition use_sum u1 u2 :=
    match (u1,u2) with
      | (UsedMany,_) ⇒ UsedMany
      | (_,UsedMany) ⇒ UsedMany
      | (UsedOnce,UsedOnce) ⇒ UsedMany
      | (UsedOnce,NotUsed) ⇒ UsedOnce
      | (NotUsed,UsedOnce) ⇒ UsedOnce
      | (NotUsed,NotUsed) ⇒ NotUsed
    end.

  Lemma use_sum_once u1 u2:
    use_sum u1 u2 = UsedOnce ↔
    ((u1 = UsedOnce) ∧ (u2 = NotUsed)) ∨
    ((u1 = NotUsed) ∧ (u2 = UsedOnce)).

  Lemma use_sum_not u1 u2:
    use_sum u1 u2 = NotUsed ↔
    (u1 = NotUsed) ∧ (u2 = NotUsed).

  Definition use_alt u1 u2 :=
    match (u1,u2) with
      | (UsedOnce,UsedOnce) ⇒ UsedOnce
      | (NotUsed,NotUsed) ⇒ NotUsed
      | _ ⇒ UsedMany
    end.

  Lemma use_alt_once u1 u2:
    use_alt u1 u2 = UsedOnce ↔
    ((u1 = UsedOnce) ∧ (u2 = UsedOnce)).

  Lemma use_alt_not u1 u2:
    use_alt u1 u2 = NotUsed ↔
    ((u1 = NotUsed) ∧ (u2 = NotUsed)).

  Definition use_exp u1 u2 :=
    match (u1,u2) with
      | (UsedMany,_) ⇒ UsedMany
      | (_,UsedMany) ⇒ UsedMany
      | (_,UsedOnce) ⇒ UsedMany
      | (UsedOnce,NotUsed) ⇒ UsedOnce
      | (NotUsed,NotUsed) ⇒ NotUsed
    end.

  Lemma use_exp_once u1 u2:
    use_exp u1 u2 = UsedOnce ↔ (u1 = UsedOnce) ∧ (u2 = NotUsed).

  Lemma use_exp_not x y :
    (use_exp x y) = NotUsed ↔
    (x = NotUsed ∧ y = NotUsed).

  Fixpoint use_count (x:var) (e:nnrc) : var_use :=
    match e with
      | NNRCVar x' ⇒ (if x == x' then UsedOnce else NotUsed)
      | NNRCConst _ ⇒ NotUsed
      | NNRCBinop _ e1 e2 ⇒
        use_sum (use_count x e1) (use_count x e2)
      | NNRCUnop _ e1 ⇒ use_count x e1
      | NNRCLet x' e1 e2 ⇒
        if (x == x') then use_count x e1
        else use_sum (use_count x e1) (use_count x e2)
      | NNRCFor x' e1 e2 ⇒
        use_exp (use_count x e1) (if x == x' then NotUsed else (use_count x e2))
      | NNRCIf e1 e2 e3 ⇒
        use_sum (use_count x e1) (use_alt (use_count x e2) (use_count x e3))
      | NNRCEither ed xl el xr er ⇒
        use_sum
                   (use_count x ed)
                   (use_alt
                      (if x == xl then NotUsed else use_count x el)
                      (if x == xr then NotUsed else use_count x er))
      | NNRCGroupBy _ _ e1 ⇒ use_count x e1
    end.

  Lemma NotUsed_nfree v e :
    use_count v e = NotUsed ↔ ¬ In v (nnrc_free_vars e).

  Lemma not_used_ignored {h:list(string×string)} (d:data) (env:bindings) (v:var) (e:nnrc) :
    (use_count v e) = NotUsed → nnrc_core_eval h ((v,d)::env) e = nnrc_core_eval h env e.

End NNRCRewriteUtil.