Qcert.NRA.Typing.TDomain

Section TDomain.




  Context {ftype:foreign_type}.

  Definition tdomain (l:list (string × rtype₀)) : list string
    := map fst l.

  Definition tprojecto (l:list (string × rtype₀)) (ats:list string) : list (option (string × rtype₀)) :=
    projectr string_dec l ats.

  Fixpoint tprojectaux (l:list (option (string × rtype₀))) :=
    match l with
      | nil ⇒ nil
      | None :: r ⇒ tprojectaux r
      | (Some x) :: r ⇒ x :: (tprojectaux r)
    end.

  Definition tproject (l:list (string × rtype₀)) (ats:list string) :=
    tprojectaux (tprojecto l ats).

  Lemma lookup_in_domain l (a:string) :
    In a (tdomain l) → (∃ y, assoc_lookupr string_dec l a = Some y).

  Lemma lookup_in_included_domain ats l (a:string) :
    domains_included ats (tdomain l) → In a ats → (∃ y, assoc_lookupr string_dec l a = Some y).

  Lemma preserves_tdomain (l:list (string × rtype₀)) (ats:list string) :
    domains_included ats (tdomain l) → (tdomain (tproject l ats)) = ats.

End TDomain.

Section dom.
  Lemma nra_domain {m:basic_model} {τin τout} (op:nra) :
    op ▷ τin >=> τout → list string.

End dom.

Notation "d1 # d2" := (domains_disjoint d1 d2) (at level 70) : nra_scope.
Notation "x ∈ d" := (in_domain d x) (at level 70) : nra_scope. Notation "x ∉ d" := (not_in_domain d x) (at level 70) : nra_scope. Notation "d1 ⊆ d2" := (domains_included d1 d2) (at level 70) : nra_scope.
Notation "pf ⊨ 𝓐( op )" := (nra_domain op pf) (at level 70) : nra_scope.