Module Qcert.SQLPP.Lang.SQLPP

Require Import String.
Require Import ZArith.
Require Import List.
Require Import Arith.
Require Import EquivDec.
Require Import Utils.
Require Import DataRuntime.

Section SQLPP.
  Context {fruntime:foreign_runtime}.

  Unset Elimination Schemes.

  Definition sqlpp_order_spec : Set := SortDesc.
  Inductive sqlpp_distinct : Set := SPDistinct | SPAll.
  Inductive sqlpp_join_type : Set := SPInner | SPLeftOuter.

The set of function names currently supported

The SQLPP grammar according to AsterixDB

Statement ::= ( SingleStatement ( ";" )? )* <EOF>

SingleStatement ::= DatabaseDeclaration
                  | FunctionDeclaration
                  | CreateStatement
                  | DropStatement
                  | LoadStatement
                  | SetStatement
                  | InsertStatement
                  | DeleteStatement
                  | Query ";"

We currently support source files containing all possible statement types but only Query statements are passed along by the initial front end. Other statements are silently elided. Of course, this can result in semantic nonsense when, for example, a FunctionDeclaration is elided but is then used in a subsequent Query. However, eliding most other statement types works in practice since they are present for bookkeeping purposes and don't affect the semantics of the Query statements.

Query ::= (Expression | SelectStatement) ";"

The distinction between Expression and SelectStatement is a superficial grammar technicality, because a parenthesized SelectStatement is an Expression. The duality at this production amounts to saying it is ok to omit the parentheses at top level when followed by a semi-colon. At the level of the AST, though, a Query is an Expression and Expression is actually the top-level production. Most of the non-terminals below "Expression" are there to show precedence, which is important in the grammar but is not needed in the AST. So, the AST is basically a huge inductive set on Expression.

Valid operators for the second form (binary operators) are plus, minus, mult, div, mod, exp, concat, in, fuzzy-eq, eq, neq, lt, gt, le, ge, like, and, or (Actually, fuzzy-eq isn't listed in the SQL++ grammar, but it's in the AQL grammar and supported for SQL++ by AsterixDB). Note that we restrict the RHS of 'like' to be a String literal, which is more restrictive than the language spec.

  | SPPlus : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPMinus : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPMult : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPDiv : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPMod : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPExp : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPConcat : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPIn : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPEq : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPFuzzyEq : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPNeq : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPLt : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPGt : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPLe : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPGe : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPLike : sqlpp_expr -> string -> sqlpp_expr
  | SPAnd : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPOr : sqlpp_expr -> sqlpp_expr -> sqlpp_expr

Finally, the ternery BETWEEN operator

  | SPBetween : sqlpp_expr -> sqlpp_expr -> sqlpp_expr -> sqlpp_expr


  | SPSimpleCase : sqlpp_expr -> list sqlpp_when_then -> option sqlpp_expr -> sqlpp_expr
  | SPSearchedCase : list sqlpp_when_then -> option sqlpp_expr -> sqlpp_expr


  | SPSome : list (string * sqlpp_expr) -> sqlpp_expr -> sqlpp_expr
  | SPEvery : list (string * sqlpp_expr) -> sqlpp_expr -> sqlpp_expr


  | SPDot : sqlpp_expr -> string -> sqlpp_expr

  | SPIndex : sqlpp_expr -> sqlpp_expr -> sqlpp_expr
  | SPIndexAny : sqlpp_expr -> sqlpp_expr

  | SPLiteral : data -> sqlpp_expr
  | SPNull | SPMissing

  | SPVarRef : string -> sqlpp_expr

  | SPFunctionCall : sqlpp_function_name -> list sqlpp_expr -> sqlpp_expr


  | SPArray : list sqlpp_expr -> sqlpp_expr

  | SPBag : list sqlpp_expr -> sqlpp_expr

  | SPObject : list (string * sqlpp_expr) -> sqlpp_expr


  | SPQuery : sqlpp_select_statement -> sqlpp_expr

with sqlpp_select_statement : Set :=
SPSelectStmt :
  list (string * sqlpp_expr)
  -> sqlpp_select_block
  -> list sqlpp_union_element
  -> sqlpp_order_by
  -> sqlpp_select_statement

with sqlpp_select_block : Set :=
SPSelectBlock : sqlpp_select -> list sqlpp_from
     -> list (string * sqlpp_expr)
        -> sqlpp_where -> sqlpp_group_by
        -> list (string * sqlpp_expr)
        -> option sqlpp_expr
        -> sqlpp_select_block

with sqlpp_union_element : Set :=
  | SPBlock : sqlpp_select_block -> sqlpp_union_element
  | SPSubquery : sqlpp_select_statement -> sqlpp_union_element

with sqlpp_select : Set :=
  | SPSelectSQL : sqlpp_distinct -> list sqlpp_project -> sqlpp_select
  | SPSelectValue: sqlpp_distinct -> sqlpp_expr -> sqlpp_select

with sqlpp_project : Set :=
  | SPProject : (sqlpp_expr * option string) -> sqlpp_project
  | SPProjectStar


with sqlpp_from : Set :=
  | SPFrom : sqlpp_expr -> option string -> list sqlpp_join_clause -> sqlpp_from

with sqlpp_join_clause : Set :=
  | SPJoin : sqlpp_join_type -> sqlpp_expr -> option string -> sqlpp_expr -> sqlpp_join_clause
  | SPUnnest : sqlpp_join_type -> sqlpp_expr -> option string -> option string -> sqlpp_join_clause

with sqlpp_where : Set :=
  | SPWhere : sqlpp_expr -> sqlpp_where
  | SPNoWhere

with sqlpp_group_by : Set :=
| SPGroupBy : list (sqlpp_expr * option string)
  -> option (string * list (string * string))
  -> sqlpp_group_by
    | SPNoGroupBy

with sqlpp_order_by : Set :=
| SPOrderBy : list (sqlpp_expr * sqlpp_order_spec) -> sqlpp_order_by
| SPNoOrderBy

with sqlpp_when_then : Set:=
| SPWhenThen : sqlpp_expr -> sqlpp_expr -> sqlpp_when_then
.

  Definition sqlpp : Set := sqlpp_expr.


End SQLPP.