From 29fe17729b627736565babc99a407a679efb3e1c Mon Sep 17 00:00:00 2001
From: Robby Findler <robby@racket-lang.org>
Date: Fri, 21 Mar 2014 16:26:04 -0500
Subject: [PATCH] add small counter examples to list machine

Also include test cases that show that the counter
examples type check
---
 .../redex/examples/benchmark/list-machine/1.diff          | 8 ++++++++
 .../redex/examples/benchmark/list-machine/2.diff          | 8 ++++++++
 .../redex/examples/benchmark/list-machine/3.diff          | 8 ++++++++
 .../examples/benchmark/list-machine/list-machine-1.rkt    | 7 +++++++
 .../examples/benchmark/list-machine/list-machine-2.rkt    | 7 +++++++
 .../examples/benchmark/list-machine/list-machine-3.rkt    | 7 +++++++
 6 files changed, 45 insertions(+)

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 ba0f42e718..1b9c494bc9 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
@@ -26,3 +26,11 @@
 <   [(:lookup-Γ Γ v_0 τ_0) (:lookup-Γ Γ v_1 τ_1)
 ---
 >   [(:lookup-Γ Γ v_0 τ_0) (:lookup-Γ Γ v_0 τ_1)
+449a454,460
+> 
+> (define small-counter-example
+>   (term (l0 : (begin (cons v0 Z v0) halt) end)))
+> (test-equal (check small-counter-example) #f)
+> (test-equal (judgment-holds (check-program ,small-counter-example
+>                                            (l0 : (v0 : nil empty) empty)))
+>             #t)
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 7755aacc43..152d275d94 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
@@ -30,3 +30,11 @@
 >          ;; 20 is a small number, but some terms can get exponentially large
 >          (or stopped
 >              (empty? closure)
+449a454,460
+> 
+> (define small-counter-example
+>   (term (l0 : (begin (cons v0 v0 v0) halt) end)))
+> (test-equal (check small-counter-example) #f)
+> (test-equal (judgment-holds (check-program ,small-counter-example
+>                                            (l0 : (v0 : nil empty) empty)))
+>             #t)
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 fa014a0da4..4761daadc8 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
@@ -6,3 +6,11 @@
 <         (p r_2 ι)
 ---
 >         (p r ι)
+449a450,456
+> 
+> (define small-counter-example
+>   (term (l0 : (begin (cons v0 v0 v0) (begin (fetch-field v0 1 v0) halt)) end)))
+> (test-equal (check small-counter-example) #f)
+> (test-equal (judgment-holds (check-program ,small-counter-example
+>                                            (l0 : (v0 : nil empty) empty)))
+>             #t)
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 33fb9aad19..b12ea614dc 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
@@ -451,3 +451,10 @@
                         halt))
         (loop : (jump loop)
               end)))))
+
+(define small-counter-example
+  (term (l0 : (begin (cons v0 Z v0) halt) end)))
+(test-equal (check small-counter-example) #f)
+(test-equal (judgment-holds (check-program ,small-counter-example
+                                           (l0 : (v0 : nil empty) empty)))
+            #t)
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 e5eadcebca..56a25a9b6d 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
@@ -451,3 +451,10 @@
                         halt))
         (loop : (jump loop)
               end)))))
+
+(define small-counter-example
+  (term (l0 : (begin (cons v0 v0 v0) halt) end)))
+(test-equal (check small-counter-example) #f)
+(test-equal (judgment-holds (check-program ,small-counter-example
+                                           (l0 : (v0 : nil empty) empty)))
+            #t)
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 1120ed4bf0..fa948aaef3 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
@@ -447,3 +447,10 @@
                         halt))
         (loop : (jump loop)
               end)))))
+
+(define small-counter-example
+  (term (l0 : (begin (cons v0 v0 v0) (begin (fetch-field v0 1 v0) halt)) end)))
+(test-equal (check small-counter-example) #f)
+(test-equal (judgment-holds (check-program ,small-counter-example
+                                           (l0 : (v0 : nil empty) empty)))
+            #t)