Module Qcert.NNRC.Optim.NNRCOptimizer

Require Import String.
Require Import List.
Require Import ListSet.
Require Import BinInt.
Require Import Arith.
Require Import Equivalence.
Require Import Morphisms.
Require Import Setoid.
Require Import EquivDec.
Require Import Program.
Require Import Utils.
Require Import DataSystem.
Require Import cNNRCSystem.
Require Import NNRCSystem.
Require Import NNRCRewriteUtil.
Require Import NNRCRewrite.
Require Import TNNRCRewrite.
Require Import OptimizerLogger.
Require Import OptimizerStep.

Import ListNotations.
Local Open Scope list_scope.

Section NNRCOptimizer.
  Local Open Scope nnrc_scope.
  Local Open Scope string.

  Section engine.
    Context {fruntime:foreign_runtime}.

    Definition nnrc_map (f: nnrc -> nnrc) (e:nnrc) :=
      match e with
      | NNRCGetConstant v => NNRCGetConstant v
      | 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_eq (f e') e') -> nnrc_eq (nnrc_map f e) e.

    Fixpoint nnrc_map_deep (f: nnrc -> nnrc) (e: nnrc) :=
      match e with
      | NNRCGetConstant v => f (NNRCGetConstant v)
      | 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_eq (f e') e') -> nnrc_eq (nnrc_map_deep f e) e.



    Definition nunshadow := unshadow_simpl nil.
  
    Definition head_rew (e: nnrc) :=
      (nunshadow e).
    
    Lemma head_rew_correctness e:
      nnrc_eq (head_rew e) e.

    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).

  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_rewrites_to_trans {model:basic_model} e1 e2 e3:
    tnnrc_rewrites_to e1 e2 -> tnnrc_rewrites_to e2 e3 -> tnnrc_rewrites_to e1 e3.

  Lemma AUX {model:basic_model} f e e' :
    (forall e, tnnrc_rewrites_to e (f e)) -> tnnrc_rewrites_to e e' -> tnnrc_rewrites_to e (f e').

  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_rewrites_to p' (f p')) -> tnnrc_rewrites_to p (tnnrc_map f p).

  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_rewrites_to p' (f p')) -> tnnrc_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_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 tconcat_nil_fun {fruntime:foreign_runtime}(e:nnrc) :=
    match e with
    | NNRCBinop OpRecConcat (NNRCConst (drec nil)) ee => ee
    | NNRCBinop OpRecConcat ee (NNRCConst (drec nil)) => ee
    | _ => e
    end.
  
  Lemma tconcat_nil_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tconcat_nil_fun e).

  Definition tconcat_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "concat/nil"
         "Remove record concatenation with an empty bag"
         "tconcat_nil_fun"
         tconcat_nil_fun .

  Definition tconcat_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tconcat_nil_step tconcat_nil_fun_correctness.

  Definition tmerge_nil_fun {fruntime:foreign_runtime}(e:nnrc) :=
    match e with
    | NNRCBinop OpRecMerge (NNRCConst (drec nil)) ee => NNRCUnop OpBag ee
    | NNRCBinop OpRecMerge ee (NNRCConst (drec nil)) => NNRCUnop OpBag ee
    | _ => e
    end.
  
  Lemma tmerge_nil_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tmerge_nil_fun e).

  Definition tmerge_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "merge/nil"
         "Remove record merge with an empty bag"
         "tmerge_nil_fun"
         tmerge_nil_fun .

  Definition tmerge_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tmerge_nil_step tmerge_nil_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_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 OpBag e1) e2
      => NNRCUnop OpBag (NNRCLet x e1 e2)
    | _ => e
    end.

  Lemma tfor_singleton_to_let_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_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_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_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 OpFlatten
                 (NNRCFor v1 (NNRCUnop OpBag e2)
                         (NNRCIf e1
                                (NNRCUnop OpBag (NNRCVar v2))
                                (NNRCConst (dcoll nil))))) =>
        if (v1 == v2)
        then (NNRCLet v1 e2 (NNRCIf e1 (NNRCUnop OpBag (NNRCVar v1)) (NNRCConst (dcoll nil))))
        else e
      | _ => e
    end.


  Lemma tsigma_to_if_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_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 OpFlatten
                         (NNRCFor v1 e1
                                 (NNRCIf e2 (NNRCUnop OpBag ee) (NNRCConst (dcoll nil)))))
                e3) =>
          if (v1 == v2)
          then
            (NNRCUnop OpFlatten
                     (NNRCFor v1 e1
                             (NNRCIf e2
                                    (NNRCUnop OpBag (NNRCLet v1 ee e3))
                                    (NNRCConst (dcoll nil)))))
        else e
      | _ => e
    end.

  Lemma tmap_sigma_fusion_samevar_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_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 (OpDot s1)
                (NNRCUnop (OpRec s2) e1)) =>
        if (s1 == s2)
        then e1
        else e
      | _ => e
    end.

  Lemma tdot_of_rec_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_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 tnth0_bag_fun {fruntime:foreign_runtime}(e:nnrc) :=
    match e with
      | (NNRCBinop OpBagNth (NNRCUnop OpBag e) (NNRCConst (dnat 0))) =>
        NNRCUnop OpLeft e
      | _ => e
    end.

  Lemma tnth0_bag_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tnth0_bag_fun e).

  Definition tnth0_bag_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "nth0/bag"
         "Simplify first element of a collection with one element"
         "tnth0_bag_fun"
         tnth0_bag_fun .

  Definition tnth0_bag_step_correct {model:basic_model}
    := mkOptimizerStepModel tnth0_bag_step tnth0_bag_fun_correctness.

  Definition tnth0_nil_fun {fruntime:foreign_runtime}(e:nnrc) :=
    match e with
      | NNRCBinop OpBagNth (NNRCConst (dcoll nil)) (NNRCConst (dnat 0)) =>
        NNRCConst dnone
      | _ => e
    end.

  Lemma tnth0_nil_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tnth0_nil_fun e).

  Definition tnth0_nil_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "nth0/nil"
         "Simplify first element of an empty collection"
         "tnth0_nil_fun"
         tnth0_nil_fun .

  Definition tnth0_nil_step_correct {model:basic_model}
    := mkOptimizerStepModel tnth0_nil_step tnth0_nil_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_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 (OpDot s) (NNRCBinop OpRecConcat e1 (NNRCUnop (OpRec s2) e2)))
         => if equiv_decb s s2
            then e2
            else (NNRCUnop (OpDot s) e1)
       | _ => e
       end.

  Lemma tdot_of_concat_rec_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_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.


  Definition is_small_unop {fruntime:foreign_runtime} (u:unary_op) :=
    match u with
    | OpIdentity
    | OpNeg
    | OpBag
    | OpLeft
    | OpRight
    | OpBrand _
    | OpRec _
      => 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 OpRecConcat (NNRCUnop (OpRec _) e1) (NNRCUnop (OpRec _) 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_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_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 tloop_fusion_fun {fruntime:foreign_runtime}(e:nnrc)
      := match e with
         | NNRCFor x (NNRCFor y source body1) body2 =>
           if (in_dec string_dec y (nnrc_free_vars body2))
           then let fr := really_fresh_in
                     nnrc_unshadow_sep y (nnrc_free_vars body1 ++ nnrc_bound_vars body1) body2
                in NNRCFor fr source
                     (NNRCLet x (nnrc_subst body1 y (NNRCVar fr)) body2)
           else NNRCFor y source
                        (NNRCLet x body1 body2)
       | _ => e
       end.

  Lemma tloop_fusion_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tloop_fusion_fun e).

  Definition tloop_fusion_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "for/for"
         "Fuse nested loop comprehensions"
         "tloop_fusion_fun"
         tloop_fusion_fun .

  Definition tloop_fusion_step_correct {model:basic_model}
    := mkOptimizerStepModel tloop_fusion_step tloop_fusion_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_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_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_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 tbinop_over_if_left_const_fun {fruntime:foreign_runtime}(e:nnrc)
    := match e with
       | NNRCBinop op (NNRCIf e1 e2 (NNRCConst d)) e =>
         NNRCIf e1 (NNRCBinop op e2 e) (NNRCBinop op (NNRCConst d) e)
       | _ => e
       end.

  Lemma tbinop_over_if_left_const_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tbinop_over_if_left_const_fun e).

  Definition tbinop_over_if_left_const_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "binary/if/else const"
         "Push binary operators through if when the else branch is a constant"
         "tbinop_over_if_left_const_fun"
         tbinop_over_if_left_const_fun .

  Definition tbinop_over_if_left_const_step_correct {model:basic_model}
    := mkOptimizerStepModel tbinop_over_if_left_const_step tbinop_over_if_left_const_fun_correctness.


  Definition tbinop_over_let_left_const_fun {fruntime:foreign_runtime}(e:nnrc)
    := match e with
       | NNRCBinop op (NNRCLet x e1 e2) (NNRCConst d) =>
         NNRCLet x e1 (NNRCBinop op e2 (NNRCConst d))
       | _ => e
       end.

  Lemma tbinop_over_let_left_const_fun_correctness {model:basic_model} (e:nnrc) :
    tnnrc_rewrites_to e (tbinop_over_let_left_const_fun e).

  Definition tbinop_over_let_left_const_step {fruntime:foreign_runtime}
    := mkOptimizerStep
         "binary/let/const"
         "Push binary operators through let when the right expression is a constant"
         "tbinop_over_let_left_const_fun"
         tbinop_over_let_left_const_fun .

  Definition tbinop_over_let_left_const_step_correct {model:basic_model}
    := mkOptimizerStepModel tbinop_over_let_left_const_step tbinop_over_let_left_const_fun_correctness.


   Definition tproject_nil_fun {fruntime:foreign_runtime} (e:nnrc) :=
    match e with
      | NNRCUnop (OpRecProject nil) e₁
        => NNRCConst (drec nil)
      | _ => e
    end.

  Definition tproject_nil_fun_correctness {model:basic_model} p :
    p ⇒ᶜ tproject_nil_fun p.

  Local 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 (OpRecProject 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.

  Local 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 (OpRecProject sl)
          (NNRCUnop (OpRec s) p₁)
        => if in_dec string_dec s sl
           then NNRCUnop (OpRec s) p₁
           else ‵[||]
      | _ => e
    end.

  Definition tproject_over_rec_fun_correctness {model:basic_model} p :
    p ⇒ᶜ tproject_over_rec_fun p.

  Local 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 (OpRecProject sl)
               (NNRCBinop OpRecConcat
                        p₁ (NNRCUnop (OpRec s) p₂))
        => if in_dec string_dec s sl
           then NNRCBinop OpRecConcat
                         (NNRCUnop (OpRecProject (remove string_dec s sl)) p₁)
                        (NNRCUnop (OpRec s) p₂)
           else (NNRCUnop (OpRecProject sl) p₁)
      | _ => e
    end.

  Definition tproject_over_concat_r_fun_correctness {model:basic_model} p :
    p ⇒ᶜ tproject_over_concat_r_fun p.
                  
  Local 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 (OpRecProject sl)
               (NNRCBinop OpRecConcat
                        (NNRCUnop (OpRec s) p₁) p₂)
        => if in_dec string_dec s sl

           then e
           else (NNRCUnop (OpRecProject sl) p₂)
      | _ => e
    end.

  Definition tproject_over_concat_l_fun_correctness {model:basic_model} p :
    p ⇒ᶜ tproject_over_concat_l_fun p.
                  
  Local 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 (OpRecProject sl1)
          (NNRCUnop (OpRecProject sl2) p1)
        => NNRCUnop (OpRecProject (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.

  Local 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 (OpRecProject sl)
          (NNRCEither p xl p₁ xr p₂)
        => NNRCEither p xl (NNRCUnop (OpRecProject sl) p₁) xr (NNRCUnop (OpRecProject sl) p₂)
      | _ => e
    end.

  Definition tproject_over_either_fun_correctness {model:basic_model} p :
    p ⇒ᶜ tproject_over_either_fun p.

  Local 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_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_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)
      := [
          tconcat_nil_step
          ; tmerge_nil_step
          ; 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
          ; tnth0_bag_step
          ; tnth0_nil_step
          ; tmerge_concat_to_concat_step
          ; tdot_of_concat_rec_step
          ; tinline_let_step
          ; tfor_over_if_nil_step
          ; tloop_fusion_step
          ; tfor_over_either_nil_step
          ; tunop_over_either_const_step
          ; tunop_over_if_const_step
          ; tbinop_over_if_left_const_step
          ; tbinop_over_let_left_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_rewrites_to)
      := [
          tconcat_nil_step_correct
          ; tmerge_nil_step_correct
          ; 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
          ; tnth0_bag_step_correct
          ; tnth0_nil_step_correct
          ; tmerge_concat_to_concat_step_correct
          ; tdot_of_concat_rec_step_correct
          ; tinline_let_step_correct
          ; tfor_over_if_nil_step_correct
          ; tloop_fusion_step_correct
          ; tfor_over_either_nil_step_correct
          ; tunop_over_either_const_step_correct
          ; tunop_over_if_const_step_correct
          ; tbinop_over_if_left_const_step_correct
          ; tbinop_over_let_left_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_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 nnrc_optim_top
             {fruntime:foreign_runtime}
             {logger:optimizer_logger string nnrc}
             (opc:optim_phases_config)
    : nnrc -> nnrc :=
    run_phases tnnrc_map_deep nnrc_size tnnrc_optim_list opc.

  Lemma nnrc_optim_top_correctness
        {model:basic_model} {logger:optimizer_logger string nnrc}
        (opc:optim_phases_config)
        (p:nnrc) :
    tnnrc_rewrites_to p (nnrc_optim_top 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 tnth0_bag_step
        ; optim_step_name tnth0_nil_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 tbinop_over_if_left_const_step
        ; optim_step_name tbinop_over_let_left_const_step
        ; optim_step_name tfor_over_either_nil_step
        ; optim_step_name tloop_fusion_step
        ; optim_step_name tfor_over_if_nil_step
        ; optim_step_name tfor_nil_step
        ; optim_step_name tmerge_nil_step
        ; optim_step_name tconcat_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 nnrc_optim_top_default
             {fruntime:foreign_runtime} {logger:optimizer_logger string nnrc}
    := nnrc_optim_top default_nnrc_optim_phases.

  Lemma nnrc_optim_top_default_correct
        {model:basic_model} {logger:optimizer_logger string nnrc} p:
    tnnrc_rewrites_to p (nnrc_optim_top_default p).

End NNRCOptimizer.