From 1ecd4c0563baa86d501b94e12087739f7fc19fa9 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Tue, 18 Mar 2014 21:30:10 -0500 Subject: [PATCH] change stlc-sub's 'check' function to not assume its input is well-typed --- .../benchmark/stlc-sub/stlc-sub-1.rkt | 26 +++++++++---------- .../benchmark/stlc-sub/stlc-sub-2.rkt | 26 +++++++++---------- .../benchmark/stlc-sub/stlc-sub-3.rkt | 26 +++++++++---------- .../benchmark/stlc-sub/stlc-sub-4.rkt | 26 +++++++++---------- .../benchmark/stlc-sub/stlc-sub-5.rkt | 26 +++++++++---------- .../benchmark/stlc-sub/stlc-sub-6.rkt | 26 +++++++++---------- .../benchmark/stlc-sub/stlc-sub-7.rkt | 26 +++++++++---------- .../benchmark/stlc-sub/stlc-sub-8.rkt | 26 +++++++++---------- .../benchmark/stlc-sub/stlc-sub-9.rkt | 26 +++++++++---------- .../benchmark/stlc-sub/stlc-sub-base.rkt | 26 +++++++++---------- 10 files changed, 130 insertions(+), 130 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 f49511fa3b..3a892787d4 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 @@ -5,7 +5,7 @@ racket/list racket/match racket/contract - math/base) + racket/bool) (provide (all-defined-out)) (define the-error "the order of the variable clauses is swapped") @@ -147,8 +147,8 @@ (define x? (redex-match stlc x)) -(define v? (redex-match stlc v)) -(define τ? (redex-match stlc τ)) +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) (define/contract (type-check M) (-> M? (or/c τ? #f)) (define M-t (judgment-holds (typeof • ,M τ) τ)) @@ -269,19 +269,19 @@ M] [#f #f])))) +;; check : (or/c #f term) -> boolean[#f = counterexample found!] (define (check term) (or (not term) (v? term) - (let ([red-res (apply-reduction-relation red term)] - [t-type (type-check term)]) - ;; xxx should this also be t-type IMPLIES? - (and - (= (length red-res) 1) - (let ([red-t (car red-res)]) - (or - (equal? red-t "error") - (let ([red-type (type-check red-t)]) - (equal? t-type red-type)))))))) + (let ([t-type (type-check term)]) + (implies + t-type + (let ([red-res (apply-reduction-relation red term)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (let ([red-type (type-check red-t)]) + (equal? t-type red-type)))))))))) (define (generate-enum-term) (generate-term stlc M #:i-th (pick-an-index 0.0001))) 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 32004c7e59..1541ffc2ae 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 @@ -7,7 +7,7 @@ racket/match racket/list racket/contract - math/base) + racket/bool) (provide (all-defined-out)) @@ -147,8 +147,8 @@ (define x? (redex-match stlc x)) -(define v? (redex-match stlc v)) -(define τ? (redex-match stlc τ)) +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) (define/contract (type-check M) (-> M? (or/c τ? #f)) (define M-t (judgment-holds (typeof • ,M τ) τ)) @@ -268,19 +268,19 @@ M] [#f #f])))) +;; check : (or/c #f term) -> boolean[#f = counterexample found!] (define (check term) (or (not term) (v? term) - (let ([red-res (apply-reduction-relation red term)] - [t-type (type-check term)]) - ;; xxx should this also be t-type IMPLIES? - (and - (= (length red-res) 1) - (let ([red-t (car red-res)]) - (or - (equal? red-t "error") - (let ([red-type (type-check red-t)]) - (equal? t-type red-type)))))))) + (let ([t-type (type-check term)]) + (implies + t-type + (let ([red-res (apply-reduction-relation red term)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (let ([red-type (type-check red-t)]) + (equal? t-type red-type)))))))))) (define (generate-enum-term) (generate-term stlc M #:i-th (pick-an-index 0.0001))) 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 4d95f8ef0c..8e64003d7c 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 @@ -5,7 +5,7 @@ racket/list racket/match racket/contract - math/base) + racket/bool) (provide (all-defined-out)) (define the-error "substitutes rator into rand in application") @@ -147,8 +147,8 @@ (define x? (redex-match stlc x)) -(define v? (redex-match stlc v)) -(define τ? (redex-match stlc τ)) +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) (define/contract (type-check M) (-> M? (or/c τ? #f)) (define M-t (judgment-holds (typeof • ,M τ) τ)) @@ -269,19 +269,19 @@ M] [#f #f])))) +;; check : (or/c #f term) -> boolean[#f = counterexample found!] (define (check term) (or (not term) (v? term) - (let ([red-res (apply-reduction-relation red term)] - [t-type (type-check term)]) - ;; xxx should this also be t-type IMPLIES? - (and - (= (length red-res) 1) - (let ([red-t (car red-res)]) - (or - (equal? red-t "error") - (let ([red-type (type-check red-t)]) - (equal? t-type red-type)))))))) + (let ([t-type (type-check term)]) + (implies + t-type + (let ([red-res (apply-reduction-relation red term)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (let ([red-type (type-check red-t)]) + (equal? t-type red-type)))))))))) (define (generate-enum-term) (generate-term stlc M #:i-th (pick-an-index 0.0001))) 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 7204247101..62017f9703 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 @@ -7,7 +7,7 @@ racket/match racket/list racket/contract - math/base) + racket/bool) (provide (all-defined-out)) @@ -147,8 +147,8 @@ (define x? (redex-match stlc x)) -(define v? (redex-match stlc v)) -(define τ? (redex-match stlc τ)) +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) (define/contract (type-check M) (-> M? (or/c τ? #f)) (define M-t (judgment-holds (typeof • ,M τ) τ)) @@ -268,19 +268,19 @@ M] [#f #f])))) +;; check : (or/c #f term) -> boolean[#f = counterexample found!] (define (check term) (or (not term) (v? term) - (let ([red-res (apply-reduction-relation red term)] - [t-type (type-check term)]) - ;; xxx should this also be t-type IMPLIES? - (and - (= (length red-res) 1) - (let ([red-t (car red-res)]) - (or - (equal? red-t "error") - (let ([red-type (type-check red-t)]) - (equal? t-type red-type)))))))) + (let ([t-type (type-check term)]) + (implies + t-type + (let ([red-res (apply-reduction-relation red term)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (let ([red-type (type-check red-t)]) + (equal? t-type red-type)))))))))) (define (generate-enum-term) (generate-term stlc M #:i-th (pick-an-index 0.0001))) 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 4c470ad20d..e814e54c6f 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 @@ -7,7 +7,7 @@ racket/match racket/list racket/contract - math/base) + racket/bool) (provide (all-defined-out)) @@ -145,8 +145,8 @@ (define x? (redex-match stlc x)) -(define v? (redex-match stlc v)) -(define τ? (redex-match stlc τ)) +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) (define/contract (type-check M) (-> M? (or/c τ? #f)) (define M-t (judgment-holds (typeof • ,M τ) τ)) @@ -266,19 +266,19 @@ M] [#f #f])))) +;; check : (or/c #f term) -> boolean[#f = counterexample found!] (define (check term) (or (not term) (v? term) - (let ([red-res (apply-reduction-relation red term)] - [t-type (type-check term)]) - ;; xxx should this also be t-type IMPLIES? - (and - (= (length red-res) 1) - (let ([red-t (car red-res)]) - (or - (equal? red-t "error") - (let ([red-type (type-check red-t)]) - (equal? t-type red-type)))))))) + (let ([t-type (type-check term)]) + (implies + t-type + (let ([red-res (apply-reduction-relation red term)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (let ([red-type (type-check red-t)]) + (equal? t-type red-type)))))))))) (define (generate-enum-term) (generate-term stlc M #:i-th (pick-an-index 0.0001))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt index 13267d7b16..6689433302 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt @@ -7,7 +7,7 @@ racket/match racket/list racket/contract - math/base) + racket/bool) (provide (all-defined-out)) @@ -147,8 +147,8 @@ (define x? (redex-match stlc x)) -(define v? (redex-match stlc v)) -(define τ? (redex-match stlc τ)) +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) (define/contract (type-check M) (-> M? (or/c τ? #f)) (define M-t (judgment-holds (typeof • ,M τ) τ)) @@ -268,19 +268,19 @@ M] [#f #f])))) +;; check : (or/c #f term) -> boolean[#f = counterexample found!] (define (check term) (or (not term) (v? term) - (let ([red-res (apply-reduction-relation red term)] - [t-type (type-check term)]) - ;; xxx should this also be t-type IMPLIES? - (and - (= (length red-res) 1) - (let ([red-t (car red-res)]) - (or - (equal? red-t "error") - (let ([red-type (type-check red-t)]) - (equal? t-type red-type)))))))) + (let ([t-type (type-check term)]) + (implies + t-type + (let ([red-res (apply-reduction-relation red term)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (let ([red-type (type-check red-t)]) + (equal? t-type red-type)))))))))) (define (generate-enum-term) (generate-term stlc M #:i-th (pick-an-index 0.0001))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt index 272585f00c..b917b75b3c 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt @@ -5,7 +5,7 @@ racket/list racket/match racket/contract - math/base) + racket/bool) (provide (all-defined-out)) (define the-error "swaps to/from expressions when recurring inside a constant") @@ -147,8 +147,8 @@ (define x? (redex-match stlc x)) -(define v? (redex-match stlc v)) -(define τ? (redex-match stlc τ)) +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) (define/contract (type-check M) (-> M? (or/c τ? #f)) (define M-t (judgment-holds (typeof • ,M τ) τ)) @@ -269,19 +269,19 @@ M] [#f #f])))) +;; check : (or/c #f term) -> boolean[#f = counterexample found!] (define (check term) (or (not term) (v? term) - (let ([red-res (apply-reduction-relation red term)] - [t-type (type-check term)]) - ;; xxx should this also be t-type IMPLIES? - (and - (= (length red-res) 1) - (let ([red-t (car red-res)]) - (or - (equal? red-t "error") - (let ([red-type (type-check red-t)]) - (equal? t-type red-type)))))))) + (let ([t-type (type-check term)]) + (implies + t-type + (let ([red-res (apply-reduction-relation red term)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (let ([red-type (type-check red-t)]) + (equal? t-type red-type)))))))))) (define (generate-enum-term) (generate-term stlc M #:i-th (pick-an-index 0.0001))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt index 85cb936fb4..4ed5aeab63 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt @@ -7,7 +7,7 @@ racket/match racket/list racket/contract - math/base) + racket/bool) (provide (all-defined-out)) @@ -147,8 +147,8 @@ (define x? (redex-match stlc x)) -(define v? (redex-match stlc v)) -(define τ? (redex-match stlc τ)) +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) (define/contract (type-check M) (-> M? (or/c τ? #f)) (define M-t (judgment-holds (typeof • ,M τ) τ)) @@ -268,19 +268,19 @@ M] [#f #f])))) +;; check : (or/c #f term) -> boolean[#f = counterexample found!] (define (check term) (or (not term) (v? term) - (let ([red-res (apply-reduction-relation red term)] - [t-type (type-check term)]) - ;; xxx should this also be t-type IMPLIES? - (and - (= (length red-res) 1) - (let ([red-t (car red-res)]) - (or - (equal? red-t "error") - (let ([red-type (type-check red-t)]) - (equal? t-type red-type)))))))) + (let ([t-type (type-check term)]) + (implies + t-type + (let ([red-res (apply-reduction-relation red term)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (let ([red-type (type-check red-t)]) + (equal? t-type red-type)))))))))) (define (generate-enum-term) (generate-term stlc M #:i-th (pick-an-index 0.0001))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt index 1d62818511..a1ad155e0b 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt @@ -7,7 +7,7 @@ racket/match racket/list racket/contract - math/base) + racket/bool) (provide (all-defined-out)) @@ -147,8 +147,8 @@ (define x? (redex-match stlc x)) -(define v? (redex-match stlc v)) -(define τ? (redex-match stlc τ)) +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) (define/contract (type-check M) (-> M? (or/c τ? #f)) (define M-t (judgment-holds (typeof • ,M τ) τ)) @@ -268,19 +268,19 @@ M] [#f #f])))) +;; check : (or/c #f term) -> boolean[#f = counterexample found!] (define (check term) (or (not term) (v? term) - (let ([red-res (apply-reduction-relation red term)] - [t-type (type-check term)]) - ;; xxx should this also be t-type IMPLIES? - (and - (= (length red-res) 1) - (let ([red-t (car red-res)]) - (or - (equal? red-t "error") - (let ([red-type (type-check red-t)]) - (equal? t-type red-type)))))))) + (let ([t-type (type-check term)]) + (implies + t-type + (let ([red-res (apply-reduction-relation red term)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (let ([red-type (type-check red-t)]) + (equal? t-type red-type)))))))))) (define (generate-enum-term) (generate-term stlc M #:i-th (pick-an-index 0.0001))) 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 b7a80aa555..9ba980cc3d 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 @@ -7,7 +7,7 @@ racket/match racket/list racket/contract - math/base) + racket/bool) (provide (all-defined-out)) @@ -147,8 +147,8 @@ (define x? (redex-match stlc x)) -(define v? (redex-match stlc v)) -(define τ? (redex-match stlc τ)) +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) (define/contract (type-check M) (-> M? (or/c τ? #f)) (define M-t (judgment-holds (typeof • ,M τ) τ)) @@ -268,19 +268,19 @@ M] [#f #f])))) +;; check : (or/c #f term) -> boolean[#f = counterexample found!] (define (check term) (or (not term) (v? term) - (let ([red-res (apply-reduction-relation red term)] - [t-type (type-check term)]) - ;; xxx should this also be t-type IMPLIES? - (and - (= (length red-res) 1) - (let ([red-t (car red-res)]) - (or - (equal? red-t "error") - (let ([red-type (type-check red-t)]) - (equal? t-type red-type)))))))) + (let ([t-type (type-check term)]) + (implies + t-type + (let ([red-res (apply-reduction-relation red term)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (let ([red-type (type-check red-t)]) + (equal? t-type red-type)))))))))) (define (generate-enum-term) (generate-term stlc M #:i-th (pick-an-index 0.0001)))