Qcert.Compiler.QLib.QData


Module QData(runtime:CompilerRuntime).


  Definition json : Set
    := JSON.json.
  Definition data : Set
    := RData.data.
  Definition t : Set
    := data.

  Definition jnil : json
    := JSON.jnil.
  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
    := RData.dunit.
  Definition dnat z : data
    := RData.dnat z.
  Definition dbool b : data
    := RData.dbool b.
  Definition dstring s : data
    := RData.dstring s.
  Definition dcoll dl : data
    := RData.dcoll dl.
  Definition drec dl : data
    := RData.drec dl.
  Definition dleft : data → data
    := RData.dleft.
  Definition dright : data → data
    := RData.dright.
  Definition dbrand b : data → data
    := RData.dbrand b.

JSON -> data conversion (META variant)
  Definition json_to_data br : JSON.json → data
    := JSONtoData.json_to_data br.
JSON -> data conversion (Enhanced variant)
  Definition json_enhanced_to_data br : JSON.json → data
    := JSONtoData.json_enhanced_to_data br.
data -> JSON *string* conversion
  Definition dataToJS s : data → String.string
    := NNRCtoJavascript.dataToJS s.

  Definition jsonToJS s : JSON.json → String.string
    := NNRCtoJavascript.jsonToJS s.

  Section dist.
    Definition ddata : Set := DData.ddata.
    Definition dlocal : data → ddata := DData.Dlocal.
    Definition ddistr (x:data) : option ddata :=
      match x with
      | RData.dcoll c ⇒ Some (DData.Ddistr c)
      | _ ⇒ None
      end.
  End dist.
End QData.