Module Qcert.Data.Operators.ForeignOperators

Require Import EquivDec.
Require Import String.
Require Import Utils.
Require Import BrandRelation.
Require Import ForeignData.
Require Import Data.
Require Import DataNorm.

Section ForeignOperators.
  Class foreign_operators {fdata:foreign_data}
  : Type
    := mk_foreign_operators {
           foreign_operators_unary : Set
           ; foreign_operators_unary_dec :> EqDec foreign_operators_unary eq
           ; foreign_operators_unary_tostring :> ToString foreign_operators_unary
           ; foreign_operators_unary_interp
               (br:brand_relation_t)
               (op:foreign_operators_unary)
               (d:data) : option data
           ; foreign_operators_unary_normalized
               (br:brand_relation_t)
               (op:foreign_operators_unary) (d o:data) :
               foreign_operators_unary_interp br op d = Some o ->
               data_normalized br d ->
               data_normalized br o
           ; foreign_operators_binary : Set
           ; foreign_operators_binary_dec :> EqDec foreign_operators_binary eq
           ; foreign_operators_binary_tostring :> ToString foreign_operators_binary
           ; foreign_operators_binary_interp
               (br:brand_relation_t)
               (op:foreign_operators_binary)
               (d1 d2:data) : option data
           ; foreign_operators_binary_normalized
               (br:brand_relation_t)
               (op:foreign_operators_binary) (d1 d2 o:data) :
               foreign_operators_binary_interp br op d1 d2 = Some o ->
               data_normalized br d1 ->
               data_normalized br d2 ->
               data_normalized br o
           ; foreign_operators_unary_data_tostring : data -> string
           ; foreign_operators_unary_data_totext : data -> string
         }.

End ForeignOperators.