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)