Module ForeignToReduceOps

Section ForeignToReduceOps.
  Require Import EquivDec.
  Require Import Utils.
  Require Import BasicRuntime.
  Require Import NNRCMRRuntime.

  Class foreign_to_reduce_op
        {fruntime:foreign_runtime}
        {fredop:foreign_reduce_op}
      : Type
      := mk_foreign_to_reduce_op {
             foreign_to_reduce_op_of_unary_op
               (uop:unaryOp) : option reduce_op
             ; foreign_to_reduce_op_of_unary_op_correct
                 (uop:unaryOp) (rop:reduce_op)
                 (br:brand_relation_t)
                 (dl:list data) :
                 foreign_to_reduce_op_of_unary_op uop = Some rop ->
                 fun_of_unaryop br uop (dcoll dl) =
                 reduce_op_eval br rop dl
             ; foreign_to_reduce_op_to_unary_op
               (uop:reduce_op) : option unaryOp
             ; foreign_to_reduce_op_to_unary_op_correct
                 (rop:reduce_op) (uop:unaryOp)
                 (br:brand_relation_t)
                 (dl:list data) :
                 foreign_to_reduce_op_to_unary_op rop = Some uop ->
                 reduce_op_eval br rop dl =
                 fun_of_unaryop br uop (dcoll dl)
         }.

End ForeignToReduceOps.