Module Qcert.SQLPP.Lang.SQLPP


Section SQLPP.
  Require Import String.
  Require Import ZArith.
  Require Import List.
  Require Import Arith.
  Require Import EquivDec.
  Require Import Utils.
  Require Import CommonSystem.

  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
  Inductive sqlpp_function_name : Set :=
      SPFget_year
  | SPFget_month
  | SPFget_day
  | SPFget_hour
  | SPFget_minute
  | SPFget_second
  | SPFget_millisecond
  | SPFavg
  | SPFmin
  | SPFmax
  | SPFcount
  | SPFsum
  | SPFcoll_avg
  | SPFcoll_min
  | SPFcoll_max
  | SPFcoll_count
  | SPFcoll_sum
  | SPFarray_avg
  | SPFarray_min
  | SPFarray_max
  | SPFarray_count
  | SPFarray_sum
  | SPFsqrt
  | SPFsubstring
  | SPFregexp_contains
  | SPFcontains
  .
  
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.

  Inductive sqlpp_expr : Set :=


  | SPPositive : sqlpp_expr -> sqlpp_expr
  | SPNegative : sqlpp_expr -> sqlpp_expr
  | SPExists : sqlpp_expr -> sqlpp_expr
  | SPNot : sqlpp_expr -> sqlpp_expr
  | SPIsNull : sqlpp_expr -> sqlpp_expr
  | SPIsMissing : sqlpp_expr -> sqlpp_expr
  | SPIsUnknown : sqlpp_expr -> sqlpp_expr

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.