Module ErgoSpec.Backend.Lib.QData

Require Import String.
Require Import Qcert.Data.DataRuntime.
Require Import Qcert.JSON.JSONSystem.
Require Import Qcert.Translation.Model.DataToEJson.
Require Import Qcert.Translation.Model.EJsonToJSON.

Require Import ErgoSpec.Backend.Lib.QBackendModel.
Require Import ErgoSpec.Backend.Lib.QBackendRuntime.

Module QData(ergomodel:QBackendModel).
  
  Definition json : Set
    := JSON.json.
  Definition data : Set
    := Data.data.
  Definition t : Set
    := data.
  
  Definition jnull : json
    := JSON.jnull.
  Definition jnumber z : json
    := JSON.jnumber z.
  Definition jbool b : json
    := JSON.jbool b.
  Definition jstring s : json
    := JSON.jstring s.
  Definition jarray jl : json
    := JSON.jarray jl.
  Definition jobject jl : json
    := JSON.jobject jl.

  Definition dunit : data
    := Data.dunit.
  Definition dnat z : data
    := Data.dnat z.
  Definition dfloat f : data
    := Data.dfloat f.
  Definition dbool b : data
    := Data.dbool b.
  Definition dstring s : data
    := Data.dstring s.
  Definition dcoll dl : data
    := Data.dcoll dl.
  Definition drec dl : data
    := Data.drec dl.
  Definition dleft : data -> data
    := Data.dleft.
  Definition dright : data -> data
    := Data.dright.
  Definition dbrand b : data -> data
    := Data.dbrand b.

  Definition dsome : data -> data
    := Data.dsome.
  Definition dnone : data
    := Data.dnone.
  
  Definition dsuccess : data -> data
    := Data.dleft.
  Definition derror : data -> data
    := Data.dright.
  

End QData.