Make the denotational semantics total.

1 files changed, 58 insertions, 78 deletions

diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index 359fbd4..d92c1b2 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -14,13 +14,14 @@ module Helium.Semantics.Denotational.Core
 open import Algebra.Core
 open import Data.Bool as Bool using (Bool)
 open import Data.Fin hiding (lift)
-open import Data.Maybe using (Maybe; just; nothing; map; _>>=_)
 open import Data.Nat using (ℕ; zero; suc)
 import Data.Nat.Properties as ℕₚ
-open import Data.Product using (_×_; _,_; map₂; uncurry)
+open import Data.Product hiding (_<*>_; _,′_)
 open import Data.Product.Nary.NonDependent
+open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Unit using (⊤)
-open import Level renaming (suc to ℓsuc) hiding (lift)
+open import Level renaming (suc to ℓsuc) hiding (zero)
+open import Function using (_∘_; _∘₂_; _|>_)
 open import Function.Nary.NonDependent.Base
 open import Relation.Nullary.Decidable using (True)
 
@@ -42,122 +43,101 @@ private
   update zero    y (_ , xs) = y , xs
   update (suc i) y (x , xs) = x , update i y xs
 
+PureExpr : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′)
+PureExpr n Γ τ = (σ : State) → (ρ : Product⊤ n Γ) → τ
+
 Expr : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′)
-Expr _ Γ τ = (σ : State) → (ρ : Product⊤ _ Γ) → Maybe (State × τ)
+Expr n Γ τ = (σ : State) → (ρ : Product⊤ n Γ) → State × τ
+
 
 record Reference n {ls} (Γ : Sets n ls) (τ : Set ℓ) : Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′) where
   field
-    get : Expr n Γ τ
-    set : (σ : State) → (ρ : Product⊤ _ Γ) → τ → Maybe (State × Product⊤ _ Γ)
-
-Statement : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′)
-Statement n Γ τ = (cont : Expr n Γ τ) → Expr n Γ τ
-
-ForStatement : ∀ n {ls} → Sets n ls → Set ℓ → ℕ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′)
-ForStatement n Γ τ m = (cont break : Expr n Γ τ) → Expr (suc n) (Fin m , Γ) τ
+    get : PureExpr n Γ τ
+    set : τ → (σ : State) → (ρ : Product⊤ n Γ) → State × Product⊤ n Γ
 
 Function : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′)
-Function = Statement
+Function = Expr
 
 Procedure : ∀ n {ls} → Sets n ls → Set (⨆ n ls ⊔ ℓ′)
 Procedure n Γ = Function n Γ ⊤
 
+Block : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′)
+Block n Γ τ = (σ : State) → (ρ : Product⊤ n Γ) → State × (Product⊤ n Γ ⊎ τ)
+
 -- Expressions
 
-unknown : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ τ
-unknown σ ρ = nothing
+pure′ : ∀ {n ls} {Γ : Sets n ls} → τ → PureExpr n Γ τ
+pure′ v σ ρ = v
 
 pure : ∀ {n ls} {Γ : Sets n ls} → τ → Expr n Γ τ
-pure v σ ρ = just (σ , v)
+pure v σ ρ = σ , v
 
-apply : ∀ {n ls} {Γ : Sets n ls} → (τ → τ′) → Expr n Γ τ → Expr n Γ τ′
-apply f e σ ρ = map (map₂ f) (e σ ρ)
+↓_ : ∀ {n ls} {Γ : Sets n ls} → PureExpr n Γ τ → Expr n Γ τ
+(↓ e) σ ρ = σ , e σ ρ
 
 _<*>_ : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ (τ → τ′) → Expr n Γ τ → Expr n Γ τ′
-_<*>_ f e σ ρ = f σ ρ >>= λ (σ , f) → apply f e σ ρ
+_<*>_ f e σ ρ = f σ ρ |> λ (σ , f) → map₂ f (e σ ρ)
 
-!_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Expr n Γ τ
+!_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → PureExpr n Γ τ
 ! r = Reference.get r
 
