add stlc-sub with type soundness property
This commit is contained in:
Burke Fetscher
parent
bbec642284
commit
51651d2dc4
|
|
@ -0,0 +1,49 @@
|
|||
3c3
|
||||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "forgot the variable case")
|
||||
106,107d105
|
||||
< [(subst x x M_x)
|
||||
< M_x]
|
||||
272,294c270,281
|
||||
< ;; rewrite all βv redexes already in the term
|
||||
< ;; (but not any new ones that might appear)
|
||||
< (define-metafunction stlc
|
||||
< βv-> : M -> M
|
||||
< [(βv-> ((λ (x τ) M) v)) (subst (βv-> M) x (βv-> v))]
|
||||
< [(βv-> ((λ (x τ) M) y)) (subst (βv-> M) x y)]
|
||||
< [(βv-> (λ (x τ) M)) (λ (x τ) (βv-> M))]
|
||||
< [(βv-> (M N)) ((βv-> M) (βv-> N))]
|
||||
< [(βv-> M) M])
|
||||
<
|
||||
< ;; check : (or/c #f M) -> boolean[#f = counterexample found!]
|
||||
< (define (check M)
|
||||
< (or (not M)
|
||||
< (let ([M-type (type-check M)])
|
||||
< (implies M-type
|
||||
< (let* ([N (term (βv-> ,M))][N-type (type-check N)])
|
||||
< (and (equal? N-type M-type)
|
||||
< (let ([a1 (Eval M)] [a2 (Eval N)])
|
||||
< (and (not (string? a1)) (not (string? a2))
|
||||
< (equal? a1 a2)
|
||||
< (or (equal? a1 'error)
|
||||
< (and (equal? (type-check a1) M-type)
|
||||
< (equal? (type-check a2) M-type)))))))))))
|
||||
---
|
||||
> (define (check term)
|
||||
> (or (not term)
|
||||
> (v? term)
|
||||
> (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))))))))))
|
||||
298a286,289
|
||||
> (define small-counter-example
|
||||
> (term ((λ (x int) x) 1)))
|
||||
> (test-equal (check small-counter-example) #f)
|
||||
>
|
||||
|
|
@ -0,0 +1,52 @@
|
|||
3c3
|
||||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "wrong order of arguments to replace call")
|
||||
111c111
|
||||
< (λ (x_new τ) (subst (replace M y x_new) x M_x))
|
||||
---
|
||||
> (λ (x_new τ) (subst (replace M x_new y) x M_x))
|
||||
147a148
|
||||
>
|
||||
272,294c273,284
|
||||
< ;; rewrite all βv redexes already in the term
|
||||
< ;; (but not any new ones that might appear)
|
||||
< (define-metafunction stlc
|
||||
< βv-> : M -> M
|
||||
< [(βv-> ((λ (x τ) M) v)) (subst (βv-> M) x (βv-> v))]
|
||||
< [(βv-> ((λ (x τ) M) y)) (subst (βv-> M) x y)]
|
||||
< [(βv-> (λ (x τ) M)) (λ (x τ) (βv-> M))]
|
||||
< [(βv-> (M N)) ((βv-> M) (βv-> N))]
|
||||
< [(βv-> M) M])
|
||||
<
|
||||
< ;; check : (or/c #f M) -> boolean[#f = counterexample found!]
|
||||
< (define (check M)
|
||||
< (or (not M)
|
||||
< (let ([M-type (type-check M)])
|
||||
< (implies M-type
|
||||
< (let* ([N (term (βv-> ,M))][N-type (type-check N)])
|
||||
< (and (equal? N-type M-type)
|
||||
< (let ([a1 (Eval M)] [a2 (Eval N)])
|
||||
< (and (not (string? a1)) (not (string? a2))
|
||||
< (equal? a1 a2)
|
||||
< (or (equal? a1 'error)
|
||||
< (and (equal? (type-check a1) M-type)
|
||||
< (equal? (type-check a2) M-type)))))))))))
|
||||
---
|
||||
> (define (check term)
|
||||
> (or (not term)
|
||||
> (v? term)
|
||||
> (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))))))))))
|
||||
298a289,292
|
||||
> (define small-counter-example
|
||||
> (term ((λ (x int) (λ (y int) y)) 1)))
|
||||
> (test-equal (check small-counter-example) #f)
|
||||
>
|
||||
|
|
@ -0,0 +1,50 @@
|
|||
3c3
|
||||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "swaps function and argument position in application")
|
||||
115c115
|
||||
< ((subst M x M_x) (subst N x M_x))]
|
||||
---
|
||||
> ((subst N x M_x) (subst M x M_x))]
|
||||
272,294c272,283
|
||||
< ;; rewrite all βv redexes already in the term
|
||||
< ;; (but not any new ones that might appear)
|
||||
< (define-metafunction stlc
|
||||
< βv-> : M -> M
|
||||
< [(βv-> ((λ (x τ) M) v)) (subst (βv-> M) x (βv-> v))]
|
||||
< [(βv-> ((λ (x τ) M) y)) (subst (βv-> M) x y)]
|
||||
< [(βv-> (λ (x τ) M)) (λ (x τ) (βv-> M))]
|
||||
< [(βv-> (M N)) ((βv-> M) (βv-> N))]
|
||||
< [(βv-> M) M])
|
||||
<
|
||||
< ;; check : (or/c #f M) -> boolean[#f = counterexample found!]
|
||||
< (define (check M)
|
||||
< (or (not M)
|
||||
< (let ([M-type (type-check M)])
|
||||
< (implies M-type
|
||||
< (let* ([N (term (βv-> ,M))][N-type (type-check N)])
|
||||
< (and (equal? N-type M-type)
|
||||
< (let ([a1 (Eval M)] [a2 (Eval N)])
|
||||
< (and (not (string? a1)) (not (string? a2))
|
||||
< (equal? a1 a2)
|
||||
< (or (equal? a1 'error)
|
||||
< (and (equal? (type-check a1) M-type)
|
||||
< (equal? (type-check a2) M-type)))))))))))
|
||||
---
|
||||
> (define (check term)
|
||||
> (or (not term)
|
||||
> (v? term)
|
||||
> (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))))))))))
|
||||
297a287,290
|
||||
>
|
||||
> (define small-counter-example
|
||||
> (term ((λ (x int) (+ 1)) 1)))
|
||||
> (test-equal (check small-counter-example) #f)
|
||||
|
|
@ -0,0 +1,50 @@
|
|||
3c3
|
||||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "replace all variables")
|
||||
106c106
|
||||
< [(subst x x M_x)
|
||||
---
|
||||
> [(subst x y M_x)
|
||||
272,294c272,283
|
||||
< ;; rewrite all βv redexes already in the term
|
||||
< ;; (but not any new ones that might appear)
|
||||
< (define-metafunction stlc
|
||||
< βv-> : M -> M
|
||||
< [(βv-> ((λ (x τ) M) v)) (subst (βv-> M) x (βv-> v))]
|
||||
< [(βv-> ((λ (x τ) M) y)) (subst (βv-> M) x y)]
|
||||
< [(βv-> (λ (x τ) M)) (λ (x τ) (βv-> M))]
|
||||
< [(βv-> (M N)) ((βv-> M) (βv-> N))]
|
||||
< [(βv-> M) M])
|
||||
<
|
||||
< ;; check : (or/c #f M) -> boolean[#f = counterexample found!]
|
||||
< (define (check M)
|
||||
< (or (not M)
|
||||
< (let ([M-type (type-check M)])
|
||||
< (implies M-type
|
||||
< (let* ([N (term (βv-> ,M))][N-type (type-check N)])
|
||||
< (and (equal? N-type M-type)
|
||||
< (let ([a1 (Eval M)] [a2 (Eval N)])
|
||||
< (and (not (string? a1)) (not (string? a2))
|
||||
< (equal? a1 a2)
|
||||
< (or (equal? a1 'error)
|
||||
< (and (equal? (type-check a1) M-type)
|
||||
< (equal? (type-check a2) M-type)))))))))))
|
||||
---
|
||||
> (define (check term)
|
||||
> (or (not term)
|
||||
> (v? term)
|
||||
> (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))))))))))
|
||||
298a288,291
|
||||
> (define small-counter-example
|
||||
> (term ((λ (x int) (λ (y (list int)) (hd y))) 1)))
|
||||
> (test-equal (check small-counter-example) #f)
|
||||
>
|
||||
|
|
@ -0,0 +1,295 @@
|
|||
#lang racket/base
|
||||
|
||||
(define the-error "forgot the variable case")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/match
|
||||
racket/list
|
||||
racket/contract
|
||||
racket/bool)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define-language stlc
|
||||
(M N ::=
|
||||
(λ (x σ) M)
|
||||
(M N)
|
||||
x
|
||||
c)
|
||||
(Γ (x σ Γ)
|
||||
•)
|
||||
(σ τ ::=
|
||||
int
|
||||
(list int)
|
||||
(σ → τ))
|
||||
(c d ::= cons nil hd tl + integer)
|
||||
((x y) variable-not-otherwise-mentioned)
|
||||
|
||||
(v (λ (x τ) M)
|
||||
c
|
||||
(cons v)
|
||||
((cons v) v)
|
||||
(+ v))
|
||||
(E hole
|
||||
(E M)
|
||||
(v E)))
|
||||
|
||||
(define-judgment-form stlc
|
||||
#:mode (typeof I I O)
|
||||
#:contract (typeof Γ M σ)
|
||||
|
||||
[---------------------------
|
||||
(typeof Γ c (const-type c))]
|
||||
|
||||
[(where τ (lookup Γ x))
|
||||
----------------------
|
||||
(typeof Γ x τ)]
|
||||
|
||||
[(typeof (x σ Γ) M σ_2)
|
||||
--------------------------------
|
||||
(typeof Γ (λ (x σ) M) (σ → σ_2))]
|
||||
|
||||
[(typeof Γ M (σ → σ_2))
|
||||
(typeof Γ M_2 σ)
|
||||
----------------------
|
||||
(typeof Γ (M M_2) σ_2)])
|
||||
|
||||
(define-metafunction stlc
|
||||
const-type : c -> σ
|
||||
[(const-type nil)
|
||||
(list int)]
|
||||
[(const-type cons)
|
||||
(int → ((list int) → (list int)))]
|
||||
[(const-type hd)
|
||||
((list int) → int)]
|
||||
[(const-type tl)
|
||||
((list int) → (list int))]
|
||||
[(const-type +)
|
||||
(int → (int → int))]
|
||||
[(const-type integer)
|
||||
int])
|
||||
|
||||
(define-metafunction stlc
|
||||
lookup : Γ x -> σ or #f
|
||||
[(lookup (x σ Γ) x)
|
||||
σ]
|
||||
[(lookup (x σ Γ) x_2)
|
||||
(lookup Γ x_2)]
|
||||
[(lookup • x)
|
||||
#f])
|
||||
|
||||
(define red
|
||||
(reduction-relation
|
||||
stlc
|
||||
(--> (in-hole E ((λ (x τ) M) v))
|
||||
(in-hole E (subst M x v))
|
||||
"βv")
|
||||
(--> (in-hole E (hd ((cons v_1) v_2)))
|
||||
(in-hole E v_1)
|
||||
"hd")
|
||||
(--> (in-hole E (tl ((cons v_1) v_2)))
|
||||
(in-hole E v_2)
|
||||
"tl")
|
||||
(--> (in-hole E (hd nil))
|
||||
"error"
|
||||
"hd-err")
|
||||
(--> (in-hole E (tl nil))
|
||||
"error"
|
||||
"tl-err")
|
||||
(--> (in-hole E ((+ integer_1) integer_2))
|
||||
(in-hole E ,(+ (term integer_1) (term integer_2)))
|
||||
"+")))
|
||||
|
||||
(define-metafunction stlc
|
||||
subst : M x M -> M
|
||||
[(subst (λ (x τ) M) x M_x)
|
||||
(λ (x τ) M)]
|
||||
[(subst (λ (y τ) M) x M_x)
|
||||
(λ (x_new τ) (subst (replace M y x_new) x M_x))
|
||||
(where x_new ,(variable-not-in (term (x y M))
|
||||
(term y)))]
|
||||
[(subst (M N) x M_x)
|
||||
((subst M x M_x) (subst N x M_x))]
|
||||
[(subst M x M_z)
|
||||
M])
|
||||
|
||||
(define-metafunction stlc
|
||||
[(replace (any_1 ...) x_1 x_new)
|
||||
((replace any_1 x_1 x_new) ...)]
|
||||
[(replace x_1 x_1 x_new)
|
||||
x_new]
|
||||
[(replace any_1 x_1 x_new)
|
||||
any_1])
|
||||
|
||||
(define M? (redex-match stlc M))
|
||||
(define/contract (Eval M)
|
||||
(-> M? (or/c M? string? 'error))
|
||||
(define M-t (judgment-holds (typeof • ,M τ) τ))
|
||||
(cond
|
||||
[(pair? M-t)
|
||||
(define res (apply-reduction-relation* red M))
|
||||
(cond
|
||||
[(= 1 (length res))
|
||||
(define ans (car res))
|
||||
(if (equal? "error" ans)
|
||||
'error
|
||||
(let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
|
||||
(cond
|
||||
[(equal? M-t ans-t) ans]
|
||||
[else (format "internal error: type soundness fails for ~s" M)])))]
|
||||
[else
|
||||
(format "internal error: not exactly 1 result ~s => ~s" M res)])]
|
||||
[else
|
||||
(error 'Eval "argument doesn't typecheck: ~s" M)]))
|
||||
|
||||
(define x? (redex-match stlc x))
|
||||
|
||||
(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 τ) τ))
|
||||
(cond
|
||||
[(empty? M-t)
|
||||
#f]
|
||||
[(null? (cdr M-t))
|
||||
(car M-t)]
|
||||
[else
|
||||
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
|
||||
|
||||
(test-equal (type-check (term 5))
|
||||
(term int))
|
||||
(test-equal (type-check (term (5 5)))
|
||||
#f)
|
||||
|
||||
(define (progress-holds? M)
|
||||
(if (type-check M)
|
||||
(or (v? M)
|
||||
(not (null? (apply-reduction-relation red (term ,M)))))
|
||||
#t))
|
||||
|
||||
(define (interesting-term? M)
|
||||
(and (type-check M)
|
||||
(term (uses-bound-var? () ,M))))
|
||||
|
||||
(define-metafunction stlc
|
||||
[(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
|
||||
#t]
|
||||
[(uses-bound-var? (x_0 ...) (λ (x τ) M))
|
||||
(uses-bound-var? (x x_0 ...) M)]
|
||||
[(uses-bound-var? (x ...) (M N))
|
||||
,(or (term (uses-bound-var? (x ...) M))
|
||||
(term (uses-bound-var? (x ...) N)))]
|
||||
[(uses-bound-var? (x ...) (cons M))
|
||||
(uses-bound-var? (x ...) M)]
|
||||
[(uses-bound-var? (x ...) any)
|
||||
#f])
|
||||
|
||||
(define (really-interesting-term? M)
|
||||
(and (interesting-term? M)
|
||||
(term (applies-bv? () ,M))))
|
||||
|
||||
(define-metafunction stlc
|
||||
[(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
|
||||
#t]
|
||||
[(applies-bv? (x_0 ...) (λ (x τ) M))
|
||||
(applies-bv? (x x_0 ...) M)]
|
||||
[(applies-bv? (x ...) (M N))
|
||||
,(or (term (applies-bv? (x ...) M))
|
||||
(term (applies-bv? (x ...) N)))]
|
||||
[(applies-bv? (x ...) (cons M))
|
||||
(applies-bv? (x ...) M)]
|
||||
[(applies-bv? (x ...) any)
|
||||
#f])
|
||||
|
||||
(define (reduction-step-count/func red v?)
|
||||
(λ (term)
|
||||
(let loop ([t term]
|
||||
[n 0])
|
||||
(define res (apply-reduction-relation red t))
|
||||
(cond
|
||||
[(and (empty? res)
|
||||
(v? t))
|
||||
n]
|
||||
[(and (empty? res)
|
||||
(equal? t "error"))
|
||||
n]
|
||||
[(= (length res) 1)
|
||||
(loop (car res) (add1 n))]
|
||||
[else
|
||||
(error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
|
||||
|
||||
(define reduction-step-count
|
||||
(reduction-step-count/func red v?))
|
||||
|
||||
(define (generate-M-term)
|
||||
(generate-term stlc M 5))
|
||||
|
||||
(define (generate-M-term-from-red)
|
||||
(generate-term #:source red 5))
|
||||
|
||||
(define (generate-typed-term)
|
||||
(match (generate-term stlc
|
||||
#:satisfying
|
||||
(typeof • M τ)
|
||||
5)
|
||||
[`(typeof • ,M ,τ)
|
||||
M]
|
||||
[#f #f]))
|
||||
|
||||
(define (generate-typed-term-from-red)
|
||||
(define candidate
|
||||
(case (random 5)
|
||||
[(0)
|
||||
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
|
||||
[(1)
|
||||
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
|
||||
[(2)
|
||||
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
|
||||
[(3)
|
||||
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
|
||||
[(4)
|
||||
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
|
||||
(match candidate
|
||||
[`(typeof • ,M ,τ)
|
||||
M]
|
||||
[#f #f]))
|
||||
|
||||
(define (typed-generator)
|
||||
(let ([g (redex-generator stlc
|
||||
(typeof • M τ)
|
||||
5)])
|
||||
(λ ()
|
||||
(match (g)
|
||||
[`(typeof • ,M ,τ)
|
||||
M]
|
||||
[#f #f]))))
|
||||
|
||||
|
||||
(define (check term)
|
||||
(or (not term)
|
||||
(v? term)
|
||||
(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.035)))
|
||||
|
||||
(define small-counter-example
|
||||
(term ((λ (x int) x) 1)))
|
||||
(test-equal (check small-counter-example) #f)
|
||||
|
||||
(define (ordered-enum-generator)
|
||||
(let ([index 0])
|
||||
(λ ()
|
||||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
|
@ -0,0 +1,298 @@
|
|||
#lang racket/base
|
||||
|
||||
(define the-error "wrong order of arguments to replace call")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/match
|
||||
racket/list
|
||||
racket/contract
|
||||
racket/bool)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define-language stlc
|
||||
(M N ::=
|
||||
(λ (x σ) M)
|
||||
(M N)
|
||||
x
|
||||
c)
|
||||
(Γ (x σ Γ)
|
||||
•)
|
||||
(σ τ ::=
|
||||
int
|
||||
(list int)
|
||||
(σ → τ))
|
||||
(c d ::= cons nil hd tl + integer)
|
||||
((x y) variable-not-otherwise-mentioned)
|
||||
|
||||
(v (λ (x τ) M)
|
||||
c
|
||||
(cons v)
|
||||
((cons v) v)
|
||||
(+ v))
|
||||
(E hole
|
||||
(E M)
|
||||
(v E)))
|
||||
|
||||
(define-judgment-form stlc
|
||||
#:mode (typeof I I O)
|
||||
#:contract (typeof Γ M σ)
|
||||
|
||||
[---------------------------
|
||||
(typeof Γ c (const-type c))]
|
||||
|
||||
[(where τ (lookup Γ x))
|
||||
----------------------
|
||||
(typeof Γ x τ)]
|
||||
|
||||
[(typeof (x σ Γ) M σ_2)
|
||||
--------------------------------
|
||||
(typeof Γ (λ (x σ) M) (σ → σ_2))]
|
||||
|
||||
[(typeof Γ M (σ → σ_2))
|
||||
(typeof Γ M_2 σ)
|
||||
----------------------
|
||||
(typeof Γ (M M_2) σ_2)])
|
||||
|
||||
(define-metafunction stlc
|
||||
const-type : c -> σ
|
||||
[(const-type nil)
|
||||
(list int)]
|
||||
[(const-type cons)
|
||||
(int → ((list int) → (list int)))]
|
||||
[(const-type hd)
|
||||
((list int) → int)]
|
||||
[(const-type tl)
|
||||
((list int) → (list int))]
|
||||
[(const-type +)
|
||||
(int → (int → int))]
|
||||
[(const-type integer)
|
||||
int])
|
||||
|
||||
(define-metafunction stlc
|
||||
lookup : Γ x -> σ or #f
|
||||
[(lookup (x σ Γ) x)
|
||||
σ]
|
||||
[(lookup (x σ Γ) x_2)
|
||||
(lookup Γ x_2)]
|
||||
[(lookup • x)
|
||||
#f])
|
||||
|
||||
(define red
|
||||
(reduction-relation
|
||||
stlc
|
||||
(--> (in-hole E ((λ (x τ) M) v))
|
||||
(in-hole E (subst M x v))
|
||||
"βv")
|
||||
(--> (in-hole E (hd ((cons v_1) v_2)))
|
||||
(in-hole E v_1)
|
||||
"hd")
|
||||
(--> (in-hole E (tl ((cons v_1) v_2)))
|
||||
(in-hole E v_2)
|
||||
"tl")
|
||||
(--> (in-hole E (hd nil))
|
||||
"error"
|
||||
"hd-err")
|
||||
(--> (in-hole E (tl nil))
|
||||
"error"
|
||||
"tl-err")
|
||||
(--> (in-hole E ((+ integer_1) integer_2))
|
||||
(in-hole E ,(+ (term integer_1) (term integer_2)))
|
||||
"+")))
|
||||
|
||||
(define-metafunction stlc
|
||||
subst : M x M -> M
|
||||
[(subst x x M_x)
|
||||
M_x]
|
||||
[(subst (λ (x τ) M) x M_x)
|
||||
(λ (x τ) M)]
|
||||
[(subst (λ (y τ) M) x M_x)
|
||||
(λ (x_new τ) (subst (replace M x_new y) x M_x))
|
||||
(where x_new ,(variable-not-in (term (x y M))
|
||||
(term y)))]
|
||||
[(subst (M N) x M_x)
|
||||
((subst M x M_x) (subst N x M_x))]
|
||||
[(subst M x M_z)
|
||||
M])
|
||||
|
||||
(define-metafunction stlc
|
||||
[(replace (any_1 ...) x_1 x_new)
|
||||
((replace any_1 x_1 x_new) ...)]
|
||||
[(replace x_1 x_1 x_new)
|
||||
x_new]
|
||||
[(replace any_1 x_1 x_new)
|
||||
any_1])
|
||||
|
||||
(define M? (redex-match stlc M))
|
||||
(define/contract (Eval M)
|
||||
(-> M? (or/c M? string? 'error))
|
||||
(define M-t (judgment-holds (typeof • ,M τ) τ))
|
||||
(cond
|
||||
[(pair? M-t)
|
||||
(define res (apply-reduction-relation* red M))
|
||||
(cond
|
||||
[(= 1 (length res))
|
||||
(define ans (car res))
|
||||
(if (equal? "error" ans)
|
||||
'error
|
||||
(let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
|
||||
(cond
|
||||
[(equal? M-t ans-t) ans]
|
||||
[else (format "internal error: type soundness fails for ~s" M)])))]
|
||||
[else
|
||||
(format "internal error: not exactly 1 result ~s => ~s" M res)])]
|
||||
[else
|
||||
(error 'Eval "argument doesn't typecheck: ~s" M)]))
|
||||
|
||||
|
||||
(define x? (redex-match stlc x))
|
||||
|
||||
(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 τ) τ))
|
||||
(cond
|
||||
[(empty? M-t)
|
||||
#f]
|
||||
[(null? (cdr M-t))
|
||||
(car M-t)]
|
||||
[else
|
||||
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
|
||||
|
||||
(test-equal (type-check (term 5))
|
||||
(term int))
|
||||
(test-equal (type-check (term (5 5)))
|
||||
#f)
|
||||
|
||||
(define (progress-holds? M)
|
||||
(if (type-check M)
|
||||
(or (v? M)
|
||||
(not (null? (apply-reduction-relation red (term ,M)))))
|
||||
#t))
|
||||
|
||||
(define (interesting-term? M)
|
||||
(and (type-check M)
|
||||
(term (uses-bound-var? () ,M))))
|
||||
|
||||
(define-metafunction stlc
|
||||
[(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
|
||||
#t]
|
||||
[(uses-bound-var? (x_0 ...) (λ (x τ) M))
|
||||
(uses-bound-var? (x x_0 ...) M)]
|
||||
[(uses-bound-var? (x ...) (M N))
|
||||
,(or (term (uses-bound-var? (x ...) M))
|
||||
(term (uses-bound-var? (x ...) N)))]
|
||||
[(uses-bound-var? (x ...) (cons M))
|
||||
(uses-bound-var? (x ...) M)]
|
||||
[(uses-bound-var? (x ...) any)
|
||||
#f])
|
||||
|
||||
(define (really-interesting-term? M)
|
||||
(and (interesting-term? M)
|
||||
(term (applies-bv? () ,M))))
|
||||
|
||||
(define-metafunction stlc
|
||||
[(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
|
||||
#t]
|
||||
[(applies-bv? (x_0 ...) (λ (x τ) M))
|
||||
(applies-bv? (x x_0 ...) M)]
|
||||
[(applies-bv? (x ...) (M N))
|
||||
,(or (term (applies-bv? (x ...) M))
|
||||
(term (applies-bv? (x ...) N)))]
|
||||
[(applies-bv? (x ...) (cons M))
|
||||
(applies-bv? (x ...) M)]
|
||||
[(applies-bv? (x ...) any)
|
||||
#f])
|
||||
|
||||
(define (reduction-step-count/func red v?)
|
||||
(λ (term)
|
||||
(let loop ([t term]
|
||||
[n 0])
|
||||
(define res (apply-reduction-relation red t))
|
||||
(cond
|
||||
[(and (empty? res)
|
||||
(v? t))
|
||||
n]
|
||||
[(and (empty? res)
|
||||
(equal? t "error"))
|
||||
n]
|
||||
[(= (length res) 1)
|
||||
(loop (car res) (add1 n))]
|
||||
[else
|
||||
(error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
|
||||
|
||||
(define reduction-step-count
|
||||
(reduction-step-count/func red v?))
|
||||
|
||||
(define (generate-M-term)
|
||||
(generate-term stlc M 5))
|
||||
|
||||
(define (generate-M-term-from-red)
|
||||
(generate-term #:source red 5))
|
||||
|
||||
(define (generate-typed-term)
|
||||
(match (generate-term stlc
|
||||
#:satisfying
|
||||
(typeof • M τ)
|
||||
5)
|
||||
[`(typeof • ,M ,τ)
|
||||
M]
|
||||
[#f #f]))
|
||||
|
||||
(define (generate-typed-term-from-red)
|
||||
(define candidate
|
||||
(case (random 5)
|
||||
[(0)
|
||||
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
|
||||
[(1)
|
||||
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
|
||||
[(2)
|
||||
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
|
||||
[(3)
|
||||
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
|
||||
[(4)
|
||||
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
|
||||
(match candidate
|
||||
[`(typeof • ,M ,τ)
|
||||
M]
|
||||
[#f #f]))
|
||||
|
||||
(define (typed-generator)
|
||||
(let ([g (redex-generator stlc
|
||||
(typeof • M τ)
|
||||
5)])
|
||||
(λ ()
|
||||
(match (g)
|
||||
[`(typeof • ,M ,τ)
|
||||
M]
|
||||
[#f #f]))))
|
||||
|
||||
|
||||
(define (check term)
|
||||
(or (not term)
|
||||
(v? term)
|
||||
(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.035)))
|
||||
|
||||
(define small-counter-example
|
||||
(term ((λ (x int) (λ (y int) y)) 1)))
|
||||
(test-equal (check small-counter-example) #f)
|
||||
|
||||
(define (ordered-enum-generator)
|
||||
(let ([index 0])
|
||||
(λ ()
|
||||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
|
@ -0,0 +1,297 @@
|
|||
#lang racket/base
|
||||
|
||||
(define the-error "swaps function and argument position in application")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/match
|
||||
racket/list
|
||||
racket/contract
|
||||
racket/bool)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define-language stlc
|
||||
(M N ::=
|
||||
(λ (x σ) M)
|
||||
(M N)
|
||||
x
|
||||
c)
|
||||
(Γ (x σ Γ)
|
||||
•)
|
||||
(σ τ ::=
|
||||
int
|
||||
(list int)
|
||||
(σ → τ))
|
||||
(c d ::= cons nil hd tl + integer)
|
||||
((x y) variable-not-otherwise-mentioned)
|
||||
|
||||
(v (λ (x τ) M)
|
||||
c
|
||||
(cons v)
|
||||
((cons v) v)
|
||||
(+ v))
|
||||
(E hole
|
||||
(E M)
|
||||
(v E)))
|
||||
|
||||
(define-judgment-form stlc
|
||||
#:mode (typeof I I O)
|
||||
#:contract (typeof Γ M σ)
|
||||
|
||||
[---------------------------
|
||||
(typeof Γ c (const-type c))]
|
||||
|
||||
[(where τ (lookup Γ x))
|
||||
----------------------
|
||||
(typeof Γ x τ)]
|
||||
|
||||
[(typeof (x σ Γ) M σ_2)
|
||||
--------------------------------
|
||||
(typeof Γ (λ (x σ) M) (σ → σ_2))]
|
||||
|
||||
[(typeof Γ M (σ → σ_2))
|
||||
(typeof Γ M_2 σ)
|
||||
----------------------
|
||||
(typeof Γ (M M_2) σ_2)])
|
||||
|
||||
(define-metafunction stlc
|
||||
const-type : c -> σ
|
||||
[(const-type nil)
|
||||
(list int)]
|
||||
[(const-type cons)
|
||||
(int → ((list int) → (list int)))]
|
||||
[(const-type hd)
|
||||
((list int) → int)]
|
||||
[(const-type tl)
|
||||
((list int) → (list int))]
|
||||
[(const-type +)
|
||||
(int → (int → int))]
|
||||
[(const-type integer)
|
||||
int])
|
||||
|
||||
(define-metafunction stlc
|
||||
lookup : Γ x -> σ or #f
|
||||
[(lookup (x σ Γ) x)
|
||||
σ]
|
||||
[(lookup (x σ Γ) x_2)
|
||||
(lookup Γ x_2)]
|
||||
[(lookup • x)
|
||||
#f])
|
||||
|
||||
(define red
|
||||
(reduction-relation
|
||||
stlc
|
||||
(--> (in-hole E ((λ (x τ) M) v))
|
||||
(in-hole E (subst M x v))
|
||||
"βv")
|
||||
(--> (in-hole E (hd ((cons v_1) v_2)))
|
||||
(in-hole E v_1)
|
||||
"hd")
|
||||
(--> (in-hole E (tl ((cons v_1) v_2)))
|
||||
(in-hole E v_2)
|
||||
"tl")
|
||||
(--> (in-hole E (hd nil))
|
||||
"error"
|
||||
"hd-err")
|
||||
(--> (in-hole E (tl nil))
|
||||
"error"
|
||||
"tl-err")
|
||||
(--> (in-hole E ((+ integer_1) integer_2))
|
||||
(in-hole E ,(+ (term integer_1) (term integer_2)))
|
||||
"+")))
|
||||
|
||||
(define-metafunction stlc
|
||||
subst : M x M -> M
|
||||
[(subst x x M_x)
|
||||
M_x]
|
||||
[(subst (λ (x τ) M) x M_x)
|
||||
(λ (x τ) M)]
|
||||
[(subst (λ (y τ) M) x M_x)
|
||||
(λ (x_new τ) (subst (replace M y x_new) x M_x))
|
||||
(where x_new ,(variable-not-in (term (x y M))
|
||||
(term y)))]
|
||||
[(subst (M N) x M_x)
|
||||
((subst N x M_x) (subst M x M_x))]
|
||||
[(subst M x M_z)
|
||||
M])
|
||||
|
||||
(define-metafunction stlc
|
||||
[(replace (any_1 ...) x_1 x_new)
|
||||
((replace any_1 x_1 x_new) ...)]
|
||||
[(replace x_1 x_1 x_new)
|
||||
x_new]
|
||||
[(replace any_1 x_1 x_new)
|
||||
any_1])
|
||||
|
||||
(define M? (redex-match stlc M))
|
||||
(define/contract (Eval M)
|
||||
(-> M? (or/c M? string? 'error))
|
||||
(define M-t (judgment-holds (typeof • ,M τ) τ))
|
||||
(cond
|
||||
[(pair? M-t)
|
||||
(define res (apply-reduction-relation* red M))
|
||||
(cond
|
||||
[(= 1 (length res))
|
||||
(define ans (car res))
|
||||
(if (equal? "error" ans)
|
||||
'error
|
||||
(let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
|
||||
(cond
|
||||
[(equal? M-t ans-t) ans]
|
||||
[else (format "internal error: type soundness fails for ~s" M)])))]
|
||||
[else
|
||||
(format "internal error: not exactly 1 result ~s => ~s" M res)])]
|
||||
[else
|
||||
(error 'Eval "argument doesn't typecheck: ~s" M)]))
|
||||
|
||||
(define x? (redex-match stlc x))
|
||||
|
||||
(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 τ) τ))
|
||||
(cond
|
||||
[(empty? M-t)
|
||||
#f]
|
||||
[(null? (cdr M-t))
|
||||
(car M-t)]
|
||||
[else
|
||||
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
|
||||
|
||||
(test-equal (type-check (term 5))
|
||||
(term int))
|
||||
(test-equal (type-check (term (5 5)))
|
||||
#f)
|
||||
|
||||
(define (progress-holds? M)
|
||||
(if (type-check M)
|
||||
(or (v? M)
|
||||
(not (null? (apply-reduction-relation red (term ,M)))))
|
||||
#t))
|
||||
|
||||
(define (interesting-term? M)
|
||||
(and (type-check M)
|
||||
(term (uses-bound-var? () ,M))))
|
||||
|
||||
(define-metafunction stlc
|
||||
[(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
|
||||
#t]
|
||||
[(uses-bound-var? (x_0 ...) (λ (x τ) M))
|
||||
(uses-bound-var? (x x_0 ...) M)]
|
||||
[(uses-bound-var? (x ...) (M N))
|
||||
,(or (term (uses-bound-var? (x ...) M))
|
||||
(term (uses-bound-var? (x ...) N)))]
|
||||
[(uses-bound-var? (x ...) (cons M))
|
||||
(uses-bound-var? (x ...) M)]
|
||||
[(uses-bound-var? (x ...) any)
|
||||
#f])
|
||||
|
||||
(define (really-interesting-term? M)
|
||||
(and (interesting-term? M)
|
||||
(term (applies-bv? () ,M))))
|
||||
|
||||
(define-metafunction stlc
|
||||
[(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
|
||||
#t]
|
||||
[(applies-bv? (x_0 ...) (λ (x τ) M))
|
||||
(applies-bv? (x x_0 ...) M)]
|
||||
[(applies-bv? (x ...) (M N))
|
||||
,(or (term (applies-bv? (x ...) M))
|
||||
(term (applies-bv? (x ...) N)))]
|
||||
[(applies-bv? (x ...) (cons M))
|
||||
(applies-bv? (x ...) M)]
|
||||
[(applies-bv? (x ...) any)
|
||||
#f])
|
||||
|
||||
(define (reduction-step-count/func red v?)
|
||||
(λ (term)
|
||||
(let loop ([t term]
|
||||
[n 0])
|
||||
(define res (apply-reduction-relation red t))
|
||||
(cond
|
||||
[(and (empty? res)
|
||||
(v? t))
|
||||
n]
|
||||
[(and (empty? res)
|
||||
(equal? t "error"))
|
||||
n]
|
||||
[(= (length res) 1)
|
||||
(loop (car res) (add1 n))]
|
||||
[else
|
||||
(error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
|
||||
|
||||
(define reduction-step-count
|
||||
(reduction-step-count/func red v?))
|
||||
|
||||
(define (generate-M-term)
|
||||
(generate-term stlc M 5))
|
||||
|
||||
(define (generate-M-term-from-red)
|
||||
(generate-term #:source red 5))
|
||||
|
||||
(define (generate-typed-term)
|
||||
(match (generate-term stlc
|
||||
#:satisfying
|
||||
(typeof • M τ)
|
||||
5)
|
||||
[`(typeof • ,M ,τ)
|
||||
M]
|
||||
[#f #f]))
|
||||
|
||||
(define (generate-typed-term-from-red)
|
||||
(define candidate
|
||||
(case (random 5)
|
||||
[(0)
|
||||
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
|
||||
[(1)
|
||||
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
|
||||
[(2)
|
||||
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
|
||||
[(3)
|
||||
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
|
||||
[(4)
|
||||
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
|
||||
(match candidate
|
||||
[`(typeof • ,M ,τ)
|
||||
M]
|
||||
[#f #f]))
|
||||
|
||||
(define (typed-generator)
|
||||
(let ([g (redex-generator stlc
|
||||
(typeof • M τ)
|
||||
5)])
|
||||
(λ ()
|
||||
(match (g)
|
||||
[`(typeof • ,M ,τ)
|
||||
M]
|
||||
[#f #f]))))
|
||||
|
||||
|
||||
(define (check term)
|
||||
(or (not term)
|
||||
(v? term)
|
||||
(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.035)))
|
||||
|
||||
(define small-counter-example
|
||||
(term ((λ (x int) (+ 1)) 1)))
|
||||
(test-equal (check small-counter-example) #f)
|
||||
|
||||
(define (ordered-enum-generator)
|
||||
(let ([index 0])
|
||||
(λ ()
|
||||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
|
@ -0,0 +1,297 @@
|
|||
#lang racket/base
|
||||
|
||||
(define the-error "replace all variables")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/match
|
||||
racket/list
|
||||
racket/contract
|
||||
racket/bool)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define-language stlc
|
||||
(M N ::=
|
||||
(λ (x σ) M)
|
||||
(M N)
|
||||
x
|
||||
c)
|
||||
(Γ (x σ Γ)
|
||||
•)
|
||||
(σ τ ::=
|
||||
int
|
||||
(list int)
|
||||
(σ → τ))
|
||||
(c d ::= cons nil hd tl + integer)
|
||||
((x y) variable-not-otherwise-mentioned)
|
||||
|
||||
(v (λ (x τ) M)
|
||||
c
|
||||
(cons v)
|
||||
((cons v) v)
|
||||
(+ v))
|
||||
(E hole
|
||||
(E M)
|
||||
(v E)))
|
||||
|
||||
(define-judgment-form stlc
|
||||
#:mode (typeof I I O)
|
||||
#:contract (typeof Γ M σ)
|
||||
|
||||
[---------------------------
|
||||
(typeof Γ c (const-type c))]
|
||||
|
||||
[(where τ (lookup Γ x))
|
||||
----------------------
|
||||
(typeof Γ x τ)]
|
||||
|
||||
[(typeof (x σ Γ) M σ_2)
|
||||
--------------------------------
|
||||
(typeof Γ (λ (x σ) M) (σ → σ_2))]
|
||||
|
||||
[(typeof Γ M (σ → σ_2))
|
||||
(typeof Γ M_2 σ)
|
||||
----------------------
|
||||
(typeof Γ (M M_2) σ_2)])
|
||||
|
||||
(define-metafunction stlc
|
||||
const-type : c -> σ
|
||||
[(const-type nil)
|
||||
(list int)]
|
||||
[(const-type cons)
|
||||
(int → ((list int) → (list int)))]
|
||||
[(const-type hd)
|
||||
((list int) → int)]
|
||||
[(const-type tl)
|
||||
((list int) → (list int))]
|
||||
[(const-type +)
|
||||
(int → (int → int))]
|
||||
[(const-type integer)
|
||||
int])
|
||||
|
||||
(define-metafunction stlc
|
||||
lookup : Γ x -> σ or #f
|
||||
[(lookup (x σ Γ) x)
|
||||
σ]
|
||||
[(lookup (x σ Γ) x_2)
|
||||
(lookup Γ x_2)]
|
||||
[(lookup • x)
|
||||
#f])
|
||||
|
||||
(define red
|
||||
(reduction-relation
|
||||
stlc
|
||||
(--> (in-hole E ((λ (x τ) M) v))
|
||||
(in-hole E (subst M x v))
|
||||
"βv")
|
||||
(--> (in-hole E (hd ((cons v_1) v_2)))
|
||||
(in-hole E v_1)
|
||||
"hd")
|
||||
(--> (in-hole E (tl ((cons v_1) v_2)))
|
||||
(in-hole E v_2)
|
||||
"tl")
|
||||
(--> (in-hole E (hd nil))
|
||||
"error"
|
||||
"hd-err")
|
||||
(--> (in-hole E (tl nil))
|
||||
"error"
|
||||
"tl-err")
|
||||
(--> (in-hole E ((+ integer_1) integer_2))
|
||||
(in-hole E ,(+ (term integer_1) (term integer_2)))
|
||||
"+")))
|
||||
|
||||
(define-metafunction stlc
|
||||
subst : M x M -> M
|
||||
[(subst x y M_x)
|
||||
M_x]
|
||||
[(subst (λ (x τ) M) x M_x)
|
||||
(λ (x τ) M)]
|
||||
[(subst (λ (y τ) M) x M_x)
|
||||
(λ (x_new τ) (subst (replace M y x_new) x M_x))
|
||||
(where x_new ,(variable-not-in (term (x y M))
|
||||
(term y)))]
|
||||
[(subst (M N) x M_x)
|
||||
((subst M x M_x) (subst N x M_x))]
|
||||
[(subst M x M_z)
|
||||
M])
|
||||
|
||||
(define-metafunction stlc
|
||||
[(replace (any_1 ...) x_1 x_new)
|
||||
((replace any_1 x_1 x_new) ...)]
|
||||
[(replace x_1 x_1 x_new)
|
||||
x_new]
|
||||
[(replace any_1 x_1 x_new)
|
||||
any_1])
|
||||
|
||||
(define M? (redex-match stlc M))
|
||||
(define/contract (Eval M)
|
||||
(-> M? (or/c M? string? 'error))
|
||||
(define M-t (judgment-holds (typeof • ,M τ) τ))
|
||||
(cond
|
||||
[(pair? M-t)
|
||||
(define res (apply-reduction-relation* red M))
|
||||
(cond
|
||||
[(= 1 (length res))
|
||||
(define ans (car res))
|
||||
(if (equal? "error" ans)
|
||||
'error
|
||||
(let ([ans-t (judgment-holds (typeof • ,ans τ) τ)])
|
||||
(cond
|
||||
[(equal? M-t ans-t) ans]
|
||||
[else (format "internal error: type soundness fails for ~s" M)])))]
|
||||
[else
|
||||
(format "internal error: not exactly 1 result ~s => ~s" M res)])]
|
||||
[else
|
||||
(error 'Eval "argument doesn't typecheck: ~s" M)]))
|
||||
|
||||
(define x? (redex-match stlc x))
|
||||
|
||||
(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 τ) τ))
|
||||
(cond
|
||||
[(empty? M-t)
|
||||
#f]
|
||||
[(null? (cdr M-t))
|
||||
(car M-t)]
|
||||
[else
|
||||
(error 'type-check "non-unique type: ~s : ~s" M M-t)]))
|
||||
|
||||
(test-equal (type-check (term 5))
|
||||
(term int))
|
||||
(test-equal (type-check (term (5 5)))
|
||||
#f)
|
||||
|
||||
(define (progress-holds? M)
|
||||
(if (type-check M)
|
||||
(or (v? M)
|
||||
(not (null? (apply-reduction-relation red (term ,M)))))
|
||||
#t))
|
||||
|
||||
(define (interesting-term? M)
|
||||
(and (type-check M)
|
||||
(term (uses-bound-var? () ,M))))
|
||||
|
||||
(define-metafunction stlc
|
||||
[(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1)
|
||||
#t]
|
||||
[(uses-bound-var? (x_0 ...) (λ (x τ) M))
|
||||
(uses-bound-var? (x x_0 ...) M)]
|
||||
[(uses-bound-var? (x ...) (M N))
|
||||
,(or (term (uses-bound-var? (x ...) M))
|
||||
(term (uses-bound-var? (x ...) N)))]
|
||||
[(uses-bound-var? (x ...) (cons M))
|
||||
(uses-bound-var? (x ...) M)]
|
||||
[(uses-bound-var? (x ...) any)
|
||||
#f])
|
||||
|
||||
(define (really-interesting-term? M)
|
||||
(and (interesting-term? M)
|
||||
(term (applies-bv? () ,M))))
|
||||
|
||||
(define-metafunction stlc
|
||||
[(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M))
|
||||
#t]
|
||||
[(applies-bv? (x_0 ...) (λ (x τ) M))
|
||||
(applies-bv? (x x_0 ...) M)]
|
||||
[(applies-bv? (x ...) (M N))
|
||||
,(or (term (applies-bv? (x ...) M))
|
||||
(term (applies-bv? (x ...) N)))]
|
||||
[(applies-bv? (x ...) (cons M))
|
||||
(applies-bv? (x ...) M)]
|
||||
[(applies-bv? (x ...) any)
|
||||
#f])
|
||||
|
||||
(define (reduction-step-count/func red v?)
|
||||
(λ (term)
|
||||
(let loop ([t term]
|
||||
[n 0])
|
||||
(define res (apply-reduction-relation red t))
|
||||
(cond
|
||||
[(and (empty? res)
|
||||
(v? t))
|
||||
n]
|
||||
[(and (empty? res)
|
||||
(equal? t "error"))
|
||||
n]
|
||||
[(= (length res) 1)
|
||||
(loop (car res) (add1 n))]
|
||||
[else
|
||||
(error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)]))))
|
||||
|
||||
(define reduction-step-count
|
||||
(reduction-step-count/func red v?))
|
||||
|
||||
(define (generate-M-term)
|
||||
(generate-term stlc M 5))
|
||||
|
||||
(define (generate-M-term-from-red)
|
||||
(generate-term #:source red 5))
|
||||
|
||||
(define (generate-typed-term)
|
||||
(match (generate-term stlc
|
||||
#:satisfying
|
||||
(typeof • M τ)
|
||||
5)
|
||||
[`(typeof • ,M ,τ)
|
||||
M]
|
||||
[#f #f]))
|
||||
|
||||
(define (generate-typed-term-from-red)
|
||||
(define candidate
|
||||
(case (random 5)
|
||||
[(0)
|
||||
(generate-term stlc #:satisfying (typeof • ((λ (x τ_x) M) v) ((list int) → (list int))) 5)]
|
||||
[(1)
|
||||
(generate-term stlc #:satisfying (typeof • (hd ((cons v_1) v_2)) ((list int) → (list int))) 5)]
|
||||
[(2)
|
||||
(generate-term stlc #:satisfying (typeof • (tl ((cons v_1) v_2)) ((list int) → (list int))) 5)]
|
||||
[(3)
|
||||
(generate-term stlc #:satisfying (typeof • (hd nil) ((list int) → (list int))) 5)]
|
||||
[(4)
|
||||
(generate-term stlc #:satisfying (typeof • (tl nil) ((list int) → (list int))) 5)]))
|
||||
(match candidate
|
||||
[`(typeof • ,M ,τ)
|
||||
M]
|
||||
[#f #f]))
|
||||
|
||||
(define (typed-generator)
|
||||
(let ([g (redex-generator stlc
|
||||
(typeof • M τ)
|
||||
5)])
|
||||
(λ ()
|
||||
(match (g)
|
||||
[`(typeof • ,M ,τ)
|
||||
M]
|
||||
[#f #f]))))
|
||||
|
||||
|
||||
(define (check term)
|
||||
(or (not term)
|
||||
(v? term)
|
||||
(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.035)))
|
||||
|
||||
(define small-counter-example
|
||||
(term ((λ (x int) (λ (y (list int)) (hd y))) 1)))
|
||||
(test-equal (check small-counter-example) #f)
|
||||
|
||||
(define (ordered-enum-generator)
|
||||
(let ([index 0])
|
||||
(λ ()
|
||||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
Loading…
Reference in New Issue
Block a user