Section NNRCOptimizer.
Require Import String.
Require Import List ListSet.
Require Import Arith.
Require Import Equivalence.
Require Import Morphisms.
Require Import Setoid.
Require Import EquivDec.
Require Import Program.
Require Import Utils.
Require Import BasicSystem.
Require Import cNNRCSystem.
Require Import NNRCSystem.
Require Import NNRCRewriteUtil.
Require Import NNRCRewrite.
Require Import TNNRCRewrite.
Require Import OptimizerLogger.
Require Import OptimizerStep.
Local Open Scope nnrc_scope.
Local Open Scope string.
Section engine.
Apply the function f to the direct child of p
Context {
fruntime:
foreign_runtime}.
Definition nnrc_map (
f:
nnrc ->
nnrc) (
e:
nnrc) :=
match e with
|
NNRCVar v =>
NNRCVar v
|
NNRCConst d =>
NNRCConst d
|
NNRCBinop bop e1 e2 =>
NNRCBinop bop (
f e1) (
f e2)
|
NNRCUnop uop e1 =>
NNRCUnop uop (
f e1)
|
NNRCLet v e1 e2 =>
NNRCLet v (
f e1) (
f e2)
|
NNRCFor v e1 e2 =>
NNRCFor v (
f e1) (
f e2)
|
NNRCIf e1 e2 e3 =>
NNRCIf (
f e1) (
f e2) (
f e3)
|
NNRCEither ed xl el xr er =>
NNRCEither (
f ed)
xl (
f el)
xr (
f er)
|
NNRCGroupBy g sl e1 =>
NNRCGroupBy g sl (
f e1)
end.
Lemma nnrc_map_correctness:
forall f:
nnrc ->
nnrc,
forall e:
nnrc,
(
forall e',
nnrc_ext_eq (
f e')
e') ->
nnrc_ext_eq (
nnrc_map f e)
e.
Proof.
intros f e Hf.
nnrc_cases (induction e) Case;
try solve [simpl; repeat rewrite Hf; reflexivity].
Qed.
Apply the function f to all subexpression of e.
Fixpoint nnrc_map_deep (
f:
nnrc ->
nnrc) (
e:
nnrc) :=
match e with
|
NNRCVar v =>
f (
NNRCVar v)
|
NNRCConst d =>
f (
NNRCConst d)
|
NNRCBinop bop e1 e2 =>
f (
NNRCBinop bop (
nnrc_map_deep f e1) (
nnrc_map_deep f e2))
|
NNRCUnop uop e1 =>
f (
NNRCUnop uop (
nnrc_map_deep f e1))
|
NNRCLet v e1 e2 =>
f (
NNRCLet v (
nnrc_map_deep f e1) (
nnrc_map_deep f e2))
|
NNRCFor v e1 e2 =>
f (
NNRCFor v (
nnrc_map_deep f e1) (
nnrc_map_deep f e2))
|
NNRCIf e1 e2 e3 =>
f (
NNRCIf (
nnrc_map_deep f e1) (
nnrc_map_deep f e2) (
nnrc_map_deep f e3))
|
NNRCEither ed xl el xr er =>
f (
NNRCEither (
nnrc_map_deep f ed)
xl (
nnrc_map_deep f el)
xr (
nnrc_map_deep f er))
|
NNRCGroupBy g sl e1 =>
f (
NNRCGroupBy g sl (
nnrc_map_deep f e1))
end.
Lemma nnrc_map_deep_corretness:
forall f:
nnrc ->
nnrc,
forall e:
nnrc,
(
forall e',
nnrc_ext_eq (
f e')
e') ->
nnrc_ext_eq (
nnrc_map_deep f e)
e.
Proof.
intros f e Hf.
nnrc_cases (induction e) Case; simpl;
try solve [repeat rewrite Hf; reflexivity];
try solve [repeat rewrite Hf; rewrite IHe; reflexivity ];
try solve [repeat rewrite Hf; rewrite IHe1; rewrite IHe2; reflexivity ];
try solve [repeat rewrite Hf; rewrite IHe1; rewrite IHe2; rewrite IHe3; reflexivity ].
Qed.
Definition nunshadow :=
unshadow_simpl nil.
Definition head_rew (
e:
nnrc) :=
(
nunshadow e).
Lemma head_rew_correctness e:
nnrc_ext_eq (
head_rew e)
e.
Proof.
Lemma rewriter_simpl_rew_no_free_var :
forall (
op :
nnrc) (
x :
var),
In x (
nnrc_free_vars (
head_rew op)) ->
In x (
nnrc_free_vars op).
Proof.
End engine.
Ltac tcorrectness_prover :=
simpl;
repeat progress
(
try match goal with
| [|-
context [
match ?
p with |
_ =>
_ end] ] =>
destruct p
end;
try reflexivity;
try unfold Equivalence.equiv in *;
try subst).
Ltac tprove_correctness p :=
destruct p;
tcorrectness_prover.
Lemma tnnrc_ext_rewrites_to_trans {
model:
basic_model}
e1 e2 e3:
tnnrc_ext_rewrites_to e1 e2 ->
tnnrc_ext_rewrites_to e2 e3 ->
tnnrc_ext_rewrites_to e1 e3.
Proof.
apply transitivity.
Qed.
Lemma AUX {
model:
basic_model}
f e e' :
(
forall e,
tnnrc_ext_rewrites_to e (
f e)) ->
tnnrc_ext_rewrites_to e e' ->
tnnrc_ext_rewrites_to e (
f e').
Proof.
intros.
rewrite H0 at 1.
rewrite (H e') at 1.
reflexivity.
Qed.
Definition tnnrc_map {
fruntime:
foreign_runtime} :=
nnrc_map.
Lemma tnnrc_map_correctness {
model:
basic_model}:
forall f:
nnrc ->
nnrc,
forall p:
nnrc,
(
forall p',
tnnrc_ext_rewrites_to p' (
f p')) ->
tnnrc_ext_rewrites_to p (
tnnrc_map f p).
Proof.
intros.
nnrc_cases (induction p) Case; try solve [simpl; apply Hf]; simpl;
try reflexivity;
try (rewrite (H p1) at 1; rewrite (H p2) at 1; reflexivity).
rewrite (H p) at 1; reflexivity.
simpl.
rewrite (H p1) at 1; rewrite (H p2) at 1; rewrite (H p3) at 1.
reflexivity.
rewrite (H p1) at 1; rewrite (H p2) at 1; rewrite (H p3) at 1.
reflexivity.
rewrite (H p) at 1; reflexivity.
Qed.
Definition tnnrc_map_deep {
fruntime:
foreign_runtime} :=
nnrc_map_deep.
Lemma tnnrc_map_deep_correctness {
model:
basic_model}:
forall f:
nnrc ->
nnrc,
forall p:
nnrc,
(
forall p',
tnnrc_ext_rewrites_to p' (
f p')) ->
tnnrc_ext_rewrites_to p (
tnnrc_map_deep f p).
Proof.
intros f p Hf.
nnrc_cases (induction p) Case; try solve [simpl; apply Hf];
try reflexivity; simpl;
try (rewrite IHp1 at 1; rewrite IHp2 at 1; rewrite Hf at 1; reflexivity);
try (rewrite IHp at 1; rewrite Hf at 1; reflexivity).
rewrite IHp1 at 1; rewrite IHp2 at 1; rewrite IHp3 at 1; rewrite Hf at 1; reflexivity.
rewrite IHp1 at 1; rewrite IHp2 at 1; rewrite IHp3 at 1; rewrite Hf at 1; reflexivity.
Qed.
Definition tunshadow_preserves_fun {
fruntime:
foreign_runtime} (
e:
nnrc) :=
unshadow_simpl nil e.
Lemma tunshadow_preserves_fun_correctness {
model:
basic_model} (
e:
nnrc):
tnnrc_ext_rewrites_to e (
tunshadow_preserves_fun e).
Proof.
Definition tunshadow_preserves_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
unshadow"
"
Renames variables to avoid shadowing"
"
tunshadow_preserves_fun"
tunshadow_preserves_fun .
Definition tunshadow_preserves_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tunshadow_preserves_step tunshadow_preserves_fun_correctness.
Definition tfor_nil_fun {
fruntime:
foreign_runtime}(
e:
nnrc) :=
match e with
|
NNRCFor x ‵{||}
e2 => ‵{||}
|
_ =>
e
end.
Lemma tfor_nil_fun_correctness {
model:
basic_model} (
e:
nnrc) :
tnnrc_ext_rewrites_to e (
tfor_nil_fun e).
Proof.
Definition tfor_nil_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
for/
nil"
"
Remove loop comprehensions over empty bags"
"
tfor_nil_fun"
tfor_nil_fun .
Definition tfor_nil_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tfor_nil_step tfor_nil_fun_correctness.
Definition tfor_singleton_to_let_fun {
fruntime:
foreign_runtime} (
e:
nnrc) :=
match e with
|
NNRCFor x (
NNRCUnop AColl e1)
e2
=>
NNRCUnop AColl (
NNRCLet x e1 e2)
|
_ =>
e
end.
Lemma tfor_singleton_to_let_fun_correctness {
model:
basic_model} (
e:
nnrc) :
tnnrc_ext_rewrites_to e (
tfor_singleton_to_let_fun e).
Proof.
Definition tfor_singleton_to_let_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
for/
singleton"
"
Lower a loop comprehension over a singleton into a singleton of a let"
"
tfor_singleton_to_let_step"
tfor_singleton_to_let_fun .
Definition tfor_singleton_to_let_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tfor_singleton_to_let_step tfor_singleton_to_let_fun_correctness.
Definition tflatten_singleton_fun {
fruntime:
foreign_runtime} (
e:
nnrc)
:=
match e with
| ♯
flatten(‵{|
e1 |}) =>
e1
|
_ =>
e
end.
Lemma tflatten_singleton_fun_correctness {
model:
basic_model} (
e:
nnrc) :
tnnrc_ext_rewrites_to e (
tflatten_singleton_fun e).
Proof.
Definition tflatten_singleton_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
flatten/
singleton"
"
Simplify a flatten of a singleton bag"
"
tflatten_singleton_fun"
tflatten_singleton_fun .
Definition tflatten_singleton_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tflatten_singleton_step tflatten_singleton_fun_correctness.
Definition tflatten_nil_fun {
fruntime:
foreign_runtime} (
e:
nnrc)
:=
match e with
| ♯
flatten(‵{||}) => ‵{||}
|
_ =>
e
end.
Lemma tflatten_nil_fun_correctness {
model:
basic_model} (
e:
nnrc) :
tnnrc_ext_rewrites_to e (
tflatten_nil_fun e).
Proof.
Definition tflatten_nil_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
flatten/
nil"
"
Simplify flatten of an empty bag"
"
tflatten_nil_fun"
tflatten_nil_fun .
Definition tflatten_nil_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tflatten_nil_step tflatten_nil_fun_correctness.
Definition tsigma_to_if_fun {
fruntime:
foreign_runtime}(
e:
nnrc) :=
match e with
| (
NNRCUnop AFlatten
(
NNRCFor v1 (
NNRCUnop AColl e2)
(
NNRCIf e1
(
NNRCUnop AColl (
NNRCVar v2))
(
NNRCConst (
dcoll nil))))) =>
if (
v1 ==
v2)
then (
NNRCLet v1 e2 (
NNRCIf e1 (
NNRCUnop AColl (
NNRCVar v1)) (
NNRCConst (
dcoll nil))))
else e
|
_ =>
e
end.
Lemma tsigma_to_if_fun_correctness {
model:
basic_model} (
e:
nnrc) :
tnnrc_ext_rewrites_to e (
tsigma_to_if_fun e).
Proof.
Definition tsigma_to_if_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
sigma/
if"
"???"
"
tsigma_to_if_fun"
tsigma_to_if_fun .
Definition tsigma_to_if_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tsigma_to_if_step tsigma_to_if_fun_correctness.
Definition tmap_sigma_fusion_samevar_fun {
fruntime:
foreign_runtime}(
e:
nnrc) :=
match e with
| (
NNRCFor v2
(
NNRCUnop AFlatten
(
NNRCFor v1 e1
(
NNRCIf e2 (
NNRCUnop AColl (
NNRCVar v1')) (
NNRCConst (
dcoll nil)))))
e3) =>
if (
v1 ==
v1')
then
if (
v1 ==
v2)
then
(
NNRCUnop AFlatten
(
NNRCFor v1 e1
(
NNRCIf e2
(
NNRCUnop AColl e3)
(
NNRCConst (
dcoll nil)))))
else e
else e
|
_ =>
e
end.
Lemma tmap_sigma_fusion_samevar_fun_correctness {
model:
basic_model} (
e:
nnrc) :
tnnrc_ext_rewrites_to e (
tmap_sigma_fusion_samevar_fun e).
Proof.
Definition tmap_sigma_fusion_samevar_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
sigma/
same var fusion"
"???"
"
tmap_sigma_fusion_samevar_fun"
tmap_sigma_fusion_samevar_fun .
Definition tmap_sigma_fusion_samevar_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tmap_sigma_fusion_samevar_step tmap_sigma_fusion_samevar_fun_correctness.
Definition tdot_of_rec_fun {
fruntime:
foreign_runtime}(
e:
nnrc) :=
match e with
| (
NNRCUnop (
ADot s1)
(
NNRCUnop (
ARec s2)
e1)) =>
if (
s1 ==
s2)
then e1
else e
|
_ =>
e
end.
Lemma tdot_of_rec_fun_correctness {
model:
basic_model} (
e:
nnrc) :
tnnrc_ext_rewrites_to e (
tdot_of_rec_fun e).
Proof.
Definition tdot_of_rec_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
dot/
rec"
"
Simplify lookup of a new record constructor"
"
tdot_of_rec_fun"
tdot_of_rec_fun .
Definition tdot_of_rec_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tdot_of_rec_step tdot_of_rec_fun_correctness.
Definition tmerge_concat_to_concat_fun {
fruntime:
foreign_runtime}(
e:
nnrc)
:=
match e with
| (‵[| (
s1,
p1)|] ⊗ ‵[| (
s2,
p2)|])
=>
if (
equiv_decb s1 s2)
then e
else (‵{|‵[| (
s1,
p1)|] ⊕ ‵[| (
s2,
p2)|]|})
|
_ =>
e
end.
Lemma tmerge_concat_to_concat_fun_correctness {
model:
basic_model} (
e:
nnrc) :
tnnrc_ext_rewrites_to e (
tmerge_concat_to_concat_fun e).
Proof.
destruct e;
simpl;
try reflexivity.
destruct b;
simpl;
try reflexivity.
destruct e1;
simpl;
try reflexivity.
destruct u;
simpl;
try reflexivity.
destruct e2;
simpl;
try reflexivity.
destruct u;
simpl;
try reflexivity.
unfold equiv_decb.
destruct (
equiv_dec s s0);
try reflexivity.
apply tnnrc_merge_concat_to_concat_arrow;
trivial.
Qed.
Definition tmerge_concat_to_concat_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
merge-
concat->
merge"
"
Simplify a merge-
concat of two singleton records with different fields using concat"
"
tmerge_concat_to_concat_fun"
tmerge_concat_to_concat_fun .
Definition tmerge_concat_to_concat_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tmerge_concat_to_concat_step tmerge_concat_to_concat_fun_correctness.
Definition tdot_of_concat_rec_fun {
fruntime:
foreign_runtime}(
e:
nnrc)
:=
match e with
| (
NNRCUnop (
ADot s) (
NNRCBinop AConcat e1 (
NNRCUnop (
ARec s2)
e2)))
=>
if equiv_decb s s2
then e2
else (
NNRCUnop (
ADot s)
e1)
|
_ =>
e
end.
Lemma tdot_of_concat_rec_fun_correctness {
model:
basic_model} (
e:
nnrc) :
tnnrc_ext_rewrites_to e (
tdot_of_concat_rec_fun e).
Proof.
Definition tdot_of_concat_rec_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
dot/
concat/
rec 2"
"
Simplifies lookup of a concatenation with a record constructor"
"
tdot_of_concat_rec_fun"
tdot_of_concat_rec_fun .
Definition tdot_of_concat_rec_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tdot_of_concat_rec_step tdot_of_concat_rec_fun_correctness.
Inlining
Definition is_small_unop {
fruntime:
foreign_runtime} (
u:
unaryOp) :=
match u with
|
AIdOp
|
ANeg
|
AColl
|
ALeft
|
ARight
|
ABrand _
|
ARec _
=>
true
|
_ =>
false
end.
Fixpoint should_inline_small {
fruntime:
foreign_runtime} (
from:
nnrc)
:=
match from with
|
NNRCVar _
|
NNRCConst _ =>
true
|
NNRCUnop u e =>
is_small_unop u &&
should_inline_small e
|
NNRCBinop AConcat (
NNRCUnop (
ARec _)
e1) (
NNRCUnop (
ARec _)
e2) =>
true
|
_ =>
false
end.
Definition should_inline_few_occurences {
fruntime:
foreign_runtime} (
x:
var) (
to:
nnrc)
:=
match use_count x to with
|
NotUsed
|
UsedOnce =>
true
|
_ =>
false
end.
Definition should_inline {
fruntime:
foreign_runtime} (
x:
var) (
from to:
nnrc)
:=
should_inline_small from
||
should_inline_few_occurences x to.
Definition tinline_let_fun {
fruntime:
foreign_runtime}(
e:
nnrc)
:=
match e with
|
NNRCLet x e1 e2 =>
if should_inline x e1 e2
then nnrc_subst (
unshadow_simpl (
nnrc_free_vars e1)
e2)
x e1
else e
|
_ =>
e
end.
Lemma tinline_let_fun_correctness {
model:
basic_model} (
e:
nnrc) :
tnnrc_ext_rewrites_to e (
tinline_let_fun e).
Proof.
Definition tinline_let_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
let inline"
"
Inline let statements heuristically deemed suitable for inlining"
"
tinline_let_fun"
tinline_let_fun .
Definition tinline_let_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tinline_let_step tinline_let_fun_correctness.
Definition tfor_over_if_nil_fun {
fruntime:
foreign_runtime}(
e:
nnrc)
:=
match e with
|
NNRCFor x (
NNRCIf e1 e2 ‵{||})
ebody =>
(
NNRCIf e1 (
NNRCFor x e2 ebody) ‵{||})
|
_ =>
e
end.
Lemma tfor_over_if_nil_fun_correctness {
model:
basic_model} (
e:
nnrc) :
tnnrc_ext_rewrites_to e (
tfor_over_if_nil_fun e).
Proof.
Definition tfor_over_if_nil_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
for/
if/
else nil"
"
Push loop comprehension over an if statement through the if statement when the else clause just constructs an empty bag"
"
tfor_over_if_nil_fun"
tfor_over_if_nil_fun .
Definition tfor_over_if_nil_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tfor_over_if_nil_step tfor_over_if_nil_fun_correctness.
Definition tfor_over_either_nil_fun {
fruntime:
foreign_runtime} (
e:
nnrc)
:=
match e with
| (
NNRCFor x (
NNRCEither e1 xl el xr ‵{||})
ebody)
=>
(
let xl' :=
really_fresh_in nnrc_unshadow_sep xl (
nnrc_free_vars el ++
nnrc_bound_vars el)
ebody in
(
NNRCEither e1
xl' (
NNRCFor x (
nnrc_subst el xl (
NNRCVar xl'))
ebody)
xr ‵{||}))
|
_ =>
e
end.
Lemma tfor_over_either_nil_fun_correctness {
model:
basic_model} (
e:
nnrc) :
tnnrc_ext_rewrites_to e (
tfor_over_either_nil_fun e).
Proof.
Definition tfor_over_either_nil_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
for/
either/
right nil"
"
Push loop comprehension over an either statement through the either statement when the right clause just constructs an empty bag"
"
tfor_over_either_nil_fun"
tfor_over_either_nil_fun .
Definition tfor_over_either_nil_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tfor_over_either_nil_step tfor_over_either_nil_fun_correctness.
Definition tunop_over_either_const_fun {
fruntime:
foreign_runtime}(
e:
nnrc)
:=
match e with
|
NNRCUnop op (
NNRCEither e1 xl el xr (
NNRCConst d)) =>
NNRCEither e1 xl (
NNRCUnop op el)
xr (
NNRCUnop op (
NNRCConst d))
|
_ =>
e
end.
Lemma tunop_over_either_const_fun_correctness {
model:
basic_model} (
e:
nnrc) :
tnnrc_ext_rewrites_to e (
tunop_over_either_const_fun e).
Proof.
Definition tunop_over_either_const_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
unary/
either/
right const"
"
Push unary operators through either when the right branch is a constant"
"
tunop_over_either_const_fun"
tunop_over_either_const_fun .
Definition tunop_over_either_const_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tunop_over_either_const_step tunop_over_either_const_fun_correctness.
Definition tunop_over_if_const_fun {
fruntime:
foreign_runtime}(
e:
nnrc)
:=
match e with
|
NNRCUnop op (
NNRCIf e1 e2 (
NNRCConst d)) =>
NNRCIf e1 (
NNRCUnop op e2) (
NNRCUnop op (
NNRCConst d))
|
_ =>
e
end.
Lemma tunop_over_if_const_fun_correctness {
model:
basic_model} (
e:
nnrc) :
tnnrc_ext_rewrites_to e (
tunop_over_if_const_fun e).
Proof.
Definition tunop_over_if_const_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
unary/
if/
else const"
"
Push unary operators through if when the else branch is a constant"
"
tunop_over_if_const_fun"
tunop_over_if_const_fun .
Definition tunop_over_if_const_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tunop_over_if_const_step tunop_over_if_const_fun_correctness.
Definition tproject_nil_fun {
fruntime:
foreign_runtime} (
e:
nnrc) :=
match e with
|
NNRCUnop (
ARecProject nil)
e₁
=>
NNRCConst (
drec nil)
|
_ =>
e
end.
Definition tproject_nil_fun_correctness {
model:
basic_model}
p :
p ⇒ᶜ
tproject_nil_fun p.
Proof.
Hint Rewrite @
tproject_nil_fun_correctness :
toptim_correct.
Definition tproject_nil_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
project/
nil"
"
Simplify record projection over empty bags"
"
tproject_nil_fun"
tproject_nil_fun .
Definition tproject_nil_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tproject_nil_step tproject_nil_fun_correctness.
Definition tproject_over_const_fun {
fruntime:
foreign_runtime} (
e:
nnrc) :=
match e with
|
NNRCUnop (
ARecProject sl)
(
NNRCConst (
drec l))
=>
NNRCConst (
drec (
rproject l sl))
|
_ =>
e
end.
Definition tproject_over_const_fun_correctness {
model:
basic_model}
p :
p ⇒ᶜ
tproject_over_const_fun p.
Proof.
Hint Rewrite @
tproject_over_const_fun_correctness :
toptim_correct.
Definition tproject_over_const_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
project/
const rec"
"
Simplify record projection over constant records"
"
tproject_over_const_fun"
tproject_over_const_fun .
Definition tproject_over_const_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tproject_over_const_step tproject_over_const_fun_correctness.
Definition tproject_over_rec_fun {
fruntime:
foreign_runtime} (
e:
nnrc) :=
match e with
|
NNRCUnop (
ARecProject sl)
(
NNRCUnop (
ARec s)
p₁)
=>
if in_dec string_dec s sl
then NNRCUnop (
ARec s)
p₁
else ‵[||]
|
_ =>
e
end.
Definition tproject_over_rec_fun_correctness {
model:
basic_model}
p :
p ⇒ᶜ
tproject_over_rec_fun p.
Proof.
Hint Rewrite @
tproject_over_rec_fun_correctness :
toptim_correct.
Definition tproject_over_rec_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
project/
rec"
"
Simplify record projection over a record constructor"
"
tproject_over_rec_fun"
tproject_over_rec_fun .
Definition tproject_over_rec_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tproject_over_rec_step tproject_over_rec_fun_correctness.
Definition tproject_over_concat_r_fun {
fruntime:
foreign_runtime} (
e:
nnrc) :=
match e with
|
NNRCUnop (
ARecProject sl)
(
NNRCBinop AConcat
p₁ (
NNRCUnop (
ARec s)
p₂))
=>
if in_dec string_dec s sl
then NNRCBinop AConcat
(
NNRCUnop (
ARecProject (
remove string_dec s sl))
p₁)
(
NNRCUnop (
ARec s)
p₂)
else (
NNRCUnop (
ARecProject sl)
p₁)
|
_ =>
e
end.
Definition tproject_over_concat_r_fun_correctness {
model:
basic_model}
p :
p ⇒ᶜ
tproject_over_concat_r_fun p.
Proof.
Hint Rewrite @
tproject_over_concat_r_fun_correctness :
toptim_correct.
Definition tproject_over_concat_r_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
project/
concat/
right rec"
"
Simplify record projection over concatenation with a record constructor"
"
tproject_over_concat_r_fun"
tproject_over_concat_r_fun .
Definition tproject_over_concat_r_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tproject_over_concat_r_step tproject_over_concat_r_fun_correctness.
Definition tproject_over_concat_l_fun {
fruntime:
foreign_runtime} (
e:
nnrc) :=
match e with
|
NNRCUnop (
ARecProject sl)
(
NNRCBinop AConcat
(
NNRCUnop (
ARec s)
p₁)
p₂)
=>
if in_dec string_dec s sl
then e
else (
NNRCUnop (
ARecProject sl)
p₂)
|
_ =>
e
end.
Definition tproject_over_concat_l_fun_correctness {
model:
basic_model}
p :
p ⇒ᶜ
tproject_over_concat_l_fun p.
Proof.
Hint Rewrite @
tproject_over_concat_l_fun_correctness :
toptim_correct.
Definition tproject_over_concat_l_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
project/
concat/
left rec"
"
Simplify record projection over concatenation with a record constructor"
"
tproject_over_concat_l_fun"
tproject_over_concat_l_fun .
Definition tproject_over_concat_l_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tproject_over_concat_l_step tproject_over_concat_l_fun_correctness.
Definition tproject_over_project_fun {
fruntime:
foreign_runtime} (
e:
nnrc) :=
match e with
|
NNRCUnop (
ARecProject sl1)
(
NNRCUnop (
ARecProject sl2)
p1)
=>
NNRCUnop (
ARecProject (
set_inter string_dec sl2 sl1))
p1
|
_ =>
e
end.
Definition tproject_over_project_fun_correctness {
model:
basic_model}
p :
p ⇒ᶜ
tproject_over_project_fun p.
Proof.
Hint Rewrite @
tproject_over_project_fun_correctness :
toptim_correct.
Definition tproject_over_project_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
project/
project"
"
Fuse nested record projections"
"
tproject_over_project_fun"
tproject_over_project_fun .
Definition tproject_over_project_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tproject_over_project_step tproject_over_project_fun_correctness.
Definition tproject_over_either_fun {
fruntime:
foreign_runtime} (
e:
nnrc) :=
match e with
|
NNRCUnop (
ARecProject sl)
(
NNRCEither p xl p₁
xr p₂)
=>
NNRCEither p xl (
NNRCUnop (
ARecProject sl)
p₁)
xr (
NNRCUnop (
ARecProject sl)
p₂)
|
_ =>
e
end.
Definition tproject_over_either_fun_correctness {
model:
basic_model}
p :
p ⇒ᶜ
tproject_over_either_fun p.
Proof.
Hint Rewrite @
tproject_over_either_fun_correctness :
toptim_correct.
Definition tproject_over_either_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
project/
either/"
"
Push record projection through either"
"
tproject_over_either_fun"
tproject_over_either_fun .
Definition tproject_over_either_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tproject_over_either_step tproject_over_either_fun_correctness.
Definition tcount_over_flat_for_either_if_nil_fun {
fruntime:
foreign_runtime} (
e:
nnrc)
:=
match e with
| (♯
count(♯
flatten(
NNRCFor v
ehead (
NNRCEither e1 xl
(
NNRCIf e11(‵{|
e12|}) ‵{||})
xr ‵{||}))))
=> (♯
count(♯
flatten(
NNRCFor v
ehead (
NNRCEither e1 xl
(
NNRCIf e11(‵{| ‵(
dunit) |}) ‵{||})
xr ‵{||}))))
|
_ =>
e
end.
Lemma tcount_over_flat_for_either_if_nil_fun_correctness {
model:
basic_model} (
e:
nnrc) :
tnnrc_ext_rewrites_to e (
tcount_over_flat_for_either_if_nil_fun e).
Proof.
Definition tcount_over_flat_for_either_if_nil_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
count/
flatten/
for/
either/
right if/
else nil"
"
Remove work that is not needed when only the bag count is needed"
"
tcount_over_flat_for_either_if_nil_fun"
tcount_over_flat_for_either_if_nil_fun .
Definition tcount_over_flat_for_either_if_nil_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tcount_over_flat_for_either_if_nil_step tcount_over_flat_for_either_if_nil_fun_correctness.
Definition tcount_over_flat_for_either_either_nil_fun {
fruntime:
foreign_runtime}(
e:
nnrc)
:=
match e with
| (♯
count(♯
flatten(
NNRCFor v
ehead (
NNRCEither e1 xl
(
NNRCEither e11 xll (‵{|
e12|})
xrr ‵{||})
xr ‵{||}))))
=> (♯
count(♯
flatten(
NNRCFor v
ehead (
NNRCEither e1 xl
(
NNRCEither e11 xll (‵{| ‵(
dunit) |})
xrr ‵{||})
xr ‵{||}))))
|
_ =>
e
end.
Lemma tcount_over_flat_for_either_either_nil_fun_correctness {
model:
basic_model} (
e:
nnrc) :
tnnrc_ext_rewrites_to e (
tcount_over_flat_for_either_either_nil_fun e).
Proof.
Definition tcount_over_flat_for_either_either_nil_step {
fruntime:
foreign_runtime}
:=
mkOptimizerStep
"
count/
flatten/
for/
either/
right either/
right nil"
"
Remove work that is not needed when only the bag count is needed"
"
tcount_over_flat_for_either_either_nil_fun"
tcount_over_flat_for_either_either_nil_fun .
Definition tcount_over_flat_for_either_either_nil_step_correct {
model:
basic_model}
:=
mkOptimizerStepModel tcount_over_flat_for_either_either_nil_step tcount_over_flat_for_either_either_nil_fun_correctness.
Definition tnnrc_optim_list {
fruntime:
foreign_runtime} :
list (@
OptimizerStep nnrc)
:= [
tfor_nil_step
;
tfor_singleton_to_let_step
;
tflatten_singleton_step
;
tflatten_nil_step
;
tsigma_to_if_step
;
tmap_sigma_fusion_samevar_step
;
tdot_of_rec_step
;
tmerge_concat_to_concat_step
;
tdot_of_concat_rec_step
;
tinline_let_step
;
tfor_over_if_nil_step
;
tfor_over_either_nil_step
;
tunop_over_either_const_step
;
tunop_over_if_const_step
;
tproject_nil_step
;
tproject_over_const_step
;
tproject_over_rec_step
;
tproject_over_concat_r_step
;
tproject_over_concat_l_step
;
tproject_over_project_step
;
tproject_over_either_step
;
tcount_over_flat_for_either_if_nil_step
;
tcount_over_flat_for_either_either_nil_step
].
Definition tnnrc_optim_model_list {
model:
basic_model} :
list (
OptimizerStepModel tnnrc_ext_rewrites_to)
:= [
tfor_nil_step_correct
;
tfor_singleton_to_let_step_correct
;
tflatten_singleton_step_correct
;
tflatten_nil_step_correct
;
tsigma_to_if_step_correct
;
tmap_sigma_fusion_samevar_step_correct
;
tdot_of_rec_step_correct
;
tmerge_concat_to_concat_step_correct
;
tdot_of_concat_rec_step_correct
;
tinline_let_step_correct
;
tfor_over_if_nil_step_correct
;
tfor_over_either_nil_step_correct
;
tunop_over_either_const_step_correct
;
tunop_over_if_const_step_correct
;
tproject_nil_step_correct
;
tproject_over_const_step_correct
;
tproject_over_rec_step_correct
;
tproject_over_concat_r_step_correct
;
tproject_over_concat_l_step_correct
;
tproject_over_project_step_correct
;
tproject_over_either_step_correct
;
tcount_over_flat_for_either_if_nil_step_correct
;
tcount_over_flat_for_either_either_nil_step_correct
].
Lemma tnnrc_optim_model_list_complete {
model:
basic_model}
:
optim_model_list_complete tnnrc_optim_list tnnrc_optim_model_list.
Proof.
optim_correct_list_complete_prover.
Qed.
Definition tnnrc_optim_list_correct {
model:
basic_model}
:
optim_list_correct tnnrc_ext_rewrites_to tnnrc_optim_list
:=
optim_list_correct_from_model tnnrc_optim_model_list_complete.
Lemma tnnrc_optim_list_distinct {
fruntime:
foreign_runtime}:
optim_list_distinct tnnrc_optim_list.
Proof.
Definition run_nnrc_optims
{
fruntime:
foreign_runtime}
{
logger:
optimizer_logger string nnrc}
(
opc:
optim_phases_config)
:
nnrc ->
nnrc :=
run_phases tnnrc_map_deep NNRCSize.nnrc_size tnnrc_optim_list opc.
Lemma run_nnrc_optims_correctness
{
model:
basic_model} {
logger:
optimizer_logger string nnrc}
(
opc:
optim_phases_config)
(
p:
nnrc) :
tnnrc_ext_rewrites_to p (
run_nnrc_optims opc p).
Proof.
Section default.
Definition nnrc_default_optim_list {
fruntime:
foreign_runtime} :
list string
:= [
optim_step_name tinline_let_step
;
optim_step_name tcount_over_flat_for_either_either_nil_step
;
optim_step_name tcount_over_flat_for_either_if_nil_step
;
optim_step_name tmerge_concat_to_concat_step
;
optim_step_name tdot_of_concat_rec_step
;
optim_step_name tdot_of_rec_step
;
optim_step_name tflatten_singleton_step
;
optim_step_name tflatten_nil_step
;
optim_step_name tfor_singleton_to_let_step
;
optim_step_name tunop_over_either_const_step
;
optim_step_name tunop_over_if_const_step
;
optim_step_name tfor_over_either_nil_step
;
optim_step_name tfor_over_if_nil_step
;
optim_step_name tfor_nil_step
;
optim_step_name tmap_sigma_fusion_samevar_step
;
optim_step_name tproject_nil_step
;
optim_step_name tproject_over_const_step
;
optim_step_name tproject_over_rec_step
;
optim_step_name tproject_over_concat_r_step
;
optim_step_name tproject_over_concat_l_step
;
optim_step_name tproject_over_project_step
;
optim_step_name tproject_over_either_step
].
Remark nnrc_default_optim_list_all_valid {
fruntime:
foreign_runtime}
:
valid_optims tnnrc_optim_list nnrc_default_optim_list = (
nnrc_default_optim_list,
nil).
Proof.
vm_compute; trivial.
Qed.
Definition default_nnrc_optim_phases {
fruntime:
foreign_runtime} :=
("[
nnrc]
default"%
string,
nnrc_default_optim_list,10)::
nil.
End default.
Definition run_nnrc_optims_default
{
fruntime:
foreign_runtime} {
logger:
optimizer_logger string nnrc}
:=
run_nnrc_optims default_nnrc_optim_phases.
Lemma run_nnrc_optims_default_correct
{
model:
basic_model} {
logger:
optimizer_logger string nnrc}
p:
tnnrc_ext_rewrites_to p (
run_nnrc_optims_default p).
Proof.
End NNRCOptimizer.