Module Qcert.SQL.Lang.SQLSize

Require Import String.
Require Import ZArith.
Require Import List.
Require Import Arith.
Require Import EquivDec.
Require Import Utils.
Require Import DataRuntime.
Require Import SQL.
  
Section SQLSize.
  Context {fruntime:foreign_runtime}.

  Section size.
    Fixpoint sql_query_size (q:sql_query) :=
      match q with
      | SUnion _ q1 q2 =>
        (sql_query_size q1) + (sql_query_size q2) + 1
      | SIntersect _ q1 q2 =>
        (sql_query_size q1) + (sql_query_size q2) + 1
      | SExcept _ q1 q2 =>
        (sql_query_size q1) + (sql_query_size q2) + 1
      | SQuery selects froms opt_where opt_group opt_order =>
        List.fold_left (fun acc select => acc + sql_select_size select) selects 0
        + List.fold_left (fun acc from => acc + sql_from_size from) froms 0
        + match opt_where with
          | None => 0
          | Some cond => sql_condition_size cond
          end
        + match opt_group with
          | None => 0
          | Some (_, Some cond) => sql_condition_size cond
          | Some (_, _) => 1
          end
        + match opt_order with
          | None => 0
          | Some cond => 1
          end
      end
        
    with sql_select_size (select: sql_select) :=
      match select with
      | SSelectColumn _ => 1
      | SSelectColumnDeref _ _ => 1
      | SSelectStar => 1
      | SSelectExpr _ e => sql_expr_size e
      end

    with sql_from_size (from: sql_from) :=
      match from with
      | SFromTable _ => 1
      | SFromTableAlias _ _ => 1
      | SFromQuery _ q => sql_query_size q
      end

    with sql_condition_size (cond: sql_condition) :=
      match cond with
      | SCondAnd c1 c2
      | SCondOr c1 c2 =>
        1 + sql_condition_size c1 + sql_condition_size c2
      | SCondNot c =>
        1 + sql_condition_size c
      | SCondBinary _ e1 e2 =>
        1 + sql_expr_size e1 + sql_expr_size e2
      | SCondExists q =>
        1 + sql_query_size q
      | SCondIn e1 e2 =>
        1 + sql_expr_size e1 + sql_expr_size e2
      | SCondLike e _ =>
        1 + sql_expr_size e
      | SCondBetween e1 e2 e3 =>
        1 + sql_expr_size e1 + sql_expr_size e2 + sql_expr_size e3
      end

    with sql_expr_size (expr: sql_expr) :=
      match expr with
      | SExprConst _ => 1
      | SExprColumn _ => 1
      | SExprColumnDeref _ _ => 1
      | SExprStar => 1
      | SExprUnary _ e => 1 + sql_expr_size e
      | SExprBinary _ e1 e2 => 1 + sql_expr_size e1 + sql_expr_size e2
      | SExprCase c e1 e2 =>
        1 + sql_condition_size c + sql_expr_size e1 + sql_expr_size e2
      | SExprAggExpr _ e => 1 + sql_expr_size e
      | SExprQuery q => 1 + sql_query_size q
      end.

    Definition sql_statement_size (st:sql_statement) :=
      match st with
      | SRunQuery q => sql_query_size q
      | SCreateView _ q => sql_query_size q
      | SDropView _ => 1
      end.

    Definition sql_size (q:sql) :=
      List.fold_left (fun acc st => acc + sql_statement_size st) q 0.

  End size.

  Section depth.

    Fixpoint sql_query_depth (q:sql_query) :=
      match q with
      | SUnion _ q1 q2 =>
        1 + (max (sql_query_depth q1) (sql_query_depth q2))
      | SIntersect _ q1 q2 =>
        1 + (max (sql_query_depth q1) (sql_query_depth q2))
      | SExcept _ q1 q2 =>
        1 + (max (sql_query_depth q1) (sql_query_depth q2))
      | SQuery selects froms opt_where opt_group opt_order =>
        max (List.fold_left (fun acc select => max acc (sql_select_depth select)) selects 0)
            (max (List.fold_left (fun acc from => max acc (sql_from_depth from)) froms 0)
                 (max (match opt_where with
                       | None => 0
                       | Some cond => sql_condition_depth cond
                       end)
                      (max (match opt_group with
                            | None => 0
                            | Some (_, Some cond) => sql_condition_depth cond
                            | Some (_, _) => 1
                            end)
                           (match opt_order with
                            | None => 0
                            | Some cond => 1
                            end))))
      end

    with sql_select_depth (select: sql_select) :=
      match select with
      | SSelectColumn _ => 0
      | SSelectColumnDeref _ _ => 0
      | SSelectStar => 0
      | SSelectExpr _ e => sql_expr_depth e
      end

    with sql_from_depth (from: sql_from) :=
      match from with
      | SFromTable _ => 0
      | SFromTableAlias _ _ => 0
      | SFromQuery _ q => 1 + sql_query_depth q
      end

    with sql_condition_depth (cond: sql_condition) :=
      match cond with
      | SCondAnd c1 c2
      | SCondOr c1 c2 =>
        max (sql_condition_depth c1) (sql_condition_depth c2)
      | SCondNot c =>
        sql_condition_depth c
      | SCondBinary _ e1 e2 =>
        max (sql_expr_depth e1) (sql_expr_depth e2)
      | SCondExists q =>
        sql_query_depth q
      | SCondIn e1 e2 =>
        max (sql_expr_depth e1) (sql_expr_depth e2)
      | SCondLike e _ =>
        sql_expr_depth e
      | SCondBetween e1 e2 e3 =>
        max (sql_expr_depth e1) (max (sql_expr_depth e2) (sql_expr_depth e3))
      end

    with sql_expr_depth (expr: sql_expr) :=
      match expr with
      | SExprConst _ => 0
      | SExprColumn _ => 0
      | SExprColumnDeref _ _ => 0
      | SExprStar => 0
      | SExprUnary _ e => sql_expr_depth e
      | SExprBinary _ e1 e2 => max (sql_expr_depth e1) (sql_expr_depth e2)
      | SExprCase c e1 e2 =>
        max (sql_condition_depth c) (max (sql_expr_depth e1) (sql_expr_depth e2))
      | SExprAggExpr _ e => sql_expr_depth e
      | SExprQuery q => sql_query_depth q
      end.

    Definition sql_statement_depth (st:sql_statement) :=
      match st with
      | SRunQuery q => 1 + sql_query_depth q
      | SCreateView _ q => sql_query_depth q
      | SDropView _ => 1
      end.

    Definition sql_depth (q:sql) :=
      List.fold_left (fun acc st => max acc (sql_statement_depth st)) q 0.

  End depth.
  
End SQLSize.