From 5250643e58e3eb4d277178f06c8984027ca3e01a Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sat, 19 Feb 2022 16:06:57 +0000 Subject: Unalias bit type. --- src/Helium/Semantics/Core.agda | 82 ----------------------------- src/Helium/Semantics/Denotational/Core.agda | 67 +++++++++++++++++++---- 2 files changed, 56 insertions(+), 93 deletions(-) delete mode 100644 src/Helium/Semantics/Core.agda (limited to 'src/Helium/Semantics') diff --git a/src/Helium/Semantics/Core.agda b/src/Helium/Semantics/Core.agda deleted file mode 100644 index 749e1ca..0000000 --- a/src/Helium/Semantics/Core.agda +++ /dev/null @@ -1,82 +0,0 @@ ------------------------------------------------------------------------- --- Agda Helium --- --- Shared definitions between semantic systems ------------------------------------------------------------------------- - -{-# OPTIONS --safe --without-K #-} - -open import Helium.Data.Pseudocode.Types using (RawPseudocode) - -module Helium.Semantics.Core - {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃} - (rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃) - where - -private - open module C = RawPseudocode rawPseudocode - -open import Data.Bool using (Bool) -open import Data.Fin using (Fin; zero; suc) -open import Data.Product using (_×_; _,_) -open import Data.Unit using (⊤) -open import Data.Vec using (Vec; []; _∷_; lookup) -open import Helium.Data.Pseudocode.Core -open import Level hiding (zero; suc) - -⟦_⟧ₗ : Type → Level -⟦ bool ⟧ₗ = 0ℓ -⟦ int ⟧ₗ = i₁ -⟦ fin n ⟧ₗ = 0ℓ -⟦ real ⟧ₗ = r₁ -⟦ bits n ⟧ₗ = b₁ -⟦ tuple n ts ⟧ₗ = helper ts - where - helper : ∀ {n} → Vec Type n → Level - helper [] = 0ℓ - helper (t ∷ ts) = ⟦ t ⟧ₗ ⊔ helper ts -⟦ array t n ⟧ₗ = ⟦ t ⟧ₗ - -⟦_⟧ₜ : ∀ t → Set ⟦ t ⟧ₗ -⟦_⟧ₜ′ : ∀ {n} ts → Set ⟦ tuple n ts ⟧ₗ - -⟦ bool ⟧ₜ = Bool -⟦ int ⟧ₜ = ℤ -⟦ fin n ⟧ₜ = Fin n -⟦ real ⟧ₜ = ℝ -⟦ bits n ⟧ₜ = Bits n -⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′ -⟦ array t n ⟧ₜ = Vec ⟦ t ⟧ₜ n - -⟦ [] ⟧ₜ′ = ⊤ -⟦ t ∷ [] ⟧ₜ′ = ⟦ t ⟧ₜ -⟦ t ∷ t′ ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ t′ ∷ ts ⟧ₜ′ - -⟦_⟧ₜˡ : Type → Set (b₁ ⊔ i₁ ⊔ r₁) -⟦_⟧ₜˡ′ : ∀ {n} → Vec Type n → Set (b₁ ⊔ i₁ ⊔ r₁) - -⟦ bool ⟧ₜˡ = Lift (b₁ ⊔ i₁ ⊔ r₁) Bool -⟦ int ⟧ₜˡ = Lift (b₁ ⊔ r₁) ℤ -⟦ fin n ⟧ₜˡ = Lift (b₁ ⊔ i₁ ⊔ r₁) (Fin n) -⟦ real ⟧ₜˡ = Lift (b₁ ⊔ i₁) ℝ -⟦ bits n ⟧ₜˡ = Lift (i₁ ⊔ r₁) (Bits n) -⟦ tuple n ts ⟧ₜˡ = ⟦ ts ⟧ₜˡ′ -⟦ array t n ⟧ₜˡ = Vec ⟦ t ⟧ₜˡ n - -⟦ [] ⟧ₜˡ′ = Lift (b₁ ⊔ i₁ ⊔ r₁) ⊤ -⟦ t ∷ [] ⟧ₜˡ′ = ⟦ t ⟧ₜˡ -⟦ t ∷ t′ ∷ ts ⟧ₜˡ′ = ⟦ t ⟧ₜˡ × ⟦ t′ ∷ ts ⟧ₜˡ′ - -fetch : ∀ {n} ts → ⟦ tuple n ts ⟧ₜ → ∀ i → ⟦ lookup ts i ⟧ₜ -fetch (_ ∷ []) x zero = x -fetch (_ ∷ _ ∷ _) (x , xs) zero = x -fetch (_ ∷ t ∷ ts) (x , xs) (suc i) = fetch (t ∷ ts) xs i - -fetchˡ : ∀ {n} ts → ⟦ tuple n ts ⟧ₜˡ → ∀ i → ⟦ lookup ts i ⟧ₜˡ -fetchˡ (_ ∷ []) x zero = x -fetchˡ (_ ∷ _ ∷ _) (x , xs) zero = x -fetchˡ (_ ∷ t ∷ ts) (x , xs) (suc i) = fetchˡ (t ∷ ts) xs i - -consˡ : ∀ {n t} ts → ⟦ t ⟧ₜˡ → ⟦ tuple n ts ⟧ₜˡ → ⟦ t ∷ ts ⟧ₜˡ′ -consˡ [] x xs = x -consˡ (_ ∷ _) x xs = x , xs diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda index 6ec0b24..46d68bc 100644 --- a/src/Helium/Semantics/Denotational/Core.agda +++ b/src/Helium/Semantics/Denotational/Core.agda @@ -29,21 +29,57 @@ open import Data.Vec.Relation.Unary.All using (All; []; _∷_) import Data.Vec.Functional as VecF open import Function using (case_of_; _∘′_; id) open import Helium.Data.Pseudocode.Core -open import Helium.Semantics.Core rawPseudocode import Induction as I import Induction.WellFounded as Wf +open import Level using (Level; _⊔_; 0ℓ) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) open import Relation.Nullary using (does) open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromWitness) +⟦_⟧ₗ : Type → Level +⟦ bool ⟧ₗ = 0ℓ +⟦ int ⟧ₗ = i₁ +⟦ fin n ⟧ₗ = 0ℓ +⟦ real ⟧ₗ = r₁ +⟦ bit ⟧ₗ = b₁ +⟦ bits n ⟧ₗ = b₁ +⟦ tuple n ts ⟧ₗ = helper ts + where + helper : ∀ {n} → Vec Type n → Level + helper [] = 0ℓ + helper (t ∷ ts) = ⟦ t ⟧ₗ ⊔ helper ts +⟦ array t n ⟧ₗ = ⟦ t ⟧ₗ + +⟦_⟧ₜ : ∀ t → Set ⟦ t ⟧ₗ +⟦_⟧ₜ′ : ∀ {n} ts → Set ⟦ tuple n ts ⟧ₗ + +⟦ bool ⟧ₜ = Bool +⟦ int ⟧ₜ = ℤ +⟦ fin n ⟧ₜ = Fin n +⟦ real ⟧ₜ = ℝ +⟦ bit ⟧ₜ = Bit +⟦ bits n ⟧ₜ = Bits n +⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′ +⟦ array t n ⟧ₜ = Vec ⟦ t ⟧ₜ n + +⟦ [] ⟧ₜ′ = ⊤ +⟦ t ∷ [] ⟧ₜ′ = ⟦ t ⟧ₜ +⟦ t ∷ t′ ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ t′ ∷ ts ⟧ₜ′ + -- The case for bitvectors looks odd so that the right-most bit is bit 0. 𝒦 : ∀ {t} → Literal t → ⟦ t ⟧ₜ -𝒦 (x ′b) = x -𝒦 (x ′i) = x ℤ′.×′ 1ℤ -𝒦 (x ′f) = x -𝒦 (x ′r) = x ℝ′.×′ 1ℝ -𝒦 (xs ′x) = Vec.foldl Bits (λ bs b → (Bool.if b then 1𝔹 else 0𝔹) VecF.∷ bs) VecF.[] xs -𝒦 (x ′a) = Vec.replicate (𝒦 x) +𝒦 (x ′b) = x +𝒦 (x ′i) = x ℤ′.×′ 1ℤ +𝒦 (x ′f) = x +𝒦 (x ′r) = x ℝ′.×′ 1ℝ +𝒦 (x ′x) = Bool.if x then 1𝔹 else 0𝔹 +𝒦 (xs ′xs) = Vec.foldl Bits (λ bs b → (Bool.if b then 1𝔹 else 0𝔹) VecF.∷ bs) VecF.[] xs +𝒦 (x ′a) = Vec.replicate (𝒦 x) + +fetch : ∀ {n} ts → ⟦ tuple n ts ⟧ₜ → ∀ i → ⟦ Vec.lookup ts i ⟧ₜ +fetch (_ ∷ []) x zero = x +fetch (_ ∷ _ ∷ _) (x , xs) zero = x +fetch (_ ∷ t ∷ ts) (x , xs) (suc i) = fetch (t ∷ ts) xs i updateAt : ∀ {n} ts i → ⟦ Vec.lookup ts i ⟧ₜ → ⟦ tuple n ts ⟧ₜ → ⟦ tuple n ts ⟧ₜ updateAt (_ ∷ []) zero v _ = v @@ -66,6 +102,7 @@ equal bool x y = does (x Bool.≟ y) equal int x y = does (x ≟ᶻ y) equal fin x y = does (x Fin.≟ y) equal real x y = does (x ≟ʳ y) +equal bit x y = does (x ≟ᵇ₁ y) equal bits x y = does (x ≟ᵇ y) comp : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → Bool @@ -118,6 +155,14 @@ updateSliced t {i} {j} orig off v f = f (casted t (≡.sym eq) (join t (join t u dropped = take t (Fin.toℕ off) (casted t eq orig) untaken = drop t j (drop t (Fin.toℕ off) (casted t eq orig)) +box : ∀ t → ⟦ elemType t ⟧ₜ → ⟦ asType t 1 ⟧ₜ +box bits v = v VecF.∷ VecF.[] +box (array t) v = v ∷ [] + +unboxed : ∀ t → ⟦ asType t 1 ⟧ₜ → ⟦ elemType t ⟧ₜ +unboxed bits v = v (Fin.zero) +unboxed (array t) (v ∷ []) = v + neg : ∀ {t} → IsNumeric t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ neg int x = ℤ.- x neg real x = ℝ.- x @@ -167,8 +212,8 @@ module Expression ⟦ not e ⟧ᵉ σ γ = Bits.¬_ (⟦ e ⟧ᵉ σ γ) ⟦ e and e₁ ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ Bits.∧ ⟦ e₁ ⟧ᵉ σ γ ⟦ e or e₁ ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ Bits.∨ ⟦ e₁ ⟧ᵉ σ γ - ⟦ [ e ] ⟧ᵉ σ γ = ⟦ e ⟧ᵉ σ γ Vec.∷ [] - ⟦ unbox e ⟧ᵉ σ γ = Vec.head (⟦ e ⟧ᵉ σ γ) + ⟦ [_] {t = t} e ⟧ᵉ σ γ = box t (⟦ e ⟧ᵉ σ γ) + ⟦ unbox {t = t} e ⟧ᵉ σ γ = unboxed t (⟦ e ⟧ᵉ σ γ) ⟦ _∶_ {t = t} e e₁ ⟧ᵉ σ γ = join t (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ) ⟦ slice {t = t} e e₁ ⟧ᵉ σ γ = sliced t (⟦ e ⟧ᵉ σ γ) (⟦ e₁ ⟧ᵉ σ γ) ⟦ cast {t = t} eq e ⟧ᵉ σ γ = casted t eq (⟦ e ⟧ᵉ σ γ) @@ -224,8 +269,8 @@ module Expression update (_∶_ {m = m} {t = t} e e₁) v σ γ = do let σ′ , γ′ = update e (sliced t v (Fin.fromℕ _)) σ γ update e₁ (sliced t (casted t (ℕₚ.+-comm _ m) v) zero) σ′ γ′ - update [ e ] v σ γ = update e (Vec.head v) σ γ - update (unbox e) v σ γ = update e (v ∷ []) σ γ + update ([_] {t = t} e) v σ γ = update e (unboxed t v) σ γ + update (unbox {t = t} e) v σ γ = update e (box t v) σ γ update (slice {t = t} {e₁ = e₁} a e₂) v σ γ = updateSliced t (⟦ e₁ ⟧ᵉ σ γ) (⟦ e₂ ⟧ᵉ σ γ) v (λ v → update a v σ γ) update (cast {t = t} eq e) v σ γ = update e (casted t (≡.sym eq) v) σ γ update (tup {es = []} x) v σ γ = σ , γ -- cgit v1.2.3