blob: 749e1ca91d43c9dce0678294205999853728b235 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
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
|
