redex-lang-test.rkt

#lang s-exp "redex-lang.rkt"

(axiom x : Nat)
(axiom y : Nat)

(lambda ((x : Nat)) y)

((lambda ((x : Nat)) y) 0)

; type error
(axiom y : (-> Nat Nat))
((lambda ((x : Nat)) 0) y)

redex-lang.rkt

#lang racket

(require
 "redex-model.rkt"
 redex/reduction-semantics)

(define (interp x)
  (define (interp-te env te)
    (match te
      [`(axiom ,x : ,A)
       (values (append env `((,x : ,A))) (void))]
      [_
       (unless (judgment-holds (types ,env ,te A))
         (error "Ill-typed term" te))
       (values env (car (judgment-holds (eval ,te e) e)))]))
  (match x
    [`(module-begin ,tes ...)
     (define-values (_ vs)
       (for/fold ([env '()]
                   [vs '()])
                  ([e tes])
         (let-values ([(env new-v) (interp-te env e)])
           (values env (cons new-v vs)))))
     (for-each displayln (reverse (filter (compose not void?) vs)))]))

(provide
 (rename-out [module-begin #%module-begin])
 #%top-interaction)

(define-syntax (module-begin stx)
  (syntax-case stx ()
    [(_ e ...)
     #`(#%module-begin
        (interp `(module-begin #,@(syntax->datum #'(e ...)))))]))

redex-model.rkt

#lang racket

(require
 redex/reduction-semantics)

(provide (all-defined-out))

(define-language stlcL
  [x :: variable-not-otherwise-mentioned]
  [e ::= x (lambda ((x : A) ...) e) (e e ...) natural]
  [A B ::= Nat (-> A ... B)]

  [v ::= x natural (lambda ((x : A) ...) e)]
  [E ::= hole (v ... E e ...)]
  [Γ ::= ((x : A) ...)]

  #:binding-forms
  (lambda ((x : A) #:...bind (clauses x (shadow clauses x))) e #:refers-to clauses))

(define-metafunction stlcL
  subst-all : e (x ...) (e ...) -> e
  [(subst-all e () ())
   e]
  [(subst-all e (x_1 x_r ...) (e_1 e_r ...))
   (subst-all (substitute e x_1 e_1) (x_r ...) (e_r ...))])

(define-judgment-form stlcL
  #:contract (step e e)
  #:mode (step I O)

  [(step ((lambda ((x : A) ..._1) e) e_a ..._1)
         (subst-all e (x ...) (e_a ...)))])

(define-judgment-form stlcL
  #:contract (reduce e e)
  #:mode (reduce I O)

  [(reduce e e)]

  [(step e e_1)
   (reduce e_1 e_2)
   ---------
   (reduce (in-hole E e) (in-hole E e_2))])

(define-judgment-form stlcL
  #:contract (eval e v)
  #:mode (eval I O)

  [(reduce e v)
   -----------
   (eval e v)])

(define-judgment-form stlcL
  #:contract (types Γ e A)
  #:mode (types I I O)

  [(types (any ... (x : A) (x_!_1 : B) ...) (name x x_!_1) A)]

  [(types Γ natural Nat)]

  [(types (any ... (x : A) ...) e B)
   --------------------------------------------------------
   (types (any ...) (lambda ((x : A) ...) e) (-> A ... B))]

  [(types Γ e (-> A ..._1 B))
   (types Γ e_r A) ...
   -------------------------
   (types Γ (e e_r ..._1) B)])