Qcert.Tests.NRATest

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 NRATest.






  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) :=
    [| ("name", dstring name);
       ("age", dnat age);
       ("zip", dnat zip);
       ("company", dstring company) |].

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

  Definition p1 := mkperson "John" 23 1008 "IBM".
  Definition p2 := mkperson "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 mkpersons l :=
    dcoll (mkpersons_aux l).

  Definition persons :=
    mkpersons
      (("John",23,1008,"IBM")
         :: ("Jane",24,1009,"AIG")
         :: ("Jill",25,1010,"IBM")
         :: ("Jack",27,1010,"CMU")
         :: 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") |] |}.



  Definition tables : data :=
    [| ("persons",persons); ("companies",companies) |].


  Definition qtpersons := ID·"persons".

  Definition qtcompanies := ID·"companies".

  Definition nothing : data := dunit.

  Definition qpersons := (AXConst (persons)).

  Definition qcompanies := (AXConst (companies)).




  Definition q0 := ♯count(ID).



  Definition q0' := ‵one_to_ten⌈"n"⌋.


  Definition q1 := χ⟨ ID ⟩(qpersons).


  Definition q2 := χ⟨ ID·"age" ⟩(qpersons).


  Definition q2' := χ⌈"n"⌋⟨ ID·"age" ⟩(qpersons).



  Definition q3 := (σ⟨ ‵‵true ⟩(qpersons)).


  Definition q4 := (σ⟨ ID·"age" ≐ ‵‵23 ⟩(qpersons)).



  Definition q5 := (qpersons × qcompanies).




  Definition q6 := σ⟨ ID·"company" ≐ ID·"cname" ⟩(qpersons × qcompanies).


  Definition q6' := ⋈⟨ ID·"company" ≐ ID·"cname" ⟩(qpersons, qcompanies).



  Definition q61 := ⋉⟨ ID·"company" ≐ ID·"cname" ⟩(qpersons, qcompanies).



  Definition q62 := ▷⟨ ID·"company" ≐ ID·"cname" ⟩(qpersons, qcompanies).



  Definition q7 := ⋈ᵈ⟨ ‵{|‵[| ("emps", σ⟨ ID·"company" ≐ ID·"cname" ⟩(qpersons × ‵{|ID|})) |]|} ⟩( qcompanies ).


  Definition q8 := ⋈ᵈ⟨ ‵{|‵[| ("emp_count",♯count(σ⟨ ID·"company" ≐ ID·"cname" ⟩(qpersons × ‵{|ID|}))) |]|} ⟩( qcompanies ).



  Definition q9 := Π[](qpersons).


  Definition q10 := Π["name"](qpersons).


  Definition q11 := Π["name","company"](qpersons).


  Definition q12 := Π["name","company","cname"](q6').


  Definition q13 := Π["name","company","cname","stock"](q6').



  Definition q14 := ¬Π["name"](q6').



  Definition q15 := ρ[ "name" ↦ "nom" ](q6').



  Definition q16 := μ["emps"](q7).


  Definition q7' := Π["cname","zips"](χ⌈"zips"⌋⟨χ⟨ ID·"zip" ⟩(ID·"emps")⟩(q7)).


  Definition q17 := μ["zips"]["zip"](q7').




  Definition q18 := Γ["g"]["cname"](q6').



End NRATest.