From 1ef73b146cfa46cff4e1813d63f9e5e6ca9cca46 Mon Sep 17 00:00:00 2001 From: Max New Date: Sun, 23 Feb 2014 11:49:20 -0600 Subject: [PATCH] Add enum to poly-stlc bench --- .../redex/examples/benchmark/poly-stlc/10.diff | 6 +++--- .../redex/examples/benchmark/poly-stlc/2.diff | 6 +++--- .../redex/examples/benchmark/poly-stlc/3.diff | 6 +++--- .../redex/examples/benchmark/poly-stlc/4.diff | 6 +++--- .../redex/examples/benchmark/poly-stlc/5.diff | 6 +++--- .../redex/examples/benchmark/poly-stlc/6.diff | 6 +++--- .../redex/examples/benchmark/poly-stlc/7.diff | 6 +++--- .../redex/examples/benchmark/poly-stlc/8.diff | 6 +++--- .../redex/examples/benchmark/poly-stlc/9.diff | 6 +++--- .../redex/examples/benchmark/poly-stlc/poly-stlc-10.rkt | 4 ++++ .../redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt | 4 ++++ .../redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt | 4 ++++ .../redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt | 4 ++++ .../redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt | 4 ++++ .../redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt | 4 ++++ .../redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt | 4 ++++ .../redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt | 4 ++++ .../redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt | 4 ++++ .../redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt | 4 ++++ 19 files changed, 67 insertions(+), 27 deletions(-) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/10.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/10.diff index 6976367ebf..8833a15243 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/10.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/10.diff @@ -1,12 +1,12 @@ -11c11 +12c12 < (define the-error "no error") --- > (define the-error "app rule the range of the function is matched to the argument") -72c72 +73c73 < [(typeof Γ M (σ → σ_2)) --- > [(typeof Γ M (σ_2 → σ_2)) -261c261 +262c262 < M] --- > M] diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/2.diff index dd2bd37d65..7828d2587b 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/2.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/2.diff @@ -1,10 +1,10 @@ -11c11 +12c12 < (define the-error "no error") --- > (define the-error "the (([cons @ τ] v) v) value has been omitted") -46d45 +47d46 < (([cons @ τ] v) v) -261,262c260 +262,263c261 < M] < [#f #f])) --- diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/3.diff index 423df29b6a..fcffd11709 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/3.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/3.diff @@ -1,12 +1,12 @@ -11c11 +12c12 < (define the-error "no error") --- > (define the-error "the order of the types in the function position of application has been swapped") -72c72 +73c73 < [(typeof Γ M (σ → σ_2)) --- > [(typeof Γ M (σ_2 → σ)) -261c261 +262c262 < M] --- > M] diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/4.diff index f34cda4c7f..a718d7e909 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/4.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/4.diff @@ -1,12 +1,12 @@ -11c11 +12c12 < (define the-error "no error") --- > (define the-error "the type of cons is incorrect") -119c119 +120c120 < (∀ a (a → ((list a) → (list a))))] --- > (∀ a (a → ((list a) → a)))] -261c261 +262c262 < M] --- > M] diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/5.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/5.diff index 43926df654..c82b84ceb8 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/5.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/5.diff @@ -1,12 +1,12 @@ -11c11 +12c12 < (define the-error "no error") --- > (define the-error "the tail reduction returns the wrong value") -165c165 +166c166 < (in-hole E v_2) --- > (in-hole E v_1) -261c261 +262c262 < M] --- > M] diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/6.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/6.diff index 194a90d1d2..70fcc31c17 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/6.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/6.diff @@ -1,12 +1,12 @@ -11c11 +12c12 < (define the-error "no error") --- > (define the-error "hd reduction acts on partially applied cons") -161c161 +162c162 < (--> (in-hole E ((hd @ τ) (((cons @ τ) v_1) v_2))) --- > (--> (in-hole E ((hd @ τ) ((cons @ τ) v_1))) -261c261 +262c262 < M] --- > M] diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/7.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/7.diff index cefcfac696..7d0a06b54a 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/7.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/7.diff @@ -1,13 +1,13 @@ -11c11 +12c12 < (define the-error "no error") --- > (define the-error "evaluation isn't allowed on the rhs of applications") -49,50c49 +50,51c50 < (E M) < (v E))) --- > (E M))) -261c260 +262c261 < M] --- > M] diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/8.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/8.diff index 4ab4f4b2b0..097e2a9774 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/8.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/8.diff @@ -1,12 +1,12 @@ -11c11 +12c12 < (define the-error "no error") --- > (define the-error "lookup always returns int") -108c108 +109c109 < σ] --- > int] -261c261 +262c262 < M] --- > M] diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/9.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/9.diff index e88bd9c4ff..842f9f2b1e 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/9.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/9.diff @@ -1,12 +1,12 @@ -11c11 +12c12 < (define the-error "no error") --- > (define the-error "variables aren't required to match in lookup") -107c107 +108c108 < [(lookup (x σ Γ) x) --- > [(lookup (x σ Γ) x_2) -261c261 +262c262 < M] --- > M] diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-10.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-10.rkt index c25f119d8f..ddc7a1a816 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-10.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-10.rkt @@ -4,6 +4,7 @@ racket/list racket/match racket/contract + math/base "tut-subst.rkt") (provide (all-defined-out)) @@ -278,3 +279,6 @@ (or (equal? (car red-res) "error") (equal? t-type (type-check (car red-res)))))))) + +(define (generate-enum-term) + (generate-term poly-stlc M #:i-th (random-natural #e10e200))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt index cfd35abe18..a8a9a738b7 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt @@ -4,6 +4,7 @@ racket/list racket/match racket/contract + math/base "tut-subst.rkt") (provide (all-defined-out)) @@ -276,3 +277,6 @@ (or (equal? (car red-res) "error") (equal? t-type (type-check (car red-res)))))))) + +(define (generate-enum-term) + (generate-term poly-stlc M #:i-th (random-natural #e10e200))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt index 7aa19076cd..9feecff405 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt @@ -4,6 +4,7 @@ racket/list racket/match racket/contract + math/base "tut-subst.rkt") (provide (all-defined-out)) @@ -278,3 +279,6 @@ (or (equal? (car red-res) "error") (equal? t-type (type-check (car red-res)))))))) + +(define (generate-enum-term) + (generate-term poly-stlc M #:i-th (random-natural #e10e200))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt index 926c8bdbc1..15ad7c3809 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt @@ -4,6 +4,7 @@ racket/list racket/match racket/contract + math/base "tut-subst.rkt") (provide (all-defined-out)) @@ -278,3 +279,6 @@ (or (equal? (car red-res) "error") (equal? t-type (type-check (car red-res)))))))) + +(define (generate-enum-term) + (generate-term poly-stlc M #:i-th (random-natural #e10e200))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt index 8a49736dce..c8c6832d22 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt @@ -4,6 +4,7 @@ racket/list racket/match racket/contract + math/base "tut-subst.rkt") (provide (all-defined-out)) @@ -278,3 +279,6 @@ (or (equal? (car red-res) "error") (equal? t-type (type-check (car red-res)))))))) + +(define (generate-enum-term) + (generate-term poly-stlc M #:i-th (random-natural #e10e200))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt index 5a915d95ab..b6910ec76c 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt @@ -4,6 +4,7 @@ racket/list racket/match racket/contract + math/base "tut-subst.rkt") (provide (all-defined-out)) @@ -278,3 +279,6 @@ (or (equal? (car red-res) "error") (equal? t-type (type-check (car red-res)))))))) + +(define (generate-enum-term) + (generate-term poly-stlc M #:i-th (random-natural #e10e200))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt index bf80be85d8..bd2e236127 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt @@ -4,6 +4,7 @@ racket/list racket/match racket/contract + math/base "tut-subst.rkt") (provide (all-defined-out)) @@ -277,3 +278,6 @@ (or (equal? (car red-res) "error") (equal? t-type (type-check (car red-res)))))))) + +(define (generate-enum-term) + (generate-term poly-stlc M #:i-th (random-natural #e10e200))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt index 50e7e19877..4de83e5819 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt @@ -4,6 +4,7 @@ racket/list racket/match racket/contract + math/base "tut-subst.rkt") (provide (all-defined-out)) @@ -278,3 +279,6 @@ (or (equal? (car red-res) "error") (equal? t-type (type-check (car red-res)))))))) + +(define (generate-enum-term) + (generate-term poly-stlc M #:i-th (random-natural #e10e200))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt index 200d905d9d..593d4d6024 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt @@ -4,6 +4,7 @@ racket/list racket/match racket/contract + math/base "tut-subst.rkt") (provide (all-defined-out)) @@ -278,3 +279,6 @@ (or (equal? (car red-res) "error") (equal? t-type (type-check (car red-res)))))))) + +(define (generate-enum-term) + (generate-term poly-stlc M #:i-th (random-natural #e10e200))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt index 511c86dadd..774456792b 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt @@ -4,6 +4,7 @@ racket/list racket/match racket/contract + math/base "tut-subst.rkt") (provide (all-defined-out)) @@ -278,3 +279,6 @@ (or (equal? (car red-res) "error") (equal? t-type (type-check (car red-res)))))))) + +(define (generate-enum-term) + (generate-term poly-stlc M #:i-th (random-natural #e10e200)))