Module Qcert.NNRC.Lang.NNRCEq

Require Import Equivalence.
Require Import Morphisms.
Require Import Setoid.
Require Import EquivDec.
Require Import Program.
Require Import String.
Require Import List.
Require Import Arith.
Require Import DataRuntime.
Require Import cNNRC.
Require Import cNNRCNorm.
Require Import cNNRCEq.
Require Import NNRC.

Section NNRCEq.
  Context {fruntime:foreign_runtime}.


  Definition nnrc_eq (e1 e2:nnrc) : Prop :=
    forall (h:brand_relation_t),
    forall (cenv:bindings),
    forall (env:bindings),
      Forall (data_normalized h) (map snd cenv) ->
      Forall (data_normalized h) (map snd env) ->
      @nnrc_eval _ h cenv env e1 = @nnrc_eval _ h cenv env e2.

  Global Instance nnrc_equiv : Equivalence nnrc_eq.


  Global Instance proper_NNRCGetConstant : Proper (eq ==> nnrc_eq) NNRCGetConstant.

  Global Instance proper_NNRCVar : Proper (eq ==> nnrc_eq) NNRCVar.

  Global Instance proper_NNRCConst : Proper (eq ==> nnrc_eq) NNRCConst.

  
  Global Instance proper_NNRCBinop : Proper (binary_op_eq ==> nnrc_eq ==> nnrc_eq ==> nnrc_eq) NNRCBinop.


  Global Instance proper_NNRCUnnop : Proper (unary_op_eq ==> nnrc_eq ==> nnrc_eq) NNRCUnop.
    
  
  Global Instance proper_NNRCLet : Proper (eq ==> nnrc_eq ==> nnrc_eq ==> nnrc_eq) NNRCLet.


  Global Instance proper_NNRCFor : Proper (eq ==> nnrc_eq ==> nnrc_eq ==> nnrc_eq) NNRCFor.

  
  Global Instance proper_NNRCIf : Proper (nnrc_eq ==> nnrc_eq ==> nnrc_eq ==> nnrc_eq) NNRCIf.

  Global Instance proper_NNRCEither : Proper (nnrc_eq ==> eq ==> nnrc_eq ==> eq ==> nnrc_eq ==> nnrc_eq) NNRCEither.

  Global Instance proper_NNRCGroupBy : Proper (eq ==> eq ==> nnrc_eq ==> nnrc_eq) NNRCGroupBy.

End NNRCEq.

Notation "X ≡ᶜ Y" := (nnrc_eq X Y) (at level 90) : nnrc_scope.