redex: elminate another #f/failure confusion

(cherry picked from commit 468d2b192e)
This commit is contained in:
Burke Fetscher 2013-04-10 12:59:15 -05:00 committed by Ryan Culpepper
parent 7fa5db7b63
commit cf78ce0c6e
2 changed files with 26 additions and 9 deletions

View File

@ -186,7 +186,7 @@
[(cons (eqn lhs rhs) rest) [(cons (eqn lhs rhs) rest)
(eqn lhs rhs) (eqn lhs rhs)
(define u-res (unify lhs rhs e lang)) (define u-res (unify lhs rhs e lang))
(and u-res (and (not-failed? u-res)
(loop (p*e-e u-res) rest))]))] (loop (p*e-e u-res) rest))]))]
[else #f])])) [else #f])]))

View File

@ -15,8 +15,9 @@
(define-syntax-rule (is-false e) (define-syntax-rule (is-false e)
(test e #f)) (test e #f))
(define-language L0)
(let () (let ()
(define-language L0)
(test (check-dq (dq '() (list `a `a)) (make-hash) L0 (hash)) (test (check-dq (dq '() (list `a `a)) (make-hash) L0 (hash))
#f) #f)
@ -590,7 +591,6 @@
(g))))) (g)))))
(let () (let ()
(define-language L0)
(define-relation L0 (define-relation L0
[(a any)]) [(a any)])
(define-relation L0 (define-relation L0
@ -629,9 +629,6 @@
(let () (let ()
(define-language L0)
(define-relation L0 (define-relation L0
[(R number) [(R number)
number] number]
@ -677,7 +674,6 @@
(is-not-false (generate-term L0 #:satisfying (J ((#t) (2))) 5))) (is-not-false (generate-term L0 #:satisfying (J ((#t) (2))) 5)))
(let () (let ()
(define-language L0)
(define-metafunction L0 (define-metafunction L0
[(f (any_1 any_2)) [(f (any_1 any_2))
@ -713,7 +709,6 @@
[else #t])))) [else #t]))))
(let () (let ()
(define-language L0)
(define-relation L0 (define-relation L0
[(R (#f #f #f) 3)] [(R (#f #f #f) 3)]
@ -754,4 +749,26 @@
#:satisfying #:satisfying
(R #f any) (R #f any)
+inf.0)) +inf.0))
) )
(let ()
(define-relation L0
[(not-mem any_1 (any_2 any_3))
(not-mem any_1 any_3)
(where (any_!_4 any_!_4) (any_1 any_2))]
[(not-mem any_1 ())])
(is-not-false
(generate-term
L0
#:satisfying
(not-mem d (a (b (c ()))))
+inf.0))
(is-false
(generate-term
L0
#:satisfying
(not-mem b (a (b (c ()))))
+inf.0)))