ULC.Semantics

module ULC.Semantics where

open import ULC.Variables
open import ULC.Terms
open import ULC.Domains
open import ULC.Environments

⟦_⟧ : Exp → Env → D∞
-- ⟦ e ⟧ ρ is the value of e with ρ giving the values of free variables 

⟦ var  v      ⟧ ρ  = ρ v
⟦ lam  v e    ⟧ ρ  = from ( λ d → ⟦ e ⟧ (ρ [ d / v ]) )
⟦ app  e₁ e₂  ⟧ ρ  = to ( ⟦ e₁ ⟧ ρ ) ( ⟦ e₂ ⟧ ρ )