+↓!_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Expr n Γ τ
+↓! r = ↓ ! r
+
 call : ∀ {m n ls₁ ls₂} {Γ : Sets m ls₁} {Δ : Sets n ls₂} → Function m Γ τ → Expr n Δ (Product m Γ) → Expr n Δ τ
-call f e σ ρ = e σ ρ >>= λ (σ , v) → f unknown σ (toProduct⊤ _ v)
+call f e σ ρ = e σ ρ |> map₂ (toProduct⊤ _) |> uncurry f
+
+declare : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ τ → Expr (suc n) (τ , Γ) τ′ → Expr n Γ τ′
+declare e s σ ρ = e σ ρ |> map₂ (_, ρ) |> uncurry s
 
 -- References
 
 var : ∀ {n ls} {Γ : Sets n ls} i → Reference n Γ (Projₙ Γ i)
 var i = record
-  { get = λ σ ρ → just (σ , projₙ _ i (toProduct _ ρ))
-  ; set = λ σ ρ v → just (σ , update i v ρ)
+  { get = λ σ ρ → projₙ _ i (toProduct _ ρ)
+  ; set = λ v → curry (map₂ (update i v))
   }
 
-!#_ : ∀ {n ls} {Γ : Sets n ls} m {m<n : True (suc m ℕₚ.≤? n)} → Expr n Γ (Projₙ Γ (#_ m {n} {m<n}))
-(!# m) {m<n} = ! (var (#_ m {m<n = m<n}))
-
-wknRef : ∀ {m ls} {Γ : Sets m ls} → Reference m Γ τ → Reference (suc m) (τ′ , Γ) τ
-wknRef &x = record
-  { get = λ σ (_ , ρ) → Reference.get &x σ ρ
-  ; set = λ σ (v , ρ) x → Reference.set &x σ ρ x >>= λ (σ , ρ) → just (σ , (v , ρ))
-  }
+!#_ : ∀ {n ls} {Γ : Sets n ls} m {m<n : True (suc m ℕₚ.≤? n)} → PureExpr n Γ (Projₙ Γ (#_ m {n} {m<n}))
+(!# m) {m<n} = ! var (#_ m {m<n = m<n})
 
 _,′_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Reference n Γ τ′ → Reference n Γ (τ × τ′)
 &x ,′ &y = record
-  { get = λ σ ρ → Reference.get &x σ ρ >>= λ (σ , x) → Reference.get &y σ ρ >>= λ (σ , y) → just (σ , (x , y))
-  ; set = λ σ ρ (x , y) → Reference.set &x σ ρ x >>= λ (σ , ρ) → Reference.set &y σ ρ y
+  { get = λ σ ρ → Reference.get &x σ ρ , Reference.get &y σ ρ
+  ; set = λ (x , y) σ ρ → uncurry (Reference.set &y y) (Reference.set &x x σ ρ)
   }
 
--- Statements
+-- Blocks
 
 infixr 1 _∙_
-infix 4 _≔_ _⟵_
 infixl 2 if_then_else_
+infix 4 _≔_ _⟵_
 
-skip : ∀ {n ls} {Γ : Sets n ls} → Statement n Γ τ
-skip cont = cont
+skip : ∀ {n ls} {Γ : Sets n ls} → Block n Γ τ
+skip σ ρ = σ , inj₁ ρ
 
-ignore : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ τ → Statement n Γ τ′
-ignore e cont σ ρ = e σ ρ >>= λ (σ , _) → cont σ ρ
+invoke : ∀ {m n ls₁ ls₂} {Γ : Sets m ls₁} {Δ : Sets n ls₂} → Procedure m Γ → Expr n Δ (Product m Γ) → Block n Δ τ
+invoke f e σ ρ = call f e σ ρ |> map₂ (λ _ → inj₁ ρ)
 
-return : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ τ → Statement n Γ τ
-return e _ = e
+_≔_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Expr n Γ τ → Block n Γ τ′
+(&x ≔ e) σ ρ = e σ ρ |> λ (σ , x) → Reference.set &x x σ ρ |> map₂ inj₁
 
-_≔_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Expr n Γ τ → Statement n Γ τ′
-(ref ≔ e) cont σ ρ = e σ ρ >>= λ (σ , v) → Reference.set ref σ ρ v >>= λ (σ , v) → cont σ v
+_⟵_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Op₁ τ → Block n Γ τ′
+&x ⟵ e = &x ≔ ⦇ e (↓ (! &x)) ⦈
 
-_⟵_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Op₁ τ → Statement n Γ τ′
-ref ⟵ e = ref ≔ ⦇ e (! ref) ⦈
+if_then_else_ : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ Bool → Block n Γ τ → Block n Γ τ → Block n Γ τ
+(if e then b₁ else b₂) σ ρ = e σ ρ |> λ (σ , b) → Bool.if b then b₁ σ ρ else b₂ σ ρ
 
-label : ∀ {n ls} {Γ : Sets n ls} → smap _ (Reference n Γ) n Γ ⇉ Statement n Γ τ → Statement n Γ τ
-label {n = n} s = uncurry⊤ₙ n s vars
+for : ∀ {n ls} {Γ : Sets n ls} m → Block (suc n) (Fin m , Γ) τ → Block n Γ τ
+for zero    b σ ρ = σ , inj₁ ρ
+for (suc m) b σ ρ with b σ (zero , ρ)
+... | σ′ , inj₂ x        = σ′ , inj₂ x
+... | σ′ , inj₁ (_ , ρ′) = for m b′ σ′ ρ′
   where
-  vars : ∀ {n ls} {Γ : Sets n ls} → Product⊤ n (smap _ (Reference n Γ) n Γ)
-  vars {zero}  = _
-  vars {suc n} = var (# 0) , mapAll _ _ wknRef vars
-
-declare : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ τ → Statement (suc n) (τ , Γ) τ′ → Statement n Γ τ′
-declare e s cont σ ρ = e σ ρ >>= λ (σ , v) → s (λ σ (_ , ρ) → cont σ ρ) σ (v , ρ)
-
-if_then_else_ : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ Bool → Statement n Γ τ → Statement n Γ τ → Statement n Γ τ
-(if e then b₁ else b₂) cont σ ρ = e σ ρ >>= λ (σ , b) → Bool.if b then b₁ cont σ ρ else b₂ cont σ ρ
-
-for : ∀ {n ls} {Γ : Sets n ls} m → ForStatement n Γ τ m → Statement n Γ τ
-for zero    s cont σ ρ = cont σ ρ
-for (suc m) s cont σ ρ = s (for m (λ cont break σ (i , ρ) → s cont break σ (suc i , ρ)) cont) cont σ (# 0 , ρ)
-
-_∙_ : ∀ {n ls} {Γ : Sets n ls} → Op₂ (Statement n Γ τ)
-(s ∙ t) cont = s (t cont)
-
--- For statements
-
-infixr 9 _∙′_
-
-lift : ∀ {m n ls} {Γ : Sets n ls} → Statement (suc n) (Fin m , Γ) τ → ForStatement n Γ τ m
-lift s cont _ = s (λ σ (_ , ρ) → cont σ ρ)
-
-continue : ∀ {m n ls} {Γ : Sets n ls} → ForStatement n Γ τ m
-continue cont break σ (_ , ρ) = cont σ ρ
-
-break : ∀ {m n ls} {Γ : Sets n ls} → ForStatement n Γ τ m
-break cont break σ (_ , ρ) = break σ ρ
+  b′ : Block (suc _) (Fin m , _) _
+  b′ σ (i , ρ) with b σ (suc i , ρ)
+  ... | σ′ , inj₂ x        = σ′ , inj₂ x
+  ... | σ′ , inj₁ (_ , ρ′) = σ′ , inj₁ (i , ρ′)
 
-_∙′_ : ∀ {m n ls} {Γ : Sets n ls} → Op₂ (ForStatement n Γ τ m)
-(s ∙′ t) cont break σ (i , ρ) = s (λ σ ρ → t cont break σ (i , ρ)) break σ (i , ρ)
+_∙_ : ∀ {n ls} {Γ : Sets n ls} → Block n Γ τ → Expr n Γ τ → Expr n Γ τ
+(b ∙ e) σ τ = b σ τ |> λ (σ , ρ⊎x) → [ e σ , σ ,_ ]′ ρ⊎x