Handle failing case for relation generation.
This commit is contained in:
parent
7c7c1fbafc
commit
26766e413a
|
@ -441,7 +441,8 @@
|
||||||
(λ ()
|
(λ ()
|
||||||
(match (gen-proc)
|
(match (gen-proc)
|
||||||
[`(,jf-name (,trms (... ...)))
|
[`(,jf-name (,trms (... ...)))
|
||||||
`(,jf-name ,@trms)])))
|
`(,jf-name ,@trms)]
|
||||||
|
[#f #f])))
|
||||||
#`(make-jf-gen/proc 'jf/mf-id #,clauses lang-id 'pat size))))]
|
#`(make-jf-gen/proc 'jf/mf-id #,clauses lang-id 'pat size))))]
|
||||||
[_
|
[_
|
||||||
(raise-syntax-error 'redex-generator
|
(raise-syntax-error 'redex-generator
|
||||||
|
|
|
@ -73,6 +73,9 @@
|
||||||
(test-equal (generate-term nats #:satisfying (sum (s z) (s z) n) +inf.0)
|
(test-equal (generate-term nats #:satisfying (sum (s z) (s z) n) +inf.0)
|
||||||
'(sum (s z) (s z) (s (s z))))
|
'(sum (s z) (s z) (s (s z))))
|
||||||
|
|
||||||
|
(test-equal (generate-term nats #:satisfying (sum z z (s z)) 5)
|
||||||
|
#f)
|
||||||
|
|
||||||
(for ([_ 100])
|
(for ([_ 100])
|
||||||
(match (generate-term nats #:satisfying (sum n_1 n_2 n_3) 5)
|
(match (generate-term nats #:satisfying (sum n_1 n_2 n_3) 5)
|
||||||
[`(sum ,l ,r ,res)
|
[`(sum ,l ,r ,res)
|
||||||
|
|
Loading…
Reference in New Issue
Block a user