(module pict mzscheme
(require (lib "mrpict.ss" "texpict")
(lib "utils.ss" "texpict")
(lib "etc.ss")
(lib "list.ss")
(lib "mred.ss" "mred")
(lib "class.ss")
(lib "kw.ss")
"reduction-semantics.ss"
"struct.ss"
"loc-wrapper.ss"
"matcher.ss"
"arrow.ss"
"core-layout.ss")
(provide language->pict
language->ps
reduction-relation->pict
reduction-relation->ps
metafunction->pict
metafunction->ps
set-rule-picts-style!
compact-vertical-min-width)
(define STIX? #f)
(define reduction-relation->pict
(lambda/kw (rr #:key [rules #f] [converters #hash()])
(current-rule-picts->pict
(map (rr-lws->trees (language-nts (reduction-relation-lang rr)) converters)
(if rules
(let ([ht (make-hash-table 'equal)])
(for-each (lambda (rp)
(hash-table-put! ht (rule-pict-label rp) rp))
(reduction-relation-lws rr))
(map (lambda (label)
(hash-table-get ht label
(lambda ()
(error 'reduction-relation->pict
"no rule found for label: ~e"
label))))
rules))
(reduction-relation-lws rr))))))
(define/kw (reduction-relation->ps rr filename #:key [rules #f] [converters #hash()])
(save-as-ps (λ () (reduction-relation->pict rr #:rules rules #:converters converters))
filename))
(define ((rr-lws->trees nts converters) rp)
(let ([tp (λ (x) (lw->pict nts x))])
(make-rule-pict (rule-pict-arrow rp)
(tp (rule-pict-lhs rp))
(tp (rule-pict-rhs rp))
(rule-pict-label rp)
(map tp (rule-pict-side-conditions rp))
(map tp (rule-pict-fresh-vars rp))
(map (lambda (v)
(cons (tp (car v)) (tp (cdr v))))
(rule-pict-pattern-binds rp)))))
(define (rule-picts->pict/horizontal rps)
(let ([lhs-space (make-horiz-space (map rule-pict-lhs rps))]
[rhs-space (make-horiz-space (map rule-pict-rhs rps))]
[label-space (make-horiz-space (map rp->pict-label rps))]
[side-condition-width
(pict-width (apply rt-superimpose (map (lambda (rp) (rp->side-condition-pict rp +inf.0)) rps)))]
[arrow-space
(inset (make-horiz-space (map arrow->pict (map rule-pict-arrow rps)))
2
0)])
(apply
vr-append
(add-between
(blank 0 4)
(map (λ (rp)
(vr-append (widen
side-condition-width
(htl-append
(inset (rule-pict-lhs rp)
(- (pict-width lhs-space)
(pict-width (rule-pict-lhs rp)))
0 0 0)
(blank 2 0)
(let* ([ap (arrow->pict (rule-pict-arrow rp))]
[extra-space
(/ (- (pict-width arrow-space)
(pict-width ap))
2)])
(inset ap extra-space 0 extra-space 0))
(blank 2 0)
(inset (rule-pict-rhs rp)
0 0
(- (pict-width rhs-space)
(pict-width (rule-pict-rhs rp)))
0)
(blank 2 0)
(inset (rp->pict-label rp)
0 0
(- (pict-width label-space)
(pict-width (rp->pict-label rp)))
0)))
(rp->side-condition-pict rp +inf.0)))
rps)))))
(define current-label-extra-space (make-parameter 0))
(define (widen w pict)
(cond
[(< (pict-width pict) w)
(htl-append (blank (- w (pict-width pict)) 0)
pict)]
[else
pict]))
(define (rule-picts->pict/horizontal rps)
(let ([sep 2])
(let ([max-rhs (apply max
0
(map pict-width
(map rule-pict-rhs rps)))]
[max-w (apply max
0
(map (lambda (rp)
(+ sep sep
(pict-width (rule-pict-lhs rp))
(pict-width (arrow->pict (rule-pict-arrow rp)))
(pict-width (rule-pict-rhs rp))))
rps))])
(table 4
(apply
append
(map (lambda (rp)
(let ([arrow (arrow->pict (rule-pict-arrow rp))]
[lhs (rule-pict-lhs rp)]
[rhs (rule-pict-rhs rp)]
[spc (basic-text " " default-style)]
[label (rp->pict-label rp)]
[sep (blank 4)])
(list lhs arrow rhs label
(blank) (blank)
(let ([sc (rp->side-condition-pict rp max-w)])
(inset sc (min 0 (- max-rhs (pict-width sc))) 0 0 0))
(blank)
sep (blank) (blank) (blank))))
rps))
(list* rtl-superimpose ctl-superimpose ltl-superimpose)
(list* rtl-superimpose ctl-superimpose ltl-superimpose)
(list* sep sep (+ sep (current-label-extra-space))) 2))))
(define ((make-vertical-style side-condition-combiner) rps)
(let* ([mk-top-line-spacer
(λ (rp)
(hbl-append (rule-pict-lhs rp)
(basic-text " " default-style)
(arrow->pict (rule-pict-arrow rp))
(basic-text " " default-style)
(rp->pict-label rp)))]
[mk-bot-line-spacer
(λ (rp)
(rt-superimpose
(rule-pict-rhs rp)
(rp->side-condition-pict rp +inf.0)))]
[multi-line-spacer
(ghost
(launder
(ctl-superimpose
(apply ctl-superimpose (map mk-top-line-spacer rps))
(apply ctl-superimpose (map mk-bot-line-spacer rps)))))]
[spacer (dc void
(pict-width multi-line-spacer)
(pict-descent multi-line-spacer) 0
(pict-descent multi-line-spacer))])
(apply
vl-append
(add-between
(blank 0 4)
(map (λ (rp)
(side-condition-combiner
(vl-append
(ltl-superimpose
(htl-append (rule-pict-lhs rp)
(basic-text " " default-style)
(arrow->pict (rule-pict-arrow rp)))
(rtl-superimpose
spacer
(rp->pict-label rp)))
(rule-pict-rhs rp))
(rp->side-condition-pict rp +inf.0)))
rps)))))
(define compact-vertical-min-width (make-parameter 0))
(define rule-picts->pict/vertical
(make-vertical-style vr-append))
(define rule-picts->pict/vertical-overlapping-side-conditions
(make-vertical-style rbl-superimpose))
(define (rule-picts->pict/compact-vertical rps)
(let ([max-w (apply max
(compact-vertical-min-width)
(map pict-width
(append
(map rule-pict-lhs rps)
(map rule-pict-rhs rps))))])
(table 3
(apply
append
(map (lambda (rp)
(let ([arrow (arrow->pict (rule-pict-arrow rp))]
[lhs (rule-pict-lhs rp)]
[rhs (rule-pict-rhs rp)]
[spc (basic-text " " default-style)]
[label (rp->pict-label rp)]
[sep (blank (compact-vertical-min-width) 4)])
(if ((apply + (map pict-width (list lhs spc arrow spc rhs)))
. < .
max-w)
(list
(blank) (hbl-append lhs spc arrow spc rhs) label
(blank) (rp->side-condition-pict rp max-w) (blank)
(blank) sep (blank))
(list (blank) lhs label
arrow rhs (blank)
(blank) (rp->side-condition-pict rp max-w) (blank)
(blank) sep (blank)))))
rps))
ltl-superimpose ltl-superimpose
(list* 2 (+ 2 (current-label-extra-space))) 2)))
(define (side-condition-pict fresh-vars side-conditions pattern-binds max-w)
(let* ([frsh
(if (null? fresh-vars)
null
(list
(hbl-append
(apply
hbl-append
(add-between
'comma
fresh-vars))
(basic-text " fresh" default-style))))]
[binds (map (lambda (b)
(htl-append
(car b)
(make-=)
(cdr b)))
pattern-binds)]
[lst (add-between
'comma
(append
binds
side-conditions
frsh))])
(if (null? lst)
(blank)
(let ([where (basic-text " where " default-style)])
(let ([max-w (- max-w (pict-width where))])
(htl-append where
(let loop ([p (car lst)][lst (cdr lst)])
(cond
[(null? lst) p]
[(eq? (car lst) 'comma)
(loop (htl-append p (basic-text ", " default-style))
(cdr lst))]
[((+ (pict-width p) (pict-width (car lst))) . > . max-w)
(vl-append p
(loop (car lst) (cdr lst)))]
[else (loop (htl-append p (car lst)) (cdr lst))]))))))))
(define (rp->side-condition-pict rp max-w)
(side-condition-pict (rule-pict-fresh-vars rp)
(rule-pict-side-conditions rp)
(rule-pict-pattern-binds rp)
max-w))
(define (rp->pict-label rp)
(if (rule-pict-label rp)
(let ([m (regexp-match #rx"^([^_]*)(?:_([^_]*)|)$"
(format "~a" (rule-pict-label rp)))])
(hbl-append
(text " [" label-style (label-font-size))
(text (cadr m) label-style (label-font-size))
(if (caddr m)
(text (caddr m) `(subscript . ,label-style) (label-font-size))
(blank))
(text "]" label-style (label-font-size))))
(blank)))
(define (add-between i l)
(cond
[(null? l) l]
[else
(cons (car l)
(apply append
(map (λ (x) (list i x)) (cdr l))))]))
(define (make-horiz-space picts) (blank (pict-width (apply cc-superimpose picts)) 0))
(define current-rule-picts->pict rule-picts->pict/vertical)
(define (set-rule-picts-style! s)
(set! current-rule-picts->pict
(case s
[(vertical) rule-picts->pict/vertical]
[(compact-vertical) rule-picts->pict/compact-vertical]
[(vertical-overlapping-side-conditions)
rule-picts->pict/vertical-overlapping-side-conditions]
[else rule-picts->pict/horizontal])))
(define (mk-arrow-pict sz style)
(make-arrow-pict sz style default-style (default-font-size)))
(define long-arrow-pict (mk-arrow-pict "xxx" 'straight))
(define short-arrow-pict (mk-arrow-pict "m" 'straight))
(define curvy-arrow-pict (mk-arrow-pict "xxx" 'curvy))
(define short-curvy-arrow-pict (mk-arrow-pict "m" 'curvy))
(define double-arrow-pict (mk-arrow-pict "xxx" 'straight-double))
(define short-double-arrow-pict (mk-arrow-pict "m" 'straight-double))
(define (arrow->pict arr)
(case arr
[(--> -+>) (long-arrow-pict)]
[(==>) (double-arrow-pict)]
[(->) (short-arrow-pict)]
[(=>) (short-double-arrow-pict)]
[(..>) (basic-text "\u21E2" default-style)]
[(>->) (basic-text "\u21a3" default-style)]
[(~~>) (curvy-arrow-pict)]
[(~>) (short-curvy-arrow-pict)]
[(:->) (basic-text "\u21a6" default-style)]
[(c->) (basic-text "\u21aa" default-style)]
[(-->>) (basic-text "\u21a0" default-style)]
[(>--) (basic-text "\u291a" default-style)]
[(--<) (basic-text "\u2919" default-style)]
[(>>--) (basic-text "\u291c" default-style)]
[(--<<) (basic-text "\u291b" default-style)]
[else (error 'arrow->pict "unknown arrow ~s" arr)]))
(define/kw (language->ps lang non-terminals filename #:key [pict-wrap (lambda (p) p)])
(save-as-ps (λ () (pict-wrap (language->pict lang non-terminals)))
filename))
(define (language->pict lang non-terminals)
(let* ([all-non-terminals (hash-table-map (compiled-lang-ht lang) (λ (x y) x))]
[non-terminals (or non-terminals all-non-terminals)])
(make-grammar-pict (compiled-lang-pict-builder lang)
non-terminals
all-non-terminals)))
(define (save-as-ps mk-pict filename)
(let ([ps-dc (make-ps-dc filename)])
(parameterize ([dc-for-text-size ps-dc])
(send ps-dc start-doc "x")
(send ps-dc start-page)
(draw-pict (mk-pict) ps-dc 0 0)
(send ps-dc end-page)
(send ps-dc end-doc))))
(define (make-ps-dc filename)
(let ([ps-setup (make-object ps-setup%)])
(send ps-setup copy-from (current-ps-setup))
(send ps-setup set-file filename)
(parameterize ([current-ps-setup ps-setup])
(make-object post-script-dc% #f #f))))
(define (make-grammar-pict raw-info nts all-nts)
(let* ([info (filter (λ (x) (member (car x) nts))
raw-info)]
[term-space
(launder
(ghost
(apply cc-superimpose (map (λ (x) (non-terminal (format "~a" (car x))))
info))))])
(apply vl-append
(map (λ (line)
(htl-append
(rc-superimpose term-space (non-terminal (format "~a" (car line))))
(add-bars
(map (λ (x) (lw->pict all-nts x))
(cdr line)))))
info))))
(define (make-::=) (basic-text " ::= " default-style))
(define (make-bar) (basic-text " | " default-style))
(define (add-bars lst)
(apply vl-append lst))
(define (add-bars lst)
(cond
[(null? lst) null]
[else
(cons
(let ([fst (car lst)])
(make-loc-wrapper
(rc-superimpose (ghost (make-bar)) (make-::=))
(loc-wrapper-line fst)
(loc-wrapper-line-span fst)
(loc-wrapper-column fst)
0
(loc-wrapper-column fst)))
(let loop ([fst (car lst)]
[rst (cdr lst)])
(cond
[(null? rst) (list fst)]
[else
(let* ([snd (car rst)]
[bar
(cond
[(= (loc-wrapper-line snd)
(loc-wrapper-line fst))
(let* ([line (loc-wrapper-line snd)]
[line-span (loc-wrapper-line-span snd)]
[column (+ (loc-wrapper-column fst)
(loc-wrapper-span fst))]
[span (- (loc-wrapper-column snd)
(+ (loc-wrapper-column fst)
(loc-wrapper-span fst)))]
[last-column (+ column span)])
(make-loc-wrapper (make-bar) line line-span column span last-column))]
[else
(make-loc-wrapper
(rc-superimpose (make-bar) (ghost (make-::=)))
(loc-wrapper-line snd)
(loc-wrapper-line-span snd)
(loc-wrapper-column snd)
0
(loc-wrapper-column snd))])])
(list* fst
bar
(loop snd (cdr rst))))])))]))
(define (make-=) (basic-text " = " default-style))
(define metafunction->pict
(lambda/kw (mf #:key [converters #hash()] [linebreaks #f])
(let ([all-nts (language-nts (metafunc-proc-lang (metafunction-proc mf)))]
[sep 2])
(let ([wrapper->pict (lambda (lw) (lw->pict all-nts lw))])
(table 3
(apply append
(let* ([eqns (metafunc-proc-pict-info (metafunction-proc mf))]
[lhss (map (lambda (eqn) (wrapper->pict (car eqn))) eqns)]
[scs (map (lambda (eqn)
(if (and (null? (cadr eqn))
(null? (caddr eqn)))
#f
(side-condition-pict null
(map wrapper->pict (cadr eqn))
(map (lambda (p)
(cons (wrapper->pict (car p)) (wrapper->pict (cdr p))))
(caddr eqn))
+inf.0)))
eqns)]
[rhss (map (lambda (eqn) (wrapper->pict (cadddr eqn))) eqns)]
[linebreaks (or linebreaks
(map (lambda (x) #f) eqns))]
[=-pict (make-=)]
[max-lhs-w (apply max (map pict-width lhss))]
[max-line-w (apply
max
(map (lambda (lhs sc rhs linebreak?)
(max
(if sc (pict-width sc) 0)
(if linebreak?
(max (pict-width lhs)
(+ (pict-width rhs) (pict-width =-pict)))
(+ (pict-width lhs) (pict-width rhs) (pict-width =-pict)
(* 2 sep)))))
lhss scs rhss linebreaks))])
(map (lambda (lhs sc rhs linebreak?)
(append
(if linebreak?
(list lhs (blank) (blank))
(list lhs =-pict rhs))
(if linebreak?
(let ([p rhs])
(list (hbl-append sep
=-pict
(inset p 0 0 (- 5 (pict-width p)) 0))
(blank)
(blank (max 0 (- (pict-width p) max-lhs-w sep))
0)))
null)
(if (not sc)
null
(list (inset sc 0 0 (- 5 (pict-width sc)) 0)
(blank)
(blank (max 0 (- (pict-width sc) max-lhs-w (pict-width =-pict) (* 2 sep)))
0)))))
lhss
scs
rhss
linebreaks)))
ltl-superimpose ltl-superimpose
sep sep)))))
(define/kw (metafunction->ps mf filename #:key [converters #hash()] [linebreaks #f])
(save-as-ps (λ () (metafunction->pict mf #:converters converters #:linebreaks linebreaks))
filename)))