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

adjust check function for poly-stlc and put Jay's counter

Browse Source 
example for bug #2 into the file
This commit is contained in:
Robby Findler 2014-03-19 11:41:06 -05:00
parent 3d175cba40
commit bc9729358a
11 changed files with 147 additions and 140 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/2.diff
View File

@ -9,3 +9,7 @@
< [#f #f]))
---
> M]))
294a293,295
> (define small-counter-example (term (([cons @ int] 1) [nil @ int])))
> (test-equal (check small-counter-example) #f)
>

28
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-1.rkt
View File

@ -2,7 +2,7 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/bool
racket/match
racket/contract
"tut-subst.rkt")
@ -210,13 +210,13 @@
[(subst M x N)
,(subst/proc x? (term (x)) (term (N)) (term M))])
(define v? (redex-match poly-stlc v))
(define τ? (redex-match poly-stlc τ))
(define v? (redex-match? poly-stlc v))
(define τ? (redex-match? poly-stlc τ))
(define/contract (type-check M)
(-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(cond
[(empty? M-t)
[(null? M-t)
#f]
[(null? (cdr M-t))
(car M-t)]
@ -268,19 +268,19 @@
M]
[#f #f]))))
;; check : (or/c #f M[from poly-stlc language]) -> 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 poly-stlc M #:i-th (pick-an-index 0.065)))

31
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-2.rkt
View File

@ -2,7 +2,7 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/bool
racket/match
racket/contract
"tut-subst.rkt")
@ -209,13 +209,13 @@
[(subst M x N)
,(subst/proc x? (term (x)) (term (N)) (term M))])
(define v? (redex-match poly-stlc v))
(define τ? (redex-match poly-stlc τ))
(define v? (redex-match? poly-stlc v))
(define τ? (redex-match? poly-stlc τ))
(define/contract (type-check M)
(-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(cond
[(empty? M-t)
[(null? M-t)
#f]
[(null? (cdr M-t))
(car M-t)]
@ -266,19 +266,19 @@
M]
[#f #f]))))
;; check : (or/c #f M[from poly-stlc language]) -> 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 poly-stlc M #:i-th (pick-an-index 0.065)))
@ -290,6 +290,9 @@
(generate-term poly-stlc M #:i-th index)
(set! index (add1 index))))))
(define small-counter-example (term (([cons @ int] 1) [nil @ int])))
(test-equal (check small-counter-example) #f)
(define fixed
(term
(;; 2

28
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-3.rkt
View File

@ -2,7 +2,7 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/bool
racket/match
racket/contract
"tut-subst.rkt")
@ -210,13 +210,13 @@
[(subst M x N)
,(subst/proc x? (term (x)) (term (N)) (term M))])
(define v? (redex-match poly-stlc v))
(define τ? (redex-match poly-stlc τ))
(define v? (redex-match? poly-stlc v))
(define τ? (redex-match? poly-stlc τ))
(define/contract (type-check M)
(-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(cond
[(empty? M-t)
[(null? M-t)
#f]
[(null? (cdr M-t))
(car M-t)]
@ -268,19 +268,19 @@
M]
[#f #f]))))
;; check : (or/c #f M[from poly-stlc language]) -> 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 poly-stlc M #:i-th (pick-an-index 0.065)))

28
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-4.rkt
View File

@ -2,7 +2,7 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/bool
racket/match
racket/contract
"tut-subst.rkt")
@ -210,13 +210,13 @@
[(subst M x N)
,(subst/proc x? (term (x)) (term (N)) (term M))])
(define v? (redex-match poly-stlc v))
(define τ? (redex-match poly-stlc τ))
(define v? (redex-match? poly-stlc v))
(define τ? (redex-match? poly-stlc τ))
(define/contract (type-check M)
(-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(cond
[(empty? M-t)
[(null? M-t)
#f]
[(null? (cdr M-t))
(car M-t)]
@ -268,19 +268,19 @@
M]
[#f #f]))))
;; check : (or/c #f M[from poly-stlc language]) -> 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 poly-stlc M #:i-th (pick-an-index 0.065)))

28
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-5.rkt
View File

@ -2,7 +2,7 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/bool
racket/match
racket/contract
"tut-subst.rkt")
@ -210,13 +210,13 @@
[(subst M x N)
,(subst/proc x? (term (x)) (term (N)) (term M))])
(define v? (redex-match poly-stlc v))
(define τ? (redex-match poly-stlc τ))
(define v? (redex-match? poly-stlc v))
(define τ? (redex-match? poly-stlc τ))
(define/contract (type-check M)
(-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(cond
[(empty? M-t)
[(null? M-t)
#f]
[(null? (cdr M-t))
(car M-t)]
@ -268,19 +268,19 @@
M]
[#f #f]))))
;; check : (or/c #f M[from poly-stlc language]) -> 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 poly-stlc M #:i-th (pick-an-index 0.065)))

28
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-6.rkt
View File

@ -2,7 +2,7 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/bool
racket/match
racket/contract
"tut-subst.rkt")
@ -210,13 +210,13 @@
[(subst M x N)
,(subst/proc x? (term (x)) (term (N)) (term M))])
(define v? (redex-match poly-stlc v))
(define τ? (redex-match poly-stlc τ))
(define v? (redex-match? poly-stlc v))
(define τ? (redex-match? poly-stlc τ))
(define/contract (type-check M)
(-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(cond
[(empty? M-t)
[(null? M-t)
#f]
[(null? (cdr M-t))
(car M-t)]
@ -268,19 +268,19 @@
M]
[#f #f]))))
;; check : (or/c #f M[from poly-stlc language]) -> 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 poly-stlc M #:i-th (pick-an-index 0.065)))

28
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-7.rkt
View File

@ -2,7 +2,7 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/bool
racket/match
racket/contract
"tut-subst.rkt")
@ -209,13 +209,13 @@
[(subst M x N)
,(subst/proc x? (term (x)) (term (N)) (term M))])
(define v? (redex-match poly-stlc v))
(define τ? (redex-match poly-stlc τ))
(define v? (redex-match? poly-stlc v))
(define τ? (redex-match? poly-stlc τ))
(define/contract (type-check M)
(-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(cond
[(empty? M-t)
[(null? M-t)
#f]
[(null? (cdr M-t))
(car M-t)]
@ -267,19 +267,19 @@
M]
[#f #f]))))
;; check : (or/c #f M[from poly-stlc language]) -> 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 poly-stlc M #:i-th (pick-an-index 0.065)))

28
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-8.rkt
View File

@ -2,7 +2,7 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/bool
racket/match
racket/contract
"tut-subst.rkt")
@ -210,13 +210,13 @@
[(subst M x N)
,(subst/proc x? (term (x)) (term (N)) (term M))])
(define v? (redex-match poly-stlc v))
(define τ? (redex-match poly-stlc τ))
(define v? (redex-match? poly-stlc v))
(define τ? (redex-match? poly-stlc τ))
(define/contract (type-check M)
(-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(cond
[(empty? M-t)
[(null? M-t)
#f]
[(null? (cdr M-t))
(car M-t)]
@ -268,19 +268,19 @@
M]
[#f #f]))))
;; check : (or/c #f M[from poly-stlc language]) -> 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 poly-stlc M #:i-th (pick-an-index 0.065)))

28
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-9.rkt
View File

@ -2,7 +2,7 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/bool
racket/match
racket/contract
"tut-subst.rkt")
@ -210,13 +210,13 @@
[(subst M x N)
,(subst/proc x? (term (x)) (term (N)) (term M))])
(define v? (redex-match poly-stlc v))
(define τ? (redex-match poly-stlc τ))
(define v? (redex-match? poly-stlc v))
(define τ? (redex-match? poly-stlc τ))
(define/contract (type-check M)
(-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(cond
[(empty? M-t)
[(null? M-t)
#f]
[(null? (cdr M-t))
(car M-t)]
@ -268,19 +268,19 @@
M]
[#f #f]))))
;; check : (or/c #f M[from poly-stlc language]) -> 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 poly-stlc M #:i-th (pick-an-index 0.065)))

28
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/poly-stlc/poly-stlc-base.rkt
View File

@ -2,7 +2,7 @@
(require redex/reduction-semantics
(only-in redex/private/generate-term pick-an-index)
racket/list
racket/bool
racket/match
racket/contract
"tut-subst.rkt")
@ -210,13 +210,13 @@
[(subst M x N)
,(subst/proc x? (term (x)) (term (N)) (term M))])
(define v? (redex-match poly-stlc v))
(define τ? (redex-match poly-stlc τ))
(define v? (redex-match? poly-stlc v))
(define τ? (redex-match? poly-stlc τ))
(define/contract (type-check M)
(-> M? (or/c τ? #f))
(define M-t (judgment-holds (typeof • ,M τ) τ))
(cond
[(empty? M-t)
[(null? M-t)
#f]
[(null? (cdr M-t))
(car M-t)]
@ -268,19 +268,19 @@
M]
[#f #f]))))
;; check : (or/c #f M[from poly-stlc language]) -> 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 poly-stlc M #:i-th (pick-an-index 0.065)))