Module 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
.