Module Qcert.Translation.Operators.ForeignToReduceOps

Require Import EquivDec.
Require Import Utils.
Require Import DataRuntime.
Require Import NNRCMRRuntime.

Section ForeignToReduceOps.
  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:unary_op) : option reduce_op
             ; foreign_to_reduce_op_of_unary_op_correct
                 (uop:unary_op) (rop:reduce_op)
                 (br:brand_relation_t)
                 (dl:list data) :
                 foreign_to_reduce_op_of_unary_op uop = Some rop ->
                 unary_op_eval br uop (dcoll dl) =
                 reduce_op_eval br rop dl
             ; foreign_to_reduce_op_to_unary_op
               (uop:reduce_op) : option unary_op
             ; foreign_to_reduce_op_to_unary_op_correct
                 (rop:reduce_op) (uop:unary_op)
                 (br:brand_relation_t)
                 (dl:list data) :
                 foreign_to_reduce_op_to_unary_op rop = Some uop ->
                 reduce_op_eval br rop dl =
                 unary_op_eval br uop (dcoll dl)
         }.

End ForeignToReduceOps.