Qcert.Compiler.QLib.QLang

Module QLang(runtime:CompilerRuntime).




  Section QL.
    Context {bm:brand_model}.
    Context {ftyping: foreign_typing}.

    Definition rule := rule.
    Definition camp := camp.
    Definition oql := oql.
    Definition sql := sql.
    Definition lambda_nra := lambda_nra.
    Definition nra := nra.
    Definition nraenv_core := nraenv_core.
    Definition nraenv := nraenv.
    Definition nnrc := nnrc.
    Definition nnrcmr := nnrcmr.
    Definition cldmr := cldmr.
    Definition dnnrc_dataset := dnnrc_dataset.
    Definition dnnrc_typed_dataset {bm:brand_model} := dnnrc_typed_dataset.
    Definition javascript := javascript.
    Definition java := java.
    Definition spark_rdd := spark_rdd.
    Definition spark_dataset := spark_dataset.
    Definition cloudant := cloudant.

    Definition language : Set := language.

    Definition query : Set := query.

    Definition language_of_name_case_sensitive : string → language :=
      language_of_name_case_sensitive.
    Definition name_of_language : language → string :=
      name_of_language.
    Definition language_of_query : query → language := language_of_query.
    Definition name_of_query : query → string := name_of_query.

    Definition export_desc : Set := export_desc.
    Definition export_language_descriptions : export_desc := export_language_descriptions.

    Definition vdistr := Vdistr.
    Definition vlocal := Vlocal.
    Definition vdbindings := vdbindings.
    Definition tdbindings := tdbindings.
  End QL.
End QLang.