Module Qcert.Translation.ForeignToSpark


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

Local Open Scope string_scope.

Section ForeigntoSpark.

  Class foreign_to_spark
        {fruntime:foreign_runtime}
        {fredop:foreign_reduce_op} : Type
  := mk_foreign_to_spark {
         foreign_to_spark_reduce_op
           (rop:foreign_reduce_op_type)
           (scala_endl quotel:string) : string
         ; foreign_to_spark_prepare_nnrcmr :
             nnrcmr -> nnrcmr
       }.

End ForeigntoSpark.