Define the semantics of pseudocode data types.

1 files changed, 0 insertions, 68 deletions

diff --git a/src/Helium/Algebra/Construct/Pointwise.agda b/src/Helium/Algebra/Construct/Pointwise.agda
deleted file mode 100644
index d3aa560..0000000
--- a/src/Helium/Algebra/Construct/Pointwise.agda
+++ /dev/null
@@ -1,68 +0,0 @@
-------------------------------------------------------------------------
--- Agda Helium
---
--- Construct algebras of vectors in a pointwise manner
-------------------------------------------------------------------------
-
-{-# OPTIONS --safe --without-K #-}
-
-module Helium.Algebra.Construct.Pointwise where
-
-open import Algebra
-open import Relation.Binary.Core using (Rel)
-open import Data.Nat using (ℕ)
-open import Data.Product using (_,_)
-open import Data.Vec.Functional using (replicate; map; zipWith)
-open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise)
-import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pwₚ
-open import Function using (_$_)
-open import Relation.Binary.Bundles using (Setoid)
-
-module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} where
-  private
-    _≋_ = Pointwise _≈_
-
-  module _ {∨ ∧ : Op₂ A} where
-    isLattice : IsLattice _≈_ ∨ ∧ → ∀ n → IsLattice (_≋_ {n}) (zipWith ∨) (zipWith ∧)
-    isLattice L n = record
-      { isEquivalence = Pwₚ.isEquivalence isEquivalence n
-      ; ∨-comm        = λ x y i → ∨-comm (x i) (y i)
-      ; ∨-assoc       = λ x y z i → ∨-assoc (x i) (y i) (z i)
-      ; ∨-cong        = λ x≈y u≈v i → ∨-cong (x≈y i) (u≈v i)
-      ; ∧-comm        = λ x y i → ∧-comm (x i) (y i)
-      ; ∧-assoc       = λ x y z i → ∧-assoc (x i) (y i) (z i)
-      ; ∧-cong        = λ x≈y u≈v i → ∧-cong (x≈y i) (u≈v i)
-      ; absorptive    = (λ x y i → ∨-absorbs-∧ (x i) (y i))
-                      , (λ x y i → ∧-absorbs-∨ (x i) (y i))
-      }
-      where open IsLattice L
-
-    isDistributiveLattice : IsDistributiveLattice _≈_ ∨ ∧ → ∀ n → IsDistributiveLattice (_≋_ {n}) (zipWith ∨) (zipWith ∧)
-    isDistributiveLattice L n = record
-      { isLattice = isLattice L.isLattice n
-      ; ∨-distribʳ-∧ = λ x y z i → L.∨-distribʳ-∧ (x i) (y i) (z i)
-      }
-      where module L = IsDistributiveLattice L
-
-  module _ {∨ ∧ : Op₂ A} {¬ : Op₁ A} {⊤ ⊥ : A} where
-    isBooleanAlgebra : IsBooleanAlgebra _≈_ ∨ ∧ ¬ ⊤ ⊥ → ∀ n → IsBooleanAlgebra (_≋_ {n}) (zipWith ∨) (zipWith ∧) (map ¬) (replicate ⊤) (replicate ⊥)
-    isBooleanAlgebra B n = record
-      { isDistributiveLattice = isDistributiveLattice B.isDistributiveLattice n
-      ; ∨-complementʳ = λ x i → B.∨-complementʳ (x i)
-      ; ∧-complementʳ = λ x i → B.∧-complementʳ (x i)
-      ; ¬-cong = λ x≈y i → B.¬-cong (x≈y i)
-      }
-      where module B = IsBooleanAlgebra B
-
-lattice : ∀ {a ℓ} → Lattice a ℓ → ℕ → Lattice a ℓ
-lattice L n = record { isLattice = isLattice (Lattice.isLattice L) n }
-
-distributiveLattice : ∀ {a ℓ} → DistributiveLattice a ℓ → ℕ → DistributiveLattice a ℓ
-distributiveLattice L n = record
-  { isDistributiveLattice =
-    isDistributiveLattice (DistributiveLattice.isDistributiveLattice L) n
-  }
-
-booleanAlgebra : ∀ {a ℓ} → BooleanAlgebra a ℓ → ℕ → BooleanAlgebra a ℓ
-booleanAlgebra B n = record
-  { isBooleanAlgebra = isBooleanAlgebra (BooleanAlgebra.isBooleanAlgebra B) n }