From 535e4297a08c626d0e2e1923914727f914b8c9bd Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sat, 19 Mar 2022 13:28:42 +0000 Subject: Modify pseudocode definition. This change makes the following changes to the definition of pseudocode: - Add a separate type `bit` for single-bit values. - Change `var` and `state` to take `Fin`s instead of bounded naturals. - Make `[_]` and `unbox` work for any sliced type. - Generalise `_:_` and `slice` into `splice` and `cut` respectively, making the two new operations inverses. - Replace `tup` with `nil` and `cons` for building tuples. - Add destructors `head` and `tail` for tuple types. - Make function and procedure calls take a vector of arguments instead of a tuple. - Introduce an `if_then_` expression for if statements with a trivial else branch. --- src/Helium/Semantics/Denotational/Core.agda | 156 +++++++++++++++++----------- 1 file changed, 95 insertions(+), 61 deletions(-) (limited to 'src/Helium/Semantics/Denotational') diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda index b425252..0bd1794 100644 --- a/src/Helium/Semantics/Denotational/Core.agda +++ b/src/Helium/Semantics/Denotational/Core.agda @@ -17,7 +17,7 @@ private open module C = RawPseudocode rawPseudocode open import Data.Bool as Bool using (Bool; true; false) -open import Data.Fin as Fin using (Fin; zero; suc; #_) +open import Data.Fin as Fin using (Fin; zero; suc) import Data.Fin.Properties as Finₚ open import Data.Nat as ℕ using (ℕ; zero; suc) import Data.Nat.Properties as ℕₚ @@ -31,7 +31,7 @@ open import Function using (case_of_; _∘′_; id) open import Helium.Data.Pseudocode.Core import Induction as I import Induction.WellFounded as Wf -open import Level hiding (zero; suc) +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) @@ -41,6 +41,7 @@ open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromW ⟦ int ⟧ₗ = i₁ ⟦ fin n ⟧ₗ = 0ℓ ⟦ real ⟧ₗ = r₁ +⟦ bit ⟧ₗ = b₁ ⟦ bits n ⟧ₗ = b₁ ⟦ tuple n ts ⟧ₗ = helper ts where @@ -56,6 +57,7 @@ open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromW ⟦ int ⟧ₜ = ℤ ⟦ fin n ⟧ₜ = Fin n ⟦ real ⟧ₜ = ℝ +⟦ bit ⟧ₜ = Bit ⟦ bits n ⟧ₜ = Bits n ⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′ ⟦ array t n ⟧ₜ = Vec ⟦ t ⟧ₜ n @@ -66,13 +68,13 @@ open import Relation.Nullary.Decidable.Core using (True; False; toWitness; fromW -- 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 @@ -96,10 +98,11 @@ tupTail [] x = _ tupTail (_ ∷ _) (x , xs) = xs equal : ∀ {t} → HasEquality t → ⟦ t ⟧ₜ → ⟦ t ⟧ₜ → Bool -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 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 @@ -108,8 +111,8 @@ comp real x y = does (x <ʳ? y) -- 0 of y is 0 of result join : ∀ t {m n} → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ -join bits {m} x y = y VecF.++ x -join (array _) {m} x y = y Vec.++ x +join bits x y = y VecF.++ x +join (array _) x y = y Vec.++ x -- take from 0 take : ∀ t i {j} → ⟦ asType t (i ℕ.+ j) ⟧ₜ → ⟦ asType t i ⟧ₜ @@ -131,38 +134,59 @@ module _ where m≤n⇒m+k≡n ℕ.z≤n = _ , ≡.refl m≤n⇒m+k≡n (ℕ.s≤s m≤n) = P.dmap id (≡.cong suc) (m≤n⇒m+k≡n m≤n) - slicedSize : ∀ i j (off : Fin (suc i)) → P.∃ λ k → i ℕ.+ j ≡ Fin.toℕ off ℕ.+ (j ℕ.+ k) - slicedSize i j off = k , (begin - i ℕ.+ j ≡˘⟨ ≡.cong (ℕ._+ j) (P.proj₂ off+k≤i) ⟩ - (Fin.toℕ off ℕ.+ k) ℕ.+ j ≡⟨ ℕₚ.+-assoc (Fin.toℕ off) k j ⟩ - Fin.toℕ off ℕ.+ (k ℕ.+ j) ≡⟨ ≡.cong (Fin.toℕ off ℕ.+_) (ℕₚ.+-comm k j) ⟩ - Fin.toℕ off ℕ.+ (j ℕ.+ k) ∎) + slicedSize : ∀ n m (i : Fin (suc n)) → P.∃ λ k → n ℕ.+ m ≡ Fin.toℕ i ℕ.+ (m ℕ.+ k) × Fin.toℕ i ℕ.+ k ≡ n + slicedSize n m i = k , (begin + n ℕ.+ m ≡˘⟨ ≡.cong (ℕ._+ m) (P.proj₂ i+k≡n) ⟩ + (Fin.toℕ i ℕ.+ k) ℕ.+ m ≡⟨ ℕₚ.+-assoc (Fin.toℕ i) k m ⟩ + Fin.toℕ i ℕ.+ (k ℕ.+ m) ≡⟨ ≡.cong (Fin.toℕ i ℕ.+_) (ℕₚ.+-comm k m) ⟩ + Fin.toℕ i ℕ.+ (m ℕ.+ k) ∎) , + P.proj₂ i+k≡n where open ≡-Reasoning - off+k≤i = m≤n⇒m+k≡n (ℕₚ.≤-pred (Finₚ.toℕ