Module Qcert.Translation.Model.ForeignEJsonToJSON

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

Require Import ForeignEJson.
Require Import JSONRuntime.

Local Open Scope string_scope.

Class foreign_to_json
      {foreign_ejson_model:Set}
      {fejson:foreign_ejson foreign_ejson_model}
  : Type
  := mk_foreign_to_json {
         foreign_to_json_to_ejson
             (fd:json) : option foreign_ejson_model
         ; foreign_to_json_from_ejson
             (j:foreign_ejson_model) : json
       }.