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

Adjust fixed mode and add new stlc counterexamples

Browse Source
This commit is contained in:
Burke Fetscher 2014-03-18 14:39:42 -05:00
parent 2f18cd202f
commit 28e99cf9eb
20 changed files with 164 additions and 171 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -2,17 +2,9 @@
< (define the-error "no error")
---
> (define the-error "app rule the range of the function is matched to the argument")
8d7
< racket/contract
9a9
> racket/contract
58c58
< (typeof Γ M_2 σ)
---
> (typeof Γ M_2 σ_2)
232d231
<
249c248
< (= (length red-res) 1)
---
> (= (length red-res) 1)

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

@ -7,7 +7,3 @@
< ((cons v) v))
---
> (cons v))
249c248
< (= (length red-res) 1)
---
> (= (length red-res) 1)

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

@ -2,15 +2,7 @@
< (define the-error "no error")
---
> (define the-error "the order of the types in the function position of application has been swapped")
8d7
< racket/contract
9a9
> racket/contract
57c57
< [(typeof Γ M (σ → σ_2))
---
> [(typeof Γ M (σ_2 → σ))
249c249
< (= (length red-res) 1)
---
> (= (length red-res) 1)

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

@ -2,15 +2,7 @@
< (define the-error "no error")
---
> (define the-error "the type of cons is incorrect")
8d7
< racket/contract
9a9
> racket/contract
67c67
< (int → ((list int) → (list int)))]
---
> (int → ((list int) → int))]
249c249
< (= (length red-res) 1)
---
> (= (length red-res) 1)

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

@ -2,17 +2,9 @@
< (define the-error "no error")
---
> (define the-error "the tail reduction returns the wrong value")
8d7
< racket/contract
9a9
> racket/contract
92c92
< (in-hole E v_2)
---
> (in-hole E v_1)
232d231
<
249c248
< (= (length red-res) 1)
---
> (= (length red-res) 1)

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

@ -2,17 +2,9 @@
< (define the-error "no error")
---
> (define the-error "hd reduction acts on partially applied cons")
8d7
< racket/contract
9a9
> racket/contract
88c88
< (--> (in-hole E (hd ((cons v_1) v_2)))
---
> (--> (in-hole E (hd (cons v_1)))
232d231
<
249c248
< (= (length red-res) 1)
---
> (= (length red-res) 1)

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

@ -2,10 +2,6 @@
< (define the-error "no error")
---
> (define the-error "evaluation isn't allowed on the rhs of applications")
8d7
< racket/contract
9a9
> racket/contract
36,37c36
< (E M)
< (v E)))
@ -13,7 +9,3 @@
> (E M)))
232d230
<
249c247
< (= (length red-res) 1)
---
> (= (length red-res) 1)

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

@ -2,17 +2,9 @@
< (define the-error "no error")
---
> (define the-error "lookup always returns int")
8d7
< racket/contract
9a9
> racket/contract
76c76
< σ]
---
> int]
232d231
<
249c248
< (= (length red-res) 1)
---
> (= (length red-res) 1)

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

@ -2,17 +2,9 @@
< (define the-error "no error")
---
> (define the-error "variables aren't required to match in lookup")
8d7
< racket/contract
9a9
> racket/contract
75c75
< [(lookup (x σ Γ) x)
---
> [(lookup (x σ Γ) x_2)
232d231
<
249c248
< (= (length red-res) 1)
---
> (= (length red-res) 1)

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

@ -264,15 +264,21 @@
(define fixed
(term
(;; 2
((cons 1) 2)
((cons 1) nil)
;; 3
((λ (x int) (hd x))
((λ (x (list int)) 1)
7)
;; 4 (if we hadn't changed number->v in cons)
(cons ((cons 0) nil))
;; 5
(tl ((cons 1) nil))
;; 6
(hd ((cons 1) nil))
;; 7
((λ (x int) x) (hd ((cons 1) nil)))
;; 8
((λ (x (list int)) (cons x)) nil)
;; 9
((λ (x int) (λ (y (list int)) x)) 1)
;; 10
((λ (x (list int)) (hd x))
7)
;; 5, 6, 7, 8, 9
((λ (x int) (hd x))
((cons 1) nil))
;; 4
(hd ((cons ((cons 1) nil)) nil)))))
(hd 0))))

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

@ -5,8 +5,8 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/contract
racket/match
racket/contract
"tut-subst.rkt")
(provide (all-defined-out))
@ -264,15 +264,21 @@
(define fixed
(term
(;; 2
((cons 1) 2)
((cons 1) nil)
;; 3
((λ (x int) (hd x))
((λ (x (list int)) 1)
7)
;; 4 (if we hadn't changed number->v in cons)
(cons ((cons 0) nil))
;; 5
(tl ((cons 1) nil))
;; 6
(hd ((cons 1) nil))
;; 7
((λ (x int) x) (hd ((cons 1) nil)))
;; 8
((λ (x (list int)) (cons x)) nil)
;; 9
((λ (x int) (λ (y (list int)) x)) 1)
;; 10
((λ (x (list int)) (hd x))
7)
;; 5, 6, 7, 8, 9
((λ (x int) (hd x))
((cons 1) nil))
;; 4
(hd ((cons ((cons 1) nil)) nil)))))
(hd 0))))

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

