add delim-cont counterexamples, adjust check property

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/1.diff

@@ -11,32 +11,20 @@
 >         (monitor ctc (ccm mk t) k l j) 
 326a330
 > 
-938a943
+939a944
+> 
+949a955,968
 > 
-948a954,979
 > (define small-counter-example
->   (term
->    ;; (List Num)
->    (ccm 
->     ;; (Mark Num)
->     (MG ;; (Con Num)
->         (flat (λ (x : Num) (number? x)))
->         ;; (Mark Num)
->         (make-cm-key Num)
->         "k" "l" "j")
->     Num)))
+>   '(ccm 
+>     (monitor 
+>      (mark/c 
+>       (mark/c (flat (λ (p : Num) #t)) 
+>               Num)
+>       (Mark Num)) 
+>      (make-cm-key (Mark Num))
+>      "" "" "") 
+>     (Mark Num)))
 > 
-> (local 
->  ()
->  (define ctc-fun (term (λ (x : Num) (number? x))))
->  (test-equal (judgment-holds (tc · · ,ctc-fun (→ Num Bool))) #t)
->  (define ctc (term (flat ,ctc-fun)))
->  (test-equal (judgment-holds (tcc · · ,ctc (Con Num))) #t)
->  (define v (term (make-cm-key Num)))
->  (test-equal (judgment-holds (tc · · ,v (Mark Num))) #t)
->  (test-equal (redex-match? abort-lang l "k") #t)
->  (test-equal (redex-match? abort-lang l "l") #t)
->  (test-equal (redex-match? abort-lang l "j") #t)
->  ;; XXX This makes no sense, given the definition on line 495
->  (test-equal (judgment-holds (tc · · (MG ,ctc ,v "k" "l" "j") (Mark Num))) #t))
 > (test-equal (check small-counter-example) #f)
+> 

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/2.diff

@@ -8,6 +8,14 @@
 >    (--> (monitor ctc (cons v_1 v_2) k l j)
 326a327
 > 
-937a939,940
+939a941,942
 > 
 > 
+949a953,958
+> (define small-counter-example
+>   '(monitor (list/c (flat (λ (k : Bool) #t))) 
+>             (cons #t (null Bool)) 
+>             "" "" ""))
+> 
+> (test-equal (check small-counter-example) #f)
+\ No newline at end of file

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/3.diff

@@ -8,6 +8,6 @@
 <   [(tc Γ Σ e_1 (→ (→ t_3 t_2) t_3))
 ---
 >   [(tc Γ Σ e_1 (→ t_2 t_3))
-937a939,940
+939a941,942
 > 
 > 

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-1.rkt

@@ -935,7 +935,8 @@
 
 (define (check term)
   (or (not term)
-      (soundness-holds? term)))
+      (implies (type-check term)
+               (soundness-holds? term))))
 
 (define (type-check e)
   (judgment-holds (tc · · ,e t)))
@@ -951,29 +952,17 @@
       (set! index (add1 index))
       (generate-term abort-lang e #:i-th index))))
 
-(define small-counter-example
-  (term
-   ;; (List Num)
-   (ccm 
-    ;; (Mark Num)
-    (MG ;; (Con Num)
-        (flat (λ (x : Num) (number? x)))
-        ;; (Mark Num)
-        (make-cm-key Num)
-        "k" "l" "j")
-    Num)))
 
-(local 
- ()
- (define ctc-fun (term (λ (x : Num) (number? x))))
- (test-equal (judgment-holds (tc · · ,ctc-fun (→ Num Bool))) #t)
- (define ctc (term (flat ,ctc-fun)))
- (test-equal (judgment-holds (tcc · · ,ctc (Con Num))) #t)
- (define v (term (make-cm-key Num)))
- (test-equal (judgment-holds (tc · · ,v (Mark Num))) #t)
- (test-equal (redex-match? abort-lang l "k") #t)
- (test-equal (redex-match? abort-lang l "l") #t)
- (test-equal (redex-match? abort-lang l "j") #t)
- ;; XXX This makes no sense, given the definition on line 495
- (test-equal (judgment-holds (tc · · (MG ,ctc ,v "k" "l" "j") (Mark Num))) #t))
+(define small-counter-example
+  '(ccm 
+    (monitor 
+     (mark/c 
+      (mark/c (flat (λ (p : Num) #t)) 
+              Num)
+      (Mark Num)) 
+     (make-cm-key (Mark Num))
+     "" "" "") 
+    (Mark Num)))
+
 (test-equal (check small-counter-example) #f)
+

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-2.rkt

@@ -932,7 +932,8 @@
 
 (define (check term)
   (or (not term)
-      (soundness-holds? term)))
+      (implies (type-check term)
+               (soundness-holds? term))))
 
 (define (type-check e)
   (judgment-holds (tc · · ,e t)))
@@ -949,3 +950,9 @@
       (set! index (add1 index))
       (generate-term abort-lang e #:i-th index))))
 
+(define small-counter-example
+  '(monitor (list/c (flat (λ (k : Bool) #t))) 
+            (cons #t (null Bool)) 
+            "" "" ""))
+
+(test-equal (check small-counter-example) #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-3.rkt

@@ -932,7 +932,8 @@
 
 (define (check term)
   (or (not term)
-      (soundness-holds? term)))
+      (implies (type-check term)
+               (soundness-holds? term))))
 
 (define (type-check e)
   (judgment-holds (tc · · ,e t)))

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/delim-cont/delim-cont-base.rkt

@@ -931,7 +931,8 @@
 
 (define (check term)
   (or (not term)
-      (soundness-holds? term)))
+      (implies (type-check term)
+               (soundness-holds? term))))
 
 (define (type-check e)
   (judgment-holds (tc · · ,e t)))