Module Qcert.NNRC.Lang.NNRCSugar


This module contains some additional properties for extended operators in NNRC. Some of those are notably useful later on for proving translations from NRAEnv.

Require Import String.
Require Import List.
Require Import Arith.
Require Import EquivDec.
Require Import Morphisms.
Require Import Arith.
Require Import Max.
Require Import Bool.
Require Import Peano_dec.
Require Import EquivDec.
Require Import Decidable.
Require Import Utils.
Require Import DataRuntime.
Require Import cNNRCRuntime.
Require Import NNRC.

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

Group By


This is an alternative macro for group by. This is used as a scafolding to prove translation from the GroupBy in NRAEnv to the one in NNRC correct.
  
  Definition nnrc_group_by_from_nraenv (vid venv:var) (g:string) (sl:list string) (e:nnrc) :=
    (NNRCLet (fresh_var "tappe$" (vid :: venv :: nil))
             (NNRCUnop (OpRec "$pregroup") e)
             (NNRCFor
                (fresh_var "tmap$"
                           (vid :: fresh_var "tappe$" (vid :: venv :: nil) :: nil))
                (NNRCUnop OpDistinct
                          (NNRCFor
                             (fresh_var "tmap$"
                                        (vid :: fresh_var "tappe$" (vid :: venv :: nil) :: nil))
                             (NNRCUnop (OpDot "$pregroup")
                                       (NNRCVar (fresh_var "tappe$" (vid :: venv :: nil))))
                             (NNRCUnop (OpRecProject sl)
                                       (NNRCVar
                                          (fresh_var "tmap$"
                                                     (vid
                                                        :: fresh_var "tappe$" (vid :: venv :: nil)
                                                        :: nil))))))
                (NNRCBinop OpRecConcat
                           (NNRCVar
                              (fresh_var "tmap$"
                                         (vid :: fresh_var "tappe$" (vid :: venv :: nil) :: nil)))
                           (NNRCUnop (OpRec g)
                                     (NNRCLet
                                        (fresh_var "tappe$"
                                                   (fresh_var "tmap$"
                                                              (vid
                                                                 :: fresh_var "tappe$" (vid :: venv :: nil)
                                                                 :: nil)
                                                              :: fresh_var "tappe$" (vid :: venv :: nil) :: nil))
                                        (NNRCBinop OpRecConcat
                                                   (NNRCUnop (OpRec "$key")
                                                             (NNRCVar
                                                                (fresh_var "tmap$"
                                                                           (vid
                                                                              :: fresh_var "tappe$" (vid :: venv :: nil)
                                                                              :: nil))))
                                                   (NNRCVar (fresh_var "tappe$" (vid :: venv :: nil))))
                                        (NNRCUnop OpFlatten
                                                  (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 (OpDot "$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 OpEqual
                                                                   (NNRCUnop (OpRecProject 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 (OpDot "$key")
                                                                             (NNRCVar
                                                                                (fresh_var "tappe$"
                                                                                           (fresh_var "tmap$"
                                                                                                      (vid
                                                                                                         :: fresh_var "tappe$"
                                                                                                         (vid :: venv :: nil)
                                                                                                         :: nil)
                                                                                                      :: fresh_var "tappe$"
                                                                                                      (vid :: venv :: nil) :: nil)))))
                                                        (NNRCUnop OpBag
                                                                  (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)))))))))).
  
  Lemma pick_fresh_distinct_second v v1 v2 rest:
    exists v3,
      v3 = (fresh_var v (v1 :: v2 :: rest)) /\
      v2 <> v3.
Proof.

  Lemma build_group_ext (x:data) (o1 o2:option data) :
    o1 = o2 ->
    match o1 with
    | Some d2 =>
      match x with
      | drec r1 =>
        match d2 with
        | drec r2 => Some (drec (rec_sort (r1 ++ r2)))
        | _ => None
        end
      | _ => None
      end
    | None => None
    end =
    match o2 with
    | Some d2 =>
      match x with
      | drec r1 =>
        match d2 with
        | drec r2 => Some (drec (rec_sort (r1 ++ r2)))
        | _ => None
        end
      | _ => None
      end
    | None => None
    end.
Proof.

The following states that the principal definition for group by and this alternative are equivalent.
  
  Lemma nnrc_core_eval_group_by_eq {cenv} env (g:string) (sl:list string) (e1 e2:nnrc):
    nnrc_core_eval h cenv env e1 = nnrc_core_eval h cenv env e2 ->
    forall vid venv,
      nnrc_core_eval h cenv env (nnrc_group_by g sl e1)
      = nnrc_core_eval h cenv env (nnrc_group_by_from_nraenv vid venv g sl e2).
