Qcert.Translation.SQLtoNRAEnv

Section SQLtoNRAEnv.



  Context {fruntime:foreign_runtime}.


  Definition sql_order_to_nraenv (acc:nraenv) (opt_order:option sql_order_spec) :=
    match opt_order with
    | None ⇒ acc
    | Some sql_order_spec ⇒
      NRAEnvUnop (AOrderBy sql_order_spec) acc
    end.

  Definition column_of_select (select:sql_select) : (option string × string) :=
    match select with
    | SSelectColumn cname ⇒ (None,cname)
    | SSelectColumnDeref tname cname ⇒ (Some tname,cname)
    | SSelectStar ⇒ (None,""%string)
    | SSelectExpr cname _ ⇒ (None,cname)
    end.

  Definition columns_of_selects (selects:list sql_select) : list (option string × string) :=
    map column_of_select selects.

  Fixpoint columns_of_query (q:sql_query) : list (option string × string) :=
    match q with
    | SUnion _ q1 q2 ⇒
      columns_of_query q1
    | SIntersect _ q1 q2 ⇒
      columns_of_query q1
    | SExcept _ q1 q2 ⇒
      columns_of_query q1
    | SQuery selects _ _ _ _ ⇒
      columns_of_selects selects
    end.

  Fixpoint create_renaming
           (out_columns:list string)
           (in_columns:list (option string × string)) :=
    match out_columns,in_columns with
    | nil,_ | _,nil ⇒ (NRAEnvConst (drec nil))
    | out_cname :: out_columns', (None,in_cname) :: in_columns' ⇒
      NRAEnvBinop AConcat
                  (NRAEnvUnop (ARec out_cname) (NRAEnvUnop (ADot in_cname) NRAEnvID))
                  (create_renaming out_columns' in_columns')
    | out_cname :: out_columns', (Some in_tname,in_cname) :: in_columns' ⇒
      NRAEnvBinop AConcat
                  (NRAEnvUnop (ARec out_cname) (NRAEnvUnop (ADot in_cname) (NRAEnvUnop (ADot in_tname) NRAEnvID)))
                  (create_renaming out_columns' in_columns')
    end.

  Definition nraenv_if b expr1 expr2
    :=
      NRAEnvApp
        (NRAEnvEither
           (NRAEnvApp expr1 (NRAEnvUnop (ADot "id"%string) NRAEnvID))
           (NRAEnvApp expr2 (NRAEnvUnop (ADot "id"%string) NRAEnvID)))
        (NRAEnvEitherConcat
           (NRAEnvApp (NRAEnvEither (NRAEnvConst (dleft (drec nil))) (NRAEnvConst (dright (drec nil))))
                      (NRAEnvUnop ASingleton (NRAEnvSelect NRAEnvID (NRAEnvUnop AColl b))))
           ((NRAEnvUnop (ARec "id"%string) NRAEnvID))).


  Section queryvar.
    Context (view_list:list string).

    Definition lookup_table (table_name:string) : nraenv
      := if in_dec string_eqdec table_name view_list
         then NRAEnvUnop (ADot table_name) NRAEnvEnv
         else NRAEnvGetConstant table_name.

    Fixpoint sql_query_to_nraenv (create_table:bool) (q:sql_query) {struct q} : nraenv :=
      let q_is_singleton : bool := is_singleton_sql_query q in
      match q with
      | SUnion SAll q1 q2 ⇒
        NRAEnvBinop AUnion
                    (sql_query_to_nraenv create_table q1)
                    (sql_query_to_nraenv create_table q2)
      | SUnion SDistinct q1 q2 ⇒
        NRAEnvUnop ADistinct
                   (NRAEnvBinop AUnion
                                (sql_query_to_nraenv create_table q1)
                                (sql_query_to_nraenv create_table q2))
      | SIntersect SAll q1 q2 ⇒
        NRAEnvBinop AMin
                    (sql_query_to_nraenv create_table q1)
                    (sql_query_to_nraenv create_table q2)
      | SIntersect SDistinct q1 q2 ⇒
        NRAEnvUnop ADistinct
                   (NRAEnvBinop AMin
                                (sql_query_to_nraenv create_table q1)
                                (sql_query_to_nraenv create_table q2))
      | SExcept SAll q1 q2 ⇒
        NRAEnvBinop AMinus
                    (sql_query_to_nraenv create_table q1)
                    (sql_query_to_nraenv create_table q2)
      | SExcept SDistinct q1 q2 ⇒
        NRAEnvUnop ADistinct
                   (NRAEnvBinop AMinus
                                (sql_query_to_nraenv create_table q1)
                                (sql_query_to_nraenv create_table q2))
      | SQuery selects froms opt_where opt_group opt_order ⇒
        let nraenv_from_clause :=
            fold_left sql_from_to_nraenv froms (NRAEnvUnop AColl NRAEnvID)
        in
        let nraenv_where_clause :=
            match opt_where with
            | None ⇒ nraenv_from_clause
            | Some cond ⇒ NRAEnvSelect (sql_condition_to_nraenv NRAEnvID cond) nraenv_from_clause
            end
        in
        let nraenv_group_by_clause :=
            match opt_group with
            | None ⇒ nraenv_where_clause
            | Some (sl,None) ⇒ NRAEnvGroupBy "partition" sl nraenv_where_clause
            | Some (sl,Some cond) ⇒
              NRAEnvSelect (sql_condition_to_nraenv (NRAEnvUnop (ADot "partition") NRAEnvID) cond)
                           (NRAEnvGroupBy "partition" sl nraenv_where_clause)
            end
        in
        let nraenv_select_clause :=
            if q_is_singleton
            then
              match selects with
              | SSelectExpr _ expr :: nil ⇒
                sql_expr_to_nraenv true nraenv_group_by_clause expr
              | _ ⇒ NRAEnvConst dunit
              end
            else
              if create_table
              then
                NRAEnvMap (fold_left sql_select_to_nraenv selects (NRAEnvConst (drec nil)))
                          nraenv_group_by_clause
              else
                if (is_value_sequence_sql_query q)
                then
                  match selects with
                  | SSelectExpr _ expr :: nil ⇒
                    NRAEnvMap (sql_expr_to_nraenv false NRAEnvID expr) nraenv_group_by_clause
                  | SSelectColumn cname :: nil ⇒
                    NRAEnvMap (NRAEnvUnop (ADot cname) NRAEnvID) nraenv_group_by_clause
                  | SSelectColumnDeref tname cname :: nil ⇒
                    NRAEnvMap (NRAEnvUnop (ADot cname) (NRAEnvUnop (ADot tname) NRAEnvID)) nraenv_group_by_clause
                  | _ ⇒ NRAEnvConst dunit
                  end
                else
                  NRAEnvConst dunit
        in
        let nraenv_order_by_clause := sql_order_to_nraenv nraenv_select_clause opt_order in
        nraenv_order_by_clause
      end
    with sql_from_to_nraenv (acc:nraenv) (from:sql_from) {struct from} :=
           match from with
           | (SFromTable tname) ⇒ NRAEnvProduct (lookup_table tname) acc
           | (SFromTableAlias new_name tname) ⇒
             NRAEnvProduct (NRAEnvMap (NRAEnvUnop (ARec new_name) NRAEnvID) (lookup_table tname)) acc
           | SFromQuery tspec q ⇒
             let (tname,opt_columns) := tspec in
             match opt_columns with
             | Some out_columns ⇒
               let in_columns := columns_of_query q in
               NRAEnvMap (create_renaming out_columns in_columns)
                         (sql_query_to_nraenv true q)
             | None ⇒ sql_query_to_nraenv true q
             end
           end
    with sql_select_to_nraenv (acc:nraenv) (select:sql_select) {struct select} :=
           match select with
           | SSelectColumn cname ⇒
             NRAEnvBinop AConcat
                         (NRAEnvUnop (ARec cname) (NRAEnvUnop (ADot cname) NRAEnvID))
                         acc
           | SSelectColumnDeref tname cname ⇒
             NRAEnvBinop AConcat
                         (NRAEnvUnop (ARec cname) (NRAEnvUnop (ADot cname) (NRAEnvUnop (ADot tname) NRAEnvID)))
                         acc
           | SSelectStar ⇒
             NRAEnvBinop AConcat NRAEnvID acc
           | SSelectExpr cname expr ⇒
             NRAEnvBinop AConcat
                         (NRAEnvUnop (ARec cname) (sql_expr_to_nraenv false (NRAEnvUnop (ADot "partition") NRAEnvID) expr))
                         acc
           end
    with sql_expr_to_nraenv (create_table:bool) (acc:nraenv) (expr:sql_expr) {struct expr} :=
           match expr with
           | SExprConst d ⇒ NRAEnvConst d
           | SExprColumn cname ⇒ NRAEnvUnop (ADot cname) NRAEnvID
           | SExprColumnDeref tname cname ⇒ NRAEnvUnop (ADot cname) (NRAEnvUnop (ADot tname) NRAEnvID)
           | SExprStar ⇒ NRAEnvID
           | SExprUnary (SSubstring n1 on2) expr1 ⇒
             NRAEnvUnop (ASubstring n1 on2)
                        (sql_expr_to_nraenv create_table acc expr1)
           | SExprUnary (SUnaryForeignExpr fu) expr1 ⇒
             NRAEnvUnop (AForeignUnaryOp fu)
                        (sql_expr_to_nraenv create_table acc expr1)
           | SExprBinary (SBinaryForeignExpr fb) expr1 expr2 ⇒
             NRAEnvBinop (AForeignBinaryOp fb)
                         (sql_expr_to_nraenv create_table acc expr1)
                         (sql_expr_to_nraenv create_table acc expr2)
           | SExprBinary SPlus expr1 expr2 ⇒
             NRAEnvBinop (ABArith ArithPlus)
                         (sql_expr_to_nraenv create_table acc expr1)
                         (sql_expr_to_nraenv create_table acc expr2)
           | SExprBinary SSubtract expr1 expr2 ⇒
             NRAEnvBinop (ABArith ArithMinus)
                         (sql_expr_to_nraenv create_table acc expr1)
                         (sql_expr_to_nraenv create_table acc expr2)
           | SExprUnary SMinus expr1 ⇒
             NRAEnvBinop (ABArith ArithMinus)
                         (NRAEnvConst (dnat 0))
                         (sql_expr_to_nraenv create_table acc expr1)
           | SExprBinary SMult expr1 expr2 ⇒
             NRAEnvBinop (ABArith ArithMult)
                         (sql_expr_to_nraenv create_table acc expr1)
                         (sql_expr_to_nraenv create_table acc expr2)
           | SExprBinary SDivide expr1 expr2 ⇒
             NRAEnvBinop (ABArith ArithDivide)
                         (sql_expr_to_nraenv create_table acc expr1)
                         (sql_expr_to_nraenv create_table acc expr2)
           | SExprBinary SConcat expr1 expr2 ⇒
             NRAEnvBinop ASConcat
                         (sql_expr_to_nraenv create_table acc expr1)
                         (sql_expr_to_nraenv create_table acc expr2)
           | SExprCase cond expr1 expr2 ⇒
             nraenv_if
               (sql_condition_to_nraenv acc cond)
               (sql_expr_to_nraenv create_table acc expr1)
               (sql_expr_to_nraenv create_table acc expr2)
           | SExprAggExpr SSum expr1 ⇒
             NRAEnvUnop ASum (NRAEnvMap (sql_expr_to_nraenv create_table NRAEnvID expr1) acc)
           | SExprAggExpr SAvg expr1 ⇒
             NRAEnvUnop AArithMean (NRAEnvMap (sql_expr_to_nraenv create_table NRAEnvID expr1) acc)
           | SExprAggExpr SCount expr1 ⇒
             NRAEnvUnop ACount (NRAEnvMap (sql_expr_to_nraenv create_table NRAEnvID expr1) acc)
           | SExprAggExpr SMin expr1 ⇒
             NRAEnvUnop ANumMin (NRAEnvMap (sql_expr_to_nraenv create_table NRAEnvID expr1) acc)
           | SExprAggExpr SMax expr1 ⇒
             NRAEnvUnop ANumMax (NRAEnvMap (sql_expr_to_nraenv create_table NRAEnvID expr1) acc)
           | SExprQuery q ⇒
             if create_table
             then sql_query_to_nraenv true q
             else sql_query_to_nraenv false q
           end
    with sql_condition_to_nraenv (acc:nraenv) (cond:sql_condition) {struct cond} :=
           match cond with
           | SCondAnd cond1 cond2 ⇒
             NRAEnvBinop AAnd
                         (sql_condition_to_nraenv acc cond1)
                         (sql_condition_to_nraenv acc cond2)
           | SCondOr cond1 cond2 ⇒
             NRAEnvBinop AOr
                         (sql_condition_to_nraenv acc cond1)
                         (sql_condition_to_nraenv acc cond2)
           | SCondNot cond1 ⇒
             NRAEnvUnop ANeg
                        (sql_condition_to_nraenv acc cond1)
           | SCondBinary SEq expr1 expr2 ⇒
             NRAEnvBinop AEq
                         (sql_expr_to_nraenv true acc expr1)
                         (sql_expr_to_nraenv true acc expr2)
           | SCondBinary SLe expr1 expr2 ⇒
             NRAEnvBinop ALe
                         (sql_expr_to_nraenv true acc expr1)
                         (sql_expr_to_nraenv true acc expr2)
           | SCondBinary SLt expr1 expr2 ⇒
             NRAEnvBinop ALt
                         (sql_expr_to_nraenv true acc expr1)
                         (sql_expr_to_nraenv true acc expr2)
           | SCondBinary SGe expr1 expr2 ⇒
             NRAEnvUnop ANeg (NRAEnvBinop ALt
                                          (sql_expr_to_nraenv true acc expr1)
                                          (sql_expr_to_nraenv true acc expr2))
           | SCondBinary SGt expr1 expr2 ⇒
             NRAEnvUnop ANeg (NRAEnvBinop ALe
                                          (sql_expr_to_nraenv true acc expr1)
                                          (sql_expr_to_nraenv true acc expr2))
           | SCondBinary SDiff expr1 expr2 ⇒
             NRAEnvUnop ANeg (NRAEnvBinop AEq
                                          (sql_expr_to_nraenv true acc expr1)
                                          (sql_expr_to_nraenv true acc expr2))
           | SCondBinary (SBinaryForeignCond fb) expr1 expr2 ⇒
             NRAEnvBinop (AForeignBinaryOp fb)
                         (sql_expr_to_nraenv true acc expr1)
                         (sql_expr_to_nraenv true acc expr2)
           | SCondExists q ⇒
             NRAEnvUnop ANeg (NRAEnvBinop ALe
                                          (NRAEnvUnop ACount (sql_query_to_nraenv true q))
                                          (NRAEnvConst (dnat 0)))
           | SCondIn expr1 expr2 ⇒
             NRAEnvBinop AContains
                         (sql_expr_to_nraenv true acc expr1)
                         (sql_expr_to_nraenv false acc expr2)
           | SCondLike expr1 slike ⇒
             NRAEnvUnop (ALike slike None) (sql_expr_to_nraenv true acc expr1)
           | SCondBetween expr1 expr2 expr3 ⇒
             NRAEnvBinop AAnd
                         (NRAEnvBinop ALe
                                      (sql_expr_to_nraenv true acc expr2)
                                      (sql_expr_to_nraenv true acc expr1))
                         (NRAEnvBinop ALe
                                      (sql_expr_to_nraenv true acc expr1)
                                      (sql_expr_to_nraenv true acc expr3))
           end.

    Definition sql_query_to_nraenv_top (q:sql_query) : nraenv :=
      NRAEnvApp (sql_query_to_nraenv true q) (NRAEnvConst (drec nil)).
    End queryvar.

  Fixpoint sql_statements_to_nraenv
           (view_list:list string) (q:sql) : nraenv
    := match q with
       | nil ⇒ NRAEnvID
       | (SRunQuery q)::rest ⇒
         NRAEnvApp
           (sql_statements_to_nraenv view_list rest)
           (sql_query_to_nraenv_top view_list q)
       | (SCreateView s q)::rest ⇒
         NRAEnvAppEnv
           (sql_statements_to_nraenv (s::view_list) rest)
           (NRAEnvBinop AConcat
                        NRAEnvEnv
                        (NRAEnvUnop (ARec s)
                                    (sql_query_to_nraenv_top view_list q)))
       | (SDropView s)::rest ⇒
         NRAEnvAppEnv
           (sql_statements_to_nraenv (remove_all s view_list) rest)
           (NRAEnvUnop (ARecRemove s) NRAEnvEnv)
       end.

  Definition sql_to_nraenv (q:sql) : nraenv
    :=
      NRAEnvAppEnv
        (NRAEnvApp (sql_statements_to_nraenv nil q) (NRAEnvConst dunit))
        (NRAEnvConst (drec nil)).

End SQLtoNRAEnv.