suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Fixes define-relation's handling of ellipses across clauses

Browse Source 
closes PR 12378
This commit is contained in:
Robby Findler 2011-11-17 16:59:36 -06:00
parent 36a408096c
commit 755dc28e55
2 changed files with 32 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
collects/redex/private/reduction-semantics.rkt
View File

@ -1438,7 +1438,7 @@
(with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
[(lhs-for-lw ...) (lhs-lws pats)])
(with-syntax ([((rhs stuff ...) ...) (if relation?
#'((,(and (term raw-rhses) ...)) ...)
#'(((AND raw-rhses ...)) ...)
#'((raw-rhses ...) ...))]
[(lhs ...) #'((lhs-clauses ...) ...)])
(parse-extras #'((stuff ...) ...))
@ -2920,3 +2920,12 @@
covered-cases
(rename-out [fresh-coverage make-coverage])
coverage?)
;; the AND metafunction is defined here to be used
;; in define-relation so that ellipses work properly
;; across clauses in relations
(define-language L)
(define-metafunction L
AND : any ... -> any
[(AND any ...)
,(andmap values (term (any ...)))])

22
collects/redex/tests/tl-test.rkt
View File

@ -1117,6 +1117,28 @@
'failed)
'passed))
(let ()
(define-language types
((τ σ) int
num
(τ ... → τ)))
(define-relation types
subtype ⊆ τ × τ
[(subtype int num)]
[(subtype (τ_1 ..._1 → τ_2) (σ_1 ..._1 → σ_2))
(subtype σ_1 τ_1) ...
(subtype τ_2 σ_2)]
[(subtype τ τ)])
(test (term (subtype int int)) #t)
(test (term (subtype int num)) #t)
(test (term (subtype (int int int → int) (int int → int))) #f)
(test (term (subtype (int int → int) (int num → int))) #f)
(test (term (subtype (int num → int) (int int → int))) #t)
(test (term (subtype (int int → int) (int int → num))) #t))
(exec-syntax-error-tests "syn-err-tests/relation-definition.rktd")
; ;; ; ;; ;