Use new random natural function for enum benchmarks
This commit is contained in:
parent
0a3dcf3288
commit
3a98152f33
|
@ -6,7 +6,7 @@
|
|||
;; with commit: 4b848777d12a2e5b59b43c8e77f9f68b747d1151
|
||||
|
||||
(require redex/reduction-semantics
|
||||
math/base)
|
||||
(only-in redex/private/generate-term pick-an-index))
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
@ -942,4 +942,4 @@
|
|||
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term abort-lang e #:i-th (random-natural #e10e200)))
|
||||
(generate-term abort-lang e #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,7 +3,7 @@
|
|||
(define the-error "list/c contracts aren't applied properly in the cons case")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
math/base)
|
||||
(only-in redex/private/generate-term pick-an-index))
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
@ -940,4 +940,4 @@
|
|||
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term abort-lang e #:i-th (random-natural #e10e200)))
|
||||
(generate-term abort-lang e #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,7 +3,7 @@
|
|||
(define the-error "the function argument to call/comp has the wrong type")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
math/base)
|
||||
(only-in redex/private/generate-term pick-an-index))
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
@ -940,4 +940,4 @@
|
|||
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term abort-lang e #:i-th (random-natural #e10e200)))
|
||||
(generate-term abort-lang e #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,7 +3,7 @@
|
|||
(define the-error "no-error")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
math/base)
|
||||
(only-in redex/private/generate-term pick-an-index))
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
@ -937,4 +937,4 @@
|
|||
(judgment-holds (tc · · ,e t)))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term abort-lang e #:i-th (random-natural #e10e200)))
|
||||
(generate-term abort-lang e #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,9 +3,9 @@
|
|||
(define the-error "confuses the lhs value for the rhs value in cons type rule")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
math/base)
|
||||
racket/match)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
@ -434,4 +434,4 @@
|
|||
[#f #f]))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (random-natural #e10e200)))
|
||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,9 +3,9 @@
|
|||
(define the-error "var-set may skip a var with matching id (in reduction)")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
math/base)
|
||||
racket/match)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
@ -434,4 +434,4 @@
|
|||
[#f #f]))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (random-natural #e10e200)))
|
||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,9 +3,9 @@
|
|||
(define the-error "cons doesn't actually update the store")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
math/base)
|
||||
racket/match)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
@ -430,4 +430,4 @@
|
|||
[#f #f]))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (random-natural #e10e200)))
|
||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,9 +3,9 @@
|
|||
(define the-error "no error")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
math/base)
|
||||
racket/match)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
@ -430,4 +430,4 @@
|
|||
[#f #f]))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (random-natural #e10e200)))
|
||||
(generate-term list-machine-typing (l0 : ι p) #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -281,4 +281,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -279,4 +279,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -281,4 +281,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -281,4 +281,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -281,4 +281,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -281,4 +281,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -280,4 +280,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -281,4 +281,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -281,4 +281,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -281,4 +281,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term poly-stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,8 +3,8 @@
|
|||
(define the-error "ins does no rebalancing")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
racket/match
|
||||
math/base)
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/match)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
@ -290,4 +290,4 @@
|
|||
(ins-preserves-rb-tree t)))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term rbtrees t #:i-th (random-natural #e10e200)))
|
||||
(generate-term rbtrees t #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,8 +3,8 @@
|
|||
(define the-error "the first case is removed from balance")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
racket/match
|
||||
math/base)
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/match)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
@ -288,4 +288,4 @@
|
|||
(ins-preserves-rb-tree t)))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term rbtrees t #:i-th (random-natural #e10e200)))
|
||||
(generate-term rbtrees t #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,8 +3,8 @@
|
|||
(define the-error "doesn't increment black depth in non-empty case")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
racket/match
|
||||
math/base)
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/match)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
@ -290,4 +290,4 @@
|
|||
(ins-preserves-rb-tree t)))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term rbtrees t #:i-th (random-natural #e10e200)))
|
||||
(generate-term rbtrees t #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,8 +3,8 @@
|
|||
(define the-error "no-error")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
racket/match
|
||||
math/base)
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/match)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
@ -290,4 +290,4 @@
|
|||
(ins-preserves-rb-tree t)))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term rbtrees t #:i-th (random-natural #e10e200)))
|
||||
(generate-term rbtrees t #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,18 +1,18 @@
|
|||
3,4d2
|
||||
< (define the-error "no error")
|
||||
<
|
||||
6d3
|
||||
7d4
|
||||
< racket/match
|
||||
7a5
|
||||
8a6
|
||||
> racket/match
|
||||
11a10,11
|
||||
12a11,12
|
||||
> (define the-error "the order of the variable clauses is swapped")
|
||||
>
|
||||
103,104d102
|
||||
104,105d103
|
||||
< [(subst x x M)
|
||||
< M]
|
||||
106a105,106
|
||||
107a106,107
|
||||
> [(subst x x M)
|
||||
> M]
|
||||
254a255
|
||||
255a256
|
||||
>
|
||||
|
|
|
@ -1,14 +1,14 @@
|
|||
3,4d2
|
||||
< (define the-error "no error")
|
||||
<
|
||||
6d3
|
||||
7d4
|
||||
< racket/match
|
||||
7a5
|
||||
8a6
|
||||
> racket/match
|
||||
11a10,11
|
||||
12a11,12
|
||||
> (define the-error "only substitutes inside of hd constants")
|
||||
>
|
||||
113,114c113,114
|
||||
114,115c114,115
|
||||
< [(subst (c M) x M_x)
|
||||
< (c (subst M x M_x))]
|
||||
---
|
||||
|
|
|
@ -1,16 +1,16 @@
|
|||
3,4d2
|
||||
< (define the-error "no error")
|
||||
<
|
||||
6d3
|
||||
7d4
|
||||
< racket/match
|
||||
7a5
|
||||
8a6
|
||||
> racket/match
|
||||
11a10,11
|
||||
12a11,12
|
||||
> (define the-error "substitutes rator into rand in application")
|
||||
>
|
||||
116c116
|
||||
117c117
|
||||
< ((subst M x M_x) (subst N x M_x))]
|
||||
---
|
||||
> ((subst M x M_x) (subst N x M))]
|
||||
254a255
|
||||
255a256
|
||||
>
|
||||
|
|
|
@ -1,21 +1,21 @@
|
|||
3,4d2
|
||||
< (define the-error "no error")
|
||||
<
|
||||
6d3
|
||||
7d4
|
||||
< racket/match
|
||||
7a5
|
||||
8a6
|
||||
> racket/match
|
||||
11a10,11
|
||||
12a11,12
|
||||
> (define the-error "substitutes inside of λ that binds the sub variable")
|
||||
>
|
||||
107,108d106
|
||||
108,109d107
|
||||
< [(subst (λ (x τ) M) x M_x)
|
||||
< (λ (x τ) M)]
|
||||
113,114d110
|
||||
114,115d111
|
||||
< [(subst (c M) x M_x)
|
||||
< (c (subst M x M_x))]
|
||||
116a113,114
|
||||
117a114,115
|
||||
> [(subst (c M) x M_x)
|
||||
> (c (subst M x M_x))]
|
||||
254a253
|
||||
255a254
|
||||
>
|
||||
|
|
|
@ -1,12 +1,12 @@
|
|||
3,4d2
|
||||
< (define the-error "no error")
|
||||
<
|
||||
6d3
|
||||
7d4
|
||||
< racket/match
|
||||
7a5
|
||||
8a6
|
||||
> racket/match
|
||||
11a10,11
|
||||
12a11,12
|
||||
> (define the-error "picks up the bound variable when recurring inside λ")
|
||||
>
|
||||
253a254
|
||||
254a255
|
||||
>
|
||||
|
|
|
@ -1,12 +1,12 @@
|
|||
3,4d2
|
||||
< (define the-error "no error")
|
||||
<
|
||||
6d3
|
||||
7d4
|
||||
< racket/match
|
||||
7a5
|
||||
8a6
|
||||
> racket/match
|
||||
11a10,11
|
||||
12a11,12
|
||||
> (define the-error "swaps the bound var when recurring inside λ")
|
||||
>
|
||||
253a254
|
||||
254a255
|
||||
>
|
||||
|
|
|
@ -1,16 +1,16 @@
|
|||
3,4d2
|
||||
< (define the-error "no error")
|
||||
<
|
||||
6d3
|
||||
7d4
|
||||
< racket/match
|
||||
7a5
|
||||
8a6
|
||||
> racket/match
|
||||
11a10,11
|
||||
12a11,12
|
||||
> (define the-error "swaps to/from expressions when recurring inside a constant")
|
||||
>
|
||||
114c114
|
||||
115c115
|
||||
< (c (subst M x M_x))]
|
||||
---
|
||||
> (c (subst M_x x M))]
|
||||
254a255
|
||||
255a256
|
||||
>
|
||||
|
|
|
@ -1,16 +1,16 @@
|
|||
3,4d2
|
||||
< (define the-error "no error")
|
||||
<
|
||||
6d3
|
||||
7d4
|
||||
< racket/match
|
||||
7a5
|
||||
8a6
|
||||
> racket/match
|
||||
11a10,11
|
||||
12a11,12
|
||||
> (define the-error "swaps the order of the λ clauses")
|
||||
>
|
||||
107,108d106
|
||||
108,109d107
|
||||
< [(subst (λ (x τ) M) x M_x)
|
||||
< (λ (x τ) M)]
|
||||
112a111,112
|
||||
113a112,113
|
||||
> [(subst (λ (x τ) M) x M_x)
|
||||
> (λ (x τ) M)]
|
||||
|
|
|
@ -1,18 +1,18 @@
|
|||
3,4d2
|
||||
< (define the-error "no error")
|
||||
<
|
||||
6d3
|
||||
7d4
|
||||
< racket/match
|
||||
7a5
|
||||
8a6
|
||||
> racket/match
|
||||
11a10,11
|
||||
12a11,12
|
||||
> (define the-error "swaps to/from expressions when recurring in the rhs of app")
|
||||
>
|
||||
111a112,113
|
||||
112a113,114
|
||||
> [(subst (M N) x M_x)
|
||||
> ((subst M_x x M) (subst N x M_x))]
|
||||
115,116d116
|
||||
116,117d117
|
||||
< [(subst (M N) x M_x)
|
||||
< ((subst M x M_x) (subst N x M_x))]
|
||||
254a255
|
||||
255a256
|
||||
>
|
||||
|
|
|
@ -1,6 +1,7 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
|
@ -275,4 +276,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,6 +1,7 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
|
@ -274,4 +275,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,6 +1,7 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
|
@ -275,4 +276,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,6 +1,7 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
|
@ -273,4 +274,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,6 +1,7 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
|
@ -275,4 +276,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,6 +1,7 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
|
@ -275,4 +276,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,6 +1,7 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
|
@ -275,4 +276,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,6 +1,7 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
|
@ -274,4 +275,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -1,6 +1,7 @@
|
|||
#lang racket/base
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
|
@ -275,4 +276,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,6 +3,7 @@
|
|||
(define the-error "no error")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/match
|
||||
racket/list
|
||||
racket/contract
|
||||
|
@ -274,4 +275,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -2,9 +2,9 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "app rule the range of the function is matched to the argument")
|
||||
7d6
|
||||
8d7
|
||||
< racket/contract
|
||||
8a8
|
||||
9a9
|
||||
> racket/contract
|
||||
58c58
|
||||
< (typeof Γ M_2 σ)
|
||||
|
|
|
@ -2,9 +2,9 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "the order of the types in the function position of application has been swapped")
|
||||
7d6
|
||||
8d7
|
||||
< racket/contract
|
||||
8a8
|
||||
9a9
|
||||
> racket/contract
|
||||
57c57
|
||||
< [(typeof Γ M (σ → σ_2))
|
||||
|
|
|
@ -2,9 +2,9 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "the type of cons is incorrect")
|
||||
7d6
|
||||
8d7
|
||||
< racket/contract
|
||||
8a8
|
||||
9a9
|
||||
> racket/contract
|
||||
67c67
|
||||
< (int → ((list int) → (list int)))]
|
||||
|
|
|
@ -2,9 +2,9 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "the tail reduction returns the wrong value")
|
||||
7d6
|
||||
8d7
|
||||
< racket/contract
|
||||
8a8
|
||||
9a9
|
||||
> racket/contract
|
||||
92c92
|
||||
< (in-hole E v_2)
|
||||
|
|
|
@ -2,9 +2,9 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "hd reduction acts on partially applied cons")
|
||||
7d6
|
||||
8d7
|
||||
< racket/contract
|
||||
8a8
|
||||
9a9
|
||||
> racket/contract
|
||||
88c88
|
||||
< (--> (in-hole E (hd ((cons v_1) v_2)))
|
||||
|
|
|
@ -2,9 +2,9 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "evaluation isn't allowed on the rhs of applications")
|
||||
7d6
|
||||
8d7
|
||||
< racket/contract
|
||||
8a8
|
||||
9a9
|
||||
> racket/contract
|
||||
36,37c36
|
||||
< (E M)
|
||||
|
|
|
@ -2,9 +2,9 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "lookup always returns int")
|
||||
7d6
|
||||
8d7
|
||||
< racket/contract
|
||||
8a8
|
||||
9a9
|
||||
> racket/contract
|
||||
76c76
|
||||
< σ]
|
||||
|
|
|
@ -2,9 +2,9 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "variables aren't required to match in lookup")
|
||||
7d6
|
||||
8d7
|
||||
< racket/contract
|
||||
8a8
|
||||
9a9
|
||||
> racket/contract
|
||||
75c75
|
||||
< [(lookup (x σ Γ) x)
|
||||
|
|
|
@ -3,10 +3,10 @@
|
|||
(define the-error "app rule the range of the function is matched to the argument")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -251,4 +251,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,10 +3,10 @@
|
|||
(define the-error "the ((cons number) v) value has been omitted")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/contract
|
||||
racket/match
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -251,4 +251,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,10 +3,10 @@
|
|||
(define the-error "the order of the types in the function position of application has been swapped")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -252,4 +252,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,10 +3,10 @@
|
|||
(define the-error "the type of cons is incorrect")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -252,4 +252,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,10 +3,10 @@
|
|||
(define the-error "the tail reduction returns the wrong value")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -251,4 +251,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,10 +3,10 @@
|
|||
(define the-error "hd reduction acts on partially applied cons")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -251,4 +251,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,10 +3,10 @@
|
|||
(define the-error "evaluation isn't allowed on the rhs of applications")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -250,4 +250,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,10 +3,10 @@
|
|||
(define the-error "lookup always returns int")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -251,4 +251,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,10 +3,10 @@
|
|||
(define the-error "variables aren't required to match in lookup")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -251,4 +251,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -3,10 +3,10 @@
|
|||
(define the-error "no error")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/list
|
||||
racket/contract
|
||||
racket/match
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -252,4 +252,4 @@
|
|||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term stlc M #:i-th (random-natural #e10e200)))
|
||||
(generate-term stlc M #:i-th (pick-an-index)))
|
||||
|
|
|
@ -822,4 +822,5 @@
|
|||
exn:fail:redex:generation-failure?
|
||||
redex-generator
|
||||
(struct-out counterexample)
|
||||
(struct-out exn:fail:redex:test))
|
||||
(struct-out exn:fail:redex:test)
|
||||
pick-an-index)
|
||||
|
|
Loading…
Reference in New Issue
Block a user