Module ForeignOps

Section ForeignOp.

  Require Import EquivDec.

  Require Import Utils.
  Require Import RData.
  Require Import ForeignData.
  Require Import RDataNorm.
  Require Import BrandRelation.

    Class foreign_unary_op {fdata:foreign_data}
      : Type
    := mk_foreign_unary_op {
           foreign_unary_op_type : Set
           ; foreign_unary_op_dec :> EqDec foreign_unary_op_type eq
           ; foreign_unary_op_tostring :> ToString foreign_unary_op_type
           ; foreign_unary_op_interp
               (br:brand_relation_t)
               (op:foreign_unary_op_type)
               (d:data) : option data
           ; foreign_unary_op_normalized
               (br:brand_relation_t)
               (op:foreign_unary_op_type) (d o:data) :
               foreign_unary_op_interp br op d = Some o ->
               data_normalized br d ->
               data_normalized br o
         }.

    Class foreign_binary_op {fdata:foreign_data}
      : Type
    := mk_foreign_binary_op {
           foreign_binary_op_type : Set
           ; foreign_binary_op_dec :> EqDec foreign_binary_op_type eq
           ; foreign_binary_op_tostring :> ToString foreign_binary_op_type
           ; foreign_binary_op_interp
               (br:brand_relation_t)
               (op:foreign_binary_op_type)
               (d1 d2:data) : option data
           ; foreign_binary_op_normalized
               (br:brand_relation_t)
               (op:foreign_binary_op_type) (d1 d2 o:data) :
               foreign_binary_op_interp br op d1 d2 = Some o ->
               data_normalized br d1 ->
               data_normalized br d2 ->
               data_normalized br o
         }.

End ForeignOp.