1 files changed, 82 insertions, 0 deletions
diff --git a/src/Helium/Semantics/Core.agda b/src/Helium/Semantics/Core.agda
new file mode 100644
index 0000000..749e1ca
--- /dev/null
+++ b/src/Helium/Semantics/Core.agda
@@ -0,0 +1,82 @@
+------------------------------------------------------------------------
+-- 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