Qcert.DNNRC.Lang.DNNRCEq

Section DNNRCEq.



  Context {fruntime:foreign_runtime}.
  Context {A plug_type:Set}.
  Context {eqdec:EqDec A eq}.
  Context {plug:AlgPlug plug_type}.

  Definition dnnrc_eq (e1 e2:dnnrc A plug_type) : Prop :=
    ∀ (h:brand_relation_t) (denv:dbindings),
      Forall (ddata_normalized h) (map snd denv) →
      dnnrc_eval h denv e1 = dnnrc_eval h denv e2.

  Global Instance dnnrc_equiv : Equivalence dnnrc_eq.


  Global Instance dvar_proper : Proper (eq ==> eq ==> dnnrc_eq) DNNRCVar.


  Global Instance dconst_proper : Proper (eq ==> eq ==> dnnrc_eq) DNNRCConst.


  Global Instance dbinop_proper : Proper (eq ==> binop_eq ==> dnnrc_eq ==> dnnrc_eq ==> dnnrc_eq) DNNRCBinop.


  Global Instance dunop_proper : Proper (eq ==> unaryop_eq ==> dnnrc_eq ==> dnnrc_eq) DNNRCUnop.


  Global Instance dlet_proper : Proper (eq ==> eq ==> dnnrc_eq ==> dnnrc_eq ==> dnnrc_eq) DNNRCLet.



  Global Instance dfor_proper : Proper (eq ==> eq ==> dnnrc_eq ==> dnnrc_eq ==> dnnrc_eq) DNNRCFor.
  Global Instance dif_proper : Proper (eq ==> dnnrc_eq ==> dnnrc_eq ==> dnnrc_eq ==> dnnrc_eq) DNNRCIf.

  Global Instance deither_proper : Proper (eq ==> dnnrc_eq ==> eq ==> dnnrc_eq ==> eq ==> dnnrc_eq ==> dnnrc_eq) DNNRCEither.

  Global Instance dgroupby_proper : Proper (eq ==> eq ==> eq ==> dnnrc_eq ==>dnnrc_eq) DNNRCGroupBy.

  Global Instance dcollect_proper : Proper (eq ==> dnnrc_eq ==> dnnrc_eq) DNNRCCollect.

  Global Instance ddispatch_proper : Proper (eq ==> dnnrc_eq ==> dnnrc_eq) DNNRCDispatch.

  Global Instance dalg_proper : Proper (eq ==> eq ==> Forall2 (fun n1 n2 ⇒ fst n1 = fst n2 ∧ dnnrc_eq (snd n1) (snd n2)) ==> dnnrc_eq) DNNRCAlg.

End DNNRCEq.

Notation "X ≡ᵈ Y" := (dnnrc_eq X Y) (at level 90) : dnnrc_scope.