suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

change stlc-sub's 'check' function to not assume

Browse Source 
its input is well-typed
This commit is contained in:
Robby Findler 2014-03-18 21:30:10 -05:00
parent dea6e7c6e9
commit 1ecd4c0563
10 changed files with 130 additions and 130 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-1.rkt
View File

@ -5,7 +5,7 @@
racket/list racket/list
racket/match racket/match
racket/contract racket/contract
math/base) racket/bool)
(provide (all-defined-out)) (provide (all-defined-out))
(define the-error "the order of the variable clauses is swapped") (define the-error "the order of the variable clauses is swapped")
@ -147,8 +147,8 @@
(define x? (redex-match stlc x)) (define x? (redex-match stlc x))
(define v? (redex-match stlc v)) (define v? (redex-match? stlc v))
(define τ? (redex-match stlc τ)) (define τ? (redex-match? stlc τ))
(define/contract (type-check M) (define/contract (type-check M)
(-> M? (or/c τ? #f)) (-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ)) (define M-t (judgment-holds (typeof • ,M τ) τ))
@ -269,19 +269,19 @@
M] M]
[#f #f])))) [#f #f]))))
;; check : (or/c #f term) -> boolean[#f = counterexample found!]
(define (check term) (define (check term)
(or (not term) (or (not term)
(v? term) (v? term)
(let ([red-res (apply-reduction-relation red term)] (let ([t-type (type-check term)])
[t-type (type-check term)]) (implies
;; xxx should this also be t-type IMPLIES? t-type
(and (let ([red-res (apply-reduction-relation red term)])
(= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (or (equal? red-t "error")
(equal? red-t "error") (let ([red-type (type-check red-t)])
(let ([red-type (type-check red-t)]) (equal? t-type red-type))))))))))
(equal? t-type red-type))))))))
(define (generate-enum-term) (define (generate-enum-term)
(generate-term stlc M #:i-th (pick-an-index 0.0001))) (generate-term stlc M #:i-th (pick-an-index 0.0001)))

26
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-2.rkt
View File

@ -7,7 +7,7 @@
racket/match racket/match
racket/list racket/list
racket/contract racket/contract
math/base) racket/bool)
(provide (all-defined-out)) (provide (all-defined-out))
@ -147,8 +147,8 @@
(define x? (redex-match stlc x)) (define x? (redex-match stlc x))
(define v? (redex-match stlc v)) (define v? (redex-match? stlc v))
(define τ? (redex-match stlc τ)) (define τ? (redex-match? stlc τ))
(define/contract (type-check M) (define/contract (type-check M)
(-> M? (or/c τ? #f)) (-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ)) (define M-t (judgment-holds (typeof • ,M τ) τ))
@ -268,19 +268,19 @@
M] M]
[#f #f])))) [#f #f]))))
;; check : (or/c #f term) -> boolean[#f = counterexample found!]
(define (check term) (define (check term)
(or (not term) (or (not term)
(v? term) (v? term)
(let ([red-res (apply-reduction-relation red term)] (let ([t-type (type-check term)])
[t-type (type-check term)]) (implies
;; xxx should this also be t-type IMPLIES? t-type
(and (let ([red-res (apply-reduction-relation red term)])
(= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (or (equal? red-t "error")
(equal? red-t "error") (let ([red-type (type-check red-t)])
(let ([red-type (type-check red-t)]) (equal? t-type red-type))))))))))
(equal? t-type red-type))))))))
(define (generate-enum-term) (define (generate-enum-term)
(generate-term stlc M #:i-th (pick-an-index 0.0001))) (generate-term stlc M #:i-th (pick-an-index 0.0001)))

26
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-3.rkt
View File

@ -5,7 +5,7 @@
racket/list racket/list
racket/match racket/match
racket/contract racket/contract
math/base) racket/bool)
(provide (all-defined-out)) (provide (all-defined-out))
(define the-error "substitutes rator into rand in application") (define the-error "substitutes rator into rand in application")
@ -147,8 +147,8 @@
(define x? (redex-match stlc x)) (define x? (redex-match stlc x))
(define v? (redex-match stlc v)) (define v? (redex-match? stlc v))
(define τ? (redex-match stlc τ)) (define τ? (redex-match? stlc τ))
(define/contract (type-check M) (define/contract (type-check M)
(-> M? (or/c τ? #f)) (-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ)) (define M-t (judgment-holds (typeof • ,M τ) τ))
@ -269,19 +269,19 @@
M] M]
[#f #f])))) [#f #f]))))
;; check : (or/c #f term) -> boolean[#f = counterexample found!]
(define (check term) (define (check term)
(or (not term) (or (not term)
(v? term) (v? term)
(let ([red-res (apply-reduction-relation red term)] (let ([t-type (type-check term)])
[t-type (type-check term)]) (implies
;; xxx should this also be t-type IMPLIES? t-type
(and (let ([red-res (apply-reduction-relation red term)])
(= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (or (equal? red-t "error")
(equal? red-t "error") (let ([red-type (type-check red-t)])
(let ([red-type (type-check red-t)]) (equal? t-type red-type))))))))))
(equal? t-type red-type))))))))
(define (generate-enum-term) (define (generate-enum-term)
(generate-term stlc M #:i-th (pick-an-index 0.0001))) (generate-term stlc M #:i-th (pick-an-index 0.0001)))

26
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-4.rkt
View File

@ -7,7 +7,7 @@
racket/match racket/match
racket/list racket/list
racket/contract racket/contract
math/base) racket/bool)
(provide (all-defined-out)) (provide (all-defined-out))
@ -147,8 +147,8 @@
(define x? (redex-match stlc x)) (define x? (redex-match stlc x))
(define v? (redex-match stlc v)) (define v? (redex-match? stlc v))
(define τ? (redex-match stlc τ)) (define τ? (redex-match? stlc τ))
(define/contract (type-check M) (define/contract (type-check M)
(-> M? (or/c τ? #f)) (-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ)) (define M-t (judgment-holds (typeof • ,M τ) τ))
@ -268,19 +268,19 @@
M] M]
[#f #f])))) [#f #f]))))
;; check : (or/c #f term) -> boolean[#f = counterexample found!]
(define (check term) (define (check term)
(or (not term) (or (not term)
(v? term) (v? term)
(let ([red-res (apply-reduction-relation red term)] (let ([t-type (type-check term)])
[t-type (type-check term)]) (implies
;; xxx should this also be t-type IMPLIES? t-type
(and (let ([red-res (apply-reduction-relation red term)])
(= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (or (equal? red-t "error")
(equal? red-t "error") (let ([red-type (type-check red-t)])
(let ([red-type (type-check red-t)]) (equal? t-type red-type))))))))))
(equal? t-type red-type))))))))
(define (generate-enum-term) (define (generate-enum-term)
(generate-term stlc M #:i-th (pick-an-index 0.0001))) (generate-term stlc M #:i-th (pick-an-index 0.0001)))

26
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-5.rkt
View File

@ -7,7 +7,7 @@
racket/match racket/match
racket/list racket/list
racket/contract racket/contract
math/base) racket/bool)
(provide (all-defined-out)) (provide (all-defined-out))
@ -145,8 +145,8 @@
(define x? (redex-match stlc x)) (define x? (redex-match stlc x))
(define v? (redex-match stlc v)) (define v? (redex-match? stlc v))
(define τ? (redex-match stlc τ)) (define τ? (redex-match? stlc τ))
(define/contract (type-check M) (define/contract (type-check M)
(-> M? (or/c τ? #f)) (-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ)) (define M-t (judgment-holds (typeof • ,M τ) τ))
@ -266,19 +266,19 @@
M] M]
[#f #f])))) [#f #f]))))
;; check : (or/c #f term) -> boolean[#f = counterexample found!]
(define (check term) (define (check term)
(or (not term) (or (not term)
(v? term) (v? term)
(let ([red-res (apply-reduction-relation red term)] (let ([t-type (type-check term)])
[t-type (type-check term)]) (implies
;; xxx should this also be t-type IMPLIES? t-type
(and (let ([red-res (apply-reduction-relation red term)])
(= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (or (equal? red-t "error")
(equal? red-t "error") (let ([red-type (type-check red-t)])
(let ([red-type (type-check red-t)]) (equal? t-type red-type))))))))))
(equal? t-type red-type))))))))
(define (generate-enum-term) (define (generate-enum-term)
(generate-term stlc M #:i-th (pick-an-index 0.0001))) (generate-term stlc M #:i-th (pick-an-index 0.0001)))

26
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-6.rkt
View File

@ -7,7 +7,7 @@
racket/match racket/match
racket/list racket/list
racket/contract racket/contract
math/base) racket/bool)
(provide (all-defined-out)) (provide (all-defined-out))
@ -147,8 +147,8 @@
(define x? (redex-match stlc x)) (define x? (redex-match stlc x))
(define v? (redex-match stlc v)) (define v? (redex-match? stlc v))
(define τ? (redex-match stlc τ)) (define τ? (redex-match? stlc τ))
(define/contract (type-check M) (define/contract (type-check M)
(-> M? (or/c τ? #f)) (-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ)) (define M-t (judgment-holds (typeof • ,M τ) τ))
@ -268,19 +268,19 @@
M] M]
[#f #f])))) [#f #f]))))
;; check : (or/c #f term) -> boolean[#f = counterexample found!]
(define (check term) (define (check term)
(or (not term) (or (not term)
(v? term) (v? term)
(let ([red-res (apply-reduction-relation red term)] (let ([t-type (type-check term)])
[t-type (type-check term)]) (implies
;; xxx should this also be t-type IMPLIES? t-type
(and (let ([red-res (apply-reduction-relation red term)])
(= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (or (equal? red-t "error")
(equal? red-t "error") (let ([red-type (type-check red-t)])
(let ([red-type (type-check red-t)]) (equal? t-type red-type))))))))))
(equal? t-type red-type))))))))
(define (generate-enum-term) (define (generate-enum-term)
(generate-term stlc M #:i-th (pick-an-index 0.0001))) (generate-term stlc M #:i-th (pick-an-index 0.0001)))

26
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-7.rkt
View File

@ -5,7 +5,7 @@
racket/list racket/list
racket/match racket/match
racket/contract racket/contract
math/base) racket/bool)
(provide (all-defined-out)) (provide (all-defined-out))
(define the-error "swaps to/from expressions when recurring inside a constant") (define the-error "swaps to/from expressions when recurring inside a constant")
@ -147,8 +147,8 @@
(define x? (redex-match stlc x)) (define x? (redex-match stlc x))
(define v? (redex-match stlc v)) (define v? (redex-match? stlc v))
(define τ? (redex-match stlc τ)) (define τ? (redex-match? stlc τ))
(define/contract (type-check M) (define/contract (type-check M)
(-> M? (or/c τ? #f)) (-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ)) (define M-t (judgment-holds (typeof • ,M τ) τ))
@ -269,19 +269,19 @@
M] M]
[#f #f])))) [#f #f]))))
;; check : (or/c #f term) -> boolean[#f = counterexample found!]
(define (check term) (define (check term)
(or (not term) (or (not term)
(v? term) (v? term)
(let ([red-res (apply-reduction-relation red term)] (let ([t-type (type-check term)])
[t-type (type-check term)]) (implies
;; xxx should this also be t-type IMPLIES? t-type
(and (let ([red-res (apply-reduction-relation red term)])
(= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (or (equal? red-t "error")
(equal? red-t "error") (let ([red-type (type-check red-t)])
(let ([red-type (type-check red-t)]) (equal? t-type red-type))))))))))
(equal? t-type red-type))))))))
(define (generate-enum-term) (define (generate-enum-term)
(generate-term stlc M #:i-th (pick-an-index 0.0001))) (generate-term stlc M #:i-th (pick-an-index 0.0001)))

26
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-8.rkt
View File

@ -7,7 +7,7 @@
racket/match racket/match
racket/list racket/list
racket/contract racket/contract
math/base) racket/bool)
(provide (all-defined-out)) (provide (all-defined-out))
@ -147,8 +147,8 @@
(define x? (redex-match stlc x)) (define x? (redex-match stlc x))
(define v? (redex-match stlc v)) (define v? (redex-match? stlc v))
(define τ? (redex-match stlc τ)) (define τ? (redex-match? stlc τ))
(define/contract (type-check M) (define/contract (type-check M)
(-> M? (or/c τ? #f)) (-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ)) (define M-t (judgment-holds (typeof • ,M τ) τ))
@ -268,19 +268,19 @@
M] M]
[#f #f])))) [#f #f]))))
;; check : (or/c #f term) -> boolean[#f = counterexample found!]
(define (check term) (define (check term)
(or (not term) (or (not term)
(v? term) (v? term)
(let ([red-res (apply-reduction-relation red term)] (let ([t-type (type-check term)])
[t-type (type-check term)]) (implies
;; xxx should this also be t-type IMPLIES? t-type
(and (let ([red-res (apply-reduction-relation red term)])
(= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (or (equal? red-t "error")
(equal? red-t "error") (let ([red-type (type-check red-t)])
(let ([red-type (type-check red-t)]) (equal? t-type red-type))))))))))
(equal? t-type red-type))))))))
(define (generate-enum-term) (define (generate-enum-term)
(generate-term stlc M #:i-th (pick-an-index 0.0001))) (generate-term stlc M #:i-th (pick-an-index 0.0001)))

26
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-9.rkt
View File

@ -7,7 +7,7 @@
racket/match racket/match
racket/list racket/list
racket/contract racket/contract
math/base) racket/bool)
(provide (all-defined-out)) (provide (all-defined-out))
@ -147,8 +147,8 @@
(define x? (redex-match stlc x)) (define x? (redex-match stlc x))
(define v? (redex-match stlc v)) (define v? (redex-match? stlc v))
(define τ? (redex-match stlc τ)) (define τ? (redex-match? stlc τ))
(define/contract (type-check M) (define/contract (type-check M)
(-> M? (or/c τ? #f)) (-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ)) (define M-t (judgment-holds (typeof • ,M τ) τ))
@ -268,19 +268,19 @@
M] M]
[#f #f])))) [#f #f]))))
;; check : (or/c #f term) -> boolean[#f = counterexample found!]
(define (check term) (define (check term)
(or (not term) (or (not term)
(v? term) (v? term)
(let ([red-res (apply-reduction-relation red term)] (let ([t-type (type-check term)])
[t-type (type-check term)]) (implies
;; xxx should this also be t-type IMPLIES? t-type
(and (let ([red-res (apply-reduction-relation red term)])
(= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (or (equal? red-t "error")
(equal? red-t "error") (let ([red-type (type-check red-t)])
(let ([red-type (type-check red-t)]) (equal? t-type red-type))))))))))
(equal? t-type red-type))))))))
(define (generate-enum-term) (define (generate-enum-term)
(generate-term stlc M #:i-th (pick-an-index 0.0001))) (generate-term stlc M #:i-th (pick-an-index 0.0001)))

26
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc-sub/stlc-sub-base.rkt
View File

@ -7,7 +7,7 @@
racket/match racket/match
racket/list racket/list
racket/contract racket/contract
math/base) racket/bool)
(provide (all-defined-out)) (provide (all-defined-out))
@ -147,8 +147,8 @@
(define x? (redex-match stlc x)) (define x? (redex-match stlc x))
(define v? (redex-match stlc v)) (define v? (redex-match? stlc v))
(define τ? (redex-match stlc τ)) (define τ? (redex-match? stlc τ))
(define/contract (type-check M) (define/contract (type-check M)
(-> M? (or/c τ? #f)) (-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ)) (define M-t (judgment-holds (typeof • ,M τ) τ))
@ -268,19 +268,19 @@
M] M]
[#f #f])))) [#f #f]))))
;; check : (or/c #f term) -> boolean[#f = counterexample found!]
(define (check term) (define (check term)
(or (not term) (or (not term)
(v? term) (v? term)
(let ([red-res (apply-reduction-relation red term)] (let ([t-type (type-check term)])
[t-type (type-check term)]) (implies
;; xxx should this also be t-type IMPLIES? t-type
(and (let ([red-res (apply-reduction-relation red term)])
(= (length red-res) 1) (and (= (length red-res) 1)
(let ([red-t (car red-res)]) (let ([red-t (car red-res)])
(or (or (equal? red-t "error")
(equal? red-t "error") (let ([red-type (type-check red-t)])
(let ([red-type (type-check red-t)]) (equal? t-type red-type))))))))))
(equal? t-type red-type))))))))
(define (generate-enum-term) (define (generate-enum-term)
(generate-term stlc M #:i-th (pick-an-index 0.0001))) (generate-term stlc M #:i-th (pick-an-index 0.0001)))