Module Qcert.Translation.Operators.ForeignToJava

Require Import List.
Require Import String.
Require Import Utils.
Require Import ForeignRuntime.
Require Import JavaRuntime.

Local Open Scope string_scope.

Section ForeigntoJava.
  Class foreign_to_java {fruntime:foreign_runtime}: Type
    := mk_foreign_to_java {
           foreign_to_java_data
             (quotel:string) (fd:foreign_data_model) : java_json
           ; foreign_to_java_unary_op
               (indent:nat) (eol:string)
               (quotel:string) (fu:foreign_operators_unary)
               (d:java_json) : java_json
           ; foreign_to_java_binary_op
               (indent:nat) (eol:string)
               (quotel:string) (fb:foreign_operators_binary)
               (d1 d2:java_json) : java_json
         }.
      
End ForeigntoJava.