Qcert.Tests.SQLTest
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 SQLTest.
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 mkperson (name:string) (age:Z) (zip:Z) (company:string) (position:string) :=
[| ("name", dstring name);
("age", dnat age);
("zip", dnat zip);
("company", dstring company);
("position", dstring position) |].
Definition mkpersons_aux l :=
map (fun x ⇒
match x with (name, age, zip, company, position) ⇒ mkperson name age zip company position
end) l.
Definition p1 := mkperson "John" 23 1008 "IBM" "CEO".
Definition p2 := mkperson "Jane" 24 1009 "AIG" "CFO".
Definition mkpersons l :=
dcoll (mkpersons_aux l).
Definition persons :=
mkpersons
(("John",30,1008,"IBM", "CEO")
:: ("Jane",12,1009,"AIG", "CFO")
:: ("Joan",30,1008,"AIG", "CEO")
:: ("Jade",30,1008,"AIG", "VP Sales")
:: ("Jacques",30,1008,"AIG", "VP Compliance")
:: ("Jill",25,1010,"IBM", "CFO")
:: ("Joo",24,1010,"IBM", "VP Engineering")
:: ("Just",12,1010,"IBM", "VP M&A")
:: ("Jack",56,1010,"Apricot", "CEO")
:: ("Jerome",56,1010,"Apricot", "Dean")
:: nil).
Definition companies : data :=
{| [|("cname", dstring "IBM"); ("stock", dnat 200); ("ticker", dstring "IBM") |];
[|("cname", dstring "AIG"); ("stock", dnat 20); ("ticker", dstring "AIG") |];
[|("cname", dstring "AMD"); ("stock", dnat 25); ("ticker", dstring "AMD") |];
[|("cname", dstring "Apricot"); ("stock", dnat 135); ("ticker", dstring "APR") |] |}.
Definition tables : list (string×data) :=
(("persons",persons) :: ("companies",companies) :: nil).
Definition sql_just_query_to_nraenv (q:sql_query)
:= sql_to_nraenv (SRunQuery q::nil).
Definition sql_just_query_eval (q:sql_query)
:= @eval_sql _ nil (SRunQuery q::nil).
Definition sql1 :=
SQuery (SSelectColumn "name"::nil) (SFromTable "persons"::nil) None None None.
Definition nraenv1 :=
sql_just_query_to_nraenv sql1.
Definition sql2 :=
SQuery (SSelectColumn "name"::SSelectColumn "age"::nil)
(SFromTable "persons"::nil) None None (Some (("age",Ascending)::nil)).
Definition sql3 :=
SQuery (SSelectColumn "name"::nil)
(SFromTable "persons"::nil) None None (Some (("age",Ascending)::nil)).
Definition sql4 :=
SQuery (SSelectColumn "name"::nil)
(SFromTable "persons"::nil)
(Some (SCondBinary SEq (SExprColumn "company")
(SExprConst (dstring "IBM"))))
None (Some (("age",Ascending)::nil)).
Definition sql5 :=
[SRunQuery (SQuery (SSelectExpr ""
(SExprAggExpr SSum (SExprColumn "age"))::nil)
(SFromTable "persons"::nil) None None None)].
Definition sql6 :=
SQuery (SSelectExpr ""
(SExprAggExpr SCount SExprStar)::nil)
(SFromTable "persons"::nil) None None None.
Definition sql7 :=
SQuery (SSelectExpr ""
(SExprAggExpr SCount SExprStar)::nil)
(SFromQuery ("IBMers",None) sql4 :: nil) None None None.
Definition sql8 :=
SQuery (SSelectExpr "res" SExprStar::nil)
(SFromTable "persons"::nil) None (Some (("age"::nil),None)) None.
Definition sql9 :=
SQuery (SSelectColumn "age" :: SSelectExpr "nb"
(SExprAggExpr SCount SExprStar)::nil)
(SFromTable "persons"::nil) None (Some (("age"::nil),None)) None.
Definition sql10 :=
SQuery (SSelectColumn "age" :: SSelectExpr "nb"
(SExprAggExpr SCount SExprStar)::nil)
(SFromTable "persons"::nil) None
(Some (("age"::nil),None)) (Some (("age",Ascending)::nil)).
Definition sql11 :=
SQuery (SSelectColumn "age" :: SSelectExpr "nb"
(SExprAggExpr SCount SExprStar)::nil)
(SFromTable "persons"::nil)
None (Some (("age"::nil),
Some (SCondBinary SGt (SExprAggExpr SCount SExprStar)
(SExprConst (dnat 1)))))
(Some (("age",Ascending)::nil)).
Definition sql12 :=
SQuery (SSelectColumn "age" :: SSelectColumn "company" :: SSelectExpr "nb"
(SExprAggExpr SCount SExprStar)::nil)
(SFromTable "persons"::nil)
None
(Some (("age"::"company"::nil),None)) None.
Definition sql13 :=
SQuery (SSelectColumn "name"::SSelectColumn "age"::nil)
(SFromTable "persons"::nil)
(Some (SCondBinary SEq (SExprColumn "company")
(SExprConst (dstring "IBM"))))
None (Some (("age",Ascending)::nil)).
Definition sql14 :=
SQuery (SSelectColumn "nom"::nil)
(SFromQuery ("IBMers",Some ("nom"::"age"::nil)) sql13 :: nil)
None None None.
Definition sql15 :=
SQuery ((SSelectColumn "cname")
:: (SSelectColumn "stock")
:: SSelectExpr "nb_employees" (SExprAggExpr SCount SExprStar)::nil)
(SFromTable "persons"::SFromTable "companies"::nil)
(Some (SCondBinary SEq (SExprColumn "cname") (SExprColumn "company")))
(Some (("cname"::"stock"::nil),
Some (SCondBinary SGt
(SExprColumn "stock")
(SExprConst (dnat 50)))))
(Some (("stock"%string,Ascending)::nil)).
Definition sql16 :=
SQuery ((SSelectColumn "name")
:: (SSelectColumn "company")
::nil)
(SFromTable "persons"::nil)
(Some (SCondIn (SExprColumn "company")
(SExprQuery
(SQuery ((SSelectColumn "cname")::nil)
(SFromTable "companies"::nil)
(Some (SCondBinary SGt
(SExprColumn "stock")
(SExprConst (dnat 50))))
None None))))
None
None.
Definition sql17 :=
SQuery ((SSelectColumnDeref "p1" "age")
:: (SSelectColumnDeref "p1" "company")
:: (SSelectExpr "emp1" (SExprColumnDeref "p1" "name"))
:: (SSelectExpr "emp2" (SExprColumnDeref "p2" "name"))
:: nil)
(SFromTableAlias "p1" "persons"::SFromTableAlias "p2" "persons"::nil)
(Some (SCondAnd
(SCondAnd
(SCondBinary SEq (SExprColumnDeref "p1" "age")
(SExprColumnDeref "p2" "age"))
(SCondBinary SEq (SExprColumnDeref "p1" "company")
(SExprColumnDeref "p2" "company")))
(SCondBinary SDiff (SExprColumnDeref "p1" "name")
(SExprColumnDeref "p2" "name"))))
None
None.
End SQLTest.