Qcert.NNRC.Typing.TcNNRCEq

Section TcNNRCEq.





  Context {m:basic_model}.

  Definition tnnrc_rewrites_to (e1 e2:nnrc) : Prop :=
    ∀ (τenv : tbindings) (τout:rtype),
      nnrc_type τenv e1 τout →
      (nnrc_type τenv e2 τout) ∧ (∀ (env:bindings),
                                     bindings_type env τenv → nnrc_core_eval brand_relation_brands env e1 = nnrc_core_eval brand_relation_brands env e2).

  Notation "e1 ⇒ᶜᶜ e2" := (tnnrc_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_rewrites_typed_with_untyped (e1 e2:nnrc) :
    e1 ≡ᶜᶜ e2 →
    (∀ {τenv: tbindings} {τout:rtype}, nnrc_type τenv e1 τout → nnrc_type τenv e2 τout)
    → e1 ⇒ᶜᶜ e2.





  Global Instance tnnrc_rewrites_to_pre : PreOrder tnnrc_rewrites_to.


  Global Instance nnrcvar_tproper:
    Proper (eq ==> tnnrc_rewrites_to) NNRCVar.


  Global Instance nnrcconst_tproper:
    Proper (eq ==> tnnrc_rewrites_to) NNRCConst.


  Global Instance nnrcbinop_tproper:
    Proper (eq ==> tnnrc_rewrites_to
               ==> tnnrc_rewrites_to
               ==> tnnrc_rewrites_to) NNRCBinop.


  Global Instance nnrcunop_tproper :
    Proper (eq ==> tnnrc_rewrites_to ==> tnnrc_rewrites_to) NNRCUnop.


  Global Instance nnrclet_tproper :
    Proper (eq ==> tnnrc_rewrites_to ==> tnnrc_rewrites_to ==> tnnrc_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 nnrcfor_tproper :
    Proper (eq ==> tnnrc_rewrites_to ==> tnnrc_rewrites_to ==> tnnrc_rewrites_to) NNRCFor.


  Global Instance nnrcif_tproper :
    Proper (tnnrc_rewrites_to ==> tnnrc_rewrites_to
                             ==> tnnrc_rewrites_to
                             ==> tnnrc_rewrites_to) NNRCIf.

  Global Instance nnrceither_tproper :
    Proper (tnnrc_rewrites_to ==> eq ==> tnnrc_rewrites_to ==> eq ==> tnnrc_rewrites_to ==> tnnrc_rewrites_to) NNRCEither.

End TcNNRCEq.

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