add clause-name to define-metafunction, to be used with the
newly extended metafunction-cases
This commit is contained in:
Robby Findler
parent
551150e805
commit
0c5c41fd54
|
|
@ -82,7 +82,7 @@
|
|||
(parameter/c reduction-rule-style/c)]
|
||||
[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?))))))]
|
||||
[metafunction-cases (parameter/c (or/c #f (and/c pair? (listof (or/c exact-nonnegative-integer? string?)))))]
|
||||
[judgment-form-cases (parameter/c (or/c #f (and/c (listof (or/c exact-nonnegative-integer? string?))
|
||||
pair?)))]
|
||||
[metafunction-pict-style
|
||||
|
|
|
|||
|
|
@ -4,6 +4,7 @@
|
|||
racket/class
|
||||
racket/match
|
||||
racket/pretty
|
||||
racket/set
|
||||
(only-in racket/list drop-right last partition)
|
||||
|
||||
texpict/mrpict
|
||||
|
|
@ -786,29 +787,38 @@
|
|||
|
||||
(define metafunction-pict-style (make-parameter 'left-right))
|
||||
(define metafunction-cases (make-parameter #f))
|
||||
(define (select-mf-cases eqns)
|
||||
(let ([cases (metafunction-cases)])
|
||||
(if cases
|
||||
(let loop ([eqns eqns]
|
||||
[cases (remove-dups (sort cases <))]
|
||||
[i 0])
|
||||
(cond
|
||||
[(null? eqns) null]
|
||||
[(null? cases) null]
|
||||
[else
|
||||
(define (select-mf-cases eqns case-labelss)
|
||||
(define mf-cases (metafunction-cases))
|
||||
(cond
|
||||
[mf-cases
|
||||
(define i 0)
|
||||
(define sorted-cases (remove-dups (sort (filter number? mf-cases) <)))
|
||||
(define named-cases (apply set (filter string? mf-cases)))
|
||||
(apply
|
||||
append
|
||||
(for/list ([eqns (in-list eqns)]
|
||||
[case-labels (in-list case-labelss)])
|
||||
(filter
|
||||
values
|
||||
(for/list ([eqn (in-list eqns)]
|
||||
[case-label (in-list case-labels)])
|
||||
(begin0
|
||||
(cond
|
||||
[(= i (car cases))
|
||||
(cons (car eqns)
|
||||
(loop (cdr eqns) (cdr cases) (+ i 1)))]
|
||||
[else
|
||||
(loop (cdr eqns) cases (+ i 1))])]))
|
||||
eqns)))
|
||||
[(and (pair? sorted-cases) (= i (car sorted-cases)))
|
||||
(set! sorted-cases (cdr sorted-cases))
|
||||
eqn]
|
||||
[(set-member? named-cases case-label)
|
||||
eqn]
|
||||
[else #f])
|
||||
(set! i (+ i 1)))))))]
|
||||
[else (apply append eqns)]))
|
||||
|
||||
(define judgment-form-cases (make-parameter #f))
|
||||
(define (select-jf-cases eqns conclusions eqn-names)
|
||||
(define cases
|
||||
(or (judgment-form-cases)
|
||||
(metafunction-cases)))
|
||||
(and (metafunction-cases)
|
||||
(filter number? (metafunction-cases)))))
|
||||
(cond
|
||||
[cases
|
||||
(define-values (rev-eqns rev-concs rev-eqn-names)
|
||||
|
|
@ -845,46 +855,46 @@
|
|||
(metafunc-proc-lang (metafunction-proc mf))))
|
||||
mfs)
|
||||
(error name "expected metafunctions that are all drawn from the same language"))
|
||||
(let* ([current-linebreaks (linebreaks)]
|
||||
[all-nts (language-nts (metafunc-proc-lang (metafunction-proc (car mfs))))]
|
||||
[sep 2]
|
||||
[style (metafunction-pict-style)]
|
||||
[wrapper->pict (lambda (lw) (lw->pict all-nts lw))]
|
||||
[all-eqns (apply append (map (λ (mf) (metafunc-proc-pict-info (metafunction-proc mf))) mfs))]
|
||||
[all-lhss
|
||||
(apply append
|
||||
(map (λ (mf)
|
||||
(map (lambda (eqn)
|
||||
(wrapper->pict
|
||||
(metafunction-call (metafunc-proc-name (metafunction-proc mf))
|
||||
(list-ref eqn 0))))
|
||||
(metafunc-proc-pict-info (metafunction-proc mf))))
|
||||
mfs))]
|
||||
[eqns (select-mf-cases all-eqns)]
|
||||
[lhss (select-mf-cases all-lhss)]
|
||||
[rhss (map (lambda (eqn) (wrapper->pict (list-ref eqn 2))) eqns)]
|
||||
[_ (unless (or (not current-linebreaks)
|
||||
(= (length current-linebreaks) (length eqns)))
|
||||
(error 'metafunction->pict "expected the current-linebreaks parameter to be a list whose length matches the number of cases in the metafunction (~a), but got ~s"
|
||||
(length eqns)
|
||||
current-linebreaks))]
|
||||
[linebreak-list (or current-linebreaks
|
||||
(map (lambda (x) #f) eqns))]
|
||||
[mode (case style
|
||||
(define current-linebreaks (linebreaks))
|
||||
(define all-nts (language-nts (metafunc-proc-lang (metafunction-proc (car mfs)))))
|
||||
(define sep 2)
|
||||
(define style (metafunction-pict-style))
|
||||
(define (wrapper->pict lw) (lw->pict all-nts lw))
|
||||
(define all-eqns (map (λ (mf) (metafunc-proc-pict-info (metafunction-proc mf))) mfs))
|
||||
(define all-lhss
|
||||
(map (λ (mf)
|
||||
(map (lambda (eqn)
|
||||
(wrapper->pict
|
||||
(metafunction-call (metafunc-proc-name (metafunction-proc mf))
|
||||
(list-ref eqn 0))))
|
||||
(metafunc-proc-pict-info (metafunction-proc mf))))
|
||||
mfs))
|
||||
(define case-labels (map (λ (mf) (metafunc-proc-clause-names (metafunction-proc mf))) mfs))
|
||||
(define eqns (select-mf-cases all-eqns case-labels))
|
||||
(define lhss (select-mf-cases all-lhss case-labels))
|
||||
(define rhss (map (lambda (eqn) (wrapper->pict (list-ref eqn 2))) eqns))
|
||||
(unless (or (not current-linebreaks)
|
||||
(= (length current-linebreaks) (length eqns)))
|
||||
(error 'metafunction->pict "expected the current-linebreaks parameter to be a list whose length matches the number of cases in the metafunction (~a), but got ~s"
|
||||
(length eqns)
|
||||
current-linebreaks))
|
||||
(define linebreak-list (or current-linebreaks
|
||||
(map (lambda (x) #f) eqns)))
|
||||
(define mode (case style
|
||||
[(left-right left-right/vertical-side-conditions left-right/compact-side-conditions left-right/beside-side-conditions)
|
||||
'horizontal]
|
||||
[(up-down up-down/vertical-side-conditions up-down/compact-side-conditions) 'vertical]
|
||||
[else (error 'metafunctions->pict "unknown mode")])]
|
||||
[=-pict (make-=)]
|
||||
[vertical-side-conditions?
|
||||
(memq style '(up-down/vertical-side-conditions
|
||||
left-right/vertical-side-conditions
|
||||
left-right*/vertical-side-conditions))]
|
||||
[compact-side-conditions?
|
||||
(memq style '(up-down/compact-side-conditions
|
||||
left-right/compact-side-conditions
|
||||
left-right*/compact-side-conditions))]
|
||||
[max-line-w/pre-sc (and
|
||||
[else (error 'metafunctions->pict "unknown mode")]))
|
||||
(define =-pict (make-=))
|
||||
(define vertical-side-conditions?
|
||||
(memq style '(up-down/vertical-side-conditions
|
||||
left-right/vertical-side-conditions
|
||||
left-right*/vertical-side-conditions)))
|
||||
(define compact-side-conditions?
|
||||
(memq style '(up-down/compact-side-conditions
|
||||
left-right/compact-side-conditions
|
||||
left-right*/compact-side-conditions)))
|
||||
(define max-line-w/pre-sc (and
|
||||
compact-side-conditions?
|
||||
(apply
|
||||
max
|
||||
|
|
@ -899,112 +909,111 @@
|
|||
[else
|
||||
(+ (pict-width lhs) (pict-width rhs) (pict-width =-pict)
|
||||
(* 2 sep))]))
|
||||
lhss rhss linebreak-list)))]
|
||||
[scs (map (lambda (eqn)
|
||||
(let ([scs (reverse (list-ref eqn 1))])
|
||||
(if (null? scs)
|
||||
#f
|
||||
(let-values ([(fresh where/sc) (partition metafunc-extra-fresh? scs)])
|
||||
(side-condition-pict (foldl (λ (clause picts)
|
||||
(foldr (λ (l ps) (cons (wrapper->pict l) ps))
|
||||
picts (metafunc-extra-fresh-vars clause)))
|
||||
'() fresh)
|
||||
(map (match-lambda
|
||||
[(struct metafunc-extra-where (lhs rhs))
|
||||
(where-pict (wrapper->pict lhs) (wrapper->pict rhs))]
|
||||
[(struct metafunc-extra-side-cond (expr))
|
||||
(wrapper->pict expr)])
|
||||
where/sc)
|
||||
(cond
|
||||
[vertical-side-conditions?
|
||||
;; maximize line breaks:
|
||||
0]
|
||||
[compact-side-conditions?
|
||||
;; maximize line break as needed:
|
||||
max-line-w/pre-sc]
|
||||
[else
|
||||
;; no line breaks:
|
||||
+inf.0]))))))
|
||||
eqns)])
|
||||
(case mode
|
||||
[(horizontal)
|
||||
(define (adjust-for-fills rows)
|
||||
;; Some rows have the form (list <pict> 'fill 'fill),
|
||||
;; in which case we want the <pict> to span all columns.
|
||||
;; To do that, we need to know the total width of the first
|
||||
;; two columns of non-spanning rows.
|
||||
(define max-w-before-rhs (apply
|
||||
max
|
||||
(map (lambda (row)
|
||||
(match row
|
||||
[(list lhs 'fill 'fill)
|
||||
(+ sep sep)]
|
||||
[else
|
||||
(+ (pict-width (car row))
|
||||
sep
|
||||
(pict-width (cadr row))
|
||||
sep)]))
|
||||
rows)))
|
||||
(apply
|
||||
append
|
||||
(map (lambda (row)
|
||||
(match row
|
||||
[(list lhs 'fill 'fill)
|
||||
(list
|
||||
;; pretend that content is zero-width:
|
||||
(inset lhs 0 0 (- (pict-width lhs)) 0)
|
||||
(blank)
|
||||
;; blank that's wide enough to ensure that the
|
||||
;; right column covers the spanning pict
|
||||
;; (and no more)
|
||||
(blank (max 0 (- (pict-width lhs) max-w-before-rhs))
|
||||
0))]
|
||||
[else row]))
|
||||
rows)))
|
||||
(table 3
|
||||
(adjust-for-fills
|
||||
(apply append
|
||||
(map (lambda (lhs sc rhs linebreak?)
|
||||
(append
|
||||
(list
|
||||
(cond
|
||||
[linebreak?
|
||||
(list lhs 'fill 'fill)]
|
||||
[(and sc (eq? style 'left-right/beside-side-conditions))
|
||||
(list lhs =-pict (htl-append 10 rhs sc))]
|
||||
[else
|
||||
(list lhs =-pict rhs)]))
|
||||
(if linebreak?
|
||||
(list
|
||||
(list (htl-append sep =-pict rhs)
|
||||
'fill
|
||||
'fill))
|
||||
null)
|
||||
(if (or (not sc)
|
||||
(and (not linebreak?)
|
||||
(eq? style 'left-right/beside-side-conditions)))
|
||||
null
|
||||
(list
|
||||
(list sc 'fill 'fill)))))
|
||||
lhss
|
||||
scs
|
||||
rhss
|
||||
linebreak-list)))
|
||||
ltl-superimpose ltl-superimpose
|
||||
sep sep)]
|
||||
[(vertical)
|
||||
(apply vl-append
|
||||
sep
|
||||
(apply append
|
||||
(map (lambda (lhs sc rhs)
|
||||
(cons
|
||||
(vl-append (htl-append lhs =-pict) rhs)
|
||||
(if (not sc)
|
||||
null
|
||||
(list sc))))
|
||||
lhss
|
||||
scs
|
||||
rhss)))])))
|
||||
lhss rhss linebreak-list))))
|
||||
(define scs (for/list ([eqn (in-list eqns)])
|
||||
(let ([scs (reverse (list-ref eqn 1))])
|
||||
(if (null? scs)
|
||||
#f
|
||||
(let-values ([(fresh where/sc) (partition metafunc-extra-fresh? scs)])
|
||||
(side-condition-pict (foldl (λ (clause picts)
|
||||
(foldr (λ (l ps) (cons (wrapper->pict l) ps))
|
||||
picts (metafunc-extra-fresh-vars clause)))
|
||||
'() fresh)
|
||||
(map (match-lambda
|
||||
[(struct metafunc-extra-where (lhs rhs))
|
||||
(where-pict (wrapper->pict lhs) (wrapper->pict rhs))]
|
||||
[(struct metafunc-extra-side-cond (expr))
|
||||
(wrapper->pict expr)])
|
||||
where/sc)
|
||||
(cond
|
||||
[vertical-side-conditions?
|
||||
;; maximize line breaks:
|
||||
0]
|
||||
[compact-side-conditions?
|
||||
;; maximize line break as needed:
|
||||
max-line-w/pre-sc]
|
||||
[else
|
||||
;; no line breaks:
|
||||
+inf.0])))))))
|
||||
(case mode
|
||||
[(horizontal)
|
||||
(define (adjust-for-fills rows)
|
||||
;; Some rows have the form (list <pict> 'fill 'fill),
|
||||
;; in which case we want the <pict> to span all columns.
|
||||
;; To do that, we need to know the total width of the first
|
||||
;; two columns of non-spanning rows.
|
||||
(define max-w-before-rhs (apply
|
||||
max
|
||||
(map (lambda (row)
|
||||
(match row
|
||||
[(list lhs 'fill 'fill)
|
||||
(+ sep sep)]
|
||||
[else
|
||||
(+ (pict-width (car row))
|
||||
sep
|
||||
(pict-width (cadr row))
|
||||
sep)]))
|
||||
rows)))
|
||||
(apply
|
||||
append
|
||||
(map (lambda (row)
|
||||
(match row
|
||||
[(list lhs 'fill 'fill)
|
||||
(list
|
||||
;; pretend that content is zero-width:
|
||||
(inset lhs 0 0 (- (pict-width lhs)) 0)
|
||||
(blank)
|
||||
;; blank that's wide enough to ensure that the
|
||||
;; right column covers the spanning pict
|
||||
;; (and no more)
|
||||
(blank (max 0 (- (pict-width lhs) max-w-before-rhs))
|
||||
0))]
|
||||
[else row]))
|
||||
rows)))
|
||||
(table 3
|
||||
(adjust-for-fills
|
||||
(apply append
|
||||
(map (lambda (lhs sc rhs linebreak?)
|
||||
(append
|
||||
(list
|
||||
(cond
|
||||
[linebreak?
|
||||
(list lhs 'fill 'fill)]
|
||||
[(and sc (eq? style 'left-right/beside-side-conditions))
|
||||
(list lhs =-pict (htl-append 10 rhs sc))]
|
||||
[else
|
||||
(list lhs =-pict rhs)]))
|
||||
(if linebreak?
|
||||
(list
|
||||
(list (htl-append sep =-pict rhs)
|
||||
'fill
|
||||
'fill))
|
||||
null)
|
||||
(if (or (not sc)
|
||||
(and (not linebreak?)
|
||||
(eq? style 'left-right/beside-side-conditions)))
|
||||
null
|
||||
(list
|
||||
(list sc 'fill 'fill)))))
|
||||
lhss
|
||||
scs
|
||||
rhss
|
||||
linebreak-list)))
|
||||
ltl-superimpose ltl-superimpose
|
||||
sep sep)]
|
||||
[(vertical)
|
||||
(apply vl-append
|
||||
sep
|
||||
(apply append
|
||||
(map (lambda (lhs sc rhs)
|
||||
(cons
|
||||
(vl-append (htl-append lhs =-pict) rhs)
|
||||
(if (not sc)
|
||||
null
|
||||
(list sc))))
|
||||
lhss
|
||||
scs
|
||||
rhss)))]))
|
||||
|
||||
(define (metafunction-call name an-lw)
|
||||
(struct-copy lw an-lw
|
||||
|
|
|
|||
|
|
@ -1174,6 +1174,34 @@
|
|||
defs))
|
||||
(syntax defs))))))]))
|
||||
|
||||
(define-for-syntax (extract-clause-names stuffss)
|
||||
(for/list ([stuffs (in-list (syntax->list stuffss))])
|
||||
(define the-clause-name #f)
|
||||
(define stuff-without-clause-name
|
||||
(for/fold ([stuffs '()]) ([stuff+name (in-list (syntax->list stuffs))])
|
||||
(syntax-case* stuff+name (clause-name) (λ (x y) (eq? (syntax-e x) (syntax-e y)))
|
||||
[(clause-name id)
|
||||
(begin
|
||||
(unless (or (identifier? #'id)
|
||||
(string? (syntax-e #'id)))
|
||||
(raise-syntax-error 'define-metafunction
|
||||
"expected an identifier or a string"
|
||||
#'id))
|
||||
(when the-clause-name
|
||||
(raise-syntax-error 'define-metafunction
|
||||
"multiple names in a single clause"
|
||||
#f
|
||||
#f
|
||||
(list the-clause-name #'id)))
|
||||
(set! the-clause-name #'id)
|
||||
stuffs)]
|
||||
[_ (cons stuff+name stuffs)])))
|
||||
(cons (cond
|
||||
[(not the-clause-name) #f]
|
||||
[(identifier? the-clause-name) (symbol->string (syntax-e the-clause-name))]
|
||||
[else the-clause-name])
|
||||
(reverse stuff-without-clause-name))))
|
||||
|
||||
(define-syntax (generate-metafunction stx)
|
||||
(syntax-case stx ()
|
||||
[(_ orig-stx lang prev-metafunction name name-predicate dom-ctcs codom-contracts pats syn-error-name)
|
||||
|
|
@ -1186,152 +1214,154 @@
|
|||
(definition-nts #'lang #'orig-stx syn-error-name))
|
||||
(with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
|
||||
[(lhs-for-lw ...) (lhs-lws pats)])
|
||||
(with-syntax ([((rhs stuff ...) ...) #'((raw-rhses ...) ...)]
|
||||
(with-syntax ([((rhs stuff+names ...) ...) #'((raw-rhses ...) ...)]
|
||||
[(lhs ...) #'((lhs-clauses ...) ...)])
|
||||
(parse-extras #'((stuff ...) ...))
|
||||
(with-syntax ([((side-conditions-rewritten lhs-names lhs-namess/ellipses) ...)
|
||||
(map (λ (x) (rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
syn-error-name
|
||||
#t
|
||||
x))
|
||||
(syntax->list (syntax (lhs ...))))])
|
||||
(with-syntax ([(rhs/wheres ...)
|
||||
(map (λ (sc/b rhs names names/ellipses)
|
||||
(bind-withs
|
||||
syn-error-name '()
|
||||
#'effective-lang lang-nts
|
||||
sc/b 'flatten
|
||||
#`(list (term #,rhs #:lang lang))
|
||||
(syntax->list names)
|
||||
(syntax->list names/ellipses)
|
||||
#t
|
||||
#f))
|
||||
(syntax->list #'((stuff ...) ...))
|
||||
(syntax->list #'(rhs ...))
|
||||
(syntax->list #'(lhs-names ...))
|
||||
(syntax->list #'(lhs-namess/ellipses ...)))]
|
||||
[(rg-rhs/wheres ...)
|
||||
(map (λ (sc/b rhs names names/ellipses)
|
||||
(bind-withs
|
||||
syn-error-name '()
|
||||
#'effective-lang lang-nts
|
||||
sc/b 'predicate
|
||||
#`#t
|
||||
(syntax->list names)
|
||||
(syntax->list names/ellipses)
|
||||
#t
|
||||
#f))
|
||||
(syntax->list #'((stuff ...) ...))
|
||||
(syntax->list #'(rhs ...))
|
||||
(syntax->list #'(lhs-names ...))
|
||||
(syntax->list #'(lhs-namess/ellipses ...)))])
|
||||
(with-syntax ([((rg-side-conditions-rewritten rg-names rg-names/ellipses ...) ...)
|
||||
(map (λ (x) (rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
syn-error-name
|
||||
#t
|
||||
x))
|
||||
(syntax->list (syntax ((side-condition lhs rg-rhs/wheres) ...))))]
|
||||
[(clause-src ...)
|
||||
(map (λ (lhs)
|
||||
(format "~a:~a:~a"
|
||||
(and (path? (syntax-source lhs))
|
||||
(path->relative-string/library (syntax-source lhs)))
|
||||
(syntax-line lhs)
|
||||
(syntax-column lhs)))
|
||||
pats)]
|
||||
[(dom-side-conditions-rewritten dom-names dom-names/ellipses)
|
||||
(if dom-ctcs
|
||||
(rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
syn-error-name
|
||||
#f
|
||||
dom-ctcs)
|
||||
#'(any () ()))]
|
||||
[((codom-side-conditions-rewritten codom-names codom-names/ellipses) ...)
|
||||
(map (λ (codom-contract)
|
||||
(rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
syn-error-name
|
||||
#f
|
||||
codom-contract))
|
||||
codom-contracts)]
|
||||
[(rhs-fns ...)
|
||||
(map (λ (names names/ellipses rhs/where)
|
||||
(with-syntax ([(names ...) names]
|
||||
[(names/ellipses ...) names/ellipses]
|
||||
[rhs/where rhs/where])
|
||||
(syntax
|
||||
(λ (name bindings)
|
||||
(term-let-fn ((name name))
|
||||
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
|
||||
rhs/where))))))
|
||||
(with-syntax ([((clause-name stuff ...) ...) (extract-clause-names #'((stuff+names ...) ...))])
|
||||
(parse-extras #'((stuff ...) ...))
|
||||
(with-syntax ([((side-conditions-rewritten lhs-names lhs-namess/ellipses) ...)
|
||||
(map (λ (x) (rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
syn-error-name
|
||||
#t
|
||||
x))
|
||||
(syntax->list (syntax (lhs ...))))])
|
||||
(with-syntax ([(rhs/wheres ...)
|
||||
(map (λ (sc/b rhs names names/ellipses)
|
||||
(bind-withs
|
||||
syn-error-name '()
|
||||
#'effective-lang lang-nts
|
||||
sc/b 'flatten
|
||||
#`(list (term #,rhs #:lang lang))
|
||||
(syntax->list names)
|
||||
(syntax->list names/ellipses)
|
||||
#t
|
||||
#f))
|
||||
(syntax->list #'((stuff ...) ...))
|
||||
(syntax->list #'(rhs ...))
|
||||
(syntax->list #'(lhs-names ...))
|
||||
(syntax->list #'(lhs-namess/ellipses ...))
|
||||
(syntax->list (syntax (rhs/wheres ...))))]
|
||||
[((gen-clause lhs-pat) ...)
|
||||
(make-mf-clauses (syntax->list #'(lhs ...))
|
||||
(syntax->list #'(rhs ...))
|
||||
(syntax->list #'((stuff ...) ...))
|
||||
lang-nts syn-error-name #'name #'lang)])
|
||||
(syntax-property
|
||||
(prune-syntax
|
||||
#`(let ([sc `(side-conditions-rewritten ...)]
|
||||
[dsc `dom-side-conditions-rewritten])
|
||||
(let ([cases (map (λ (pat rhs-fn rg-lhs src)
|
||||
(make-metafunc-case
|
||||
(λ (effective-lang) (compile-pattern effective-lang pat #t))
|
||||
rhs-fn
|
||||
rg-lhs src (gensym)))
|
||||
sc
|
||||
(list (λ (effective-lang) rhs-fns) ...)
|
||||
(list (λ (effective-lang) `rg-side-conditions-rewritten) ...)
|
||||
`(clause-src ...))]
|
||||
[parent-cases
|
||||
#,(if prev-metafunction
|
||||
#`(metafunc-proc-cases #,(term-fn-get-id (syntax-local-value prev-metafunction)))
|
||||
#'null)]
|
||||
[new-lhs-pats '(lhs-pat ...)])
|
||||
(build-metafunction
|
||||
lang
|
||||
cases
|
||||
parent-cases
|
||||
(λ (f/dom)
|
||||
(make-metafunc-proc
|
||||
(let ([name (lambda (x) (f/dom x))]) name)
|
||||
(generate-lws #f
|
||||
(lhs ...)
|
||||
(lhs-for-lw ...)
|
||||
((stuff ...) ...)
|
||||
(rhs ...)
|
||||
#t)
|
||||
lang
|
||||
#t ;; multi-args?
|
||||
'name
|
||||
(let ([name (lambda (x) (name-predicate x))]) name)
|
||||
dsc
|
||||
(append cases parent-cases)
|
||||
#,(cond
|
||||
[prev-metafunction
|
||||
#`(extend-mf-clauses #,(term-fn-get-id (syntax-local-value prev-metafunction))
|
||||
(λ ()
|
||||
#,(check-pats #'(list gen-clause ...)))
|
||||
new-lhs-pats)]
|
||||
[else
|
||||
#`(memoize0
|
||||
(λ ()
|
||||
#,(check-pats #'(list gen-clause ...))))])
|
||||
#,(if prev-metafunction
|
||||
#`(extend-lhs-pats #,(term-fn-get-id (syntax-local-value prev-metafunction))
|
||||
new-lhs-pats)
|
||||
#`new-lhs-pats)))
|
||||
#,(if dom-ctcs #'dsc #f)
|
||||
`(codom-side-conditions-rewritten ...)
|
||||
'name))))
|
||||
'disappeared-use
|
||||
(map syntax-local-introduce
|
||||
(syntax->list #'(original-names ...))))))))))]))
|
||||
(syntax->list #'(lhs-namess/ellipses ...)))]
|
||||
[(rg-rhs/wheres ...)
|
||||
(map (λ (sc/b rhs names names/ellipses)
|
||||
(bind-withs
|
||||
syn-error-name '()
|
||||
#'effective-lang lang-nts
|
||||
sc/b 'predicate
|
||||
#`#t
|
||||
(syntax->list names)
|
||||
(syntax->list names/ellipses)
|
||||
#t
|
||||
#f))
|
||||
(syntax->list #'((stuff ...) ...))
|
||||
(syntax->list #'(rhs ...))
|
||||
(syntax->list #'(lhs-names ...))
|
||||
(syntax->list #'(lhs-namess/ellipses ...)))])
|
||||
(with-syntax ([((rg-side-conditions-rewritten rg-names rg-names/ellipses ...) ...)
|
||||
(map (λ (x) (rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
syn-error-name
|
||||
#t
|
||||
x))
|
||||
(syntax->list (syntax ((side-condition lhs rg-rhs/wheres) ...))))]
|
||||
[(clause-src ...)
|
||||
(map (λ (lhs)
|
||||
(format "~a:~a:~a"
|
||||
(and (path? (syntax-source lhs))
|
||||
(path->relative-string/library (syntax-source lhs)))
|
||||
(syntax-line lhs)
|
||||
(syntax-column lhs)))
|
||||
pats)]
|
||||
[(dom-side-conditions-rewritten dom-names dom-names/ellipses)
|
||||
(if dom-ctcs
|
||||
(rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
syn-error-name
|
||||
#f
|
||||
dom-ctcs)
|
||||
#'(any () ()))]
|
||||
[((codom-side-conditions-rewritten codom-names codom-names/ellipses) ...)
|
||||
(map (λ (codom-contract)
|
||||
(rewrite-side-conditions/check-errs
|
||||
lang-nts
|
||||
syn-error-name
|
||||
#f
|
||||
codom-contract))
|
||||
codom-contracts)]
|
||||
[(rhs-fns ...)
|
||||
(map (λ (names names/ellipses rhs/where)
|
||||
(with-syntax ([(names ...) names]
|
||||
[(names/ellipses ...) names/ellipses]
|
||||
[rhs/where rhs/where])
|
||||
(syntax
|
||||
(λ (name bindings)
|
||||
(term-let-fn ((name name))
|
||||
(term-let ([names/ellipses (lookup-binding bindings 'names)] ...)
|
||||
rhs/where))))))
|
||||
(syntax->list #'(lhs-names ...))
|
||||
(syntax->list #'(lhs-namess/ellipses ...))
|
||||
(syntax->list (syntax (rhs/wheres ...))))]
|
||||
[((gen-clause lhs-pat) ...)
|
||||
(make-mf-clauses (syntax->list #'(lhs ...))
|
||||
(syntax->list #'(rhs ...))
|
||||
(syntax->list #'((stuff ...) ...))
|
||||
lang-nts syn-error-name #'name #'lang)])
|
||||
(syntax-property
|
||||
(prune-syntax
|
||||
#`(let ([sc `(side-conditions-rewritten ...)]
|
||||
[dsc `dom-side-conditions-rewritten])
|
||||
(let ([cases (map (λ (pat rhs-fn rg-lhs src)
|
||||
(make-metafunc-case
|
||||
(λ (effective-lang) (compile-pattern effective-lang pat #t))
|
||||
rhs-fn
|
||||
rg-lhs src (gensym)))
|
||||
sc
|
||||
(list (λ (effective-lang) rhs-fns) ...)
|
||||
(list (λ (effective-lang) `rg-side-conditions-rewritten) ...)
|
||||
`(clause-src ...))]
|
||||
[parent-cases
|
||||
#,(if prev-metafunction
|
||||
#`(metafunc-proc-cases #,(term-fn-get-id (syntax-local-value prev-metafunction)))
|
||||
#'null)]
|
||||
[new-lhs-pats '(lhs-pat ...)])
|
||||
(build-metafunction
|
||||
lang
|
||||
cases
|
||||
parent-cases
|
||||
(λ (f/dom)
|
||||
(make-metafunc-proc
|
||||
(let ([name (lambda (x) (f/dom x))]) name)
|
||||
'(clause-name ...)
|
||||
(generate-lws #f
|
||||
(lhs ...)
|
||||
(lhs-for-lw ...)
|
||||
((stuff ...) ...)
|
||||
(rhs ...)
|
||||
#t)
|
||||
lang
|
||||
#t ;; multi-args?
|
||||
'name
|
||||
(let ([name (lambda (x) (name-predicate x))]) name)
|
||||
dsc
|
||||
(append cases parent-cases)
|
||||
#,(cond
|
||||
[prev-metafunction
|
||||
#`(extend-mf-clauses #,(term-fn-get-id (syntax-local-value prev-metafunction))
|
||||
(λ ()
|
||||
#,(check-pats #'(list gen-clause ...)))
|
||||
new-lhs-pats)]
|
||||
[else
|
||||
#`(memoize0
|
||||
(λ ()
|
||||
#,(check-pats #'(list gen-clause ...))))])
|
||||
#,(if prev-metafunction
|
||||
#`(extend-lhs-pats #,(term-fn-get-id (syntax-local-value prev-metafunction))
|
||||
new-lhs-pats)
|
||||
#`new-lhs-pats)))
|
||||
#,(if dom-ctcs #'dsc #f)
|
||||
`(codom-side-conditions-rewritten ...)
|
||||
'name))))
|
||||
'disappeared-use
|
||||
(map syntax-local-introduce
|
||||
(syntax->list #'(original-names ...)))))))))))]))
|
||||
|
||||
(define (extend-lhs-pats old-m new-pats)
|
||||
(append new-pats (metafunc-proc-lhs-pats old-m)))
|
||||
|
|
@ -1443,7 +1473,7 @@
|
|||
#'form-name))]
|
||||
[_
|
||||
(raise-syntax-error 'define-metafunction
|
||||
"expected a side-condition or where clause"
|
||||
"expected a side-condition, where, or clause-name"
|
||||
stuff)]))
|
||||
(syntax->list stuffs)))
|
||||
(syntax->list extras)))
|
||||
|
|
@ -2313,6 +2343,7 @@
|
|||
metafunction? metafunction-proc
|
||||
in-domain?
|
||||
metafunc-proc-lang
|
||||
metafunc-proc-clause-names
|
||||
metafunc-proc-pict-info
|
||||
metafunc-proc-name
|
||||
metafunc-proc-multi-arg?
|
||||
|
|
|
|||
|
|
@ -13,6 +13,7 @@
|
|||
defined-check
|
||||
not-expression-context
|
||||
|
||||
metafunc-proc-clause-names
|
||||
metafunc-proc-pict-info
|
||||
metafunc-proc-lang
|
||||
metafunc-proc-multi-arg?
|
||||
|
|
@ -72,13 +73,14 @@
|
|||
variable-not-otherwise-mentioned hole symbol))
|
||||
|
||||
(define-values (struct:metafunc-proc make-metafunc-proc metafunc-proc? metafunc-proc-ref metafunc-proc-set!)
|
||||
(make-struct-type 'metafunc-proc #f 10 0 #f null (current-inspector) 0))
|
||||
(define metafunc-proc-pict-info (make-struct-field-accessor metafunc-proc-ref 1))
|
||||
(define metafunc-proc-lang (make-struct-field-accessor metafunc-proc-ref 2))
|
||||
(define metafunc-proc-multi-arg? (make-struct-field-accessor metafunc-proc-ref 3))
|
||||
(define metafunc-proc-name (make-struct-field-accessor metafunc-proc-ref 4))
|
||||
(define metafunc-proc-in-dom? (make-struct-field-accessor metafunc-proc-ref 5))
|
||||
(define metafunc-proc-dom-pat (make-struct-field-accessor metafunc-proc-ref 6))
|
||||
(define metafunc-proc-cases (make-struct-field-accessor metafunc-proc-ref 7))
|
||||
(define metafunc-proc-gen-clauses (make-struct-field-accessor metafunc-proc-ref 8))
|
||||
(define metafunc-proc-lhs-pats (make-struct-field-accessor metafunc-proc-ref 9))
|
||||
(make-struct-type 'metafunc-proc #f 11 0 #f null (current-inspector) 0))
|
||||
(define metafunc-proc-clause-names (make-struct-field-accessor metafunc-proc-ref 1))
|
||||
(define metafunc-proc-pict-info (make-struct-field-accessor metafunc-proc-ref 2))
|
||||
(define metafunc-proc-lang (make-struct-field-accessor metafunc-proc-ref 3))
|
||||
(define metafunc-proc-multi-arg? (make-struct-field-accessor metafunc-proc-ref 4))
|
||||
(define metafunc-proc-name (make-struct-field-accessor metafunc-proc-ref 5))
|
||||
(define metafunc-proc-in-dom? (make-struct-field-accessor metafunc-proc-ref 6))
|
||||
(define metafunc-proc-dom-pat (make-struct-field-accessor metafunc-proc-ref 7))
|
||||
(define metafunc-proc-cases (make-struct-field-accessor metafunc-proc-ref 8))
|
||||
(define metafunc-proc-gen-clauses (make-struct-field-accessor metafunc-proc-ref 9))
|
||||
(define metafunc-proc-lhs-pats (make-struct-field-accessor metafunc-proc-ref 10))
|
||||
|
|
|
|||
|
|
@ -1092,7 +1092,8 @@ reduce it further).
|
|||
(where pat @#,tttterm)
|
||||
(where/hidden pat @#,tttterm)
|
||||
(judgment-holds
|
||||
(judgment-form-id pat/term ...))])]{
|
||||
(judgment-form-id pat/term ...))
|
||||
(clause-name name)])]{
|
||||
|
||||
The @racket[define-metafunction] form builds a function on
|
||||
sexpressions according to the pattern and right-hand-side
|
||||
|
|
@ -1109,6 +1110,23 @@ no clauses match, if one of the clauses matches multiple ways
|
|||
(and that leads to different results for the different matches),
|
||||
or if the contract is violated.
|
||||
|
||||
The @racket[side-condition] extra is evaluated after a successful match
|
||||
to the corresponding argument pattern. If it returns @racket[#f],
|
||||
the clause is considered not to have matched, and the next one is tried.
|
||||
The @racket[side-condition/hidden] extra behaves the same, but is
|
||||
not typeset.
|
||||
|
||||
The @racket[where] and @racket[where/hidden] extra are like
|
||||
@racket[side-condition] and @racket[side-condition/hidden],
|
||||
except the match guards the clause.
|
||||
|
||||
The @racket[judgment-holds] clause is like @racket[side-condition]
|
||||
and @racket[where], except the given judgment must hold for the
|
||||
clause to be taken.
|
||||
|
||||
The @racket[clause-name] is used only when typesetting. See
|
||||
@racket[metafunction-cases].
|
||||
|
||||
Note that metafunctions are assumed to always return the same results
|
||||
for the same inputs, and their results are cached, unless
|
||||
@racket[caching-enabled?] is set to @racket[#f]. Accordingly, if a
|
||||
|
|
@ -2704,15 +2722,18 @@ precede ellipses that represent argument sequences; when it is
|
|||
|
||||
@defparam[metafunction-cases
|
||||
cases
|
||||
(or/c #f (and/c (listof (and/c integer?
|
||||
(or/c zero? positive?)))
|
||||
(or/c #f (and/c (listof (or/c exact-nonnegative-integer?
|
||||
string?))
|
||||
pair?))]{
|
||||
|
||||
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]).
|
||||
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, then only
|
||||
the selected cases appear. The numbers indicate the cases counting from
|
||||
@racket[0] and the strings indicate cases named with @racket[clause-name].
|
||||
|
||||
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].
|
||||
only in the case that @racket[judgment-form-cases] is @racket[#f] (and in that
|
||||
case, only the numbers are used).
|
||||
}
|
||||
|
||||
@defparam[judgment-form-cases
|
||||
|
|
|
|||
|
|
@ -114,7 +114,8 @@
|
|||
(define-metafunction lang
|
||||
[(T x y)
|
||||
1
|
||||
(side-condition (not (eq? (term x) (term y))))]
|
||||
(side-condition (not (eq? (term x) (term y))))
|
||||
(clause-name first-one)]
|
||||
[(T x x)
|
||||
(any_1 any_2)
|
||||
(where any_1 2)
|
||||
|
|
@ -123,7 +124,9 @@
|
|||
;; in this test, the metafunction has 2 clauses
|
||||
;; with a side-condition on the first clause
|
||||
;; and a 'where' in the second clause
|
||||
(btest (render-metafunction T) "metafunction-T.png")
|
||||
(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
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user