Qcert.Rule.Typing.TRule

Section TRule.



  Context {m:basic_model}.

  Definition mkTWorld (τworld:rtype) : tbindings
    := ("WORLD",Coll τworld)::nil.

  Definition rule_type (τworld τout:rtype) (r:rule) : Prop :=
    pat_type (mkTWorld τworld) nil (rule_to_pattern r) Unit τout.

  Lemma typed_rule_correct {τworld τout} (r:rule):
    rule_type τworld τout r →
    ∀ (world:list data),
      bindings_type (mkWorld world) (mkTWorld τworld) →
      (∃ d, eval_rule brand_relation_brands r world = Some (d::nil) ∧ (data_type d τout))
      ∨ (eval_rule brand_relation_brands r world = Some nil).

End TRule.