Fixes domain checking of unioned reduction relations

This commit is contained in:
Casey Klein 2011-05-06 16:46:47 -05:00
parent 33c848fcda
commit dd58b457a9
2 changed files with 18 additions and 13 deletions

View File

@ -68,20 +68,17 @@
language combined-rules combined-rule-names lws
(map (λ (rule)
(define specialized (rule language))
(define (f-with-contract t)
(unless (match-pattern compiled-domain t)
(error 'reduction-relation "relation reduced to ~s via ~a, which is outside its domain"
t
(let ([name (rewrite-proc-name rule)])
(if name
(format "the rule named ~a" name)
"an unnamed rule"))))
t)
(λ (tl-exp exp f acc)
(unless (match-pattern compiled-domain tl-exp)
(error 'reduction-relation "relation not defined for ~s" tl-exp))
(let ([ress (specialized tl-exp exp f acc)])
(for-each
(λ (res)
(let ([term (caddr res)])
(unless (match-pattern compiled-domain term)
(error 'reduction-relation "relation reduced to ~s via ~a, which is outside its domain"
term
(let ([name (rewrite-proc-name rule)])
(if name
(format "the rule named ~a" name)
"an unnamed rule"))))))
ress)
ress)))
(specialized tl-exp exp f-with-contract acc)))
combined-rules)))

View File

@ -1317,6 +1317,14 @@
'x)
(list 'a 'b 'c 'd))
(let ([R (reduction-relation empty-language #:domain number (--> 1 a "first"))]
[S (reduction-relation empty-language (--> 2 a "second"))])
(test (apply-reduction-relation (union-reduction-relations R S) 2)
(list 'a))
(test (apply-reduction-relation (union-reduction-relations S R) 2)
(list 'a)))
(test (apply-reduction-relation
(reduction-relation
empty-language