Module TOpsEq

Section TOpsEq.

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

  Require Import List.
  Require Import String.

  Require Import Utils Types BasicRuntime.
  Require Import ForeignDataTyping ForeignOpsTyping.
  Require Import TData TOps.

    Context {fdata:foreign_data}.
    Context {fuop:foreign_unary_op}.
    Context {fbop:foreign_binary_op}.
    Context {ftype:foreign_type}.
    Context {fdtyping:foreign_data_typing}.
    Context {m:brand_model}.
    Context {fuoptyping:foreign_unary_op_typing}.
    Context {fboptyping:foreign_binary_op_typing}.

  Definition typed_unaryOp τin τout := {u:unaryOp|unaryOp_type u τin τout}.

  Definition tunaryop_eq {τin τout} (uop1 uop2:typed_unaryOp τin τout) : Prop :=
    forall (x:data), data_type x τin -> (fun_of_unaryop brand_relation_brands (`uop1)) x = (fun_of_unaryop brand_relation_brands (`uop2)) x.
  
  Global Instance tunaryop_equiv {τin τout} : Equivalence (@tunaryop_eq τin τout).

  Definition tunaryOp_rewrites_to {τ₁ τ₂} (u1 u2:unaryOp) :=
    unaryOp_type u1 τ₁ τ₂ ->
    unaryOp_type u2 τ₁ τ₂ ->
    (forall (x:data), data_type x τ₁ -> (fun_of_unaryop brand_relation_brands u1) x = (fun_of_unaryop brand_relation_brands u2) x).
  
  Definition typed_binOp τ₁ τ₂ τout := {b:binOp|binOp_type b τ₁ τ₂ τout}.

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

  Global Instance tbinop_equiv {τ₁ τ₂ τout} : Equivalence (@tbinop_eq τ₁ τ₂ τout).

  Definition tbinaryOp_rewrites_to {τ₁ τ₂ τ₃} (b1 b2:binOp) :=
    binOp_type b1 τ₁ τ₂ τ₃ ->
    binOp_type b2 τ₁ τ₂ τ₃ /\
    (forall (x1 x2:data), data_type x1 τ₁ -> data_type x2 τ₂ ->
                          (fun_of_binop brand_relation_brands b1) x1 x2 = (fun_of_binop brand_relation_brands b2) x1 x2).

End TOpsEq.