Qcert.NNRC.Optim.TNNRCOptimizer
Section TNNRCOptimizer.
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.
Lemma AUX {model:basic_model} f e e' :
(∀ e, tnnrc_ext_rewrites_to e (f e)) → tnnrc_ext_rewrites_to e e' → tnnrc_ext_rewrites_to e (f e').
Definition tnnrc_map {fruntime:foreign_runtime} := nnrc_map.
Lemma tnnrc_map_correctness {model:basic_model}:
∀ f: nnrc → nnrc,
∀ p: nnrc,
(∀ p', tnnrc_ext_rewrites_to p' (f p')) → tnnrc_ext_rewrites_to p (tnnrc_map f p).
Definition tnnrc_map_deep {fruntime:foreign_runtime} := NNRCOptimizer.nnrc_map_deep.
Lemma tnnrc_map_deep_correctness {model:basic_model}:
∀ f: nnrc → nnrc,
∀ p: nnrc,
(∀ p', tnnrc_ext_rewrites_to p' (f p')) → tnnrc_ext_rewrites_to p (tnnrc_map_deep f p).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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).
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.
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.
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.
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.
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.
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.
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.
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).
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).
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.
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.
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).
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).
Definition default_nnrc_optim_phases {fruntime:foreign_runtime} :=
("[nnrc] default"%string,nnrc_default_optim_list,10)::nil.
End default.
Definition trew_old
{fruntime:foreign_runtime} {logger:optimizer_logger string nnrc}
:= run_nnrc_optims default_nnrc_optim_phases.
Lemma trew_old_correctness
{model:basic_model} {logger:optimizer_logger string nnrc} p:
tnnrc_ext_rewrites_to p (trew_old p).
End TNNRCOptimizer.