Module Qcert.Compiler.Lib.QType

Require Import CompilerRuntime.
Require Import Types.
Require RType.
Require TypeToJSON.
Require DTypeToJSON.
Require String.
Require DatatoSparkDF.
Require Data.
Require TUtil.
Require Schema.

Module QType(runtime:CompilerRuntime).

  Definition empty_brand_model (x:unit) := TBrandModel.empty_brand_model.

  Definition record_kind : Set
    := RType.record_kind.

  Definition open_kind : record_kind
    := RType.Open.

  Definition closed_kind : record_kind
    := RType.Closed.

  Definition qtype_struct {m:brand_relation} : Set
    := RType.rtype₀.
  Definition qtype {m:brand_relation} : Set
    := RType.rtype.
  Definition t {m:brand_relation} : Set
    := qtype.

  Definition sorted_pf_type {m:brand_relation} srl
      := SortingAdd.is_list_sorted Bindings.ODT_lt_dec (@Assoc.domain String.string qtype srl) = true.

  Definition bottom {m:brand_relation} : qtype
    := RType.Bottom.
  Definition top {m:brand_relation} : qtype
    := RType.Top.
  Definition unit {m:brand_relation} : qtype
    := RType.Unit.
  Definition nat {m:brand_relation} : qtype
    := RType.Nat.
  Definition bool {m:brand_relation} : qtype
    := RType.Bool.
  Definition string {m:brand_relation} : qtype
    := RType.String.
  Definition bag {m:brand_relation} : qtype -> qtype
    := RType.Coll.
  Definition record {m:brand_relation} : record_kind -> forall (r:list (String.string*qtype)), sorted_pf_type r -> qtype
    := RType.Rec.
  Definition either {m:brand_relation} : qtype -> qtype -> qtype
    := RType.Either.
  Definition arrow {m:brand_relation} : qtype -> qtype -> qtype
    := RType.Arrow.
  Definition brand {m:brand_relation} : list String.string -> qtype
    := RType.Brand.

  
  Definition json_to_rtype {m:brand_relation} := TypeToJSON.json_to_rtype.

  Definition json_to_rtype_with_fail {m:brand_relation} := TypeToJSON.json_to_rtype_with_fail.

  
  Definition qcert_dtype {m:brand_relation} : Set
    := DType.drtype.
  Definition dt {m:brand_relation} : Set
    := qcert_dtype.

  Definition json_to_drtype {m:brand_relation} : JSON.json -> qcert_dtype := DTypeToJSON.json_to_drtype.

  Definition json_to_vrtype_with_fail {m:brand_relation} : JSON.json -> option (String.string * qtype) :=
    TypeToJSON.json_to_vrtype_with_fail.

  Definition tlocal {m:brand_relation} : qtype -> qcert_dtype := DType.Tlocal.
  Definition tdistr {m:brand_relation} : qtype -> qcert_dtype := DType.Tdistr.


  Definition qtype_uncoll (m:brand_model) : qtype -> option qtype
    := @TUtil.tuncoll _ m.
  
  Definition data_to_sjson (m:brand_model) : Data.data -> qtype -> option String.string
    := @DatatoSparkDF.data_to_sjson _ _ _ _ _ _ m.


  Definition brand_relation : Set := brand_relation.
  Definition make_brand_relation := Schema.mk_brand_relation.
  Definition brand_model : Set := brand_model.
  Definition make_brand_model := Schema.make_brand_model_from_decls_fails.

End QType.