-
Notifications
You must be signed in to change notification settings - Fork 5
/
normal-order-test.ss
35 lines (34 loc) · 1.24 KB
/
normal-order-test.ss
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
#lang scheme ; File normal-order-test.ss
(require redex "tracer.ss")
(provide normal-order-test)
(define-syntax normal-order-test
(syntax-rules ()
((_ grammar reductor βNf?)
(begin
(tracer reductor
(((((λ (x y) x) y) z) ((((λ (z) (z z)) (λ (x y) (x (x y)))) a) z))
(y (a (a (a (a z))))))
(((((λ (z) (z z)) (λ (x y) (x (x y)))) a) z) (a (a (a (a z)))))
((λ (x) (y x)) (λ (x) (y x)))
(((λ (x) x) y) y)
(((λ (x y z) (x y z)) a b c) (a b c))
(((λ (z) ((a b) z)) c) (a b c))
(((λ (x) (x x)) (λ (x) (x x))) #f))
(redex-check grammar ‹term›
(let*
((nf? (term (βNf? ‹term›)))
(redices
(apply-reduction-relation
reductor
(term ‹term›))))
(cond
((and (pair? redices) (pair? (cdr redices)))
(error 'test "more than one left most redex for term ~s"
(term ‹term›)))
((and nf? (pair? redices))
(error 'test "(βNf? ~s)->#t but reductor found redex ~s."
(term ‹term›) (car redices)))
((and (not nf?) (null? redices))
(error 'test "(βNf? ~s)->#f but reductor found no redex ~s."
(term ‹term›)))))
#:attempts 10000 #:retries 100)))))