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

Misc cleanups to stlc and stlc-sub benchmarks:

Browse Source 
- add +
 - tweak definition of c to make more like Palka's dissertation
 - remove non-bugs from stlc-sub
 - share test suite between stlc and stlc-sub
This commit is contained in:
Robby Findler 2014-03-18 16:42:20 -05:00
parent e106ec381f
commit 2dc333de74
43 changed files with 577 additions and 2130 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/make-diffs.rkt
View File

@ -31,4 +31,10 @@
(module+ main
(command-line
#:args ([dir #f])
(void (make-diffs dir))))
(begin
(when dir
(unless (member dir directories)
(raise-user-error 'make-diffs.rkt
"expected one of the following directories: ~s"
directories)))
(void (make-diffs dir)))))

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/make-mutants.rkt
View File

@ -46,4 +46,10 @@
(module+ main
(command-line
#:args ([dir #f])
(void (make-mutants dir))))
(begin
(when dir
(unless (member dir directories)
(raise-user-error 'make-mutants.rkt
"expected one of the following directories: ~s"
directories)))
(void (make-mutants dir)))))

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

@ -8,11 +8,11 @@
12a11,12
> (define the-error "the order of the variable clauses is swapped")
>
104,105d103
106,107d105
< [(subst x x M)
< M]
107a106,107
109a108,109
> [(subst x x M)
> M]
255a256
257a258
>

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

@ -1,16 +0,0 @@
3,4d2
< (define the-error "no error")
<
7d4
< racket/match
8a6
> racket/match
12a11,12
> (define the-error "only substitutes inside of hd constants")
>
114,115c114,115
< [(subst (c M) x M_x)
< (c (subst M x M_x))]
---
> [(subst (hd M) x M_x)
> (hd (subst M x M_x))]

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

@ -8,9 +8,9 @@
12a11,12
> (define the-error "substitutes rator into rand in application")
>
117c117
119c119
< ((subst M x M_x) (subst N x M_x))]
---
> ((subst M x M_x) (subst N x M))]
255a256
257a258
>

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

@ -1,21 +0,0 @@
3,4d2
< (define the-error "no error")
<
7d4
< racket/match
8a6
> racket/match
12a11,12
> (define the-error "substitutes inside of λ that binds the sub variable")
>
108,109d107
< [(subst (λ (x τ) M) x M_x)
< (λ (x τ) M)]
114,115d111
< [(subst (c M) x M_x)
< (c (subst M x M_x))]
117a114,115
> [(subst (c M) x M_x)
> (c (subst M x M_x))]
255a254
>

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

@ -1,12 +0,0 @@
3,4d2
< (define the-error "no error")
<
7d4
< racket/match
8a6
> racket/match
12a11,12
> (define the-error "picks up the bound variable when recurring inside λ")
>
254a255
>

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

@ -1,12 +0,0 @@
3,4d2
< (define the-error "no error")
<
7d4
< racket/match
8a6
> racket/match
12a11,12
> (define the-error "swaps the bound var when recurring inside λ")
>
254a255
>

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

@ -8,9 +8,9 @@
12a11,12
> (define the-error "swaps to/from expressions when recurring inside a constant")
>
115c115
117c117
< (c (subst M x M_x))]
---
> (c (subst M_x x M))]
255a256
257a258
>

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

