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 eis_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
       | UsedOncetrue
       | _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.