Module Qcert.Data.OperatorsTyping.TOperatorsEq

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 Types.
Require Import DataModel.
Require Import ForeignData.
Require Import ForeignOperators.
Require Import ForeignDataTyping.
Require Import ForeignOperatorsTyping.
Require Import Operators.
Require Import TData.
Require Import TUnaryOperators.
Require Import TBinaryOperators.

Section TOperatorsEq.
  Context {fdata:foreign_data}.
  Context {foperators:foreign_operators}.
  Context {ftype:foreign_type}.
  Context {fdtyping:foreign_data_typing}.
  Context {m:brand_model}.
  Context {foptyping:foreign_operators_typing}.

  Definition typed_unary_op τin τout := {u:unary_op|unary_op_type u τin τout}.

  Definition tunary_op_eq {τin τout} (uop1 uop2:typed_unary_op τin τout) : Prop :=
    forall (x:data),
      data_type x τin ->
      (unary_op_eval brand_relation_brands (`uop1)) x
      = (unary_op_eval brand_relation_brands (`uop2)) x.
  
  Global Instance tunary_op_equiv {τin τout} : Equivalence (@tunary_op_eq τin τout).

  Definition tunary_op_rewrites_to (u1 u2:unary_op) :=
    forall τ₁ τ₂,
    unary_op_type u1 τ₁ τ₂ ->
    unary_op_type u2 τ₁ τ₂ /\
    (forall (x:data),
        data_type x τ₁ ->
        (unary_op_eval brand_relation_brands u1) x
        = (unary_op_eval brand_relation_brands u2) x).

  Global Instance tunary_op_rewrites_to_pre : PreOrder tunary_op_rewrites_to.
  
  Definition typed_binary_op τ₁ τ₂ τout := {b:binary_op|binary_op_type b τ₁ τ₂ τout}.

  Definition tbinary_op_eq {τ₁ τ₂ τout} (bop1 bop2:typed_binary_op τ₁ τ₂ τout) : Prop :=
    forall (x1 x2:data),
      data_type x1 τ₁ -> data_type x2 τ₂ ->
      (binary_op_eval brand_relation_brands (`bop1)) x1 x2
      = (binary_op_eval brand_relation_brands (`bop2)) x1 x2.

  Global Instance tbinary_op_equiv {τ₁ τ₂ τout} : Equivalence (@tbinary_op_eq τ₁ τ₂ τout).

  Definition tbinary_op_rewrites_to (b1 b2:binary_op) :=
    forall τ₁ τ₂ τ₃,
    binary_op_type b1 τ₁ τ₂ τ₃ ->
    binary_op_type b2 τ₁ τ₂ τ₃ /\
    (forall (x1 x2:data),
        data_type x1 τ₁ ->
        data_type x2 τ₂ ->
        (binary_op_eval brand_relation_brands b1) x1 x2
        = (binary_op_eval brand_relation_brands b2) x1 x2).

  Global Instance tbinary_op_rewrites_to_pre : PreOrder tbinary_op_rewrites_to.
  
End TOperatorsEq.