428 lines
12 KiB
Racket
428 lines
12 KiB
Racket
#lang racket
|
||
(require "bitmap-test-util.rkt"
|
||
"../main.rkt"
|
||
slideshow/pict)
|
||
|
||
;; tests:
|
||
;; - language,
|
||
;; - multi-line non-terminals, single-line non-terminals
|
||
(define-language lang
|
||
(e (e e)
|
||
x
|
||
(λ (x) e)
|
||
number)
|
||
(v number (λ (x) e))
|
||
((x y) variable-not-otherwise-mentioned))
|
||
|
||
(btest (render-language lang) "language.png")
|
||
|
||
(btest (render-language lang #:nts '(e v)) "language-nox.png")
|
||
|
||
(define-extended-language lang++ lang
|
||
(e .... number (+ e e))
|
||
(v .... number))
|
||
|
||
(btest (render-language lang++) "extended-language.png")
|
||
|
||
(define red
|
||
(reduction-relation
|
||
lang
|
||
(--> ((λ (x) e) v) (S x v e))))
|
||
|
||
;; tests: reduction-relation
|
||
(btest (render-reduction-relation red)
|
||
"reduction-relation.png")
|
||
|
||
(btest (render-reduction-relation
|
||
(extend-reduction-relation red lang (--> 1 2)))
|
||
"extended-reduction-relation.png")
|
||
|
||
(btest (render-reduction-relation
|
||
(with-unquote-rewriter
|
||
(let ([once? #f])
|
||
(λ (l)
|
||
(if once?
|
||
l
|
||
(begin0
|
||
(struct-copy lw
|
||
l
|
||
[e "a: any"]
|
||
[unq? #f])
|
||
(set! once? #t)))))
|
||
(reduction-relation
|
||
lang
|
||
(--> (a any) 1 "a" (computed-name (format "a: ~a" (term any))))
|
||
(--> (b any) 2 "b" (computed-name (format "b: ~a" (term any))))
|
||
(--> (c any) 3 (computed-name (format "c: ~a" (term any)))))))
|
||
"reduction-relation-with-computed-labels.png")
|
||
|
||
(let ([R (reduction-relation
|
||
lang
|
||
(--> 1 1 "a")
|
||
(--> 2 2 "b" (computed-name "a"))
|
||
(--> 3 3 (computed-name "c")))])
|
||
(btest (parameterize ([render-reduction-relation-rules (remq 'b (reduction-relation->rule-names R))])
|
||
(render-reduction-relation R))
|
||
"reduction-relation-with-computed-labels-and-hiding.png"))
|
||
|
||
;; this test should fail because it gets the order wrong
|
||
;; for the where/side-conditions
|
||
(define red2
|
||
(reduction-relation
|
||
lang
|
||
(--> (number_a number_b number_c number_d)
|
||
any_z
|
||
(where (any_x any_y) (number_a number_b))
|
||
(side-condition (= (term number_c) 5))
|
||
(where any_z any_x)
|
||
(side-condition (= (term number_d) 5)))))
|
||
|
||
(btest (render-reduction-relation red2)
|
||
"red2.png")
|
||
|
||
(let ()
|
||
(define-judgment-form lang
|
||
#:mode (id I O)
|
||
[(id e e)])
|
||
(btest (render-reduction-relation
|
||
(reduction-relation
|
||
lang
|
||
(--> e_1
|
||
q
|
||
(where (name q e_2) e_1)
|
||
(judgment-holds (id e_2 (name r e_3))))))
|
||
"red-with-where-name.png"))
|
||
|
||
(define-metafunction lang
|
||
[(S x v e) e])
|
||
|
||
(btest (render-metafunction S)
|
||
"metafunction.png")
|
||
|
||
(let ()
|
||
(define-metafunction lang
|
||
[(f (e_1 e_2))
|
||
(e_3 e_4)
|
||
(judgment-holds (J e_1 e_3))
|
||
(judgment-holds (J e_2 e_4))])
|
||
(define-judgment-form lang
|
||
#:mode (J I O)
|
||
[(J e e)])
|
||
(btest (render-metafunction f)
|
||
"metafunction-judgment-holds.png"))
|
||
|
||
(define-metafunction lang
|
||
[(T x y)
|
||
1
|
||
(side-condition (not (eq? (term x) (term y))))
|
||
(clause-name first-one)]
|
||
[(T x x)
|
||
(any_1 any_2)
|
||
(where any_1 2)
|
||
(where any_2 2)])
|
||
|
||
;; in this test, the metafunction has 2 clauses
|
||
;; with a side-condition on the first clause
|
||
;; and a 'where' in the second clause
|
||
(btest (parameterize ([metafunction-cases '("first-one" 1)])
|
||
(render-metafunction T))
|
||
"metafunction-T.png")
|
||
|
||
;; in this test, the `x' is italic and the 'z' is sf, since 'x' is in the grammar, and 'z' is not.
|
||
(btest (render-lw
|
||
lang
|
||
(to-lw ((λ (x) (x x))
|
||
(λ (z) (z z)))))
|
||
"lw.png")
|
||
|
||
(define-metafunction lang
|
||
[(TL 1) (a
|
||
,(term-let ((x (term 1)))
|
||
(term x))
|
||
below-only)]
|
||
[(TL 2) (a
|
||
,(term-let ((x (term 1)))
|
||
(term x)) beside
|
||
below)])
|
||
|
||
;; this tests that term-let is sucked away properly
|
||
;; when the metafunction is rendered
|
||
(btest (render-metafunction TL) "metafunction-TL.png")
|
||
|
||
(define-metafunction lang
|
||
[(Name (name x-arg arg))
|
||
,(term-let ((x-term-let (term 1)))
|
||
(term (x-where x-term-let)))
|
||
(where x-where 2)]
|
||
[(Name number) short])
|
||
|
||
;; this tests that the three variable bindings
|
||
;; (x-arg, x-term-let, and x-where)
|
||
;; all show up in the output.
|
||
(btest (render-metafunction Name) "metafunction-Name.png")
|
||
|
||
;; same as previous, but with vertical organization of the bindings
|
||
(btest (parameterize ([metafunction-pict-style 'up-down/vertical-side-conditions])
|
||
(render-metafunction Name))
|
||
"metafunction-Name-vertical.png")
|
||
|
||
;; compact turns out to be the same, since a line break is needed before
|
||
;; each side-condition clause:
|
||
(btest (parameterize ([metafunction-pict-style 'up-down/compact-side-conditions])
|
||
(render-metafunction Name))
|
||
"metafunction-Name-vertical.png")
|
||
|
||
;; in horizontal mode:
|
||
(btest (vl-append
|
||
(clip
|
||
(parameterize ([metafunction-pict-style 'left-right])
|
||
(render-metafunction Name)))
|
||
(clip
|
||
(parameterize ([metafunction-pict-style 'left-right/beside-side-conditions])
|
||
(render-metafunction Name)))
|
||
(clip
|
||
(parameterize ([metafunction-pict-style 'left-right/vertical-side-conditions])
|
||
(render-metafunction Name)))
|
||
(clip
|
||
(parameterize ([metafunction-pict-style 'left-right/compact-side-conditions])
|
||
(render-metafunction Name)))
|
||
(clip
|
||
(parameterize ([metafunction-pict-style 'left-right/compact-side-conditions]
|
||
[linebreaks '(#t #f)])
|
||
(render-metafunction Name)))
|
||
(clip
|
||
(parameterize ([metafunction-pict-style 'left-right/compact-side-conditions]
|
||
[linebreaks '(#f #t)])
|
||
(render-metafunction Name)))
|
||
(clip
|
||
(parameterize ([metafunction-pict-style 'left-right/beside-side-conditions]
|
||
[linebreaks '(#t #f)])
|
||
(render-metafunction Name))))
|
||
"metafunction-Name-horizontal.png")
|
||
|
||
;; makes sure that there is no overlap inside or across metafunction calls
|
||
;; or when there are unquotes involved
|
||
(define-metafunction lang
|
||
[(multi-arg a
|
||
b
|
||
c)
|
||
((multi-arg a
|
||
b
|
||
c)
|
||
(multi-arg a
|
||
b
|
||
c))]
|
||
[(multi-arg unquote-test)
|
||
(,@(term (multi-arg with-unquote))
|
||
,@(term (multi-arg with-unquote))
|
||
,@(term (multi-arg with-unquote)))])
|
||
|
||
(btest (render-metafunction multi-arg) "metafunction-multi-arg.png")
|
||
|
||
;; makes sure that the LHS and RHS of metafunctions are appropriately
|
||
;; rewritten
|
||
|
||
(define-metafunction lang
|
||
subst : e x e -> e
|
||
[(subst x x e) e]
|
||
[(subst number x e) number]
|
||
[(subst x_1 x_2 e) x_1]
|
||
[(subst (e_1 e_2) x e)
|
||
((subst e_1 x e) (subst e_2 x e))]
|
||
[(subst (λ (x) e_b) x e)
|
||
(λ (x) e)]
|
||
[(subst (λ (x_f) e_f) x_a e_a)
|
||
(λ (x_f) (subst e_f x_a e_a))])
|
||
|
||
(define (subst-rw lws)
|
||
(list ""
|
||
(list-ref lws 2)
|
||
"{"
|
||
(list-ref lws 3)
|
||
":="
|
||
(list-ref lws 4)
|
||
"}"))
|
||
|
||
(btest (with-atomic-rewriter
|
||
'number "number" ;; this rewriter has no effect; here to test that path in the code
|
||
(with-compound-rewriter
|
||
'subst subst-rw
|
||
(render-metafunction subst)))
|
||
"metafunction-subst.png")
|
||
|
||
|
||
;; make sure two metafunctions simultaneously rewritten line up properly
|
||
(btest (render-metafunctions S T TL) "metafunctions-multiple.png")
|
||
|
||
;; make sure that the ellipses don't have commas before them.
|
||
(define-metafunction lang
|
||
rdups : x ... -> (x ...)
|
||
[(rdups x_1 x_2 ... x_1 x_3 ...)
|
||
(rdups x_2 ... x_1 x_3 ...)]
|
||
[(rdups x_1 x_2 ...)
|
||
(x_1 x_3 ...)
|
||
(where (x_3 ...) (rdups x_2 ...))]
|
||
[(rdups) ()])
|
||
|
||
(btest (render-metafunction rdups) "rdups-delimited.png")
|
||
(parameterize ([delimit-ellipsis-arguments? #f])
|
||
(btest (render-metafunction rdups) "rdups-undelimited.png"))
|
||
|
||
;; Non-terminal superscripts
|
||
(btest (render-lw lang (to-lw (x_^abcdef x_q^abcdef)))
|
||
"superscripts.png")
|
||
|
||
;; `variable-not-in' in `where' RHS rendered as `fresh'
|
||
(define-metafunction lang
|
||
[(f (name n 1))
|
||
(x x_1 x_2 x_3)
|
||
(where x ,(variable-not-in 'y 'x))
|
||
(where (x_1 x_2) ,(variables-not-in 'z '(x1 x2)))
|
||
(where x_3 (variables-not-in 'z '(x1 x2)))])
|
||
(btest (render-metafunction f) "var-not-in.png")
|
||
(let ([variable-not-in list])
|
||
(define-metafunction lang
|
||
[(g 1)
|
||
x
|
||
(where x ,(variable-not-in 'y 'x))])
|
||
(btest (render-metafunction g) "var-not-in-rebound.png"))
|
||
|
||
;; hidden `where' and `side-condition' clauses
|
||
(define-metafunction lang
|
||
[(mf-hidden 1)
|
||
2
|
||
(where/hidden number 7)
|
||
(side-condition/hidden (= 1 2))])
|
||
(btest (render-metafunction mf-hidden) "mf-hidden.png")
|
||
(btest (render-reduction-relation
|
||
(reduction-relation
|
||
lang
|
||
(--> 1
|
||
2
|
||
(where/hidden number 7)
|
||
(side-condition/hidden (= 1 2)))))
|
||
"rr-hidden.png")
|
||
|
||
;; holes
|
||
(let ()
|
||
(define-language L
|
||
(n (hole x) ; a "named hole" at one time
|
||
hole))
|
||
(btest (render-language L) "holes.png"))
|
||
|
||
(let ()
|
||
;; the 'has no lambdas' relation (useful because it has a case with no premises)
|
||
(define-relation lang
|
||
[(r e_1 e_2) (r e_1) (r e_2)]
|
||
[(r x)])
|
||
(btest (render-relation r) "relation.png"))
|
||
|
||
(let ()
|
||
;; a relation with a `name' pattern in its conclusion
|
||
(define-relation lang
|
||
[(r (name e (λ (x) x)))
|
||
(r x)])
|
||
(btest (render-relation r) "relation-with-name.png"))
|
||
|
||
;; judgment form
|
||
(let ()
|
||
(define-language nats
|
||
(n z (s n)))
|
||
|
||
(define-judgment-form nats
|
||
#:mode (sum I I O)
|
||
[----------- "sumz"
|
||
(sum z n n)]
|
||
[(sum n_1 n_2 n_3)
|
||
------------------------- "sums"
|
||
(sum (s n_1) n_2 (s n_3))])
|
||
|
||
(define-judgment-form nats
|
||
#:mode (mfw I O)
|
||
[(mfw n_1 n_2)
|
||
(where n_2 (f n_1))])
|
||
|
||
(define-metafunction nats
|
||
[(f n) n])
|
||
|
||
(define-judgment-form nats
|
||
#:mode (nps I O)
|
||
[(nps (name a (s n_1)) n_2)
|
||
(nps z (name n_1 (s (s n_1))))
|
||
(where (name b n_2) z)])
|
||
|
||
(define-judgment-form nats
|
||
#:mode (lt2 I)
|
||
[(lt2 z)]
|
||
[(lt2 (s z))])
|
||
|
||
(define-judgment-form nats
|
||
#:mode (uses-ellipses I)
|
||
[(uses-ellipses (n ...))
|
||
(lt2 n) ... (sum z z z)])
|
||
|
||
(btest (vc-append
|
||
10
|
||
(render-judgment-form sum)
|
||
|
||
(with-compound-rewriter
|
||
'sum
|
||
(λ (lws) (list "" (list-ref lws 2) " + " (list-ref lws 3) " = " (list-ref lws 4)))
|
||
(render-judgment-form sum))
|
||
|
||
(render-judgment-form mfw)
|
||
|
||
(render-judgment-form nps)
|
||
|
||
(render-judgment-form uses-ellipses))
|
||
|
||
"judgment-form-examples.png"))
|
||
|
||
(let ()
|
||
(define-language STLC
|
||
(e (λ (x : τ) e)
|
||
(e e)
|
||
x)
|
||
(x variable-not-otherwise-mentioned)
|
||
((τ σ) b
|
||
(τ → τ))
|
||
(Γ ([x τ] ...)))
|
||
|
||
(define-judgment-form STLC
|
||
#:mode (typeof I I O)
|
||
#:contract (typeof Γ e τ)
|
||
[(typeof Γ (e_1 e_2) τ)
|
||
(typeof Γ e_1 (τ_2 → τ)) (typeof Γ e_2 τ_2)]
|
||
[(typeof Γ (λ (x : τ) e) (τ → σ))
|
||
(typeof (extend Γ x τ) e σ)]
|
||
[(typeof Γ x τ)
|
||
(where τ (lookup Γ x))])
|
||
|
||
(define-metafunction STLC
|
||
extend : Γ x τ -> Γ
|
||
[(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] ...)) τ_i])
|
||
|
||
(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) ")"))
|
||
|
||
(btest (with-compound-rewriters
|
||
(['typeof rewrite-typeof]
|
||
['extend rewrite-extend]
|
||
['lookup rewrite-lookup])
|
||
(render-judgment-form typeof))
|
||
"stlc.png"))
|
||
|
||
(printf "bitmap-test.rkt: ")
|
||
(done)
|