Qcert.Basic.Typing.TOpsEq

Section TOpsEq.




    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 :=
    ∀ (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 τ₁ τ₂ →
    (∀ (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 :=
    ∀ (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 τ₁ τ₂ τ₃ ∧
    (∀ (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.