cek.clj

(ns machines.cek
  (:require
   [clojure.core.match :as match]
   [clojure.spec :as spec]))

;; e ∈ Exp ::= x | (e e) | (λ (x) e)
;; x ∈ Var
;; ς ∈ Σ = Exp × Env × Kont
;; v ∈ Val ::= (λ (x) e)
;; ρ ∈ Env = Var →_fin Val × Env
;; κ ∈ Kont ::= mt | (ar e ρ κ) | (fn v ρ κ)

;; ς ↦CEK ς'
(defn step [ς]
  (match/match [ς]
    ;; ⟨x, ρ, κ⟩ ↦ ⟨v, ρ', κ⟩ where (ρ x) = (v, ρ')
    [{:c (x :guard symbol?) :e ρ :k κ}]
    (match/match [(get ρ x)]
      [(['clo λ ρ'] :seq)]
      {:c λ
       :e ρ'
       :k κ})

    ;; ⟨(e₀ e₁), ρ, κ⟩ ↦ ⟨e₀, ρ, (ar e₁ ρ κ)⟩
    [{:c ([e₀ e₁] :seq) :e ρ :k κ}]
    {:c e₀
     :e ρ
     :k `(~'ar ~e₁ ~ρ ~κ)}

    ;; ⟨v, ρ, (ar e ρ' κ)⟩ ↦ ⟨e, ρ', (fn v ρ κ)⟩
    [{:c v :e ρ :k (['ar e ρ' κ] :seq)}]
    {:c e
     :e ρ'
     :k `(~'fn ~v ~ρ ~κ)}

    ;; ⟨v, ρ, (fn (λ (x) e), ρ', κ)⟩ ↦ ⟨e, ρ'[x ↦ (v, ρ)], κ)
    [{:c v :e ρ :k (['fn (['λ ([x] :seq) e] :seq) ρ' κ] :seq)}]
    {:c e
     :e (assoc ρ' x `(~'clo ~v ~ρ))
     :k κ}

    :else
    ς))

(defn step*
  ([ς]
   (step* ς [ς]))
  ([ς ς*]
   (let [ς' (step ς)]
     (if (= ς' ς)
       ς*
       (let [ς*' (conj ς* ς')]
         (recur ς' ς*'))))))

;; (inject e) = ⟨e, ∅, mt⟩
(defn inject [e]
  {:c e
   :e {}
   :k 'mt})

;; (eval e) = { ς | (inject e) ↠CEK ς }
(defn eval [e]
  (loop [ς (inject e)]
    (let [ς' (step ς)]
      (match/match [ς']
        [{:c (['λ _ _] :seq) :e ρ :k 'mt}]
        (get ς' :c)

        :else
        (recur ς')))))

(comment
  (let [e '((λ (x) ((λ (z) z) x))
            (λ (y) y))]
    
    (eval e)
    ;; =>
    '(λ (y) y))

  (let [ς (inject e)]
    (step* ς)
    ;; =>
    '[{:c ((λ (x) ((λ (z) z) x)) (λ (y) y)), :e {}, :k mt}
      {:c (λ (x) ((λ (z) z) x)), :e {}, :k (ar (λ (y) y) {} mt)}
      {:c (λ (y) y), :e {}, :k (fn (λ (x) ((λ (z) z) x)) {} mt)}
      {:c ((λ (z) z) x), :e {x (clo (λ (y) y) {})}, :k mt}
      {:c (λ (z) z), :e {x (clo (λ (y) y) {})}, :k (ar x {x (clo (λ (y) y) {})} mt)}
      {:c x, :e {x (clo (λ (y) y) {})}, :k (fn (λ (z) z) {x (clo (λ (y) y) {})} mt)}
      {:c (λ (y) y), :e {}, :k (fn (λ (z) z) {x (clo (λ (y) y) {})} mt)}
      {:c z, :e {x (clo (λ (y) y) {}), z (clo (λ (y) y) {})}, :k mt}
      {:c (λ (y) y), :e {}, :k mt}]))