\begin{code}
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 β†’ 𝐋
𝐂     =  𝐒 β†’ 𝐀
\end{code}
\iflatex
\clearpage
\fi
\begin{code}
-- Injections, tests, and projections

postulate
  _𝐓-in-𝐄    : 𝐓   β†’ 𝐄
  _∈-𝐓       : 𝐄   β†’ Bool +βŠ₯
  _|-𝐓       : 𝐄   β†’ 𝐓

  _𝐑-in-𝐄    : 𝐑   β†’ 𝐄
  _∈-𝐑       : 𝐄   β†’ Bool +βŠ₯
  _|-𝐑       : 𝐄   β†’ 𝐑

  _𝐏-in-𝐄    : 𝐏  β†’ 𝐄
  _∈-𝐏       : 𝐄   β†’ Bool +βŠ₯
  _|-𝐏       : 𝐄   β†’ 𝐏

  _𝐌-in-𝐄    : 𝐌   β†’ 𝐄
  _∈-𝐌       : 𝐄   β†’ Bool +βŠ₯
  _|-𝐌       : 𝐄   β†’ 𝐌

  _𝐅-in-𝐄    : 𝐅   β†’ 𝐄
  _∈-𝐅       : 𝐄   β†’ Bool +βŠ₯
  _|-𝐅       : 𝐄   β†’ 𝐅

-- Operations on flat domains

postulate
  _==α΄Έ_  : 𝐋 β†’ 𝐋 β†’ 𝐓
  _==α΄Ή_  : 𝐌 β†’ 𝐌 β†’ 𝐓
  _==α΄Ώ_  : 𝐑 β†’ 𝐑 β†’ 𝐓
  _==α΅€_  : 𝐓 β†’ 𝐓 β†’ 𝐓
  _<α΄Ώ_   : 𝐑 β†’ 𝐑 β†’ 𝐓
  _+α΄Ώ_   : 𝐑 β†’ 𝐑 β†’ 𝐑
  _βˆ§α΅€_   : 𝐓 β†’ 𝐓 β†’ 𝐓
\end{code}