open import Relation.Unary
open import Relation.Nullary.Decidable using (yes ; no )
open import Relation.Binary.Definitions using (DecidableEquality)

module lambda (𝓥 : Set) (_≈_ : DecidableEquality 𝓥) where

  infixl 5 _∙_
  infix 6 `_
  infix 4 ƛ_↦_
  data Λ : Set where
    `_ : 𝓥 → Λ
    _∙_ : Λ → Λ → Λ
    ƛ_↦_ : 𝓥 → Λ → Λ

  data value : Λ → Set where
    ƛ-value : ∀ {v t} →
      value (ƛ v ↦ t)

  value-dec : Decidable value
  value-dec (` x) = no (λ ())
  value-dec (s ∙ t) = no (λ ())
  value-dec (ƛ v ↦ t) = yes ƛ-value

  infix 9 _[_/_]
  _[_/_] : Λ → Λ → 𝓥 → Λ
  (` x) [ t / v ] with v ≈ x
  ... | yes _ = t
  ... | no _ = ` x
  (n ∙ m) [ t / v ] = (n [ t / v ]) ∙ (m [ t / v ])
  (ƛ x ↦ n) [ t / v ] with v ≈ x
  ... | yes _ = ƛ x ↦ n
  ... | no _ = ƛ x ↦ (n [ t / v ])

  infix 4 _⟶β_
  data _⟶β_ : Λ → Λ → Set where
    appₗ : ∀ {s s' t : Λ} →
      s ⟶β s' →
      s ∙ t ⟶β s' ∙ t

    appᵣ : ∀ {s t t' : Λ} →
      t ⟶β t' →
      s ∙ t ⟶β s ∙ t'

    β : ∀ {s t : Λ} {v : 𝓥}  →
      value t →
      (ƛ v ↦ s) ∙ t ⟶β s [ t / v ]

  module mstep where
    infix 4 _↠β_
    -- reflexive transitive closure of _⟶_
    infix  3 _∎
    infixr 2 _⟶β⟨_⟩_
    data _↠β_ : Λ → Λ → Set where
      _∎ : ∀ (F : Λ) →
        F ↠β F
      cons : ∀ {F G H : Λ} →
        F ⟶β G →
        G ↠β H →
        F ↠β H

    pattern _⟶β⟨_⟩_ F F⟶G G↠H = cons {F} F⟶G G↠H
    
    infix 1 βegin_
    βegin_ : ∀ {F G : Λ} →
      F ↠β G →
      F ↠β G
    βegin step = step

    mappₗ : ∀ {F G H : Λ} →
      F ↠β H →
      (F ∙ G) ↠β (H ∙ G)
    mappₗ {F} {G} (_ ∎) = F ∙ G ∎
    mappₗ (cons F⟶H' G↠H) = cons (appₗ F⟶H') (mappₗ G↠H)

    mappᵣ : ∀ {F G H : Λ} →
      G ↠β H →
      (F ∙ G) ↠β (F ∙ H)
    mappᵣ {F} {_} {H} (_ ∎) = F ∙ H ∎
    mappᵣ {F} (cons G⟶H' H'↠H) = cons (appᵣ G⟶H') (mappᵣ H'↠H)

    β-once : ∀ {F G : Λ} →
      F ⟶β G →
      F ↠β G
    β-once {G = G} step = cons step (G ∎)


    infixr 2 _↠β⟨_⟩_
    _↠β⟨_⟩_ : ∀ (F : Λ) {G H : Λ} →
      F ↠β G →
      G ↠β H →
      F ↠β H
    _↠β⟨_⟩_ F (_ ∎) step' = step'
    _↠β⟨_⟩_ F (cons {G = G} x step) step' = cons x (_↠β⟨_⟩_ G step step')

  open mstep public