Qcert.Compiler.QLib.QOQL

Module QOQL(runtime:CompilerRuntime).

  Module Data := QData.QData runtime.
  Module Ops := QOperators.QOperators runtime.

  Definition expr : Set
    := OQL.oql_expr.
  Definition program : Set
    := OQL.oql.
  Definition t : Set
    := program.
  Definition var : Set
    := String.string.

  Definition select_expr : Set
    := OQL.oql_select_expr.
  Definition in_expr : Set
    := OQL.oql_in_expr.
  Definition where_expr : Set
    := OQL.oql_where_expr.
  Definition order_by_expr : Set
    := OQL.oql_order_by_expr.

  Definition ovar : var → expr
    := OQL.OVar.
  Definition oconst : Data.data → expr
    := OQL.OConst.
  Definition otable : String.string → expr
    := OQL.OTable.
  Definition obinop : Ops.Binary.op → expr →expr → expr
    := OQL.OBinop.
  Definition ounop : Ops.Unary.op → expr → expr
    := OQL.OUnop.
  Definition osfw : select_expr → list in_expr → where_expr → order_by_expr → expr
    := OQL.OSFW.
  Definition oselect : expr → select_expr
    := OQL.OSelect.
  Definition oselectdistinct : expr → select_expr
    := OQL.OSelectDistinct.
  Definition oin : String.string → expr → in_expr
    := OQL.OIn.
  Definition oincast : String.string → String.string → expr → in_expr
    := OQL.OInCast.
  Definition otrue : where_expr
    := OQL.OTrue.
  Definition owhere : expr → where_expr
    := OQL.OWhere.
  Definition onoorder : order_by_expr
    := OQL.ONoOrder.
  Definition oorder_by : expr → RDataSort.SortDesc → order_by_expr
    := OQL.OOrderBy.

  Definition odot : String.string → expr → expr
    := OQLSugar.ODot.
  Definition oarrow : String.string → expr → expr
    := OQLSugar.OArrow.
  Definition ostruct : list (String.string × expr) → expr
    := OQLSugar.OStruct.

  Definition tableify : expr → expr
    := OQLSugar.tableify.

  Definition define : String.string → expr → program → program
    := OQL.ODefineQuery.

  Definition undefine : String.string → program → program
    := OQL.OUndefineQuery.

  Definition query : expr → program
    := OQL.OQuery.

End QOQL.