Qcert.NNRC.Optim.NNRCOptimizer

Section NNRCOptimizer.



  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:
    ∀ f: nnrc → nnrc,
    ∀ e: nnrc,
      (∀ e', nnrc_ext_eq (f e') e') → nnrc_ext_eq (nnrc_map f e) 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:
    ∀ f: nnrc → nnrc,
    ∀ e: nnrc,
      (∀ e', nnrc_ext_eq (f e') e') → nnrc_ext_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_ext_eq (head_rew e) e.

  Lemma rewriter_simpl_rew_no_free_var :
    ∀ (op : nnrc) (x : var),
      In x (nnrc_free_vars (head_rew op)) → In x (nnrc_free_vars op).

End NNRCOptimizer.