Adds define-judgment-form form
This commit is contained in:
Casey Klein
parent
8887ea2ef3
commit
576272362b
|
|
@ -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?))))]
|
||||
|
|
|
|||
17
collects/redex/private/defined-checks.rkt
Normal file
17
collects/redex/private/defined-checks.rkt
Normal file
|
|
@ -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))
|
||||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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,8 +929,7 @@
|
|||
scs
|
||||
rhss))))])))
|
||||
|
||||
(define (metafunction-call name an-lw flattened?)
|
||||
(if flattened?
|
||||
(define (metafunction-call name an-lw)
|
||||
(struct-copy lw an-lw
|
||||
[e
|
||||
(list*
|
||||
|
|
@ -949,34 +950,7 @@
|
|||
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))))
|
||||
(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))]))
|
||||
|
||||
;
|
||||
;
|
||||
;
|
||||
|
|
|
|||
|
|
@ -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,37 +327,12 @@
|
|||
(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
|
||||
(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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]))]
|
||||
|
|
|
|||
|
|
@ -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))))
|
||||
|
|
@ -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 ...)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
@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.
|
||||
|
||||
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))]
|
||||
|
||||
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))]
|
||||
|
||||
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)))]
|
||||
|
||||
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 ...] ...)
|
||||
([relation-contract (code:line)
|
||||
(code:line id ⊂ pat x ... x pat)
|
||||
(code:line id ⊆ pat × ... × pat)])]{
|
||||
[(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.
|
||||
|
||||
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|.
|
||||
@examples[
|
||||
#:eval redex-eval
|
||||
(define-language types
|
||||
((τ σ) int
|
||||
num
|
||||
(τ → τ)))
|
||||
|
||||
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).
|
||||
(define-relation types
|
||||
subtype ⊆ τ × τ
|
||||
[(subtype int num)]
|
||||
[(subtype (τ_1 → τ_2) (σ_1 → σ_2))
|
||||
(subtype σ_1 τ_1)
|
||||
(subtype τ_2 σ_2)]
|
||||
[(subtype τ τ)])
|
||||
|
||||
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.
|
||||
|
||||
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.
|
||||
(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
|
||||
|
|
@ -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,12 +2204,16 @@ 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)]{})]{
|
||||
Like @racket[render-metafunction] but for relations.
|
||||
|
||||
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).
|
||||
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].
|
||||
|
|
@ -2094,6 +2225,11 @@ This function sets @racket[dc-for-text-size]. See also
|
|||
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}
|
||||
|
||||
|
|
|
|||
|
|
@ -28,6 +28,8 @@
|
|||
define-metafunction
|
||||
define-metafunction/extension
|
||||
define-relation
|
||||
define-judgment-form
|
||||
judgment-holds
|
||||
in-domain?
|
||||
caching-enabled?
|
||||
make-coverage)
|
||||
|
|
|
|||
|
|
@ -79,6 +79,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)
|
||||
Binary file not shown.
|
After Width: | Height: | Size: 1.5 KiB |
BIN
collects/redex/tests/bmps-macosx/judgment-form-name-patterns.png
Normal file
BIN
collects/redex/tests/bmps-macosx/judgment-form-name-patterns.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 3.0 KiB |
BIN
collects/redex/tests/bmps-macosx/judgment-form-not-rewritten.png
Normal file
BIN
collects/redex/tests/bmps-macosx/judgment-form-not-rewritten.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 2.3 KiB |
BIN
collects/redex/tests/bmps-macosx/judgment-form-rewritten.png
Normal file
BIN
collects/redex/tests/bmps-macosx/judgment-form-rewritten.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 1.9 KiB |
BIN
collects/redex/tests/bmps-macosx/red-with-where-name.png
Normal file
BIN
collects/redex/tests/bmps-macosx/red-with-where-name.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 2.3 KiB |
BIN
collects/redex/tests/bmps-macosx/stlc.png
Normal file
BIN
collects/redex/tests/bmps-macosx/stlc.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 4.5 KiB |
|
|
@ -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)))
|
||||
|
|
@ -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))
|
||||
42
collects/redex/tests/run-err-tests/term.rktd
Normal file
42
collects/redex/tests/run-err-tests/term.rktd
Normal file
|
|
@ -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))
|
||||
|
|
@ -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
|
||||
|
|
|
|||
103
collects/redex/tests/syn-err-tests/judgment-form-definition.rktd
Normal file
103
collects/redex/tests/syn-err-tests/judgment-form-definition.rktd
Normal file
|
|
@ -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)))
|
||||
3
collects/redex/tests/syn-err-tests/judgment-holds.rktd
Normal file
3
collects/redex/tests/syn-err-tests/judgment-holds.rktd
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
(#rx"expected a judgment form name"
|
||||
([not-judgment-form junk])
|
||||
(judgment-holds (not-judgment-form z (s z))))
|
||||
25
collects/redex/tests/syn-err-tests/language-definition.rktd
Normal file
25
collects/redex/tests/syn-err-tests/language-definition.rktd
Normal file
|
|
@ -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))
|
||||
|
|
@ -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))
|
||||
3
collects/redex/tests/syn-err-tests/redex-let.rktd
Normal file
3
collects/redex/tests/syn-err-tests/redex-let.rktd
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
(#rx"redex-let: duplicate pattern variable"
|
||||
([dup number])
|
||||
(redex-let syn-err-lang ([(dup) 1] [dup 1]) (term dup)))
|
||||
|
|
@ -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)))
|
||||
15
collects/redex/tests/syn-err-tests/relation-definition.rktd
Normal file
15
collects/redex/tests/syn-err-tests/relation-definition.rktd
Normal file
|
|
@ -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))
|
||||
8
collects/redex/tests/syn-err-tests/term.rktd
Normal file
8
collects/redex/tests/syn-err-tests/term.rktd
Normal file
|
|
@ -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 ...)))))
|
||||
|
|
@ -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))
|
||||
(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))
|
||||
|
|
|
|||
|
|
@ -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 @@
|
|||
"<unknown file>")])
|
||||
(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 (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)
|
||||
(define (syntax-error-test-setup thunk)
|
||||
(parameterize ([current-namespace syn-err-test-namespace])
|
||||
(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))]))
|
||||
(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)
|
||||
#'(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)
|
||||
|
|
|
|||
|
|
@ -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)))
|
||||
|
|
@ -1958,6 +1806,18 @@
|
|||
(--> 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,12 +1863,185 @@
|
|||
|
||||
(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"))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;;
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user