Qcert.Tests.LambdaNRATests





Section LambdaNRATests.

  Definition h : brand_relation_t := nil.

  Definition db1 :=
    (dcoll ((drec (("addr",(drec (("city", dstring "NYC")::nil)))::nil))::nil))%string.

  Definition child1 :=
    (dcoll ((drec (("name",dstring "Jane")::("age",dnat 2)::nil))
              :: (drec (("name",dstring "Joan")::("age",dnat 99)::nil))
              :: nil))%string.

  Definition child2 :=
    (dcoll ((drec (("name",dstring "Jules")::("age",dnat 24)::nil))
              :: (drec (("name",dstring "Jim")::("age",dnat 26)::nil))
              :: nil))%string.

  Definition db2 :=
    (dcoll ((drec (("name",dstring "John")::("age",dnat 24)::("child",child1)::nil))
              :: (drec (("name",dstring "Jack")::("age",dnat 40)::("child",child2)::nil))
              :: nil))%string.

The original version of T1
  Definition T1l P :=
    LNRAMap (LNRALambda "a" (LNRAUnop (ADot "city") (LNRAVar "a")))
            (LNRAMap (LNRALambda "p" (LNRAUnop (ADot "addr") (LNRAVar "p"))) P).

The simplified version of T1
  Definition T1r P :=
    LNRAMap (LNRALambda "p" (LNRAUnop (ADot "city") (LNRAUnop (ADot "addr") (LNRAVar "p")))) P.

  Lemma T1lr_equiv P : lnra_eq (T1l P) (T1r P).



  Definition T2l P :=
    LNRAMap (LNRALambda "x" (LNRAUnop (ADot "age") (LNRAVar "x")))
            (LNRAFilter (LNRALambda "p" (LNRABinop ALt
                                                   (LNRAConst (dnat 25))
                                                   (LNRAUnop (ADot "age") (LNRAVar "p")))) P).

  Definition T2r P :=
    LNRAFilter (LNRALambda "a" (LNRABinop ALt
                                          (LNRAConst (dnat 25))
                                          (LNRAVar "a")))
               (LNRAMap (LNRALambda "p" (LNRAUnop (ADot "age") (LNRAVar "p"))) P).




  Definition A3 P :=
    LNRAMap
      (LNRALambda "p"
                  (LNRABinop AConcat (LNRAUnop (ARec "person") (LNRAVar "p"))
                             (LNRAUnop (ARec "kids")
                                       (LNRAFilter
                                          (LNRALambda "c"
                                                      (LNRABinop ALt
                                                                 (LNRAConst (dnat 25))
                                                                 (LNRAUnop (ADot "age") (LNRAVar "c"))))
                                          (LNRAUnop (ADot "child") (LNRAVar "p")))))) P.



  Definition A4 P :=
    LNRAMap
      (LNRALambda "p"
                  (LNRABinop AConcat (LNRAUnop (ARec "person") (LNRAVar "p"))
                             (LNRAUnop (ARec "kids")
                                       (LNRAFilter
                                          (LNRALambda "c"
                                                      (LNRABinop ALt
                                                                 (LNRAConst (dnat 25))
                                                                 (LNRAUnop (ADot "age") (LNRAVar "p"))))
                                          (LNRAUnop (ADot "child") (LNRAVar "p")))))) P.


End LambdaNRATests.

Section LambdaNRALinq.

  Definition linq_example Persons
    := LNRAMap
         (LNRALambda "p"
                     (LNRAUnop (ADot "name") (LNRAVar "p")))
         (LNRAFilter
            (LNRALambda "p"
                        (LNRABinop ALt
                                   (LNRAUnop (ADot "name") (LNRAVar "p"))
                                   (LNRAConst (dnat 30))))
            Persons).

End LambdaNRALinq.



Context {l:optimizer_logger string nraenv}.

Definition T1env : nraenv := (nraenv_of_lnra_lambda (q_to_lambda T1l)).
Definition T1env_opt := nraenv_optim_default T1env.
Definition T1nnrc_opt :=
  TrivialCompiler.QDriver.nraenv_optim_to_nnrc_optim T1env_opt.

Definition T2env := (nraenv_of_lnra_lambda (q_to_lambda T2l)).
Definition T2env_opt := nraenv_optim_default T2env.
Definition T2nnrc_opt := TrivialCompiler.QDriver.nraenv_optim_to_nnrc_optim T2env_opt.