adjust let-poly check functions so they count exns as failure,

but only for the bugs that are expected to show up that way

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff

@@ -10,9 +10,33 @@
 >    (τ (eliminate-τ x τ σ) (eliminate-G x τ G))]
 >   [(eliminate-G x τ (y σ G))
 >    (y (eliminate-τ x τ σ) (eliminate-G x τ G))])
-571a574,578
+560,571c562,577
+<       (let ([t-type (type-check M)])
+<         (implies
+<          t-type
+<          (let loop ([Σ+M `(· ,M)])
+<            (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
+<            (and (consistent-with? t-type new-type)
+<                 (or (v? (list-ref Σ+M 1))
+<                     (let ([red-res (apply-reduction-relation red Σ+M)])
+<                       (and (= (length red-res) 1)
+<                            (let ([red-t (car red-res)])
+<                              (or (equal? red-t "error")
+<                                  (loop red-t))))))))))))
+---
+>       (with-handlers ([exn:fail? (λ (x) #f)])
+>         (let ([t-type (type-check M)])
+>           (implies
+>            t-type
+>            (let loop ([Σ+M `(· ,M)])
+>              (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
+>              (and (consistent-with? t-type new-type)
+>                   (or (v? (list-ref Σ+M 1))
+>                       (let ([red-res (apply-reduction-relation red Σ+M)])
+>                         (and (= (length red-res) 1)
+>                              (let ([red-t (car red-res)])
+>                                (or (equal? red-t "error")
+>                                    (loop red-t)))))))))))))
 > 
 > (define small-counter-example (term (cons 1)))
-> (test-equal (with-handlers ([exn:fail? (λ (x) #f)])
+> (test-equal (check small-counter-example) #f)
->               (check small-counter-example))
->             #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff

@@ -6,9 +6,33 @@
 <   [(∨ boolean_1 boolean_2) #t])
 ---
 >   [(∨ boolean boolean) #t])
-571a572,576
+560,571c560,575
+<       (let ([t-type (type-check M)])
+<         (implies
+<          t-type
+<          (let loop ([Σ+M `(· ,M)])
+<            (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
+<            (and (consistent-with? t-type new-type)
+<                 (or (v? (list-ref Σ+M 1))
+<                     (let ([red-res (apply-reduction-relation red Σ+M)])
+<                       (and (= (length red-res) 1)
+<                            (let ([red-t (car red-res)])
+<                              (or (equal? red-t "error")
+<                                  (loop red-t))))))))))))
+---
+>       (with-handlers ([exn:fail? (λ (x) #f)])
+>         (let ([t-type (type-check M)])
+>           (implies
+>            t-type
+>            (let loop ([Σ+M `(· ,M)])
+>              (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
+>              (and (consistent-with? t-type new-type)
+>                   (or (v? (list-ref Σ+M 1))
+>                       (let ([red-res (apply-reduction-relation red Σ+M)])
+>                         (and (= (length red-res) 1)
+>                              (let ([red-t (car red-res)])
+>                                (or (equal? red-t "error")
+>                                    (loop red-t)))))))))))))
 > 
 > (define small-counter-example (term ((λ x x) 1)))
-> (test-equal (with-handlers ([exn:fail? (λ (x) #f)])
+> (test-equal (check small-counter-example) #f)
->                (check small-counter-example))
->             #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt

@@ -559,6 +559,7 @@ from the given term.
 
 (define (check M)
   (or (not M)
+      (with-handlers ([exn:fail? (λ (x) #f)])
         (let ([t-type (type-check M)])
           (implies
            t-type
@@ -570,9 +571,7 @@ from the given term.
                         (and (= (length red-res) 1)
                              (let ([red-t (car red-res)])
                                (or (equal? red-t "error")
-                                 (loop red-t))))))))))))
+                                   (loop red-t)))))))))))))
 
 (define small-counter-example (term (cons 1)))
-(test-equal (with-handlers ([exn:fail? (λ (x) #f)])
+(test-equal (check small-counter-example) #f)
-              (check small-counter-example))
-            #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt

@@ -557,6 +557,7 @@ from the given term.
 
 (define (check M)
   (or (not M)
+      (with-handlers ([exn:fail? (λ (x) #f)])
         (let ([t-type (type-check M)])
           (implies
            t-type
@@ -568,9 +569,7 @@ from the given term.
                         (and (= (length red-res) 1)
                              (let ([red-t (car red-res)])
                                (or (equal? red-t "error")
-                                 (loop red-t))))))))))))
+                                   (loop red-t)))))))))))))
 
 (define small-counter-example (term ((λ x x) 1)))
-(test-equal (with-handlers ([exn:fail? (λ (x) #f)])
+(test-equal (check small-counter-example) #f)
-               (check small-counter-example))
-            #f)