add enum to list-machine benchmarks
This commit is contained in:
parent
c237fdfff1
commit
eaf71ac6c8
|
@ -2,18 +2,18 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "confuses the lhs value for the rhs value in cons type rule")
|
||||
112c112,113
|
||||
113c113,114
|
||||
< (let ([closure (apply-reduction-relation*
|
||||
---
|
||||
> (let* ([stopped #f]
|
||||
> [closure (apply-reduction-relation*
|
||||
119c120,122
|
||||
120c121,123
|
||||
< (count . > . 1000)
|
||||
---
|
||||
> (count . > . 100)
|
||||
> (when (count . > . 100)
|
||||
> (set! stopped #t))
|
||||
122,124c125,128
|
||||
123,125c126,129
|
||||
< ;; (if the #:stop-when condition is true, we get back an empty list,
|
||||
< ;; and the same thing for a reduction cycle)
|
||||
< (or (empty? closure)
|
||||
|
@ -22,7 +22,7 @@
|
|||
> ;; (when the reduction is stopped artificially, the current term is returned)
|
||||
> (or stopped
|
||||
> (empty? closure)
|
||||
225c229
|
||||
226c230
|
||||
< [(:lookup-Γ Γ v_0 τ_0) (:lookup-Γ Γ v_1 τ_1)
|
||||
---
|
||||
> [(:lookup-Γ Γ v_0 τ_0) (:lookup-Γ Γ v_0 τ_1)
|
||||
|
|
|
@ -2,23 +2,23 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "var-set may skip a var with matching id (in reduction)")
|
||||
43,44c43
|
||||
44,45c44
|
||||
< [(where #t (different v v_2))
|
||||
< (var-set r v_2 a_2 r_2)
|
||||
---
|
||||
> [(var-set r v_2 a_2 r_2)
|
||||
112c111,112
|
||||
113c112,113
|
||||
< (let ([closure (apply-reduction-relation*
|
||||
---
|
||||
> (let* ([stopped #f]
|
||||
> [closure (apply-reduction-relation*
|
||||
119c119,121
|
||||
120c120,122
|
||||
< (count . > . 1000)
|
||||
---
|
||||
> (count . > . 20)
|
||||
> (when (count . > . 20)
|
||||
> (set! stopped #t))
|
||||
121,124c123,128
|
||||
122,125c124,129
|
||||
< ;; if reduction terminates in less than 1000 steps, check it ends with halt
|
||||
< ;; (if the #:stop-when condition is true, we get back an empty list,
|
||||
< ;; and the same thing for a reduction cycle)
|
||||
|
|
|
@ -2,7 +2,7 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "cons doesn't actually update the store")
|
||||
78c78
|
||||
79c79
|
||||
< (p r_2 ι)
|
||||
---
|
||||
> (p r ι)
|
||||
|
|
|
@ -4,7 +4,8 @@
|
|||
|
||||
(require redex/reduction-semantics
|
||||
racket/list
|
||||
racket/match)
|
||||
racket/match
|
||||
math/base)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
@ -431,3 +432,6 @@
|
|||
[`(check-program ,p ,Π)
|
||||
p]
|
||||
[#f #f]))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (random-natural #e10e200)))
|
||||
|
|
|
@ -4,7 +4,8 @@
|
|||
|
||||
(require redex/reduction-semantics
|
||||
racket/list
|
||||
racket/match)
|
||||
racket/match
|
||||
math/base)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
@ -431,3 +432,6 @@
|
|||
[`(check-program ,p ,Π)
|
||||
p]
|
||||
[#f #f]))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (random-natural #e10e200)))
|
||||
|
|
|
@ -4,7 +4,8 @@
|
|||
|
||||
(require redex/reduction-semantics
|
||||
racket/list
|
||||
racket/match)
|
||||
racket/match
|
||||
math/base)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
@ -427,3 +428,6 @@
|
|||
[`(check-program ,p ,Π)
|
||||
p]
|
||||
[#f #f]))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (random-natural #e10e200)))
|
||||
|
|
|
@ -4,7 +4,8 @@
|
|||
|
||||
(require redex/reduction-semantics
|
||||
racket/list
|
||||
racket/match)
|
||||
racket/match
|
||||
math/base)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
@ -427,3 +428,6 @@
|
|||
[`(check-program ,p ,Π)
|
||||
p]
|
||||
[#f #f]))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (random-natural #e10e200)))
|
||||
|
|
Loading…
Reference in New Issue
Block a user