racket redex big-step define-language λ

bigstep.rkt

#lang racket
(require redex)
(provide λ λV ev)

(define-language λ
  (e ::= (e e) x (λ (x τ) e) (if0 e e e) (e + e) n)
  (n ::= number)
  (τ ::= (τ -> τ) num)
  (x ::= variable-not-otherwise-mentioned))

(define-extended-language λV λ
  (V ::= n (clo Δ x e))
  (Δ ::= · (x V Δ)))

(define-judgment-form λV
  #:mode (ev I I I O)
  #:contract (ev Δ ⊢ e V)
  [------------ "E-Value"
   (ev Δ ⊢ V V)]

  [(ev Δ ⊢ e_1 n_1)
   (ev Δ ⊢ e_2 n_2)
   (where n_3 (Σ n_1 n_2))
   ------------------------ "E-Plus"
   (ev Δ ⊢ (e_1 + e_2) n_3)]

  [(ev Δ ⊢ e_1 0) (ev Δ ⊢ e_2 V)
   ----------------------------- "E-If0"
   (ev Δ ⊢ (if0 e_1 e_2 e_3) V)]

  [(ev Δ ⊢ e_1 V_1)
   (where #t ,(not (= (term V_1) 0)))
   (ev Δ ⊢ e_3 V_3)
   ---------------------------------- "E-If0-Else"
   (ev Δ ⊢ (if0 e_1 e_2 e_3) V_3)]

  [(where V (lookup Δ x))
   ---------------------- "E-Var"
   (ev Δ ⊢ x V)]

  [(ev Δ ⊢ e_1 (clo Δ_1 x e_3))
   (ev Δ ⊢ e_2 V_2)
   (ev (x V_2 Δ_1) ⊢ e_3 V_3)
   ---------------------------- "E-App"
   (ev Δ ⊢ (e_1 e_2) V_3)]

  [-------------------------------- "E-Lambda"
   (ev Δ ⊢ (λ (x τ) e) (clo Δ x e))])

(define-metafunction λ
  Σ : n n -> n
  [(Σ n_1 n_2)
   ,(+ (term n_1) (term n_2))])

(define-metafunction λV
  lookup : Δ x -> V or #f
  [(lookup (x V Δ) x) V]
  [(lookup (x_1 V Δ) x_2) (lookup Δ x_2)]
  [(lookup · x) #f])

(define (evl e)
  (match (judgment-holds (ev · ⊢ ,e V) V)
    [(list) #f]
    [(list V) V]
    [_ (error 'evaluetion
              "multiple eval derivations for term ~a"
              e)]))

(test-equal (evl (term ((λ (x num) x) 1))) 1)
(test-equal (evl (term (((λ (x num) (λ (y num) x)) 1) 2))) 1)
(test-equal (evl (term (((λ (x num) (λ (y num) y)) 1) 2))) 2)
(test-equal (evl (term (((λ (x num) (λ (x num) x)) 1) 2))) 2)
(test-equal (evl (term (((λ (x num) (λ (y num) x)) 1) 2))) 1)
(test-equal (evl (term ((λ (x num) (x + x)) 2))) 4)
(test-equal (evl (term ((λ (x num) (if0 x x (x + 1))) 2))) 3)
(test-equal (evl (term ((λ (x num) (if0 x x (x + 1))) 0))) 0)
(test-equal (evl (term (((λ (x num) (λ (y num) (λ (z num) x))) 1) 2)))
            (term (clo (y 2 (x 1 ·)) z x)))
(test-equal (evl (term ((1 + 2) + (3 + 4))))
            (term 10))

(test-results)