Scm.Domain-Equations
module Scm.Domain-Equations where open import Scm.Notation open import Scm.Abstract-Syntax using (Ide; Int) -- Domain declarations postulate π : Domain -- locations variable Ξ± : π π : Domain -- natural numbers π : Domain -- booleans π : Domain -- numbers π : Domain -- pairs π : Domain -- miscellaneous variable ΞΌ : π π : Domain -- procedure values variable Ο : π postulate π : Domain -- expressed values variable Ο΅ : π π : Domain -- stores variable Ο : π π : Domain -- environments variable Ο : π π : Domain -- command continuations variable ΞΈ : π postulate π : Domain -- answers πβ = π β variable Ο΅β : πβ -- Domain equations data Misc : Set where null unallocated undefined unspecified : Misc π = Natβ₯ π = Boolβ₯ π = Int +β₯ π = π Γ π π = Misc +β₯ π = πβ β (π β π) β π -- π = π + π + π + π + π π = π β π π = Ide β π π = π β π
\iflatex \clearpage \fi
-- Injections, tests, and projections postulate _π-in-π : π β π _β-π : π β Bool +β₯ _|-π : π β π _π-in-π : π β π _β-π : π β Bool +β₯ _|-π : π β π _π-in-π : π β π _β-π : π β Bool +β₯ _|-π : π β π _π-in-π : π β π _β-π : π β Bool +β₯ _|-π : π β π _π -in-π : π β π _β-π : π β Bool +β₯ _|-π : π β π -- Operations on flat domains postulate _==α΄Έ_ : π β π β π _==α΄Ή_ : π β π β π _==α΄Ώ_ : π β π β π _==α΅_ : π β π β π _<α΄Ώ_ : π β π β π _+α΄Ώ_ : π β π β π _β§α΅_ : π β π β π