@ -265,15 +265,21 @@
(define fixed
(term
(;; 2
((cons 1) 2)
((cons 1) nil)
;; 3
((λ (x int) (hd x))
((λ (x (list int)) 1)
7)
;; 4 (if we hadn't changed number->v in cons)
(cons ((cons 0) nil))
;; 5
(tl ((cons 1) nil))
;; 6
(hd ((cons 1) nil))
;; 7
((λ (x int) x) (hd ((cons 1) nil)))
;; 8
((λ (x (list int)) (cons x)) nil)
;; 9
((λ (x int) (λ (y (list int)) x)) 1)
;; 10
((λ (x (list int)) (hd x))
7)
;; 5, 6, 7, 8, 9
((λ (x int) (hd x))
((cons 1) nil))
;; 4
(hd ((cons ((cons 1) nil)) nil)))))
(hd 0))))

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

@ -265,15 +265,21 @@
(define fixed
(term
(;; 2
((cons 1) 2)
((cons 1) nil)
;; 3
((λ (x int) (hd x))
((λ (x (list int)) 1)
7)
;; 4 (if we hadn't changed number->v in cons)
(cons ((cons 0) nil))
;; 5
(tl ((cons 1) nil))
;; 6
(hd ((cons 1) nil))
;; 7
((λ (x int) x) (hd ((cons 1) nil)))
;; 8
((λ (x (list int)) (cons x)) nil)
;; 9
((λ (x int) (λ (y (list int)) x)) 1)
;; 10
((λ (x (list int)) (hd x))
7)
;; 5, 6, 7, 8, 9
((λ (x int) (hd x))
((cons 1) nil))
;; 4
(hd ((cons ((cons 1) nil)) nil)))))
(hd 0))))

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

@ -264,15 +264,21 @@
(define fixed
(term
(;; 2
((cons 1) 2)
((cons 1) nil)
;; 3
((λ (x int) (hd x))
((λ (x (list int)) 1)
7)
;; 4 (if we hadn't changed number->v in cons)
(cons ((cons 0) nil))
;; 5
(tl ((cons 1) nil))
;; 6
(hd ((cons 1) nil))
;; 7
((λ (x int) x) (hd ((cons 1) nil)))
;; 8
((λ (x (list int)) (cons x)) nil)
;; 9
((λ (x int) (λ (y (list int)) x)) 1)
;; 10
((λ (x (list int)) (hd x))
7)
;; 5, 6, 7, 8, 9
((λ (x int) (hd x))
((cons 1) nil))
;; 4
(hd ((cons ((cons 1) nil)) nil)))))
(hd 0))))

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

@ -264,15 +264,21 @@
(define fixed
(term
(;; 2
((cons 1) 2)
((cons 1) nil)
;; 3
((λ (x int) (hd x))
((λ (x (list int)) 1)
7)
;; 4 (if we hadn't changed number->v in cons)
(cons ((cons 0) nil))
;; 5
(tl ((cons 1) nil))
;; 6
(hd ((cons 1) nil))
;; 7
((λ (x int) x) (hd ((cons 1) nil)))
;; 8
((λ (x (list int)) (cons x)) nil)
;; 9
((λ (x int) (λ (y (list int)) x)) 1)
;; 10
((λ (x (list int)) (hd x))
7)
;; 5, 6, 7, 8, 9
((λ (x int) (hd x))
((cons 1) nil))
;; 4
(hd ((cons ((cons 1) nil)) nil)))))
(hd 0))))

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