Proof.

Unnest

  
  Definition unnest_from_nraenv vid venv a b n1 :=
    (NNRCFor (fresh_var "tmap$" (vid :: venv :: nil))
             (NNRCUnop OpFlatten
                       (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 (OpDot a) (NNRCVar (fresh_var "tmc$" (vid :: venv :: nil))))
                                            (NNRCUnop (OpRec b) (NNRCVar (fresh_var "tmap$" (vid :: venv :: nil)))))
                                   (NNRCBinop OpRecConcat (NNRCVar (fresh_var "tmc$" (vid :: venv :: nil)))
                                              (NNRCVar
                                                 (fresh_var "tmc$"
                                                            (fresh_var "tmc$" (vid :: venv :: nil) :: vid :: venv :: nil)))))))
             (NNRCUnop (OpRecRemove 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 OpFlatten
                       (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 (OpDot a) (NNRCVar (fresh_var "tmc$" (vid :: venv :: nil))))
                                      (NNRCUnop (OpRec b)
                                                (NNRCVar
                                                   (fresh_var "tmap$"
                                                              (fresh_var "tmc$" (vid :: venv :: nil) :: venv :: nil)))))
                                   (NNRCBinop OpRecConcat (NNRCVar (fresh_var "tmc$" (vid :: venv :: nil)))
                                              (NNRCVar
                                                 (fresh_var "tmc$"
                                                            (fresh_var "tmc$" (vid :: venv :: nil) :: vid :: venv :: nil)))))))
             (NNRCUnop (OpRecRemove a) (NNRCVar (fresh_var "tmap$" (vid :: venv :: nil))))).

  Lemma unnest_from_nraenv_and_nraenv_core_eq {cenv} vid venv env a b op1 op1' :
    nnrc_core_eval h cenv env op1 = nnrc_core_eval h cenv env op1' ->
    nnrc_core_eval h cenv env (unnest_from_nraenv vid venv a b op1) =
    nnrc_core_eval h cenv env (unnest_from_nraenv_core vid venv a b op1').
Proof.

  Section natural_join.
    Definition nnrc_natural_join (vid venv:var) (e1 e2:nnrc) : nnrc :=
      (NNRCUnop OpFlatten
                (NNRCUnop OpFlatten
                          (NNRCFor (fresh_var "tprod$" (vid :: venv :: nil)) e1
                                   (NNRCFor (fresh_var "tprod$" (fresh_var "tprod$" (vid :: venv :: nil) :: vid :: venv :: nil))
                                            e2
                                            (NNRCBinop OpRecMerge (NNRCVar (fresh_var "tprod$" (vid :: venv :: nil)))
                                                       (NNRCVar (fresh_var "tprod$" (fresh_var "tprod$" (vid :: venv :: nil) :: vid :: venv :: nil)))))))).

    Definition nnrc_natural_join_from_nraenv (vid venv:var) (e1 e2:nnrc) : nnrc :=
      (NNRCUnop OpFlatten
                (NNRCFor (fresh_var "tmap$" (vid :: venv :: nil))
                         (NNRCUnop OpFlatten
                                   (NNRCFor (fresh_var "tprod$" (vid :: venv :: nil))
                                            (NNRCFor (fresh_var "tmap$" (vid :: venv :: nil))
                                                     e1
                                                     (NNRCUnop (OpRec "t1") (NNRCVar (fresh_var "tmap$" (vid :: venv :: nil)))))
                                            (NNRCFor (fresh_var "tprod$" (fresh_var "tprod$" (vid :: venv :: nil) :: vid :: venv :: nil))
                                                     (NNRCFor (fresh_var "tmap$" (vid :: venv :: nil))
                                                              e2
                                                              (NNRCUnop (OpRec "t2") (NNRCVar (fresh_var "tmap$" (vid :: venv :: nil)))))
                                                     (NNRCBinop OpRecConcat (NNRCVar (fresh_var "tprod$" (vid :: venv :: nil)))
                                                                (NNRCVar
                                                                   (fresh_var "tprod$" (fresh_var "tprod$" (vid :: venv :: nil) :: vid :: venv :: nil)))))))
                         (NNRCBinop OpRecMerge (NNRCUnop (OpDot "t1") (NNRCVar (fresh_var "tmap$" (vid :: venv :: nil))))
                                    (NNRCUnop (OpDot "t2") (NNRCVar (fresh_var "tmap$" (vid :: venv :: nil))))))).

  End natural_join.
End NNRCSugar.

Generated by coq2html