From 6e3a9861c6000104b13a8af197fee4fd4ae669ff Mon Sep 17 00:00:00 2001 From: Jay McCarthy Date: Wed, 19 Mar 2014 15:10:30 -0600 Subject: [PATCH] removing fixed --- .../benchmark/stlc-sub/stlc-sub-1.rkt | 31 ------------------- .../benchmark/stlc-sub/stlc-sub-2.rkt | 31 ------------------- .../benchmark/stlc-sub/stlc-sub-3.rkt | 31 ------------------- .../benchmark/stlc-sub/stlc-sub-4.rkt | 31 ------------------- .../benchmark/stlc-sub/stlc-sub-5.rkt | 31 ------------------- .../benchmark/stlc-sub/stlc-sub-base.rkt | 31 ------------------- 6 files changed, 186 deletions(-) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt index 631721e758..2e684e4f71 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt @@ -286,34 +286,3 @@ (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. - - ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt index 1ad4deb20d..98e1b8a2fa 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt @@ -288,34 +288,3 @@ (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. - - ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt index 2c57f2237f..373a69477a 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt @@ -288,34 +288,3 @@ (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. - - ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt index 7d2688f9ae..88dc194034 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt @@ -288,34 +288,3 @@ (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. - - ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt index 2278885c2b..a8a53c2a12 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt @@ -288,34 +288,3 @@ (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. - - ))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt index 3fab6149ba..5705699559 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt @@ -288,34 +288,3 @@ (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. - - )))