public
Created

STLC with define-judgment-form

  • Download Gist
stlc.rkt
Racket
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
#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)))))

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.