Qcert.Tests.OQLTest

Notation "⊥" := (dunit) : data_scope.
Notation "[||]" := (drec nil) : data_scope. Notation "[| x1 ; .. ; xn |]" := (RData.drec (cons x1 .. (cons xn nil) ..)) : data_scope.

Notation "{||}" := (dcoll nil) : data_scope. Notation "{| x1 ; .. ; xn |}" := (dcoll (cons x1 .. (cons xn nil) ..)) : data_scope.

Section OQLTest.






  Fixpoint natcoll_aux (n n0:nat) : list data :=
    match n with
      | O ⇒ nil
      | S n' ⇒ (dnat (Z_of_nat (n0 - n))) :: (natcoll_aux n' n0)
    end.

  Definition natcoll (n:nat) : data :=
    (dcoll (natcoll_aux n (n+1))).



  Example ex1 := [||].



  Definition one_to_ten := (natcoll 10).


  Definition h := (@nil (string×string)).


  Definition mkemployee (name:string) (age:Z) (zip:Z) (company:string) :=
    dbrand ("Employee"::nil)
           [| ("name", dstring name);
              ("age", dnat age);
              ("zip", dnat zip);
              ("company", dstring company) |].

  Definition mkemployees_aux l :=
    map (fun x ⇒
           match x with (name, age, zip, company) ⇒ mkemployee name age zip company
           end) l.

  Definition p1 := mkemployee "John" 23 1008 "IBM".
  Definition p2 := mkemployee "Jane" 24 1009 "AIG".

  Definition myc x1 x2 :=
  match x1,x2 with
    | drec d1, drec d2 ⇒ Some (rec_concat_sort d1 d2)
    | _,_ ⇒ None
  end.


  Definition mkemployees l :=
    dcoll (mkemployees_aux l).

  Definition employees :=
    mkemployees
      (("John",23,1008,"IBM")
         :: ("Jane",24,1009,"AIG")
         :: ("Jill",25,1010,"IBM")
         :: ("Jack",27,1010,"CMU")
         :: nil).



  Definition companies : data :=
    {| dbrand ("Company"::nil) [|("cname", dstring "IBM"); ("stock", dnat 200); ("ticker", dstring "IBM");
                                 ("departments", dcoll ((dstring "Cloud") :: (dstring "Cognitive") :: nil)) |];
       dbrand ("Company"::nil) [|("cname", dstring "AIG"); ("stock", dnat 20); ("ticker", dstring "AIG");
                                 ("departments", dcoll ((dstring "Insurance") :: (dstring "Derivatives") :: nil)) |];
       dbrand ("Company"::nil) [|("cname", dstring "AMD"); ("stock", dnat 25); ("ticker", dstring "AMD");
                                 ("departments", dcoll nil) |] |}.

  Definition CPRModel :=
    ("Company","Entity")::("Employee","Entity")::nil.



  Definition tables : oql_env :=
    (("Employees",employees) :: ("Companies",companies) :: nil).

  Definition init_env : oql_env := nil.




  Definition q0 : oql_expr := OUnop ACount (OTable "Companies").
  Definition q0_eval : option data := oql_expr_interp CPRModel tables q0 init_env.




  Definition q1 : oql_expr :=
    OSFW
      (OSelect (OUnop (ADot "age") (OUnop AUnbrand (OVar "e"))))
      ((OIn "e" (OTable "Employees"))::nil)
      (OWhere (OBinop AEq (OUnop (ADot "name") (OUnop AUnbrand (OVar "e"))) (OConst (dstring "John"))))
      ONoOrder.

  Definition q1_eval : option data := oql_expr_interp CPRModel tables q1 init_env.




  Definition q2 : oql_expr :=
    OSFW
      (OSelect (OBinop AConcat
                       (OUnop (ARec "employee") (OUnop (ADot "name") (OUnop AUnbrand (OVar "e"))))
                       (OUnop (ARec "worksfor") (OUnop (ADot "cname") (OUnop AUnbrand (OVar "c"))))))
      ((OIn "e" (OTable "Employees"))::(OIn "c" (OTable "Companies"))::nil)
      (OWhere (OBinop AEq
                      (OUnop (ADot "company") (OUnop AUnbrand (OVar "e")))
                      (OUnop (ADot "cname") (OUnop AUnbrand (OVar "c")))))
      ONoOrder.

  Definition q2_eval : option data := oql_expr_interp CPRModel tables q2 init_env.



  Definition q2' : oql_expr :=
    OSFW
      (OSelect (OStruct (("employee", (OUnop (ADot "name") (OUnop AUnbrand (OVar "e"))))
                           :: ("worksfor", (OUnop (ADot "cname") (OUnop AUnbrand (OVar "c"))))
                           :: nil)))
      ((OIn "e" (OTable "Employees"))::(OIn "c" (OTable "Companies"))::nil)
      (OWhere (OBinop AEq
                      (OUnop (ADot "company") (OUnop AUnbrand (OVar "e")))
                      (OUnop (ADot "cname") (OUnop AUnbrand (OVar "c")))))
      ONoOrder.

  Definition q2'_eval : option data := oql_expr_interp CPRModel tables q2' init_env.



  Definition q3 : oql_expr :=
    OSFW
      (OSelect (OBinop AConcat
                       (OUnop (ARec "company") (OUnop (ADot "cname") (OUnop AUnbrand (OVar "c"))))
                       (OUnop (ARec "dept") (OVar "d"))))
      ((OIn "c" (OTable "Companies"))::(OIn "d" (OUnop (ADot "departments") (OUnop AUnbrand (OVar "c"))))::nil)
      OTrue
      ONoOrder.

  Definition q3_eval : option data := oql_expr_interp CPRModel tables q3 init_env.



  Definition q3wrong : oql_expr :=
    OSFW
      (OSelect (OBinop AConcat
                       (OUnop (ARec "company") (OUnop (ADot "cname") (OUnop AUnbrand (OVar "c"))))
                       (OUnop (ARec "dept") (OVar "d"))))
      ((OIn "d" (OUnop (ADot "departments") (OUnop AUnbrand (OVar "c"))))::(OIn "c" (OTable "Companies"))::nil)
      OTrue
      ONoOrder.

  Definition q3wrong_eval : option data := oql_expr_interp CPRModel tables q3wrong init_env.


End OQLTest.