diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/1.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/1.diff index b4249fd0ac..ba0f42e718 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/1.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/1.diff @@ -2,18 +2,18 @@ < (define the-error "no error") --- > (define the-error "confuses the lhs value for the rhs value in cons type rule") -112c112,113 +113c113,114 < (let ([closure (apply-reduction-relation* --- > (let* ([stopped #f] > [closure (apply-reduction-relation* -119c120,122 +120c121,123 < (count . > . 1000) --- > (count . > . 100) > (when (count . > . 100) > (set! stopped #t)) -122,124c125,128 +123,125c126,129 < ;; (if the #:stop-when condition is true, we get back an empty list, < ;; and the same thing for a reduction cycle) < (or (empty? closure) @@ -22,7 +22,7 @@ > ;; (when the reduction is stopped artificially, the current term is returned) > (or stopped > (empty? closure) -225c229 +226c230 < [(:lookup-Γ Γ v_0 τ_0) (:lookup-Γ Γ v_1 τ_1) --- > [(:lookup-Γ Γ v_0 τ_0) (:lookup-Γ Γ v_0 τ_1) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/2.diff index 260130782d..7755aacc43 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/2.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/2.diff @@ -2,23 +2,23 @@ < (define the-error "no error") --- > (define the-error "var-set may skip a var with matching id (in reduction)") -43,44c43 +44,45c44 < [(where #t (different v v_2)) < (var-set r v_2 a_2 r_2) --- > [(var-set r v_2 a_2 r_2) -112c111,112 +113c112,113 < (let ([closure (apply-reduction-relation* --- > (let* ([stopped #f] > [closure (apply-reduction-relation* -119c119,121 +120c120,122 < (count . > . 1000) --- > (count . > . 20) > (when (count . > . 20) > (set! stopped #t)) -121,124c123,128 +122,125c124,129 < ;; if reduction terminates in less than 1000 steps, check it ends with halt < ;; (if the #:stop-when condition is true, we get back an empty list, < ;; and the same thing for a reduction cycle) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/3.diff index b39d09de48..fa014a0da4 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/3.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/3.diff @@ -2,7 +2,7 @@ < (define the-error "no error") --- > (define the-error "cons doesn't actually update the store") -78c78 +79c79 < (p r_2 ι) --- > (p r ι) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-1.rkt index 6b6a181efe..080e6ef58c 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-1.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-1.rkt @@ -4,7 +4,8 @@ (require redex/reduction-semantics racket/list - racket/match) + racket/match + math/base) (provide (all-defined-out)) @@ -430,4 +431,7 @@ 7) [`(check-program ,p ,Π) p] - [#f #f])) \ No newline at end of file + [#f #f])) + +(define (generate-enum-term) + (generate-term list-machine-typing (l0 : ι p) #:i-th (random-natural #e10e200))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-2.rkt index a8656fb788..da7d3b6e13 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-2.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-2.rkt @@ -4,7 +4,8 @@ (require redex/reduction-semantics racket/list - racket/match) + racket/match + math/base) (provide (all-defined-out)) @@ -430,4 +431,7 @@ 7) [`(check-program ,p ,Π) p] - [#f #f])) \ No newline at end of file + [#f #f])) + +(define (generate-enum-term) + (generate-term list-machine-typing (l0 : ι p) #:i-th (random-natural #e10e200))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-3.rkt index 638421a9a8..a1dd59547b 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-3.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-3.rkt @@ -4,7 +4,8 @@ (require redex/reduction-semantics racket/list - racket/match) + racket/match + math/base) (provide (all-defined-out)) @@ -426,4 +427,7 @@ 7) [`(check-program ,p ,Π) p] - [#f #f])) \ No newline at end of file + [#f #f])) + +(define (generate-enum-term) + (generate-term list-machine-typing (l0 : ι p) #:i-th (random-natural #e10e200))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-base.rkt index 5adfd5d7e6..120256151b 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-base.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/list-machine/list-machine-base.rkt @@ -4,7 +4,8 @@ (require redex/reduction-semantics racket/list - racket/match) + racket/match + math/base) (provide (all-defined-out)) @@ -426,4 +427,7 @@ 7) [`(check-program ,p ,Π) p] - [#f #f])) \ No newline at end of file + [#f #f])) + +(define (generate-enum-term) + (generate-term list-machine-typing (l0 : ι p) #:i-th (random-natural #e10e200)))