From 9901eac3a64249b58789588385a10df9802c9f42 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Wed, 12 Jan 2022 18:32:48 +0000 Subject: Eliminate even more state from the denotational semantics. --- src/Helium/Semantics/Denotational.agda | 90 ++++++++++++++--------------- src/Helium/Semantics/Denotational/Core.agda | 87 ++++++++++++---------------- 2 files changed, 81 insertions(+), 96 deletions(-) (limited to 'src') diff --git a/src/Helium/Semantics/Denotational.agda b/src/Helium/Semantics/Denotational.agda index 2a18957..3a616c0 100644 --- a/src/Helium/Semantics/Denotational.agda +++ b/src/Helium/Semantics/Denotational.agda @@ -23,7 +23,7 @@ import Data.Nat.Properties as ℕₚ open import Data.Product using (∃; _×_; _,_; dmap) open import Data.Sum using ([_,_]′) open import Data.Vec.Functional as V using (Vector; []; _∷_) -open import Function using (_$_; _∘₂_) +open import Function using (_|>_; _$_; _∘₂_) open import Function.Nary.NonDependent.Base import Helium.Instructions as Instr import Helium.Semantics.Denotational.Core as Core @@ -68,19 +68,19 @@ ElmtMask = Bits 4 -- State properties -&R : ∀ {n ls} {Γ : Sets n ls} → PureExpr n Γ (Fin 16) → Reference n Γ (Bits 32) +&R : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ (Fin 16) → Reference n Γ (Bits 32) &R e = record { get = λ σ ρ → State.R σ (e σ ρ) ; set = λ x σ ρ → record σ { R = V.updateAt (e σ ρ) (λ _ → x) (State.R σ) } , ρ } -&S : ∀ {n ls} {Γ : Sets n ls} → PureExpr n Γ (Fin 32) → Reference n Γ (Bits 32) +&S : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ (Fin 32) → Reference n Γ (Bits 32) &S e = record { get = λ σ ρ → State.S σ (e σ ρ) ; set = λ x σ ρ → record σ { S = V.updateAt (e σ ρ) (λ _ → x) (State.S σ) } , ρ } -&Q : ∀ {n ls} {Γ : Sets n ls} → PureExpr n Γ Instr.VecReg → PureExpr n Γ Beat → Reference n Γ (Bits 32) +&Q : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ Instr.VecReg → Expr n Γ Beat → Reference n Γ (Bits 32) &Q reg beat = &S λ σ ρ → combine (reg σ ρ) (beat σ ρ) &FPSCR-QC : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ Bit @@ -115,7 +115,7 @@ ElmtMask = Bits 4 ; set = λ x σ ρ → Reference.set &v (cast (sym eq) x) σ ρ } -slice : ∀ {k m n ls} {Γ : Sets n ls} → Reference n Γ (Bits m) → PureExpr n Γ (∃ λ (i : Fin (suc m)) → ∃ λ j → toℕ (i - j) ≡ k) → Reference n Γ (Bits k) +slice : ∀ {k m n ls} {Γ : Sets n ls} → Reference n Γ (Bits m) → Expr n Γ (∃ λ (i : Fin (suc m)) → ∃ λ j → toℕ (i - j) ≡ k) → Reference n Γ (Bits k) slice &v idx = record { get = λ σ ρ → let (i , j , i-j≡k) = idx σ ρ in cast i-j≡k (sliceᵇ i j (Reference.get &v σ ρ)) ; set = λ v σ ρ → @@ -123,7 +123,7 @@ slice &v idx = record Reference.set &v (updateᵇ i j (cast (sym (i-j≡k)) v) (Reference.get &v σ ρ)) σ ρ } -elem : ∀ {k n ls} {Γ : Sets n ls} m → Reference n Γ (Bits (k * m)) → PureExpr n Γ (Fin k) → Reference n Γ (Bits m) +elem : ∀ {k n ls} {Γ : Sets n ls} m → Reference n Γ (Bits (k * m)) → Expr n Γ (Fin k) → Reference n Γ (Bits m) elem m &v idx = slice &v (λ σ ρ → helper _ _ (idx σ ρ)) where helper : ∀ m n → Fin m → ∃ λ (i : Fin (suc (m * n))) → ∃ λ j → toℕ (i - j) ≡ n @@ -158,11 +158,11 @@ copyMasked : Instr.VecReg → Procedure 3 (Bits 32 , Beat , ElmtMask , _) copyMasked dest = for 4 ( -- 0:e 1:result 2:beat 3:elmtMask - if ⦇ hasBit (↓ !# 0) (↓ !# 3) ⦈ + if ⦇ hasBit (!# 0) (!# 3) ⦈ then - elem 8 (&Q (pure′ dest) (!# 2)) (!# 0) ≔ ↓! elem 8 (var (# 1)) (!# 0) - else skip) ∙ - ⦇ _ ⦈ + elem 8 (&Q ⦇ dest ⦈ (!# 2)) (!# 0) ≔ ! elem 8 (var (# 1)) (!# 0) + else skip) + ∙end module fun-sliceᶻ (1<> toℕ esize) - (↓! elem (toℕ esize) (&cast (sym e*e≡32) (var (# 2))) (!# 0)) - ([ (λ src₂ → ↓! slice (&R (pure′ src₂)) (pure′ (esize , zero , refl))) - , (λ src₂ → ↓! elem (toℕ esize) (&cast (sym e*e≡32) (&Q (pure′ src₂) (!# 4))) (!# 0)) + (! elem (toℕ esize) (&cast (sym e*e≡32) (var (# 2))) (!# 0)) + ([ (λ src₂ → ! slice (&R ⦇ src₂ ⦈) ⦇ (esize , zero , refl) ⦈) + , (λ src₂ → ! elem (toℕ esize) (&cast (sym e*e≡32) (&Q ⦇ src₂ ⦈ (!# 4))) (!# 0)) ]′ src₂) ⦈ ∙ - if ↓ !# 1 - then if ⦇ (λ m e → hasBit (combine e zero) (cast (sym e*e>>3≡4) m)) (↓ !# 5) (↓ !# 0) ⦈ + if !# 1 + then if ⦇ (λ m e → hasBit (combine e zero) (cast (sym e*e>>3≡4) m)) (!# 5) (!# 0) ⦈ then &FPSCR-QC ≔ ⦇ 1𝔹 ⦈ else skip else skip) ∙ - invoke (copyMasked dest) ⦇ ↓ !# 2 , ⦇ ↓ !# 3 , ↓ !# 4 ⦈ ⦈ ∙ - ⦇ _ ⦈ + invoke (copyMasked dest) ⦇ !# 2 , ⦇ !# 3 , !# 4 ⦈ ⦈ + ∙end where open Instr.VQDMulH d rval = Bool.if rounding then 1ℤ << toℕ esize-1 else 0ℤ @@ -306,5 +306,5 @@ module _ open List using (List; []; _∷_) ⟦_⟧ : List (Instr.Instruction) → Procedure 0 _ - ⟦ [] ⟧ = ⦇ _ ⦈ - ⟦ i ∷ is ⟧ = invoke ⟦ i ⟧₁ ⦇ _ ⦈ ∙ ⟦ is ⟧ + ⟦ [] ⟧ = skip ∙end + ⟦ i ∷ is ⟧ = invoke ⟦ i ⟧₁ ⦇ _ ⦈ ∙ invoke ⟦ is ⟧ ⦇ _ ⦈ ∙end diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda index d92c1b2..9b6a3c8 100644 --- a/src/Helium/Semantics/Denotational/Core.agda +++ b/src/Helium/Semantics/Denotational/Core.agda @@ -18,7 +18,7 @@ open import Data.Nat using (ℕ; zero; suc) import Data.Nat.Properties as ℕₚ open import Data.Product hiding (_<*>_; _,′_) open import Data.Product.Nary.NonDependent -open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′) +open import Data.Sum using (_⊎_; inj₁; inj₂; fromInj₂; [_,_]′) open import Data.Unit using (⊤) open import Level renaming (suc to ℓsuc) hiding (zero) open import Function using (_∘_; _∘₂_; _|>_) @@ -30,65 +30,43 @@ private ℓ ℓ₁ ℓ₂ : Level τ τ′ : Set ℓ - mapAll : ∀ {m ls} {Γ : Sets m ls} {l l′} - (f : ∀ {ℓ} → Set ℓ → Set (l ℓ)) - (g : ∀ {ℓ} → Set ℓ → Set (l′ ℓ)) - (h : ∀ {a} {A : Set a} → f A → g A) → - Product⊤ m (smap l f m Γ) → - Product⊤ m (smap l′ g m Γ) - mapAll {zero} f g h xs = xs - mapAll {suc m} f g h (x , xs) = h x , mapAll f g h xs - update : ∀ {n ls} {Γ : Sets n ls} i → Projₙ Γ i → Product⊤ n Γ → Product⊤ n Γ 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 n Γ τ = (σ : State) → (ρ : Product⊤ n Γ) → State × τ - +Expr n Γ τ = (σ : State) → (ρ : Product⊤ n Γ) → τ record Reference n {ls} (Γ : Sets n ls) (τ : Set ℓ) : Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′) where field - get : PureExpr n Γ τ - set : τ → (σ : State) → (ρ : Product⊤ n Γ) → State × Product⊤ n Γ + get : Expr n Γ τ + set : τ → Expr n Γ (State × Product⊤ n Γ) Function : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′) -Function = Expr +Function n Γ τ = Expr n Γ τ Procedure : ∀ n {ls} → Sets n ls → Set (⨆ n ls ⊔ ℓ′) -Procedure n Γ = Function n Γ ⊤ +Procedure n Γ = Expr n Γ State -Block : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′) -Block n Γ τ = (σ : State) → (ρ : Product⊤ n Γ) → State × (Product⊤ n Γ ⊎ τ) +Statement : ∀ n {ls} → Sets n ls → Set ℓ → Set (ℓ ⊔ ⨆ n ls ⊔ ℓ′) +Statement n Γ τ = Expr n Γ (State × (Product⊤ n Γ ⊎ τ)) -- Expressions -pure′ : ∀ {n ls} {Γ : Sets n ls} → τ → PureExpr n Γ τ -pure′ v σ ρ = v - pure : ∀ {n ls} {Γ : Sets n ls} → τ → Expr n Γ τ -pure v σ ρ = σ , v - -↓_ : ∀ {n ls} {Γ : Sets n ls} → PureExpr n Γ τ → Expr n Γ τ -(↓ e) σ ρ = σ , e σ ρ +pure v σ ρ = v _<*>_ : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ (τ → τ′) → Expr n Γ τ → Expr n Γ τ′ -_<*>_ f e σ ρ = f σ ρ |> λ (σ , f) → map₂ f (e σ ρ) +_<*>_ f e σ ρ = f σ ρ |> λ f → f (e σ ρ) -!_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → PureExpr n Γ τ +!_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Expr 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 σ ρ |> map₂ (toProduct⊤ _) |> uncurry f +call f e σ ρ = e σ ρ |> toProduct⊤ _ |> f σ declare : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ τ → Expr (suc n) (τ , Γ) τ′ → Expr n Γ τ′ -declare e s σ ρ = e σ ρ |> map₂ (_, ρ) |> uncurry s +declare e s σ ρ = e σ ρ |> _, ρ |> s σ -- References @@ -98,7 +76,7 @@ var i = record ; set = λ v → curry (map₂ (update i v)) } -!#_ : ∀ {n ls} {Γ : Sets n ls} m {m map₂ (λ _ → inj₁ ρ) +invoke : ∀ {m n ls₁ ls₂} {Γ : Sets m ls₁} {Δ : Sets n ls₂} → Procedure m Γ → Expr n Δ (Product m Γ) → Statement n Δ τ +invoke f e σ ρ = call f e σ ρ |> _, inj₁ ρ -_≔_ : ∀ {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 Γ τ′ +(&x ≔ e) σ ρ = e σ ρ |> λ x → Reference.set &x x σ ρ |> map₂ inj₁ -_⟵_ : ∀ {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 Γ τ′ +&x ⟵ e = &x ≔ ⦇ e (! &x) ⦈ -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₂ σ ρ +if_then_else_ : ∀ {n ls} {Γ : Sets n ls} → Expr n Γ Bool → Statement n Γ τ → Statement n Γ τ → Statement n Γ τ +(if e then b₁ else b₂) σ ρ = e σ ρ |> (Bool.if_then b₁ σ ρ else b₂ σ ρ) -for : ∀ {n ls} {Γ : Sets n ls} m → Block (suc n) (Fin m , Γ) τ → Block n Γ τ +for : ∀ {n ls} {Γ : Sets n ls} m → Statement (suc n) (Fin m , Γ) τ → Statement n Γ τ for zero b σ ρ = σ , inj₁ ρ for (suc m) b σ ρ with b σ (zero , ρ) ... | σ′ , inj₂ x = σ′ , inj₂ x ... | σ′ , inj₁ (_ , ρ′) = for m b′ σ′ ρ′ where - b′ : Block (suc _) (Fin m , _) _ + b′ : Statement (suc _) (Fin m , _) _ b′ σ (i , ρ) with b σ (suc i , ρ) ... | σ′ , inj₂ x = σ′ , inj₂ x ... | σ′ , inj₁ (_ , ρ′) = σ′ , inj₁ (i , ρ′) -_∙_ : ∀ {n ls} {Γ : Sets n ls} → Block n Γ τ → Expr n Γ τ → Expr n Γ τ -(b ∙ e) σ τ = b σ τ |> λ (σ , ρ⊎x) → [ e σ , σ ,_ ]′ ρ⊎x +_∙_ : ∀ {n ls} {Γ : Sets n ls} → Statement n Γ τ → Statement n Γ τ → Statement n Γ τ +(b₁ ∙ b₂) σ ρ = b₁ σ ρ |> λ (σ , ρ⊎x) → [ b₂ σ , (σ ,_) ∘ inj₂ ]′ ρ⊎x + +_∙end : ∀ {n ls} {Γ : Sets n ls} → Statement n Γ ⊤ → Procedure n Γ +_∙end s σ ρ = s σ ρ |> proj₁ + +_∙return_ : ∀ {n ls} {Γ : Sets n ls} → Statement n Γ τ → Expr n Γ τ → Function n Γ τ +(s ∙return e) σ ρ = s σ ρ |> λ (σ , ρ⊎x) → fromInj₂ (e σ) ρ⊎x -- cgit v1.2.3