From 687f7031131ac12bd382be831114661be785dd0d Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sun, 13 Feb 2022 13:51:43 +0000 Subject: Finish definition of denotational semantics. --- src/Helium/Data/Pseudocode.agda | 32 ++- src/Helium/Data/Pseudocode/Core.agda | 84 ++++---- src/Helium/Data/Pseudocode/Types.agda | 264 ----------------------- src/Helium/Semantics/Denotational/Core.agda | 323 ++++++++++++++++++++++++++++ 4 files changed, 384 insertions(+), 319 deletions(-) create mode 100644 src/Helium/Semantics/Denotational/Core.agda diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda index 9e4707d..9f936f2 100644 --- a/src/Helium/Data/Pseudocode.agda +++ b/src/Helium/Data/Pseudocode.agda @@ -71,19 +71,15 @@ BeatId = state 6 -- Indirect -tup⇒array : ∀ {n Γ t m} → Expression {n} Γ (tuple (suc m) (Vec.replicate t)) → Expression Γ (array t (suc m)) -tup⇒array {m = zero} xs = [ head xs ] -tup⇒array {m = suc m} xs = [ head xs ] ∶ tup⇒array (tail xs) - group : ∀ {n Γ t k} m → Expression {n} Γ (asType t (k ℕ.* suc m)) → Expression Γ (array (asType t k) (suc m)) group {k = k} zero x = [ cast (P.trans (ℕₚ.*-comm k 1) (ℕₚ.+-comm k 0)) x ] -group {k = k} (suc m) x = [ slice (cast (ℕₚ.+-comm k _) x′) (lit (zero ′f)) ] ∶ group m (slice (cast (P.cong (k ℕ.+_) (ℕₚ.*-comm (suc m) k)) x′) (lit (Fin.fromℕ k ′f))) +group {k = k} (suc m) x = group m (slice x′ (lit (Fin.fromℕ k ′f))) ∶ [ slice (cast (ℕₚ.+-comm k _) x′) (lit (zero ′f)) ] where - x′ = cast (ℕₚ.*-comm k (suc (suc m))) x + x′ = cast (P.trans (ℕₚ.*-comm k _) (P.cong (k ℕ.+_) (ℕₚ.*-comm _ k))) x join : ∀ {n Γ t k m} → Expression {n} Γ (array (asType t k) (suc m)) → Expression Γ (asType t (k ℕ.* suc m)) join {k = k} {zero} x = cast (P.trans (ℕₚ.+-comm 0 k) (ℕₚ.*-comm 1 k)) (unbox x) -join {k = k} {suc m} x = cast eq (unbox (slice {i = suc m} (cast (ℕₚ.+-comm 1 (suc m)) x) (lit (zero ′f))) ∶ join (slice x (lit (Fin.fromℕ 1 ′f)))) +join {k = k} {suc m} x = cast eq (join (slice x (lit (Fin.fromℕ 1 ′f))) ∶ unbox (slice {i = suc m} (cast (ℕₚ.+-comm 1 _) x) (lit (zero ′f)))) where eq = P.trans (P.cong (k ℕ.+_) (ℕₚ.*-comm k (suc m))) (ℕₚ.*-comm (suc (suc m)) k) @@ -106,7 +102,7 @@ hasBit {n} x i = index x i ≟ lit ((true ∷ []) ′x) sliceⁱ : ∀ {n Γ m} → ℕ → Expression {n} Γ int → Expression Γ (bits m) sliceⁱ {m = zero} n i = lit ([] ′x) -sliceⁱ {m = suc m} n i = get (m ℕ.+ n) i ∶ sliceⁱ n i +sliceⁱ {m = suc m} n i = sliceⁱ (suc n) i ∶ get n i --- Functions @@ -126,18 +122,18 @@ SignedSatQ n = declare (lit (true ′b)) ( var 0 ≔ lit (false ′b) ∙return tup (sliceⁱ 0 (var 1) ∷ var 0 ∷ [])) where - max = lit (2 ′i) ^ lit (n ′i) + - lit (1 ′i) - min = - (lit (2 ′i) ^ lit (n ′i)) + max = lit (2 ′i) ^ n + - lit (1 ′i) + min = - (lit (2 ′i) ^ n) -- actual shift if 'shift + 1' LSL-C : ∀ {n} (shift : ℕ) → Function (bits n ∷ []) (tuple 2 (bits n ∷ bit ∷ [])) LSL-C {n} shift = declare (var 0 ∶ lit ((Vec.replicate {n = (suc shift)} false) ′x)) (skip ∙return tup - ( slice (cast (ℕₚ.+-comm n _) (var 0)) (lit (zero ′f)) - ∷ slice (cast eq₂ (var 0)) (lit (Fin.inject+ shift (Fin.fromℕ n) ′f)) + ( slice (var 0) (lit (zero ′f)) + ∷ slice (cast eq (var 0)) (lit (Fin.inject+ shift (Fin.fromℕ n) ′f)) ∷ [])) where - eq₂ = P.trans (P.cong (n ℕ.+_) (ℕₚ.+-comm 1 shift)) (P.sym (ℕₚ.+-assoc n shift 1)) + eq = P.trans (ℕₚ.+-comm 1 (shift ℕ.+ n)) (P.cong (ℕ._+ 1) (ℕₚ.+-comm shift n)) --- Procedures @@ -229,7 +225,7 @@ module _ (d : Instr.VecOp₂) where declare (lit (Vec.replicate false ′x)) ( -- 0:elmtMask 1:curBeat tup (var 1 ∷ var 0 ∷ []) ≔ call GetCurInstrBeat (tup []) ∙ - declare (lit (Vec.replicate (Vec.replicate false ′x) ′a)) ( + declare (lit ((Vec.replicate false ′x) ′a)) ( declare (from32 size (index (index Q (lit (src₁ ′f))) (var 2))) ( -- 0:op₁ 1:result 2:elmtMask 3:curBeat for (toℕ elements) ( @@ -266,7 +262,7 @@ vmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) open Instr.VMulH d; toInt = λ i → call Int (tup (i ∷ lit (unsigned ′b) ∷ [])) vrmulh : Instr.VRMulH → Procedure [] -vrmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) * toInt (var 1) + lit (1 ′i) << lit (toℕ esize-1 ′i))) +vrmulh d = vec-op₂ op₂ (skip ∙return sliceⁱ (toℕ esize) (toInt (var 0) * toInt (var 1) + lit (1 ′i) << toℕ esize-1)) where open Instr.VRMulH d; toInt = λ i → call Int (tup (i ∷ lit (unsigned ′b) ∷ [])) @@ -277,7 +273,7 @@ private declare (lit (Vec.replicate false ′x)) ( -- 0:elmtMask 1:curBeat tup (var 1 ∷ var 0 ∷ []) ≔ call GetCurInstrBeat (tup []) ∙ - declare (lit (Vec.replicate (Vec.replicate false ′x) ′a)) ( + declare (lit ((Vec.replicate false ′x) ′a)) ( declare (from32 size (index (index Q (lit (src₁ ′f))) (var 2))) ( -- 0:op₁ 1:result 2:elmtMask 3:curBeat for (toℕ elements) ( @@ -313,9 +309,9 @@ private helper Instr.32bit i = Fin.combine i zero vqdmulh : Instr.VQDMulH → Procedure [] -vqdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0 * var 1 >> lit (toℕ esize ′i)) +vqdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0 * var 1 >> toℕ esize) where open Instr.VecOp₂ d using (esize) vqrdmulh : Instr.VQRDMulH → Procedure [] -vqrdmulh d = vqr?dmulh d (skip ∙return (lit (2 ′i) * var 0 * var 1 + lit (1 ′i) << lit (toℕ esize-1 ′i)) >> lit (toℕ esize ′i)) +vqrdmulh d = vqr?dmulh d (skip ∙return lit (2 ′i) * var 0 * var 1 + lit (1 ′i) << toℕ esize-1 >> toℕ esize) where open Instr.VecOp₂ d using (esize; esize-1) diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda index 7b21824..a63cc39 100644 --- a/src/Helium/Data/Pseudocode/Core.agda +++ b/src/Helium/Data/Pseudocode/Core.agda @@ -8,9 +8,10 @@ module Helium.Data.Pseudocode.Core where -open import Data.Bool using (Bool) +open import Data.Bool using (Bool; true; false) open import Data.Fin using (Fin; #_) -open import Data.Nat as ℕ using (ℕ; suc) +open import Data.Nat as ℕ using (ℕ; zero; suc) +open import Data.Nat.Properties using (+-comm) open import Data.Product using (∃; _,_; proj₂; uncurry) open import Data.Vec using (Vec; []; _∷_; lookup; map) open import Data.Vec.Relation.Unary.All using (All; []; _∷_; reduce; all?) @@ -29,7 +30,6 @@ data Type : Set where fin : (n : ℕ) → Type real : Type bits : (n : ℕ) → Type - enum : (n : ℕ) → Type tuple : ∀ n → Vec Type n → Type array : Type → (n : ℕ) → Type @@ -42,7 +42,6 @@ data HasEquality : Type → Set where fin : ∀ {n} → HasEquality (fin n) real : HasEquality real bits : ∀ {n} → HasEquality (bits n) - enum : ∀ {n} → HasEquality (enum n) hasEquality? : Decidable HasEquality hasEquality? unit = no (λ ()) @@ -51,7 +50,6 @@ hasEquality? int = yes int hasEquality? (fin n) = yes fin hasEquality? real = yes real hasEquality? (bits n) = yes bits -hasEquality? (enum n) = yes enum hasEquality? (tuple n x) = no (λ ()) hasEquality? (array t n) = no (λ ()) @@ -66,7 +64,6 @@ isNumeric? int = yes int isNumeric? real = yes real isNumeric? (fin n) = no (λ ()) isNumeric? (bits n) = no (λ ()) -isNumeric? (enum n) = no (λ ()) isNumeric? (tuple n x) = no (λ ()) isNumeric? (array t n) = no (λ ()) @@ -95,8 +92,7 @@ data Literal : Type → Set where _′f : ∀ {n} → Fin n → Literal (fin n) _′r : ℕ → Literal real _′x : ∀ {n} → Vec Bool n → Literal (bits n) - _′e : ∀ {n} → Fin n → Literal (enum n) - _′a : ∀ {n t} → Vec (Literal t) n → Literal (array t n) + _′a : ∀ {n t} → Literal t → Literal (array t n) --- Expressions, references, statements, functions and procedures @@ -111,7 +107,8 @@ module Code {o} (Σ : Vec Type o) where infix 8 -_ infixr 7 _^_ - infixl 6 _*_ _/_ _and_ + infixl 6 _*_ _and_ _>>_ + -- infixl 6 _/_ infixl 5 _+_ _or_ _&&_ _||_ _∶_ infix 4 _≟_ _>_ : Expression Γ int → ℕ → Expression Γ int rnd : Expression Γ real → Expression Γ int - get : ℕ → Expression Γ int → Expression Γ bit + -- get : ℕ → Expression Γ int → Expression Γ bit fin : ∀ {k ms n} → (All (Fin) ms → Fin n) → Expression Γ (tuple k (map fin ms)) → Expression Γ (fin n) asInt : ∀ {n} → Expression Γ (fin n) → Expression Γ int tup : ∀ {m ts} → All (Expression Γ) ts → Expression Γ (tuple m ts) - head : ∀ {m t ts} → Expression Γ (tuple (suc m) (t ∷ ts)) → Expression Γ t - tail : ∀ {m t ts} → Expression Γ (tuple (suc m) (t ∷ ts)) → Expression Γ (tuple m ts) call : ∀ {t m Δ} → Function Δ t → Expression Γ (tuple m Δ) → Expression Γ t if_then_else_ : ∀ {t} → Expression Γ bool → Expression Γ t → Expression Γ t → Expression Γ t data CanAssign {n} {Γ} where - state : ∀ {i} {i> e₁) = no λ () canAssign? (rnd e) = no λ () - canAssign? (get x e) = no λ () + -- canAssign? (get x e) = no λ () canAssign? (fin x e) = no λ () canAssign? (asInt e) = no λ () canAssign? (tup es) = map′ tup (λ { (tup es) → es }) (canAssignAll? es) - canAssign? (head e) = map′ head (λ { (head e) → e }) (canAssign? e) - canAssign? (tail e) = map′ tail (λ { (tail e) → e }) (canAssign? e) canAssign? (call x e) = no λ () canAssign? (if e then e₁ else e₂) = no λ () @@ -222,13 +211,34 @@ module Code {o} (Σ : Vec Type o) where _∙end : Statement Γ unit → Procedure Γ declare : ∀ {t} → Expression Γ t → Procedure (t ∷ Γ) → Procedure Γ - infixl 6 _<<_ _>>_ + infixl 6 _<<_ infixl 5 _-_ + + slice′ : ∀ {n Γ i j t} → Expression {n} Γ (asType t (i ℕ.+ j)) → Expression Γ (fin (suc j)) → Expression Γ (asType t i) + slice′ {i = i} e₁ e₂ = slice (cast (+-comm i _) e₁) e₂ + _-_ : ∀ {n Γ t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression {n} Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ {isNumeric₁} {isNumeric₂}) _-_ {isNumeric₂ = isNumeric₂} x y = x + (-_ {isNumeric = isNumeric₂} y) - _<<_ : ∀ {n Γ} → Expression {n} Γ int → Expression Γ int → Expression Γ int + _<<_ : ∀ {n Γ} → Expression {n} Γ int → ℕ → Expression Γ int x << n = rnd (x * lit (2 ′r) ^ n) - _>>_ : ∀ {n Γ} → Expression {n} Γ int → Expression Γ int → Expression Γ int - x >> n = rnd (x * lit (2 ′r) ^ - n) + get : ∀ {n Γ} → ℕ → Expression {n} Γ int → Expression Γ bit + get i x = if x - x >> suc i << suc i >_ - _>>_ : ℤ → ℕ → ℤ - x >> zero = x - x >> suc n = (x div (1ℤ << suc n)) {1<> 1) - - uint : ∀ {n} → Bits n → ℤ - uint x = ℤ′.sum λ i → if hasBit i x then 1ℤ << toℕ i else 0ℤ - - sint : ∀ {n} → Bits n → ℤ - sint {zero} x = 0ℤ - sint {suc n} x = uint x ℤ.+ ℤ.- (if hasBit (fromℕ n) x then 1ℤ << suc n else 0ℤ) - record Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ ⊔ b₂ ⊔ i₁ ⊔ i₂ ⊔ i₃ ⊔ r₁ ⊔ r₂ ⊔ r₃)) where field @@ -222,191 +146,3 @@ record Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : ; _/1 = _/1 ; ⌊_⌋ = ⌊_⌋ } - - open RawPseudocode rawPseudocode public - using - ( 2ℤ; cast; getᵇ; setᵇ; sliceᵇ; updateᵇ; hasBit - ; _div_; _mod_; _<<_; uint; sint - ) - - private - -- FIXME: move almost all of these proofs into a separate module - a-a : ∀ {a} → 0ℤ ℤ.< a → 0ℤ ℤ.> ℤ.- a - 0-a {a} 0a⇒0<-a : ∀ {a} → 0ℤ ℤ.> a → 0ℤ ℤ.< ℤ.- a - 0>a⇒0<-a {a} 0>a = begin-strict - 0ℤ ≈˘⟨ ℤ.-‿inverseʳ a ⟩ - a ℤ.- a <⟨ ℤ.+-invariantʳ _ 0>a ⟩ - 0ℤ ℤ.- a ≈⟨ ℤ.+-identityˡ _ ⟩ - ℤ.- a ∎ - where open ℤ-Reasoning - - 0<-a⇒0>a : ∀ {a} → 0ℤ ℤ.< ℤ.- a → 0ℤ ℤ.> a - 0<-a⇒0>a {a} 0<-a = begin-strict - a ≈˘⟨ ℤ.+-identityʳ a ⟩ - a ℤ.+ 0ℤ <⟨ ℤ.+-invariantˡ a 0<-a ⟩ - a ℤ.- a ≈⟨ ℤ.-‿inverseʳ a ⟩ - 0ℤ ∎ - where open ℤ-Reasoning - - 0>-a⇒0 ℤ.- a → 0ℤ ℤ.< a - 0>-a⇒0-a = begin-strict - 0ℤ ≈˘⟨ ℤ.-‿inverseʳ a ⟩ - a ℤ.- a <⟨ ℤ.+-invariantˡ a 0>-a ⟩ - a ℤ.+ 0ℤ ≈⟨ ℤ.+-identityʳ a ⟩ - a ∎ - where open ℤ-Reasoning - - 0>a+0ab : ∀ {a b} → 0ℤ ℤ.> a → 0ℤ ℤ.< b → 0ℤ ℤ.> a ℤ.* b - 0>a+0ab {a} {b} 0>a 0a $ begin-strict - 0ℤ <⟨ ℤ.0a⇒0<-a 0>a) 0b⇒0>ab : ∀ {a b} → 0ℤ ℤ.< a → 0ℤ ℤ.> b → 0ℤ ℤ.> a ℤ.* b - 0b⇒0>ab {a} {b} 0b = 0<-a⇒0>a $ begin-strict - 0ℤ <⟨ ℤ.0a⇒0<-a 0>b) ⟩ - a ℤ.* ℤ.- b ≈⟨ a*-b≈-ab a b ⟩ - ℤ.- (a ℤ.* b) ∎ - where open ℤ-Reasoning - - 0>a+0>b⇒0 a → 0ℤ ℤ.> b → 0ℤ ℤ.< a ℤ.* b - 0>a+0>b⇒0a 0>b = begin-strict - 0ℤ <⟨ ℤ.0a⇒0<-a 0>a) (0>a⇒0<-a 0>b) ⟩ - ℤ.- a ℤ.* ℤ.- b ≈⟨ -a*b≈-ab a (ℤ.- b) ⟩ - ℤ.- (a ℤ.* ℤ.- b) ≈⟨ ℤ.-‿cong $ a*-b≈-ab a b ⟩ - ℤ.- (ℤ.- (a ℤ.* b)) ≈⟨ -‿idem (a ℤ.* b) ⟩ - a ℤ.* b ∎ - where open ℤ-Reasoning - - a≉0+b≉0⇒ab≉0 : ∀ {a b} → a ℤ.≉ 0ℤ → b ℤ.≉ 0ℤ → a ℤ.* b ℤ.≉ 0ℤ - a≉0+b≉0⇒ab≉0 {a} {b} a≉0 b≉0 ab≈0 with ℤ.compare a 0ℤ | ℤ.compare b 0ℤ - ... | tri< a<0 _ _ | tri< b<0 _ _ = ℤ.irrefl (ℤ.Eq.sym ab≈0) $ 0>a+0>b⇒0 _ _ b>0 = ℤ.irrefl ab≈0 $ 0>a+0ab a<0 b>0 - ... | tri≈ _ a≈0 _ | _ = a≉0 a≈0 - ... | tri> _ _ a>0 | tri< b<0 _ _ = ℤ.irrefl ab≈0 $ 0b⇒0>ab a>0 b<0 - ... | tri> _ _ a>0 | tri≈ _ b≈0 _ = b≉0 b≈0 - ... | tri> _ _ a>0 | tri> _ _ b>0 = ℤ.irrefl (ℤ.Eq.sym ab≈0) $ ℤ.00 b>0 - - ab≈0⇒a≈0⊎b≈0 : ∀ {a b} → a ℤ.* b ℤ.≈ 0ℤ → a ℤ.≈ 0ℤ ⊎ b ℤ.≈ 0ℤ - ab≈0⇒a≈0⊎b≈0 {a} {b} ab≈0 with a ℤ.≟ 0ℤ | b ℤ.≟ 0ℤ - ... | yes a≈0 | _ = inj₁ a≈0 - ... | no a≉0 | yes b≈0 = inj₂ b≈0 - ... | no a≉0 | no b≉0 = ⊥-elim (a≉0+b≉0⇒ab≉0 a≉0 b≉0 ab≈0) - - 2a< _ _ 0>1 = begin-strict - 0ℤ ≈˘⟨ ℤ.zeroʳ (ℤ.- 1ℤ) ⟩ - ℤ.- 1ℤ ℤ.* 0ℤ <⟨ aa⇒0<-a 0>1) (0>a⇒0<-a 0>1) ⟩ - ℤ.- 1ℤ ℤ.* ℤ.- 1ℤ ≈⟨ -a*b≈-ab 1ℤ (ℤ.- 1ℤ) ⟩ - ℤ.- (1ℤ ℤ.* ℤ.- 1ℤ) ≈⟨ ℤ.-‿cong $ ℤ.*-identityˡ (ℤ.- 1ℤ) ⟩ - ℤ.- (ℤ.- 1ℤ) ≈⟨ -‿idem 1ℤ ⟩ - 1ℤ ∎ - where open ℤ-Reasoning - - 0<2 : 0ℤ ℤ.< 2ℤ - 0<2 = begin-strict - 0ℤ ≈˘⟨ ℤ.+-identity² ⟩ - 0ℤ ℤ.+ 0ℤ <⟨ ℤ.+-invariantˡ 0ℤ 0<1 ⟩ - 0ℤ ℤ.+ 1ℤ <⟨ ℤ.+-invariantʳ 1ℤ 0<1 ⟩ - 2ℤ ∎ - where open ℤ-Reasoning - - 1<>_ e n ⟧ᵉ σ γ = P.map₂ (λ x → shiftr 2≉0 x n) (⟦ e ⟧ᵉ σ γ) + ⟦ rnd e ⟧ᵉ σ γ = P.map₂ ⌊_⌋ (⟦ e ⟧ᵉ σ γ) + ⟦ fin x e ⟧ᵉ σ γ = P.map₂ (apply x) (⟦ e ⟧ᵉ σ γ) + where + apply : ∀ {k ms n} → (All Fin ms → Fin n) → ⟦ Vec.map {n = k} fin ms ⟧ₜ′ → ⟦ fin n ⟧ₜ + apply {zero} {[]} f xs = f [] + apply {suc k} {_ ∷ ms} f xs = + apply (λ x → f (tupHead (Vec.map fin ms) xs ∷ x)) (tupTail (Vec.map fin ms) xs) + ⟦ asInt e ⟧ᵉ σ γ = P.map₂ (λ i → Fin.toℕ i ℤ′.×′ 1ℤ) (⟦ e ⟧ᵉ σ γ) + ⟦ tup [] ⟧ᵉ σ γ = σ , _ + ⟦ tup (e ∷ []) ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ + ⟦ tup (e ∷ e′ ∷ es) ⟧ᵉ σ γ = do + let σ′ , v = ⟦ e ⟧ᵉ σ γ + let σ′′ , vs = ⟦ tup (e′ ∷ es) ⟧ᵉ σ′ γ + σ′′ , (v , vs) + ⟦ call f e ⟧ᵉ σ γ = P.uncurry ⟦ f ⟧ᶠ (⟦ e ⟧ᵉ σ γ) + ⟦ if e then e₁ else e₂ ⟧ᵉ σ γ = do + let σ′ , x = ⟦ e ⟧ᵉ σ γ + Bool.if x then ⟦ e₁ ⟧ᵉ σ′ γ else ⟦ e₂ ⟧ᵉ σ′ γ + + ⟦ s ∙ s₁ ⟧ˢ σ γ = do + let σ′ , v = ⟦ s ⟧ˢ σ γ + S.[ ⟦ s ⟧ˢ σ′ , (λ v → σ′ , ret v) ] v + ⟦ skip ⟧ˢ σ γ = σ , next γ + ⟦ _≔_ ref {canAssign = canAssign} e ⟧ˢ σ γ = do + let σ′ , v = ⟦ e ⟧ᵉ σ γ + let σ′′ , γ′ = update (toWitness canAssign) v σ′ γ + σ′′ , next γ′ + ⟦_⟧ˢ {Γ = Γ} (declare e s) σ γ = do + let σ′ , x = ⟦ e ⟧ᵉ σ γ + let σ′′ , v = ⟦ s ⟧ˢ σ′ (tupCons Γ x γ) + σ′′ , S.map₁ (tupTail Γ) v + ⟦ invoke p e ⟧ˢ σ γ = do + let σ′ , v = ⟦ e ⟧ᵉ σ γ + ⟦ p ⟧ᵖ σ′ v , next γ + ⟦ if e then s₁ else s₂ ⟧ˢ σ γ = do + let σ′ , x = ⟦ e ⟧ᵉ σ γ + Bool.if x then ⟦ s₁ ⟧ˢ σ′ γ else ⟦ s₂ ⟧ˢ σ′ γ + ⟦_⟧ˢ {Γ = Γ} {ret = t} (for m s) σ γ = helper m ⟦ s ⟧ˢ σ γ + where + helper : ∀ m → (⟦ Σ ⟧ₜ′ → ⟦ fin m ∷ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × (⟦ fin m ∷ Γ ⟧ₜ′ ⊎ ⟦ t ⟧ₜ)) → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × (⟦ Γ ⟧ₜ′ ⊎ ⟦ t ⟧ₜ) + helper zero s σ γ = σ , next γ + helper (suc m) s σ γ with s σ (tupCons Γ zero γ) + ... | σ′ , ret v = σ′ , ret v + ... | σ′ , next γ′ = helper m s′ σ′ (tupTail Γ γ′) + where + s′ : ⟦ Σ ⟧ₜ′ → ⟦ fin m ∷ Γ ⟧ₜ′ → ⟦ Σ ⟧ₜ′ × (⟦ fin m ∷ Γ ⟧ₜ′ ⊎ ⟦ t ⟧ₜ) + s′ σ γ = + P.map₂ (S.map₁ (tupCons Γ (tupHead Γ γ) ∘′ (tupTail Γ))) + (s σ (tupCons Γ (suc (tupHead Γ γ)) (tupTail Γ γ))) + + ⟦ s ∙return e ⟧ᶠ σ γ with ⟦ s ⟧ˢ σ γ + ... | σ′ , ret v = σ′ , v + ... | σ′ , next γ′ = ⟦ e ⟧ᵉ σ′ γ′ + ⟦_⟧ᶠ {Γ = Γ} (declare e f) σ γ = do + let σ′ , x = ⟦ e ⟧ᵉ σ γ + ⟦ f ⟧ᶠ σ′ (tupCons Γ x γ) + + ⟦ s ∙end ⟧ᵖ σ γ = P.proj₁ (⟦ s ⟧ˢ σ γ) + ⟦_⟧ᵖ {Γ = Γ} (declare e p) σ γ = do + let σ′ , x = ⟦ e ⟧ᵉ σ γ + ⟦ p ⟧ᵖ σ′ (tupCons Γ x γ) + + update (state i {i