Module Qcert.Translation.ForeignToJava


Require Import List.
Require Import String.
Require Import Utils.
Require Import ForeignRuntime.
Require Import OperatorsUtils.

Local Open Scope string_scope.

Section ForeigntoJava.

         
  Inductive java_json : Set
    := mk_java_json : string -> java_json.

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