#lang racket/base
(require "amb.rkt"
"util.rkt"
redex
slideshow
slideshow/play
racket/gui/base)
(provide typeset-amb)
(define steps
(cond
[(getenv "SPEEDUP") 2]
[else 32]))
(define (typeset-amb)
(cond
[printing?
(slide (nth-pict 0))
(slide (nth-pict 1))]
[else
(play-n
#:steps (- steps 1)
(λ (n) (hash-ref nth-pict-table n)))]))
(default-font-size 24)
(label-font-size (default-font-size))
(metafunction-font-size (default-font-size))
(literal-style '(bold . roman))
(label-style "Gill Sans")
(default-style 'roman)
(define (nth-pict n)
(define-values (x0 y0 w0 h0) (find-p-grammar L-pict))
(define-values (x1 y1 w1 h1) (find-grammar L-pict))
(define-values (x2 y2 w2 h2) (find-red red-pict))
(define-values (x3 y3 w3 h3) (find-types types-pict))
(define-values (src0 w/src0) (extract-subpict main L-pict x0 y0 w0 h0 n))
(define-values (src1 w/src1) (extract-subpict w/src0 L-pict x1 y1 w1 h1 n))
(define-values (src2 w/src2) (extract-subpict w/src1 red-pict x2 y2 w2 h2 n))
(define-values (src3 w/src3) (extract-subpict w/src2 types-pict x3 y3 w3 h3 n))
(define dest0 (scale (ghost+launder src0) 2))
(define dest1 (scale (ghost+launder src1) 2))
(define dest2 (scale (ghost+launder src2) 2))
(define dest3 (scale (ghost+launder src3) 2))
(define w/dest3 (cc-superimpose w/src3 (vc-append 40
dest1 dest3
(blank) (blank)
dest0 dest2)))
(cc-superimpose
(cellophane main (+ 1/4 (* 3/4 (- 1 n))))
(slide-pict
(slide-pict
(slide-pict
(slide-pict
(ghost w/dest3)
(scale src3 (+ 1 n))
src3 dest3 n)
(scale src2 (+ 1 n))
src2 dest2 n)
(scale src1 (+ 1 n))
src1 dest1 n)
(scale src0 (+ 1 n))
src0 dest0 n)))
(define (ghost+launder p)
(ghost (launder p)))
(define (find-p-grammar L-pict)
(define lh (default-line-height))
(values -10
0
120
lh))
(define (find-grammar L-pict)
(define lh (default-line-height))
(values 30
(* lh 6)
130
lh))
(define (find-red red-pict)
(define lh (default-line-height))
(values 0
(+ (* lh 4)
(* 2 (reduction-relation-rule-separation))
30 )
(pict-width red-pict)
(* 2 lh)))
(define (find-types types-pict)
(define lh (default-line-height))
(define width-inset 70)
(values width-inset
(+ (* lh 13)
(* (horizontal-bar-spacing) 14)
(* 20 7)
0 )
(- (pict-width types-pict)
width-inset
width-inset)
(+ (* 2 lh)
(* (horizontal-bar-spacing) 2))))
(define (default-line-height)
(pict-height (text "xY" (default-style) (default-font-size))))
(define (extract-subpict main p x y w h n)
(define dest
(fade-frame
n
(white-backing
(launder
(inset/clip p
(- x)
(- y)
(- (- (pict-width p) x w))
(- (- (pict-height p) y h)))))))
(define-values (mx my) (lt-find main p))
(values dest
(pin-over main
(+ mx x)
(+ my y)
dest)))
(define (fade-frame n p)
(refocus
(cc-superimpose p
(cellophane
(frame (blank (+ (pict-width p) selection-region-extra-space)
(+ (pict-height p) selection-region-extra-space)))
n))
p))
(define (white-backing p)
(refocus (cc-superimpose
(colorize (filled-rectangle (+ (pict-width p) selection-region-extra-space)
(+ (pict-height p) selection-region-extra-space))
"white")
p)
p))
(define selection-region-extra-space 8)
(define (with-rewriters/proc t)
(with-atomic-rewriter
':
(λ () (text ":" (default-style) (default-font-size)))
(with-compound-rewriter
'types
(λ (lws)
(define gamma (list-ref lws 2))
(define exp (list-ref lws 3))
(define type (list-ref lws 4))
(list "" gamma " ⊢ " exp " : " type ""))
(with-compound-rewriter
'different
(λ (lws)
(define lhs (list-ref lws 2))
(define rhs (list-ref lws 3))
(list "" lhs " ≠ " rhs ""))
(with-compound-rewriter
'subst
(λ (lws)
(define xv (lw-e (list-ref lws 3)))
(define x (list-ref xv 1))
(define v (list-ref xv 2))
(define body (list-ref lws 2))
(list "" body "{" x ":=" v " ...}"))
(with-compound-rewriter
'λ
(λ (lws)
(match-define (list opn lam params body close) lws)
(define (open-paren? x)
(and (lw? x) (equal? "(" (lw-e x))))
(define new-params
(for/list ([param (in-list (lw-e params))]
[n (in-naturals)])
(match (lw-e param)
[(list (? open-paren? op) x t cp)
(struct-copy lw param
[e
(if (= n 1)
(list 'spring
x
'spring
(just-before ":" t)
t)
(list 'spring
(just-before " " x)
x
'spring
(just-before ":" t)
t))])]
[else param])))
(list opn "λ "
(struct-copy lw params
[e new-params])
body close))
(t)))))))
(define-syntax-rule
(with-rewriters e)
(with-rewriters/proc (λ () e)))
(define types-pict
(with-rewriters
(judgment-form->pict types)))
(define red-pict
(with-rewriters
(reduction-relation->pict
red
#:style 'compact-vertical)))
(define L-pict
(with-rewriters
(language->pict L
#:nts (remove 'x (language-nts L)))))
(define Ev-pict
(with-rewriters
(language->pict Ev)))
(define main
(evenize
(hc-append 50
(vl-append 40
L-pict
Ev-pict
red-pict)
types-pict)))
(define nth-pict-table (make-hash))
(unless printing?
(time
(begin
(printf "rendering amb ") (flush-output)
(for ([x (in-range steps)])
(define n (/ x (- steps 1) 1.0))
(hash-set! nth-pict-table n (to-bitmap (nth-pict n)))
(display ".") (flush-output))
(printf " done\n"))))