Module Qcert.NNRCMR.Lang.ForeignReduceOps

Require Import EquivDec.
Require Import List.
Require Import Utils.
Require Import DataRuntime.

Section ForeignReduceOps.
  Class foreign_reduce_op {fdata:foreign_data}
  : Type
    := mk_foreign_reduce_op {
           foreign_reduce_op_type : Set
           ; foreign_reduce_op_dec :> EqDec foreign_reduce_op_type eq
           ; foreign_reduce_op_tostring :> ToString foreign_reduce_op_type
           ; foreign_reduce_op_interp
               (br:brand_relation_t)
               (op:foreign_reduce_op_type)
               (dl:list data) : option data
           ; foreign_reduce_op_normalized
               (br:brand_relation_t)
               (op:foreign_reduce_op_type) (dl:list data) (o:data) :
               foreign_reduce_op_interp br op dl = Some o ->
               Forall (data_normalized br) dl ->
               data_normalized br o
         }.

End ForeignReduceOps.