Qcert.NNRC.Lang.NNRC


Section NNRC.





Named Nested Relational Calculus - Extended

  Context {fruntime:foreign_runtime}.
  Context {h:brand_relation_t}.

  Section macros.
e groupbyg,keys == LET group3 = πkeys) THEN {group3 ∈ group2 ∈ ♯distinct({ πkeys(group1 ∈
    Definition nnrc_group_by (g:string) (sl:list string) (e:nnrc) : nnrc :=
      let t0 := "$group0"%string in
      let t1 := "$group1"%string in
      let t2 := "$group2"%string in
      let t3 := "$group3"%string in
      NNRCLet t0 e
             (NNRCFor t2
                     (NNRCUnop ADistinct
                              (NNRCFor t1 (NNRCVar t0) (NNRCUnop (ARecProject sl) (NNRCVar t1))))
                     (NNRCBinop AConcat
                               (NNRCUnop (ARec g)
                                        (NNRCUnop AFlatten
                                                 (NNRCFor t3 (NNRCVar t0)
                                                          (NNRCIf (NNRCBinop AEq (NNRCUnop (ARecProject sl) (NNRCVar t3)) (NNRCVar t2))
                                                                  (NNRCUnop AColl (NNRCVar t3))
                                                                  (NNRCConst (dcoll nil))))))
                               (NNRCVar t2))).

    Lemma nnrc_group_by_correct env
          (g:string) (sl:list string)
          (e:nnrc)
          (incoll outcoll:list data):
      nnrc_core_eval h env e = Some (dcoll incoll) →
      group_by_nested_eval_table g sl incoll = Some outcoll →
      nnrc_core_eval h env (nnrc_group_by g sl e) = Some (dcoll outcoll).

    Definition nnrc_group_by_from_nraenv (vid venv:var) (g:string) (sl:list string) (e:nnrc) :=
    (NNRCLet (fresh_var "tappe$" (vid :: venv :: nil))
       (NNRCUnop (ARec "$pregroup") e)
       (NNRCFor
          (fresh_var "tmap$"
             (vid :: fresh_var "tappe$" (vid :: venv :: nil) :: nil))
          (NNRCUnop ADistinct
             (NNRCFor
                (fresh_var "tmap$"
                   (vid :: fresh_var "tappe$" (vid :: venv :: nil) :: nil))
                (NNRCUnop (ADot "$pregroup")
                   (NNRCVar (fresh_var "tappe$" (vid :: venv :: nil))))
                (NNRCUnop (ARecProject sl)
                   (NNRCVar
                      (fresh_var "tmap$"
                         (vid
                          :: fresh_var "tappe$" (vid :: venv :: nil)
                             :: nil))))))
          (NNRCBinop AConcat
             (NNRCUnop (ARec g)
                (NNRCLet
                   (fresh_var "tappe$"
                      (fresh_var "tmap$"
                         (vid
                          :: fresh_var "tappe$" (vid :: venv :: nil)
                             :: nil)
                       :: fresh_var "tappe$" (vid :: venv :: nil) :: nil))
                   (NNRCBinop AConcat
                      (NNRCUnop (ARec "$key")
                         (NNRCVar
                            (fresh_var "tmap$"
                               (vid
                                :: fresh_var "tappe$" (vid :: venv :: nil)
                                   :: nil))))
                      (NNRCVar (fresh_var "tappe$" (vid :: venv :: nil))))
                   (NNRCUnop AFlatten
                      (NNRCFor
                         (fresh_var "tsel$"
                            (fresh_var "tmap$"
                               (vid
                                :: fresh_var "tappe$" (vid :: venv :: nil)
                                   :: nil)
                             :: fresh_var "tappe$"
                                  (fresh_var "tmap$"
                                     (vid
                                      :: fresh_var "tappe$"
                                           (vid :: venv :: nil) :: nil)
                                   :: fresh_var "tappe$"
                                        (vid :: venv :: nil) :: nil)
                                :: nil))
                         (NNRCUnop (ADot "$pregroup")
                            (NNRCVar
                               (fresh_var "tappe$"
                                  (fresh_var "tmap$"
                                     (vid
                                      :: fresh_var "tappe$"
                                           (vid :: venv :: nil) :: nil)
                                   :: fresh_var "tappe$"
                                        (vid :: venv :: nil) :: nil))))
                         (NNRCIf
                            (NNRCBinop AEq
                               (NNRCUnop (ARecProject sl)
                                  (NNRCVar
                                     (fresh_var "tsel$"
                                        (fresh_var "tmap$"
                                           (vid
                                            :: fresh_var "tappe$"
                                                (vid :: venv :: nil)
                                               :: nil)
                                         :: fresh_var "tappe$"
                                              (fresh_var "tmap$"
                                                (vid
                                                ::
                                                fresh_var "tappe$"
                                                (vid :: venv :: nil)
                                                :: nil)
                                               ::
                                               fresh_var "tappe$"
                                                (vid :: venv :: nil)
                                               :: nil) :: nil))))
                               (NNRCUnop (ADot "$key")
                                  (NNRCVar
                                     (fresh_var "tappe$"
                                        (fresh_var "tmap$"
                                           (vid
                                            :: fresh_var "tappe$"
                                                (vid :: venv :: nil)
                                               :: nil)
                                         :: fresh_var "tappe$"
                                              (vid :: venv :: nil) :: nil)))))
                            (NNRCUnop AColl
                               (NNRCVar
                                  (fresh_var "tsel$"
                                     (fresh_var "tmap$"
                                        (vid
                                         :: fresh_var "tappe$"
                                              (vid :: venv :: nil) :: nil)
                                      :: fresh_var "tappe$"
                                           (fresh_var "tmap$"
                                              (vid
                                               ::
                                               fresh_var "tappe$"
                                                (vid :: venv :: nil)
                                               :: nil)
                                            :: fresh_var "tappe$"
                                                (vid :: venv :: nil)
                                               :: nil) :: nil))))
                            (NNRCConst (dcoll nil)))))))
             (NNRCVar
                (fresh_var "tmap$"
                   (vid :: fresh_var "tappe$" (vid :: venv :: nil) :: nil)))))).

    Lemma rmap1 sl l :
      (rmap
         (fun d1 : data ⇒
            match d1 with
            | dunit ⇒ None
            | dnat _ ⇒ None
            | dbool _ ⇒ None
            | dstring _ ⇒ None
            | dcoll _ ⇒ None
            | drec r ⇒ Some (drec (rproject r sl))
            | dleft _ ⇒ None
            | dright _ ⇒ None
            | dbrand _ _ ⇒ None
            | dforeign _ ⇒ None
            end) l) =
      (rmap
         (fun d1 : data ⇒
            olift
              (fun d0 : data ⇒
                 match d0 with
                 | dunit ⇒ None
                 | dnat _ ⇒ None
                 | dbool _ ⇒ None
                 | dstring _ ⇒ None
                 | dcoll _ ⇒ None
                 | drec r ⇒ Some (drec (rproject r sl))
                 | dleft _ ⇒ None
                 | dright _ ⇒ None
                 | dbrand _ _ ⇒ None
                 | dforeign _ ⇒ None
                 end) (Some d1)) l).

    Lemma pick_fresh_distinct_second v v1 v2 rest:
      ∃ v3,
        v3 = (fresh_var v (v1 :: v2 :: rest)) ∧
        v2 ≠ v3.

    Lemma build_group_ext (x:data) (o1 o2:option data) :
      o1 = o2 →
      match o1 with
      | Some dunit ⇒ None
      | Some (dnat _) ⇒ None
      | Some (dbool _) ⇒ None
      | Some (dstring _) ⇒ None
      | Some (dcoll _) ⇒ None
      | Some (drec r1) ⇒
        match x with
        | dunit ⇒ None
        | dnat _ ⇒ None
        | dbool _ ⇒ None
        | dstring _ ⇒ None
        | dcoll _ ⇒ None
        | drec r2 ⇒ Some (drec (rec_sort (r1 ++ r2)))
        | dleft _ ⇒ None
        | dright _ ⇒ None
        | dbrand _ _ ⇒ None
        | dforeign _ ⇒ None
        end
      | Some (dleft _) ⇒ None
      | Some (dright _) ⇒ None
      | Some (dbrand _ _) ⇒ None
      | Some (dforeign _) ⇒ None
      | None ⇒ None
      end =
      match o2 with
      | Some dunit ⇒ None
      | Some (dnat _) ⇒ None
      | Some (dbool _) ⇒ None
      | Some (dstring _) ⇒ None
      | Some (dcoll _) ⇒ None
      | Some (drec r1) ⇒
        match x with
        | dunit ⇒ None
        | dnat _ ⇒ None
        | dbool _ ⇒ None
        | dstring _ ⇒ None
        | dcoll _ ⇒ None
        | drec r2 ⇒ Some (drec (rec_sort (r1 ++ r2)))
        | dleft _ ⇒ None
        | dright _ ⇒ None
        | dbrand _ _ ⇒ None
        | dforeign _ ⇒ None
        end
      | Some (dleft _) ⇒ None
      | Some (dright _) ⇒ None
      | Some (dbrand _ _) ⇒ None
      | Some (dforeign _) ⇒ None
      | None ⇒ None
      end.

    Lemma nnrc_core_eval_group_by_eq env (g:string) (sl:list string) (e1 e2:nnrc):
      nnrc_core_eval h env e1 = nnrc_core_eval h env e2 →
      ∀ vid venv,
        nnrc_core_eval h env (nnrc_group_by g sl e1)
        = nnrc_core_eval h env (nnrc_group_by_from_nraenv vid venv g sl e2).

  End macros.

  Section translation.
    Fixpoint nnrc_ext_to_nnrc (e:nnrc) : nnrc :=
      match e with
      | NNRCVar v ⇒ NNRCVar v
      | NNRCConst d ⇒ NNRCConst d
      | NNRCBinop b e1 e2 ⇒
        NNRCBinop b (nnrc_ext_to_nnrc e1) (nnrc_ext_to_nnrc e2)
      | NNRCUnop u e1 ⇒
        NNRCUnop u (nnrc_ext_to_nnrc e1)
      | NNRCLet v e1 e2 ⇒
        NNRCLet v (nnrc_ext_to_nnrc e1) (nnrc_ext_to_nnrc e2)
      | NNRCFor v e1 e2 ⇒
        NNRCFor v (nnrc_ext_to_nnrc e1) (nnrc_ext_to_nnrc e2)
      | NNRCIf e1 e2 e3 ⇒
        NNRCIf (nnrc_ext_to_nnrc e1) (nnrc_ext_to_nnrc e2) (nnrc_ext_to_nnrc e3)
      | NNRCEither e1 v2 e2 v3 e3 ⇒
        NNRCEither (nnrc_ext_to_nnrc e1) v2 (nnrc_ext_to_nnrc e2) v3 (nnrc_ext_to_nnrc e3)
      | NNRCGroupBy g sl e1 ⇒
        nnrc_group_by g sl (nnrc_ext_to_nnrc e1)
      end.

    Lemma nnrc_ext_to_nnrc_is_core (e:nnrc) :
      nnrcIsCore (nnrc_ext_to_nnrc e).

    Lemma core_nnrc_to_nnrc_ext_id (e:nnrc) :
      nnrcIsCore e →
      (nnrc_ext_to_nnrc e) = e.

    Lemma core_nnrc_to_nnrc_ext_idempotent (e1 e2:nnrc) :
      e1 = nnrc_ext_to_nnrc e2 →
      nnrc_ext_to_nnrc e1 = e1.

    Corollary core_nnrc_to_nnrc_ext_idempotent_corr (e:nnrc) :
      nnrc_ext_to_nnrc (nnrc_ext_to_nnrc e) = (nnrc_ext_to_nnrc e).

  End translation.

  Section semantics.
Semantics of NNRCExt

    Definition nnrc_ext_eval (env:bindings) (e:nnrc) : option data :=
      nnrc_core_eval h env (nnrc_ext_to_nnrc e).

    Remark nnrc_ext_to_nnrc_eq (e:nnrc):
      ∀ env,
        nnrc_ext_eval env e = nnrc_core_eval h env (nnrc_ext_to_nnrc e).

    Remark nnrc_to_nnrc_ext_eq (e:nnrc):
      nnrcIsCore e →
      ∀ env,
        nnrc_core_eval h env e = nnrc_ext_eval env e.

    Global Instance nnrc_ext_eval_lookup_equiv_prop :
      Proper (lookup_equiv ==> eq ==> eq) nnrc_ext_eval.

  End semantics.

  Section prop.

    Lemma nnrc_ext_to_nnrc_free_vars_same e:
      nnrc_free_vars e = nnrc_free_vars (nnrc_ext_to_nnrc e).

    Lemma nnrc_ext_to_nnrc_bound_vars_impl x e:
      In x (nnrc_bound_vars e) → In x (nnrc_bound_vars (nnrc_ext_to_nnrc e)).

    Lemma nnrc_ext_to_nnrc_bound_vars_impl_not x e:
      ¬ In x (nnrc_bound_vars (nnrc_ext_to_nnrc e)) → ¬ In x (nnrc_bound_vars e).

    Definition really_fresh_in_ext sep oldvar avoid e :=
      really_fresh_in sep oldvar avoid (nnrc_ext_to_nnrc e).

    Lemma really_fresh_from_free_ext sep old avoid (e:nnrc) :
      ¬ In (really_fresh_in_ext sep old avoid e) (nnrc_free_vars (nnrc_ext_to_nnrc e)).

    Lemma nnrc_ext_to_nnrc_subst_comm e1 v1 e2:
      nnrc_subst (nnrc_ext_to_nnrc e1) v1 (nnrc_ext_to_nnrc e2) =
      nnrc_ext_to_nnrc (nnrc_subst e1 v1 e2).

    Lemma nnrc_ext_to_nnrc_rename_lazy_comm e v1 v2:
      nnrc_rename_lazy (nnrc_ext_to_nnrc e) v1 v2 =
      nnrc_ext_to_nnrc (nnrc_rename_lazy e v1 v2).

    Lemma unshadow_over_nnrc_ext_idem sep renamer avoid e:
      (nnrc_ext_to_nnrc (unshadow sep renamer avoid (nnrc_ext_to_nnrc e))) =
      (unshadow sep renamer avoid (nnrc_ext_to_nnrc e)).

    Lemma nnrc_ext_eval_cons_subst e env v x v' :
      ¬ (In v' (nnrc_free_vars e)) →
      ¬ (In v' (nnrc_bound_vars e)) →
      nnrc_ext_eval ((v',x)::env) (nnrc_subst e v (NNRCVar v')) =
      nnrc_ext_eval ((v,x)::env) e.

    Definition unnest_from_nraenv vid venv a b n1 :=
      (NNRCFor (fresh_var "tmap$" (vid :: venv :: nil))
               (NNRCUnop AFlatten
                         (NNRCFor (fresh_var "tmc$" (vid :: venv :: nil))
                                  n1
                                  (NNRCFor
                                     (fresh_var "tmc$" (fresh_var "tmc$" (vid :: venv :: nil) :: vid :: venv :: nil))
                                     (NNRCFor (fresh_var "tmap$" (vid :: venv :: nil))
                                              (NNRCUnop (ADot a) (NNRCVar (fresh_var "tmc$" (vid :: venv :: nil))))
                                              (NNRCUnop (ARec b) (NNRCVar (fresh_var "tmap$" (vid :: venv :: nil)))))
                                     (NNRCBinop AConcat (NNRCVar (fresh_var "tmc$" (vid :: venv :: nil)))
                                                (NNRCVar
                                                   (fresh_var "tmc$"
                                                              (fresh_var "tmc$" (vid :: venv :: nil) :: vid :: venv :: nil)))))))
               (NNRCUnop (ARecRemove a) (NNRCVar (fresh_var "tmap$" (vid :: venv :: nil))))).

    Definition unnest_from_nraenv_core vid venv a b n1 :=
      (NNRCFor (fresh_var "tmap$" (vid :: venv :: nil))
               (NNRCUnop AFlatten
                         (NNRCFor (fresh_var "tmc$" (vid :: venv :: nil))
                                  n1
                                  (NNRCFor
                                     (fresh_var "tmc$" (fresh_var "tmc$" (vid :: venv :: nil) :: vid :: venv :: nil))
                                     (NNRCFor
                                        (fresh_var "tmap$" (fresh_var "tmc$" (vid :: venv :: nil) :: venv :: nil))
                                        (NNRCUnop (ADot a) (NNRCVar (fresh_var "tmc$" (vid :: venv :: nil))))
                                        (NNRCUnop (ARec b)
                                                  (NNRCVar
                                                     (fresh_var "tmap$"
                                                                (fresh_var "tmc$" (vid :: venv :: nil) :: venv :: nil)))))
                                     (NNRCBinop AConcat (NNRCVar (fresh_var "tmc$" (vid :: venv :: nil)))
                                                (NNRCVar
                                                   (fresh_var "tmc$"
                                                              (fresh_var "tmc$" (vid :: venv :: nil) :: vid :: venv :: nil)))))))
               (NNRCUnop (ARecRemove a) (NNRCVar (fresh_var "tmap$" (vid :: venv :: nil))))).

    Lemma unnest_from_nraenv_and_nraenv_core_eq vid venv env a b op1 op1' :
      nnrc_core_eval h env op1 = nnrc_core_eval h env op1' →
      nnrc_core_eval h env (unnest_from_nraenv vid venv a b op1) =
      nnrc_core_eval h env (unnest_from_nraenv_core vid venv a b op1').

  End prop.

  Section core.
    Program Definition nnrc_to_nnrc_core (e:nnrc) : nnrc_core :=
      nnrc_ext_to_nnrc e.

  End core.

End NNRC.