From 576272362b159815cd7458128d79f70ea089b5a9 Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Fri, 5 Aug 2011 07:18:35 -0500 Subject: [PATCH] Adds define-judgment-form form --- collects/redex/pict.rkt | 4 +- collects/redex/private/defined-checks.rkt | 17 + collects/redex/private/loc-wrapper-ct.rkt | 3 +- collects/redex/private/pict.rkt | 157 ++--- .../redex/private/reduction-semantics.rkt | 534 ++++++++++++++---- .../redex/private/rewrite-side-conditions.rkt | 8 +- collects/redex/private/term-fn.rkt | 17 +- collects/redex/private/term.rkt | 17 +- collects/redex/redex.scrbl | 216 +++++-- collects/redex/reduction-semantics.rkt | 2 + collects/redex/tests/bitmap-test.rkt | 100 +++- .../judgment-form-metafunction-where.png | Bin 0 -> 1487 bytes .../judgment-form-name-patterns.png | Bin 0 -> 3098 bytes .../judgment-form-not-rewritten.png | Bin 0 -> 2334 bytes .../bmps-macosx/judgment-form-rewritten.png | Bin 0 -> 1931 bytes .../tests/bmps-macosx/red-with-where-name.png | Bin 0 -> 2349 bytes collects/redex/tests/bmps-macosx/stlc.png | Bin 0 -> 4562 bytes .../judgment-form-contracts.rktd | 12 + .../judgment-form-undefined.rktd | 9 + collects/redex/tests/run-err-tests/term.rktd | 42 ++ collects/redex/tests/run-tests.rkt | 2 +- .../judgment-form-definition.rktd | 103 ++++ .../tests/syn-err-tests/judgment-holds.rktd | 3 + .../syn-err-tests/language-definition.rktd | 25 + .../metafunction-definition.rktd | 11 + .../redex/tests/syn-err-tests/redex-let.rktd | 3 + .../reduction-relation-definition.rktd | 126 +++++ .../syn-err-tests/relation-definition.rktd | 15 + collects/redex/tests/syn-err-tests/term.rktd | 8 + collects/redex/tests/term-test.rkt | 78 +-- collects/redex/tests/test-util.rkt | 129 +++-- collects/redex/tests/tl-test.rkt | 363 ++++++------ 32 files changed, 1496 insertions(+), 508 deletions(-) create mode 100644 collects/redex/private/defined-checks.rkt create mode 100644 collects/redex/tests/bmps-macosx/judgment-form-metafunction-where.png create mode 100644 collects/redex/tests/bmps-macosx/judgment-form-name-patterns.png create mode 100644 collects/redex/tests/bmps-macosx/judgment-form-not-rewritten.png create mode 100644 collects/redex/tests/bmps-macosx/judgment-form-rewritten.png create mode 100644 collects/redex/tests/bmps-macosx/red-with-where-name.png create mode 100644 collects/redex/tests/bmps-macosx/stlc.png create mode 100644 collects/redex/tests/run-err-tests/judgment-form-contracts.rktd create mode 100644 collects/redex/tests/run-err-tests/judgment-form-undefined.rktd create mode 100644 collects/redex/tests/run-err-tests/term.rktd create mode 100644 collects/redex/tests/syn-err-tests/judgment-form-definition.rktd create mode 100644 collects/redex/tests/syn-err-tests/judgment-holds.rktd create mode 100644 collects/redex/tests/syn-err-tests/language-definition.rktd create mode 100644 collects/redex/tests/syn-err-tests/metafunction-definition.rktd create mode 100644 collects/redex/tests/syn-err-tests/redex-let.rktd create mode 100644 collects/redex/tests/syn-err-tests/reduction-relation-definition.rktd create mode 100644 collects/redex/tests/syn-err-tests/relation-definition.rktd create mode 100644 collects/redex/tests/syn-err-tests/term.rktd diff --git a/collects/redex/pict.rkt b/collects/redex/pict.rkt index abb27d9d18..62c20874b1 100644 --- a/collects/redex/pict.rkt +++ b/collects/redex/pict.rkt @@ -48,10 +48,12 @@ (provide relation->pict metafunction->pict metafunctions->pict + judgment-form->pict render-relation render-metafunction - render-metafunctions) + render-metafunctions + render-judgment-form) (provide/contract [render-language-nts (parameter/c (or/c false/c (listof (or/c string? symbol?))))] diff --git a/collects/redex/private/defined-checks.rkt b/collects/redex/private/defined-checks.rkt new file mode 100644 index 0000000000..261866f2ab --- /dev/null +++ b/collects/redex/private/defined-checks.rkt @@ -0,0 +1,17 @@ +#lang racket/base + +(require "error.rkt") +(provide check-defined-lexical + check-defined-module) + +(define (check-defined-lexical value name desc) + (when (eq? (letrec ([x x]) x) value) + (report-undefined name desc))) + +(define (check-defined-module thunk name desc) + (with-handlers ([exn:fail:contract:variable? + (λ (_) (report-undefined name desc))]) + (thunk))) + +(define (report-undefined name desc) + (redex-error #f "~a ~s applied before its definition" desc name)) \ No newline at end of file diff --git a/collects/redex/private/loc-wrapper-ct.rkt b/collects/redex/private/loc-wrapper-ct.rkt index 52d330adfb..fd259c277e 100644 --- a/collects/redex/private/loc-wrapper-ct.rkt +++ b/collects/redex/private/loc-wrapper-ct.rkt @@ -61,7 +61,8 @@ [x (and (identifier? #'x) (and (syntax-transforming?) - (term-fn? (syntax-local-value #'x (λ () #f))))) + (or (term-fn? (syntax-local-value #'x (λ () #f))) + (judgment-form? (syntax-local-value #'x (λ () #f)))))) #`(make-lw '#,(syntax-e #'x) #,(syntax-line stx) diff --git a/collects/redex/private/pict.rkt b/collects/redex/private/pict.rkt index 0efb8b15e1..adfb89b40e 100644 --- a/collects/redex/private/pict.rkt +++ b/collects/redex/private/pict.rkt @@ -14,7 +14,8 @@ "matcher.rkt" "arrow.rkt" "core-layout.rkt") -(require (for-syntax racket/base)) +(require (for-syntax racket/base + "term-fn.rkt")) (provide render-term term->pict @@ -30,10 +31,12 @@ relation->pict metafunction->pict metafunctions->pict - + judgment-form->pict + render-relation render-metafunction render-metafunctions + render-judgment-form basic-text @@ -727,9 +730,9 @@ (define-syntax (relation->pict stx) (syntax-case stx () - [(_ name1) + [(form name1) (identifier? #'name1) - #'(relation->pict/proc (metafunction name1) 'relation->pict)])) + #'(inference-rules-pict/relation 'form (metafunction name1))])) (define-syntax (render-metafunctions stx) (syntax-case stx () @@ -753,12 +756,12 @@ (define-syntax (render-relation stx) (syntax-case stx () - [(_ name) + [(form name) (identifier? #'name) - #'(render-relation/proc (metafunction name) #f)] - [(_ name #:file filename) + #'(render-relation/proc 'form (metafunction name) #f)] + [(form name #:file filename) (identifier? #'name) - #'(render-relation/proc (metafunction name) filename)])) + #'(render-relation/proc 'form (metafunction name) filename)])) (define linebreaks (make-parameter #f)) @@ -813,8 +816,7 @@ (map (lambda (eqn) (wrapper->pict (metafunction-call (metafunc-proc-name (metafunction-proc mf)) - (list-ref eqn 0) - (metafunc-proc-multi-arg? (metafunction-proc mf))))) + (list-ref eqn 0)))) (metafunc-proc-pict-info (metafunction-proc mf)))) mfs))] [eqns (select-cases all-eqns)] @@ -927,56 +929,28 @@ scs rhss))))]))) -(define (metafunction-call name an-lw flattened?) - (if flattened? - (struct-copy lw an-lw - [e - (list* - ;; the first loc wrapper is just there to make the - ;; shape of this line be one that the apply-rewrites - ;; function (in core-layout.rkt) recognizes as a metafunction - (make-lw "(" - (lw-line an-lw) - 0 - (lw-column an-lw) - 0 - #f - #f) - (make-lw name - (lw-line an-lw) - 0 - (lw-column an-lw) - 0 - #f - #t) - (cdr (lw-e an-lw)))]) - - (build-lw - (list - (build-lw "(" - (lw-line an-lw) - 0 - (lw-column an-lw) - 0) - (make-lw name - (lw-line an-lw) - 0 - (lw-column an-lw) - 0 - #f - #t) - an-lw - (build-lw ")" - (+ (lw-line an-lw) - (lw-line-span an-lw)) - 0 - (+ (lw-column an-lw) - (lw-column-span an-lw)) - 0)) - (lw-line an-lw) - (lw-line-span an-lw) - (lw-column an-lw) - (lw-column-span an-lw)))) +(define (metafunction-call name an-lw) + (struct-copy lw an-lw + [e + (list* + ;; the first loc wrapper is just there to make the + ;; shape of this line be one that the apply-rewrites + ;; function (in core-layout.rkt) recognizes as a metafunction + (make-lw "(" + (lw-line an-lw) + 0 + (lw-column an-lw) + 0 + #f + #f) + (make-lw name + (lw-line an-lw) + 0 + (lw-column an-lw) + 0 + #f + #t) + (cdr (lw-e an-lw)))])) (define (add-commas-and-rewrite-parens eles) (let loop ([eles eles] @@ -1044,36 +1018,42 @@ (parameterize ([dc-for-text-size (make-object bitmap-dc% (make-object bitmap% 1 1))]) (metafunctions->pict/proc mfs name))])) -(define (render-relation/proc mf filename) +(define (render-relation/proc form mf filename) + (render-pict (λ () (inference-rules-pict/relation form mf)) + filename)) + +(define (inference-rules-pict/relation form mf) + (unless (metafunc-proc-relation? (metafunction-proc mf)) + (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)) + (metafunc-proc-lang (metafunction-proc mf)))) + +(define (render-pict make-pict filename) (cond [filename - (save-as-ps (λ () (relation->pict/proc mf 'render-reduction-relation)) - filename)] + (save-as-ps make-pict filename)] [else (parameterize ([dc-for-text-size (make-object bitmap-dc% (make-object bitmap% 1 1))]) - (relation->pict/proc mf 'render-reduction-relation))])) + (make-pict))])) - -(define (relation->pict/proc mf name) - (unless (metafunc-proc-relation? (metafunction-proc mf)) - (error name "expected relation as argument, got a metafunction")) - (let* ([all-nts (language-nts (metafunc-proc-lang (metafunction-proc mf)))] +(define (inference-rules-pict name all-eqns lang) + (let* ([all-nts (language-nts lang)] [wrapper->pict (lambda (lw) (lw->pict all-nts lw))] - [all-eqns (metafunc-proc-pict-info (metafunction-proc mf))] [all-conclusions (map (lambda (eqn) (wrapper->pict - (metafunction-call (metafunc-proc-name (metafunction-proc mf)) - (list-ref eqn 0) - (metafunc-proc-multi-arg? (metafunction-proc mf))))) - (metafunc-proc-pict-info (metafunction-proc mf)))] + (metafunction-call name (list-ref eqn 0)))) + all-eqns)] [eqns (select-cases all-eqns)] [conclusions (select-cases all-conclusions)] [premisess (map (lambda (eqn) (append (map wrapper->pict (list-ref eqn 2)) (map (match-lambda [(struct metafunc-extra-where (lhs rhs)) - (where-pict (wrapper->pict lhs) (wrapper->pict rhs))]) + (where-pict (wrapper->pict lhs) (wrapper->pict rhs))] + [(struct metafunc-extra-side-cond (expr)) + (wrapper->pict expr)]) (list-ref eqn 1)))) eqns)]) ((relation-clauses-combine) @@ -1091,6 +1071,33 @@ (define horizontal-bar-spacing (make-parameter 4)) (define relation-clauses-combine (make-parameter (λ (l) (apply vc-append 20 l)))) +(define-for-syntax (inference-rules-pict/judgment-form form-name) + (define jf (syntax-local-value form-name)) + (syntax-property + #`(inference-rules-pict '#,(judgment-form-name jf) + #,(judgment-form-lws jf) + #,(judgment-form-lang jf)) + 'disappeared-use + form-name)) + +(define-syntax (render-judgment-form stx) + (syntax-case stx () + [(_ form-name . opt-arg) + (if (judgment-form-id? #'form-name) + (let ([save-as (syntax-case #'opt-arg () + [() #'#f] + [(path) #'path])]) + #`(render-pict (λ () #,(inference-rules-pict/judgment-form #'form-name)) + #,save-as)) + (raise-syntax-error #f "expected a judgment form name" stx #'form-name))])) + +(define-syntax (judgment-form->pict stx) + (syntax-case stx () + [(_ form-name) + (if (judgment-form-id? #'form-name) + (inference-rules-pict/judgment-form #'form-name) + (raise-syntax-error #f "expected a judgment form name" stx #'form-name))])) + ; ; ; diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt index b2ad722df8..cb14524538 100644 --- a/collects/redex/private/reduction-semantics.rkt +++ b/collects/redex/private/reduction-semantics.rkt @@ -17,8 +17,11 @@ "term-fn.rkt" "underscore-allowed.rkt" syntax/boundmap + syntax/id-table scheme/base - (prefix-in pattern- scheme/match) + racket/list + racket/match + racket/syntax syntax/parse syntax/parse/experimental/contract syntax/name)) @@ -271,8 +274,51 @@ (with-syntax ([orig-stx stx]) (syntax/loc stx (do-reduction-relation orig-stx extend-reduction-relation orig-reduction-relation #t lang args ...)))])) +(define-for-syntax (where-keyword? id) + (or (free-identifier=? id #'where) + (free-identifier=? id #'where/hidden))) + +(define-for-syntax (split-by-mode xs mode) + (for/fold ([ins '()] [outs '()]) + ([x (reverse xs)] + [m (reverse mode)]) + (match m + ['I (values (cons x ins) outs)] + ['O (values ins (cons x outs))]))) + +(define-for-syntax (generate-binding-constraints names names/ellipses bindings syn-err-name) + (define (id/depth stx) + (syntax-case stx () + [(s (... ...)) + (let ([r (id/depth #'s)]) + (make-id/depth (id/depth-id r) (add1 (id/depth-depth r))))] + [s (make-id/depth #'s 0)])) + (define temporaries (generate-temporaries names)) + (values + (for/fold ([cs '()]) + ([n names] + [w/e names/ellipses] + [x temporaries]) + (cond [(hash-ref bindings (syntax-e n) #f) + => (λ (b) + (let ([b-id/depth (id/depth b)] + [n-id/depth (id/depth w/e)]) + (if (= (id/depth-depth b-id/depth) (id/depth-depth n-id/depth)) + (cons #`(equal? #,x (term #,b)) cs) + (raise-ellipsis-depth-error + syn-err-name + (id/depth-id n-id/depth) (id/depth-depth n-id/depth) + (id/depth-id b-id/depth) (id/depth-depth b-id/depth)))))] + [else cs])) + temporaries + (for/fold ([extended bindings]) + ([name names] + [w/ellipses names/ellipses]) + (hash-set extended (syntax-e name) w/ellipses)))) + ;; the withs, freshs, and side-conditions come in backwards order (define-for-syntax (bind-withs orig-name main lang lang-nts stx where-mode body names w/ellipses) + (with-disappeared-uses (let loop ([stx stx] [to-not-be-in main] [env (make-immutable-hash @@ -281,52 +327,27 @@ (syntax-case stx (fresh) [() body] [((-where x e) y ...) - (or (free-identifier=? #'-where #'where) - (free-identifier=? #'-where #'where/hidden)) + (where-keyword? #'-where) (let-values ([(names names/ellipses) (extract-names lang-nts 'reduction-relation #t #'x)]) - (let ([env+ (for/fold ([env env]) - ([name names] - [w/ellipses names/ellipses]) - (hash-set env (syntax-e name) w/ellipses))] - [temporaries (generate-temporaries names)]) - (define (id/depth stx) - (syntax-case stx () - [(s (... ...)) - (let ([r (id/depth #'s)]) - (make-id/depth (id/depth-id r) (add1 (id/depth-depth r))))] - [s (make-id/depth #'s 0)])) - (with-syntax ([(binding-constraints ...) - (for/fold ([cs '()]) - ([n names] - [w/e names/ellipses] - [x temporaries]) - (cond [(hash-ref env (syntax-e n) #f) - => (λ (b) - (let ([b-id/depth (id/depth b)] - [n-id/depth (id/depth w/e)]) - (if (= (id/depth-depth b-id/depth) (id/depth-depth n-id/depth)) - (cons #`(equal? #,x (term #,b)) cs) - (raise-ellipsis-depth-error - orig-name - (id/depth-id n-id/depth) (id/depth-depth n-id/depth) - (id/depth-id b-id/depth) (id/depth-depth b-id/depth)))))] - [else cs]))]) - (with-syntax ([side-conditions-rewritten (rewrite-side-conditions/check-errs - lang-nts - 'reduction-relation - #f - #'x)] - [(names ...) names] - [(names/ellipses ...) names/ellipses] - [(x ...) temporaries]) - (let ([rest-body (loop #'(y ...) #`(list x ... #,to-not-be-in) env+)]) - #`(let* ([mtchs (match-pattern (compile-pattern #,lang `side-conditions-rewritten #t) (term e))] - [result (λ (mtch) - (let ([bindings (mtch-bindings mtch)]) - (let ([x (lookup-binding bindings 'names)] ...) - (and binding-constraints ... - (term-let ([names/ellipses x] ...) - #,rest-body)))))]) + (define-values (binding-constraints temporaries env+) + (generate-binding-constraints names names/ellipses env orig-name)) + (with-syntax ([(binding-constraints ...) binding-constraints] + [side-conditions-rewritten (rewrite-side-conditions/check-errs + lang-nts + 'reduction-relation + #f + #'x)] + [(names ...) names] + [(names/ellipses ...) names/ellipses] + [(x ...) temporaries]) + (let ([rest-body (loop #'(y ...) #`(list x ... #,to-not-be-in) env+)]) + #`(let* ([mtchs (match-pattern (compile-pattern #,lang `side-conditions-rewritten #t) (term e))] + [result (λ (mtch) + (let ([bindings (mtch-bindings mtch)]) + (let ([x (lookup-binding bindings 'names)] ...) + (and binding-constraints ... + (term-let ([names/ellipses x] ...) + #,rest-body)))))]) (if mtchs #, (case where-mode @@ -337,7 +358,7 @@ [(predicate) #`(ormap result mtchs)] [else (error 'unknown-where-mode "~s" where-mode)]) - #f)))))))] + #f)))))] [((-side-condition s ...) y ...) (or (free-identifier=? #'-side-condition #'side-condition) (free-identifier=? #'-side-condition #'side-condition/hidden)) @@ -364,7 +385,68 @@ [len-counter (term (x ...))]) (verify-names-ok '#,orig-name the-names len-counter) (variables-not-in #,to-not-be-in the-names))]) - #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) env))]))) + #,(loop #'(z ...) #`(list (term (y #,'...)) #,to-not-be-in) env))] + [((form-name . pats) . rest-clauses) + (judgment-form-id? #'form-name) + (let*-values ([(judgment-form) (syntax-local-value/record #'form-name (λ (_) #t))] + [(mode) (judgment-form-mode judgment-form)] + [(judgment-proc) (judgment-form-proc judgment-form)] + [(input-template output-pre-pattern) (split-by-mode (syntax->list #'pats) mode)] + [(output-pattern) + (rewrite-side-conditions/check-errs lang-nts orig-name #t output-pre-pattern)] + [(output-names output-names/ellipses) + (extract-names lang-nts orig-name #t output-pattern)] + [(binding-constraints temporaries env+) + (generate-binding-constraints output-names output-names/ellipses env orig-name)] + [(rest-body) (loop #'rest-clauses #`(list judgment-output #,to-not-be-in) env+)] + [(call) (quasisyntax/loc #'form-name + (call-judgment-form + 'form-name #,judgment-proc '#,mode (term #,input-template)))]) + (with-syntax ([(output-name ...) output-names] + [(output-name/ellipsis ...) output-names/ellipses] + [(temp ...) temporaries] + [(binding-constraint ...) binding-constraints]) + (syntax-case stx () [(clause . _) #'clause]) + #`(begin + (void #,(defined-check judgment-proc "judgment form" #:external #'form-name)) + (for/fold ([outputs '()]) ([sub-output #,call]) + (define mtchs + (match-pattern (compile-pattern #,lang `#,output-pattern #t) sub-output)) + (if mtchs + (for/fold ([outputs outputs]) ([mtch mtchs]) + (let ([temp (lookup-binding (mtch-bindings mtch) 'output-name)] ...) + (and binding-constraint ... + (term-let ([output-name/ellipsis temp] ...) + (let ([output-rest #,rest-body]) + (and output-rest + (append outputs output-rest))))))) + outputs)))))])))) + +(define (call-judgment-form form-name form-proc mode input) + (define traced (current-traced-metafunctions)) + (if (or (eq? 'all traced) (memq form-name traced)) + (let ([outputs #f]) + (define spacers + (for/fold ([s '()]) ([m mode]) + (case m [(I) s] [(O) (cons '_ s)]))) + (define (assemble inputs outputs) + (let loop ([ms mode] [is inputs] [os outputs]) + (if (null? ms) + '() + (case (car ms) + [(I) (cons (car is) (loop (cdr ms) (cdr is) os))] + [(O) (cons (car os) (loop (cdr ms) is (cdr os)))])))) + (define (wrapped . _) + (set! outputs (form-proc input)) + (for/list ([output outputs]) + (cons form-name (assemble input output)))) + (apply trace-call form-name wrapped (assemble input spacers)) + outputs) + (form-proc input))) + +(define-for-syntax (name-pattern-lws pat) + (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/proc (cdr x)))) + (extract-pattern-binds pat))) (define-syntax-set (do-reduction-relation) (define (do-reduction-relation/proc stx) @@ -466,6 +548,11 @@ [with (cdr lst)] [else (loop (cdr lst))]))]))) + (define (name-pattern-lws/rr pat) + (for/list ([lw-pair (name-pattern-lws pat)]) + (match lw-pair + [(cons l r) #`(cons #,l #,r)]))) + (define (rule->lws rule) (syntax-case rule () [(arrow lhs rhs stuff ...) @@ -481,7 +568,8 @@ (syntax-case (car stuffs) (where where/hidden side-condition side-condition/hidden fresh variable-not-in - computed-name) + computed-name + judgment-holds) [(fresh xs ...) (loop (cdr stuffs) label @@ -514,7 +602,7 @@ label computed-label (cons #`(cons #,(to-lw/proc #'x) #,(to-lw/proc #'e)) - scs/withs) + (append (name-pattern-lws/rr #'x) scs/withs)) fvars)] [(where/hidden x e) (loop (cdr stuffs) label computed-label scs/withs fvars)] @@ -545,6 +633,17 @@ label #'e scs/withs + fvars)] + [(judgment-holds (form-name . pieces)) + (judgment-form-id? #'form-name) + (loop (cdr stuffs) + label + computed-label + (let*-values ([(mode) (judgment-form-mode (syntax-local-value #'form-name))] + [(_ outs) (split-by-mode (syntax->list #'pieces) mode)]) + (cons (to-lw/proc #'(form-name . pieces)) + (for/fold ([binds scs/withs]) ([out outs]) + (append (name-pattern-lws/rr out) binds)))) fvars)])]))]) (with-syntax ([(scs/withs ...) scs/withs] [(fvars ...) fvars] @@ -761,7 +860,7 @@ (if (or (memq x nts) (memq x underscore-allowed)) (string-append (symbol->string x) "_") x))) - (let-values ([(bound _) (extract-names nts what #t pat #f)]) + (let-values ([(bound _) (extract-names nts what #t pat 'binds-anywhere)]) (let ([renames (make-bound-identifier-mapping)]) (for-each (λ (x) @@ -870,7 +969,7 @@ (cond [(null? extras) '()] [else - (syntax-case (car extras) (fresh computed-name) + (syntax-case (car extras) (fresh computed-name judgment-holds) [name (or (identifier? (car extras)) (string? (syntax-e (car extras)))) @@ -929,12 +1028,10 @@ (free-identifier=? #'-side-condition #'side-condition/hidden)) (cons (car extras) (loop (cdr extras)))] [(-where x e) - (or (free-identifier=? #'-where #'where) - (free-identifier=? #'-where #'where/hidden)) + (where-keyword? #'-where) (cons (car extras) (loop (cdr extras)))] [(-where . x) - (or (free-identifier=? #'-where #'where) - (free-identifier=? #'-where #'where/hidden)) + (where-keyword? #'-where) (raise-syntax-error orig-name "malformed where clause" stx (car extras))] [(computed-name e) (if computed-name-stx @@ -944,6 +1041,8 @@ (loop (cdr extras))] [(computed-name . _) (raise-syntax-error orig-name "malformed computed-name clause" stx (car extras))] + [(judgment-holds judgment) + (cons #'judgment (loop (cdr extras)))] [_ (raise-syntax-error orig-name "unknown extra" stx (car extras))])]))]) (values the-name computed-name-stx sides/withs/freshs))) @@ -1178,6 +1277,15 @@ ((metafunc-proc-in-dom? mp) exp))) +(define-for-syntax (definition-nts lang orig-stx syn-error-name) + (unless (identifier? lang) + (raise-syntax-error #f "expected an identifier in the language position" orig-stx lang)) + (language-id-nts lang syn-error-name)) + +(define-for-syntax (lhs-lws clauses) + (with-syntax ([((lhs-for-lw _ ...) ...) clauses]) + (map (λ (x) (to-lw/proc (datum->syntax #f (cdr (syntax-e x)) x))) + (syntax->list #'(lhs-for-lw ...))))) ; ; @@ -1195,7 +1303,9 @@ ; ; -(define-syntax-set (define-metafunction define-metafunction/extension define-relation) +(define-syntax-set (define-metafunction define-metafunction/extension + define-relation + define-judgment-form) (define (define-metafunction/proc stx) (syntax-case stx () @@ -1224,7 +1334,7 @@ 'define-metafunction))]) (define lang-nts ;; keep this near the beginning, so it signals the first error (PR 10062) - (relevant-nts #'lang orig-stx syn-error-name)) + (definition-nts #'lang orig-stx syn-error-name)) (when (null? (syntax-e #'rest)) (raise-syntax-error syn-error-name "no clauses" orig-stx)) (when prev-metafunction @@ -1233,8 +1343,9 @@ (λ () (raise-syntax-error syn-error-name "expected a previously defined metafunction" orig-stx prev-metafunction)))) (let () - (let-values ([(contract-name dom-ctcs codom-contracts pats) - (split-out-contract orig-stx syn-error-name #'rest relation?)]) + (let*-values ([(contract-name dom-ctcs codom-contracts pats) + (split-out-contract orig-stx syn-error-name #'rest relation?)] + [(name _) (defined-name contract-name pats orig-stx)]) (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats] [(lhs-for-lw ...) (lhs-lws pats)]) (with-syntax ([((rhs stuff ...) ...) (if relation? @@ -1242,12 +1353,12 @@ #'((raw-rhses ...) ...))]) (parameterize () (with-syntax ([(lhs ...) #'((lhs-clauses ...) ...)] - [name (defined-name contract-name pats orig-stx)]) + [name name]) (when (and prev-metafunction (eq? (syntax-e #'name) (syntax-e prev-metafunction))) (raise-syntax-error syn-error-name "the extended and extending metafunctions cannot share a name" orig-stx prev-metafunction)) (parse-extras #'((stuff ...) ...)) (let-values ([(lhs-namess lhs-namess/ellipsess) - (bound-names (syntax->list (syntax (lhs ...))) lang-nts syn-error-name)]) + (lhss-bound-names (syntax->list (syntax (lhs ...))) lang-nts syn-error-name)]) (with-syntax ([(rhs/wheres ...) (map (λ (sc/b rhs names names/ellipses) (bind-withs @@ -1376,7 +1487,82 @@ (map syntax-local-introduce (syntax->list #'(original-names ...)))))))))))))))])) - (define (bound-names lhss nts syn-error-name) + (define (define-judgment-form/proc stx) + (syntax-case stx () + [(def-form-id lang . body) + (let ([lang #'lang] + [syn-err-name (syntax-e #'def-form-id)]) + (define nts (definition-nts lang stx syn-err-name)) + (define-values (judgment-form-name dup-form-names mode position-contracts clauses) + (parse-define-judgment-form-body #'body syn-err-name stx)) + (syntax-property + (prune-syntax + #`(begin + (define-syntax #,judgment-form-name + (judgment-form '#,judgment-form-name '#,mode #'judgment-form-proc #'#,lang #'judgment-form-lws)) + (define judgment-form-proc + (let-syntax ([delayed + (λ (stx) + (syntax-case stx () + [(_ lang clauses ctcs full-def) + (let ([nts (definition-nts #'lang #'full-def '#,syn-err-name)]) + (mode-check '#,mode (syntax->list #'clauses) nts '#,syn-err-name) + (compile-judgment-form-proc + '#,judgment-form-name '#,mode (syntax->list #'clauses) #'ctcs nts #'lang '#,syn-err-name))]))]) + (delayed #,lang #,clauses #,position-contracts #,stx))) + (define judgment-form-lws + (let-syntax ([delayed + (λ (stx) + (syntax-case stx () + [(_ clauses) + (compile-judgment-form-lws (syntax->list #'clauses))]))]) + (delayed #,clauses))))) + 'disappeared-use + (map syntax-local-introduce dup-form-names)))])) + + (define (parse-define-judgment-form-body body syn-err-name full-stx) + (define-values (mode rest-body) + (parse-mode-spec body full-stx)) + (define-values (declared-form-name contracts clauses) + (syntax-case rest-body () + [(form-name . rest-contract+clauses) + (identifier? #'form-name) + (let-values ([(contracts clauses) + (parse-relation-contract #'rest-contract+clauses syn-err-name full-stx)]) + (values #'form-name contracts clauses))] + [_ (values #f #f (syntax->list rest-body))])) + (check-clauses full-stx syn-err-name clauses #t) + (check-arity-consistency mode contracts clauses full-stx) + (define-values (form-name dup-names) + (syntax-case clauses () + [() (raise-syntax-error #f "expected at least one clause after mode" full-stx)] + [_ (defined-name declared-form-name clauses full-stx)])) + (values form-name dup-names mode contracts clauses)) + + (define (check-arity-consistency mode contracts clauses full-def) + (when (and contracts (not (= (length mode) (length contracts)))) + (raise-syntax-error + #f "mode and contract specify different numbers of positions" full-def))) + + (define (parse-mode-spec body full-stx) + (syntax-case body (mode :) + [(mode : . rest-body) + (let loop ([rest-body #'rest-body] + [pos-modes '()] + [idx 1]) + (syntax-case rest-body (I O) + [(I . more) + (loop #'more (cons 'I pos-modes) (+ 1 idx))] + [(O . more) + (loop #'more (cons 'O pos-modes) (+ 1 idx))] + [_ (values (reverse pos-modes) rest-body)]))] + [_ (raise-syntax-error + #f "expected a mode specification after the language declaration" + (if (pair? (syntax-e body)) + (car (syntax-e body)) + full-stx))])) + + (define (lhss-bound-names lhss nts syn-error-name) (let loop ([lhss lhss]) (if (null? lhss) (values null null) @@ -1387,36 +1573,27 @@ (values (cons names namess) (cons names/ellipses namess/ellipsess)))))) - (define (lhs-lws clauses) - (with-syntax ([((lhs-for-lw _ ...) ...) clauses]) - (map (λ (x) (to-lw/proc (datum->syntax #f (cdr (syntax-e x)) x))) - (syntax->list #'(lhs-for-lw ...))))) - - (define (relevant-nts lang orig-stx syn-error-name) - (unless (identifier? lang) - (raise-syntax-error #f "expected an identifier in the language position" orig-stx lang)) - (language-id-nts lang syn-error-name)) - (define (defined-name declared-name clauses orig-stx) (with-syntax ([(((used-names _ ...) _ ...) ...) clauses]) - (let loop ([name (if declared-name - declared-name - (car (syntax->list #'(used-names ...))))] - [names (if declared-name - (syntax->list #'(used-names ...)) - (cdr (syntax->list #'(used-names ...))))]) + (define-values (the-name other-names) + (if declared-name + (values declared-name + (syntax->list #'(used-names ...))) + (values (car (syntax->list #'(used-names ...))) + (cdr (syntax->list #'(used-names ...)))))) + (let loop ([others other-names]) (cond - [(null? names) name] + [(null? others) (values the-name other-names)] [else - (unless (eq? (syntax-e name) (syntax-e (car names))) + (unless (eq? (syntax-e the-name) (syntax-e (car others))) (raise-syntax-error #f (if declared-name "expected each clause and the contract to use the same name" "expected each clause to use the same name") orig-stx - name (list (car names)))) - (loop name (cdr names))])))) + the-name (list (car others)))) + (loop (cdr others))])))) (define (split-out-contract stx syn-error-name rest relation?) ;; initial test determines if a contract is specified or not @@ -1569,6 +1746,163 @@ (cons (cadr more) arg-pats))] [else (values (reverse arg-pats) more)])))]))) +(define-for-syntax (check-judgment-arity judgment) + (syntax-case judgment () + [(form-name pat ...) + (judgment-form-id? #'form-name) + (let ([expected (length (judgment-form-mode (syntax-local-value #'form-name)))]) + (unless (= (length (syntax->list #'(pat ...))) expected) + (raise-syntax-error #f "arity mismatch" judgment)))])) + +(define-syntax (judgment-holds stx) + (syntax-case stx () + [(j-h judgment) + #`(not (null? #,(syntax/loc stx (j-h judgment #t))))] + [(j-h (form-name . pats) tmpl) + (judgment-form-id? #'form-name) + (let* ([syn-err-name (syntax-e #'j-h)] + [lang (judgment-form-lang (syntax-local-value #'form-name))] + [nts (definition-nts lang stx syn-err-name)]) + (check-judgment-arity #'(form-name . pats)) + (bind-withs syn-err-name '() lang nts (list #'(form-name . pats)) + 'flatten #`(list (term #,#'tmpl)) '() '()))] + [(_ (not-form-name . _) . _) + (not (judgment-form-id? #'form-name)) + (raise-syntax-error #f "expected a judgment form name" stx #'not-form-name)])) + +(define-for-syntax (compile-judgment-form-proc name mode clauses contracts nts lang syn-error-name) + (define (compile-clause clause) + (syntax-case clause () + [((_ . conc-pats) . prems) + (let-values ([(input-pats output-pats) (split-by-mode (syntax->list #'conc-pats) mode)]) + (define-values (input-names input-names/ellipses) + (extract-names nts syn-error-name #t input-pats)) + (define ((rewrite-pattern binds?) pat) + (rewrite-side-conditions/check-errs nts syn-error-name binds? pat)) + (define (contracts-compilation ctcs) + (and ctcs #`(map (λ (p) (compile-pattern #,lang p #f)) `#,ctcs))) + (define-values (input-contracts output-contracts) + (syntax-case contracts () + [#f (values #f #f)] + [(p ...) + (let-values ([(ins outs) (split-by-mode (syntax->list #'(p ...)) mode)]) + (values (map (rewrite-pattern #f) ins) + (map (rewrite-pattern #f) outs)))])) + (define lhs (map (rewrite-pattern #t) input-pats)) + (define body + (bind-withs syn-error-name '() lang nts (syntax->list #'prems) + 'flatten #`(list (term (#,@output-pats))) input-names input-names/ellipses)) + (with-syntax ([(names ...) input-names] + [(names/ellipses ...) input-names/ellipses]) + #`(let ([compiled-lhs (compile-pattern #,lang `#,lhs #t)] + [compiled-input-ctcs #,(contracts-compilation input-contracts)] + [compiled-output-ctcs #,(contracts-compilation output-contracts)]) + (λ (input) + (check-judgment-form-contract `#,name input compiled-input-ctcs 'I '#,mode) + (define mtchs (match-pattern compiled-lhs input)) + (define outputs + (if mtchs + (for/fold ([outputs '()]) ([m mtchs]) + (define os + (term-let ([names/ellipses (lookup-binding (mtch-bindings m) 'names)] ...) + #,body)) + (if os (append os outputs) outputs)) + '())) + (for ([output outputs]) + (check-judgment-form-contract `#,name output compiled-output-ctcs 'O '#,mode)) + outputs))))])) + (with-syntax ([(clause-proc ...) (map compile-clause clauses)]) + #'(λ (input) + (for/fold ([outputs '()]) ([rule (list clause-proc ...)]) + (append (rule input) outputs))))) + +(define-for-syntax (in-order-non-hidden extras) + (reverse + (filter (λ (extra) + (syntax-case extra (where/hidden + side-condition/hidden) + [(where/hidden pat exp) #f] + [(side-condition/hidden x) #f] + [_ #t])) + (syntax->list extras)))) + +(define-for-syntax (compile-judgment-form-lws clauses) + (syntax-case clauses () + [(((_ . conc-body) . prems) ...) + (let ([rev-premss + ; for consistency with metafunction extras + (for/list ([prems (syntax->list #'(prems ...))]) + (reverse (syntax->list prems)))] + [no-rhss (map (λ (_) '()) clauses)]) + #`(generate-lws #t (conc-body ...) #,(lhs-lws clauses) #,rev-premss #,no-rhss))])) + +(define (check-judgment-form-contract form-name terms contracts mode modes) + (define description + (case mode + [(I) "input"] + [(O) "output"])) + (when contracts + (let loop ([rest-modes modes] [rest-terms terms] [rest-ctcs contracts] [pos 1]) + (unless (null? rest-modes) + (if (eq? mode (car rest-modes)) + (if (match-pattern (car rest-ctcs) (car rest-terms)) + (loop (cdr rest-modes) (cdr rest-terms) (cdr rest-ctcs) (+ 1 pos)) + (redex-error form-name "~a ~s at position ~s does not match its contract" + description (car rest-terms) pos)) + (loop (cdr rest-modes) rest-terms rest-ctcs (+ 1 pos))))))) + +(define-for-syntax (mode-check mode clauses nts syn-err-name) + (define ((check-template named-vars) temp bound) + (let check ([t temp]) + (syntax-case t (unquote) + [(unquote . _) + (raise-syntax-error syn-err-name "unquote unsupported" t)] + [x + (identifier? #'x) + (when (and (or (id-binds? nts #t #'x) (free-id-table-ref named-vars #'x #f)) + (not (free-id-table-ref bound #'x #f))) + (raise-syntax-error syn-err-name "unbound pattern variable" #'x))] + [(u ...) + (for-each check (syntax->list #'(u ...)))] + [_ (void)]))) + (define ((bind kind) pat bound) + (define-values (ids _) + (extract-names nts syn-err-name #t pat kind)) + (for/fold ([b bound]) ([x ids]) + (free-id-table-set b x #t))) + (define (split-body judgment) + (syntax-case judgment () + [(form-name . body) + (split-by-mode (syntax->list #'body) (judgment-form-mode (syntax-local-value #'form-name)))])) + (define (fold-clause pat-pos tmpl-pos acc-init clause) + (syntax-case clause () + [(conc . prems) + (let-values ([(conc-in conc-out) (split-body #'conc)]) + (check-judgment-arity #'conc) + (define acc-out + (for/fold ([acc (foldl pat-pos acc-init conc-in)]) + ([prem (syntax->list #'prems)]) + (syntax-case prem () + [(form-name . _) + (judgment-form-id? #'form-name) + (let-values ([(prem-in prem-out) (split-body prem)]) + (check-judgment-arity prem) + (for ([pos prem-in]) (tmpl-pos pos acc)) + (foldl pat-pos acc prem-out))] + [(-where pat tmpl) + (where-keyword? #'-where) + (begin + (tmpl-pos #'tmpl acc) + (pat-pos #'pat acc))] + [_ (raise-syntax-error syn-err-name "malformed premise" prem)]))) + (for ([pos conc-out]) (tmpl-pos pos acc-out)) + acc-out)])) + (for ([clause clauses]) + (define do-tmpl + (check-template + (fold-clause (bind 'name-only) void (make-immutable-free-id-table) clause))) + (fold-clause (bind 'rhs-only) do-tmpl (make-immutable-free-id-table) clause))) + ;; Defined as a macro instead of an ordinary phase 1 function so that the ;; to-lw/proc calls occur after bindings are established for all meta-functions ;; and relations. @@ -1583,16 +1917,16 @@ [#f (map to-lw/proc (syntax->list #'seq-of-rhs))])] [(((bind-id/lw . bind-pat/lw) ...) ...) ;; Also for pict, extract pattern bindings - (map (λ (x) (map (λ (x) (cons (to-lw/proc (car x)) (to-lw/proc (cdr x)))) - (extract-pattern-binds x))) - (syntax->list #'seq-of-lhs))] - + (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))] [(where pat (unquote (f _ _))) (and (or (identifier? #'pat) (andmap identifier? (syntax->list #'pat))) @@ -1611,16 +1945,21 @@ [(side-condition x) #`(make-metafunc-extra-side-cond #,(to-lw/uq/proc #'x))])) - (reverse - (filter (λ (lst) - (syntax-case lst (where/hidden - side-condition/hidden) - [(where/hidden pat exp) #f] - [(side-condition/hidden x) #f] - [_ #t])) - (syntax->list hm))))) + (in-order-non-hidden hm))) + (syntax->list #'seq-of-tl-side-cond/binds))] + [(((where-bind-id/lw . where-bind-pat/lw) ...) ...) + (map (λ (clauses) + (for/fold ([binds '()]) ([clause (in-order-non-hidden clauses)]) + (syntax-case clause (where) + [(form-name . pieces) + (judgment-form-id? #'form-name) + (let*-values ([(mode) (judgment-form-mode (syntax-local-value #'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))] - [(((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)))) @@ -1630,6 +1969,7 @@ [(x-lhs-for-lw ...) #'seq-of-lhs-for-lw]) #'(list (list x-lhs-for-lw (list (make-metafunc-extra-where bind-id/lw bind-pat/lw) ... + (make-metafunc-extra-where where-bind-id/lw where-bind-pat/lw) ... (make-metafunc-extra-where rhs-bind-id/lw rhs-bind-pat/lw/uq) ... where/sc/lw ...) rhs/lw) @@ -2387,6 +2727,8 @@ define-metafunction define-metafunction/extension define-relation + define-judgment-form + judgment-holds (rename-out [metafunction-form metafunction]) metafunction? metafunction-proc diff --git a/collects/redex/private/rewrite-side-conditions.rkt b/collects/redex/private/rewrite-side-conditions.rkt index f477df0a48..577402c8a5 100644 --- a/collects/redex/private/rewrite-side-conditions.rkt +++ b/collects/redex/private/rewrite-side-conditions.rkt @@ -8,6 +8,7 @@ (provide rewrite-side-conditions/check-errs extract-names + (rename-out [binds? id-binds?]) raise-ellipsis-depth-error make-language-id language-id-nts) @@ -122,7 +123,7 @@ (define-struct id/depth (id depth)) ;; extract-names : syntax syntax -> (values (listof syntax) (listof syntax[x | (x ...) | ((x ...) ...) | ...])) - (define (extract-names all-nts what bind-names? orig-stx [rhs-only? #t]) + (define (extract-names all-nts what bind-names? orig-stx [mode 'rhs-only]) (let* ([dups (let loop ([stx orig-stx] [names null] @@ -158,7 +159,10 @@ (loop (car pats) names (+ depth 1))))]))] [x (and (identifier? (syntax x)) - ((if rhs-only? binds-in-right-hand-side? binds?) + ((case mode + [(rhs-only) binds-in-right-hand-side?] + [(binds-anywhere) binds?] + [(name-only) (λ (_1 _2 _3) #f)]) all-nts bind-names? (syntax x))) (cons (make-id/depth (syntax x) depth) names)] [else names]))] diff --git a/collects/redex/private/term-fn.rkt b/collects/redex/private/term-fn.rkt index 26d246660a..1440fe2efb 100644 --- a/collects/redex/private/term-fn.rkt +++ b/collects/redex/private/term-fn.rkt @@ -1,12 +1,27 @@ #lang scheme/base +(require (for-template racket/base "defined-checks.rkt")) (provide make-term-fn term-fn? term-fn-get-id - (struct-out term-id)) + (struct-out term-id) + (struct-out judgment-form) + judgment-form-id? + defined-check) (define-values (struct-type make-term-fn term-fn? term-fn-get term-fn-set!) (make-struct-type 'term-fn #f 1 0)) (define term-fn-get-id (make-struct-field-accessor term-fn-get 0)) (define-struct term-id (id depth)) + +(define-struct judgment-form (name mode proc lang lws)) + +(define (judgment-form-id? stx) + (and (identifier? stx) + (judgment-form? (syntax-local-value stx (λ () 'not-a-judgment-form))))) + +(define (defined-check id desc #:external [external id]) + (if (eq? (identifier-binding id) 'lexical) + (quasisyntax/loc external (check-defined-lexical #,id '#,external #,desc)) + (quasisyntax/loc external (check-defined-module (λ () #,id) '#,external #,desc)))) \ No newline at end of file diff --git a/collects/redex/private/term.rkt b/collects/redex/private/term.rkt index 0ce68d3e26..a64a39d00c 100644 --- a/collects/redex/private/term.rkt +++ b/collects/redex/private/term.rkt @@ -115,10 +115,7 @@ #`(begin #,@(free-identifier-mapping-map applied-metafunctions - (λ (f _) - (if (eq? (identifier-binding f) 'lexical) - #`(check-defined-lexical #,f '#,f) - #`(check-defined-module (λ () #,f) '#,f)))) + (λ (f _) (defined-check f "metafunction"))) #,(let loop ([bs (reverse outer-bindings)]) (cond [(null? bs) (syntax (syntax->datum (quasisyntax rewritten)))] @@ -127,18 +124,6 @@ (syntax (with-syntax (fst) rec)))])))))])) -(define (check-defined-lexical value name) - (when (eq? (letrec ([x x]) x) value) - (report-undefined-metafunction name))) - -(define (check-defined-module thunk name) - (with-handlers ([exn:fail:contract:variable? - (λ (_) (report-undefined-metafunction name))]) - (thunk))) - -(define (report-undefined-metafunction name) - (redex-error #f "metafunction ~s applied before its definition" name)) - (define-syntax (term-let-fn stx) (syntax-case stx () [(_ ([f rhs] ...) body1 body2 ...) diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index 2a8b0405bb..a9fb313d8e 100644 --- a/collects/redex/redex.scrbl +++ b/collects/redex/redex.scrbl @@ -697,6 +697,7 @@ otherwise. (fresh fresh-clause ...) (side-condition racket-expression) (where @#,ttpattern @#,tttterm) + (judgment-holds (judgment-form-id pat/term)) (side-condition/hidden racket-expression) (where/hidden @#,ttpattern @#,tttterm)] [shortcuts (code:line) @@ -706,7 +707,9 @@ otherwise. [rule-name identifier string (computed-name racket-expression)] - [fresh-clause var ((var1 ...) (var2 ...))])]{ + [fresh-clause var ((var1 ...) (var2 ...))] + [pat/term @#,ttpattern + @#,tttterm])]{ Defines a reduction relation casewise, one case for each of the @racket[reduction-case] clauses. @@ -792,6 +795,10 @@ metafunction result. The bindings are the same as bindings in a same as a @racket[where] clause, but the clause is not rendered when typesetting via @racketmodname[redex/pict]. +Each @racket[judgment-holds] clause acts like a @racket[where] clause, where +the left-hand side pattern incorporates each of the patterns used in the +judgment form's output positions. + Each @racket[shortcut] clause defines arrow names in terms of @racket[base-arrow-name] and earlier @racket[shortcut] definitions. The left- and right-hand sides of a @racket[shortcut] definition @@ -940,7 +947,7 @@ it is traversing through the reduction graph. @racket[reduction-relation]. A @racket[with] form is an error elsewhere. } -@section{Metafunctions and Relations} +@section{Other Relations} @declare-exporting[redex/reduction-semantics redex] @@ -1062,35 +1069,157 @@ legtimate inputs according to @racket[metafunction-name]'s contract, and @racket[#f] otherwise. } -@defform/subs[#:literals () - (define-relation language - relation-contract - [(name @#,ttpattern ...) @#,tttterm ...] ...) - ([relation-contract (code:line) - (code:line id ⊂ pat x ... x pat) - (code:line id ⊆ pat × ... × pat)])]{ +@defform/subs[#:literals (mode : I O ⊂ ⊆ × x where) + (define-judgment-form language + mode-spec + maybe-contract + [conclusion premise ...] ...) + ([mode-spec (code:line mode : use ...)] + [use I + O] + [maybe-contract (code:line) + (code:line form-id ⊂ @#,ttpattern x ... x @#,ttpattern) + (code:line form-id ⊆ @#,ttpattern × ... × @#,ttpattern)] + [conclusion (form-id pat/term ...)] + [premise (judgment-form-id pat/term ...) + (where @#,ttpattern @#,tttterm)] + [pat/term @#,ttpattern + @#,tttterm])]{ +Defines @racket[form-id] as a relation on terms via a set of inference rules. +Each rule must be such that its premises can be evaluated left-to-right +without ``guessing'' values for any of their pattern variables. Redex checks this +property using the @racket[mode-spec] declaration, which partitions positions +into inputs @racket[I] and outputs @racket[O]. Output positions in conclusions +and input positions in premises must be @|tttterm|s with no uses of +@racket[unquote]; input positions in conclusions and output positions in +premises must be @|ttpattern|s. When the optional @racket[relation-contract] +declaration is present, Redex dynamically checks that the terms flowing through +these positions match the provided patterns, raising an exception recognized by +@racket[exn:fail:redex] if not. -The @racket[define-relation] form builds a relation on -sexpressions according to the pattern and right-hand-side -expressions. The first argument indicates the language used -to resolve non-terminals in the pattern expressions. Each of -the rhs-expressions is implicitly wrapped in @|tttterm|. +For example, the following defines addition on natural numbers: +@interaction[ +#:eval redex-eval + (define-language nats + (n z (s n))) + (define-judgment-form nats + mode : I I O + sum ⊆ n × n × n + [(sum z n n)] + [(sum (s n_1) n_2 (s n_3)) + (sum n_1 n_2 n_3)])] + +The @racket[judgment-holds] form checks whether a relation holds for any +assignment of pattern variables in output positions. +@examples[ +#:eval redex-eval + (judgment-holds (sum (s (s z)) (s z) (s (s (s z))))) + (judgment-holds (sum (s (s z)) (s z) (s (s (s n))))) + (judgment-holds (sum (s (s z)) (s z) (s (s (s (s n))))))] +Alternatively, this form constructs a list of terms based on the satisfying +pattern variable assignments. +@examples[ +#:eval redex-eval + (judgment-holds (sum (s (s z)) (s z) (s (s (s n)))) n) + (judgment-holds (sum (s (s z)) (s z) (s (s (s (s n))))) n) + (judgment-holds (sum (s (s z)) (s z) (s (s (s n)))) (s n))] -Relations are like metafunctions in that they are called with -arguments and return results (unlike in, say, prolog, where a relation -definition would be able to synthesize some of the arguments based on -the values of others). +Declaring different modes for the same inference rules enables different forms +of computation. For example, the following mode allows @racket[judgment-holds] +to compute all pairs with a given sum. +@interaction[ +#:eval redex-eval + (define-judgment-form nats + mode : O O I + sumr ⊆ n × n × n + [(sumr z n n)] + [(sumr (s n_1) n_2 (s n_3)) + (sumr n_1 n_2 n_3)]) + (judgment-holds (sumr n_1 n_2 (s (s z))) (n_1 n_2))] -Unlike metafunctions, relations check all possible ways to match each -case, looking for a true result and if none of the clauses match, then -the result is @racket[#f]. If there are multiple expressions on -the right-hand side of a relation, then all of them must be satisfied -in order for that clause of the relation to be satisfied. +A rule's @racket[where] clause premises behave as in @racket[reduction-relation] +and @racket[define-metafunction]. +@interaction[ +#:eval redex-eval + (define-judgment-form nats + mode : I I + le ⊆ n × n + [(le z n)] + [(le (s n_1) (s n_2)) + (le n_1 n_2)]) + (define-metafunction nats + pred : n -> n or #f + [(pred z) #f] + [(pred (s n)) n]) + (define-judgment-form nats + mode : I I + gt ⊆ n × n + [(gt n_1 n_2) + (where n_3 (pred n_1)) + (le n_2 n_3)]) + (judgment-holds (gt (s (s z)) (s z))) + (judgment-holds (gt (s z) (s z)))] -The contract specification for a relation restricts the patterns that can -be used as input to a relation. For each argument to the relation, there -should be a single pattern, using @racket[x] or @racket[×] to separate -the argument contracts. +Redex evaluates premises depth-first, even when it doing so leads to +non-termination. For example, consider the following definitions: +@interaction[ +#:eval redex-eval + (define-language vertices + (v a b c)) + (define-judgment-form vertices + mode : I O + edge ⊆ v × v + [(edge a b)] + [(edge b c)]) + (define-judgment-form vertices + mode : I I + path ⊆ v × v + [(path v v)] + [(path v_1 v_2) + (path v_2 v_1)] + [(path v_1 v_3) + (edge v_1 v_2) + (path v_2 v_3)])] +Due to the second @racket[path] rule, the follow query fails to terminate: +@racketinput[(judgment-holds (path a c))] +} + +@defform*/subs[((judgment-holds judgment) + (judgment-holds judgment @#,tttterm)) + ([judgment (judgment-form-id pat/term ...)])]{ +In its first form, checks whether @racket[judgment] holds for any assignment of +the pattern variables in @racket[judgment-id]'s output positions. In its second +form, produces a list of terms by instantiating the supplied term template with +each satisfying assignment of pattern variables. +See @racket[define-judgment-form] for examples. +} + +@defform[(define-relation language + relation-contract + [(name @#,ttpattern ...) @#,tttterm ...] ...)]{ +Similar to @racket[define-judgment-form] but suitable only when every position +is an input. There is no associated form corresponding to +@racket[judgment-holds]; querying the result uses the same syntax as +metafunction application. + +@examples[ +#:eval redex-eval + (define-language types + ((τ σ) int + num + (τ → τ))) + + (define-relation types + subtype ⊆ τ × τ + [(subtype int num)] + [(subtype (τ_1 → τ_2) (σ_1 → σ_2)) + (subtype σ_1 τ_1) + (subtype τ_2 σ_2)] + [(subtype τ τ)]) + + (term (subtype int num)) + (term (subtype (int → int) (num → num))) + (term (subtype (num → int) (num → num)))] Note that relations are assumed to always return the same results for the same inputs, and their results are cached, unless @@ -1098,7 +1227,7 @@ the same inputs, and their results are cached, unless relation is called with the same inputs twice, then its right-hand sides are evaluated only once. } - + @defparam[current-traced-metafunctions traced-metafunctions (or/c 'all (listof symbol?))]{ Controls which metafunctions are currently being traced. If it is @@ -1940,6 +2069,7 @@ and for use in DrRacket to easily adjust the typesetting: @racket[render-language], @racket[render-reduction-relation], @racket[render-relation], +@racket[render-judgment-form], @racket[render-metafunctions], and @racket[render-lw], and one @@ -1947,6 +2077,8 @@ for use in combination with other libraries that operate on picts @racket[term->pict], @racket[language->pict], @racket[reduction-relation->pict], +@racket[relation->pict], +@racket[judgment-form->pict], @racket[metafunction->pict], and @racket[lw->pict]. The primary difference between these functions is that the former list @@ -2043,12 +2175,7 @@ other tools that combine picts together. @defform[(render-metafunctions metafunction-name ...)]{} @defform/none[#:literals (render-metafunctions) (render-metafunctions metafunction-name ... #:file filename)]{}]]{ - -If provided with one argument, @racket[render-metafunction] -produces a pict that renders properly in the definitions -window in DrRacket. If given two arguments, it writes -postscript into the file named by @racket[filename] (which -may be either a string or bytes). +Like @racket[render-reduction-relation] but for metafunctions. Similarly, @racket[render-metafunctions] accepts multiple metafunctions and renders them together, lining up all of the @@ -2077,23 +2204,32 @@ This function sets @racket[dc-for-text-size]. See also @deftogether[(@defform[(render-relation relation-name)]{} @defform/none[#:literals (render-relation) (render-relation relation-name filename)]{})]{ - -If provided with one argument, @racket[render-relation] -produces a pict that renders properly in the definitions -window in DrRacket. If given two arguments, it writes -postscript into the file named by @racket[filename] (which -may be either a string or bytes). +Like @racket[render-metafunction] but for relations. This function sets @racket[dc-for-text-size]. See also @racket[relation->pict]. } +@deftogether[(@defform[(render-judgment-form judgment-form-name)]{} + @defform/none[#:literals (render-judgment-form) + (render-judgment-form judgment-form-name filename)]{})]{ +Like @racket[render-metafunction] but for judgment forms. + +This function sets @racket[dc-for-text-size]. See also +@racket[relation->pict]. +} + @defform[(relation->pict relation-name)]{ This produces a pict, but without setting @racket[dc-for-text-size]. It is suitable for use in Slideshow or other libraries that combine picts. } +@defform[(judgment-form->pict judgment-form-name)]{ + This produces a pict, but without setting @racket[dc-for-text-size]. + It is suitable for use in Slideshow or other libraries that combine + picts. +} @subsection{Customization} diff --git a/collects/redex/reduction-semantics.rkt b/collects/redex/reduction-semantics.rkt index 4e5fce2685..f213d6d6de 100644 --- a/collects/redex/reduction-semantics.rkt +++ b/collects/redex/reduction-semantics.rkt @@ -28,6 +28,8 @@ define-metafunction define-metafunction/extension define-relation + define-judgment-form + judgment-holds in-domain? caching-enabled? make-coverage) diff --git a/collects/redex/tests/bitmap-test.rkt b/collects/redex/tests/bitmap-test.rkt index 7d917ff198..e304c4ccf5 100644 --- a/collects/redex/tests/bitmap-test.rkt +++ b/collects/redex/tests/bitmap-test.rkt @@ -78,6 +78,19 @@ (test (render-reduction-relation red2) "red2.png") + +(let () + (define-judgment-form lang + mode : I O + [(id e e)]) + (test (render-reduction-relation + (reduction-relation + lang + (--> e_1 + q + (where (name q e_2) e_1) + (judgment-holds (id e_2 (name r e_3)))))) + "red-with-where-name.png")) (define-metafunction lang [(S x v e) e]) @@ -257,5 +270,90 @@ (r x)]) (test (render-relation r) "relation-with-name.png")) +;; judgment form +(let () + (define-language nats + (n z (s n))) + + (define-judgment-form nats + mode : I I O + [(sum z n n)] + [(sum (s n_1) n_2 (s n_3)) + (sum n_1 n_2 n_3)]) + + (test (render-judgment-form sum) "judgment-form-not-rewritten.png") + + (test (with-compound-rewriter + 'sum + (λ (lws) (list "" (list-ref lws 2) " + " (list-ref lws 3) " = " (list-ref lws 4))) + (render-judgment-form sum)) + "judgment-form-rewritten.png") + + (define-judgment-form nats + mode : I O + [(mfw n_1 n_2) + (where n_2 (f n_1))]) + + (define-metafunction nats + [(f n) n]) + + (test (render-judgment-form mfw) "judgment-form-metafunction-where.png") + + (define-judgment-form nats + mode : I O + [(nps (name a (s n_1)) n_2) + (nps z (name n_1 (s (s n_1)))) + (where (name b n_2) z)]) + + (test (render-judgment-form nps) "judgment-form-name-patterns.png")) + +(let () + (define-language STLC + (e (λ (x : τ) e) + (e e) + x) + (x variable-not-otherwise-mentioned) + ((τ σ) b + (τ → τ)) + (Γ ([x τ] ...))) + + (define-judgment-form STLC + mode : I I O + typeof ⊆ Γ × e × τ + [(typeof Γ (e_1 e_2) τ) + (typeof Γ e_1 (τ_2 → τ)) + (typeof Γ e_2 τ_2)] + [(typeof Γ (λ (x : τ) e) (τ → σ)) + (typeof (extend Γ x τ) e σ)] + [(typeof Γ x τ) + (where τ (lookup Γ x))]) + + (define-metafunction STLC + extend : Γ x τ -> Γ + [(extend ([x_1 τ_1] ...) x_0 τ_0) + ([x_0 τ_0] [x_1 τ_1] ...)]) + + (define-metafunction STLC + lookup : Γ x -> τ + [(lookup ([x_0 τ_0] ... [x_i τ_i] [x_i+1 τ_i+1] ...)) τ_i]) + + (define (rewrite-typeof lws) + (list "" (list-ref lws 2) " ⊢ " (list-ref lws 3) " : " (list-ref lws 4))) + + (define (rewrite-extend lws) + (list "" (list-ref lws 2) ", " (list-ref lws 3) ":" (list-ref lws 4))) + + (define (rewrite-lookup lws) + (list "" (list-ref lws 2) "(" (list-ref lws 3) ")")) + + (test (with-compound-rewriter + 'typeof rewrite-typeof + (with-compound-rewriter + 'extend rewrite-extend + (with-compound-rewriter + 'lookup rewrite-lookup + (render-judgment-form typeof)))) + "stlc.png")) + (printf "bitmap-test.rkt: ") -(done) +(done) \ No newline at end of file diff --git a/collects/redex/tests/bmps-macosx/judgment-form-metafunction-where.png b/collects/redex/tests/bmps-macosx/judgment-form-metafunction-where.png new file mode 100644 index 0000000000000000000000000000000000000000..85c4a46ce43a541f5003d5ce14c0b62c9054d637 GIT binary patch literal 1487 zcmV;=1u*)FP)Vy1DrcrwH>iAkEK zD4x~H%)R%#lYuw$4vV5F;1!t7=H1=hxVSj)$oa}-GB3z{{`{FBh@U@yip64)NHj4q zVX;_VzkWS6HD$3_;^N}&-Mi;_f=ZCdeZJ@jYkw{cs zU5&U=kr$bkGG^Sy|!X z;i;*qPo6xnH^e1HXW(b^YG`O^aBy&HYU;qiKz)6EM@NUjV7Pz(zDA?j*w`Ql!q?ZA zF0QGmDJdyoOo)z-c4-~<6i-f0=I7`6e11$!j0cPX0F+84hG9~vRIOG=MMWhgB^iyz zt*tG!TK)a|_qw_|x{|};a5x;7RGm}=00adEefjdGy}jMlX||1-Os3h{*`}r@Hk&;< zI!X`(03a+Zj39{P<70-6&d$!SU%xUYyn6Mjw6xUub=XuyI6XZL4-a>K6oPGIV`F2F zA3uKj^eF&fbaeF1n>Q+zN+1vz42H9_Gm%JSU5w-Sg9i^76Zm|-OY5+wxVpNUoSf{^ zCsPY&M%N76=3afxr#zYZUbC^E1bl z?xkyP!)`3+MtCZ-<{v#4XTXT%d`OaBuV!6_V)DjkR%BJ=b!Jl?;5 zUt3$-*w~0+SaNc5TU%RMSy@q0(em;#xSXHmLSPMuSi&WU*LFOG^;KtgI{?$7g3}S5{Um z7E4A(hCLZZx@I&QuTJ)CPft6J zTu{1JQBlE2*HCO25D?%}Bb{)fEx=>Oa&mGM3PoUGAeYPK^ZDoJ=K})+j*T(WHG&{i zDiyj#$A)^nUM`oPpPygbh!W0+4<9muz`r$?l9Cb@7KXAE7K?@Bcx-HJVq&6$maFMn zLP7!nz&bYU>+8$U&mS5Za;DK{!g&cEe^*}nf;JkBG;eKfg%Hv|<#PG*^0K|jbR&Ax zP!wf0o6(ix;^OY^Zfo*SK7t{H>+91nJ$m%W z-dMWv?c28_BO@gxCEMHE2L}fzjr;ZM7b2*}^9N0hMq@IW003+@8@;d0_g98}oecndUv3#)vk5PuK94cG`(3oZl>X?ab@vTp zsPNe`=}|UZU`0-oo4v8q--_Hy&DxW}*PR~PwQA4ttQ*^^AxF$S@=v&n9DU93D_3kb zRJtJ57EE&IN8L-TcWrT3wmi2@+IaeFh85y}9!rN@8(C>U@-y@q5hIN4wKea*k`2e8 zx?gSUUE*e+1rZ>31Px$jy6^G_4IGAXvXTT zN=}-^X{o73(pG_ijf@FFK|y(Wc^_Y2td@p=GdjrvQ~caI)#znOiCF4OODQN6(!l!o z@#B5R2)V!hirD)}s!}Ufm_q=oWb#E7l_yW02=j2dySp=%HwLm5mX?+Z5pwysw|-NC z;^Hb0-Uf#cp#t0w!ih;s{ZBz5^kPS#nwt9bNmpE+augNwJ#eZ7(}?f+K26NBZuriZ zbiLBLu&{7ot)T9-v|zOiigwl z%ZrS(G~Cco3%t(HKS*1w+%lXpd8t*a&244mxl7aT>S%>}VePwjXVQkJj@v7HT)l#@ zE*f5*n3w?f`Fpa_nXxgatgKAKGQ@%Oj0_D84e-#4va*GR?t~L3P6V`XanIPoYHc%* zRCUE^`#WSJk?5#H;cFKgsP6?2O-f4Q;NXDX8G~YxDSl>u;Yw-?X!{Gcrnqp(~$j z$Lt43Mz$fZT!ip)0iQ`hHmr4Y!#hNMx091lSu#ICv^L%KyNgFluQW*_?tl&Ge=1>u z=Qze+R;Zb^J5+eNiZv6^S*bYa1vM8+vsBD6t)z2BP0!4Lo*J;W?`pjWpFA#|xeC4w zohzVAJ?ku`mvdY;AIG2(RE5(x*x5A$<|%;*#uaNpJ+XmMEiF}tww&r|zt+UW#Ldmk ztgNiZj~}O`9QRbHsj1=R4CoFMz+g0Pldmy=p8;(ZVZyfK}nTMABJ*lms9APZuFXL)%O z1VU+MCQ6-5h&!UHrCmMyX&CAn96a7JNDNeQXbWB+uWoD8Nih;Ub!rTcC#|e_#@%ss zb#-%db98hxG3n2eyA7*H90#sly9WBUL+ni+)j*+8@VY!|N&i_D#!*_C7hC!vZMwgO ztu1)c3p(Exg085jK%>cXVT7GNLyO2>!~0V{mo9@u5Y+qZe&sUCWYHQzx~0Sqfk1Yd z%(y*L{#YCFz1x{?^{npmW}Ucv)wdYT&i1zM&(AWz*Xil?_VkB8K4;Q8m?Py|`1=op z(mqv*iHcs))%C-`&!@7-kBpet!R+C`rDoI%Wd8d4dJqy>7}ej`SC4paZDmEI(Nwbs z)Ya7s4Cb&=VOxuzs%pQJ_o5G5r0%3m`EAf>COQ}l=HdIiPS{xsy3Y&BS2 zRa;wIT|Mdr6-<%U)6-K_^qRJ%yboUcHjj-$*VG8BI;QJKD#2U+>0eq4Zfk9A9U3xY zGMr&q#83a1lghmJEAt(Bd3hIq?VUe=9*@WCiZ`^i6;YG(!sa7hcXYg{2Ga=}Fi~sQ z4DPzP=#rckMwzs-vr8F7-)~S+RXrj%bb1vX?k+uTaKsKG@}57B*;>5O`a-+RQc+kL z-V(zM6@PkKOsu4!pbCbb5_!1RIOV4wvJSa3mYtnFAHM1w5YB&5dD1a1VA?rTFaw@z znpDG2W_M}&9X&}&NjW*LIv$YmxDZsG{ac;(aQ%Z#!=hIPM+ZnC&{lu5@l<02U${Y* z!{fb9e0O*EHIPz+@Ve0G=#sjSicv+u6pDRhWF*|)UN0`m3tE(ulLIcYxrfHjwEDY} zABzU-I6QbDVVoc*CkJYxKqME2oKM%@=Ds-TL-eIK-d+O+*};&G`e0Zr7JppGlTWNL z&Jhp>bUNKz6`A)(fUr}SeimCr9awR)6)apXRgSHNQm08lsG^1AewfYYp_e7)vbl8I z9Tg!PQ_Zhmzg7TmB{ci)HQvXfRDXCv4(mvmn`3=EWnpvgUO9W8Qv5mojGg2Rkqmh? zwaxNm@t@z!Jv}`Uh!Q3V@hA%PONQ!kb#P>4#PdajM_{0uq-0l^MMQje2^SA%PYK7$ z5k!zD@jcG~J7-UHvKt#a>Z;_Q%UW(B&#o5Go>_4ISL@ti_y$0!5v1(mLA@oDPW?d8 z|1;X$$HxbWY{vV{b;Nu?sJw;OMe9p2Y5uvUBmskiM(?p#M4~eWjs+)Ne8RO4I>l*s zc_yWhsJ%xGjQPj!TUnYYlpD$}!-6r-ZC3pCN< z12R5_Nf&}ZfcS1F?XV58vBU0T5f4Xz&V|5oNA{RW|~5w2wjBf?u_3B znIt14^V^Tx&6>r^`ued)hpdw)PXb@Z$Ag!L3WtleEJ%G|6H;!NEFvPJf_S$%pio+( z{qTCZe)MkI&z8Z6OO?sDp!p>1jCQRPwWD&lVOIOeA7jIyySq+h@I?B7bm; zZJpe>EXy~%jh$^S2wj+@Ve2dvO>f^;b!-o3(*3cHwB-u@>BNr8${W&|AdJ64 zsj-&?{5x6uuM;6zzT5fKxaGJZ5Qfii4;mnWP-3ko+*0O+tcIX>Z+iiASZYn z(B1oy{nX%aw@AZxadB~?&ORTMoE#{gYGJ?v>-zpW9xWp+9ZH*LjhaXdxT&{n(X|NC zzZTO}Ul_#AAMS&FguAC_#m}y;F3=*;{7rX|A_r0bdWTE_zU&ldp^x)#k-EzQEzIPz z2i#KA)7?bKWO7tgREUm)wY6YmX;?3V5Z3@hpHIDRk_F;~lbf6Us+E{{0hP6}??;1nM6XoUQnVFg3Q`XpA z$R0@Keb*zq3weY4T#`tgpP8GR14}NjK%)g{7PC2lP+9etknzEYoRj#dE2plWwI`jR f=KKFlJK!MYZ69`?CX&HsAGmeH+^GJ#)1&_Yx4tXX literal 0 HcmV?d00001 diff --git a/collects/redex/tests/bmps-macosx/judgment-form-not-rewritten.png b/collects/redex/tests/bmps-macosx/judgment-form-not-rewritten.png new file mode 100644 index 0000000000000000000000000000000000000000..65ddce9c67922f310630f2e188095eacf3f9795c GIT binary patch literal 2334 zcmbtWc{JPG7EY-tralt9@NkP>s#HY`rBqSX1{L?$|K9uit+USAYn`>%Ui<9t`}RJW&KGSY!7wlg1d_C~ zMY{qv9oR0S0>DX>|MK%f80TPv1|9uer9F=yf)Z zx=4D8=&FDK%DGg*A0q+lv{v#rmsPK+$=ELylh4YzeYXIM%SE3Y`1g_^#>!duG~7j9 zPi8+Ywv;y8XZWspzDhMl-vTzJ>EKl58 zx&!<5wz&4FXYdoR+$J&jr2lR27rRQQ3wEG>dU5?i6(T=PdI$=|@|kWHaB*?b(b0ir zokAje7!1dXiH@$WCg1k^92k?y^zTb5$;na8vme4;x3D0$w%+veQs8FtRfa|A<7T9- z(yA(r2qP1dSAOPEQBgiVJ|q&a+Oa5#jahIQE4T6WeOqREXLfe>#PPkaA7w#U98Lh0 zv%P(Nwv5T#pR9EQs%ep;YU|+OkdV+#rw5==Dd>}#Sy{VVTecT3(h3XDmG1CJ_;l10D|og|@b}&3DJT1<2{<$A6Ok_U#+pEIEcqtVjr0y|aI? zbN{|nA?8s*!3g)pt!mhq@rQYt!kyU?Chq{gOr#W z+Rr|1Z=Ze>6BF}n#U$y6QPEgqO^w$?OIg`5P!5%PQYQ01O#z$l-&^LvTb-M1oSdBS zc>JYHmx#ojk&z6GG7|qsXI>r@WFCL00E3;R*Hl(6j};+WTU*h_H}#Ro!$tO;d-o&^ zi{>ULA+oYS7_M{EFaY~Rh0Vdi!7-4bp`p0A`2765A|fI>Iy!;3wYa&^x6qdy;OS|j z?{M|%`c%DV)8(!Y%ggEyY}IAN_#qhGeDUMtp&_gCowx0gsbum1n|%z#qj%KTKX=E+ zmHKC2?uyxX{UqpZTezw6Syfe44Gj$ggWMq;m&?t|%j@ju@au^BMNKU=_|e_F;4Ew6 z_R>&Ra!34kUC_Ik7QBd*5@~l0Iz&dc(jyI{Is>i1dvcH|`ZumF_w(D&`iELHD@Zdji6ZqcL2CJHa2FK z^h57_b5oO(>WM1`FgHPfTVGY6D0pSHi5=F z%U(Sue@|ILVn48PC5lzt^xxdLGG)oQl%JnJ&f!o4>bkm$C@Q4OspLP+sD9*Lk*8s; z`-7RX`i1xE(7U_4fH2${ZAvikhn+n@Cup|7%c*8J4-cqq}l9DCG#V^LjfGO}YcD|;zcBboAQ;J*KgY`3aXyp7p&d;Rq zSFVgqO?kv$Yb=-?iBZJkS6D2RU{xbC9M1r^0S-2`?lOohyD&^@HiN;yoPrm}-8{VD z4(+ZqyD~)9StY!lVcx8FKRxxik5h?GR#Qv>D7ol4Q2+URS=~F0LzK4MHIx&Z^GL_H zfx)P9)#|NiqfLtwnZ4MFmCBPR`HEOA`WK=!tLd#->|LOi#BHS2$Fv%xwQ| zDL*lHkx~K-WnW)kK$=wVxVSiysWQKZ-B3`AP28|}ae(UJNt0^CvRo8D)BqnIke$^< JbfX29{5PrFa=rin literal 0 HcmV?d00001 diff --git a/collects/redex/tests/bmps-macosx/judgment-form-rewritten.png b/collects/redex/tests/bmps-macosx/judgment-form-rewritten.png new file mode 100644 index 0000000000000000000000000000000000000000..b872e095225aa4ff44ff00601d6c34dcd0cdfc22 GIT binary patch literal 1931 zcmb7_c{JN;7sr1xO2^u%rD&*8DK(*Km8wQ*?P6~&QB_-0wbYKI!hR_VO|s zG5`R`J382Sit|nJ_1F&*zX1bB>cmMZ7-4S%eBV2zorGKfkhXHPxo|nLXt^lL*)vM5 zPjUb0eAQ}S#--8BD2Lj`V@6|7BYz?AtXpDnDDu{2^EN)Bc~o(PSNO*kv+z1E3TYho zJS0x;rESY~+3B8)@G=SGW2IqA3Ty^;>;qg{;lvrNKkr+Lc}ZNcrD&Z?eNFpq86^S0 zB$fFrtyf3nz9?wD*Mx)Ls34)LoI>Zd6dx1exx{}ZeAZr_yTE>p>A+w& zzps|Slgi!o`)~O9`I$zu!5XZQk=I;dTlDPkh8kLNFj-GoMzk`604F3Q@NT#B`TPc) zYUZPrQM`nMhF!%;6BDm0&yjul${DS#txTa-4uMQY8sueXWfhyn=;-Njw?(V(?}zkd z?<#?i1}{NJb$R4&j=-U6G&MCfS+wF|q@MMLfwv4%i{}m(Zwk55Gwmw02Co|Lber

>_>6i!yWG)YJ|)G(4=jU-F~@3?z(r7WnDDy2_qDEMULZ+j*d!6OCQCK)UgDD7_A)9La*$_Ps}pw-+??QFV*h4D{a9(fs#wy z;(&S|ePu2K&lPUQQ#5G}Yin!G&COFP&3?;;CJ`AK88A8C>S}akgkJ4N@PBVXpptB!=_<>d!frNq5RH;el;PUQ6E^pTj8lWie=3JX)=EmZXGo!zbV z_xE>pcKYpXyaFZH4lBbykU@Kh|A(e@lClrE(Vq6>qTN0$H&Lt z=AVEZ9O!-|i@`B9@z&PXs+m>g<)G0&~m(Jef@YI-T1~Z z?3C$?A(ZKh9Pn9Cu3@@OXC^ZU>E&gcaLA^QySpvITO`{lq^*4GxU(Lflti9g#Ujo+ zl+UW%)_jJ+V1gT;A2(_H+rq-a<)h`pm2dFG&!u)1>gwvq)=1=z`ga|V)eq)S6OEx~ zhF8=)XfZniPM?X13Azjac2NpbMzKUfy>H$;z8UgUcI8^i^zzr@a|!YB@kYo$bYoh! zwzksKe+2h2N-SRF=H`}8e;gycrPF@}&o%^Er+VJI%7A8bBKO9hE1RnqW?x_m|B>Z^ zCW)<*N78l3e^e?QJBMc^Y<^iB7#QeL$+8Q%ckkYUxihY3901Pa>q(^S*TvxR@b#?2 zXP$c^9#&STNdTm)l)t8@H9Bf1c{MLzN`fxL#0YA9>a_y`Q7F4(xh~Gm%zge{=-qi5 z_5fY*bbNdY0IEF6QGc5TYi#YJ$^O(^GwsrfT911d=ybZ3_JP%Rs77BgM<0@ZnQVhE z)Vs#yo2}9jN4KcNL^BBFItrEcc_I+@t65R~wJs0n@TSoh3VNXZr{fI|51ft8aVYd%ON7t$>x&~5_DOIp)<%+WX-K@) z^-mMwE$w1M5l=U>Qdyqu5pNVEWQv z0fw`Yq4G<=v1xa!p(T1}PPl3FoHnnWza9M0wWGYeo44-y^<;)$NT@*zo6RPXNNje1 zQ#e=wJH}*+9nk8wS?yIyYiX(WiM?Pf$G=^SC0=$yOSE@uR%zEvg!6bj&U&^hJTk>J zJPSu0*I$2kjVJ-YwHPZilz}D@4XY@H5xe||p*bk0PYF&<6f6k2jC2kThnt?B?iblX z^jAdN(X&)};IVm0gHAd@3J8mc5Z>vW`%c{D6JZ6;@7*#I8(ERPy}dLV4FCvZtf?t8 z3k&%=yZO)aw3e2Z25S{_3+RaIA`LPL8fO#O~z rkt(d1R~ypBz|{W$ohRag literal 0 HcmV?d00001 diff --git a/collects/redex/tests/bmps-macosx/red-with-where-name.png b/collects/redex/tests/bmps-macosx/red-with-where-name.png new file mode 100644 index 0000000000000000000000000000000000000000..b5b3a0d3f5c9aeaa0b4b30e3f815518a25f249cf GIT binary patch literal 2349 zcmV+|3DWk7P)lhM6**A-W=zYTa7r_s2<^uC430)gR95 zAD`!P&inH`=i?mbJRgr51VI1+VWU8)+5v>^h0+6VZf;K55(t|Jr3YMNW86O>}*m}l43P@JYGslN_cpYg}p zVyzlH9xpXDl}e=|k5mKa5YnP9Y4*-D4Wa9C7EEe0<)wO^BeuW4?5R{gdmYkd{ z8@>qJ5L8f5(D3kZL_|bUQ4yER#bU7lfSQ^bI0XMY4Gj%MA`yu;1Q<2hr7bp_9S{&u zQc|*K&z}D-FgG^`2QdNykQ;Ca2+9LlOGVgFkbpzjP>_H_*ievwL)cJI0DzH^5r2Pw zJRVP_QcFuq0|Ek6?G?h71p`6Q$&)9ALLrStV=|eMk&(v6#;W!TVatN4t*!0t?HwE( zgcnI!EEbZ!hM+u9pFe+gaBvVW$saj#M70hfY;92E;{wzdkrLD=%3EG#T~ zdV0iVNgDw{;h;z)5{JVnEGz^73=9lBfBsz6E+K4XP}bJgSy@@p(a|^@&febM%gamE zE+K4XPym3asHoA=(Ym_2(a}*Nk*I2y5VkTH_=k>;&cTBRRqG1Ec0hV*3yZ}X8XBs^ z6@={ok`K3KfgosRW=2a(OHEBpvVMMkULX*tDhGQFi}yuEMQAj-tE)?S-XJIt4u_+y ztu6bVtGc?{$;k<}-QC?oLPE;Q%3NGrU}JJ}QX%T!zI}V~;st>~NK8zGjqL1fu%>{c zP$(D-Mj_rHYybuZ29=eSEB>DVnM^)=_ADBWh7CPEJ%y+{IyzFR)T2j_nwy)$2K+2t zTY3@-rQmcXRVAvZM0a|6+Re?awYBxknKSq9-BY$4pU=<8$e5Uz003|}oS>i}8ylP8 z;NYR5A!W!dH9GMF9X9?6pu)mJLqo%7&z`Z_Y!43)CnqN+lL-L0aN$B`W+vR{>({TR zPoFk2GAb@EhHL8T>Y}2e+}+*bduByNg}1l&%a(c9a*wYBx?)vH=s zS_ugW%8*;-=>B;`QYe(<lqi7JVSiTU~Y zQk4k_370QlmaJLR-YBZlg$WD{q|s;_CInwq+O`!)c;-roMhhYv9^F~-KmzP`SP4ojWxVSh9g(6jH zVqzj$l-(PpySw|>uU|wW5sgO6j#+uSOYO-biJzaJY~}jo_6|M@L6KpI=^HPN7hWi;KOyygWTUrMjuB zs|$rf005K8^!4=(4GjeVBqt}sttb=<-ZesQtC-a!s^D-q91ge40A%+@nVg*b{rh)& zdwXYR=ZzaTWDil2E?9a`7D;yQ+^HzJsi`SzYwNpr@201xFLUg~#Khjcd&R{S6KvNp zrOS^_66t`mva&jK=um!szK)L0#fuk1LqjnbOloTCQpX=SaGjEIOhckUc)%kGV$si{dM5~ru9m%4;X(uI+`C(DYg zPmaN0yng+f!C)+Za!X6gyu3W2PzZlyXl!g;zW+L=boI#j%n=qAcIC>IpFe+^nVF%{ zXfzrPzh6KQBoc|>8=Fulgbfmj zSQru#0w=1--fTQPJj~6_r7G?0?8LU*y-~Pa?%doQ{HN>K*jP(T3yDM$zhWy-S8`7l zS>0t=pWONL=WA+ehK7dlc>FSQ{{H?+NlA1%JuED&t*x!HvQqLlM3!|-=^B7!;PH6T z(b2G-mX_Ar+Y8%tIvoHI7Z=Cna${p-0RW|?r6Q3iBqRg?U~6l8?bXGW zGMW76&mY-VDXpBG98FD4Q&Ur2UEQFdAOe9P>(BE1{rh*{zJ1~0;dDB^rKJUepoN76 zI-L$d(ER*71VK-pJOKbO7z}0WLJ*Xmp5D~d1lzK@@E3|7KYpxLYbiMhf-*8Prl+Un z%CXsO06=$lHv~bsxw#q|8s_HaIyyQxZ{8G-*UilhK16KD)mqJz${ih)5el0LXi!s)~}55@%=U?W4OrL9#^A!=;+vQ z>u4B)V+D9*KFJ-zMK(kaC+;QNZ~)B zld2Vv8h+~*uaI~Qxp!Nkg7bow4|ZF~4k(9%xaRwZS8a@>A(G)(2W%F#d|C6Gd^m)G~DbT^U9 z3s_&;KK^fQ?p1T=eKU|?`?@Y}a< z3#0=5wW74tR9U{eK0dNm3@o0gl-l43GrV0?TG~S-5~-)B=ird9Cqi2Ak@p~{msGGZ zh3Sdt>glEX%L#^uhJ|gR4zq7X?(!Kpk-C|-)wsC0E(i-pCC9|XY;A2}8H-KJuk*5v zh8viem>3$i&4kc)R{OqunI==*u4`*)aj>(mbBDaoPmZ7w*b=&Yjt=&gmfR3x(L9pA zNMs6~W@kr7L}cXL&!1*4#_;4~WAU8XmB|LvvPYcJ9i;rb4QQILj?U+aI`5|{_ix|s zS{kdAfBIb`xO;JzlarJ3oZ8bFb8eaT2m^INasGNv=Fvc-4_jMXuaq|;_=UM*{F=sw zhkdt~%)|RXf7Y?I6fhz@C^k_!+$3SHPEJmalw0j=ZFN}H)YRnXcKXW8cD zPf{gd2U=RP79M}uRhXTfeevQ2Khe>KK7VAG*(ODwv&=vzM1A z0O>7mp&HTt{=4zo0@*%g<>f8D%c=I=M*1qVD=TFKPOmU8UoxFPf8NT9k|3&oA>5%S zmHXVe2J26uJeK}1p6CDx#i{O#ks1=$kth@@G&EEpwyzDMC)pj|U%-RwEzrp}aHBLo zzQ~oKfJ77zZE&rpc{B(78ZND>suI?YW#iyL`TGlofB*iSo`GQ@!`sVidu7sf?82Go zYceu$t7g5bT^j9Nj8@$v0T?WV0M>&uUJ131R8>XjvbWDFS!{V*pn&;v_)NCpYqqy)zvjJ zI%S_7NhJrava_?Fjp+oX1CdhsE+e2@J3Ahe^;^-B&7OXKb7)U(sa|HB^7BxL&3S_R zBv8WU#zyK7YE4xYgo){O$27BQISf`M7!q}&`G`p;M39b45K2dfeW7{jCcXPvI%XK; zCOzbjw{+@s7a{v2=Gs3?shJ~vfi=xA*gSXWPUAD}pIg+-Qb{QP`mBWHS{k7@&{B4*L0S=!aAaW9UuBPab5& zOXcUs-u>^lXPqNx@IT z(`a>bjKCj&Lsb z-o(;A>Ep+qdfVQs5cRHKbIrOTDpMJk9%kttHP8hZKwj9Gd3#fLD8U|Er4I@2z*{M` z$R}Ub$>^QQXTOFoUAlBgTWvw3(J3h@sHV(S9npjnSJYop8jmiglpb3%)AOGCbXELC z7vsNLb`$pBI{1HnDdfPW6u-Ri?ba((s3Tq_!wV|Q9=!a$8dy`y(f*Yqd{NQu@{!1h zh#MNangJ-zs;n}4lDtV-q+n-Tv#Z0hoDep%c^UB7PZV9Zs6gu3hK^!`xXX+ z2_|&4wY6d3kHux>1Z~JN*FDIOOiYF+Cwp+gC{#UY=k4183wg;B<4TH(&(UaBR@QUp z&JjySFC^UoKja)4=K}T^#MIac`4qiw%+>J}*IwKx2Xr zw~~hlZXZY6Z~`$y^s-BZLyPa<3nCtZ>VWv>yng&8TuZ!%*^mZ{lai7gD#!5a(;d+u z^nqWyRM$5({TZ)IP{^@mHTr{(9<_{}pLeqD-s_0wk>iVbKtu@%N~l*P$K43n_+TvF z!5s!OEHV}n5@HGy5)%_sRaKRj=dlX3z_=qdI?fc^+e>7R#41kXr7+p5rT`GE1>r`5B8|Z66T>Tz^E!6dJxc*9*5k4SL1HL@cjJzYy%XO zm6xWbq%&obeWcjV@$y=4#O6b8N+~M3Tu&>wo7VZ{Vxw@a9E24VrI-+6$+0j}5}xeBbVd8W6W8SW~Bh2(M$^U-5{{);MqY$kp>Ow+pg*)t#{ zq<}31G9mNZkU}5;nEnW*`jJsDyS`VHe3xL+9pXtJ8yaX?!AC%If!j;C@kV<oFJHPbamNfr0z_`h6gsRw66j z8;g&WJ?_pcxO;|NvyZ0QDm4cmAC;6yJdDG)r%o`b^TudNN|uL)(&u#8$=rY5S;LhfzHE)eGDL+HW z&x=2$sM1)xr?1a3ZftRkXm@;c2oCsX>0~!GHGQ3FXlR&|lasHXRW{^8RQ}6a%GlWWYnps{US1v^FQcGP zTU_k=mHKgLv7(~Fz8j-*u-3l5z7F=Ubv$@?DiVw3Esm_JsX6n{&3(KkrinUY68>qH67xC8l!2Oic>h4IHb{hX0s@(diB%pH)q27CNWs6KKGc(XI)`_e>Z!UN-9VAQ z^tZHp!tILyt`Hs`|A|(c={DO>Z6%{X`bzb)O?{nHGoSB8$Jsrnfs;;iiLT{fv{ANP%Hm_cD`2L||ay3n$5}np{;lc$h z*YOx3LOS9LlxGNZ9|D2Y*4JY&7!D2&{ASexj+z^%YABwxdkl1y8Mty|x^#aZ1&kO> z0Qt9mqaq+2Rvx%DFD50W4z;xifX+~nhnu^uu5O@jd}v56_~_v2c#WLA{Hd67kQS0H z2Z)6+5@}|2H7hk0wYz51eFZbr%loovcRKof(5_H7(N2-3Fow792JH|0(fZ=UhYx_V zy9ro?y{$}X=H;M?8Uch3$xdc$k)S92!vVLJ-w-~&xO4Xy8(VQa{A;Vdy**J2V~~Qi zTlF}j<}Ps3hA6`7K|5#;h)ZGJj!@jYk>tCJ)X#|^Oa@U7I=?c~5E;+a=|T}Vt%4a4 zbpKDG=_q4>Tx=wPJ2t- z0|K(zqLj3ty8DA6KUa$FAf7ZN)wjnD{2jj~B`7jvkC9BtAwNxe| zZ1+1vcD-2tof7vN1-bCTb=0!2*7up;hCF2YH^%;6DH`;p6&c>N6!wN>C4`lk7gd5g z+KVguTJ*d>$;v9MsFOEnRB-Pu&Lf*YoYV($LNWMAIbJmmX3^-6n>lje=HcN1zLAjd zWK7`*P1p8m!Q(6#sKLa9xs1OM|JnVw>qj7_mX}LSiuJQp50@(YEL(ym@$DZU6ibw= zK(oPxTUc1w*w~20V*AvNAC;OYmGkwVuC;d~H-h=Eq@f`#FV0vzNeg>S+5@ZtPVh8K$M*8L=7oW%Q=(NC%eyCx|0hkD zUd-v$zjv<};Q8g4qoX6O-23q46A;K7wKrWI3p_~&IYTavJ*g2enY13Q+=0o-j6wDC zk%oo_QkLz@$Ve4s<#~E9#owD=U@F@x3BvrZ<39qX$(-*>b6$ZzY3Oci-qR>UScm=x DPNn1_ literal 0 HcmV?d00001 diff --git a/collects/redex/tests/run-err-tests/judgment-form-contracts.rktd b/collects/redex/tests/run-err-tests/judgment-form-contracts.rktd new file mode 100644 index 0000000000..aaf217461c --- /dev/null +++ b/collects/redex/tests/run-err-tests/judgment-form-contracts.rktd @@ -0,0 +1,12 @@ +(#rx"input q at position 1" + ([judgment ctc-fail]) + (judgment-holds (judgment q s))) +(#rx"output q at position 2" + ([judgment ctc-fail]) + (judgment-holds (judgment a s))) +(#rx"input q at position 1" + ([judgment ctc-fail]) + (judgment-holds (judgment b s))) +(#rx"output q at position 2" + ([judgment ctc-fail]) + (judgment-holds (judgment c s))) \ No newline at end of file diff --git a/collects/redex/tests/run-err-tests/judgment-form-undefined.rktd b/collects/redex/tests/run-err-tests/judgment-form-undefined.rktd new file mode 100644 index 0000000000..f62ed62914 --- /dev/null +++ b/collects/redex/tests/run-err-tests/judgment-form-undefined.rktd @@ -0,0 +1,9 @@ +("judgment form q applied before its definition" + ([use q]) ([def q]) + (let () + (judgment-holds (use 1)) + (define-language L) + (define-judgment-form L + mode : I + [(def 1)]) + #f)) \ No newline at end of file diff --git a/collects/redex/tests/run-err-tests/term.rktd b/collects/redex/tests/run-err-tests/term.rktd new file mode 100644 index 0000000000..0a6e36dd15 --- /dev/null +++ b/collects/redex/tests/run-err-tests/term.rktd @@ -0,0 +1,42 @@ +(#rx"incompatible ellipsis match counts" + ([body (((x y) ...) ...)]) + ([xlhs (x ...)] [ylhs ((y ...) ...)]) + (term-let ([xlhs '(a b c)] + [ylhs '((1 2) (4 5 6) (7 8 9))]) + (term body))) + +(#rx"incompatible ellipsis match counts" + ([body ((((f x) y) ...) ...)]) + ([fn f] [xlhs (x ...)] [ylhs ((y ...) ...)]) + (term-let-fn ([fn car]) + (term-let ([xlhs '(a b c)] + [ylhs '((1 2) (4 5 6) (7 8 9))]) + (term body)))) + +(#rx"incompatible ellipsis match counts" + ([body (f ((x y) ...))]) + ([fn f] [xlhs (x ...)] [ylhs (y ...)]) + (term-let-fn ([fn car]) + (term-let ([xlhs '(a b)] + [ylhs '(c d e)]) + (term body)))) + +(#rx"incompatible ellipsis match counts" + ([app (f (x y))]) + ([fn f] [xlhs (x ...)] [ylhs (y ...)] [ellipsis ...]) + (term-let-fn ([fn car]) + (term-let ([xlhs '(a b)] + [ylhs '(c d e)]) + (term (app ellipsis))))) + +(#rx"incompatible ellipsis match counts" + ([plug (in-hole hole (x y))]) + ([xlhs (x ...)] [ylhs (y ...)] [ellipsis ...]) + (term-let-fn ([fn car]) + (term-let ([xlhs '(a b)] + [ylhs '(c d e)]) + (term (plug ellipsis))))) + +(#rx"term .* does not match pattern" + ([rhs 'a]) ([ellipsis ...]) + (term-let ([(x ellipsis) rhs]) 3)) \ No newline at end of file diff --git a/collects/redex/tests/run-tests.rkt b/collects/redex/tests/run-tests.rkt index e960ce43e0..bf23e79d8f 100644 --- a/collects/redex/tests/run-tests.rkt +++ b/collects/redex/tests/run-tests.rkt @@ -1,6 +1,6 @@ ;; require this file to run all of the test suites for redex. -#lang scheme/base +#lang racket/base (require scheme/runtime-path scheme/cmdline scheme/match diff --git a/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd b/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd new file mode 100644 index 0000000000..d3abcfad3c --- /dev/null +++ b/collects/redex/tests/syn-err-tests/judgment-form-definition.rktd @@ -0,0 +1,103 @@ +(#rx"expected a mode" + ([bad-def (define-judgment-form syn-err-lang)]) + bad-def) +(#rx"expected a mode" + ([mode-kw mode]) + (define-judgment-form syn-err-lang mode-kw)) +(#rx"expected a clause" + ([junk 1]) + (define-judgment-form syn-err-lang + mode : junk + [(q 1)])) +(#rx"expected at least one clause" + ([bad-def (define-judgment-form syn-err-lang mode :)]) + bad-def) +(#rx"expected a pattern to follow" + ([cross ×]) + (define-judgment-form syn-err-lang + mode : I + J ⊆ number cross)) +(#rx"use the same name" + ([name1 J] [name2 K]) + (define-judgment-form syn-err-lang + mode : I + name1 ⊆ number + [(name2 number)])) +(#rx"malformed premise" + ([bad-prem (q)]) + (let () + (define-judgment-form syn-err-lang + mode : I + [(J number) + bad-prem]) + (void))) +(#rx"different numbers of positions" + ([bad-def (define-judgment-form syn-err-lang + mode : I + J ⊆ number × number + [(J number)])]) + bad-def) + +(#rx"unbound pattern variable" + ([unbound number_2]) + (let () + (define-judgment-form syn-err-lang + mode : I O + [(J number_1 unbound) + (J number_1 number_1)]) + (void))) +(#rx"unbound pattern variable" + ([unbound number_2]) + (let () + (define-judgment-form syn-err-lang + mode : I O + [(J number_1 number_2) + (J unbound number_1)]) + (void))) +(#rx"unbound pattern variable" + ([unbound number_3]) + (let () + (define-judgment-form syn-err-lang + mode : I O + [(J number_1 number_2) + (where number_2 unbound)]) + (void))) +(#rx"unbound pattern variable" + ([unbound q]) + (let () + (define-judgment-form syn-err-lang + mode : I O + [(J number_1 number_2) + (where number_2 unbound) + (where (name q number) number_1)]) + (void))) +(#rx"arity" + ([bad-conc (J)]) + (let () + (define-judgment-form syn-err-lang + mode : I + [bad-conc]) + (void))) +(#rx"arity" + ([bad-prem (J)]) ([name J]) + (let () + (define-judgment-form syn-err-lang + mode : I + [(name number) + bad-prem]) + (void))) +(#rx"unquote unsupported" + ([unq ,(+ 1)]) + (let () + (define-judgment-form syn-err-lang + mode : I + [(uses-unquote n) + (where n unq)]) + (void))) +(#rx"unquote unsupported" + ([unq ,'z]) + (let () + (define-judgment-form syn-err-lang + mode : I O + [(uses-unquote n unq)]) + (void))) \ No newline at end of file diff --git a/collects/redex/tests/syn-err-tests/judgment-holds.rktd b/collects/redex/tests/syn-err-tests/judgment-holds.rktd new file mode 100644 index 0000000000..2907d2aff2 --- /dev/null +++ b/collects/redex/tests/syn-err-tests/judgment-holds.rktd @@ -0,0 +1,3 @@ +(#rx"expected a judgment form name" + ([not-judgment-form junk]) + (judgment-holds (not-judgment-form z (s z)))) \ No newline at end of file diff --git a/collects/redex/tests/syn-err-tests/language-definition.rktd b/collects/redex/tests/syn-err-tests/language-definition.rktd new file mode 100644 index 0000000000..b6da94b31f --- /dev/null +++ b/collects/redex/tests/syn-err-tests/language-definition.rktd @@ -0,0 +1,25 @@ +(#rx"define-language:.*unquote disallowed" + ([illegal-unquote ,3]) + (let () + (define-language L + (n illegal-unquote)) + (void))) + +; error message shows correct form name +(#rx"define-extended-language:.*underscore" + ([bad-underscore y_1]) + (let () + (define-language L) + (define-extended-language M L + (z () (1 bad-underscore))) + (void))) + +(#rx"expected an identifier" ([not-id (L)]) (define-language not-id)) +(#rx"expected at least one production" ([separator ::=]) (define-language L (x separator))) +(#rx"expected at least one production" ([nt x]) (define-language L (nt))) +(#rx"expected at least one production" ([nt-pos (x)]) (define-language L (nt-pos))) +(#rx"expected preceding non-terminal names" ([separator ::=]) (define-language L (separator a b))) +(#rx"expected non-terminal name" ([not-nt (y)]) (define-language L (x not-nt ::= z))) +(#rx"expected production" ([not-prod ::=]) (define-language L (x ::= y not-prod z))) +(#rx"expected non-terminal definition" ([not-def q]) (define-language L not-def)) +(#rx"expected non-terminal definition" ([not-def ()]) (define-language L not-def)) \ No newline at end of file diff --git a/collects/redex/tests/syn-err-tests/metafunction-definition.rktd b/collects/redex/tests/syn-err-tests/metafunction-definition.rktd new file mode 100644 index 0000000000..b9c72c6c47 --- /dev/null +++ b/collects/redex/tests/syn-err-tests/metafunction-definition.rktd @@ -0,0 +1,11 @@ +(#rx"expected a pattern and a right-hand side" + ([clause [(f x)]]) + (define-metafunction syn-err-lang + clause)) + +(#rx"expected an identifier" + ([not-id (junk)]) + (define-metafunction not-id also-junk)) +(#rx"expected an identifier" + ([not-id junk]) + (define-metafunction not-id also-junk)) \ No newline at end of file diff --git a/collects/redex/tests/syn-err-tests/redex-let.rktd b/collects/redex/tests/syn-err-tests/redex-let.rktd new file mode 100644 index 0000000000..1e25f97940 --- /dev/null +++ b/collects/redex/tests/syn-err-tests/redex-let.rktd @@ -0,0 +1,3 @@ +(#rx"redex-let: duplicate pattern variable" + ([dup number]) + (redex-let syn-err-lang ([(dup) 1] [dup 1]) (term dup))) \ No newline at end of file diff --git a/collects/redex/tests/syn-err-tests/reduction-relation-definition.rktd b/collects/redex/tests/syn-err-tests/reduction-relation-definition.rktd new file mode 100644 index 0000000000..32bbd3c688 --- /dev/null +++ b/collects/redex/tests/syn-err-tests/reduction-relation-definition.rktd @@ -0,0 +1,126 @@ +(#rx"no rules" + ([unused ==>]) + (reduction-relation + syn-err-lang + (~~> (number_1 number_2) + ,(* (term number_1) (term number_2))) + with + [(--> (M a) (M b)) (~~> a b)] + [(~~> (M a) (M b)) (unused a b)])) + +(#rx"no rules use -->" + ([bad-def (reduction-relation syn-err-lang)]) + bad-def) + +(#rx"~~> relation is not defined" + ([undef ~~>]) + (reduction-relation + syn-err-lang + (undef (number_1 number_2) + ,(* (term number_1) (term number_2))))) + +(#rx"same name on multiple rules" + ([name1 mult] [name2 mult]) + (reduction-relation + syn-err-lang + (--> (number_1 number_2) + ,(* (term number_1) (term number_2)) + name2) + (--> (number_1 number_2) + ,(* (term number_1) (term number_2)) + name1))) + + +(#rx"different depths" + ([binder2 number_1] [binder1 number_1]) ([ellipsis ...]) + (reduction-relation + syn-err-lang + (--> binder1 + () + (where (binder2 ellipsis) '())))) + +(#rx"different depths" + ([binder1 x] [binder2 x]) ([ellipsis ...]) + (redex-match + syn-err-lang + ((name binder1 any) (name binder2 any_2) ellipsis))) + +(#rx"different depths" + ([binder1 x] [binder2 x]) ([ellipsis ...]) + (let () + (define-language bad-lang5 + (e ((name binder1 any) (name binder2 any_2) ellipsis))) + (void))) + +(#rx"==> relation is not defined" + ([undef ==>]) + (reduction-relation + syn-err-lang + (--> 1 2) + (undef 3 4))) + +(#rx"~> relation is not defined" + ([undef ~>]) + (reduction-relation + syn-err-lang + (--> 1 2) + (==> 3 4) + with + [(undef a b) (==> a b)])) + +(#rx"expected identifier" + ([not-id (+ 3 b)]) + (reduction-relation + syn-err-lang + (==> 1 2) + with + [(--> a b) + (==> a not-id)])) + +(#rx"expected identifier" + ([not-id (+ 3 a)]) + (reduction-relation + syn-err-lang + (==> 1 2) + with + [(--> a b) + (==> not-id b)])) + +(#rx"name expected to have arguments" + ([name-kw name]) + (let () (define-language bad-lang1 (e name-kw)) (void))) +(#rx"name expected to have 2 arguments" + ([bad-pat (name x)]) + (let () (define-language bad-lang2 (e bad-pat)) (void))) +(#rx"cannot use _" ([bad-underscore x_y]) (define-language bad-lang3 (bad-underscore x))) +(#rx"at least one production" ([nt b]) (define-language bad-lang4 (a 1 2) (nt))) +(#rx"at least one production" + ([nt a]) + (let () + (define-language good-lang (nt 1 2)) + (define-extended-language bad-lang5 good-lang (nt) (b 2)) + (void))) +(#rx"same non-terminal" + ([nt2 x] [nt1 x]) + (define-language bad-lang5 (nt1 1) (nt2 2))) +(#rx"same non-terminal" + ([nt2 x] [nt1 x]) + (define-language bad-lang6 ((nt1 nt2) 1))) +(#rx"same non-terminal" + ([nt2 x] [nt1 x]) + (let () + (define-language good-lang) + (define-extended-language bad-lang7 good-lang ((nt1 nt2) 1)))) + +(#rx"before underscore" + ([bad-underscore m_1]) + (redex-match syn-err-lang bad-underscore)) +(#rx"expected an identifier" + ([not-id 2]) + (redex-match syn-err-lang (variable-except a not-id c))) +(#rx"expected an identifier" + ([not-id 7]) + (redex-match syn-err-lang (variable-prefix not-id))) +(#rx"expected an identifier" + ([not-id 7]) + (redex-match syn-err-lang (cross not-id))) \ No newline at end of file diff --git a/collects/redex/tests/syn-err-tests/relation-definition.rktd b/collects/redex/tests/syn-err-tests/relation-definition.rktd new file mode 100644 index 0000000000..f63798e65b --- /dev/null +++ b/collects/redex/tests/syn-err-tests/relation-definition.rktd @@ -0,0 +1,15 @@ +(#rx"expected the name of the relation" + ([bad-def (define-relation syn-err-lang R)]) + bad-def) + +(#rx"expected a sequence of patterns separated by" + ([subset ⊂]) + (define-relation syn-err-lang R subset)) + +(#rx"expected clause definitions" + ([bad-def (define-relation syn-err-lang foo ⊆ c)]) + bad-def) + +(#rx"expected a pattern" + ([cross ×]) + (define-relation syn-err-lang foo ⊆ c cross)) \ No newline at end of file diff --git a/collects/redex/tests/syn-err-tests/term.rktd b/collects/redex/tests/syn-err-tests/term.rktd new file mode 100644 index 0000000000..1b1742566c --- /dev/null +++ b/collects/redex/tests/syn-err-tests/term.rktd @@ -0,0 +1,8 @@ +(#rx"missing ellipses" + ([id-no-ellipsis x]) ([ellipsis ...]) + (term-let ([(id-no-ellipsis ellipsis) '(a b c)]) (term id-no-ellipsis))) + +(#rx"too few ellipses" + ([bound x]) ([bind x]) + (... (term-let ([((bind ...) ...) '()]) + (term (bound ...))))) \ No newline at end of file diff --git a/collects/redex/tests/term-test.rkt b/collects/redex/tests/term-test.rkt index 8aafb83614..4b6bfb91a8 100644 --- a/collects/redex/tests/term-test.rkt +++ b/collects/redex/tests/term-test.rkt @@ -103,81 +103,9 @@ (define-namespace-anchor here) (define ns (namespace-anchor->namespace here)) - (let ([src 'term-template]) - (test - (parameterize ([current-namespace ns]) - (runtime-error-source - '(term-let ([(x ...) '(a b c)] - [((y ...) ...) '((1 2) (4 5 6) (7 8 9))]) - (term (((x y) ...) ...))) - src)) - src)) + (parameterize ([current-namespace ns]) + (exec-runtime-error-tests "run-err-tests/term.rktd")) - (let ([src 'term-template-metafunc]) - (test - (parameterize ([current-namespace ns]) - (runtime-error-source - '(term-let-fn ((f car)) - (term-let ([(x ...) '(a b c)] - [((y ...) ...) '((1 2) (4 5 6) (7 8 9))]) - (term ((((f x) y) ...) ...)))) - src)) - src)) - - (let ([src 'ellipsis-args]) - (test - (parameterize ([current-namespace ns]) - (runtime-error-source - '(term-let-fn ((f car)) - (term-let ([(x ...) '(a b)] - [(y ...) '(c d e)]) - (term (f ((x y) ...))))) - src)) - src)) - - (let ([src 'ellipsis-args/map]) - (test - (parameterize ([current-namespace ns]) - (runtime-error-source - '(term-let-fn ((f car)) - (term-let ([(x ...) '(a b)] - [(y ...) '(c d e)]) - (term ((f (x y)) ...)))) - src)) - src)) - - (let ([src 'ellipsis-args/in-hole]) - (test - (parameterize ([current-namespace ns]) - (runtime-error-source - '(term-let ([(x ...) '(a b)] - [(y ...) '(c d e)]) - (term ((in-hole hole (x y)) ...))) - src)) - src)) - - (let ([src 'term-let-rhs]) - (test - (parameterize ([current-namespace ns]) - (runtime-error-source - '(term-let ([(x ...) 'a]) - 3) - src)) - src)) - - (test-syn-err (term-let ([(x ...) '(a b c)]) (term x)) - #rx"missing ellipses") - - (test (parameterize ([current-namespace syn-err-test-namespace]) - (with-handlers ([exn:fail:syntax? - (λ (exn) - (match (exn:fail:syntax-exprs exn) - [(list e) (syntax->datum e)] - [_ (gensym 'wrong)]))]) - (expand - '(term-let ([((label ...) ...) '()]) - (term (label ...)))) - (gensym 'wrong))) - 'label) + (exec-syntax-error-tests "syn-err-tests/term.rktd") (print-tests-passed 'term-test.rkt)) diff --git a/collects/redex/tests/test-util.rkt b/collects/redex/tests/test-util.rkt index 70345d86fa..693e15caba 100644 --- a/collects/redex/tests/test-util.rkt +++ b/collects/redex/tests/test-util.rkt @@ -3,18 +3,29 @@ (require "../private/matcher.rkt" (for-syntax syntax/parse) errortrace/errortrace-lib - errortrace/errortrace-key) + errortrace/errortrace-key + racket/runtime-path) (provide test test-syn-err tests reset-count syn-err-test-namespace print-tests-passed equal/bindings? test-contract-violation - runtime-error-source) + test-runtime-err + exec-syntax-error-tests + exec-runtime-error-tests) + +(define-runtime-path this-dir ".") (define syn-err-test-namespace (make-base-namespace)) (parameterize ([current-namespace syn-err-test-namespace]) (eval '(require redex/reduction-semantics))) +(define (read-syntax-test path) + (call-with-input-file path + (λ (port) + (port-count-lines! port) + (read-syntax path port)))) + (define-syntax (test stx) (syntax-case stx () [(_ expected got) @@ -24,40 +35,90 @@ "")]) (syntax/loc stx (test/proc (λ () expected) got line fn)))])) -(define (runtime-error-source sexp src) - (let/ec return - (cadar - (continuation-mark-set->list - (exn-continuation-marks - (with-handlers ((exn:fail? values)) - (parameterize ([current-compile (make-errortrace-compile-handler)]) - (eval (read-syntax src (open-input-string (format "~s" sexp))))) - (return 'no-source))) - errortrace-key)))) +(define (syntax-error-test-setup thunk) + (parameterize ([current-namespace syn-err-test-namespace]) + (with-handlers ([exn:fail:syntax? + (λ (exn) + (values (exn-message exn) + (map source-location (exn:fail:syntax-exprs exn))))]) + (thunk)))) +(define (runtime-error-test-setup thunk) + (parameterize ([current-compile (make-errortrace-compile-handler)]) + (with-handlers ([exn:fail? + (λ (exn) + (values (exn-message exn) + (let ([marks (continuation-mark-set->list + (exn-continuation-marks exn) + errortrace-key)]) + (if (null? marks) '() (list (cdar marks))))))]) + (thunk)))) + +(define ((exec-error-tests setup exec) path) + (for ([test (read-tests (build-path this-dir path))]) + (exec-error-test test exec setup))) +(define exec-syntax-error-tests + (exec-error-tests syntax-error-test-setup expand)) +(define exec-runtime-error-tests + (exec-error-tests runtime-error-test-setup eval)) + +(define (exec-error-test spec exec setup) + (define-values (file line expected-message expected-sources test) + (make-error-test spec)) + (let-values ([(actual-message actual-sources) + (setup (λ () (begin (exec test) (values "" '()))))]) + (test/proc (λ () actual-message) expected-message line file) + (test/proc (λ () actual-sources) expected-sources line file))) + +(define (make-error-test spec) + (syntax-case spec () + [(message named-pieces body) + (make-error-test (syntax/loc spec (message named-pieces () body)))] + [(message ([loc-name loc-piece] ...) ([non-loc-name non-loc-piece] ...) body) + (values (syntax-source spec) + (syntax-line spec) + (syntax-e #'message) + (map source-location (syntax->list #'(loc-piece ...))) + #'(let-syntax ([subst + (λ (stx) + (syntax-case stx () + [(_ loc-name ... non-loc-name ...) + #'body]))]) + (subst loc-piece ... non-loc-piece ...)))])) + +(define (source-location stx) + (list (syntax-source stx) + (syntax-line stx) + (syntax-column stx) + (syntax-position stx) + (syntax-span stx))) + +(define (read-tests path) + (call-with-input-file path + (λ (port) + (port-count-lines! port) + (let loop () + (define test (read-syntax path port)) + (if (eof-object? test) + '() + (cons test (loop))))))) (define-syntax (test-syn-err stx) - (syntax-case stx () - [(_ exp msg-re num-locs) - (with-syntax ([expected-locs (syntax/loc stx (build-list num-locs (λ (_) src)))]) - (syntax - (let* ([src (gensym)] - [p (read-syntax src (open-input-string (format "~s" 'exp)))]) - (let-values ([(locs msg) - (with-handlers ([exn:fail:syntax? - (λ (exn) - (values - (if (exn:srclocs? exn) - (map srcloc-source - ((exn:srclocs-accessor exn) exn)) - null) - (exn-message exn)))]) - (parameterize ([current-namespace syn-err-test-namespace]) - (expand p)) - (values (void) null))]) - (test msg msg-re) - (test locs expected-locs)))))] - [(tse exp msg-re) - (syntax/loc stx (tse exp msg-re 1))])) + #'(void)) + +(define-syntax (test-runtime-err stx) + #'(void) + #; + #`(parameterize ([current-compile (make-errortrace-compile-handler)]) + #,(test-error-location + stx + eval + #'[exn:fail? + (λ (exn) + (values (exn-message exn) + (let ([marks (continuation-mark-set->list + (exn-continuation-marks exn) + errortrace-key)]) + (if (null? marks) #f (list (cdar marks))))))]))) (define tests 0) (define failures 0) diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt index 9e69999e17..e0f2cd4df8 100644 --- a/collects/redex/tests/tl-test.rkt +++ b/collects/redex/tests/tl-test.rkt @@ -1,8 +1,9 @@ -#lang racket/gui +#lang racket (require "../reduction-semantics.rkt" "test-util.rkt" (only-in "../private/matcher.rkt" make-bindings make-bind) racket/match + racket/trace "../private/struct.rkt") (reset-count) @@ -10,7 +11,7 @@ (define-namespace-anchor this-namespace) (parameterize ([current-namespace syn-err-test-namespace]) (eval (quote-syntax - (define-language grammar + (define-language syn-err-lang (M (M M) number) (E hole @@ -101,22 +102,7 @@ 12))) '("....")) - (test-syn-err - (let () - (define-language L - (n ,3)) - (void)) - #rx"define-language:.*unquote disallowed" 1) - (let () - ; error message shows correct form name - (test-syn-err - (let () - (define-language L) - (define-extended-language M L - (z () (1 y_1))) - (void)) - #rx"define-extended-language:.*underscore") ; non-terminals added by extension can have underscores (define-extended-language L base-grammar (z () (1 z_1 z_1))) @@ -411,15 +397,7 @@ (::= () (number ::=))) (test (and (redex-match L ::= '(1 ())) #t) #t))) - (test-syn-err (define-language (L)) #rx"expected an identifier") - (test-syn-err (define-language L (x ::=)) #rx"expected at least one production") - (test-syn-err (define-language L (x)) #rx"expected at least one production") - (test-syn-err (define-language L ((x))) #rx"expected at least one production") - (test-syn-err (define-language L (::= a b)) #rx"expected preceding non-terminal names") - (test-syn-err (define-language L (x (y) ::= z)) #rx"expected non-terminal name") - (test-syn-err (define-language L (x ::= y ::= z)) #rx"expected production") - (test-syn-err (define-language L q) #rx"expected non-terminal definition") - (test-syn-err (define-language L ()) #rx"expected non-terminal definition") + (exec-syntax-error-tests "syn-err-tests/language-definition.rktd") ; ; ; ;;; ; @@ -1001,11 +979,10 @@ ;; errors for not-yet-defined metafunctions (test (parameterize ([current-namespace (make-empty-namespace)]) - (namespace-attach-module (namespace-anchor->namespace this-namespace) 'racket/gui) (namespace-attach-module (namespace-anchor->namespace this-namespace) 'redex/reduction-semantics) (namespace-require 'racket) (eval '(module m racket - (require redex) + (require redex/reduction-semantics) (term (q)) (define-language L) (define-metafunction L [(q) ()]))) @@ -1021,17 +998,7 @@ #f)) "metafunction q applied before its definition") - (let () - (test-syn-err - (define-metafunction grammar - [(f x)]) - #rx"expected a pattern and a right-hand side")) - - (test-syn-err (define-metafunction (junk) also-junk) - #rx"expected an identifier") - (test-syn-err (define-metafunction junk also-junk) - #rx"expected an identifier") - + (exec-syntax-error-tests "syn-err-tests/metafunction-definition.rktd") ; ; ; @@ -1123,21 +1090,7 @@ 'failed) 'passed)) - (test-syn-err - (define-relation grammar R) - #rx"expected the name of the relation") - - (test-syn-err - (define-relation grammar R ⊆) - #rx"expected a sequence of patterns separated by") - - (test-syn-err - (define-relation grammar foo ⊆ c) - #rx"expected clause definitions") - - (test-syn-err - (define-relation grammar foo ⊆ c ×) - #rx"expected a pattern") + (exec-syntax-error-tests "syn-err-tests/relation-definition.rktd") ; ;; ; ;; ; ; ; ; ; ; @@ -1547,112 +1500,7 @@ (test (apply-reduction-relation R (term (0 2 3 4 5))) '()) (test (apply-reduction-relation R (term (1 2 3 4 5 () (6) (7 8) (9 10 11)))) '(yes))) - (test-syn-err (reduction-relation - grammar - (~~> (number_1 number_2) - ,(* (term number_1) (term number_2))) - with - [(--> (M a) (M b)) (~~> a b)] - [(~~> (M a) (M b)) (==> a b)]) - #rx"no rules") - - (test-syn-err (reduction-relation - grammar - (~~> (number_1 number_2) - ,(* (term number_1) (term number_2))) - with - [(--> (M a) (M b)) (~~> a b)] - [(~~> (M a) (M b)) (==> a b)]) - #rx"no rules") - - (test-syn-err (reduction-relation grammar) - #rx"no rules use -->") - - (test-syn-err (reduction-relation - grammar - (~~> (number_1 number_2) - ,(* (term number_1) (term number_2)))) - #rx"~~> relation is not defined") - - (test-syn-err (reduction-relation - grammar - (--> (number_1 number_2) - ,(* (term number_1) (term number_2)) - mult) - (--> (number_1 number_2) - ,(* (term number_1) (term number_2)) - mult)) - #rx"same name on multiple rules" - 2) - - (test-syn-err (reduction-relation - grammar - (--> number_1 - () - (where (number_1 ...) '()))) - #rx"different depths" - 2) - - (test-syn-err (redex-match - grammar - ((name x any) (name x any_2) ...)) - #rx"different depths" - 2) - - (test-syn-err (define-language bad-lang5 - (e ((name x any) (name x any_2) ...))) - #rx"different depths" - 2) - - (test-syn-err (reduction-relation - grammar - (--> 1 2) - (==> 3 4)) - #rx"==> relation is not defined") - - (test-syn-err (reduction-relation - grammar - (--> 1 2) - (==> 3 4) - with - [(~> a b) (==> a b)]) - #rx"~> relation is not defined") - - (test-syn-err (reduction-relation - grammar - (==> 1 2) - with - [(--> a b) - (==> a (+ 3 b))]) - #rx"expected identifier") - - (test-syn-err (reduction-relation - grammar - (==> 1 2) - with - [(--> a b) - (==> (+ 3 a) b)]) - #rx"expected identifier") - - (test-syn-err (define-language bad-lang1 (e name)) #rx"name") - (test-syn-err (define-language bad-lang2 (name x)) #rx"name") - (test-syn-err (define-language bad-lang3 (x_y x)) #rx"cannot use _") - (test-syn-err (define-language bad-lang4 (a 1 2) (b)) #rx"at least one production") - (test-syn-err (let () - (define-language good-lang (a 1 2)) - (define-extended-language bad-lang5 good-lang (a) (b 2))) - #rx"at least one production") - (test-syn-err (define-language bad-lang5 (x 1) (x 2)) #rx"same non-terminal" 2) - (test-syn-err (define-language bad-lang6 ((x x) 1)) #rx"same non-terminal" 2) - (test-syn-err (let () - (define-language good-lang) - (define-extended-language bad-lang7 good-lang ((x x) 1))) - #rx"same non-terminal" 2) - - (test-syn-err (redex-match grammar m_1) #rx"before underscore") - (test-syn-err (redex-match grammar (variable-except a 2 c)) #rx"expected an identifier") - (test-syn-err (redex-match grammar (variable-prefix 7)) #rx"expected an identifier") - (test-syn-err (redex-match grammar (cross 7)) #rx"expected an identifier") + (exec-syntax-error-tests "syn-err-tests/reduction-relation-definition.rktd") ;; expect union with duplicate names to fail (test (with-handlers ((exn? (λ (x) 'passed))) @@ -1957,7 +1805,19 @@ (--> q r y) (--> r p x)))) '(a b c z y x)) - + + (let () + (define-judgment-form empty-language + mode : I O + [(R a a)] + [(R a b)]) + (test (apply-reduction-relation + (reduction-relation + empty-language + (--> a any + (judgment-holds (R a any)))) + 'a) + '(b a))) ; ; @@ -2003,13 +1863,186 @@ (test (redex-let L ([(n_1 n_1) '(1 1)]) (term n_1)) 1) - (test-syn-err - (redex-let grammar ([(number) 1] [number 1]) (term number)) - #rx"redex-let: duplicate pattern variable" 1) (test (redex-let* L ([(n_1) '(1)] [n_1 1]) (term n_1)) - 1)) + 1) + (exec-syntax-error-tests "syn-err-tests/redex-let.rktd")) + +; +; +; +; ; ;; ; ; ; ;; +; ; ; ; ; ; ; ; +; ; ; ; ; ; +; ;;;; ;;; ;;; ; ;;;; ;;; ; ; ; ;;;; ;;;; ;;;;; ;;; ;;;; ;;; ;;; ;;; ; ;; ;;;;; +; ; ; ; ; ; ; ; ; ; ; ;;;;; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;;;;; ; ; ; ;; ; ; ; ; +; ; ; ;;;;; ; ; ; ; ;;;;; ; ; ; ; ; ; ; ; ; ; ;;;;; ; ; ; ; ; ; ; ; ; ; ; +; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; +; ; ; ; ; ; ; ; ; ; ; ; ; ;; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; +; ;;;; ;;; ; ; ; ; ;;; ; ;; ; ;;;; ;;;; ; ; ; ;;; ; ; ;; ; ;;; ; ; ; ; +; ; ; +; ; ; ; +; ;; ;;; + + (exec-syntax-error-tests "syn-err-tests/judgment-form-definition.rktd") + (exec-syntax-error-tests "syn-err-tests/judgment-holds.rktd") + + (let () + (define-language nats + (n z (s n))) + + (define-judgment-form nats + mode : I I O + sumi ⊆ n × n × n + [(sumi z n n)] + [(sumi (s n_1) n_2 (s n_3)) + (sumi n_1 n_2 n_3)]) + (test (judgment-holds (sumi z (s z) n) n) + (list (term (s z)))) + (test (judgment-holds (sumi (s (s z)) (s z) n) n) + (list (term (s (s (s z)))))) + (test (judgment-holds (sumi ,'z (s z) (s z))) #t) + + (define-judgment-form nats + mode : O O I + sumo ⊆ n × n × n + [(sumo z n n)] + [(sumo (s n_1) n_2 (s n_3)) + (sumo n_1 n_2 n_3)]) + (test (judgment-holds (sumo n_1 n_2 z) ([,'n_1 n_1] [,'n_2 n_2])) + (list (term ([n_1 z] [n_2 z])))) + (test (judgment-holds (sumo n_1 n_2 (s z)) ([,'n_1 n_1] [,'n_2 n_2])) + (list (term ([n_1 (s z)] [n_2 z])) + (term ([n_1 z] [n_2 (s z)])))) + + (define-judgment-form nats + mode : O O I + [(sumo-ls (s n_1) n_2 n_3) + (sumo (s n_1) n_2 n_3)]) + (test (judgment-holds (sumo-ls n_1 n_2 (s z)) ([,'n_1 n_1] [,'n_2 n_2])) + (list (term ([n_1 (s z)] [n_2 z])))) + (test (judgment-holds (sumo-ls (s n_1) n_2 (s z))) #t) + (test (judgment-holds (sumo-ls z n_2 (s z))) #f) + (test (judgment-holds (sumo-ls z n_2 (s z)) whatever) (list)) + + (define-judgment-form nats + mode : O O I + [(sumo-lz z n_2 n_3) + (sumo z n_2 n_3)]) + (test (judgment-holds (sumo-lz n_1 n_2 (s z)) ([,'n_1 n_1] [,'n_2 n_2])) + (list (term ([n_1 z] [n_2 (s z)])))) + + (define-judgment-form nats + mode : O I + [(member n_i (n_0 ... n_i n_i+1 ...))]) + + (test (judgment-holds (member n (z (s z) z (s (s z)))) n) + (list (term (s (s z))) (term z) (term (s z)) (term z))) + + (define-judgment-form nats + mode : I + [(has-zero (n ...)) + (member z (n ...))]) + + (test (judgment-holds (has-zero ((s z) z (s (s z))))) #t) + + (define-judgment-form nats + mode : I + [(le2 n) + (le (add2 n) (s (s (s (s z)))))]) + + (define-judgment-form nats + mode : I I + [(le z n)] + [(le (s n_1) (s n_2)) + (le n_1 n_2)]) + + (define-metafunction nats + add2 : n -> n + [(add2 n) (s (s n))]) + + (test (judgment-holds (le2 (s (s z)))) #t) + (test (judgment-holds (le2 (s (s (s z))))) #f) + + (define-judgment-form nats + mode : I O + uses-add2 ⊆ n × n + [(uses-add2 n_1 n_2) + (sumo n_2 n_3 n_1) + (where n_2 (add2 n_3))]) + + (test (judgment-holds (uses-add2 (s (s (s (s z)))) n) n) + (list (term (s (s (s z)))))) + + (let-syntax ([test-trace + (syntax-rules () + [(_ expr trace-spec expected) + (test (let ([trace (open-output-string)]) + (parameterize ([current-output-port trace] + [current-traced-metafunctions trace-spec]) + expr) + (get-output-string trace)) + expected)])]) + (test-trace (judgment-holds (sumi (s z) (s (s z)) n) n) + '(sumi) + #reader scribble/reader + @string-append{>(sumi '(s z) '(s (s z)) '_) + > (sumi 'z '(s (s z)) '_) + < '((sumi z (s (s z)) (s (s z)))) + <'((sumi (s z) (s (s z)) (s (s (s z))))) + + }) + (test-trace (judgment-holds (sumo n_1 n_2 (s z))) + 'all + #reader scribble/reader + @string-append{>(sumo '_ '_ '(s z)) + > (sumo '_ '_ 'z) + < '((sumo z z z)) + <'((sumo (s z) z (s z)) (sumo z (s z) (s z))) + + }) + (test-trace (letrec ([f (match-lambda + ['z #t] + [`(s ,n) (f n)])]) + (define-judgment-form nats + mode : I I + [(ext-trace z (side-condition n (f (term n))))] + [(ext-trace (s n_1) n_2) + (ext-trace n_1 n_2)]) + (trace f) + (judgment-holds (ext-trace (s z) (s z)))) + 'all + #reader scribble/reader + @string-append{>(ext-trace '(s z) '(s z)) + > (ext-trace 'z '(s z)) + > >(f '(s z)) + > >(f 'z) + < <#t + < '((ext-trace z (s z))) + <'((ext-trace (s z) (s z))) + + }))) + + (parameterize ([current-namespace (make-base-namespace)]) + (eval '(require redex/reduction-semantics)) + (eval '(define-language L + (s a b c))) + (eval '(define-judgment-form L + mode : I O + ctc-fail ⊆ s × s + [(ctc-fail a q)] + [(ctc-fail b s) + (ctc-fail q s)] + [(ctc-fail c s) + (ctc-fail a s)])) + (exec-runtime-error-tests "run-err-tests/judgment-form-contracts.rktd") + (exec-runtime-error-tests "run-err-tests/judgment-form-undefined.rktd")) + + (parameterize ([current-namespace (make-base-namespace)]) + (eval '(require redex/reduction-semantics)) + (exec-runtime-error-tests "run-err-tests/judgment-form-undefined.rktd")) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; examples from doc.txt