diff --git a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl index 433d7c0ea9..350c9356cc 100644 --- a/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl +++ b/pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl @@ -1122,7 +1122,8 @@ reduce it further). (where/hidden pat @#,tttterm) (judgment-holds (judgment-form-id pat/term ...)) - (clause-name name)])]{ + (clause-name name) + (code:line or @#,tttterm)])]{ The @racket[define-metafunction] form builds a function on sexpressions according to the pattern and right-hand-side @@ -1219,8 +1220,19 @@ ensures that there is a unique match for that case. Without it, @racket[(term (- (x x) x))] would lead to an ambiguous match. -@history[#:changed "1.4" @list{Added @racket[#:post] conditions.}] +The @racket[or] clause is used to define a form of conditional +right-hand side of a metafunction. In particular, if any of the +@racket[where] or @racket[side-condition] clauses fail, then +evaluation continues after an @racket[or] clause, treating the +term that follows as the result (subject to any subsequent +@racket[where] clauses or @racket[side-condition]s. This construction +is equivalent to simply duplicating the left-hand side of the +clause, once for each @racket[or] expression, but signals to +the typesetting library to use a large left curly brace to group +the conditions in the @racket[or]. +@history[#:changed "1.4" @list{Added @racket[#:post] conditions.}] + #:changed "1.5" @list{Added @racket[or] clauses.}] } @defform[(define-metafunction/extension f language diff --git a/pkgs/redex-pkgs/redex-lib/info.rkt b/pkgs/redex-pkgs/redex-lib/info.rkt index c70f0fde7b..ec0f331e2d 100644 --- a/pkgs/redex-pkgs/redex-lib/info.rkt +++ b/pkgs/redex-pkgs/redex-lib/info.rkt @@ -18,4 +18,4 @@ (define pkg-authors '(robby bfetscher)) -(define version "1.4") +(define version "1.5") diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt index ae731ba84e..ecf57142c1 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt @@ -1109,7 +1109,8 @@ (define-syntax (generate-lws stx) (syntax-case stx () - [(_ relation? seq-of-lhs seq-of-lhs-for-lw seq-of-tl-side-cond/binds seq-of-rhs side-condition-unquoted?) + [(_ relation? seq-of-lhs seq-of-lhs-for-lw seq-of-tl-side-cond/binds seq-of-rhs + side-condition-unquoted?) (with-syntax ([(rhs/lw ...) (syntax-case #'relation? () @@ -1121,55 +1122,61 @@ (map name-pattern-lws (syntax->list #'seq-of-lhs))] [((where/sc/lw ...) ...) ;; Also for pict, extract where bindings - (map (λ (hm) - (map - (λ (lst) - (syntax-case lst (unquote side-condition where) - [(form-name . _) - (judgment-form-id? #'form-name) - #`(make-metafunc-extra-side-cond #,(to-lw/proc lst))] - [(form-name . _) - (judgment-form-id? #'form-name) - #`(make-metafunc-extra-side-cond #,(to-lw/proc lst))] - [(where pat (unquote (f _ _))) - (and (or (identifier? #'pat) - (let ([l (syntax->list #'pat)]) - (and l (andmap identifier? (syntax->list #'pat))))) - (or (free-identifier=? #'f #'variable-not-in) - (free-identifier=? #'f #'variables-not-in))) - (with-syntax ([(ids ...) - (map to-lw/proc - (if (identifier? #'pat) - (list #'pat) - (syntax->list #'pat)))]) - #`(make-metafunc-extra-fresh - (list ids ...)))] - [(where pat exp) - #`(make-metafunc-extra-where - #,(to-lw/proc #'pat) #,(to-lw/proc #'exp))] - [(side-condition x) - #`(make-metafunc-extra-side-cond - #,(if (syntax-e #'side-condition-unquoted?) - (to-lw/uq/proc #'x) - (to-lw/proc #'x)))] - [maybe-ellipsis - (ellipsis? #'maybe-ellipsis) - (to-lw/proc #'maybe-ellipsis)])) - (visible-extras hm))) - (syntax->list #'seq-of-tl-side-cond/binds))] + (for/list ([hm (in-list (syntax->list #'seq-of-tl-side-cond/binds))]) + (define the-extras (visible-extras hm)) + (for/list ([lst (in-list the-extras)] + [next (if (null? the-extras) + '() + (append (cdr the-extras) (list #f)))]) + (syntax-case next (or) + [or (to-lw/proc lst)] + [else + (syntax-case lst (unquote side-condition where or) + [(form-name . _) + (judgment-form-id? #'form-name) + #`(make-metafunc-extra-side-cond #,(to-lw/proc lst))] + [(form-name . _) + (judgment-form-id? #'form-name) + #`(make-metafunc-extra-side-cond #,(to-lw/proc lst))] + [(where pat (unquote (f _ _))) + (and (or (identifier? #'pat) + (let ([l (syntax->list #'pat)]) + (and l (andmap identifier? (syntax->list #'pat))))) + (or (free-identifier=? #'f #'variable-not-in) + (free-identifier=? #'f #'variables-not-in))) + (with-syntax ([(ids ...) + (map to-lw/proc + (if (identifier? #'pat) + (list #'pat) + (syntax->list #'pat)))]) + #`(make-metafunc-extra-fresh + (list ids ...)))] + [(where pat exp) + #`(make-metafunc-extra-where + #,(to-lw/proc #'pat) #,(to-lw/proc #'exp))] + [(side-condition x) + #`(make-metafunc-extra-side-cond + #,(if (syntax-e #'side-condition-unquoted?) + (to-lw/uq/proc #'x) + (to-lw/proc #'x)))] + [or ''or] + [(clause-name name) + #''(clause-name name)] + [maybe-ellipsis + (ellipsis? #'maybe-ellipsis) + (to-lw/proc #'maybe-ellipsis)])])))] [(((where-bind-id/lw . where-bind-pat/lw) ...) ...) - (map (λ (clauses) - (for/fold ([binds '()]) ([clause (visible-extras clauses)]) - (syntax-case clause (where) - [(form-name . pieces) - (judgment-form-id? #'form-name) - (let*-values ([(mode) (judgment-form-mode (lookup-judgment-form-id #'form-name))] - [(_ outs) (split-by-mode (syntax->list #'pieces) mode)]) - (for/fold ([binds binds]) ([out outs]) - (append (name-pattern-lws out) binds)))] - [(where lhs rhs) (append (name-pattern-lws #'lhs) binds)] - [_ binds]))) - (syntax->list #'seq-of-tl-side-cond/binds))] + (for/list ([clauses (in-list (syntax->list #'seq-of-tl-side-cond/binds))]) + (for/fold ([binds '()]) ([clause (visible-extras clauses)]) + (syntax-case clause (where) + [(form-name . pieces) + (judgment-form-id? #'form-name) + (let*-values ([(mode) (judgment-form-mode (lookup-judgment-form-id #'form-name))] + [(_ outs) (split-by-mode (syntax->list #'pieces) mode)]) + (for/fold ([binds binds]) ([out outs]) + (append (name-pattern-lws out) binds)))] + [(where lhs rhs) (append (name-pattern-lws #'lhs) binds)] + [_ binds])))] [(((rhs-bind-id/lw . rhs-bind-pat/lw/uq) ...) ...) ;; Also for pict, extract pattern bindings (map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/uq/proc (cdr x)))) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt index 51ff1473b8..c56c1e4d3c 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt @@ -1256,13 +1256,37 @@ (list the-clause-name #'id))) (set! the-clause-name #'id) stuffs)] - [_ (cons stuff+name 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-for-syntax (eliminate-metafunction-ors stx) + (define (is-not-or? x) + (syntax-case x (or) + [or #f] + [else #t])) + (apply + append + (for/list ([clause (in-list (syntax->list stx))]) + (syntax-case clause () + [(lhs . rhs+stuff) + (let () + (define split + (let loop ([lst (syntax->list #'rhs+stuff)]) + (define batch (takef lst is-not-or?)) + (cond + [(null? batch) '()] + [else + (define next (dropf lst is-not-or?)) + (if (pair? next) + (cons batch (loop (cdr next))) + (list batch))]))) + (map (λ (x) (cons #'lhs x)) split))])))) + (define-syntax (generate-metafunction stx) (syntax-case stx () [(_ orig-stx lang prev-metafunction-stx @@ -1288,11 +1312,17 @@ (define syn-error-name (syntax-e #'syn-error-name)) (define lang-nts (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 ([(((original-names lhs-clauses ...) raw-rhses ...) ...) + (eliminate-metafunction-ors #'pats-stx)] + [(lhs-for-lw ...) (lhs-lws pats)] + [(((_1 lhs-with-ors-intact ...) + rhs-with-ors-intact + stuff-with-ors-intact ...) ...) + pats]) (with-syntax ([((rhs stuff+names ...) ...) #'((raw-rhses ...) ...)] [(lhs ...) #'((lhs-clauses ...) ...)]) - (with-syntax ([((clause-name stuff ...) ...) (extract-clause-names #'((stuff+names ...) ...))]) + (with-syntax ([((clause-name stuff ...) ...) + (extract-clause-names #'((stuff+names ...) ...))]) (parse-extras #'((stuff ...) ...)) (with-syntax ([((syncheck-expr side-conditions-rewritten lhs-names lhs-namess/ellipses) ...) (map (λ (x) (rewrite-side-conditions/check-errs @@ -1345,7 +1375,7 @@ (path->relative-string/library (syntax-source lhs))) (syntax-line lhs) (syntax-column lhs))) - pats)] + (syntax->list #'(original-names ...)))] [(dom-syncheck-expr dom-side-conditions-rewritten (dom-names ...) dom-names/ellipses) @@ -1427,10 +1457,10 @@ ;; body of mf (generate-lws #f - (lhs ...) + ((lhs-with-ors-intact ...) ...) (lhs-for-lw ...) - ((stuff ...) ...) - (rhs ...) + ((stuff-with-ors-intact ...) ...) + (rhs-with-ors-intact ...) #t)) lang #t ;; multi-args? diff --git a/pkgs/redex-pkgs/redex-pict-lib/redex/private/core-layout.rkt b/pkgs/redex-pkgs/redex-pict-lib/redex/private/core-layout.rkt index 4cd6cb8814..8f312ded25 100644 --- a/pkgs/redex-pkgs/redex-pict-lib/redex/private/core-layout.rkt +++ b/pkgs/redex-pkgs/redex-pict-lib/redex/private/core-layout.rkt @@ -49,6 +49,10 @@ white-bracket-sizing apply-rewrites use-homemade-white-brackets + left-curly-bracket-upper-hook + left-curly-bracket-middle-piece + left-curly-bracket-lower-hook + curly-bracket-extension ;; for test suite build-lines diff --git a/pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt b/pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt index c9fe69cca3..6df8cee038 100644 --- a/pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt +++ b/pkgs/redex-pkgs/redex-pict-lib/redex/private/pict.rkt @@ -5,7 +5,8 @@ racket/match racket/pretty racket/set - (only-in racket/list drop-right last partition add-between) + (only-in racket/list drop-right last partition add-between + splitf-at) texpict/mrpict texpict/utils @@ -381,6 +382,9 @@ (define where-make-prefix-pict (make-parameter (lambda () (basic-text " where " (default-style))))) +(define otherwise-make-pict + (make-parameter (lambda () + (basic-text " otherwise" (default-style))))) (define (where-pict lhs rhs) ((where-combine) lhs rhs)) @@ -971,10 +975,7 @@ (define case-labels (map (λ (mf) (metafunc-proc-clause-names (metafunction-proc mf))) mfs)) (define eqns (select-mf-cases contracts all-eqns case-labels)) (define lhs/contracts (select-mf-cases contracts all-lhss case-labels)) - (define rhss (for/list ([eqn/contract (in-list eqns)]) - (if (pict? eqn/contract) - 'contract - (wrapper->pict (list-ref eqn/contract 2))))) + (unless (or (not current-linebreaks) (= (length current-linebreaks) (length eqns))) (error 'metafunction->pict @@ -1006,6 +1007,104 @@ (memq style '(up-down/compact-side-conditions left-right/compact-side-conditions left-right*/compact-side-conditions))) + + (define (handle-single-side-condition scs) + (define-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) + (filter + values + (for/list ([thing (in-list where/sc)]) + (match thing + [(struct metafunc-extra-where (lhs rhs)) + (where-pict (wrapper->pict lhs) (wrapper->pict rhs))] + [(struct metafunc-extra-side-cond (expr)) + (wrapper->pict expr)] + [`(clause-name ,n) #f]))) + (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]))) + + (define (build-brace-based-rhs stuff) + (define conds + (let loop ([stuff stuff]) + (define-values (before after) (splitf-at stuff (λ (x) (not (equal? x 'or))))) + (if (null? after) + (list before) + (cons before (loop (cdr after)))))) + (define last-line (- (length conds) 1)) + (define rhs+scs (for/list ([cond-line (in-list conds)] + [i (in-naturals)]) + (define rhs (wrapper->pict (car cond-line))) + (define scs + (if (and (= last-line i) (null? (cdr cond-line))) + ((otherwise-make-pict)) + (handle-single-side-condition (cdr cond-line)))) + (list rhs scs))) + (define rhs (map car rhs+scs)) + (define scs (map cadr rhs+scs)) + (define widest-rhs (apply max 0 (map pict-width rhs))) + (define widest-scs (apply max 0 (map pict-width scs))) + (add-left-brace + (apply vl-append + 2 + (for/list ([rhs (in-list rhs)] + [scs (in-list scs)]) + (htl-append (lbl-superimpose + rhs + (blank widest-rhs 0)) + (lbl-superimpose + scs + (blank widest-scs 0))))))) + + (define (add-left-brace pict) + (let loop ([i 0]) + (define extender + (apply + vl-append + (for/list ([_ (in-range i)]) + (basic-text curly-bracket-extension (default-style))))) + (define left-brace + (vl-append (basic-text left-curly-bracket-upper-hook (default-style)) + extender + (basic-text left-curly-bracket-middle-piece (default-style)) + extender + (basic-text left-curly-bracket-lower-hook (default-style)))) + (cond + [(< (pict-height pict) (pict-height left-brace)) + (define top-bottom-diff (- (pict-height left-brace) + (pict-height pict))) + (inset (refocus (hc-append left-brace pict) pict) + (pict-width left-brace) + (/ top-bottom-diff 2) + 0 + (/ top-bottom-diff 2))] + [else (loop (+ i 1))]))) + + (define rhss (for/list ([eqn/contract (in-list eqns)]) + (cond + [(pict? eqn/contract) + 'contract] + [else + (define sc-info (list-ref eqn/contract 1)) + (cond + [(member 'or sc-info) + (build-brace-based-rhs + (cons (list-ref eqn/contract 2) + (reverse sc-info)))] + [else + (wrapper->pict (list-ref eqn/contract 2))])]))) + (define max-line-w/pre-sc (and compact-side-conditions? (for/fold ([biggest 0]) ([lhs/contract (in-list lhs/contracts)] @@ -1029,6 +1128,7 @@ (pict-width rhs) (pict-width =-pict) (* 2 sep)))])))) + (define scs (for/list ([eqn (in-list eqns)]) (cond [(pict? eqn) #f] @@ -1036,29 +1136,8 @@ (define scs (reverse (list-ref eqn 1))) (cond [(null? scs) #f] - [else - (define-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]))])]))) + [(member 'or scs) #f] + [else (handle-single-side-condition scs)])]))) (case mode [(horizontal) (define (adjust-for-fills rows) diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/bitmap-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/bitmap-test.rkt index 120b958ff6..7a5a0d84b7 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/bitmap-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/bitmap-test.rkt @@ -182,7 +182,15 @@ [(TL 2) (a ,(term-let ((x (term 1))) (term x)) beside - below)]) + below)] + [(TL any) + 3333333333 + (where 3 any) + or + 2 + (where 2 any) + or + 0]) ;; this tests that term-let is sucked away properly ;; when the metafunction is rendered diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/bmps-macosx/metafunction-TL.png b/pkgs/redex-pkgs/redex-test/redex/tests/bmps-macosx/metafunction-TL.png index 38c3a3b1b3..4746e42812 100644 Binary files a/pkgs/redex-pkgs/redex-test/redex/tests/bmps-macosx/metafunction-TL.png and b/pkgs/redex-pkgs/redex-test/redex/tests/bmps-macosx/metafunction-TL.png differ diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/bmps-macosx/metafunctions-multiple.png b/pkgs/redex-pkgs/redex-test/redex/tests/bmps-macosx/metafunctions-multiple.png index d89e0455e2..441595ee3d 100644 Binary files a/pkgs/redex-pkgs/redex-test/redex/tests/bmps-macosx/metafunctions-multiple.png and b/pkgs/redex-pkgs/redex-test/redex/tests/bmps-macosx/metafunctions-multiple.png differ diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt index 3e94ca1d4f..9a5516d405 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/tl-test.rkt @@ -1305,6 +1305,24 @@ (test (term (f (a b c))) 3) (test (term (f (a b))) #f)) +(let () + ;; 'or' in metafunctions + (define-language L) + + (define-metafunction L + [(f any ...) + three + (where (any_1 any_2 any_3) (any ...)) + or + two + (where (any_1 any_2) (any ...)) + or + something-else]) + + (test (term (f a b c)) (term three)) + (test (term (f a b)) (term two)) + (test (term (f a)) (term something-else))) + ; ; ;