Qcert.Tests.CompilerTest

Definition CPRModel := ("MainEntity", "Entity") :: nil.
Instance CPRModel_relation : brand_relation
  := mkBrand_relation CPRModel (eq_refl _) (eq_refl _).

Module TR := TrivialRuntime.

Section CompilerUntypedTest.



  Definition makeMainEntity (db:Z) (id:string) (i:Z)
    := class (singleton "MainEntity")
             (drec [("doubleAttribute",dconst db);
                     ("intAttribute", dconst i);
                     ("id",dconst id)
             ]).

  Definition MainEntity (inp:Z×string×Z)
    := makeMainEntity (fst (fst inp)) (snd (fst inp)) (snd inp).

  Example exampleWM : list data
    := [makeMainEntity 120 "string1" 1;
         makeMainEntity 50 "string2" 2;
         makeMainEntity 125 "string3" 3;
         makeMainEntity 50 "string4" 4].



  Example Example1' :=
    ("total-attribute" IS AGGREGATE
                       (rule_when ("e" INSTANCEOF (singleton "MainEntity") WHERE ("doubleAttribute" !#-> … ≐ ‵50)))
                       DO ACount
                       OVER (withVar "e" …)
                       FLATTEN 0).

  Example Example1 :=
        rule_global
          ("total-attribute" IS AGGREGATE
                             (rule_when ("e" INSTANCEOF (singleton "MainEntity") WHERE ("doubleAttribute" !#-> … ≐ ‵50)))
                             DO ACount
                             OVER (withVar "e" …)
                             FLATTEN 0)
          ;; rule_return (‵"MainEntitys with doubleAttribute 50: "
                          +s+ toString (lookup "total-attribute")).

  Example Example1_result := eval_rule nil Example1 exampleWM.
  Example Example1_expected := map dconst
                                   ["MainEntitys with doubleAttribute 50: 2"].

  Definition pat5 : camp := Eval compute in Example1'.
  Definition algopt5 : nraenv_core := camp_to_nraenv_core Example1'.

  Definition rpat5 : rule := Eval compute in Example1.
  Definition ralgopt5 : nraenv := rule_to_nraenv_optim Example1.
  Definition rnnrc5 : nnrc := rule_to_nnrc_optim Example1.

  Definition inp1 : (list (string×data)) := (("WORLD", dcoll exampleWM)::nil).
  Definition inp2 : data := dunit.

  End CompilerUntypedTest.

  Section CompilerBrandModelTest.

    Program Definition MainEntityDataType :=
      Rec Open (("doubleAttribute", Nat) :: ("id", String) :: ("intAttribute", Nat) :: nil) _.

    Program Definition EntityType : rtype
      := Rec Open [] _.

    Definition CPTModelTypes :=
      [("Entity", EntityType);
      ("MainEntity", MainEntityDataType)
      ].

    Definition CPTModel
      := @mkBrand_context _ CPRModel_relation CPTModelTypes (eq_refl _).

    Instance CPModel : brand_model
      := mkBrand_model CPRModel_relation CPTModel (eq_refl _) (eq_refl _).

  End CompilerBrandModelTest.


  Module MyBrandModel <: CompilerBrandModel(TrivialForeignType).
    Definition compiler_brand_model := CPModel.
  End MyBrandModel.
  Module TM := TrivialModel(MyBrandModel).

  Section CompilerTypedTest.


    Lemma makeMainEntity_typed db id i:
      (normalize_data brand_relation_brands (makeMainEntity db id i)) ▹ (Brand (singleton "MainEntity")).


  Definition tout1 := Rec Closed (("total-attribute", Nat)::nil) eq_refl.

  Definition tinp1 := (("WORLD", Coll (Brand (singleton "MainEntity")))::nil).


  Lemma Example1'_wt τ :
    pat_type tinp1 nil Example1' τ tout1.




  Lemma alg5_wt τ :
    algopt5 ▷ τ >=> Coll tout1 ⊣ tinp1;(Rec Closed nil eq_refl).

End CompilerTypedTest.