Module Qcert.Compiler.Lib.QOQL

Require Import CompilerRuntime.
Require String.
Require SortingDesc.
Require QData.
Require QOperators.
Require OQL.
Require OQLSugar.

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.qdata -> 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 -> list 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 -> SortingDesc.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 onew : String.string -> list (String.string * expr) -> expr
    := OQLSugar.ONew.

  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.