Add enum to poly-stlc bench
This commit is contained in:
parent
e2a0724636
commit
1ef73b146c
|
@ -1,12 +1,12 @@
|
|||
11c11
|
||||
12c12
|
||||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "app rule the range of the function is matched to the argument")
|
||||
72c72
|
||||
73c73
|
||||
< [(typeof Γ M (σ → σ_2))
|
||||
---
|
||||
> [(typeof Γ M (σ_2 → σ_2))
|
||||
261c261
|
||||
262c262
|
||||
< M]
|
||||
---
|
||||
> M]
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
11c11
|
||||
12c12
|
||||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "the (([cons @ τ] v) v) value has been omitted")
|
||||
46d45
|
||||
47d46
|
||||
< (([cons @ τ] v) v)
|
||||
261,262c260
|
||||
262,263c261
|
||||
< M]
|
||||
< [#f #f]))
|
||||
---
|
||||
|
|
|
@ -1,12 +1,12 @@
|
|||
11c11
|
||||
12c12
|
||||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "the order of the types in the function position of application has been swapped")
|
||||
72c72
|
||||
73c73
|
||||
< [(typeof Γ M (σ → σ_2))
|
||||
---
|
||||
> [(typeof Γ M (σ_2 → σ))
|
||||
261c261
|
||||
262c262
|
||||
< M]
|
||||
---
|
||||
> M]
|
||||
|
|
|
@ -1,12 +1,12 @@
|
|||
11c11
|
||||
12c12
|
||||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "the type of cons is incorrect")
|
||||
119c119
|
||||
120c120
|
||||
< (∀ a (a → ((list a) → (list a))))]
|
||||
---
|
||||
> (∀ a (a → ((list a) → a)))]
|
||||
261c261
|
||||
262c262
|
||||
< M]
|
||||
---
|
||||
> M]
|
||||
|
|
|
@ -1,12 +1,12 @@
|
|||
11c11
|
||||
12c12
|
||||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "the tail reduction returns the wrong value")
|
||||
165c165
|
||||
166c166
|
||||
< (in-hole E v_2)
|
||||
---
|
||||
> (in-hole E v_1)
|
||||
261c261
|
||||
262c262
|
||||
< M]
|
||||
---
|
||||
> M]
|
||||
|
|
|
@ -1,12 +1,12 @@
|
|||
11c11
|
||||
12c12
|
||||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "hd reduction acts on partially applied cons")
|
||||
161c161
|
||||
162c162
|
||||
< (--> (in-hole E ((hd @ τ) (((cons @ τ) v_1) v_2)))
|
||||
---
|
||||
> (--> (in-hole E ((hd @ τ) ((cons @ τ) v_1)))
|
||||
261c261
|
||||
262c262
|
||||
< M]
|
||||
---
|
||||
> M]
|
||||
|
|
|
@ -1,13 +1,13 @@
|
|||
11c11
|
||||
12c12
|
||||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "evaluation isn't allowed on the rhs of applications")
|
||||
49,50c49
|
||||
50,51c50
|
||||
< (E M)
|
||||
< (v E)))
|
||||
---
|
||||
> (E M)))
|
||||
261c260
|
||||
262c261
|
||||
< M]
|
||||
---
|
||||
> M]
|
||||
|
|
|
@ -1,12 +1,12 @@
|
|||
11c11
|
||||
12c12
|
||||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "lookup always returns int")
|
||||
108c108
|
||||
109c109
|
||||
< σ]
|
||||
---
|
||||
> int]
|
||||
261c261
|
||||
262c262
|
||||
< M]
|
||||
---
|
||||
> M]
|
||||
|
|
|
@ -1,12 +1,12 @@
|
|||
11c11
|
||||
12c12
|
||||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "variables aren't required to match in lookup")
|
||||
107c107
|
||||
108c108
|
||||
< [(lookup (x σ Γ) x)
|
||||
---
|
||||
> [(lookup (x σ Γ) x_2)
|
||||
261c261
|
||||
262c262
|
||||
< M]
|
||||
---
|
||||
> M]
|
||||
|
|
|
@ -4,6 +4,7 @@
|
|||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -278,3 +279,6 @@
|
|||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
|
|
|
@ -4,6 +4,7 @@
|
|||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -276,3 +277,6 @@
|
|||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
|
|
|
@ -4,6 +4,7 @@
|
|||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -278,3 +279,6 @@
|
|||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
|
|
|
@ -4,6 +4,7 @@
|
|||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -278,3 +279,6 @@
|
|||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
|
|
|
@ -4,6 +4,7 @@
|
|||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -278,3 +279,6 @@
|
|||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
|
|
|
@ -4,6 +4,7 @@
|
|||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -278,3 +279,6 @@
|
|||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
|
|
|
@ -4,6 +4,7 @@
|
|||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -277,3 +278,6 @@
|
|||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
|
|
|
@ -4,6 +4,7 @@
|
|||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -278,3 +279,6 @@
|
|||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
|
|
|
@ -4,6 +4,7 @@
|
|||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -278,3 +279,6 @@
|
|||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
|
|
|
@ -4,6 +4,7 @@
|
|||
racket/list
|
||||
racket/match
|
||||
racket/contract
|
||||
math/base
|
||||
"tut-subst.rkt")
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
@ -278,3 +279,6 @@
|
|||
(or
|
||||
(equal? (car red-res) "error")
|
||||
(equal? t-type (type-check (car red-res))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
(generate-term poly-stlc M #:i-th (random-natural #e10e200)))
|
||||
|
|
Loading…
Reference in New Issue
Block a user