added names to clauses in define-judgment-form and added
judgment-form-cases to use the names to control typesetting
This commit is contained in:
parent
a190ecfb7b
commit
0369342bfe
|
@ -83,6 +83,8 @@
|
|||
[arrow-space (parameter/c natural-number/c)]
|
||||
[label-space (parameter/c natural-number/c)]
|
||||
[metafunction-cases (parameter/c (or/c #f (and/c pair? (listof (and/c integer? (or/c zero? positive?))))))]
|
||||
[judgment-form-cases (parameter/c (or/c #f (and/c (listof (or/c exact-nonnegative-integer? string?))
|
||||
pair?)))]
|
||||
[metafunction-pict-style
|
||||
(parameter/c (symbols 'left-right
|
||||
'left-right/vertical-side-conditions
|
||||
|
|
|
@ -337,12 +337,12 @@
|
|||
|
||||
(define-for-syntax (do-extended-judgment-form lang syn-err-name body orig stx)
|
||||
(define nts (definition-nts lang stx syn-err-name))
|
||||
(define-values (judgment-form-name dup-form-names mode position-contracts clauses)
|
||||
(define-values (judgment-form-name dup-form-names mode position-contracts clauses rule-names)
|
||||
(parse-judgment-form-body body syn-err-name stx (identifier? orig)))
|
||||
(define definitions
|
||||
#`(begin
|
||||
(define-syntax #,judgment-form-name
|
||||
(judgment-form '#,judgment-form-name '#,(cdr (syntax->datum mode)) #'judgment-form-runtime-proc #'mk-judgment-form-proc #'#,lang #'judgment-form-lws))
|
||||
(judgment-form '#,judgment-form-name '#,(cdr (syntax->datum mode)) #'judgment-form-runtime-proc #'mk-judgment-form-proc #'#,lang #'judgment-form-lws '#,rule-names))
|
||||
(define mk-judgment-form-proc
|
||||
(compile-judgment-form-proc #,judgment-form-name #,mode #,lang #,clauses #,position-contracts #,orig #,stx #,syn-err-name))
|
||||
(define judgment-form-runtime-proc (mk-judgment-form-proc #,lang))
|
||||
|
@ -375,13 +375,29 @@
|
|||
(regexp-match? #rx"^-+$" (symbol->string (syntax-e id))))
|
||||
(define-syntax-class horizontal-line
|
||||
(pattern x:id #:when (horizontal-line? #'x)))
|
||||
(define-syntax-class name
|
||||
(pattern x #:when (string? (syntax-e #'x))))
|
||||
(define (parse-rules rules)
|
||||
(for/list ([rule rules])
|
||||
(syntax-parse rule
|
||||
[(prem ... _:horizontal-line conc)
|
||||
#'(conc prem ...)]
|
||||
[_ rule])))
|
||||
(define-values (name/mode mode-stx name/contract contract rules)
|
||||
(define-values (backward-rules backward-names)
|
||||
(for/fold ([parsed-rules '()]
|
||||
[names '()])
|
||||
([rule rules])
|
||||
(syntax-parse rule
|
||||
[(prem ... _:horizontal-line n:name conc)
|
||||
(values (cons #'(conc prem ...) parsed-rules)
|
||||
(cons #'n names))]
|
||||
[(prem ... _:horizontal-line conc)
|
||||
(values (cons #'(conc prem ...) parsed-rules)
|
||||
(cons #f names))]
|
||||
[(conc prem ... n:name)
|
||||
(values (cons #'(conc prem ...) parsed-rules)
|
||||
(cons #'n names))]
|
||||
[else
|
||||
(values (cons rule parsed-rules)
|
||||
(cons #f names))])))
|
||||
(values (reverse backward-rules)
|
||||
(reverse backward-names)))
|
||||
(define-values (name/mode mode-stx name/contract contract rules rule-names)
|
||||
(syntax-parse body #:context full-stx
|
||||
[((~or (~seq #:mode ~! mode:mode-spec)
|
||||
(~seq #:contract ~! contract:contract-spec))
|
||||
|
@ -405,9 +421,10 @@
|
|||
(raise-syntax-error
|
||||
syn-err-name "expected at most one contract specification"
|
||||
#f #f (syntax->list #'dups))])])
|
||||
(values name/mode mode name/ctc ctc
|
||||
(parse-rules (syntax->list #'(rule ...)))))]))
|
||||
(define-values (parsed-rules rule-names) (parse-rules (syntax->list #'(rule ...))))
|
||||
(values name/mode mode name/ctc ctc parsed-rules rule-names))]))
|
||||
(check-clauses full-stx syn-err-name rules #t)
|
||||
(check-dup-rule-names full-stx syn-err-name rule-names)
|
||||
(check-arity-consistency mode-stx contract full-stx)
|
||||
(define-values (form-name dup-names)
|
||||
(syntax-case rules ()
|
||||
|
@ -415,8 +432,21 @@
|
|||
(not extension?)
|
||||
(raise-syntax-error #f "expected at least one rule" full-stx)]
|
||||
[_ (defined-name (list name/mode name/contract) rules full-stx)]))
|
||||
(values form-name dup-names mode-stx contract rules))
|
||||
(values form-name dup-names mode-stx contract rules rule-names))
|
||||
|
||||
;; names : (listof (or/c #f syntax[string]))
|
||||
(define-for-syntax (check-dup-rule-names full-stx syn-err-name names)
|
||||
(define tab (make-hash))
|
||||
(for ([name (in-list names)])
|
||||
(when (syntax? name)
|
||||
(define k (syntax-e name))
|
||||
(hash-set! tab k (cons name (hash-ref tab k '())))))
|
||||
(for ([(k names) (in-hash tab)])
|
||||
(unless (= 1 (length names))
|
||||
(raise-syntax-error syn-err-name
|
||||
"duplicate rule names"
|
||||
(car names) #f (cdr names)))))
|
||||
|
||||
(define-for-syntax (check-arity-consistency mode-stx contracts full-def)
|
||||
(when (and contracts (not (= (length (cdr (syntax->datum mode-stx)))
|
||||
(length contracts))))
|
||||
|
|
|
@ -62,6 +62,7 @@
|
|||
label-space
|
||||
metafunction-pict-style
|
||||
metafunction-cases
|
||||
judgment-form-cases
|
||||
compact-vertical-min-width
|
||||
extend-language-show-union
|
||||
set-arrow-pict!
|
||||
|
@ -360,23 +361,27 @@
|
|||
max-w))
|
||||
|
||||
(define (rp->pict-label rp)
|
||||
(define (bracket label)
|
||||
(hbl-append
|
||||
((current-text) " [" (label-style) (label-font-size))
|
||||
label
|
||||
((current-text) "]" (label-style) (label-font-size))))
|
||||
(cond [(rule-pict-computed-label rp) => bracket]
|
||||
[(rule-pict-label rp)
|
||||
(let ([m (regexp-match #rx"^([^_]*)(?:_([^_]*)|)$"
|
||||
(format "~a" (rule-pict-label rp)))])
|
||||
(bracket
|
||||
(hbl-append
|
||||
((current-text) (cadr m) (label-style) (label-font-size))
|
||||
(if (caddr m)
|
||||
((current-text) (caddr m) `(subscript . ,(label-style)) (label-font-size))
|
||||
(blank)))))]
|
||||
(string->bracketed-label
|
||||
(format "~a" (rule-pict-label rp)))]
|
||||
[else (blank)]))
|
||||
|
||||
(define (string->bracketed-label str)
|
||||
(define m (regexp-match #rx"^([^_]*)(?:_([^_]*)|)$" str))
|
||||
(bracket
|
||||
(hbl-append
|
||||
((current-text) (cadr m) (label-style) (label-font-size))
|
||||
(if (caddr m)
|
||||
((current-text) (caddr m) `(subscript . ,(label-style)) (label-font-size))
|
||||
(blank)))))
|
||||
|
||||
(define (bracket label)
|
||||
(hbl-append
|
||||
((current-text) " [" (label-style) (label-font-size))
|
||||
label
|
||||
((current-text) "]" (label-style) (label-font-size))))
|
||||
|
||||
(define (add-between i l)
|
||||
(cond
|
||||
[(null? l) l]
|
||||
|
@ -774,7 +779,7 @@
|
|||
|
||||
(define metafunction-pict-style (make-parameter 'left-right))
|
||||
(define metafunction-cases (make-parameter #f))
|
||||
(define (select-cases eqns)
|
||||
(define (select-mf-cases eqns)
|
||||
(let ([cases (metafunction-cases)])
|
||||
(if cases
|
||||
(let loop ([eqns eqns]
|
||||
|
@ -792,6 +797,31 @@
|
|||
(loop (cdr eqns) cases (+ i 1))])]))
|
||||
eqns)))
|
||||
|
||||
(define judgment-form-cases (make-parameter #f))
|
||||
(define (select-jf-cases eqns conclusions eqn-names)
|
||||
(define cases
|
||||
(or (judgment-form-cases)
|
||||
(metafunction-cases)))
|
||||
(cond
|
||||
[cases
|
||||
(define-values (rev-eqns rev-concs rev-eqn-names)
|
||||
(for/fold ([eqns '()]
|
||||
[concs '()]
|
||||
[eqn-names '()])
|
||||
([eqn (in-list eqns)]
|
||||
[conc (in-list conclusions)]
|
||||
[eqn-name (in-list eqn-names)]
|
||||
[i (in-naturals)])
|
||||
(if (or (member i cases)
|
||||
(member eqn-name cases))
|
||||
(values (cons eqn eqns)
|
||||
(cons conc concs)
|
||||
(cons eqn-name eqn-names))
|
||||
(values eqns concs eqn-names))))
|
||||
(values (reverse rev-eqns) (reverse rev-concs) (reverse rev-eqn-names))]
|
||||
[else
|
||||
(values eqns conclusions eqn-names)]))
|
||||
|
||||
;; remove-dups : (listof number)[sorted] -> (listof number)[sorted]
|
||||
;; removes duplicate numbers from 'l'
|
||||
(define (remove-dups l)
|
||||
|
@ -826,8 +856,8 @@
|
|||
(list-ref eqn 0))))
|
||||
(metafunc-proc-pict-info (metafunction-proc mf))))
|
||||
mfs))]
|
||||
[eqns (select-cases all-eqns)]
|
||||
[lhss (select-cases all-lhss)]
|
||||
[eqns (select-mf-cases all-eqns #f)]
|
||||
[lhss (select-mf-cases all-lhss #f)]
|
||||
[rhss (map (lambda (eqn) (wrapper->pict (list-ref eqn 2))) eqns)]
|
||||
[_ (unless (or (not current-linebreaks)
|
||||
(= (length current-linebreaks) (length eqns)))
|
||||
|
@ -1034,6 +1064,7 @@
|
|||
(error form "expected relation as argument, got a metafunction"))
|
||||
(inference-rules-pict (metafunc-proc-name (metafunction-proc mf))
|
||||
(metafunc-proc-pict-info (metafunction-proc mf))
|
||||
(map (λ (x) #f) (metafunc-proc-pict-info (metafunction-proc mf)))
|
||||
(metafunc-proc-lang (metafunction-proc mf))))
|
||||
|
||||
(define (render-pict make-pict filename)
|
||||
|
@ -1044,17 +1075,17 @@
|
|||
(parameterize ([dc-for-text-size (make-object bitmap-dc% (make-object bitmap% 1 1))])
|
||||
(make-pict))]))
|
||||
|
||||
(define (inference-rules-pict name all-eqns lang)
|
||||
(let* ([all-nts (language-nts lang)]
|
||||
[wrapper->pict (lambda (lw) (lw->pict all-nts lw))]
|
||||
[all-conclusions
|
||||
(map (lambda (eqn)
|
||||
(wrapper->pict
|
||||
(metafunction-call name (list-ref eqn 0))))
|
||||
all-eqns)]
|
||||
[eqns (select-cases all-eqns)]
|
||||
[conclusions (select-cases all-conclusions)]
|
||||
[premisess (map (lambda (eqn)
|
||||
(define (inference-rules-pict name all-eqns eqn-names lang)
|
||||
(define all-nts (language-nts lang))
|
||||
(define (wrapper->pict lw) (lw->pict all-nts lw))
|
||||
(define all-conclusions
|
||||
(map (lambda (eqn)
|
||||
(wrapper->pict
|
||||
(metafunction-call name (list-ref eqn 0))))
|
||||
all-eqns))
|
||||
(define-values (selected-eqns conclusions selected-eqn-names)
|
||||
(select-jf-cases all-eqns all-conclusions eqn-names))
|
||||
(define premisess (map (lambda (eqn)
|
||||
(append (map wrapper->pict (list-ref eqn 2))
|
||||
(map (match-lambda
|
||||
[(struct metafunc-extra-where (lhs rhs))
|
||||
|
@ -1063,18 +1094,29 @@
|
|||
(wrapper->pict expr)]
|
||||
[wrapper (wrapper->pict wrapper)])
|
||||
(list-ref eqn 1))))
|
||||
eqns)])
|
||||
((relation-clauses-combine)
|
||||
(for/list ([conclusion (in-list conclusions)]
|
||||
[premises (in-list premisess)])
|
||||
(define top (apply hbl-append 20 premises))
|
||||
(define line-w (max (pict-width top) (pict-width conclusion)))
|
||||
selected-eqns))
|
||||
((relation-clauses-combine)
|
||||
(for/list ([conclusion (in-list conclusions)]
|
||||
[premises (in-list premisess)]
|
||||
[name (in-list selected-eqn-names)])
|
||||
(define top (apply hbl-append 20 premises))
|
||||
(define line-w (max (pict-width top) (pict-width conclusion)))
|
||||
(define line (dc (λ (dc dx dy) (send dc draw-line dx dy (+ dx line-w) dy))
|
||||
line-w 1))
|
||||
(define w/out-label
|
||||
(vc-append
|
||||
(horizontal-bar-spacing)
|
||||
top
|
||||
(dc (λ (dc dx dy) (send dc draw-line dx dy (+ dx line-w) dy))
|
||||
line-w 1)
|
||||
conclusion)))))
|
||||
line
|
||||
conclusion))
|
||||
(if name
|
||||
(let ([label (string->bracketed-label name)])
|
||||
(let-values ([(x y) (rc-find w/out-label line)])
|
||||
(hb-append w/out-label
|
||||
(vl-append label
|
||||
(blank 0 (- (- (pict-height w/out-label) y)
|
||||
(/ (pict-height label) 2)))))))
|
||||
w/out-label))))
|
||||
|
||||
(define horizontal-bar-spacing (make-parameter 4))
|
||||
(define relation-clauses-combine (make-parameter (λ (l) (apply vc-append 20 l))))
|
||||
|
@ -1084,6 +1126,7 @@
|
|||
(syntax-property
|
||||
#`(inference-rules-pict '#,(judgment-form-name jf)
|
||||
#,(judgment-form-lws jf)
|
||||
'#,(judgment-form-rule-names jf)
|
||||
#,(judgment-form-lang jf))
|
||||
'disappeared-use
|
||||
form-name))
|
||||
|
|
|
@ -27,7 +27,7 @@
|
|||
(cond [(syntax-local-value stx (λ () #f)) => p?]
|
||||
[else #f])))
|
||||
|
||||
(define-struct judgment-form (name mode proc mk-proc lang lws))
|
||||
(define-struct judgment-form (name mode proc mk-proc lang lws rule-names))
|
||||
|
||||
(define-struct defined-term (value))
|
||||
(define (defined-term-id? stx)
|
||||
|
|
|
@ -1147,18 +1147,21 @@ and @racket[#f] otherwise.
|
|||
[pos-use I
|
||||
O]
|
||||
[rule [premise
|
||||
...
|
||||
dashes
|
||||
...
|
||||
dashes rule-name
|
||||
conclusion]
|
||||
[conclusion
|
||||
premise
|
||||
...]]
|
||||
...
|
||||
rule-name]]
|
||||
[conclusion (form-id pat/term ...)]
|
||||
[premise (code:line (judgment-form-id pat/term ...) maybe-ellipsis)
|
||||
(where @#,ttpattern @#,tttterm)
|
||||
(where/hidden @#,ttpattern @#,tttterm)
|
||||
(side-condition @#,tttterm)
|
||||
(side-condition/hidden @#,tttterm)]
|
||||
[rule-name (code:line)
|
||||
string]
|
||||
[pat/term @#,ttpattern
|
||||
@#,tttterm]
|
||||
[maybe-ellipsis (code:line)
|
||||
|
@ -1187,11 +1190,11 @@ For example, the following defines addition on natural numbers:
|
|||
(define-judgment-form nats
|
||||
#:mode (sum I I O)
|
||||
#:contract (sum n n n)
|
||||
[-----------
|
||||
[----------- "zero"
|
||||
(sum z n n)]
|
||||
|
||||
[(sum n_1 n_2 n_3)
|
||||
-------------------------
|
||||
------------------------- "add1"
|
||||
(sum (s n_1) n_2 (s n_3))])]
|
||||
|
||||
The @racket[judgment-holds] form checks whether a relation holds for any
|
||||
|
@ -1267,11 +1270,11 @@ one.
|
|||
#:mode (even I)
|
||||
#:contract (even n)
|
||||
|
||||
[--------
|
||||
[-------- "evenz"
|
||||
(even z)]
|
||||
|
||||
[(even n)
|
||||
----------------
|
||||
---------------- "even2"
|
||||
(even (s (s n)))])
|
||||
|
||||
(define-judgment-form nats
|
||||
|
@ -2546,8 +2549,24 @@ precede ellipses that represent argument sequences; when it is
|
|||
(or/c zero? positive?)))
|
||||
pair?))]{
|
||||
|
||||
This parameter controls which cases in a metafunction are rendered. If it is @racket[#f] (the default), then all of the
|
||||
Controls which cases in a metafunction are rendered. If it is @racket[#f] (the default), then all of the
|
||||
cases appear. If it is a list of numbers, then only the selected cases appear (counting from @racket[0]).
|
||||
|
||||
This parameter also controls how which clauses in judgment forms are rendered, but
|
||||
only in the case that @racket[judgment-form-cases] is @racket[#f].
|
||||
}
|
||||
|
||||
@defparam[judgment-form-cases
|
||||
cases
|
||||
(or/c #f
|
||||
(and/c (listof (or/c exact-nonnegative-integer?
|
||||
string?))
|
||||
pair?))]{
|
||||
Controls which clauses in a judgment form are rendered. If it is
|
||||
@racket[#f] (the default), then all of them are rendered. If
|
||||
it is a list, then only the selected clauses appear (numbers
|
||||
count from @racket[0], and strings correspond to the labels
|
||||
in a judgment form).
|
||||
}
|
||||
|
||||
@deftogether[[
|
||||
|
|
|
@ -2,6 +2,10 @@ v5.3.1
|
|||
|
||||
* added optional #:lang keyword to term
|
||||
|
||||
* added the ability to name clauses to define-judgment-form
|
||||
|
||||
* added judgment-form-cases
|
||||
|
||||
v5.3
|
||||
|
||||
* added the amb tutorial.
|
||||
|
|
Loading…
Reference in New Issue
Block a user