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)
|