Module Qcert.Translation.Model.ForeignDataToEJson

Require Import List.
Require Import String.
Require Import Utils.

Require Import DataRuntime.
Require Import ForeignRuntime.
Require Import ForeignEJson.
Require Import ForeignEJsonRuntime.

Local Open Scope string_scope.

Class foreign_to_ejson
      (foreign_ejson_model:Set)
      (foreign_ejson_runtime_op:Set)
      {fejson:foreign_ejson foreign_ejson_model}
      {fruntime:foreign_runtime}
  : Type
  := mk_foreign_to_ejson {
         foreign_to_ejson_runtime :> foreign_ejson_runtime foreign_ejson_runtime_op
         ; foreign_to_ejson_to_data
             (j:foreign_ejson_model) : foreign_data_model
         ; foreign_to_ejson_from_data
             (fd:foreign_data_model) : foreign_ejson_model
         ; foreign_to_ejson_to_data_to_ejson (fd:foreign_data_model) :
             foreign_to_ejson_to_data (foreign_to_ejson_from_data fd) = fd
       }.