25 lines
711 B
Agda
25 lines
711 B
Agda
module Language.Values where
|
||
|
||
open import Data.Integer using (ℤ)
|
||
open import Data.Bool using (Bool)
|
||
open import Data.List using (List; []; _∷_)
|
||
|
||
data Value : Set where
|
||
int : ℤ → Value
|
||
bool : Bool → Value
|
||
|
||
data ValueType : Set where
|
||
tint tbool : ValueType
|
||
|
||
variable
|
||
s s' s'' : List Value
|
||
st st' st'' : List ValueType
|
||
b b₁ b₂ : Bool
|
||
z z₁ z₂ : ℤ
|
||
|
||
-- what it means for list of value types to describe a list of values
|
||
data ⟦_⟧ˢ : List ValueType → List Value → Set where
|
||
⟦⟧ˢ-empty : ⟦ [] ⟧ˢ []
|
||
⟦⟧ˢ-int : ⟦ st ⟧ˢ s → ⟦ tint ∷ st ⟧ˢ (int z ∷ s)
|
||
⟦⟧ˢ-bool : ⟦ st ⟧ˢ s → ⟦ tbool ∷ st ⟧ˢ (bool b ∷ s)
|