added contracts to define-relation.
(also removed old, wrong tl-pat stuff from the docs)
This commit is contained in:
Robby Findler
parent
4c081c127a
commit
8bf096b1e3
|
|
@ -1438,23 +1438,55 @@
|
|||
[else
|
||||
(syntax-case rest ()
|
||||
[(id colon more ...)
|
||||
(begin
|
||||
(unless (eq? ': (syntax-e #'colon))
|
||||
(raise-syntax-error syn-error-name "expected a colon to follow the meta-function's name" stx #'colon))
|
||||
(let loop ([more (syntax->list #'(more ...))]
|
||||
[dom-pats '()])
|
||||
(cond
|
||||
[(null? more)
|
||||
(raise-syntax-error syn-error-name "expected an ->" stx)]
|
||||
[(eq? (syntax-e (car more)) '->)
|
||||
(when (null? (cdr more))
|
||||
(raise-syntax-error syn-error-name "expected a range contract to follow the arrow" stx (car more)))
|
||||
(let ([doms (reverse dom-pats)]
|
||||
[codomain (cadr more)]
|
||||
[clauses (check-clauses stx syn-error-name (cddr more) relation?)])
|
||||
(values #'id doms codomain clauses))]
|
||||
[else
|
||||
(loop (cdr more) (cons (car more) dom-pats))])))]
|
||||
(identifier? #'id)
|
||||
(cond
|
||||
[relation?
|
||||
(unless (memq (syntax-e #'colon) '(⊂ ⊆))
|
||||
(raise-syntax-error syn-error-name
|
||||
"expected ⊂ or ⊆ to follow the relation's name"
|
||||
stx #'colon))
|
||||
(let ([more (syntax->list #'(more ...))])
|
||||
(when (null? more)
|
||||
(raise-syntax-error syn-error-name
|
||||
(format "expected a sequence of patterns separated by x or × to follow ~a"
|
||||
(syntax-e #'colon))
|
||||
stx))
|
||||
(let loop ([more (cdr more)]
|
||||
[arg-pats (list (car more))])
|
||||
(cond
|
||||
[(null? more)
|
||||
(raise-syntax-error syn-error-name
|
||||
"expected clause definitions to follow domain contract"
|
||||
stx)]
|
||||
[(memq (syntax-e (car more)) '(x ×))
|
||||
(when (null? (cdr more))
|
||||
(raise-syntax-error syn-error-name
|
||||
(format "expected a pattern to follow ~a" (syntax-e (car more)))
|
||||
stx))
|
||||
(loop (cddr more)
|
||||
(cons (cadr more) arg-pats))]
|
||||
[else
|
||||
(values #'id
|
||||
(reverse arg-pats)
|
||||
#'any
|
||||
(check-clauses stx syn-error-name more relation?))])))]
|
||||
[else
|
||||
(unless (eq? ': (syntax-e #'colon))
|
||||
(raise-syntax-error syn-error-name "expected a colon to follow the meta-function's name" stx #'colon))
|
||||
(let loop ([more (syntax->list #'(more ...))]
|
||||
[dom-pats '()])
|
||||
(cond
|
||||
[(null? more)
|
||||
(raise-syntax-error syn-error-name "expected an ->" stx)]
|
||||
[(eq? (syntax-e (car more)) '->)
|
||||
(when (null? (cdr more))
|
||||
(raise-syntax-error syn-error-name "expected a range contract to follow the arrow" stx (car more)))
|
||||
(let ([doms (reverse dom-pats)]
|
||||
[codomain (cadr more)]
|
||||
[clauses (check-clauses stx syn-error-name (cddr more) relation?)])
|
||||
(values #'id doms codomain clauses))]
|
||||
[else
|
||||
(loop (cdr more) (cons (car more) dom-pats))]))])]
|
||||
[_
|
||||
(raise-syntax-error
|
||||
syn-error-name
|
||||
|
|
@ -1492,7 +1524,7 @@
|
|||
(λ (x)
|
||||
(syntax-case x ()
|
||||
[(stuff ...) (void)]
|
||||
[x (raise-syntax-error syn-error-name "expected a metafunction clause" stx #'x)]))
|
||||
[x (raise-syntax-error syn-error-name "expected a clause" stx #'x)]))
|
||||
(syntax->list #'(x ...)))
|
||||
(raise-syntax-error syn-error-name "error checking failed.2" stx))]))
|
||||
|
||||
|
|
|
|||
|
|
@ -682,15 +682,13 @@ all non-GUI portions of Redex) and also exported by
|
|||
[extras rule-name
|
||||
(fresh fresh-clause ...)
|
||||
(side-condition racket-expression)
|
||||
(where tl-pat @#,tttterm)
|
||||
(where pat @#,tttterm)
|
||||
(side-condition/hidden racket-expression)
|
||||
(where/hidden tl-pat @#,tttterm)]
|
||||
(where/hidden pat @#,tttterm)]
|
||||
[rule-name identifier
|
||||
string
|
||||
(computed-name racket-expression)]
|
||||
[fresh-clause var ((var1 ...) (var2 ...))]
|
||||
[tl-pat identifier (tl-pat-ele ...)]
|
||||
[tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{
|
||||
[fresh-clause var ((var1 ...) (var2 ...))])]{
|
||||
|
||||
Defines a reduction relation casewise, one case for each of the
|
||||
clauses beginning with @racket[-->] (or with @racket[arrow], if
|
||||
|
|
@ -930,17 +928,15 @@ all non-GUI portions of Redex) and also exported by
|
|||
|
||||
@defform/subs[#:literals (: -> where side-condition side-condition/hidden where/hidden)
|
||||
(define-metafunction language
|
||||
contract
|
||||
metafunction-contract
|
||||
[(name @#,ttpattern ...) @#,tttterm extras ...]
|
||||
...)
|
||||
([contract (code:line)
|
||||
(code:line id : @#,ttpattern ... -> @#,ttpattern)]
|
||||
([metafunction-contract (code:line)
|
||||
(code:line id : @#,ttpattern ... -> @#,ttpattern)]
|
||||
[extras (side-condition racket-expression)
|
||||
(side-condition/hidden racket-expression)
|
||||
(where tl-pat @#,tttterm)
|
||||
(where/hidden tl-pat @#,tttterm)]
|
||||
[tl-pat identifier (tl-pat-ele ...)]
|
||||
[tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{
|
||||
(where pat @#,tttterm)
|
||||
(where/hidden pat @#,tttterm)])]{
|
||||
|
||||
The @racket[define-metafunction] form builds a function on
|
||||
sexpressions according to the pattern and right-hand-side
|
||||
|
|
@ -1013,7 +1009,7 @@ match.
|
|||
}
|
||||
|
||||
@defform[(define-metafunction/extension f language
|
||||
contract
|
||||
metafunction-contract
|
||||
[(g @#,ttpattern ...) @#,tttterm extras ...]
|
||||
...)]{
|
||||
|
||||
|
|
@ -1047,8 +1043,9 @@ and @racket[#f] otherwise.
|
|||
@defform/subs[#:literals ()
|
||||
(define-relation language
|
||||
[(name @#,ttpattern ...) @#,tttterm ...] ...)
|
||||
([tl-pat identifier (tl-pat-ele ...)]
|
||||
[tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{
|
||||
([relation-contract (code:line)
|
||||
(code:line id ⊂ pat x ... x pat)
|
||||
(code:line id ⊆ pat × ... × pat)])]{
|
||||
|
||||
The @racket[define-relation] form builds a relation on
|
||||
sexpressions according to the pattern and right-hand-side
|
||||
|
|
@ -1067,6 +1064,11 @@ 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.
|
||||
|
||||
Note that relations are assumed to always return the same results for
|
||||
the same inputs, and their results are cached, unless
|
||||
@racket[caching-enable?] is set to @racket[#f]. Accordingly, if a
|
||||
|
|
|
|||
|
|
@ -899,6 +899,36 @@
|
|||
(test (term (<: 1 2 2)) #f)
|
||||
(test (term (<: 1 1 1)) #t))
|
||||
|
||||
(let ()
|
||||
(define-relation empty-language
|
||||
d ⊆ any × any
|
||||
[(d (any) (any)) (d any any)]
|
||||
[(d () ())])
|
||||
|
||||
(test (term (d ((())) ((())))) #t)
|
||||
(test (term (d ((())) ())) #f))
|
||||
|
||||
(let ()
|
||||
(define-relation empty-language
|
||||
d ⊂ any x any
|
||||
[(d (any) (any)) (d any any)]
|
||||
[(d () ())])
|
||||
|
||||
(test (term (d ((())) ((())))) #t)
|
||||
(test (term (d ((())) ())) #f))
|
||||
|
||||
(let ()
|
||||
(define-relation empty-language
|
||||
d ⊂ (any)
|
||||
[(d (1))])
|
||||
|
||||
(test (term (d (1))) #t)
|
||||
(test (term (d (2))) #f)
|
||||
(test (with-handlers ((exn:fail? (λ (x) 'passed)))
|
||||
(term (d 1))
|
||||
'failed)
|
||||
'passed))
|
||||
|
||||
|
||||
; ;; ; ;; ;
|
||||
; ; ; ; ;
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user