STLC with define-judgment-form

stlc.rkt

#lang racket

(require redex/pict
         redex/reduction-semantics)


;                                                                        
;                                                                        
;                                                                        
;   ;;;;             ;;    ;             ;             ;                 
;   ;   ;           ;      ;             ;     ;       ;                 
;   ;   ;           ;                          ;                         
;   ;   ;   ;;;    ;;;     ;    ;;;;     ;    ;;;      ;     ;;;   ;;;;  
;   ;   ;  ;   ;    ;      ;    ;   ;    ;     ;       ;    ;   ;  ;   ; 
;   ;   ;  ;;;;;    ;      ;    ;   ;    ;     ;       ;    ;   ;  ;   ; 
;   ;   ;  ;        ;      ;    ;   ;    ;     ;       ;    ;   ;  ;   ; 
;   ;   ;  ;   ;    ;      ;    ;   ;    ;     ;       ;    ;   ;  ;   ; 
;   ;;;;    ;;;     ;      ;    ;   ;    ;      ;;     ;     ;;;   ;   ; 
;                                                                        
;                                                                        
;                                                                        


(define-language STLC
  (e (λ (x τ) e)
     (e e)
     x
     integer
     add1)
  (τ int
     (τ → τ))
  (Γ ([x τ] ...))
  (x variable-not-otherwise-mentioned))

(define-judgment-form STLC
  mode : I I O
  typeof ⊆ Γ × e × τ
  [(typeof Γ (λ (x τ_1) e) (τ_1 → τ_2))
   (typeof (extend Γ x τ_1) e τ_2)]
  [(typeof Γ (e_1 e_2) τ)
   (typeof Γ e_1 (τ_2 → τ))
   (typeof Γ e_2 τ_2)]
  [(typeof Γ x τ)
   (where τ (lookup Γ x))]
  [(typeof Γ integer int)]
  [(typeof Γ add1 (int → int))])

(define-metafunction STLC
  extend : Γ x τ -> Γ
  [(extend ([x_0 τ_0] ... [x_i τ_i] [x_i+1 τ_i+1] ...) x_i τ)
   ([x_0 τ_0] ... [x_i τ] [x_i+1 τ_i+1] ...)]
  [(extend ([x_1 τ_1] ...) x_0 τ_0)
   ([x_0 τ_0] [x_1 τ_1] ...)])

(define-metafunction STLC
  lookup : Γ x -> τ
  [(lookup ([x_0 τ_0] ... [x_i τ_i] [x_i+1 τ_i+1] ...) x_i) τ_i])

(test-equal (judgment-holds (typeof () (λ (x int) (λ (x (int → int)) (x (add1 7)))) τ) τ)
            (list (term (int → ((int → int) → int)))))
(test-equal (judgment-holds (typeof () (λ (x int) (λ (x (int → int)) (add1 x))) τ))
            false)


;                                                                               
;                                                                               
;                                                                               
;   ;;;;;                                                     ;                 
;     ;                                        ;      ;       ;                 
;     ;                                        ;      ;                         
;     ;    ;   ;  ;;;;    ;;;    ;;;    ;;;   ;;;    ;;;      ;    ;;;;    ;;;; 
;     ;    ;   ;  ;   ;  ;   ;  ;   ;  ;   ;   ;      ;       ;    ;   ;  ;   ; 
;     ;    ;   ;  ;   ;  ;;;;;   ;;;   ;;;;;   ;      ;       ;    ;   ;  ;   ; 
;     ;    ;   ;  ;   ;  ;          ;  ;       ;      ;       ;    ;   ;  ;   ; 
;     ;    ;   ;  ;   ;  ;   ;  ;   ;  ;   ;   ;      ;       ;    ;   ;  ;   ; 
;     ;     ;;;;  ;;;;    ;;;    ;;;    ;;;     ;;     ;;     ;    ;   ;   ;;;; 
;              ;  ;                                                           ; 
;          ;   ;  ;                                                       ;   ; 
;           ;;;                                                            ;;;  


(define (rewrite-typeof lws)
  (list "" (list-ref lws 2) " ⊢ " (list-ref lws 3) " : " (list-ref lws 4)))
(define (rewrite-extend lws)
  (list "" (list-ref lws 2) ", " (list-ref lws 3) ":" (list-ref lws 4)))
(define (rewrite-lookup lws)
  (list "" (list-ref lws 2) "(" (list-ref lws 3) ")"))

(with-compound-rewriter 
 'typeof rewrite-typeof 
 (with-compound-rewriter
  'extend rewrite-extend 
  (with-compound-rewriter
   'lookup rewrite-lookup 
   (with-atomic-rewriter
    'integer "Z" (render-judgment-form typeof)))))