Qcert.NNRC.Optim.NNRCRewrite
Section NNRCRewrite.
Context {fruntime:foreign_runtime}.
Lemma unshadow_ext_preserves sep renamer avoid (e:nnrc) :
nnrc_ext_eq (unshadow sep renamer avoid e) e.
Lemma dot_of_rec a (e:nnrc) :
nnrc_ext_eq (NNRCUnop (ADot a) (NNRCUnop (ARec a) e)) e.
Lemma nnrc_merge_concat_to_concat s1 s2 p1 p2:
s1 ≠ s2 →
‵[| (s1, p1)|] ⊗ ‵[| (s2, p2)|] ≡ᶜ ‵{|‵[| (s1, p1)|] ⊕ ‵[| (s2, p2)|]|}.
Lemma for_nil x e2 :
nnrc_ext_eq (NNRCFor x ‵{||} e2) ‵{||}.
Lemma for_singleton_to_let x e1 e2:
nnrc_ext_eq (NNRCFor x (NNRCUnop AColl e1) e2)
(NNRCUnop AColl (NNRCLet x e1 e2)).
Lemma flatten_nil_nnrc :
nnrc_ext_eq (♯flatten(‵{||})) ‵{||}.
Lemma map_sigma_fusion (e1 e2 e3:nnrc) (v1 v2:var) :
¬ In v1 (nnrc_free_vars e3) →
nnrc_ext_eq
(NNRCFor v2
(NNRCUnop AFlatten
(NNRCFor v1 e1
(NNRCIf e2 (NNRCUnop AColl (NNRCVar v1)) (NNRCConst (dcoll nil)))))
e3)
(NNRCUnop AFlatten
(NNRCFor v1 e1
(NNRCIf e2
(NNRCUnop AColl (NNRCLet v2 (NNRCVar v1) e3))
(NNRCConst (dcoll nil))))).
Lemma map_sigma_fusion_samevar (e1 e2 e3:nnrc) (v1:var) :
nnrc_ext_eq
(NNRCFor v1
(NNRCUnop AFlatten
(NNRCFor v1 e1
(NNRCIf e2 (NNRCUnop AColl (NNRCVar v1)) (NNRCConst (dcoll nil)))))
e3)
(NNRCUnop AFlatten
(NNRCFor v1 e1
(NNRCIf e2
(NNRCUnop AColl e3)
(NNRCConst (dcoll nil))))).
Lemma for_over_if x e1 e2 e3 ebody :
nnrc_ext_eq (NNRCFor x (NNRCIf e1 e2 e3) ebody)
(NNRCIf e1 (NNRCFor x e2 ebody)
(NNRCFor x e3 ebody)).
Lemma for_over_either_disjoint x e1 xl el xr er ebody:
disjoint (xl::xr::nil) (nnrc_free_vars ebody) →
nnrc_ext_eq (NNRCFor x (NNRCEither e1 xl el xr er) ebody)
(NNRCEither e1
xl (NNRCFor x el ebody)
xr (NNRCFor x er ebody)).
Lemma nnrceither_rename_l e1 xl el xr er xl' :
¬ In xl' (nnrc_free_vars el) →
¬ In xl' (nnrc_bound_vars el) →
nnrc_ext_eq (NNRCEither e1 xl el xr er)
(NNRCEither e1 xl' (nnrc_subst el xl (NNRCVar xl')) xr er).
Lemma nnrceither_rename_r e1 xl el xr er xr' :
¬ In xr' (nnrc_free_vars er) →
¬ In xr' (nnrc_bound_vars er) →
nnrc_ext_eq (NNRCEither e1 xl el xr er)
(NNRCEither e1 xl el xr' (nnrc_subst er xr (NNRCVar xr'))).
Lemma for_over_either sep x e1 xl el xr er ebody:
nnrc_ext_eq (NNRCFor x (NNRCEither e1 xl el xr er) ebody)
( let xl' := really_fresh_in_ext sep xl (nnrc_free_vars el ++ nnrc_bound_vars el) ebody in
let xr' := really_fresh_in_ext sep xr (nnrc_free_vars er ++ nnrc_bound_vars er) ebody in
(NNRCEither e1
xl' (NNRCFor x (nnrc_subst el xl (NNRCVar xl')) ebody)
xr' (NNRCFor x (nnrc_subst er xr (NNRCVar xr')) ebody))).
Lemma nnrcunop_over_either op e1 xl el xr er:
nnrc_ext_eq (NNRCUnop op (NNRCEither e1 xl el xr er))
(NNRCEither e1 xl (NNRCUnop op el) xr (NNRCUnop op er)).
Lemma nnrcunop_over_if op e1 e2 e3:
nnrc_ext_eq (NNRCUnop op (NNRCIf e1 e2 e3))
(NNRCIf e1 (NNRCUnop op e2) (NNRCUnop op e3)).
Lemma sigma_to_if (e1 e2:nnrc) (v:var) :
nnrc_ext_eq
(NNRCUnop AFlatten
(NNRCFor v (NNRCUnop AColl e2)
(NNRCIf e1
(NNRCUnop AColl (NNRCVar v))
(NNRCConst (dcoll nil)))))
(NNRCLet v e2 (NNRCIf e1 (NNRCUnop AColl (NNRCVar v)) (NNRCConst (dcoll nil)))).
Lemma unshadow_free_vars sep renamer (x:var) (e:nnrc):
In x (nnrc_free_vars (unshadow sep renamer nil e)) → In x (nnrc_free_vars e).
optimizations for record projection
Lemma nnrcproject_over_concat sl p1 p2 :
π[sl](p1 ⊕ p2)
≡ᶜ π[sl](p1) ⊕ π[sl](p2).
Lemma nnrcproject_over_const sl l :
π[sl](NNRCConst (drec l)) ≡ᶜ NNRCConst (drec (rproject l sl)).
Lemma nnrcproject_over_rec_in sl s p :
In s sl →
π[sl](‵[| (s, p) |]) ≡ᶜ ‵[| (s, p) |].
Lemma nnrcproject_over_nnrcproject sl1 sl2 p :
π[sl1](π[sl2](p)) ≡ᶜ π[set_inter string_dec sl2 sl1](p).
Lemma nnrcproject_over_either sl p xl xr p1 p2 :
π[sl](NNRCEither p xl p1 xr p2) ≡ᶜ NNRCEither p xl (π[sl](p1)) xr (π[sl](p2)).
End NNRCRewrite.
π[sl](p1 ⊕ p2)
≡ᶜ π[sl](p1) ⊕ π[sl](p2).
Lemma nnrcproject_over_const sl l :
π[sl](NNRCConst (drec l)) ≡ᶜ NNRCConst (drec (rproject l sl)).
Lemma nnrcproject_over_rec_in sl s p :
In s sl →
π[sl](‵[| (s, p) |]) ≡ᶜ ‵[| (s, p) |].
Lemma nnrcproject_over_nnrcproject sl1 sl2 p :
π[sl1](π[sl2](p)) ≡ᶜ π[set_inter string_dec sl2 sl1](p).
Lemma nnrcproject_over_either sl p xl xr p1 p2 :
π[sl](NNRCEither p xl p1 xr p2) ≡ᶜ NNRCEither p xl (π[sl](p1)) xr (π[sl](p2)).
End NNRCRewrite.