@ -1,16 +0,0 @@
3,4d2
< (define the-error "no error")
<
7d4
< racket/match
8a6
> racket/match
12a11,12
> (define the-error "swaps the order of the λ clauses")
>
108,109d107
< [(subst (λ (x τ) M) x M_x)
< (λ (x τ) M)]
113a112,113
> [(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 @@
113a114,115
> [(subst (M N) x M_x)
> ((subst M_x x M) (subst N x M_x))]
116,117d117
118,119d119
< [(subst (M N) x M_x)
< ((subst M x M_x) (subst N x M_x))]
255a256
257a258
>

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

@ -15,7 +15,6 @@
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
@ -24,14 +23,14 @@
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
(c d ::= cons nil hd tl + integer)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons number)
((cons number) v))
(cons v)
((cons v) v)
(+ v))
(E hole
(E M)
(v E)))
@ -40,9 +39,6 @@
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
@ -68,7 +64,11 @@
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
((list int) → (list int))]
[(const-type +)
(int → (int → int))]
[(const-type integer)
int])
(define-metafunction stlc
lookup : Γ x -> σ or #f
@ -96,8 +96,10 @@
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define-metafunction stlc
subst : M x M -> M
@ -239,18 +241,21 @@
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
(define candidate
(case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
(match candidate
[`(typeof • ,M ,τ)
M]
[#f #f]))
@ -319,4 +324,3 @@
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
)))

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

@ -1,321 +0,0 @@
#lang racket/base
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/match
racket/contract
math/base)
(provide (all-defined-out))
(define the-error "only substitutes inside of hd constants")
(define-language stlc
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
•)
(σ τ ::=
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons number)
((cons number) v))
(E hole
(E M)
(v E)))
(define-judgment-form stlc
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
[(where τ (lookup Γ x))
----------------------
(typeof Γ x τ)]
[(typeof (x σ Γ) M σ_2)
--------------------------------
(typeof Γ (λ (x σ) M) (σ → σ_2))]
[(typeof Γ M (σ → σ_2))
(typeof Γ M_2 σ)
----------------------
(typeof Γ (M M_2) σ_2)])
(define-metafunction stlc
const-type : c -> σ
[(const-type nil)
(list int)]
[(const-type cons)
(int → ((list int) → (list int)))]
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
(define-metafunction stlc
lookup : Γ x -> σ or #f
[(lookup (x σ Γ) x)
σ]
[(lookup (x σ Γ) x_2)
(lookup Γ x_2)]
[(lookup • x)
#f])
(define red
(reduction-relation
stlc
(--> (in-hole E ((λ (x τ) M) v))
(in-hole E (subst M x v))
"βv")
(--> (in-hole E (hd ((cons v_1) v_2)))
(in-hole E v_1)
"hd")
(--> (in-hole E (tl ((cons v_1) v_2)))
(in-hole E v_2)
"tl")
(--> (in-hole E (hd nil))
"error"
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
(define-metafunction stlc
subst : M x M -> M
[(subst x x M)
M]
[(subst y x M)
y]
[(subst (λ (x τ) M) x M_x)
(λ (x τ) M)]
[(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 (hd M) x M_x)
(hd (subst M x M_x))]
[(subst (M N) x M_x)
((subst M x M_x) (subst N x M_x))]
[(subst M x M_x)
M])
(define-metafunction stlc
[(replace (any_1 ...) x_1 x_new)
((replace any_1 x_1 x_new) ...)]
[(replace x_1 x_1 x_new)
x_new]
[(replace any_1 x_1 x_new)
any_1])
(define M? (redex-match stlc M))
(define/contract (Eval M)
(-> M? (or/c M? "error"))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(unless (pair? M-t)
(error 'Eval "doesn't typecheck: ~s" M))
(define res (apply-reduction-relation* red M))
(unless (= 1 (length res))
(error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
(define ans (car res))
(if (equal? "error" ans)
"error"
(let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
(unless (equal? M-t ans-t)
(error 'Eval "internal error: type soundness fails for ~s" M))
ans)))
(define x? (redex-match stlc x))
(define v? (redex-match stlc v))
(define τ? (redex-match stlc τ))
(define/contract (type-check M)
(-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(cond
[(empty? M-t)
#f]
[(null? (cdr M-t))
(car M-t)]
[else
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
(test-equal (type-check (term 5))
(term int))
(test-equal (type-check (term (5 5)))
#f)
(define (progress-holds? M)
(if (type-check M)
(or (v? M)
(not (null? (apply-reduction-relation red (term ,M)))))
#t))
(define (interesting-term? M)
(and (type-check M)
(term (uses-bound-var? () ,M))))
(define-metafunction stlc
[(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
#t]
[(uses-bound-var? (x_0 ...) (λ (x τ) M))
(uses-bound-var? (x x_0 ...) M)]
[(uses-bound-var? (x ...) (M N))
,(or (term (uses-bound-var? (x ...) M))
(term (uses-bound-var? (x ...) N)))]
[(uses-bound-var? (x ...) (cons M))
(uses-bound-var? (x ...) M)]
[(uses-bound-var? (x ...) any)
#f])
(define (really-interesting-term? M)
(and (interesting-term? M)
(term (applies-bv? () ,M))))
(define-metafunction stlc
[(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
#t]
[(applies-bv? (x_0 ...) (λ (x τ) M))
(applies-bv? (x x_0 ...) M)]
[(applies-bv? (x ...) (M N))
,(or (term (applies-bv? (x ...) M))
(term (applies-bv? (x ...) N)))]
[(applies-bv? (x ...) (cons M))
(applies-bv? (x ...) M)]
[(applies-bv? (x ...) any)
#f])
(define (reduction-step-count/func red v?)
(λ (term)
(let loop ([t term]
[n 0])
(define res (apply-reduction-relation red t))
(cond
[(and (empty? res)
(v? t))
n]
[(and (empty? res)
(equal? t "error"))
n]
[(= (length res) 1)
(loop (car res) (add1 n))]
[else
(error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
(define reduction-step-count
(reduction-step-count/func red v?))
(define (generate-M-term)
(generate-term stlc M 5))
(define (generate-M-term-from-red)
(generate-term #:source red 5))
(define (generate-typed-term)
(match (generate-term stlc
#:satisfying
(typeof • M τ)
5)
[`(typeof • ,M ,τ)
M]
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
[`(typeof • ,M ,τ)
M]
[#f #f]))
(define (typed-generator)
(let ([g (redex-generator stlc
(typeof • M τ)
5)])
(λ ()
(match (g)
[`(typeof • ,M ,τ)
M]
[#f #f]))))
(define (check term)
(or (not term)
(v? term)
(let ([red-res (apply-reduction-relation red term)]
[t-type (type-check term)])
;; xxx should this also be t-type IMPLIES?
(and
(= (length red-res) 1)
(let ([red-t (car red-res)])
(or
(equal? red-t "error")
(let ([red-type (type-check red-t)])
(equal? t-type red-type))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (pick-an-index 0.0001)))
(define (ordered-enum-generator)
(let ([index 0])
(λ ()
(begin0
(generate-term stlc M #:i-th index)
(set! index (add1 index))))))
(define fixed
(term
(;; 1
((λ (x int) x) 1)
;; 9
((λ (x (list int)) (tl x)) ((cons 1) nil))
;; 2 -- xxx I don't think this is really an error because the (M
;; N) case does everything that (c M) does since M can equal
;; c. Otherwise the previous test case would work, because (tl x)
;; would not be subst'd and it has no type
;; 3
((λ (x int) ((λ (y int) y) x)) 1)
;; 4 -- xxx I don't think this is really an error because the
;; normal λ rule always does renaming so this test below works
;; fine and ends up with x1 in both places.
#;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
;; 5 & 6 --- xxx These diffs are bogus because they don't actually
;; make a change to any of the program.
;; 7
((λ (x int) (hd ((cons x) nil))) 1)
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
)))

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

@ -15,7 +15,6 @@
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
@ -24,14 +23,14 @@
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
(c d ::= cons nil hd tl + integer)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons number)
((cons number) v))
(cons v)
((cons v) v)
(+ v))
(E hole
(E M)
(v E)))
@ -40,9 +39,6 @@
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
@ -68,7 +64,11 @@
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
((list int) → (list int))]
[(const-type +)
(int → (int → int))]
[(const-type integer)
int])
(define-metafunction stlc
lookup : Γ x -> σ or #f
@ -96,8 +96,10 @@
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define-metafunction stlc
subst : M x M -> M
@ -239,18 +241,21 @@
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
(define candidate
(case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
(match candidate
[`(typeof • ,M ,τ)
M]
[#f #f]))
@ -319,4 +324,3 @@
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
)))

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

@ -1,320 +0,0 @@
#lang racket/base
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/match
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)
(M N)
number
x
c)
(Γ (x σ Γ)
•)
(σ τ ::=
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons number)
((cons number) v))
(E hole
(E M)
(v E)))
(define-judgment-form stlc
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
[(where τ (lookup Γ x))
----------------------
(typeof Γ x τ)]
[(typeof (x σ Γ) M σ_2)
--------------------------------
(typeof Γ (λ (x σ) M) (σ → σ_2))]
[(typeof Γ M (σ → σ_2))
(typeof Γ M_2 σ)
----------------------
(typeof Γ (M M_2) σ_2)])
(define-metafunction stlc
const-type : c -> σ
[(const-type nil)
(list int)]
[(const-type cons)
(int → ((list int) → (list int)))]
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
(define-metafunction stlc
lookup : Γ x -> σ or #f
[(lookup (x σ Γ) x)
σ]
[(lookup (x σ Γ) x_2)
(lookup Γ x_2)]
[(lookup • x)
#f])
(define red
(reduction-relation
stlc
(--> (in-hole E ((λ (x τ) M) v))
(in-hole E (subst M x v))
"βv")
(--> (in-hole E (hd ((cons v_1) v_2)))
(in-hole E v_1)
"hd")
(--> (in-hole E (tl ((cons v_1) v_2)))
(in-hole E v_2)
"tl")
(--> (in-hole E (hd nil))
"error"
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
(define-metafunction stlc
subst : M x M -> M
[(subst x x M)
M]
[(subst y x M)
y]
[(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 M_x) (subst N x M_x))]
[(subst (c M) x M_x)
(c (subst M x M_x))]
[(subst M x M_x)
M])
(define-metafunction stlc
[(replace (any_1 ...) x_1 x_new)
((replace any_1 x_1 x_new) ...)]
[(replace x_1 x_1 x_new)
x_new]
[(replace any_1 x_1 x_new)
any_1])
(define M? (redex-match stlc M))
(define/contract (Eval M)
(-> M? (or/c M? "error"))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(unless (pair? M-t)
(error 'Eval "doesn't typecheck: ~s" M))
(define res (apply-reduction-relation* red M))
(unless (= 1 (length res))
(error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
(define ans (car res))
(if (equal? "error" ans)
"error"
(let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
(unless (equal? M-t ans-t)
(error 'Eval "internal error: type soundness fails for ~s" M))
ans)))
(define x? (redex-match stlc x))
(define v? (redex-match stlc v))
(define τ? (redex-match stlc τ))
(define/contract (type-check M)
(-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(cond
[(empty? M-t)
#f]
[(null? (cdr M-t))
(car M-t)]
[else
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
(test-equal (type-check (term 5))
(term int))
(test-equal (type-check (term (5 5)))
#f)
(define (progress-holds? M)
(if (type-check M)
(or (v? M)
(not (null? (apply-reduction-relation red (term ,M)))))
#t))
(define (interesting-term? M)
(and (type-check M)
(term (uses-bound-var? () ,M))))
(define-metafunction stlc
[(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
#t]
[(uses-bound-var? (x_0 ...) (λ (x τ) M))
(uses-bound-var? (x x_0 ...) M)]
[(uses-bound-var? (x ...) (M N))
,(or (term (uses-bound-var? (x ...) M))
(term (uses-bound-var? (x ...) N)))]
[(uses-bound-var? (x ...) (cons M))
(uses-bound-var? (x ...) M)]
[(uses-bound-var? (x ...) any)
#f])
(define (really-interesting-term? M)
(and (interesting-term? M)
(term (applies-bv? () ,M))))
(define-metafunction stlc
[(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
#t]
[(applies-bv? (x_0 ...) (λ (x τ) M))
(applies-bv? (x x_0 ...) M)]
[(applies-bv? (x ...) (M N))
,(or (term (applies-bv? (x ...) M))
(term (applies-bv? (x ...) N)))]
[(applies-bv? (x ...) (cons M))
(applies-bv? (x ...) M)]
[(applies-bv? (x ...) any)
#f])
(define (reduction-step-count/func red v?)
(λ (term)
(let loop ([t term]
[n 0])
(define res (apply-reduction-relation red t))
(cond
[(and (empty? res)
(v? t))
n]
[(and (empty? res)
(equal? t "error"))
n]
[(= (length res) 1)
(loop (car res) (add1 n))]
[else
(error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
(define reduction-step-count
(reduction-step-count/func red v?))
(define (generate-M-term)
(generate-term stlc M 5))
(define (generate-M-term-from-red)
(generate-term #:source red 5))
(define (generate-typed-term)
(match (generate-term stlc
#:satisfying
(typeof • M τ)
5)
[`(typeof • ,M ,τ)
M]
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
[`(typeof • ,M ,τ)
M]
[#f #f]))
(define (typed-generator)
(let ([g (redex-generator stlc
(typeof • M τ)
5)])
(λ ()
(match (g)
[`(typeof • ,M ,τ)
M]
[#f #f]))))
(define (check term)
(or (not term)
(v? term)
(let ([red-res (apply-reduction-relation red term)]
[t-type (type-check term)])
;; xxx should this also be t-type IMPLIES?
(and
(= (length red-res) 1)
(let ([red-t (car red-res)])
(or
(equal? red-t "error")
(let ([red-type (type-check red-t)])
(equal? t-type red-type))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (pick-an-index 0.0001)))
(define (ordered-enum-generator)
(let ([index 0])
(λ ()
(begin0
(generate-term stlc M #:i-th index)
(set! index (add1 index))))))
(define fixed
(term
(;; 1
((λ (x int) x) 1)
;; 9
((λ (x (list int)) (tl x)) ((cons 1) nil))
;; 2 -- xxx I don't think this is really an error because the (M
;; N) case does everything that (c M) does since M can equal
;; c. Otherwise the previous test case would work, because (tl x)
;; would not be subst'd and it has no type
;; 3
((λ (x int) ((λ (y int) y) x)) 1)
;; 4 -- xxx I don't think this is really an error because the
;; normal λ rule always does renaming so this test below works
;; fine and ends up with x1 in both places.
#;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
;; 5 & 6 --- xxx These diffs are bogus because they don't actually
;; make a change to any of the program.
;; 7
((λ (x int) (hd ((cons x) nil))) 1)
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
)))

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

@ -1,322 +0,0 @@
#lang racket/base
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/match
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)
(M N)
number
x
c)
(Γ (x σ Γ)
•)
(σ τ ::=
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons number)
((cons number) v))
(E hole
(E M)
(v E)))
(define-judgment-form stlc
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
[(where τ (lookup Γ x))
----------------------
(typeof Γ x τ)]
[(typeof (x σ Γ) M σ_2)
--------------------------------
(typeof Γ (λ (x σ) M) (σ → σ_2))]
[(typeof Γ M (σ → σ_2))
(typeof Γ M_2 σ)
----------------------
(typeof Γ (M M_2) σ_2)])
(define-metafunction stlc
const-type : c -> σ
[(const-type nil)
(list int)]
[(const-type cons)
(int → ((list int) → (list int)))]
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
(define-metafunction stlc
lookup : Γ x -> σ or #f
[(lookup (x σ Γ) x)
σ]
[(lookup (x σ Γ) x_2)
(lookup Γ x_2)]
[(lookup • x)
#f])
(define red
(reduction-relation
stlc
(--> (in-hole E ((λ (x τ) M) v))
(in-hole E (subst M x v))
"βv")
(--> (in-hole E (hd ((cons v_1) v_2)))
(in-hole E v_1)
"hd")
(--> (in-hole E (tl ((cons v_1) v_2)))
(in-hole E v_2)
"tl")
(--> (in-hole E (hd nil))
"error"
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
(define-metafunction stlc
subst : M x M -> M
[(subst x x M)
M]
[(subst y x M)
y]
[(subst (λ (x τ) M) x M_x)
(λ (x τ) M)]
[(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 (c M) x M_x)
(c (subst M x M_x))]
[(subst (M N) x M_x)
((subst M x M_x) (subst N x M_x))]
[(subst M x M_x)
M])
(define-metafunction stlc
[(replace (any_1 ...) x_1 x_new)
((replace any_1 x_1 x_new) ...)]
[(replace x_1 x_1 x_new)
x_new]
[(replace any_1 x_1 x_new)
any_1])
(define M? (redex-match stlc M))
(define/contract (Eval M)
(-> M? (or/c M? "error"))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(unless (pair? M-t)
(error 'Eval "doesn't typecheck: ~s" M))
(define res (apply-reduction-relation* red M))
(unless (= 1 (length res))
(error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
(define ans (car res))
(if (equal? "error" ans)
"error"
(let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
(unless (equal? M-t ans-t)
(error 'Eval "internal error: type soundness fails for ~s" M))
ans)))
(define x? (redex-match stlc x))
(define v? (redex-match stlc v))
(define τ? (redex-match stlc τ))
(define/contract (type-check M)
(-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(cond
[(empty? M-t)
#f]
[(null? (cdr M-t))
(car M-t)]
[else
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
(test-equal (type-check (term 5))
(term int))
(test-equal (type-check (term (5 5)))
#f)
(define (progress-holds? M)
(if (type-check M)
(or (v? M)
(not (null? (apply-reduction-relation red (term ,M)))))
#t))
(define (interesting-term? M)
(and (type-check M)
(term (uses-bound-var? () ,M))))
(define-metafunction stlc
[(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
#t]
[(uses-bound-var? (x_0 ...) (λ (x τ) M))
(uses-bound-var? (x x_0 ...) M)]
[(uses-bound-var? (x ...) (M N))
,(or (term (uses-bound-var? (x ...) M))
(term (uses-bound-var? (x ...) N)))]
[(uses-bound-var? (x ...) (cons M))
(uses-bound-var? (x ...) M)]
[(uses-bound-var? (x ...) any)
#f])
(define (really-interesting-term? M)
(and (interesting-term? M)
(term (applies-bv? () ,M))))
(define-metafunction stlc
[(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
#t]
[(applies-bv? (x_0 ...) (λ (x τ) M))
(applies-bv? (x x_0 ...) M)]
[(applies-bv? (x ...) (M N))
,(or (term (applies-bv? (x ...) M))
(term (applies-bv? (x ...) N)))]
[(applies-bv? (x ...) (cons M))
(applies-bv? (x ...) M)]
[(applies-bv? (x ...) any)
#f])
(define (reduction-step-count/func red v?)
(λ (term)
(let loop ([t term]
[n 0])
(define res (apply-reduction-relation red t))
(cond
[(and (empty? res)
(v? t))
n]
[(and (empty? res)
(equal? t "error"))
n]
[(= (length res) 1)
(loop (car res) (add1 n))]
[else
(error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
(define reduction-step-count
(reduction-step-count/func red v?))
(define (generate-M-term)
(generate-term stlc M 5))
(define (generate-M-term-from-red)
(generate-term #:source red 5))
(define (generate-typed-term)
(match (generate-term stlc
#:satisfying
(typeof • M τ)
5)
[`(typeof • ,M ,τ)
M]
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
[`(typeof • ,M ,τ)
M]
[#f #f]))
(define (typed-generator)
(let ([g (redex-generator stlc
(typeof • M τ)
5)])
(λ ()
(match (g)
[`(typeof • ,M ,τ)
M]
[#f #f]))))
(define (check term)
(or (not term)
(v? term)
(let ([red-res (apply-reduction-relation red term)]
[t-type (type-check term)])
;; xxx should this also be t-type IMPLIES?
(and
(= (length red-res) 1)
(let ([red-t (car red-res)])
(or
(equal? red-t "error")
(let ([red-type (type-check red-t)])
(equal? t-type red-type))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (pick-an-index 0.0001)))
(define (ordered-enum-generator)
(let ([index 0])
(λ ()
(begin0
(generate-term stlc M #:i-th index)
(set! index (add1 index))))))
(define fixed
(term
(;; 1
((λ (x int) x) 1)
;; 9
((λ (x (list int)) (tl x)) ((cons 1) nil))
;; 2 -- xxx I don't think this is really an error because the (M
;; N) case does everything that (c M) does since M can equal
;; c. Otherwise the previous test case would work, because (tl x)
;; would not be subst'd and it has no type
;; 3
((λ (x int) ((λ (y int) y) x)) 1)
;; 4 -- xxx I don't think this is really an error because the
;; normal λ rule always does renaming so this test below works
;; fine and ends up with x1 in both places.
#;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
;; 5 & 6 --- xxx These diffs are bogus because they don't actually
;; make a change to any of the program.
;; 7
((λ (x int) (hd ((cons x) nil))) 1)
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
)))

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

@ -1,322 +0,0 @@
#lang racket/base
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/match
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)
(M N)
number
x
c)
(Γ (x σ Γ)
•)
(σ τ ::=
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons number)
((cons number) v))
(E hole
(E M)
(v E)))
(define-judgment-form stlc
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
[(where τ (lookup Γ x))
----------------------
(typeof Γ x τ)]
[(typeof (x σ Γ) M σ_2)
--------------------------------
(typeof Γ (λ (x σ) M) (σ → σ_2))]
[(typeof Γ M (σ → σ_2))
(typeof Γ M_2 σ)
----------------------
(typeof Γ (M M_2) σ_2)])
(define-metafunction stlc
const-type : c -> σ
[(const-type nil)
(list int)]
[(const-type cons)
(int → ((list int) → (list int)))]
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
(define-metafunction stlc
lookup : Γ x -> σ or #f
[(lookup (x σ Γ) x)
σ]
[(lookup (x σ Γ) x_2)
(lookup Γ x_2)]
[(lookup • x)
#f])
(define red
(reduction-relation
stlc
(--> (in-hole E ((λ (x τ) M) v))
(in-hole E (subst M x v))
"βv")
(--> (in-hole E (hd ((cons v_1) v_2)))
(in-hole E v_1)
"hd")
(--> (in-hole E (tl ((cons v_1) v_2)))
(in-hole E v_2)
"tl")
(--> (in-hole E (hd nil))
"error"
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
(define-metafunction stlc
subst : M x M -> M
[(subst x x M)
M]
[(subst y x M)
y]
[(subst (λ (x τ) M) x M_x)
(λ (x τ) M)]
[(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 (c M) x M_x)
(c (subst M x M_x))]
[(subst (M N) x M_x)
((subst M x M_x) (subst N x M_x))]
[(subst M x M_x)
M])
(define-metafunction stlc
[(replace (any_1 ...) x_1 x_new)
((replace any_1 x_1 x_new) ...)]
[(replace x_1 x_1 x_new)
x_new]
[(replace any_1 x_1 x_new)
any_1])
(define M? (redex-match stlc M))
(define/contract (Eval M)
(-> M? (or/c M? "error"))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(unless (pair? M-t)
(error 'Eval "doesn't typecheck: ~s" M))
(define res (apply-reduction-relation* red M))
(unless (= 1 (length res))
(error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
(define ans (car res))
(if (equal? "error" ans)
"error"
(let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
(unless (equal? M-t ans-t)
(error 'Eval "internal error: type soundness fails for ~s" M))
ans)))
(define x? (redex-match stlc x))
(define v? (redex-match stlc v))
(define τ? (redex-match stlc τ))
(define/contract (type-check M)
(-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(cond
[(empty? M-t)
#f]
[(null? (cdr M-t))
(car M-t)]
[else
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
(test-equal (type-check (term 5))
(term int))
(test-equal (type-check (term (5 5)))
#f)
(define (progress-holds? M)
(if (type-check M)
(or (v? M)
(not (null? (apply-reduction-relation red (term ,M)))))
#t))
(define (interesting-term? M)
(and (type-check M)
(term (uses-bound-var? () ,M))))
(define-metafunction stlc
[(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
#t]
[(uses-bound-var? (x_0 ...) (λ (x τ) M))
(uses-bound-var? (x x_0 ...) M)]
[(uses-bound-var? (x ...) (M N))
,(or (term (uses-bound-var? (x ...) M))
(term (uses-bound-var? (x ...) N)))]
[(uses-bound-var? (x ...) (cons M))
(uses-bound-var? (x ...) M)]
[(uses-bound-var? (x ...) any)
#f])
(define (really-interesting-term? M)
(and (interesting-term? M)
(term (applies-bv? () ,M))))
(define-metafunction stlc
[(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
#t]
[(applies-bv? (x_0 ...) (λ (x τ) M))
(applies-bv? (x x_0 ...) M)]
[(applies-bv? (x ...) (M N))
,(or (term (applies-bv? (x ...) M))
(term (applies-bv? (x ...) N)))]
[(applies-bv? (x ...) (cons M))
(applies-bv? (x ...) M)]
[(applies-bv? (x ...) any)
#f])
(define (reduction-step-count/func red v?)
(λ (term)
(let loop ([t term]
[n 0])
(define res (apply-reduction-relation red t))
(cond
[(and (empty? res)
(v? t))
n]
[(and (empty? res)
(equal? t "error"))
n]
[(= (length res) 1)
(loop (car res) (add1 n))]
[else
(error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
(define reduction-step-count
(reduction-step-count/func red v?))
(define (generate-M-term)
(generate-term stlc M 5))
(define (generate-M-term-from-red)
(generate-term #:source red 5))
(define (generate-typed-term)
(match (generate-term stlc
#:satisfying
(typeof • M τ)
5)
[`(typeof • ,M ,τ)
M]
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
[`(typeof • ,M ,τ)
M]
[#f #f]))
(define (typed-generator)
(let ([g (redex-generator stlc
(typeof • M τ)
5)])
(λ ()
(match (g)
[`(typeof • ,M ,τ)
M]
[#f #f]))))
(define (check term)
(or (not term)
(v? term)
(let ([red-res (apply-reduction-relation red term)]
[t-type (type-check term)])
;; xxx should this also be t-type IMPLIES?
(and
(= (length red-res) 1)
(let ([red-t (car red-res)])
(or
(equal? red-t "error")
(let ([red-type (type-check red-t)])
(equal? t-type red-type))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (pick-an-index 0.0001)))
(define (ordered-enum-generator)
(let ([index 0])
(λ ()
(begin0
(generate-term stlc M #:i-th index)
(set! index (add1 index))))))
(define fixed
(term
(;; 1
((λ (x int) x) 1)
;; 9
((λ (x (list int)) (tl x)) ((cons 1) nil))
;; 2 -- xxx I don't think this is really an error because the (M
;; N) case does everything that (c M) does since M can equal
;; c. Otherwise the previous test case would work, because (tl x)
;; would not be subst'd and it has no type
;; 3
((λ (x int) ((λ (y int) y) x)) 1)
;; 4 -- xxx I don't think this is really an error because the
;; normal λ rule always does renaming so this test below works
;; fine and ends up with x1 in both places.
#;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
;; 5 & 6 --- xxx These diffs are bogus because they don't actually
;; make a change to any of the program.
;; 7
((λ (x int) (hd ((cons x) nil))) 1)
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
)))

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

@ -15,7 +15,6 @@
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
@ -24,14 +23,14 @@
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
(c d ::= cons nil hd tl + integer)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons number)
((cons number) v))
(cons v)
((cons v) v)
(+ v))
(E hole
(E M)
(v E)))
@ -40,9 +39,6 @@
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
@ -68,7 +64,11 @@
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
((list int) → (list int))]
[(const-type +)
(int → (int → int))]
[(const-type integer)
int])
(define-metafunction stlc
lookup : Γ x -> σ or #f
@ -96,8 +96,10 @@
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define-metafunction stlc
subst : M x M -> M
@ -239,18 +241,21 @@
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
(define candidate
(case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
(match candidate
[`(typeof • ,M ,τ)
M]
[#f #f]))
@ -319,4 +324,3 @@
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
)))

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

@ -1,321 +0,0 @@
#lang racket/base
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/match
racket/contract
math/base)
(provide (all-defined-out))
(define the-error "swaps the order of the λ clauses")
(define-language stlc
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
•)
(σ τ ::=
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons number)
((cons number) v))
(E hole
(E M)
(v E)))
(define-judgment-form stlc
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
[(where τ (lookup Γ x))
----------------------
(typeof Γ x τ)]
[(typeof (x σ Γ) M σ_2)
--------------------------------
(typeof Γ (λ (x σ) M) (σ → σ_2))]
[(typeof Γ M (σ → σ_2))
(typeof Γ M_2 σ)
----------------------
(typeof Γ (M M_2) σ_2)])
(define-metafunction stlc
const-type : c -> σ
[(const-type nil)
(list int)]
[(const-type cons)
(int → ((list int) → (list int)))]
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
(define-metafunction stlc
lookup : Γ x -> σ or #f
[(lookup (x σ Γ) x)
σ]
[(lookup (x σ Γ) x_2)
(lookup Γ x_2)]
[(lookup • x)
#f])
(define red
(reduction-relation
stlc
(--> (in-hole E ((λ (x τ) M) v))
(in-hole E (subst M x v))
"βv")
(--> (in-hole E (hd ((cons v_1) v_2)))
(in-hole E v_1)
"hd")
(--> (in-hole E (tl ((cons v_1) v_2)))
(in-hole E v_2)
"tl")
(--> (in-hole E (hd nil))
"error"
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
(define-metafunction stlc
subst : M x M -> M
[(subst x x M)
M]
[(subst y x M)
y]
[(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 (λ (x τ) M) x M_x)
(λ (x τ) M)]
[(subst (c M) x M_x)
(c (subst M x M_x))]
[(subst (M N) x M_x)
((subst M x M_x) (subst N x M_x))]
[(subst M x M_x)
M])
(define-metafunction stlc
[(replace (any_1 ...) x_1 x_new)
((replace any_1 x_1 x_new) ...)]
[(replace x_1 x_1 x_new)
x_new]
[(replace any_1 x_1 x_new)
any_1])
(define M? (redex-match stlc M))
(define/contract (Eval M)
(-> M? (or/c M? "error"))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(unless (pair? M-t)
(error 'Eval "doesn't typecheck: ~s" M))
(define res (apply-reduction-relation* red M))
(unless (= 1 (length res))
(error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
(define ans (car res))
(if (equal? "error" ans)
"error"
(let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
(unless (equal? M-t ans-t)
(error 'Eval "internal error: type soundness fails for ~s" M))
ans)))
(define x? (redex-match stlc x))
(define v? (redex-match stlc v))
(define τ? (redex-match stlc τ))
(define/contract (type-check M)
(-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(cond
[(empty? M-t)
#f]
[(null? (cdr M-t))
(car M-t)]
[else
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
(test-equal (type-check (term 5))
(term int))
(test-equal (type-check (term (5 5)))
#f)
(define (progress-holds? M)
(if (type-check M)
(or (v? M)
(not (null? (apply-reduction-relation red (term ,M)))))
#t))
(define (interesting-term? M)
(and (type-check M)
(term (uses-bound-var? () ,M))))
(define-metafunction stlc
[(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
#t]
[(uses-bound-var? (x_0 ...) (λ (x τ) M))
(uses-bound-var? (x x_0 ...) M)]
[(uses-bound-var? (x ...) (M N))
,(or (term (uses-bound-var? (x ...) M))
(term (uses-bound-var? (x ...) N)))]
[(uses-bound-var? (x ...) (cons M))
(uses-bound-var? (x ...) M)]
[(uses-bound-var? (x ...) any)
#f])
(define (really-interesting-term? M)
(and (interesting-term? M)
(term (applies-bv? () ,M))))
(define-metafunction stlc
[(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
#t]
[(applies-bv? (x_0 ...) (λ (x τ) M))
(applies-bv? (x x_0 ...) M)]
[(applies-bv? (x ...) (M N))
,(or (term (applies-bv? (x ...) M))
(term (applies-bv? (x ...) N)))]
[(applies-bv? (x ...) (cons M))
(applies-bv? (x ...) M)]
[(applies-bv? (x ...) any)
#f])
(define (reduction-step-count/func red v?)
(λ (term)
(let loop ([t term]
[n 0])
(define res (apply-reduction-relation red t))
(cond
[(and (empty? res)
(v? t))
n]
[(and (empty? res)
(equal? t "error"))
n]
[(= (length res) 1)
(loop (car res) (add1 n))]
[else
(error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
(define reduction-step-count
(reduction-step-count/func red v?))
(define (generate-M-term)
(generate-term stlc M 5))
(define (generate-M-term-from-red)
(generate-term #:source red 5))
(define (generate-typed-term)
(match (generate-term stlc
#:satisfying
(typeof • M τ)
5)
[`(typeof • ,M ,τ)
M]
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
[`(typeof • ,M ,τ)
M]
[#f #f]))
(define (typed-generator)
(let ([g (redex-generator stlc
(typeof • M τ)
5)])
(λ ()
(match (g)
[`(typeof • ,M ,τ)
M]
[#f #f]))))
(define (check term)
(or (not term)
(v? term)
(let ([red-res (apply-reduction-relation red term)]
[t-type (type-check term)])
;; xxx should this also be t-type IMPLIES?
(and
(= (length red-res) 1)
(let ([red-t (car red-res)])
(or
(equal? red-t "error")
(let ([red-type (type-check red-t)])
(equal? t-type red-type))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (pick-an-index 0.0001)))
(define (ordered-enum-generator)
(let ([index 0])
(λ ()
(begin0
(generate-term stlc M #:i-th index)
(set! index (add1 index))))))
(define fixed
(term
(;; 1
((λ (x int) x) 1)
;; 9
((λ (x (list int)) (tl x)) ((cons 1) nil))
;; 2 -- xxx I don't think this is really an error because the (M
;; N) case does everything that (c M) does since M can equal
;; c. Otherwise the previous test case would work, because (tl x)
;; would not be subst'd and it has no type
;; 3
((λ (x int) ((λ (y int) y) x)) 1)
;; 4 -- xxx I don't think this is really an error because the
;; normal λ rule always does renaming so this test below works
;; fine and ends up with x1 in both places.
#;((λ (x int) ((λ (x (list int)) x) ((cons x) nil))) 1)
;; 5 & 6 --- xxx These diffs are bogus because they don't actually
;; make a change to any of the program.
;; 7
((λ (x int) (hd ((cons x) nil))) 1)
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
)))

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

@ -15,7 +15,6 @@
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
@ -24,14 +23,14 @@
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
(c d ::= cons nil hd tl + integer)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons number)
((cons number) v))
(cons v)
((cons v) v)
(+ v))
(E hole
(E M)
(v E)))
@ -40,9 +39,6 @@
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
@ -68,7 +64,11 @@
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
((list int) → (list int))]
[(const-type +)
(int → (int → int))]
[(const-type integer)
int])
(define-metafunction stlc
lookup : Γ x -> σ or #f
@ -96,8 +96,10 @@
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define-metafunction stlc
subst : M x M -> M
@ -109,10 +111,10 @@
(λ (x τ) M)]
[(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))]
(where x_new ,(variable-not-in (term (x_1 e x_2))
(term x_1)))]
[(subst (c M) x M_x)
(c (subst M x M_x))]
[(subst M x M_x)
@ -239,18 +241,21 @@
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
(define candidate
(case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
(match candidate
[`(typeof • ,M ,τ)
M]
[#f #f]))
@ -319,4 +324,3 @@
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
)))

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

@ -15,7 +15,6 @@
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
@ -24,14 +23,14 @@
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
(c d ::= cons nil hd tl + integer)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons number)
((cons number) v))
(cons v)
((cons v) v)
(+ v))
(E hole
(E M)
(v E)))
@ -40,9 +39,6 @@
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
@ -68,7 +64,11 @@
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
((list int) → (list int))]
[(const-type +)
(int → (int → int))]
[(const-type integer)
int])
(define-metafunction stlc
lookup : Γ x -> σ or #f
@ -96,8 +96,10 @@
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define-metafunction stlc
subst : M x M -> M
@ -239,20 +241,23 @@
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
(define candidate
(case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
(match candidate
[`(typeof • ,M ,τ)
M]
[#f #f]))
(define (typed-generator)
(let ([g (redex-generator stlc
(typeof • M τ)
@ -318,4 +323,3 @@
;; 8 -- xxx This isn't an error for the same reason 4 isn't.
)))

7
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/tests.rkt Normal file
View File

@ -0,0 +1,7 @@
#lang racket/base
(require "stlc-sub-base.rkt" "../stlc/tests-lib.rkt")
(stlc-tests uses-bound-var?
typeof
red
reduction-step-count
Eval)

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

@ -1,10 +1,12 @@
3c3
< (define the-error "no error")
< (define the-error "the ((cons v) v) value has been omitted")
---
> (define the-error "app rule the range of the function is matched to the argument")
58c58
31a32
> ((cons v) v)
53c54
< (typeof Γ M_2 σ)
---
> (typeof Γ M_2 σ_2)
232d231
236d236
<

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

@ -1,9 +1,6 @@
3c3
< (define the-error "no error")
< (define the-error "the ((cons v) v) value has been omitted")
---
> (define the-error "the ((cons number) v) value has been omitted")
33,34c33
< (cons v)
< ((cons v) v))
---
> (cons v))
31a32
> ((cons v) v)

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

@ -1,8 +1,10 @@
3c3
< (define the-error "no error")
< (define the-error "the ((cons v) v) value has been omitted")
---
> (define the-error "the order of the types in the function position of application has been swapped")
57c57
31a32
> ((cons v) v)
52c53
< [(typeof Γ M (σ → σ_2))
---
> [(typeof Γ M (σ_2 → σ))

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

@ -1,8 +1,10 @@
3c3
< (define the-error "no error")
< (define the-error "the ((cons v) v) value has been omitted")
---
> (define the-error "the type of cons is incorrect")
67c67
31a32
> ((cons v) v)
62c63
< (int → ((list int) → (list int)))]
---
> (int → ((list int) → int))]

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

@ -1,10 +1,12 @@
3c3
< (define the-error "no error")
< (define the-error "the ((cons v) v) value has been omitted")
---
> (define the-error "the tail reduction returns the wrong value")
92c92
31a32
> ((cons v) v)
91c92
< (in-hole E v_2)
---
> (in-hole E v_1)
232d231
236d236
<

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

@ -1,10 +1,12 @@
3c3
< (define the-error "no error")
< (define the-error "the ((cons v) v) value has been omitted")
---
> (define the-error "hd reduction acts on partially applied cons")
88c88
31a32
> ((cons v) v)
87c88
< (--> (in-hole E (hd ((cons v_1) v_2)))
---
> (--> (in-hole E (hd (cons v_1)))
232d231
236d236
<

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

@ -1,11 +1,13 @@
3c3
< (define the-error "no error")
< (define the-error "the ((cons v) v) value has been omitted")
---
> (define the-error "evaluation isn't allowed on the rhs of applications")
36,37c36
31a32
> ((cons v) v)
34,35c35
< (E M)
< (v E)))
---
> (E M)))
232d230
236d235
<

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

@ -1,10 +1,12 @@
3c3
< (define the-error "no error")
< (define the-error "the ((cons v) v) value has been omitted")
---
> (define the-error "lookup always returns int")
76c76
31a32
> ((cons v) v)
75c76
< σ]
---
> int]
232d231
236d236
<

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

@ -1,10 +1,12 @@
3c3
< (define the-error "no error")
< (define the-error "the ((cons v) v) value has been omitted")
---
> (define the-error "variables aren't required to match in lookup")
75c75
31a32
> ((cons v) v)
74c75
< [(lookup (x σ Γ) x)
---
> [(lookup (x σ Γ) x_2)
232d231
236d236
<

47
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-10.rkt → pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/stlc-1.rkt
View File

@ -4,8 +4,8 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/match
racket/list
racket/contract
"tut-subst.rkt")
@ -15,7 +15,6 @@
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
@ -24,14 +23,14 @@
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
(c d ::= cons nil hd tl + integer)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons v)
((cons v) v))
((cons v) v)
(+ v))
(E hole
(E M)
(v E)))
@ -40,9 +39,6 @@
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
@ -68,7 +64,11 @@
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
((list int) → (list int))]
[(const-type +)
(int → (int → int))]
[(const-type integer)
int])
(define-metafunction stlc
lookup : Γ x -> σ or #f
@ -96,7 +96,10 @@
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match stlc M))
(define/contract (Eval M)
@ -215,17 +218,19 @@
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
(define candidate
(case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
(match candidate
[`(typeof • ,M ,τ)
M]
[#f #f]))

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

@ -4,8 +4,8 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/match
racket/list
racket/contract
"tut-subst.rkt")
@ -15,7 +15,6 @@
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
@ -24,13 +23,14 @@
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
(c d ::= cons nil hd tl + integer)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons v))
(cons v)
((cons v) v)
(+ v))
(E hole
(E M)
(v E)))
@ -39,9 +39,6 @@
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
@ -67,7 +64,11 @@
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
((list int) → (list int))]
[(const-type +)
(int → (int → int))]
[(const-type integer)
int])
(define-metafunction stlc
lookup : Γ x -> σ or #f
@ -95,7 +96,10 @@
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match stlc M))
(define/contract (Eval M)
@ -214,17 +218,19 @@
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
(define candidate
(case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
(match candidate
[`(typeof • ,M ,τ)
M]
[#f #f]))

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

@ -4,8 +4,8 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/match
racket/list
racket/contract
"tut-subst.rkt")
@ -15,7 +15,6 @@
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
@ -24,14 +23,14 @@
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
(c d ::= cons nil hd tl + integer)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons v)
((cons v) v))
((cons v) v)
(+ v))
(E hole
(E M)
(v E)))
@ -40,9 +39,6 @@
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
@ -68,7 +64,11 @@
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
((list int) → (list int))]
[(const-type +)
(int → (int → int))]
[(const-type integer)
int])
(define-metafunction stlc
lookup : Γ x -> σ or #f
@ -96,7 +96,10 @@
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match stlc M))
(define/contract (Eval M)
@ -215,17 +218,19 @@
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
(define candidate
(case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
(match candidate
[`(typeof • ,M ,τ)
M]
[#f #f]))

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

@ -4,8 +4,8 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/match
racket/list
racket/contract
"tut-subst.rkt")
@ -15,7 +15,6 @@
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
@ -24,14 +23,14 @@
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
(c d ::= cons nil hd tl + integer)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons v)
((cons v) v))
((cons v) v)
(+ v))
(E hole
(E M)
(v E)))
@ -40,9 +39,6 @@
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
@ -68,7 +64,11 @@
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
((list int) → (list int))]
[(const-type +)
(int → (int → int))]
[(const-type integer)
int])
(define-metafunction stlc
lookup : Γ x -> σ or #f
@ -96,7 +96,10 @@
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match stlc M))
(define/contract (Eval M)
@ -215,17 +218,19 @@
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
(define candidate
(case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
(match candidate
[`(typeof • ,M ,τ)
M]
[#f #f]))

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

@ -4,8 +4,8 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/match
racket/list
racket/contract
"tut-subst.rkt")
@ -15,7 +15,6 @@
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
@ -24,14 +23,14 @@
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
(c d ::= cons nil hd tl + integer)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons v)
((cons v) v))
((cons v) v)
(+ v))
(E hole
(E M)
(v E)))
@ -40,9 +39,6 @@
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
@ -68,7 +64,11 @@
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
((list int) → (list int))]
[(const-type +)
(int → (int → int))]
[(const-type integer)
int])
(define-metafunction stlc
lookup : Γ x -> σ or #f
@ -96,7 +96,10 @@
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match stlc M))
(define/contract (Eval M)
@ -215,17 +218,19 @@
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
(define candidate
(case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
(match candidate
[`(typeof • ,M ,τ)
M]
[#f #f]))

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

@ -4,8 +4,8 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/match
racket/list
racket/contract
"tut-subst.rkt")
@ -15,7 +15,6 @@
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
@ -24,14 +23,14 @@
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
(c d ::= cons nil hd tl + integer)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons v)
((cons v) v))
((cons v) v)
(+ v))
(E hole
(E M)
(v E)))
@ -40,9 +39,6 @@
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
@ -68,7 +64,11 @@
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
((list int) → (list int))]
[(const-type +)
(int → (int → int))]
[(const-type integer)
int])
(define-metafunction stlc
lookup : Γ x -> σ or #f
@ -96,7 +96,10 @@
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match stlc M))
(define/contract (Eval M)
@ -215,17 +218,19 @@
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
(define candidate
(case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
(match candidate
[`(typeof • ,M ,τ)
M]
[#f #f]))

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

@ -4,8 +4,8 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/match
racket/list
racket/contract
"tut-subst.rkt")
@ -15,7 +15,6 @@
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
@ -24,14 +23,14 @@
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
(c d ::= cons nil hd tl + integer)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons v)
((cons v) v))
((cons v) v)
(+ v))
(E hole
(E M)))
@ -39,9 +38,6 @@
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
@ -67,7 +63,11 @@
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
((list int) → (list int))]
[(const-type +)
(int → (int → int))]
[(const-type integer)
int])
(define-metafunction stlc
lookup : Γ x -> σ or #f
@ -95,7 +95,10 @@
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match stlc M))
(define/contract (Eval M)
@ -214,17 +217,19 @@
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
(define candidate
(case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
(match candidate
[`(typeof • ,M ,τ)
M]
[#f #f]))

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

@ -4,8 +4,8 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/match
racket/list
racket/contract
"tut-subst.rkt")
@ -15,7 +15,6 @@
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
@ -24,14 +23,14 @@
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
(c d ::= cons nil hd tl + integer)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons v)
((cons v) v))
((cons v) v)
(+ v))
(E hole
(E M)
(v E)))
@ -40,9 +39,6 @@
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
@ -68,7 +64,11 @@
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
((list int) → (list int))]
[(const-type +)
(int → (int → int))]
[(const-type integer)
int])
(define-metafunction stlc
lookup : Γ x -> σ or #f
@ -96,7 +96,10 @@
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match stlc M))
(define/contract (Eval M)
@ -215,17 +218,19 @@
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
(define candidate
(case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
(match candidate
[`(typeof • ,M ,τ)
M]
[#f #f]))

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

@ -4,8 +4,8 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/match
racket/list
racket/contract
"tut-subst.rkt")
@ -15,7 +15,6 @@
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
@ -24,14 +23,14 @@
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
(c d ::= cons nil hd tl + integer)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons v)
((cons v) v))
((cons v) v)
(+ v))
(E hole
(E M)
(v E)))
@ -40,9 +39,6 @@
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
@ -68,7 +64,11 @@
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
((list int) → (list int))]
[(const-type +)
(int → (int → int))]
[(const-type integer)
int])
(define-metafunction stlc
lookup : Γ x -> σ or #f
@ -96,7 +96,10 @@
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match stlc M))
(define/contract (Eval M)
@ -215,17 +218,19 @@
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
(define candidate
(case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
(match candidate
[`(typeof • ,M ,τ)
M]
[#f #f]))

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

@ -1,11 +1,11 @@
#lang racket/base
(define the-error "no error")
(define the-error "the ((cons v) v) value has been omitted")
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/match
racket/list
racket/contract
"tut-subst.rkt")
@ -15,7 +15,6 @@
(M N ::=
(λ (x σ) M)
(M N)
number
x
c)
(Γ (x σ Γ)
@ -24,14 +23,13 @@
int
(list int)
(σ → τ))
(c d ::= cons nil hd tl)
(c d ::= cons nil hd tl + integer)
((x y) variable-not-otherwise-mentioned)
(v (λ (x τ) M)
c
number
(cons v)
((cons v) v))
(+ v))
(E hole
(E M)
(v E)))
@ -40,9 +38,6 @@
#:mode (typeof I I O)
#:contract (typeof Γ M σ)
[---------------------
(typeof Γ number int)]
[---------------------------
(typeof Γ c (const-type c))]
@ -68,7 +63,11 @@
[(const-type hd)
((list int) → int)]
[(const-type tl)
((list int) → (list int))])
((list int) → (list int))]
[(const-type +)
(int → (int → int))]
[(const-type integer)
int])
(define-metafunction stlc
lookup : Γ x -> σ or #f
@ -96,7 +95,10 @@
"hd-err")
(--> (in-hole E (tl nil))
"error"
"tl-err")))
"tl-err")
(--> (in-hole E ((+ integer_1) integer_2))
(in-hole E ,(+ (term integer_1) (term integer_2)))
"+")))
(define M? (redex-match stlc M))
(define/contract (Eval M)
@ -215,17 +217,19 @@
[#f #f]))
(define (generate-typed-term-from-red)
(match (case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)])
(define candidate
(case (random 5)
[(0)
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
[(1)
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(2)
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
[(3)
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
[(4)
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
(match candidate
[`(typeof • ,M ,τ)
M]
[#f #f]))

102
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/tests-lib.rkt Normal file
View File

@ -0,0 +1,102 @@
#lang racket/base
(require redex/reduction-semantics)
(provide stlc-tests)
(define-syntax-rule
(stlc-tests uses-bound-var?
typeof
red
reduction-step-count
Eval)
(begin
(test-equal (term (uses-bound-var? () 5))
#f)
(test-equal (term (uses-bound-var? () nil))
#f)
(test-equal (term (uses-bound-var? () (λ (x int) x)))
#t)
(test-equal (term (uses-bound-var? () (λ (x int) y)))
#f)
(test-equal (term (uses-bound-var? () ((λ (x int) x) 5)))
#t)
(test-equal (term (uses-bound-var? () ((λ (x int) xy) 5)))
#f)
(test-equal (judgment-holds (typeof • 5 τ) τ)
(list (term int)))
(test-equal (judgment-holds (typeof • nil τ) τ)
(list (term (list int))))
(test-equal (judgment-holds (typeof • (cons 1) τ) τ)
(list (term ((list int) → (list int)))))
(test-equal (judgment-holds (typeof • ((cons 1) nil) τ) τ)
(list (term (list int))))
(test-equal (judgment-holds (typeof • (λ (x int) x) τ) τ)
(list (term (int → int))))
(test-equal (judgment-holds (typeof • (λ (x (int → int)) (λ (y int) x)) τ) τ)
(list (term ((int → int) → (int → (int → int))))))
(test-equal (judgment-holds (typeof • ((+ ((+ 1) 2)) ((+ 3) 4)) τ) τ)
(list (term int)))
(test-->> red (term ((λ (x int) x) 7)) (term 7))
(test-->> red (term (((λ (x int) (λ (x int) x)) 2) 1)) (term 1))
(test-->> red (term (((λ (x int) (λ (y int) x)) 2) 1)) (term 2))
(test-->> red
(term ((λ (x int) ((cons x) nil)) 11))
(term ((cons 11) nil)))
(test-->> red
(term ((λ (x int) ((cons x) nil)) 11))
(term ((cons 11) nil)))
(test-->> red
(term ((cons ((λ (x int) x) 11)) nil))
(term ((cons 11) nil)))
(test-->> red
(term (cons ((λ (x int) x) 1)))
(term (cons 1)))
(test-->> red
(term ((cons ((λ (x int) x) 1)) nil))
(term ((cons 1) nil)))
(test-->> red
(term (hd ((λ (x int) ((cons x) nil)) 11)))
(term 11))
(test-->> red
(term (tl ((λ (x int) ((cons x) nil)) 11)))
(term nil))
(test-->> red
(term (tl nil))
"error")
(test-->> red
(term (hd nil))
"error")
(test-->> red
(term ((+ 1) (hd nil)))
"error")
(test-->> red
(term ((+ ((+ 1) 2)) ((+ 3) 4)))
(term 10))
(test-->> red
(term ((λ (f (int → (list int))) (f 3)) (cons 1)))
(term ((cons 1) 3)))
(test-->> red
(term ((λ (f (int → int)) (f 3)) (+ 1)))
(term 4))
(test-equal (Eval (term ((λ (x int) x) 3)))
(term 3))
(test-equal (reduction-step-count (term (λ (x int) x)))
0)
(test-equal (reduction-step-count (term ((λ (x int) x) 1)))
1)
(test-equal (reduction-step-count (term ((λ (x int) x) 1)))
1)
(test-equal (reduction-step-count (term ((cons 1) nil)))
0)
(test-equal (reduction-step-count (term (hd ((cons 1) nil))))
1)
(test-equal (reduction-step-count (term (hd nil)))
1)
(test-equal (reduction-step-count (term ((λ (x int) x) (hd ((cons 1) nil)))))
2)
(test-results)))

86
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/tests.rkt
View File

@ -1,81 +1,7 @@
#lang racket/base
(require redex/reduction-semantics
"stlc-base.rkt")
(test-equal (term (uses-bound-var? () 5))
#f)
(test-equal (term (uses-bound-var? () nil))
#f)
(test-equal (term (uses-bound-var? () (λ (x int) x)))
#t)
(test-equal (term (uses-bound-var? () (λ (x int) y)))
#f)
(test-equal (term (uses-bound-var? () ((λ (x int) x) 5)))
#t)
(test-equal (term (uses-bound-var? () ((λ (x int) xy) 5)))
#f)
(test-equal (judgment-holds (typeof • 5 τ) τ)
(list (term int)))
(test-equal (judgment-holds (typeof • nil τ) τ)
(list (term (list int))))
(test-equal (judgment-holds (typeof • (cons 1) τ) τ)
(list (term ((list int) → (list int)))))
(test-equal (judgment-holds (typeof • ((cons 1) nil) τ) τ)
(list (term (list int))))
(test-equal (judgment-holds (typeof • (λ (x int) x) τ) τ)
(list (term (int → int))))
(test-equal (judgment-holds (typeof • (λ (x (int → int)) (λ (y int) x)) τ) τ)
(list (term ((int → int) → (int → (int → int))))))
(test-->> red (term ((λ (x int) x) 7)) (term 7))
(test-->> red (term (((λ (x int) (λ (x int) x)) 2) 1)) (term 1))
(test-->> red (term (((λ (x int) (λ (y int) x)) 2) 1)) (term 2))
(test-->> red
(term ((λ (x int) ((cons x) nil)) 11))
(term ((cons 11) nil)))
(test-->> red
(term ((λ (x int) ((cons x) nil)) 11))
(term ((cons 11) nil)))
(test-->> red
(term ((cons ((λ (x int) x) 11)) nil))
(term ((cons 11) nil)))
(test-->> red
(term (cons ((λ (x int) x) 1)))
(term (cons 1)))
(test-->> red
(term ((cons ((λ (x int) x) 1)) nil))
(term ((cons 1) nil)))
(test-->> red
(term (hd ((λ (x int) ((cons x) nil)) 11)))
(term 11))
(test-->> red
(term (tl ((λ (x int) ((cons x) nil)) 11)))
(term nil))
(test-->> red
(term (tl nil))
"error")
(test-->> red
(term (hd nil))
"error")
(test-equal (Eval (term ((λ (x int) x) 3)))
(term 3))
(test-equal (reduction-step-count (term (λ (x int) x)))
0)
(test-equal (reduction-step-count (term ((λ (x int) x) 1)))
1)
(test-equal (reduction-step-count (term ((λ (x int) x) 1)))
1)
(test-equal (reduction-step-count (term ((cons 1) nil)))
0)
(test-equal (reduction-step-count (term (hd ((cons 1) nil))))
1)
(test-equal (reduction-step-count (term (hd nil)))
1)
(test-equal (reduction-step-count (term ((λ (x int) x) (hd ((cons 1) nil)))))
2)
(test-results)
(require "stlc-base.rkt" "tests-lib.rkt")
(stlc-tests uses-bound-var?
typeof
red
reduction-step-count
Eval)