Semantics.agda

open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open import Relation.Nullary.Decidable

module STLC.Semantics {U} (UEq : IsDecEquivalence {A = U} _≡_) (El : U → Set) where

open import STLC.Typing U
open import STLC.Syntax Type as Raw
open import STLC.Scopecheck Type as Scope
open import STLC.Typecheck UEq as TC
open import STLC.Embed El
open import STLC.Embedded

open import Data.Vec
open import Data.Product

semantics : (E : Raw.Expr) →
            {scope-prf : True (Scope.check [] E)} → let E′ = proj₁ (toWitness scope-prf) in
            {type-prf : True (TC.infer [] E′)} → let τ = proj₁ (toWitness type-prf) in
            embed-type τ
semantics E {scope-prf} {type-prf} = eval₀ (embed (proj₂ (toWitness type-prf)))