------------------------------------------------------------------------
-- Big-step semantics for the untyped λ-calculus
------------------------------------------------------------------------

module Lambda.Substitution.OneSemantics where

open import Coinduction
open import Data.Fin
open import Function
open import Data.Nat

open import Lambda.Syntax
open WHNF
open import Lambda.Substitution

-- Semantic domain. ⊥ represents non-termination.

data Sem (n : ) : Set where
: Sem n
val : (v : Value n)  Sem n

-- Big-step semantics.

mutual

infix 4 _⇒_ _⇒?_

data _⇒_ {n} : Tm n  Sem n  Set where
val :  {v}   v   val v
app :  {t₁ t₂ t v s}
(t₁⇓   : t₁ ⇒? val (ƛ t))
(t₂⇓   : t₂ ⇒? val v)
(t₁t₂⇒ : t / sub  v  ⇒? s)
t₁ · t₂  s
·ˡ  :  {t₁ t₂}
(t₁⇑ : t₁ ⇒? )
t₁ · t₂
·ʳ  :  {t₁ t₂ v}
(t₁⇓ : t₁ ⇒? val v)
(t₂⇑ : t₂ ⇒? )
t₁ · t₂

-- Conditional coinduction: coinduction only for diverging
-- computations.

_⇒?_ :  {n}  Tm n  Sem n  Set
t ⇒?      =  (t  )
t ⇒? val v = t  val v

-- Example.

Ω-loops : Ω
Ω-loops = app val val ( Ω-loops)