Module ROpsEq

Section ROpsEq.

  Require Import Equivalence.
  Require Import Morphisms.
  Require Import Setoid.
  Require Import EquivDec.
  Require Import Program.
  Require Import List.
  Require Import String.

  Require Import Utils.
  Require Import BrandRelation.
  Require Import RData RDataNorm RRelation.
  Require Import RUtilOps RBinaryOpsSem RUnaryOpsSem.
  Require Import ForeignData.
  Require Import ForeignOps.

  Context {fdata:foreign_data}.
  Context {fuop:foreign_unary_op}.
  Context {fbop:foreign_binary_op}.


  Definition unaryop_eq (uop1 uop2:unaryOp) : Prop :=
    forall (h:list (string*string)),
    forall (x:data),
      data_normalized h x ->
      (fun_of_unaryop h uop1) x = (fun_of_unaryop h uop2) x.

  Global Instance unaryop_equiv : Equivalence unaryop_eq.

  Definition binop_eq (bop1 bop2:binOp) : Prop :=
    forall (h:list (string*string)),
    forall (x:data),
      data_normalized h x ->
      forall (y:data),
        data_normalized h x ->
        (fun_of_binop h bop1) x y = (fun_of_binop h bop2) x y.

  Global Instance binop_equiv : Equivalence binop_eq.

End ROpsEq.