From 83f29fdd79665858717790d3213a8dbbd6b693e3 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Wed, 19 Jan 2022 16:56:24 +0000 Subject: Rename pseudocode file. This is anticipating the addition of pseudocode as a data type. That should make the denotational semantics much more performant, and allows the addition of new forms of semantics without duplicating effort. --- src/Helium/Data/Pseudocode/Types.agda | 412 ++++++++++++++++++++++++++++++++++ 1 file changed, 412 insertions(+) create mode 100644 src/Helium/Data/Pseudocode/Types.agda (limited to 'src/Helium/Data/Pseudocode') diff --git a/src/Helium/Data/Pseudocode/Types.agda b/src/Helium/Data/Pseudocode/Types.agda new file mode 100644 index 0000000..a545ddc --- /dev/null +++ b/src/Helium/Data/Pseudocode/Types.agda @@ -0,0 +1,412 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Definition of types and operations used by the Armv8-M pseudocode. +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +module Helium.Data.Pseudocode.Types where + +open import Algebra.Core +import Algebra.Definitions.RawSemiring as RS +open import Data.Bool.Base using (Bool; if_then_else_) +open import Data.Empty using (⊥-elim) +open import Data.Fin.Base as Fin hiding (cast) +import Data.Fin.Properties as Fₚ +import Data.Fin.Induction as Induction +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′) +open import Data.Vec.Functional +open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise) +import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pwₚ +open import Function using (_$_; _∘′_; id) +open import Helium.Algebra.Ordered.StrictTotal.Bundles +open import Helium.Algebra.Decidable.Bundles + using (BooleanAlgebra; RawBooleanAlgebra) +import Helium.Algebra.Decidable.Construct.Pointwise as Pw +open import Helium.Algebra.Morphism.Structures +open import Level using (_⊔_) renaming (suc to ℓsuc) +open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Definitions +open import Relation.Binary.PropositionalEquality as P using (_≡_) +import Relation.Binary.Reasoning.StrictPartialOrder as Reasoning +open import Relation.Binary.Structures using (IsStrictTotalOrder) +open import Relation.Nullary using (does; yes; no) +open import Relation.Nullary.Decidable.Core + using (False; toWitnessFalse; fromWitnessFalse) + +record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ ⊔ b₂ ⊔ i₁ ⊔ i₂ ⊔ i₃ ⊔ r₁ ⊔ r₂ ⊔ r₃)) where + field + bitRawBooleanAlgebra : RawBooleanAlgebra b₁ b₂ + integerRawRing : RawRing i₁ i₂ i₃ + realRawField : RawField r₁ r₂ r₃ + + bitsRawBooleanAlgebra : ℕ → RawBooleanAlgebra b₁ b₂ + bitsRawBooleanAlgebra = Pw.rawBooleanAlgebra bitRawBooleanAlgebra + + module 𝔹 = RawBooleanAlgebra bitRawBooleanAlgebra + renaming (Carrier to Bit; ⊤ to 1𝔹; ⊥ to 0𝔹) + module Bits {n} = RawBooleanAlgebra (bitsRawBooleanAlgebra n) + renaming (⊤ to ones; ⊥ to zeros) + module ℤ = RawRing integerRawRing renaming (Carrier to ℤ; 1# to 1ℤ; 0# to 0ℤ) + module ℝ = RawField realRawField renaming (Carrier to ℝ; 1# to 1ℝ; 0# to 0ℝ) + module ℤ′ = RS ℤ.Unordered.rawSemiring + module ℝ′ = RS ℝ.Unordered.rawSemiring + + Bits : ℕ → Set b₁ + Bits n = Bits.Carrier {n} + + open 𝔹 public using (Bit; 1𝔹; 0𝔹) + open Bits public using (ones; zeros) + open ℤ public using (ℤ; 1ℤ; 0ℤ) + open ℝ public using (ℝ; 1ℝ; 0ℝ) + + infix 4 _≟ᶻ_ _<ᶻ?_ _≟ʳ_ _<ʳ?_ _≟ᵇ₁_ _≟ᵇ_ + field + _≟ᶻ_ : Decidable ℤ._≈_ + _<ᶻ?_ : Decidable ℤ._<_ + _≟ʳ_ : Decidable ℝ._≈_ + _<ʳ?_ : Decidable ℝ._<_ + _≟ᵇ₁_ : Decidable 𝔹._≈_ + + _≟ᵇ_ : ∀ {n} → Decidable (Bits._≈_ {n}) + _≟ᵇ_ = Pwₚ.decidable _≟ᵇ₁_ + + field + _/1 : ℤ → ℝ + ⌊_⌋ : ℝ → ℤ + + cast : ∀ {m n} → .(eq : m ≡ n) → Bits m → Bits n + cast eq x i = x $ Fin.cast (P.sym eq) i + + 2ℤ : ℤ + 2ℤ = 2 ℤ′.×′ 1ℤ + + getᵇ : ∀ {n} → Fin n → Bits n → Bit + getᵇ i x = x (opposite i) + + setᵇ : ∀ {n} → Fin n → Bit → Op₁ (Bits n) + setᵇ i b = updateAt (opposite i) λ _ → b + + sliceᵇ : ∀ {n} (i : Fin (suc n)) j → Bits n → Bits (toℕ (i - j)) + sliceᵇ zero zero x = [] + sliceᵇ {suc n} (suc i) zero x = getᵇ i x ∷ sliceᵇ i zero (tail x) + sliceᵇ {suc n} (suc i) (suc j) x = sliceᵇ i j (tail x) + + updateᵇ : ∀ {n} (i : Fin (suc n)) j → Bits (toℕ (i - j)) → Op₁ (Bits n) + updateᵇ {n} = Induction.<-weakInduction P (λ _ _ → id) helper + where + P : Fin (suc n) → Set b₁ + P i = ∀ j → Bits (toℕ (i - j)) → Op₁ (Bits n) + + eq : ∀ {n} {i : Fin n} → toℕ i ≡ toℕ (inject₁ i) + eq = P.sym $ Fₚ.toℕ-inject₁ _ + + eq′ : ∀ {n} {i : Fin n} j → toℕ (i - j) ≡ toℕ (inject₁ i - Fin.cast eq j) + eq′ zero = eq + eq′ {i = suc _} (suc j) = eq′ j + + helper : ∀ i → P (inject₁ i) → P (suc i) + helper i rec zero y = rec zero (cast eq (tail y)) ∘′ setᵇ i (y zero) + helper i rec (suc j) y = rec (Fin.cast eq j) (cast (eq′ j) y) + + hasBit : ∀ {n} → Fin n → Bits n → Bool + hasBit i x = does (getᵇ i x ≟ᵇ₁ 1𝔹) + + infixl 7 _div_ _mod_ + + _div_ : ∀ (x y : ℤ) → {y≉0 : False (y /1 ≟ʳ 0ℝ)} → ℤ + (x div y) {y≉0} = ⌊ x /1 ℝ.* toWitnessFalse y≉0 ℝ.⁻¹ ⌋ + + _mod_ : ∀ (x y : ℤ) → {y≉0 : False (y /1 ≟ʳ 0ℝ)} → ℤ + (x mod y) {y≉0} = x ℤ.+ ℤ.- y ℤ.* (x div y) {y≉0} + + infixl 5 _<<_ + _<<_ : ℤ → ℕ → ℤ + x << n = 2ℤ ℤ′.^′ n ℤ.* x + + module ShiftNotZero + (1<>_ + _>>_ : ℤ → ℕ → ℤ + 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 + bitBooleanAlgebra : BooleanAlgebra b₁ b₂ + integerRing : CommutativeRing i₁ i₂ i₃ + realField : Field r₁ r₂ r₃ + + bitsBooleanAlgebra : ℕ → BooleanAlgebra b₁ b₂ + bitsBooleanAlgebra = Pw.booleanAlgebra bitBooleanAlgebra + + module 𝔹 = BooleanAlgebra bitBooleanAlgebra + renaming (Carrier to Bit; ⊤ to 1𝔹; ⊥ to 0𝔹) + module Bits {n} = BooleanAlgebra (bitsBooleanAlgebra n) + renaming (⊤ to ones; ⊥ to zeros) + module ℤ = CommutativeRing integerRing + renaming (Carrier to ℤ; 1# to 1ℤ; 0# to 0ℤ) + module ℝ = Field realField + renaming (Carrier to ℝ; 1# to 1ℝ; 0# to 0ℝ) + + Bits : ℕ → Set b₁ + Bits n = Bits.Carrier {n} + + open 𝔹 public using (Bit; 1𝔹; 0𝔹) + open Bits public using (ones; zeros) + open ℤ public using (ℤ; 1ℤ; 0ℤ) + open ℝ public using (ℝ; 1ℝ; 0ℝ) + + module ℤ-Reasoning = Reasoning ℤ.strictPartialOrder + module ℝ-Reasoning = Reasoning ℝ.strictPartialOrder + + field + integerDiscrete : ∀ x y → y ℤ.≤ x ⊎ x ℤ.+ 1ℤ ℤ.≤ y + 1≉0 : 1ℤ ℤ.≉ 0ℤ + + _/1 : ℤ → ℝ + ⌊_⌋ : ℝ → ℤ + /1-isHomo : IsRingHomomorphism ℤ.Unordered.rawRing ℝ.Unordered.rawRing _/1 + ⌊⌋-isHomo : IsRingHomomorphism ℝ.Unordered.rawRing ℤ.Unordered.rawRing ⌊_⌋ + /1-mono : ∀ x y → x ℤ.< y → x /1 ℝ.< y /1 + ⌊⌋-floor : ∀ x y → x ℤ.≤ ⌊ y ⌋ → ⌊ y ⌋ ℤ.< x ℤ.+ 1ℤ + ⌊⌋∘/1≗id : ∀ x → ⌊ x /1 ⌋ ℤ.≈ x + + module /1 = IsRingHomomorphism /1-isHomo renaming (⟦⟧-cong to cong) + module ⌊⌋ = IsRingHomomorphism ⌊⌋-isHomo renaming (⟦⟧-cong to cong) + + bitRawBooleanAlgebra : RawBooleanAlgebra b₁ b₂ + bitRawBooleanAlgebra = record + { _≈_ = _≈_ + ; _∨_ = _∨_ + ; _∧_ = _∧_ + ; ¬_ = ¬_ + ; ⊤ = ⊤ + ; ⊥ = ⊥ + } + where open BooleanAlgebra bitBooleanAlgebra + + rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ + rawPseudocode = record + { bitRawBooleanAlgebra = bitRawBooleanAlgebra + ; integerRawRing = ℤ.rawRing + ; realRawField = ℝ.rawField + ; _≟ᶻ_ = ℤ._≟_ + ; _<ᶻ?_ = ℤ._-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<