suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add enum to stlc-sub, rbtrees benchmarks

Browse Source
This commit is contained in:
Max New 2014-02-23 12:31:57 -06:00 committed by Robby Findler
parent 1ef73b146c
commit 0a3dcf3288
24 changed files with 106 additions and 50 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/1.diff
View File

@ -2,11 +2,11 @@
< (define the-error "no-error")
---
> (define the-error "ins does no rebalancing")
90c90
91c91
< (balance (c (ins n_1 t_1) n_2 t_2))
---
> (c (ins n_1 t_1) n_2 t_2)
93c93
94c94
< (balance (c t_1 n_2 (ins n_1 t_2)))
---
> (c t_1 n_2 (ins n_1 t_2))

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/2.diff
View File

@ -2,6 +2,6 @@
< (define the-error "no-error")
---
> (define the-error "the first case is removed from balance")
99,100d98
100,101d99
< [(balance (B (R (R t_1 n_1 t_2) n_2 t_3) n_3 t_4))
< (R (B t_1 n_1 t_2) n_2 (B t_3 n_3 t_4))]

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/3.diff
View File

@ -2,7 +2,7 @@
< (define the-error "no-error")
---
> (define the-error "doesn't increment black depth in non-empty case")
75c75
76c76
< [(rbt (B (c_1 t_11 n_1 t_12) n (c_2 t_21 n_2 t_22)) n_1min n_2max (s n_bd))
---
> [(rbt (B (c_1 t_11 n_1 t_12) n (c_2 t_21 n_2 t_22)) n_1min n_2max n_bd)

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-1.rkt
View File

@ -3,7 +3,8 @@
(define the-error "ins does no rebalancing")
(require redex/reduction-semantics
racket/match)
racket/match
math/base)
(provide (all-defined-out))
@ -286,4 +287,7 @@
(define (check t)
(or (not t)
(ins-preserves-rb-tree t)))
(ins-preserves-rb-tree t)))
(define (generate-enum-term)
(generate-term rbtrees t #:i-th (random-natural #e10e200)))

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-2.rkt
View File

@ -3,7 +3,8 @@
(define the-error "the first case is removed from balance")
(require redex/reduction-semantics
racket/match)
racket/match
math/base)
(provide (all-defined-out))
@ -284,4 +285,7 @@
(define (check t)
(or (not t)
(ins-preserves-rb-tree t)))
(ins-preserves-rb-tree t)))
(define (generate-enum-term)
(generate-term rbtrees t #:i-th (random-natural #e10e200)))

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-3.rkt
View File

@ -3,7 +3,8 @@
(define the-error "doesn't increment black depth in non-empty case")
(require redex/reduction-semantics
racket/match)
racket/match
math/base)
(provide (all-defined-out))
@ -286,4 +287,7 @@
(define (check t)
(or (not t)
(ins-preserves-rb-tree t)))
(ins-preserves-rb-tree t)))
(define (generate-enum-term)
(generate-term rbtrees t #:i-th (random-natural #e10e200)))

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-base.rkt
View File

@ -3,7 +3,8 @@
(define the-error "no-error")
(require redex/reduction-semantics
racket/match)
racket/match
math/base)
(provide (all-defined-out))
@ -286,4 +287,7 @@
(define (check t)
(or (not t)
(ins-preserves-rb-tree t)))
(ins-preserves-rb-tree t)))
(define (generate-enum-term)
(generate-term rbtrees t #:i-th (random-natural #e10e200)))

6
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/1.diff
View File

@ -8,11 +8,11 @@
11a10,11
> (define the-error "the order of the variable clauses is swapped")
>
102,103d101
103,104d102
< [(subst x x M)
< M]
105a104,105
106a105,106
> [(subst x x M)
> M]
253a254
254a255
>

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/2.diff
View File

@ -8,7 +8,7 @@
11a10,11
> (define the-error "only substitutes inside of hd constants")
>
112,113c112,113
113,114c113,114
< [(subst (c M) x M_x)
< (c (subst M x M_x))]
---

4
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/3.diff
View File

@ -8,9 +8,9 @@
11a10,11
> (define the-error "substitutes rator into rand in application")
>
115c115
116c116
< ((subst M x M_x) (subst N x M_x))]
---
> ((subst M x M_x) (subst N x M))]
253a254
254a255
>

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/4.diff
View File

@ -8,14 +8,14 @@
11a10,11
> (define the-error "substitutes inside of λ that binds the sub variable")
>
106,107d105
107,108d106
< [(subst (λ (x τ) M) x M_x)
< (λ (x τ) M)]
112,113d109
113,114d110
< [(subst (c M) x M_x)
< (c (subst M x M_x))]
115a112,113
116a113,114
> [(subst (c M) x M_x)
> (c (subst M x M_x))]
253a252
254a253
>

4
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/7.diff
View File

@ -8,9 +8,9 @@
11a10,11
> (define the-error "swaps to/from expressions when recurring inside a constant")
>
113c113
114c114
< (c (subst M x M_x))]
---
> (c (subst M_x x M))]
253a254
254a255
>

4
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/8.diff
View File

@ -8,9 +8,9 @@
11a10,11
> (define the-error "swaps the order of the λ clauses")
>
106,107d105
107,108d106
< [(subst (λ (x τ) M) x M_x)
< (λ (x τ) M)]
111a110,111
112a111,112
> [(subst (λ (x τ) M) x M_x)
> (λ (x τ) M)]

