Qcert.Tests.TNRATest

Section TNRATest.





  Definition myBR : brand_relation
    := mkBrand_relation nil (eq_refl _) (eq_refl _) .

  Definition myBC : brand_context
    := @mkBrand_context trivial_foreign_type myBR nil (eq_refl _).

  Instance myM : brand_model
    := mkBrand_model myBR myBC (eq_refl _) (eq_refl _).


  Definition person_rec_schema :=
    rec_sort (("name",String) :: ("age",Nat) :: ("zip",Nat) :: ("company",String) :: nil).
  Lemma person_rec_schema_pf :
    is_list_sorted ODT_lt_dec (domain person_rec_schema) = true.
  Definition person_schema :=
    Rec Closed person_rec_schema person_rec_schema_pf.

  Definition persons_schema :=
    Coll person_schema.

  Lemma mkperson_typed name age zip company:
    (normalize_data brand_relation_brands (mkperson name age zip company)) ▹ person_schema.

  Lemma mkpersons_typed l:
    normalize_data brand_relation_brands (mkpersons l) ▹ persons_schema.

  Lemma persons_typed:
    normalize_data brand_relation_brands persons ▹ persons_schema.

  Lemma qpersons_typed {τin} :
    qpersons ▷ τin >=> persons_schema.




  Definition nothing_schema := Unit.

  Lemma nothing_typed :
    nothing ▹ nothing_schema.


  Lemma q0_wt {τin} :
    q0 ▷ (Coll τin) >=> Nat.

  Definition q0t {τin} (d:data) (pf: d ▹ (Coll τin)) : data :=
    (q0 @▷ d) pf q0_wt.




  Lemma q1_wt {τin} :
    q1 ▷ τin >=> persons_schema.

  Definition q1t {τin} (d:data) (pf: d ▹ τin) : data :=
    (q1 @▷ nothing) nothing_typed q1_wt.



  Lemma q2_wt {τin} :
    q2 ▷ τin >=> (Coll Nat).


  Definition q2t {τin} (d:data) (pf: d ▹ τin) : data :=
    (q2 @▷ d) pf q2_wt.




  Lemma q3_wt {τin} :
    q3 ▷ τin >=> persons_schema.

  Definition q3t {τin} (d:data) (pf: d ▹ τin) : data :=
    (q3 @▷ d) pf q3_wt.




  Lemma q4_wt {τin} :
    q4 ▷ τin >=> persons_schema.

  Definition q4t {τin} (d:data) (pf: d ▹ τin) : data :=
    (q4 @▷ d) pf q4_wt.



End TNRATest.