@ -263,15 +263,21 @@
(define fixed
(term
(;; 2
((cons 1) 2)
((cons 1) nil)
;; 3
((λ (x int) (hd x))
((λ (x (list int)) 1)
7)
;; 4 (if we hadn't changed number->v in cons)
(cons ((cons 0) nil))
;; 5
(tl ((cons 1) nil))
;; 6
(hd ((cons 1) nil))
;; 7
((λ (x int) x) (hd ((cons 1) nil)))
;; 8
((λ (x (list int)) (cons x)) nil)
;; 9
((λ (x int) (λ (y (list int)) x)) 1)
;; 10
((λ (x (list int)) (hd x))
7)
;; 5, 6, 7, 8, 9
((λ (x int) (hd x))
((cons 1) nil))
;; 4
(hd ((cons ((cons 1) nil)) nil)))))
(hd 0))))

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

@ -264,15 +264,21 @@
(define fixed
(term
(;; 2
((cons 1) 2)
((cons 1) nil)
;; 3
((λ (x int) (hd x))
((λ (x (list int)) 1)
7)
;; 4 (if we hadn't changed number->v in cons)
(cons ((cons 0) nil))
;; 5
(tl ((cons 1) nil))
;; 6
(hd ((cons 1) nil))
;; 7
((λ (x int) x) (hd ((cons 1) nil)))
;; 8
((λ (x (list int)) (cons x)) nil)
;; 9
((λ (x int) (λ (y (list int)) x)) 1)
;; 10
((λ (x (list int)) (hd x))
7)
;; 5, 6, 7, 8, 9
((λ (x int) (hd x))
((cons 1) nil))
;; 4
(hd ((cons ((cons 1) nil)) nil)))))
(hd 0))))

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

@ -264,15 +264,21 @@
(define fixed
(term
(;; 2
((cons 1) 2)
((cons 1) nil)
;; 3
((λ (x int) (hd x))
((λ (x (list int)) 1)
7)
;; 4 (if we hadn't changed number->v in cons)
(cons ((cons 0) nil))
;; 5
(tl ((cons 1) nil))
;; 6
(hd ((cons 1) nil))
;; 7
((λ (x int) x) (hd ((cons 1) nil)))
;; 8
((λ (x (list int)) (cons x)) nil)
;; 9
((λ (x int) (λ (y (list int)) x)) 1)
;; 10
((λ (x (list int)) (hd x))
7)
;; 5, 6, 7, 8, 9
((λ (x int) (hd x))
((cons 1) nil))
;; 4
(hd ((cons ((cons 1) nil)) nil)))))
(hd 0))))

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

@ -5,8 +5,8 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/contract
racket/match
racket/contract
"tut-subst.rkt")
(provide (all-defined-out))
@ -247,7 +247,7 @@
[t-type (type-check term)])
;; xxx shouldn't this be t-type IMPLIES this?
(and
(= (length red-res) 1)
(= (length red-res) 1)
(or
(equal? (car red-res) "error")
(equal? t-type (type-check (car red-res))))))))
@ -265,15 +265,21 @@
(define fixed
(term
(;; 2
((cons 1) 2)
((cons 1) nil)
;; 3
((λ (x int) (hd x))
((λ (x (list int)) 1)
7)
;; 4 (if we hadn't changed number->v in cons)
(cons ((cons 0) nil))
;; 5
(tl ((cons 1) nil))
;; 6
(hd ((cons 1) nil))
;; 7
((λ (x int) x) (hd ((cons 1) nil)))
;; 8
((λ (x (list int)) (cons x)) nil)
;; 9
((λ (x int) (λ (y (list int)) x)) 1)
;; 10
((λ (x (list int)) (hd x))
7)
;; 5, 6, 7, 8, 9
((λ (x int) (hd x))
((cons 1) nil))
;; 4
(hd ((cons ((cons 1) nil)) nil)))))
(hd 0))))

21
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/test-file.rkt
View File

@ -189,7 +189,7 @@
[(equal? gen-type 'fixed)
(define some-failed?
(for/or ([t (in-list fixed)])
(define ok? (check t))
(define ok? (check (and (tc t) t)))
(not ok?)))
(unless some-failed?
(error 'fixed "Expected some term to fail, but didn't find one in ~a" fixed))]
@ -240,13 +240,14 @@
(for ([gen-type (in-list types)])
(test-file filename verbose #f gen-type (* minutes 60))))
(call-with-output-file output-file
(λ (out)
(write
(apply append
(for/list ([(type times) (in-hash results)])
(apply append
(for/list ([t times])
(list filename type t)))))
(unless (member 'fixed types)
(call-with-output-file output-file
(λ (out)
(write
(apply append
(for/list ([(type times) (in-hash results)])
(apply append
(for/list ([t times])
(list filename type t)))))
out))
#:exists 'replace)
#:exists 'replace))