4
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/9.diff
View File

@ -11,8 +11,8 @@
111a112,113
> [(subst (M N) x M_x)
> ((subst M_x x M) (subst N x M_x))]
114,115d115
115,116d116
< [(subst (M N) x M_x)
< ((subst M x M_x) (subst N x M_x))]
253a254
254a255
>

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt
View File

@ -3,12 +3,13 @@
(require redex/reduction-semantics
racket/list
racket/match
racket/contract)
racket/contract
math/base)
(provide (all-defined-out))
(define the-error "the order of the variable clauses is swapped")
(define-language stlc
(M N ::=
(λ (x σ) M)
@ -272,3 +273,6 @@
(or
(equal? (car red-res) "error")
(equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt
View File

@ -3,12 +3,13 @@
(require redex/reduction-semantics
racket/list
racket/match
racket/contract)
racket/contract
math/base)
(provide (all-defined-out))
(define the-error "only substitutes inside of hd constants")
(define-language stlc
(M N ::=
(λ (x σ) M)
@ -271,3 +272,6 @@
(or
(equal? (car red-res) "error")
(equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt
View File

@ -3,12 +3,13 @@
(require redex/reduction-semantics
racket/list
racket/match
racket/contract)
racket/contract
math/base)
(provide (all-defined-out))
(define the-error "substitutes rator into rand in application")
(define-language stlc
(M N ::=
(λ (x σ) M)
@ -272,3 +273,6 @@
(or
(equal? (car red-res) "error")
(equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt
View File

@ -3,12 +3,13 @@
(require redex/reduction-semantics
racket/list
racket/match
racket/contract)
racket/contract
math/base)
(provide (all-defined-out))
(define the-error "substitutes inside of λ that binds the sub variable")
(define-language stlc
(M N ::=
(λ (x σ) M)
@ -270,3 +271,6 @@
(or
(equal? (car red-res) "error")
(equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

10
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt
View File

@ -3,12 +3,13 @@
(require redex/reduction-semantics
racket/list
racket/match
racket/contract)
racket/contract
math/base)
(provide (all-defined-out))
(define the-error "picks up the bound variable when recurring inside λ")
(define-language stlc
(M N ::=
(λ (x σ) M)
@ -250,8 +251,8 @@
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
[`(typeof • ,M ,τ)
M]
[#f #f]))
[#f #f]))
(define (typed-generator)
(let ([g (redex-generator stlc
(typeof • M τ)
@ -272,3 +273,6 @@
(or
(equal? (car red-res) "error")
(equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

10
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt
View File

@ -3,12 +3,13 @@
(require redex/reduction-semantics
racket/list
racket/match
racket/contract)
racket/contract
math/base)
(provide (all-defined-out))
(define the-error "swaps the bound var when recurring inside λ")
(define-language stlc
(M N ::=
(λ (x σ) M)
@ -250,8 +251,8 @@
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
[`(typeof • ,M ,τ)
M]
[#f #f]))
[#f #f]))
(define (typed-generator)
(let ([g (redex-generator stlc
(typeof • M τ)
@ -272,3 +273,6 @@
(or
(equal? (car red-res) "error")
(equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt
View File

@ -3,12 +3,13 @@
(require redex/reduction-semantics
racket/list
racket/match
racket/contract)
racket/contract
math/base)
(provide (all-defined-out))
(define the-error "swaps to/from expressions when recurring inside a constant")
(define-language stlc
(M N ::=
(λ (x σ) M)
@ -272,3 +273,6 @@
(or
(equal? (car red-res) "error")
(equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt
View File

@ -3,12 +3,13 @@
(require redex/reduction-semantics
racket/list
racket/match
racket/contract)
racket/contract
math/base)
(provide (all-defined-out))
(define the-error "swaps the order of the λ clauses")
(define-language stlc
(M N ::=
(λ (x σ) M)
@ -271,3 +272,6 @@
(or
(equal? (car red-res) "error")
(equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

10
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt
View File

@ -3,12 +3,13 @@
(require redex/reduction-semantics
racket/list
racket/match
racket/contract)
racket/contract
math/base)
(provide (all-defined-out))
(define the-error "swaps to/from expressions when recurring in the rhs of app")
(define-language stlc
(M N ::=
(λ (x σ) M)
@ -108,9 +109,9 @@
[(subst (λ (x_1 τ) M) x_2 v)
(λ (x_new τ) (subst (replace M x_1 x_new) x_2 v))
(where x_new ,(variable-not-in (term (x_1 e x_2))
(term x_1)))]
[(subst (M N) x M_x)
((subst M_x x M) (subst N x M_x))]
(term x_1)))]
[(subst (c M) x M_x)
(c (subst M x M_x))]
[(subst M x M_x)
@ -272,3 +273,6 @@
(or
(equal? (car red-res) "error")
(equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

6
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt
View File

@ -5,7 +5,8 @@
(require redex/reduction-semantics
racket/match
racket/list
racket/contract)
racket/contract
math/base)
(provide (all-defined-out))
@ -271,3 +272,6 @@
(or
(equal? (car red-res) "error")
(equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))