Qcert.Translation.OQLtoNRAEnv

Section OQLtoNRAEnv.




  Context {fruntime:foreign_runtime}.

  Section query_var.
    Context (deflist:list string).


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

  Fixpoint nraenv_of_oql_expr (e:oql_expr) : nraenv :=
    match e with
    | OConst d ⇒ NRAEnvConst d
    | OVar v ⇒ NRAEnvUnop (ADot v) NRAEnvID
    | OTable t ⇒ lookup_table t
    | OBinop b e1 e2 ⇒ NRAEnvBinop b (nraenv_of_oql_expr e1) (nraenv_of_oql_expr e2)
    | OUnop u e1 ⇒ NRAEnvUnop u (nraenv_of_oql_expr e1)
    | OSFW select_clause from_clause where_clause order_clause ⇒
      let nraenv_of_from (opacc:nraenv) (from_in_expr : oql_in_expr) :=
          match from_in_expr with
            | OIn in_v from_expr ⇒
              NRAEnvMapConcat (NRAEnvMap (NRAEnvUnop (ARec in_v) NRAEnvID) (nraenv_of_oql_expr from_expr)) opacc
            | OInCast in_v brand_name from_expr ⇒
              NRAEnvMapConcat (NRAEnvMap (NRAEnvUnop (ARec in_v) NRAEnvID)
                                 (NRAEnvUnop AFlatten
                                         (NRAEnvMap
                                            (NRAEnvEither (NRAEnvUnop AColl NRAEnvID)
                                                      (NRAEnvConst (dcoll nil)))
                                            (NRAEnvMap (NRAEnvUnop (ACast (brand_name::nil)) NRAEnvID)
                                                   (nraenv_of_oql_expr from_expr))
                                         )))
                          opacc
          end
      in
      let nraenv_of_from_clause :=
          fold_left nraenv_of_from from_clause (NRAEnvUnop AColl NRAEnvID)
      in
      let nraenv_of_where_clause :=
          match where_clause with
          | OTrue ⇒ nraenv_of_from_clause
          | OWhere where_expr ⇒
            NRAEnvSelect (nraenv_of_oql_expr where_expr) nraenv_of_from_clause
          end
      in
      let nraenv_of_order_clause :=
          match order_clause with
          | ONoOrder ⇒ nraenv_of_where_clause
          | OOrderBy e sc ⇒ nraenv_of_where_clause
          end
      in
      match select_clause with
      | OSelect select_expr ⇒
        NRAEnvMap (nraenv_of_oql_expr select_expr) nraenv_of_order_clause
      | OSelectDistinct select_expr ⇒
        NRAEnvUnop ADistinct (NRAEnvMap (nraenv_of_oql_expr select_expr) nraenv_of_order_clause)
      end
    end.

  End query_var.

  Fixpoint nraenv_of_oql_query_program
               (defllist:list string) (oq:oql_query_program) : nraenv
    := match oq with
       | ODefineQuery s e rest ⇒
         NRAEnvAppEnv
              (nraenv_of_oql_query_program (s::defllist) rest)
              (NRAEnvBinop AConcat
                      NRAEnvEnv
                      (NRAEnvUnop (ARec s)
                                  (nraenv_of_oql_expr defllist e)))
       | OUndefineQuery s rest ⇒
         NRAEnvAppEnv
           (nraenv_of_oql_query_program (remove_all s defllist) rest)
           (NRAEnvUnop (ARecRemove s) NRAEnvEnv)
       | OQuery q ⇒
         nraenv_of_oql_expr defllist q
       end.

  Definition nraenv_of_oql (q:oql) : nraenv
    := NRAEnvAppEnv
         (NRAEnvApp (nraenv_of_oql_query_program nil q)
                    (NRAEnvConst (drec nil)))
         (NRAEnvConst (drec nil)).

  Definition translate_oql_to_nraenv (q:oql) : nraenv :=
    nraenv_of_oql q.



  Lemma rmap_rec_concat_map_is_map_rec_concat_map a s l1 :
    rmap
      (fun x : data ⇒
         match x with
         | dunit ⇒ None
         | dnat _ ⇒ None
         | dbool _ ⇒ None
         | dstring _ ⇒ None
         | dcoll _ ⇒ None
         | drec r1 ⇒ Some (drec (rec_concat_sort a r1))
         | dleft _ ⇒ None
         | dright _ ⇒ None
         | dbrand _ _ ⇒ None
         | dforeign _ ⇒ None
         end) (map (fun d : data ⇒ drec ((s, d) :: nil)) l1) =
    Some (map (fun x : list (string × data) ⇒ drec (rec_concat_sort a x))
              (map (fun x : data ⇒ (s, x) :: nil) l1)).

  Lemma flatten_either_is_rmap_either h bn l0:
    (olift rflatten
           (olift
              (rmap
                 (fun x : data ⇒
                    match x with
                    | dunit ⇒ None
                    | dnat _ ⇒ None
                    | dbool _ ⇒ None
                    | dstring _ ⇒ None
                    | dcoll _ ⇒ None
                    | drec _ ⇒ None
                    | dleft dl ⇒ Some (dcoll (dl :: nil))
                    | dright _ ⇒ Some (dcoll nil)
                    | dbrand _ _ ⇒ None
                    | dforeign _ ⇒ None
                    end))
              (rmap
                 (fun x : data ⇒
                    match x with
                    | dunit ⇒ None
                    | dnat _ ⇒ None
                    | dbool _ ⇒ None
                    | dstring _ ⇒ None
                    | dcoll _ ⇒ None
                    | drec _ ⇒ None
                    | dleft _ ⇒ None
                    | dright _ ⇒ None
                    | dbrand b' _ ⇒
                      if sub_brands_dec h b' (bn :: nil)
                      then Some (dsome x)
                      else Some dnone
                    | dforeign _ ⇒ None
                    end) l0))) =
    oflat_map
      (fun x : data ⇒
         match x with
         | dunit ⇒ None
         | dnat _ ⇒ None
         | dbool _ ⇒ None
         | dstring _ ⇒ None
         | dcoll _ ⇒ None
         | drec _ ⇒ None
         | dleft _ ⇒ None
         | dright _ ⇒ None
         | dbrand b' _ ⇒
           if sub_brands_dec h b' (bn :: nil)
           then Some (x :: nil)
           else Some nil
         | dforeign _ ⇒ None
         end) l0.

  Lemma map_map_drec_works s a l1 l2:
    dcoll
      (map (fun x : list (string × data) ⇒ drec (rec_concat_sort a x))
           (map (fun x : data ⇒ (s, x) :: nil) l1) ++
           map drec l2) =
    (dcoll
       (map drec
            (map (fun x : list (string × data) ⇒ rec_concat_sort a x)
                 (map (fun x : data ⇒ (s, x) :: nil) l1) ++ l2))).

  Lemma push_lift_coll_in_rmap l f :
    olift (fun x0 : list oql_env ⇒ lift dcoll (rmap f x0)) l =
    lift dcoll (olift (fun x0 : list oql_env ⇒ (rmap f x0)) l).

  Lemma olift_rondcoll_over_dcoll l f :
    (olift (fun d : data ⇒ rondcoll f d) (lift dcoll l)) =
    (lift (fun x : list data ⇒ dcoll (f x)) l).

  Lemma map_env_with_drec (s:string) (l:list data) :
    (map (fun d : data ⇒ drec ((s, d) :: nil)) l) =
    (map drec (map (fun x : data ⇒ (s, x) :: nil) l)).

  Lemma pull_drec_from_map_concat (s:string) env l :
    Some (map drec
              (env_map_concat_single env (map (fun x : data ⇒ (s, x) :: nil) l))) =
    omap_concat (drec env) (map drec (map (fun x : data ⇒ (s, x) :: nil) l)).

  Lemma oql_nra_dual_map_concat (s:string) env l:
    Some
      (dcoll
         (map drec
              (env_map_concat_single env
                                     (map (fun x : data ⇒ (s, x) :: nil) l)))) =
    lift dcoll
         match
           omap_concat (drec env)
                       (map (fun d : data ⇒ drec ((s, d) :: nil)) l)
         with
         | Some x' ⇒ Some (x' ++ nil)
         | None ⇒ None
         end.

  Lemma rmap_orecconcat_rmap_drec s a l0 :
    rmap (fun x : data ⇒ orecconcat (drec a) x)
         (map (fun d : data ⇒ drec ((s, d) :: nil)) l0) =
    Some (map (fun d : data ⇒ drec (rec_concat_sort a ((s,d)::nil))) l0).

  Lemma map_drec_app s a l0 l1:
    map (fun d : data ⇒ drec (rec_concat_sort a ((s, d) :: nil))) l0 ++
        map drec l1 =
    map drec
        (map (fun x : list (string × data) ⇒ rec_concat_sort a x)
             (map (fun x : data ⇒ (s, x) :: nil) l0) ++ l1).


  Context (h:brand_relation_t).
  Context (constant_env:list (string×data)).

  Lemma nraenv_of_select_expr_correct defls
        (o:oql_expr) xenv (env0 : option (list oql_env)) :
    (∀ xenv (env : oql_env),
        oql_expr_interp h (rec_concat_sort constant_env defls) o env =
        (h ⊢ nraenv_of_oql_expr (domain defls) o @ₓ (drec env) ⊣ constant_env; (drec (rec_concat_sort xenv defls)))%nraenv) →
    olift (fun x0 : list oql_env ⇒ lift dcoll (rmap (oql_expr_interp h (rec_concat_sort constant_env defls) o) x0)) env0 =
    olift
      (fun d : data ⇒
         lift_oncoll
           (fun c1 : list data ⇒
              lift dcoll
                   (rmap
                      (nraenv_eval h constant_env (nraenv_of_oql_expr (domain defls) o) (drec (rec_concat_sort xenv defls)))
                      c1)) d) (lift (fun x ⇒ dcoll (map drec x)) env0).


  Lemma one_from_fold_step_is_map_concat defls s o op xenv envs envs0:
    (h ⊢ op @ₓ envs ⊣ constant_env ; (drec (rec_concat_sort xenv defls)))%nraenv =
    lift (fun x : list (list (string × data)) ⇒ dcoll (map drec x)) envs0 →
    (∀ xenv0 (env : oql_env),
       oql_expr_interp h (rec_concat_sort constant_env defls) o env =
       (h ⊢ nraenv_of_oql_expr (domain defls) o @ₓ drec env ⊣ constant_env; (drec (rec_concat_sort xenv0 defls)))%nraenv) →
    ((h ⊢ (NRAEnvMapConcat (NRAEnvMap (NRAEnvUnop (ARec s) NRAEnvID) (nraenv_of_oql_expr (domain defls) o)) op) @ₓ envs ⊣ constant_env; (drec (rec_concat_sort xenv defls)))%nraenv =
     lift (fun x : list (list (string × data)) ⇒ dcoll (map drec x))
          (match envs0 with
           | Some envl' ⇒
             env_map_concat s (oql_expr_interp h (rec_concat_sort constant_env defls) o) envl'
           | None ⇒ None
           end)).


  Lemma one_from_cast_fold_step_is_map_concat_cast defls s bn o op xenv envs envs0:
    (h ⊢ op @ₓ envs ⊣ constant_env; (drec (rec_concat_sort xenv defls)))%nraenv =
    lift (fun x : list (list (string × data)) ⇒ dcoll (map drec x)) envs0 →
    (∀ xenv0 (env : oql_env),
       oql_expr_interp h (rec_concat_sort constant_env defls) o env =
       (h ⊢ nraenv_of_oql_expr (domain defls) o @ₓ drec env ⊣ constant_env; (drec (rec_concat_sort xenv0 defls)))%nraenv) →
    ((h ⊢ (NRAEnvMapConcat
             (NRAEnvMap
                (NRAEnvUnop (ARec s) NRAEnvID)
                (NRAEnvUnop AFlatten(
                              NRAEnvMap (NRAEnvEither (NRAEnvUnop AColl NRAEnvID)
                                                      (NRAEnvConst (dcoll nil)))
                                        (NRAEnvMap (NRAEnvUnop (ACast (bn :: nil)) NRAEnvID)
                                                   (nraenv_of_oql_expr (domain defls) o))))) op) @ₓ envs
        ⊣ constant_env; (drec (rec_concat_sort xenv defls)))%nraenv
     =
     lift (fun x : list (list (string × data)) ⇒ dcoll (map drec x))
          match envs0 with
          | Some envl' ⇒
            env_map_concat_cast h s bn (oql_expr_interp h (rec_concat_sort constant_env defls) o) envl'
          | None ⇒ None
          end).


  Lemma nraenv_of_from_in_correct defls env o s xenv :
    (∀ xenv0 (env0 : oql_env),
        oql_expr_interp h (rec_concat_sort constant_env defls) o env0 =
        (h ⊢ nraenv_of_oql_expr (domain defls) o @ₓ drec env0 ⊣ constant_env; (drec (rec_concat_sort xenv0 defls)))%nraenv) →
    (lift (fun x : list (list (string × data)) ⇒ dcoll (map drec x))
          (env_map_concat s (oql_expr_interp h (rec_concat_sort constant_env defls) o) (env :: nil))) =
    (nraenv_eval h constant_env (NRAEnvMapConcat (NRAEnvMap (NRAEnvUnop (ARec s) NRAEnvID) (nraenv_of_oql_expr (domain defls) o)) (NRAEnvUnop AColl NRAEnvID)) (drec (rec_concat_sort xenv defls)) (drec env)).


  Lemma nraenv_of_from_clause_correct defls op envs envs0 el xenv :
    Forall
      (fun ab : oql_in_expr ⇒
         ∀ xenv (env : oql_env),
           oql_expr_interp h (rec_concat_sort constant_env defls) (oin_expr ab) env =
           (h ⊢ nraenv_of_oql_expr (domain defls) (oin_expr ab) @ₓ drec env ⊣ constant_env;
             (drec (rec_concat_sort xenv defls)))%nraenv) el →
    (h ⊢ op @ₓ envs ⊣ constant_env; (drec (rec_concat_sort xenv defls)))%nraenv =
    (lift (fun x : list (list (string × data)) ⇒ dcoll (map drec x)) envs0) →
    (lift (fun x : list (list (string × data)) ⇒ dcoll (map drec x))
          (fold_left
             (fun (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 h (rec_concat_sort constant_env defls) from_expr) envl'
            end
          | OInCast in_v brand_name from_expr ⇒
            match envl with
            | None ⇒ None
            | Some envl' ⇒
              env_map_concat_cast h in_v brand_name (oql_expr_interp h (rec_concat_sort constant_env defls) from_expr) envl'
            end
          end
             ) el envs0)) =
    (h
       ⊢ fold_left
       (fun (opacc : nraenv) (from_in_expr : oql_in_expr) ⇒
          match from_in_expr with
          | OIn in_v from_expr ⇒
            NRAEnvMapConcat
              (NRAEnvMap (NRAEnvUnop (ARec in_v) NRAEnvID) (nraenv_of_oql_expr (domain defls) from_expr))
              opacc
          | OInCast in_v brand_name from_expr ⇒
            NRAEnvMapConcat
              (NRAEnvMap
                 (NRAEnvUnop (ARec in_v) NRAEnvID)
                 (NRAEnvUnop AFlatten
                             (NRAEnvMap (NRAEnvEither (NRAEnvUnop AColl NRAEnvID)
                                                      (NRAEnvConst (dcoll nil)))
                                        (NRAEnvMap (NRAEnvUnop (ACast (brand_name::nil))
                                                               NRAEnvID)
                                                   (nraenv_of_oql_expr (domain defls) from_expr)))))
              opacc
          end
       )
       el op @ₓ envs ⊣ constant_env; (drec (rec_concat_sort xenv defls)))%nraenv.


  Lemma nraenv_of_where_clause_correct defls
        (o:oql_expr) xenv (ol : option (list oql_env)):
    (∀ xenv (env : oql_env),
        oql_expr_interp h (rec_concat_sort constant_env defls) o env =
        (h ⊢ nraenv_of_oql_expr (domain defls) o @ₓ drec env ⊣ constant_env; (drec (rec_concat_sort xenv defls)))%nraenv) →
    lift (fun x : list (list (string × data)) ⇒ dcoll (map drec x))
         (olift
            (lift_filter
               (fun x' : oql_env ⇒
                  match oql_expr_interp h (rec_concat_sort constant_env defls) o x' with
                  | Some (dbool b) ⇒ Some b
                  | Some _ ⇒ None
                  | None ⇒ None
                  end)) ol) =
    olift
      (fun d : data ⇒
         lift_oncoll
           (fun c1 : list data ⇒
              lift dcoll
                   (lift_filter
                      (fun x' : data ⇒
                         match
                           (h ⊢ nraenv_of_oql_expr (domain defls) o @ₓ x' ⊣ constant_env; (drec (rec_concat_sort xenv defls)))%nraenv
                         with
                         | Some (dbool b) ⇒ Some b
                         | Some _ ⇒ None
                         | None ⇒ None
                         end) c1)) d)
      (lift (fun x : list (list (string × data)) ⇒ dcoll (map drec x)) ol).


  Theorem nraenv_of_oql_expr_correct (e:oql_expr) :
    ∀ xenv, ∀ defls, ∀ env,
        oql_expr_interp h (rec_concat_sort constant_env defls) e env =
        (nraenv_eval h constant_env (nraenv_of_oql_expr (domain defls) e)
                     (drec (rec_concat_sort xenv defls)) (drec env))%nraenv.

  Global Instance lookup_table_proper :
    Proper (equivlist ==> eq ==> eq) lookup_table.

  Global Instance nraenv_of_oql_expr_proper :
    Proper (equivlist ==> eq ==> eq) nraenv_of_oql_expr.

  Global Instance nraenv_of_oql_query_program_proper :
    Proper (equivlist ==> eq ==> eq) nraenv_of_oql_query_program.

  Lemma rec_concat_sort_domain_app_commutatuve_equiv {K} {odt:ODT} {B} l1 l2 :
    (equivlist (domain (rec_concat_sort l1 l2)) (domain l2 ++ @domain K B l1)).

  Lemma nraenv_of_oql_query_program_correct (defllist:list string) (oq:oql_query_program) :
    ∀ (defls:oql_env) xenv env,
      (∀ x, In x ((domain defls)++(oql_query_program_defls oq)) → ¬In x (domain xenv)) →
      oql_query_program_interp h constant_env defls oq env =
      nraenv_eval h constant_env (nraenv_of_oql_query_program (domain defls) oq) (drec (rec_concat_sort xenv defls)) (drec env).

  Theorem nraenv_of_oql_correct (q:oql) :
    ∀ xenv xdata,
      oql_interp h constant_env q =
      nraenv_eval h constant_env (nraenv_of_oql q) xenv xdata.

  Theorem translate_oql_to_nraenv_correct (q:oql) :
    ∀ xenv xdata,
      oql_interp h constant_env q =
      nraenv_eval h constant_env (translate_oql_to_nraenv q) xenv xdata.

End OQLtoNRAEnv.