Do a big refactor.

- Replace the decidable predicates on expressions and statements with
  separate data types.

- Reorganise the Hoare logic semantics to remove unnecessary
  definitions.

- Make liberal use of modules to group related definitions together.

- Unify the types for denotational and Hoare logic semantics.

- Make bits an abstraction of array types.

1 files changed, 209 insertions, 0 deletions

diff --git a/src/Helium/Semantics/Core.agda b/src/Helium/Semantics/Core.agda
new file mode 100644
index 0000000..688f6f6
--- /dev/null
+++ b/src/Helium/Semantics/Core.agda
@@ -0,0 +1,209 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Base definitions for semantics
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Data.Pseudocode.Algebra 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 Algebra.Core using (Op₁)
+open import Data.Bool as Bool using (Bool)
+open import Data.Fin as Fin using (Fin; zero; suc)
+open import Data.Fin.Patterns
+import Data.Fin.Properties as Finₚ
+open import Data.Integer as 𝕀 using () renaming (ℤ to 𝕀)
+open import Data.Nat as ℕ using (ℕ; suc)
+import Data.Nat.Properties as ℕₚ
+open import Data.Product as × using (_×_; _,_)
+open import Data.Sign using (Sign)
+open import Data.Unit using (⊤)
+open import Data.Vec as Vec using (Vec; []; _∷_; _++_; lookup; map; take; drop)
+open import Data.Vec.Relation.Binary.Pointwise.Extensional using (Pointwise; decidable)
+open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
+open import Function
+open import Helium.Data.Pseudocode.Core
+open import Level hiding (suc)
+open import Relation.Binary
+import Relation.Binary.Construct.On as On
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Decidable.Core using (map′)
+
+private
+  variable
+    a : Level
+    A : Set a
+    t t′ t₁ t₂ : Type
+    m n        : ℕ
+    Γ Δ Σ ts   : Vec Type m
+
+  ℓ = b₁ ⊔ i₁ ⊔ r₁
+  ℓ₁ = ℓ ⊔ b₂ ⊔ i₂ ⊔ r₂
+  ℓ₂ = i₁ ⊔ i₃ ⊔ r₁ ⊔ r₃
+
+  Sign⇒- : Sign → Op₁ A → Op₁ A
+  Sign⇒- Sign.+ f = id
+  Sign⇒- Sign.- f = f
+
+open ℕₚ.≤-Reasoning
+
+𝕀⇒ℤ : 𝕀 → ℤ
+𝕀⇒ℤ z = Sign⇒- (𝕀.sign z) ℤ.-_ (𝕀.∣ z ∣ ℤ′.×′ 1ℤ)
+
+𝕀⇒ℝ : 𝕀 → ℝ
+𝕀⇒ℝ z = Sign⇒- (𝕀.sign z) ℝ.-_ (𝕀.∣ z ∣ ℝ′.×′ 1ℝ)
+
+castVec : .(eq : m ≡ n) → Vec A m → Vec A n
+castVec {m = .0}     {0}     eq []       = []
+castVec {m = .suc m} {suc n} eq (x ∷ xs) = x ∷ castVec (ℕₚ.suc-injective eq) xs
+
+⟦_⟧ₜ  : Type → Set ℓ
+⟦_⟧ₜ′ : Vec Type n → Set ℓ
+
+⟦ bool ⟧ₜ      = Lift ℓ Bool
+⟦ int ⟧ₜ       = Lift ℓ ℤ
+⟦ fin n ⟧ₜ     = Lift ℓ (Fin n)
+⟦ real ⟧ₜ      = Lift ℓ ℝ
+⟦ bit ⟧ₜ       = Lift ℓ Bit
+⟦ tuple ts ⟧ₜ  = ⟦ ts ⟧ₜ′
+⟦ array t n ⟧ₜ = Vec ⟦ t ⟧ₜ n
+
+⟦ [] ⟧ₜ′          = Lift ℓ ⊤
+⟦ t ∷ [] ⟧ₜ′      = ⟦ t ⟧ₜ
+⟦ t ∷ t₁ ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ t₁ ∷ ts ⟧ₜ′
+
+fetch : ∀ (i : Fin n) Γ → ⟦ Γ ⟧ₜ′ → ⟦ lookup Γ i ⟧ₜ
+fetch 0F      (t ∷ [])     x        = x
+fetch 0F      (t ∷ t₁ ∷ Γ) (x , xs) = x
+fetch (suc i) (t ∷ t₁ ∷ Γ) (x , xs) = fetch i (t₁ ∷ Γ) xs
+
+updateAt : ∀ (i : Fin n) Γ → ⟦ lookup Γ i ⟧ₜ → ⟦ Γ ⟧ₜ′ → ⟦ Γ ⟧ₜ′
+updateAt 0F      (t ∷ [])     v x        = v
+updateAt 0F      (t ∷ t₁ ∷ Γ) v (x , xs) = v , xs
+updateAt (suc i) (t ∷ t₁ ∷ Γ) v (x , xs) = x , updateAt i (t₁ ∷ Γ) v xs
+
+cons′ : ∀ (ts : Vec Type n) → ⟦ t ⟧ₜ → ⟦ tuple ts ⟧ₜ → ⟦ tuple (t ∷ ts) ⟧ₜ
+cons′ []      x xs = x
+cons′ (_ ∷ _) x xs = x , xs
+
+head′ : ∀ (ts : Vec Type n) → ⟦ tuple (t ∷ ts) ⟧ₜ → ⟦ t ⟧ₜ
+head′ []      x        = x
+head′ (_ ∷ _) (x , xs) = x
+
+tail′ : ∀ (ts : Vec Type n) → ⟦ tuple (t ∷ ts) ⟧ₜ → ⟦ tuple ts ⟧ₜ
+tail′ []      x        = _
+tail′ (_ ∷ _) (x , xs) = xs
+
+_≈_ : ⦃ HasEquality t ⦄ → Rel ⟦ t ⟧ₜ  ℓ₁
+_≈_ ⦃ bool ⦄  = Lift ℓ₁ ∘₂ _≡_ on lower
+_≈_ ⦃ int ⦄   = Lift ℓ₁ ∘₂ ℤ._≈_ on lower
+_≈_ ⦃ fin ⦄   = Lift ℓ₁ ∘₂ _≡_ on lower
+_≈_ ⦃ real ⦄  = Lift ℓ₁ ∘₂ ℝ._≈_ on lower
+_≈_ ⦃ bit ⦄   = Lift ℓ₁ ∘₂ 𝔹._≈_ on lower
+_≈_ ⦃ array ⦄ = Pointwise _≈_
+
+_<_ : ⦃ Ordered t ⦄ → Rel ⟦ t ⟧ₜ ℓ₂
+_<_ ⦃ int ⦄  = Lift ℓ₂ ∘₂ ℤ._<_ on lower
+_<_ ⦃ fin ⦄  = Lift ℓ₂ ∘₂ Fin._<_ on lower
+_<_ ⦃ real ⦄ = Lift ℓ₂ ∘₂ ℝ._<_ on lower
+
+≈-dec : ⦃ hasEq : HasEquality t ⦄ → Decidable (_≈_ ⦃ hasEq ⦄)
+≈-dec ⦃ bool ⦄  = map′ lift lower ∘₂ On.decidable lower _≡_ Bool._≟_
+≈-dec ⦃ int ⦄   = map′ lift lower ∘₂ On.decidable lower ℤ._≈_ _≟ᶻ_
+≈-dec ⦃ fin ⦄   = map′ lift lower ∘₂ On.decidable lower _≡_ Fin._≟_
+≈-dec ⦃ real ⦄  = map′ lift lower ∘₂ On.decidable lower ℝ._≈_ _≟ʳ_
+≈-dec ⦃ bit ⦄   = map′ lift lower ∘₂ On.decidable lower 𝔹._≈_ _≟ᵇ₁_
+≈-dec ⦃ array ⦄ = decidable ≈-dec
+
+<-dec : ⦃ ordered : Ordered t ⦄ → Decidable (_<_ ⦃ ordered ⦄)
+<-dec ⦃ int ⦄  = map′ lift lower ∘₂ On.decidable lower ℤ._<_ _<ᶻ?_
+<-dec ⦃ fin ⦄  = map′ lift lower ∘₂ On.decidable lower Fin._<_ Fin._<?_
+<-dec ⦃ real ⦄ = map′ lift lower ∘₂ On.decidable lower ℝ._<_ _<ʳ?_
+
+Κ[_]_ : ∀ t → literalType t → ⟦ t ⟧ₜ
+Κ[ bool ]                x        = lift x
+Κ[ int ]                 x        = lift (𝕀⇒ℤ x)
+Κ[ fin n ]               x        = lift x
+Κ[ real ]                x        = lift (𝕀⇒ℝ x)
+Κ[ bit ]                 x        = lift (Bool.if x then 1𝔹 else 0𝔹)
+Κ[ tuple [] ]            x        = _
+Κ[ tuple (t ∷ []) ]      x        = Κ[ t ] x
+Κ[ tuple (t ∷ t₁ ∷ ts) ] (x , xs) = Κ[ t ] x , Κ[ tuple (t₁ ∷ ts) ] xs
+Κ[ array t n ]           x        = map Κ[ t ]_ x
+
+2≉0 : Set _
+2≉0 = ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ
+
+neg : ⦃ IsNumeric t ⦄ → Op₁ ⟦ t ⟧ₜ
+neg ⦃ int ⦄  = lift ∘ ℤ.-_ ∘ lower
+neg ⦃ real ⦄ = lift ∘ ℝ.-_ ∘ lower
+
+add : ⦃ isNum₁ : IsNumeric t₁ ⦄ → ⦃ isNum₂ : IsNumeric t₂ ⦄ → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ isNum₁ +ᵗ isNum₂ ⟧ₜ
+add ⦃ int ⦄  ⦃ int ⦄  x y = lift (lower x ℤ.+ lower y)
+add ⦃ int ⦄  ⦃ real ⦄ x y = lift (lower x /1 ℝ.+ lower y)
+add ⦃ real ⦄ ⦃ int ⦄  x y = lift (lower x ℝ.+ lower y /1)
+add ⦃ real ⦄ ⦃ real ⦄ x y = lift (lower x ℝ.+ lower y)
+
+mul : ⦃ isNum₁ : IsNumeric t₁ ⦄ → ⦃ isNum₂ : IsNumeric t₂ ⦄ → ⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ isNum₁ +ᵗ isNum₂ ⟧ₜ
+mul ⦃ int ⦄  ⦃ int ⦄  x y = lift (lower x ℤ.* lower y)
+mul ⦃ int ⦄  ⦃ real ⦄ x y = lift (lower x /1 ℝ.* lower y)
+mul ⦃ real ⦄ ⦃ int ⦄  x y = lift (lower x ℝ.* lower y /1)
+mul ⦃ real ⦄ ⦃ real ⦄ x y = lift (lower x ℝ.* lower y)
+
+pow : ⦃ IsNumeric t ⦄ → ⟦ t ⟧ₜ → ℕ → ⟦ t ⟧ₜ
+pow ⦃ int ⦄  = lift ∘₂ ℤ′._^′_ ∘ lower
+pow ⦃ real ⦄ = lift ∘₂ ℝ′._^′_ ∘ lower
+
+shift : 2≉0 → ℤ → ℕ → ℤ
+shift 2≉0 z n = ⌊ z /1 ℝ.* 2≉0 ℝ.⁻¹ ℝ′.^′ n ⌋
+
+lowerFin : ∀ (ms : Vec ℕ n) → ⟦ tuple (map fin ms) ⟧ₜ → literalTypes (map fin ms)
+lowerFin []            _        = _
+lowerFin (_ ∷ [])      x        = lower x
+lowerFin (_ ∷ m₁ ∷ ms) (x , xs) = lower x , lowerFin (m₁ ∷ ms) xs
+
+mergeVec : Vec A m → Vec A n → Fin (suc n) → Vec A (n ℕ.+ m)
+mergeVec {m = m} {n} xs ys i = castVec eq (low ++ xs ++ high)
+  where
+  i′ = Fin.toℕ i
+  ys′ = castVec (sym (ℕₚ.m+[n∸m]≡n (ℕ.≤-pred (Finₚ.toℕ<n i)))) ys
+  low = take i′ ys′
+  high = drop i′ ys′
+  eq = begin-equality
+    i′ ℕ.+ (m ℕ.+ (n ℕ.∸ i′)) ≡⟨ ℕₚ.+-comm i′ _ ⟩
+    m ℕ.+ (n ℕ.∸ i′) ℕ.+ i′   ≡⟨ ℕₚ.+-assoc m _ _ ⟩
+    m ℕ.+ (n ℕ.∸ i′ ℕ.+ i′)   ≡⟨ cong (m ℕ.+_) (ℕₚ.m∸n+n≡m (ℕ.≤-pred (Finₚ.toℕ<n i))) ⟩
+    m ℕ.+ n                   ≡⟨ ℕₚ.+-comm m n ⟩
+    n ℕ.+ m                   ∎
+
+sliceVec : Vec A (n ℕ.+ m) → Fin (suc n) → Vec A m
+sliceVec {n = n} {m} xs i = take m (drop i′ (castVec eq xs))
+  where
+  i′ = Fin.toℕ i
+  eq = sym $ begin-equality
+    i′ ℕ.+ (m ℕ.+ (n ℕ.∸ i′)) ≡⟨ ℕₚ.+-comm i′ _ ⟩
+    m ℕ.+ (n ℕ.∸ i′) ℕ.+ i′   ≡⟨ ℕₚ.+-assoc m _ _ ⟩
+    m ℕ.+ (n ℕ.∸ i′ ℕ.+ i′)   ≡⟨ cong (m ℕ.+_) (ℕₚ.m∸n+n≡m (ℕ.≤-pred (Finₚ.toℕ<n i))) ⟩
+    m ℕ.+ n                   ≡⟨ ℕₚ.+-comm m n ⟩
+    n ℕ.+ m                   ∎
+
+cutVec : Vec A (n ℕ.+ m) → Fin (suc n) → Vec A n
+cutVec {n = n} {m} xs i = castVec (ℕₚ.m+[n∸m]≡n (ℕ.≤-pred (Finₚ.toℕ<n i))) (take i′ (castVec eq xs) ++ drop m (drop i′ (castVec eq xs)))
+  where
+  i′ = Fin.toℕ i
+  eq = sym $ begin-equality
+    i′ ℕ.+ (m ℕ.+ (n ℕ.∸ i′)) ≡⟨ ℕₚ.+-comm i′ _ ⟩
+    m ℕ.+ (n ℕ.∸ i′) ℕ.+ i′   ≡⟨ ℕₚ.+-assoc m _ _ ⟩
+    m ℕ.+ (n ℕ.∸ i′ ℕ.+ i′)   ≡⟨ cong (m ℕ.+_) (ℕₚ.m∸n+n≡m (ℕ.≤-pred (Finₚ.toℕ<n i))) ⟩
+    m ℕ.+ n                   ≡⟨ ℕₚ.+-comm m n ⟩
+    n ℕ.+ m                   ∎