Module Qcert.Data.Operators.OperatorsEq

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 ForeignData.
Require Import Data.
Require Import DataNorm.
Require Import Iterators.
Require Import OperatorsUtils.
Require Import ForeignOperators.
Require Import BinaryOperatorsSem.
Require Import UnaryOperatorsSem.

Section OperatorsEq.
  Context {fdata:foreign_data}.
  Context {foperators:foreign_operators}.


  Definition unary_op_eq (uop1 uop2:unary_op) : Prop :=
    forall (h:list (string*string)),
    forall (x:data),
      data_normalized h x ->
      (unary_op_eval h uop1) x = (unary_op_eval h uop2) x.

  Global Instance unary_op_equiv : Equivalence unary_op_eq.

  Definition binary_op_eq (bop1 bop2:binary_op) : Prop :=
    forall (h:list (string*string)),
    forall (x:data),
      data_normalized h x ->
      forall (y:data),
        data_normalized h x ->
        (binary_op_eval h bop1) x y = (binary_op_eval h bop2) x y.

  Global Instance binary_op_equiv : Equivalence binary_op_eq.

End OperatorsEq.