Qcert.OQL.Lang.OQL

Section OQL.



  Context {fruntime:foreign_runtime}.

  Definition oql_env := list (string × data).


  Inductive oql_expr : Set :=
  | OConst : data → oql_expr
  | OVar : string → oql_expr
  | OTable : string → oql_expr
  | OBinop : binOp → oql_expr → oql_expr → oql_expr
  | OUnop : unaryOp → 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 → 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
  .


  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 : ∀ d : data, P (OConst d))
             (fvar : ∀ v : string, P (OVar v))
             (ftable : ∀ t : string, P (OTable t))
             (fbinop : ∀ b : binOp,
                 ∀ e1 e2 : oql_expr, P e1 → P e2 → P (OBinop b e1 e2))
             (funop : ∀ u : unaryOp,
                 ∀ e1 : oql_expr, P e1 → P (OUnop u e1))
             (fswf1 : ∀ e1 : oql_select_expr, ∀ el : list oql_in_expr,
                   P (oselect_expr e1) → Forallt (fun ab ⇒ P (oin_expr ab)) el → P (OSFW e1 el OTrue ONoOrder))
             (fswf2 : ∀ e1 : oql_select_expr, ∀ el : list oql_in_expr, ∀ 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 : ∀ e1 : oql_select_expr, ∀ el : list oql_in_expr, ∀ eob : oql_expr, ∀ 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 : ∀ e1 : oql_select_expr, ∀ el : list oql_in_expr, ∀ ew : oql_expr, ∀ eob : oql_expr, ∀ 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 : ∀ d : data, P (OConst d))
             (fvar : ∀ v : string, P (OVar v))
             (ftable : ∀ t : string, P (OTable t))
             (fbinop : ∀ b : binOp,
                 ∀ e1 e2 : oql_expr, P e1 → P e2 → P (OBinop b e1 e2))
             (funop : ∀ u : unaryOp,
                 ∀ e1 : oql_expr, P e1 → P (OUnop u e1))
             (fswf1 : ∀ e1 : oql_select_expr, ∀ el : list oql_in_expr,
                   P (oselect_expr e1) → Forall (fun ab ⇒ P (oin_expr ab)) el → P (OSFW e1 el OTrue ONoOrder))
             (fswf2 : ∀ e1 : oql_select_expr, ∀ el : list oql_in_expr, ∀ 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 : ∀ e1 : oql_select_expr, ∀ el : list oql_in_expr, ∀ eob : oql_expr, ∀ 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 : ∀ e1 : oql_select_expr, ∀ el : list oql_in_expr, ∀ ew : oql_expr, ∀ eob : oql_expr, ∀ 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 : ∀ d : data, P (OConst d))
             (fvar : ∀ v : string, P (OVar v))
             (ftable : ∀ t : string, P (OTable t))
             (fbinop : ∀ b : binOp,
                 ∀ e1 e2 : oql_expr, P e1 → P e2 → P (OBinop b e1 e2))
             (funop : ∀ u : unaryOp,
                 ∀ e1 : oql_expr, P e1 → P (OUnop u e1))
             (fswf1 : ∀ e1 : oql_select_expr, ∀ el : list oql_in_expr,
                   P (oselect_expr e1) → (∀ ab, In ab el → P (oin_expr ab)) → P (OSFW e1 el OTrue ONoOrder))
             (fswf2 : ∀ e1 : oql_select_expr, ∀ el : list oql_in_expr, ∀ ew : oql_expr,
                     P (oselect_expr e1) → (∀ ab, In ab el → P (oin_expr ab)) → P ew → P (OSFW e1 el (OWhere ew) ONoOrder))
             (fswf3 : ∀ e1 : oql_select_expr, ∀ el : list oql_in_expr, ∀ eob : oql_expr, ∀ sc : SortDesc,
                   P (oselect_expr e1) → (∀ ab, In ab el → P (oin_expr ab)) → P eob → P (OSFW e1 el OTrue (OOrderBy eob sc)))
             (fswf4 : ∀ e1 : oql_select_expr, ∀ el : list oql_in_expr, ∀ ew : oql_expr, ∀ eob : oql_expr, ∀ sc : SortDesc,
                     P (oselect_expr e1) → (∀ ab, In ab el → P (oin_expr ab)) → P ew → P eob → P (OSFW e1 el (OWhere ew) (OOrderBy eob sc))) :
    ∀ 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.

  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
    oflat_map apply_cast l.

  Definition oenv_map_concat_single_with_cast
             (v:string)
             (brand_name:string)
             (f:oql_env → option data)
             (a:oql_env) : option (list oql_env) :=
    match f a with
    | Some (dcoll y) ⇒
      match filter_cast (brand_name::nil) 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) :=
    oflat_map (oenv_map_concat_single v f) d.

  Definition env_map_concat_cast
             (v:string)
             (brand_name:string)
             (f:oql_env → option data)
             (d:list oql_env) : option (list oql_env) :=
    oflat_map (oenv_map_concat_single_with_cast v brand_name 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 ⇒ fun_of_binop h bop d1 d2) (oql_expr_interp q1 env) (oql_expr_interp q2 env)
    | OUnop uop q1 ⇒ olift (fun d1 ⇒ fun_of_unaryop 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 brand_name from_expr ⇒
            match envl with
            | None ⇒ None
            | Some envl' ⇒
              env_map_concat_cast in_v brand_name (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 scl e ⇒ where_result
          end
      in
      let select_result :=
          match select_clause with
          | OSelect select_expr ⇒
            olift (fun x ⇒ lift dcoll (rmap (oql_expr_interp select_expr) x))
                  order_by_result
          | OSelectDistinct select_expr ⇒
            let select_dup :=
                olift (fun x ⇒ (rmap (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) (env:oql_env) : option data :=
      match oq with
      | ODefineQuery s e rest ⇒
        olift
          (fun d ⇒ oql_query_program_interp (rec_concat_sort defls ((s,d)::nil)) rest env)
          (oql_expr_interp (rec_concat_sort constant_env defls) e env)
      | OUndefineQuery s rest ⇒
        oql_query_program_interp (rremove defls s) rest env
    | OQuery e ⇒ oql_expr_interp (rec_concat_sort constant_env defls) e env
      end.

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

  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.

End OQL.