/
generators.rkt
81 lines (72 loc) · 2.61 KB
/
generators.rkt
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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
#lang racket/base
(require racket/bool
racket/match
redex/reduction-semantics
redex/benchmark
redex/examples/racket-machine/grammar
redex/examples/racket-machine/verification
redex/examples/racket-machine/randomized-tests
(prefix-in jdg: redex/benchmark/models/rvm/verif-jdg)
(only-in redex/private/generate-term pick-an-index))
(provide (all-defined-out))
(module+ adhoc-mod
(provide generate get-generator type)
(define (get-generator) generate)
(define type 'grammar)
(define (generate)
(fix (generate-term bytecode e 5))))
(module+ enum-mod
(provide generate get-generator type)
(define (get-generator) generate)
(define type 'enum)
(define (generate [p-value 0.03])
(fix (generate-term bytecode e #:i-th (pick-an-index p-value)))))
(module+ ordered-mod
(provide generate get-generator type)
(define (get-generator)
(let ([index 0])
(λ () (begin0
(generate index)
(set! index (add1 index))))))
(define type 'ordered)
(define (generate [index 0])
(fix (generate-term bytecode e #:i-th index))))
(module+ typed-mod
(provide generate get-generator type)
(define (get-generator) generate)
(define type 'search)
(define (generate)
(match (generate-term
jdg:vl
#:satisfying
(jdg:V e • O #f • • ∅ s_1 γ_1 η_1)
4)
[#f #f]
[`(jdg:V ,e • O #f • • ∅ ,s_1 ,γ_1 ,η_1)
(fix (term (jdg:trans-e ,e)))])))
(module+ check-mod
(provide check)
(define (check e)
(let/ec vf-not-total
(or (not e)
(implies (with-handlers ([exn:fail? (λ (exc)
(maybe-log-exn exc e)
(vf-not-total #f))])
(bytecode-ok? e))
(match
(with-handlers
([exn:fail? (λ (exc)
(maybe-log-exn exc e)
#f)])
(run e '() 100))
[(cutoff) #t]
[(answer _) #t]
[_ #f])))))
(define (maybe-log-exn exc e)
(if (regexp-match? #rx"counterexample|domain|clauses" (exn-message exc))
(begin (bmark-log 'rvm-expected-exception
`(#:exn-message ,(exn-message exc) #:expression ,e))
#f)
(begin (bmark-log 'rvm-unexpected-exception
`(#:exn-message ,(exn-message exc) #:expression ,e))
(raise exc)))))