Qcert.NNRC.Typing.TNNRCEq

Section TNNRCEq.





  Context {m:basic_model}.

  Definition tnnrc_ext_rewrites_to (e1 e2:nnrc) : Prop :=
    ∀ (τenv : tbindings) (τout:rtype),
      nnrc_ext_type τenv e1 τout →
      (nnrc_ext_type τenv e2 τout) ∧ (∀ (env:bindings),
                                     bindings_type env τenv → @nnrc_ext_eval _ brand_relation_brands env e1 = @nnrc_ext_eval _ brand_relation_brands env e2).

  Notation "e1 ⇒ᶜ e2" := (tnnrc_ext_rewrites_to e1 e2) (at level 80).


  Lemma data_normalized_bindings_type_map env τenv :
    bindings_type env τenv →
    Forall (data_normalized brand_relation_brands) (map snd env).


  Lemma nnrc_ext_rewrites_typed_with_untyped (e1 e2:nnrc) :
    e1 ≡ᶜ e2 →
    (∀ {τenv: tbindings} {τout:rtype}, nnrc_ext_type τenv e1 τout → nnrc_ext_type τenv e2 τout)
    → e1 ⇒ᶜ e2.





  Global Instance tnnrc_ext_rewrites_to_pre : PreOrder tnnrc_ext_rewrites_to.


  Global Instance nnrc_ext_var_tproper:
    Proper (eq ==> tnnrc_ext_rewrites_to) NNRCVar.


  Global Instance nnrc_ext_const_tproper:
    Proper (eq ==> tnnrc_ext_rewrites_to) NNRCConst.


  Global Instance nnrc_ext_binop_tproper:
    Proper (eq ==> tnnrc_ext_rewrites_to
               ==> tnnrc_ext_rewrites_to
               ==> tnnrc_ext_rewrites_to) NNRCBinop.


  Global Instance nnrc_ext_unop_tproper :
    Proper (eq ==> tnnrc_ext_rewrites_to ==> tnnrc_ext_rewrites_to) NNRCUnop.


  Global Instance nnrc_ext_let_tproper :
    Proper (eq ==> tnnrc_ext_rewrites_to ==> tnnrc_ext_rewrites_to ==> tnnrc_ext_rewrites_to) NNRCLet.



  Lemma dcoll_wt (l:list data) (τ:rtype) (τenv:tbindings) (env:bindings) (e:nnrc):
    bindings_type env τenv →
    nnrc_type τenv e (Coll τ) →
    nnrc_core_eval brand_relation_brands env e = Some (dcoll l) →
    ∀ x:data, In x l → (data_type x τ).

  Global Instance nnrc_ext_for_tproper :
    Proper (eq ==> tnnrc_ext_rewrites_to ==> tnnrc_ext_rewrites_to ==> tnnrc_ext_rewrites_to) NNRCFor.


  Global Instance nnrc_ext_if_tproper :
    Proper (tnnrc_ext_rewrites_to ==> tnnrc_ext_rewrites_to
                              ==> tnnrc_ext_rewrites_to
                              ==> tnnrc_ext_rewrites_to) NNRCIf.


  Global Instance nnrc_ext_either_tproper :
    Proper (tnnrc_ext_rewrites_to ==> eq ==> tnnrc_ext_rewrites_to
                              ==> eq ==> tnnrc_ext_rewrites_to
                              ==> tnnrc_ext_rewrites_to) NNRCEither.


  Lemma group_by_macro_eq g sl n1 n2 :
    NNRCGroupBy g sl n1 ⇒ᶜ NNRCGroupBy g sl n2
    ↔ nnrc_group_by g sl n1 ⇒ᶜ nnrc_group_by g sl n2.

  Global Instance nnrc_ext_groupby_tproper :
    Proper (eq ==> eq ==> tnnrc_ext_rewrites_to ==> tnnrc_ext_rewrites_to) NNRCGroupBy.

End TNNRCEq.

Notation "e1 ⇒ᶜ e2" := (tnnrc_ext_rewrites_to e1 e2) (at level 80).