Module Qcert.EJson.Operators.ForeignEJsonRuntime

Require Import String.
Require Import EquivDec.
Require Import List.
Require Import Utils.
Require Import ForeignEJson.
Require Import EJson.

Section ForeignEJsonRuntime.
  Class foreign_ejson_runtime
        (foreign_ejson_runtime_op : Set)
        {foreign_ejson_model:Set}
        {fejson:foreign_ejson foreign_ejson_model}
  : Type
    := mk_foreign_ejson_runtime {
           foreign_ejson_runtime_op_dec :> EqDec foreign_ejson_runtime_op eq
           ; foreign_ejson_runtime_op_tostring :> ToString foreign_ejson_runtime_op
           ; foreign_ejson_runtime_op_interp
               (f:foreign_ejson_runtime_op)
               (dl:list (@ejson foreign_ejson_model)) : option (@ejson foreign_ejson_model)
           ; foreign_ejson_runtime_tostring : (@ejson foreign_ejson_model) -> string
           ; foreign_ejson_runtime_fromstring : string -> option foreign_ejson_runtime_op
           ; foreign_ejson_runtime_totext : (@ejson foreign_ejson_model) -> string
         }.

End ForeignEJsonRuntime.