Module Qcert.Translation.ForeignToCloudant


Require Import List.
Require Import String.
Require Import Utils.
Require Import ForeignRuntime.
Require Import NNRCMRRuntime.
Require Import CldMR.
Require Import ForeignCloudant.

Local Open Scope string_scope.

Section ForeigntoCloudant.

  Class foreign_to_cloudant
        {fruntime:foreign_runtime}
        {fredop:foreign_reduce_op} : Type
  := mk_foreign_to_cloudant {
         foreign_to_cloudant_reduce_op
           (rop:foreign_reduce_op_type)
         : cld_reduce_op
         ; foreign_to_cloudant_prepare_nnrcmr :
             nnrcmr -> nnrcmr
         ; foreign_to_cloudant_nnrcmr_prepared :
             nnrcmr -> Prop
         ; foreign_to_cloudant_prepare_nnrcmr_prepares (src:nnrcmr) :
             foreign_to_cloudant_nnrcmr_prepared
               (foreign_to_cloudant_prepare_nnrcmr src)
       }.

End ForeigntoCloudant.