Module Qcert.OQL.Lang.OQL

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

Declare Scope oql_scope.

Section OQL.
  Context {fruntime:foreign_runtime}.

  Unset Elimination Schemes.
  
  Inductive oql_expr : Set :=
  | OConst : data -> oql_expr
  | OVar : string -> oql_expr
  | OTable : string -> oql_expr
  | OBinop : binary_op -> oql_expr -> oql_expr -> oql_expr
  | OUnop : unary_op -> oql_expr -> oql_expr
  | OSFW : oql_select_expr -> (list oql_in_expr) -> oql_where_expr -> oql_order_by_expr -> oql_expr
  with oql_select_expr : Set :=
  | OSelect : oql_expr -> oql_select_expr
  | OSelectDistinct : oql_expr -> oql_select_expr
  with oql_in_expr : Set :=
  | OIn : string -> oql_expr -> oql_in_expr
  | OInCast : string -> list string -> oql_expr -> oql_in_expr
  with oql_where_expr : Set :=
  | OTrue : oql_where_expr
  | OWhere : oql_expr -> oql_where_expr
  with oql_order_by_expr : Set :=
  | ONoOrder : oql_order_by_expr
  | OOrderBy : oql_expr -> SortDesc -> oql_order_by_expr
  .

  Set Elimination Schemes.

  Inductive oql_query_program : Set :=
  | ODefineQuery : string -> oql_expr -> oql_query_program -> oql_query_program
  | OUndefineQuery : string -> oql_query_program -> oql_query_program
  | OQuery : oql_expr -> oql_query_program
  .

  Definition oql : Set := oql_query_program.
  
  Definition oselect_expr (ie:oql_select_expr) : oql_expr :=
    match ie with
    | OSelect e => e
    | OSelectDistinct e => e
    end.

  Definition oin_expr (ie:oql_in_expr) : oql_expr :=
    match ie with
    | OIn _ e => e
    | OInCast _ _ e => e
    end.
  
  Definition oql_expr_rect (P : oql_expr -> Type)
             (fconst : forall d : data, P (OConst d))
             (fvar : forall v : string, P (OVar v))
             (ftable : forall t : string, P (OTable t))
             (fbinop : forall b : binary_op,
                 forall e1 e2 : oql_expr, P e1 -> P e2 -> P (OBinop b e1 e2))
             (funop : forall u : unary_op,
                 forall e1 : oql_expr, P e1 -> P (OUnop u e1))
             (fswf1 : forall e1 : oql_select_expr, forall el : list oql_in_expr,
                   P (oselect_expr e1) -> Forallt (fun ab => P (oin_expr ab)) el -> P (OSFW e1 el OTrue ONoOrder))
             (fswf2 : forall e1 : oql_select_expr, forall el : list oql_in_expr, forall ew : oql_expr,
                   P (oselect_expr e1) -> Forallt (fun ab => P (oin_expr ab)) el -> P ew -> P (OSFW e1 el (OWhere ew) ONoOrder))
             (fswf3 : forall e1 : oql_select_expr, forall el : list oql_in_expr, forall eob : oql_expr, forall sc : SortDesc,
                   P (oselect_expr e1) -> Forallt (fun ab => P (oin_expr ab)) el -> P eob -> P (OSFW e1 el OTrue (OOrderBy eob sc)))
             (fswf4 : forall e1 : oql_select_expr, forall el : list oql_in_expr, forall ew : oql_expr, forall eob : oql_expr, forall sc : SortDesc,
                   P (oselect_expr e1) -> Forallt (fun ab => P (oin_expr ab)) el -> P ew -> P eob -> P (OSFW e1 el (OWhere ew) (OOrderBy eob sc)))
    := fix F (e : oql_expr) : P e :=
    match e as e0 return (P e0) with
      | OConst d => fconst d
      | OVar v => fvar v
      | OTable t => ftable t
      | OBinop b e1 e2 => fbinop b _ _ (F e1) (F e2)
      | OUnop u e1 => funop u _ (F e1)
      | OSFW e1 el OTrue ONoOrder =>
        fswf1 _ el (F (oselect_expr e1))
              ((fix F1 (r : list oql_in_expr) : Forallt (fun ab => P (oin_expr ab)) r :=
                  match r as c0 with
                  | nil => Forallt_nil _
                  | cons sd c0 => @Forallt_cons _ (fun ab => P (oin_expr ab)) sd c0 (F (oin_expr sd)) (F1 c0)
                  end) el)
      | OSFW e1 el (OWhere ew) ONoOrder =>
        fswf2 _ el _ (F (oselect_expr e1))
              ((fix F1 (r : list oql_in_expr) : Forallt (fun ab => P (oin_expr ab)) r :=
                  match r as c0 with
                  | nil => Forallt_nil _
                  | cons sd c0 => @Forallt_cons _ (fun ab => P (oin_expr ab)) sd c0 (F (oin_expr sd)) (F1 c0)
                  end) el)
              (F ew)
      | OSFW e1 el OTrue (OOrderBy eob sc) =>
        fswf3 _ el _ _ (F (oselect_expr e1))
              ((fix F1 (r : list oql_in_expr) : Forallt (fun ab => P (oin_expr ab)) r :=
                  match r as c0 with
                  | nil => Forallt_nil _
                  | cons sd c0 => @Forallt_cons _ (fun ab => P (oin_expr ab)) sd c0 (F (oin_expr sd)) (F1 c0)
                  end) el)
              (F eob)
      | OSFW e1 el (OWhere ew) (OOrderBy eob sc) =>
        fswf4 _ el _ _ _ (F (oselect_expr e1))
              ((fix F1 (r : list oql_in_expr) : Forallt (fun ab => P (oin_expr ab)) r :=
                  match r as c0 with
                  | nil => Forallt_nil _
                  | cons sd c0 => @Forallt_cons _ (fun ab => P (oin_expr ab)) sd c0 (F (oin_expr sd)) (F1 c0)
                  end) el)
              (F ew)
              (F eob)
    end.

  Definition oql_expr_ind (P : oql_expr -> Prop)
             (fconst : forall d : data, P (OConst d))
             (fvar : forall v : string, P (OVar v))
             (ftable : forall t : string, P (OTable t))
             (fbinop : forall b : binary_op,
                 forall e1 e2 : oql_expr, P e1 -> P e2 -> P (OBinop b e1 e2))
             (funop : forall u : unary_op,
                 forall e1 : oql_expr, P e1 -> P (OUnop u e1))
             (fswf1 : forall e1 : oql_select_expr, forall el : list oql_in_expr,
                   P (oselect_expr e1) -> Forall (fun ab => P (oin_expr ab)) el -> P (OSFW e1 el OTrue ONoOrder))
             (fswf2 : forall e1 : oql_select_expr, forall el : list oql_in_expr, forall ew : oql_expr,
                   P (oselect_expr e1) -> Forall (fun ab => P (oin_expr ab)) el -> P ew -> P (OSFW e1 el (OWhere ew) ONoOrder))
             (fswf3 : forall e1 : oql_select_expr, forall el : list oql_in_expr, forall eob : oql_expr, forall sc : SortDesc,
                   P (oselect_expr e1) -> Forall (fun ab => P (oin_expr ab)) el -> P eob -> P (OSFW e1 el OTrue (OOrderBy eob sc)))
             (fswf4 : forall e1 : oql_select_expr, forall el : list oql_in_expr, forall ew : oql_expr, forall eob : oql_expr, forall sc : SortDesc,
                   P (oselect_expr e1) -> Forall (fun ab => P (oin_expr ab)) el -> P ew -> P eob -> P (OSFW e1 el (OWhere ew) (OOrderBy eob sc)))
    := fix F (e : oql_expr) : P e :=
    match e as e0 return (P e0) with
      | OConst d => fconst d
      | OVar v => fvar v
      | OTable t => ftable t
      | OBinop b e1 e2 => fbinop b _ _ (F e1) (F e2)
      | OUnop u e1 => funop u _ (F e1)
      | OSFW e1 el OTrue ONoOrder =>
        fswf1 _ el (F (oselect_expr e1))
              ((fix F1 (r : list oql_in_expr) : Forall (fun ab => P (oin_expr ab)) r :=
                  match r as c0 with
                  | nil => Forall_nil _
                  | cons sd c0 => @Forall_cons _ (fun ab => P (oin_expr ab)) sd c0 (F (oin_expr sd)) (F1 c0)
                  end) el)
      | OSFW e1 el (OWhere ew) ONoOrder =>
        fswf2 _ el _ (F (oselect_expr e1))
              ((fix F1 (r : list oql_in_expr) : Forall (fun ab => P (oin_expr ab)) r :=
                  match r as c0 with
                  | nil => Forall_nil _
                  | cons sd c0 => @Forall_cons _ (fun ab => P (oin_expr ab)) sd c0 (F (oin_expr sd)) (F1 c0)
                  end) el)
              (F ew)
      | OSFW e1 el OTrue (OOrderBy eob sc) =>
        fswf3 _ el _ _ (F (oselect_expr e1))
              ((fix F1 (r : list oql_in_expr) : Forall (fun ab => P (oin_expr ab)) r :=
                  match r as c0 with
                  | nil => Forall_nil _
                  | cons sd c0 => @Forall_cons _ (fun ab => P (oin_expr ab)) sd c0 (F (oin_expr sd)) (F1 c0)
                  end) el)
              (F eob)
      | OSFW e1 el (OWhere ew) (OOrderBy eob sc) =>
        fswf4 _ el _ _ _ (F (oselect_expr e1))
              ((fix F1 (r : list oql_in_expr) : Forall (fun ab => P (oin_expr ab)) r :=
                  match r as c0 with
                  | nil => Forall_nil _
                  | cons sd c0 => @Forall_cons _ (fun ab => P (oin_expr ab)) sd c0 (F (oin_expr sd)) (F1 c0)
                  end) el)
              (F ew)
              (F eob)
    end.

  Definition oql_expr_rec (P:oql_expr->Set) := oql_expr_rect P.
  
  Lemma oql_expr_ind2 (P : oql_expr -> Prop)
             (fconst : forall d : data, P (OConst d))
             (fvar : forall v : string, P (OVar v))
             (ftable : forall t : string, P (OTable t))
             (fbinop : forall b : binary_op,
                 forall e1 e2 : oql_expr, P e1 -> P e2 -> P (OBinop b e1 e2))
             (funop : forall u : unary_op,
                 forall e1 : oql_expr, P e1 -> P (OUnop u e1))
             (fswf1 : forall e1 : oql_select_expr, forall el : list oql_in_expr,
                   P (oselect_expr e1) -> (forall ab, In ab el -> P (oin_expr ab)) -> P (OSFW e1 el OTrue ONoOrder))
             (fswf2 : forall e1 : oql_select_expr, forall el : list oql_in_expr, forall ew : oql_expr,
                     P (oselect_expr e1) -> (forall ab, In ab el -> P (oin_expr ab)) -> P ew -> P (OSFW e1 el (OWhere ew) ONoOrder))
             (fswf3 : forall e1 : oql_select_expr, forall el : list oql_in_expr, forall eob : oql_expr, forall sc : SortDesc,
                   P (oselect_expr e1) -> (forall ab, In ab el -> P (oin_expr ab)) -> P eob -> P (OSFW e1 el OTrue (OOrderBy eob sc)))
             (fswf4 : forall e1 : oql_select_expr, forall el : list oql_in_expr, forall ew : oql_expr, forall eob : oql_expr, forall sc : SortDesc,
                     P (oselect_expr e1) -> (forall ab, In ab el -> P (oin_expr ab)) -> P ew -> P eob -> P (OSFW e1 el (OWhere ew) (OOrderBy eob sc))) :
    forall e, P e.

  Global Instance oql_expr_eqdec : EqDec oql_expr eq.

  Global Instance oql_select_expr_eqdec : EqDec oql_select_expr eq.

  Global Instance oql_in_expr_eqdec : EqDec oql_in_expr eq.

  Global Instance oql_where_expr_eqdec : EqDec oql_where_expr eq.

  Global Instance oql_order_by_expr_eqdec : EqDec oql_order_by_expr eq.

  Global Instance oql_query_program_eqdec : EqDec oql_query_program eq.

  Global Instance oql_eqdec : EqDec oql eq.


  Definition oql_env := list (string * data).

  Context (h:brand_relation_t).
  Section sem.
    Context (constant_env:list (string*data)).

    Definition env_map_concat_single (a:oql_env) (xl:list oql_env) : list oql_env :=
      map (fun x => rec_concat_sort a x) xl.

    Definition oenv_map_concat_single
               (v:string)
               (f:oql_env -> option data)
               (a:oql_env) : option (list oql_env) :=
      match f a with
      | Some (dcoll y) => Some (env_map_concat_single a (map (fun x => ((v,x)::nil)) y))
      | _ => None
      end.

    Definition filter_cast (b:brands) (l:list data) :=
      let apply_cast x :=
          match x with
          | dbrand b' _ =>
            if (sub_brands_dec h b' b)
            then Some (x :: nil)
            else Some nil
          | _ => None
          end
      in
      lift_flat_map apply_cast l.

    Definition oenv_map_concat_single_with_cast
               (v:string)
               (brands:list string)
               (f:oql_env -> option data)
               (a:oql_env) : option (list oql_env) :=
      match f a with
      | Some (dcoll y) =>
        match filter_cast brands y with
        | Some y =>
          Some (env_map_concat_single a (map (fun x => ((v,x)::nil)) y))
        | None => None
        end
      | _ => None
      end.

    Definition env_map_concat
               (v:string)
               (f:oql_env -> option data)
               (d:list oql_env) : option (list oql_env) :=
      lift_flat_map (oenv_map_concat_single v f) d.

    Definition env_map_concat_cast
               (v:string)
               (brands:list string)
               (f:oql_env -> option data)
               (d:list oql_env) : option (list oql_env) :=
      lift_flat_map (oenv_map_concat_single_with_cast v brands f) d.

    Fixpoint oql_expr_interp (q:oql_expr) (env:oql_env) : option data :=
      match q with
      | OConst d => Some (normalize_data h d)
      | OVar n => edot env n
      | OTable t => edot constant_env t
      | OBinop bop q1 q2 =>
        olift2 (fun d1 d2 => binary_op_eval h bop d1 d2)
               (oql_expr_interp q1 env)
               (oql_expr_interp q2 env)
      | OUnop uop q1 =>
        olift (fun d1 => unary_op_eval h uop d1) (oql_expr_interp q1 env)
      | OSFW select_clause from_clause where_clause order_by_clause =>
        let init_env := Some (env :: nil) in
        let from_interp (envl:option (list oql_env)) (from_in_expr : oql_in_expr) :=
            match from_in_expr with
            | OIn in_v from_expr =>
              match envl with
              | None => None
              | Some envl' =>
                env_map_concat in_v (oql_expr_interp from_expr) envl'
              end
            | OInCast in_v brands from_expr =>
              match envl with
              | None => None
              | Some envl' =>
                env_map_concat_cast in_v brands (oql_expr_interp from_expr) envl'
              end
            end
        in
        let from_result := fold_left from_interp from_clause init_env in
        let pred (where_expr:oql_expr) (x':oql_env) :=
            match oql_expr_interp where_expr x' with
            | Some (dbool b) => Some b
            | _ => None
            end
        in
        let where_result :=
            match where_clause with
            | OTrue => from_result
            | OWhere where_expr => olift (lift_filter (pred where_expr)) from_result
            end
        in
        let order_by_result :=
            match order_by_clause with
            | ONoOrder => where_result
            | OOrderBy order_expr sc =>
              match where_result with
              | Some where_value =>
                let crit1 order_expr sc env :=
                    olift sdata_of_data (oql_expr_interp order_expr env)
                in
                table_sort (crit1 order_expr sc :: nil) where_value
              | None => None
              end
            end
        in
        let select_result :=
            match select_clause with
            | OSelect select_expr =>
              olift (fun x => lift dcoll (lift_map (oql_expr_interp select_expr) x))
                    order_by_result
            | OSelectDistinct select_expr =>
              let select_dup :=
                  olift (fun x => (lift_map (oql_expr_interp select_expr) x))
                        order_by_result
              in
              lift (fun x => dcoll ((@bdistinct data data_eq_dec) x)) select_dup
            end
        in
        select_result
      end.

  End sem.

  Section sem2.
    Context (constant_env:list (string*data)).
    Fixpoint oql_query_program_interp (defls:list (string*data))
             (oq:oql_query_program) : option data :=
      match oq with
      | ODefineQuery s e rest =>
        olift
          (fun d => oql_query_program_interp (rec_concat_sort defls ((s,d)::nil)) rest)
          (oql_expr_interp (rec_concat_sort constant_env defls) e nil)
      | OUndefineQuery s rest => oql_query_program_interp (rremove defls s) rest
      | OQuery e => oql_expr_interp (rec_concat_sort constant_env defls) e nil
      end.

    Definition oql_interp (e:oql) : option data
      := oql_query_program_interp nil e.

  End sem2.

  Section OQLScope.

    Fixpoint oql_free_vars (e:oql_expr) :=
      match e with
      | OConst d => nil
      | OVar v => v :: nil
      | OTable t => nil
      | OBinop bop e1 e2 => oql_free_vars e1 ++ oql_free_vars e2
      | OUnop uop e1 => oql_free_vars e1
      | OSFW se el we oe =>
        let one_step_scope (in_expr : oql_in_expr) previous_free_vars :=
            match in_expr with
            | OIn x e1 => oql_free_vars e1 ++ remove string_eqdec x previous_free_vars
            | OInCast x _ e1 => oql_free_vars e1 ++ remove string_eqdec x previous_free_vars
            end
        in
        fold_right one_step_scope
                   (oql_select_free_vars se
                                         ++ oql_where_free_vars we
                                         ++ oql_order_free_vars oe) el
      end
    with oql_select_free_vars (se:oql_select_expr) :=
      match se with
      | OSelect e => oql_free_vars e
      | OSelectDistinct e => oql_free_vars e
      end
    with oql_where_free_vars (we:oql_where_expr) :=
      match we with
      | OTrue => nil
      | OWhere e => oql_free_vars e
      end
    with oql_order_free_vars (oe:oql_order_by_expr) :=
      match oe with
      | ONoOrder => nil
      | OOrderBy e _ => oql_free_vars e
      end.

    Fixpoint oql_subst (e:oql_expr) (x:string) (e':oql_expr) : oql_expr :=
      match e with
      | OConst d => OConst d
      | OVar y => if y == x then e' else OVar y
      | OTable t => OTable t
      | OBinop bop e1 e2 => OBinop bop
                                   (oql_subst e1 x e')
                                   (oql_subst e2 x e')
      | OUnop uop e1 => OUnop uop (oql_subst e1 x e')
      | OSFW se el we oe =>
        let for_vars := map (fun x => match x with OIn v _ | OInCast v _ _ => v end) el in
        let el' :=
            (fix F (el:list oql_in_expr) (x:string) (e':oql_expr) :=
              match el with
              | nil => nil
              | (OIn y e) :: el' =>
                if (y == x)
                then (OIn y (oql_subst e x e')) :: el'
                else (OIn y (oql_subst e x e')) :: (F el' x e')
              | (OInCast y brand_name e) :: el' =>
                if (y == x)
                then (OInCast y brand_name (oql_subst e x e')) :: el'
                else (OInCast y brand_name (oql_subst e x e')) :: (F el' x e')
              end) el x e'
        in
        if in_dec string_dec x for_vars
        then OSFW se el' we oe
        else OSFW (oql_select_subst se x e') el'
                  (oql_where_subst we x e')
                  (oql_order_subst oe x e')
      end
    with oql_select_subst (se:oql_select_expr) (x:string) (e':oql_expr) :=
      match se with
      | OSelect e => OSelect (oql_subst e x e')
      | OSelectDistinct e => OSelectDistinct (oql_subst e x e')
      end
    with oql_where_subst (we:oql_where_expr) (x:string) (e':oql_expr) :=
      match we with
      | OTrue => OTrue
      | OWhere e => OWhere (oql_subst e x e')
      end
    with oql_order_subst (we:oql_order_by_expr) (x:string) (e':oql_expr) :=
      match we with
      | ONoOrder => ONoOrder
      | OOrderBy e sc => OOrderBy (oql_subst e x e') sc
      end.
    
  Fixpoint oql_query_program_defls
             (oq:oql_query_program) : list string :=
      match oq with
      | ODefineQuery s e rest => s::(oql_query_program_defls rest)
      | OUndefineQuery s rest => s::(oql_query_program_defls rest)
      | OQuery e => nil
      end.

  End OQLScope.

  Section Top.
    Definition oql_eval_top (q:oql) (cenv:bindings) : option data :=
      oql_interp (rec_sort cenv) q.
  End Top.
End OQL.


Notation "‵‵ c" := (OConst (dconst c)) (at level 0) : oql_scope.
Notation "‵ c" := (OConst c) (at level 0) : oql_scope.
Notation "‵{||}" := (OConst (dcoll nil)) (at level 0) : oql_scope.
Notation "‵[||]" := (OConst (drec nil)) (at level 50) : oql_scope.

Notation "r1 ∧ r2" := (OBinop OpAnd r1 r2) (right associativity, at level 65): oql_scope.
Notation "r1 ∨ r2" := (OBinop OpOr r1 r2) (right associativity, at level 70): oql_scope.
Notation "r1 ≐ r2" := (OBinop OpEqual r1 r2) (right associativity, at level 70): oql_scope.
Notation "r1 ≤ r2" := (OBinop OpLe r1 r2) (no associativity, at level 70): oql_scope.
Notation "r1 ⋃ r2" := (OBinop OpBagUnion r1 r2) (right associativity, at level 70): oql_scope.
Notation "r1 − r2" := (OBinop OpBagDiff r1 r2) (right associativity, at level 70): oql_scope.
Notation "r1 ♯min r2" := (OBinop OpBagMin r1 r2) (right associativity, at level 70): oql_scope.
Notation "r1 ♯max r2" := (OBinop OpBagMax r1 r2) (right associativity, at level 70): oql_scope.
Notation "p ⊕ r" := ((OBinop OpRecConcat) p r) (at level 70) : oql_scope.
Notation "p ⊗ r" := ((OBinop OpRecMerge) p r) (at level 70) : oql_scope.

Notation "¬( r1 )" := (OUnop OpNeg r1) (right associativity, at level 70): oql_scope.
Notation "ε( r1 )" := (OUnop OpDistinct r1) (right associativity, at level 70): oql_scope.
Notation "♯count( r1 )" := (OUnop OpCount r1) (right associativity, at level 70): oql_scope.
Notation "♯flatten( d )" := (OUnop OpFlatten d) (at level 50) : oql_scope.
Notation "‵{| d |}" := ((OUnop OpBag) d) (at level 50) : oql_scope.
Notation "‵[| ( s , r ) |]" := ((OUnop (OpRec s)) r) (at level 50) : oql_scope.
Notation "¬π[ s1 ]( r )" := ((OUnop (OpRecRemove s1)) r) (at level 50) : oql_scope.
Notation "p · r" := ((OUnop (OpDot r)) p) (left associativity, at level 40): oql_scope.

Notation "'$' v" := (OVar v%string) (at level 50, format "'$' v") : oql_scope.
Notation "'$$' v" := (OTable v%string) (at level 50, format "'$$' v") : oql_scope.

Notation "'SELECT' e1 'FROM' e2 'WHERE' e3" := (OSFW (OSelect e1) e2 e3) (at level 50, format "'SELECT' e1 'FROM' e2 'WHERE' e3") : oql_scope.
Notation "'SELECT' 'DISTINCT' e1 'FROM' e2 'WHERE' e3" := (OSFW (OSelectDistinct e1) e2 e3) (at level 50, format "'SELECT' 'DISTINCT' e1 'FROM' e2 'WHERE' e3") : oql_scope.
Notation "e 'IN' x" := (OIn e x) (at level 50, format "e 'IN' x") : oql_scope.

Tactic Notation "oql_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "OConst"%string
  | Case_aux c "OVar"%string
  | Case_aux c "OTable"%string
  | Case_aux c "OBinop"%string
  | Case_aux c "OUnop"%string
  | Case_aux c "OSFW"%string ].