add ref cells and make primitives behave polymorphically and some general cleanup
This commit is contained in:
Robby Findler
parent
3e3829c2b9
commit
af46f203cc
|
|
@ -3,13 +3,12 @@
|
|||
(define the-error "no error")
|
||||
|
||||
(require redex/reduction-semantics
|
||||
;(only-in redex/private/generate-term pick-an-index)
|
||||
(only-in redex/private/generate-term pick-an-index)
|
||||
racket/match
|
||||
racket/list
|
||||
racket/contract
|
||||
racket/bool
|
||||
redex/tut-subst
|
||||
data/union-find)
|
||||
(only-in "../stlc/tests-lib.rkt" consistent-with?))
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
|
|
@ -21,23 +20,30 @@
|
|||
c
|
||||
(let ([x M]) N))
|
||||
(Γ (x σ Γ)
|
||||
•)
|
||||
·)
|
||||
(σ τ ::=
|
||||
int
|
||||
(list τ)
|
||||
(σ → τ)
|
||||
(list τ)
|
||||
(ref τ)
|
||||
x)
|
||||
(c d ::= cons nil hd tl + integer)
|
||||
((x y) variable-not-otherwise-mentioned)
|
||||
(c d ::= c0 c1)
|
||||
(c0 ::= + integer)
|
||||
(c1 ::= cons nil hd tl new get set)
|
||||
(x y r ::= variable-not-otherwise-mentioned)
|
||||
|
||||
(v (λ x M)
|
||||
c
|
||||
(cons v)
|
||||
((cons v) v)
|
||||
(+ v))
|
||||
(cons v)
|
||||
(+ v)
|
||||
(set v)
|
||||
r)
|
||||
(E hole
|
||||
(E M)
|
||||
(v E))
|
||||
(v E)
|
||||
(let ([x E]) M))
|
||||
(Σ ::= · (r v Σ))
|
||||
|
||||
(κ ::=
|
||||
·
|
||||
|
|
@ -51,12 +57,14 @@
|
|||
(define v? (redex-match? stlc v))
|
||||
(define τ? (redex-match? stlc τ))
|
||||
(define x? (redex-match? stlc x))
|
||||
(define M? (redex-match? stlc M))
|
||||
(define Σ-M? (redex-match? stlc (Σ M)))
|
||||
|
||||
(define-judgment-form stlc
|
||||
#:mode (typeof I O)
|
||||
#:contract (typeof M σ)
|
||||
|
||||
[(tc-down • M · σ)
|
||||
[(tc-down · M · σ)
|
||||
-------------
|
||||
(typeof M σ)])
|
||||
|
||||
|
|
@ -64,16 +72,21 @@
|
|||
#:mode (tc-down I I I O)
|
||||
#:contract (tc-down Γ M κ σ)
|
||||
|
||||
[(tc-up (const-type c) κ σ_ans)
|
||||
[(tc-up (const-type0 c0) κ σ_ans)
|
||||
------------------------------
|
||||
(tc-down Γ c κ σ_ans)]
|
||||
(tc-down Γ c0 κ σ_ans)]
|
||||
|
||||
[(where τ (lookup Γ x))
|
||||
[(where x ,(variable-not-in (term (Γ κ)) 'γ))
|
||||
(tc-up (const-type1 x c1) κ σ_ans)
|
||||
------------------------------
|
||||
(tc-down Γ c1 κ σ_ans)]
|
||||
|
||||
[(where τ (lookup-Γ Γ x))
|
||||
(tc-up τ κ σ_ans)
|
||||
---------------------------
|
||||
(tc-down Γ x κ σ_ans)]
|
||||
|
||||
[(where y ,(variable-not-in (term (x Γ M κ)) 'α))
|
||||
[(where y ,(variable-not-in (term (x Γ M κ)) 'α2-))
|
||||
(tc-down (x y Γ) M (λ y κ) σ_ans) ;; BUG: the continuation had 'x' not 'y' in it
|
||||
------------------------------------------------
|
||||
(tc-down Γ (λ x M) κ σ_ans)]
|
||||
|
|
@ -82,8 +95,30 @@
|
|||
--------------------------
|
||||
(tc-down Γ (M_1 M_2) κ σ_2)]
|
||||
|
||||
[(tc-down Γ (subst N x M) κ σ_2)
|
||||
#|
|
||||
;; BUG: this is the classic bug -- it replaces the last two rules below
|
||||
[(where y ,(variable-not-in (term (x M N κ)) 'l))
|
||||
(tc-down Γ ((λ y (subst N x M)) M) κ σ_2)
|
||||
-----------------------------------------
|
||||
(tc-down Γ (let ([x M]) N) κ σ_2)]
|
||||
|#
|
||||
|
||||
#|
|
||||
;; BUG: doesn't type check 'v' when x doesn't occur free in N
|
||||
;; I knew about this and yet STILL forgot to do it properly!
|
||||
[(tc-down Γ (subst N x v) κ σ_2)
|
||||
----------------------------------
|
||||
(tc-down Γ (let ([x v]) N) κ σ_2)]
|
||||
|#
|
||||
|
||||
[(where y ,(variable-not-in (term (x v N κ)) 'l))
|
||||
(tc-down Γ ((λ y (subst N x v)) v) κ σ_2)
|
||||
----------------------------------
|
||||
(tc-down Γ (let ([x v]) N) κ σ_2)]
|
||||
|
||||
[(where #t (not-v? M))
|
||||
(tc-down Γ ((λ x N) M) κ σ_2)
|
||||
---------------------------------
|
||||
(tc-down Γ (let ([x M]) N) κ σ_2)])
|
||||
|
||||
(define-judgment-form stlc
|
||||
|
|
@ -97,7 +132,7 @@
|
|||
---------------------------
|
||||
(tc-up τ (1 Γ M κ) σ_ans)]
|
||||
|
||||
[(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'β))
|
||||
[(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-))
|
||||
(where G (unify τ_2 (τ_1 → x))) ;; BUG: swap τ_2 and τ_1 in this line
|
||||
(tc-up (apply-subst-τ G x)
|
||||
(apply-subst-κ G κ)
|
||||
|
|
@ -153,6 +188,7 @@ section in the paper.
|
|||
;; (c) -- term reduction
|
||||
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
|
||||
[(uh ((list τ) (list σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
|
||||
[(uh ((ref τ) (ref σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
|
||||
[(uh (int int G) G_r boolean) (uh G G_r #t)]
|
||||
|
||||
;; (c) -- failure
|
||||
|
|
@ -191,6 +227,7 @@ section in the paper.
|
|||
eliminate-τ : x τ σ -> σ
|
||||
[(eliminate-τ x τ (σ_1 → σ_2)) ((eliminate-τ x τ σ_1) → (eliminate-τ x τ σ_2))]
|
||||
[(eliminate-τ x τ (list σ)) (list (eliminate-τ x τ σ))]
|
||||
[(eliminate-τ x τ (ref σ)) (ref (eliminate-τ x τ σ))]
|
||||
[(eliminate-τ x τ int) int]
|
||||
[(eliminate-τ x τ x) τ]
|
||||
[(eliminate-τ x τ y) y])
|
||||
|
|
@ -212,6 +249,7 @@ section in the paper.
|
|||
in-vars-τ? : x τ -> boolean
|
||||
[(in-vars-τ? x (τ_1 → τ_2)) (∨ (in-vars-τ? x τ_1) (in-vars-τ? x τ_2))]
|
||||
[(in-vars-τ? x (list τ)) (in-vars-τ? x τ)]
|
||||
[(in-vars-τ? x (ref τ)) (in-vars-τ? x τ)]
|
||||
[(in-vars-τ? x int) #f]
|
||||
[(in-vars-τ? x x) #t]
|
||||
[(in-vars-τ? x y) #f])
|
||||
|
|
@ -243,78 +281,149 @@ section in the paper.
|
|||
|
||||
(define-metafunction stlc
|
||||
apply-subst-Γ : Gx Γ -> Γ
|
||||
[(apply-subst-Γ Gx (y σ Γ))
|
||||
(y (apply-subst-τ Gx σ)
|
||||
(apply-subst-Γ Gx Γ))]
|
||||
[(apply-subst-Γ Gx •) •])
|
||||
[(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))]
|
||||
[(apply-subst-Γ Gx ·) ·])
|
||||
|
||||
(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])
|
||||
const-type0 : c -> σ
|
||||
[(const-type0 +) (int → (int → int))]
|
||||
[(const-type0 integer) int])
|
||||
|
||||
(define-metafunction stlc
|
||||
lookup : Γ x -> σ or #f
|
||||
[(lookup (x σ Γ) x)
|
||||
σ]
|
||||
[(lookup (x σ Γ) y)
|
||||
(lookup Γ y)]
|
||||
[(lookup • x)
|
||||
#f])
|
||||
const-type1 : x c -> σ
|
||||
[(const-type1 x nil) (list x)]
|
||||
[(const-type1 x cons) (x → ((list x) → (list x)))]
|
||||
[(const-type1 x hd) ((list x) → x)]
|
||||
[(const-type1 x tl) ((list x) → (list x))]
|
||||
[(const-type1 x new) (x → (ref x))]
|
||||
[(const-type1 x get) ((ref x) → x)]
|
||||
[(const-type1 x set) ((ref x) → (x → x))])
|
||||
|
||||
(define-metafunction stlc
|
||||
lookup-Γ : Γ x -> σ or #f
|
||||
[(lookup-Γ (x σ Γ) x) σ]
|
||||
[(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)]
|
||||
[(lookup-Γ · x) #f])
|
||||
|
||||
(define-metafunction stlc
|
||||
not-v? : M -> boolean
|
||||
[(not-v? v) #f]
|
||||
[(not-v? M) #t])
|
||||
|
||||
(define red
|
||||
(reduction-relation
|
||||
stlc
|
||||
(--> (in-hole E ((λ x M) v))
|
||||
(in-hole E (subst M x v))
|
||||
(--> (Σ (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)
|
||||
(--> (Σ (in-hole E (let ([x v]) M)))
|
||||
(Σ (in-hole E (subst M x v)))
|
||||
"let")
|
||||
#|
|
||||
;; BUG: this rule in place of the one above,
|
||||
;; plus no evaluation contexts of 'let'
|
||||
;; this bug is D because it only fails due to polymorphism -- subtle
|
||||
(--> (Σ (in-hole E (let ([x M]) N)))
|
||||
(Σ (in-hole E ((λ x N) M)))
|
||||
"let")
|
||||
|#
|
||||
|
||||
(--> (Σ (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)
|
||||
(--> (Σ (in-hole E (tl ((cons v_1) v_2))))
|
||||
(Σ (in-hole E v_2))
|
||||
"tl")
|
||||
(--> (in-hole E (hd nil))
|
||||
(--> (Σ (in-hole E (hd nil)))
|
||||
"error"
|
||||
"hd-err")
|
||||
(--> (in-hole E (tl nil))
|
||||
(--> (Σ (in-hole E (tl nil)))
|
||||
"error"
|
||||
"tl-err")
|
||||
(--> (in-hole E ((+ integer_1) integer_2))
|
||||
(in-hole E ,(+ (term integer_1) (term integer_2)))
|
||||
"+")))
|
||||
(--> (Σ (in-hole E ((+ integer_1) integer_2)))
|
||||
(Σ (in-hole E ,(+ (term integer_1) (term integer_2))))
|
||||
"+")
|
||||
(--> (Σ (in-hole E (new v)))
|
||||
((r v Σ) (in-hole E r))
|
||||
(fresh r)
|
||||
"ref")
|
||||
(--> (Σ (in-hole E ((set x) v)))
|
||||
((update-Σ Σ x v) (in-hole E (lookup-Σ Σ x)))
|
||||
"set")
|
||||
(--> (Σ (in-hole E (get x)))
|
||||
(Σ (in-hole E (lookup-Σ Σ x)))
|
||||
"get")))
|
||||
|
||||
(define-metafunction stlc
|
||||
subst : M x M -> M
|
||||
[(subst x x M_x)
|
||||
M_x]
|
||||
[(subst (λ x M) x M_x)
|
||||
(λ x M)]
|
||||
[(subst (let ([x M]) N) x M_x)
|
||||
(let ([x (subst M x M_x)]) N)]
|
||||
[(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 (let ([y N]) M) x M_x)
|
||||
(let ([x_new (subst N x M_x)]) (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-metafunction stlc
|
||||
lookup-Σ : Σ x -> v
|
||||
[(lookup-Σ (x v Σ) x) v]
|
||||
[(lookup-Σ (x v Σ) y) (lookup-Σ Σ y)])
|
||||
|
||||
(define-metafunction stlc
|
||||
update-Σ : Σ x v -> Σ
|
||||
[(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)]
|
||||
[(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))])
|
||||
|
||||
(define M? (redex-match stlc M))
|
||||
(define/contract (Eval M)
|
||||
(-> M? (or/c M? "error"))
|
||||
(-> M? (or/c "error" 'list 'λ 'ref number?))
|
||||
(define M-t (judgment-holds (typeof ,M τ) τ))
|
||||
(unless (pair? M-t)
|
||||
(error 'Eval "doesn't typecheck: ~s" M))
|
||||
(define res (apply-reduction-relation* red M))
|
||||
(define res (apply-reduction-relation* red (term (· ,M))))
|
||||
(unless (= 1 (length res))
|
||||
(error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
|
||||
(define ans (car res))
|
||||
(if (equal? "error" ans)
|
||||
"error"
|
||||
(let ([ans-t (judgment-holds (typeof ,ans τ) τ)])
|
||||
(unless (equal? M-t ans-t)
|
||||
(error 'Eval "internal error: type soundness fails for ~s" M))
|
||||
ans)))
|
||||
(match (car res)
|
||||
["error" "error"]
|
||||
[`(,Σ ,N)
|
||||
(define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ))
|
||||
(unless (equal? M-t ans-t)
|
||||
(error 'Eval "internal error: type soundness fails for ~s" M))
|
||||
(match N
|
||||
[(? x?) (cond
|
||||
[(term (in-dom? ,Σ ,N))
|
||||
'ref]
|
||||
[else
|
||||
(error 'Eval "internal error: reduced to a free variable ~s"
|
||||
M)])]
|
||||
[(or `((cons ,_) ,_) `nil) 'list]
|
||||
[(or `(λ ,_ ,_) `(cons ,_) `(set ,_) `(+ ,_)) 'λ]
|
||||
[(? number?) N]
|
||||
[_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])]))
|
||||
|
||||
(define-metafunction stlc
|
||||
subst : M x M -> M
|
||||
[(subst M x N)
|
||||
,(subst/proc x? (term (x)) (term (N)) (term M))])
|
||||
Σ->lets : Σ M -> M
|
||||
[(Σ->lets · M) M]
|
||||
[(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
|
||||
|
||||
(define/contract (type-check M)
|
||||
(-> M? (or/c τ? #f))
|
||||
|
|
@ -330,82 +439,48 @@ section in the paper.
|
|||
(define (progress-holds? M)
|
||||
(if (type-check M)
|
||||
(or (v? M)
|
||||
(not (null? (apply-reduction-relation red (term ,M)))))
|
||||
(not (null? (apply-reduction-relation red (term (· ,M))))))
|
||||
#t))
|
||||
|
||||
(define-metafunction stlc ;; LOC SKIP START
|
||||
[(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 (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 τ)
|
||||
(typeof · M τ)
|
||||
5)
|
||||
[`(typeof • ,M ,τ)
|
||||
[`(typeof · ,M ,τ)
|
||||
M]
|
||||
[#f #f]))
|
||||
|
||||
(define (typed-generator)
|
||||
(let ([g (redex-generator stlc
|
||||
(typeof • M τ)
|
||||
(typeof · M τ)
|
||||
5)])
|
||||
(λ ()
|
||||
(match (g)
|
||||
[`(typeof • ,M ,τ)
|
||||
[`(typeof · ,M ,τ)
|
||||
M]
|
||||
[#f #f]))))
|
||||
|
||||
(define (check term)
|
||||
(or (not term)
|
||||
(v? term)
|
||||
(let ([t-type (type-check term)])
|
||||
(define (check M)
|
||||
(or (not M)
|
||||
(v? M)
|
||||
(let ([t-type (type-check M)])
|
||||
(implies
|
||||
t-type
|
||||
(let ([red-res (apply-reduction-relation red term)])
|
||||
(let ([red-res (apply-reduction-relation red `(· ,M))])
|
||||
(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))))))))))
|
||||
(match red-t
|
||||
[`(,Σ ,N)
|
||||
(let ([red-type (type-check (term (Σ->lets ,Σ ,N)))])
|
||||
(consistent-with? t-type red-type))])))))))))
|
||||
|
||||
(define (generate-enum-term)
|
||||
'(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
||||
(generate-term stlc M #:i-th (pick-an-index 0.035)))
|
||||
|
||||
(define (ordered-enum-generator)
|
||||
(let ([index 0])
|
||||
|
|
@ -413,3 +488,5 @@ section in the paper.
|
|||
(begin0
|
||||
(generate-term stlc M #:i-th index)
|
||||
(set! index (add1 index))))))
|
||||
|
||||
;(time (redex-check stlc M (check (term M)) #:attempts 100000))
|
||||
|
|
@ -3,26 +3,6 @@
|
|||
(only-in "../stlc/tests-lib.rkt" consistent-with?)
|
||||
redex/reduction-semantics)
|
||||
|
||||
(test-equal (term (uses-bound-var? () 5))
|
||||
#f)
|
||||
(test-equal (term (uses-bound-var? () nil))
|
||||
#f)
|
||||
(test-equal (term (uses-bound-var? () (λ x x)))
|
||||
#t)
|
||||
(test-equal (term (uses-bound-var? () (λ x y)))
|
||||
#f)
|
||||
(test-equal (term (uses-bound-var? () ((λ x x) 5)))
|
||||
#t)
|
||||
(test-equal (term (uses-bound-var? () ((λ x xy) 5)))
|
||||
#f)
|
||||
|
||||
(test-equal (consistent-with? '(λ z1 (λ z2 z2))
|
||||
'(λ z (λ z1 z)))
|
||||
#f)
|
||||
(test-equal (consistent-with? '(λ z1 (λ z2 z2))
|
||||
'(λ z (λ z1 z1)))
|
||||
#t)
|
||||
|
||||
(test-equal (term (subst ((+ 1) 1) x 2))
|
||||
(term ((+ 1) 1)))
|
||||
(test-equal (term (subst ((+ x) x) x 2))
|
||||
|
|
@ -46,6 +26,19 @@
|
|||
(term (λ z (λ z1 z))))
|
||||
#t)
|
||||
|
||||
(test-equal (consistent-with? (term (subst (let ([y x]) x) x 2))
|
||||
(term (let ([y 2]) 2)))
|
||||
#t)
|
||||
(test-equal (consistent-with? (term (subst (let ([y x]) x) x (λ q z)))
|
||||
(term (let ([y (λ q z)]) (λ q z))))
|
||||
#t)
|
||||
(test-equal (consistent-with? (term (subst (let ([y x]) x) x (λ q y)))
|
||||
(term (let ([y (λ q y)]) (λ q y))))
|
||||
#t)
|
||||
(test-equal (consistent-with? (term (subst (let ([z 11]) (let ([z1 12]) z)) q 1))
|
||||
(term (let ([z 11]) (let ([z1 12]) z))))
|
||||
#t)
|
||||
|
||||
|
||||
|
||||
(test-equal (term (unify x int))
|
||||
|
|
@ -80,17 +73,20 @@
|
|||
(test-equal (judgment-holds (typeof 5 τ) τ)
|
||||
(list (term int)))
|
||||
(test-equal (judgment-holds (typeof nil τ) τ)
|
||||
(list (term (list int))))
|
||||
(list (term (list γ))))
|
||||
(test-equal (judgment-holds (typeof (cons 1) τ) τ)
|
||||
(list (term ((list int) → (list int)))))
|
||||
(test-equal (judgment-holds (typeof ((cons 1) nil) τ) τ)
|
||||
(list (term (list int))))
|
||||
(test-equal (judgment-holds (typeof (λ x x) τ) τ)
|
||||
(list (term (α → α))))
|
||||
(test-equal (judgment-holds (typeof (λ x (λ y x)) τ) τ)
|
||||
(list (term (α → (α1 → α)))))
|
||||
(test-equal (judgment-holds (typeof (λ f (λ x (f ((+ x) 1)))) τ) τ)
|
||||
(list (term ((int → β) → (int → β)))))
|
||||
(test-equal (consistent-with? (judgment-holds (typeof (λ x x) τ) τ)
|
||||
(list (term (α → α))))
|
||||
#t)
|
||||
(test-equal (consistent-with? (judgment-holds (typeof (λ x (λ y x)) τ) τ)
|
||||
(list (term (α → (α1 → α)))))
|
||||
#t)
|
||||
(test-equal (consistent-with? (judgment-holds (typeof (λ f (λ x (f ((+ x) 1)))) τ) τ)
|
||||
(list (term ((int → α) → (int → α)))))
|
||||
#t)
|
||||
(test-equal (judgment-holds (typeof (λ f (λ x ((+ (f ((+ x) 1))) 2))) τ) τ)
|
||||
(list (term ((int → int) → (int → int)))))
|
||||
(test-equal (judgment-holds (typeof (λ f (λ x ((+ x) (f 1)))) τ) τ)
|
||||
|
|
@ -99,75 +95,99 @@
|
|||
(list))
|
||||
(test-equal (judgment-holds (typeof ((+ ((+ 1) 2)) ((+ 3) 4)) τ) τ)
|
||||
(list (term int)))
|
||||
|
||||
(test-->> red (term ((λ x x) 7)) (term 7))
|
||||
(test-->> red (term (((λ x (λ x x)) 2) 1)) (term 1))
|
||||
(test-->> red (term (((λ x (λ y x)) 2) 1)) (term 2))
|
||||
(test-->> red
|
||||
(term ((λ x ((cons x) nil)) 11))
|
||||
(term ((cons 11) nil)))
|
||||
(test-->> red
|
||||
(term ((λ x ((cons x) nil)) 11))
|
||||
(term ((cons 11) nil)))
|
||||
(test-->> red
|
||||
(term ((cons ((λ x x) 11)) nil))
|
||||
(term ((cons 11) nil)))
|
||||
(test-->> red
|
||||
(term (cons ((λ x x) 1)))
|
||||
(term (cons 1)))
|
||||
(test-->> red
|
||||
(term ((cons ((λ x x) 1)) nil))
|
||||
(term ((cons 1) nil)))
|
||||
(test-->> red
|
||||
(term (hd ((λ x ((cons x) nil)) 11)))
|
||||
(term 11))
|
||||
(test-->> red
|
||||
(term (tl ((λ x ((cons x) nil)) 11)))
|
||||
(term nil))
|
||||
(test-->> red
|
||||
(term (tl nil))
|
||||
"error")
|
||||
(test-->> red
|
||||
(term (hd nil))
|
||||
"error")
|
||||
(test-->> red
|
||||
(term ((+ 1) (hd nil)))
|
||||
"error")
|
||||
(test-->> red
|
||||
(term ((+ ((+ 1) 2)) ((+ 3) 4)))
|
||||
(term 10))
|
||||
(test-->> red
|
||||
(term ((λ f (f 3)) (cons 1)))
|
||||
(term ((cons 1) 3)))
|
||||
(test-->> red
|
||||
(term ((λ f (f 3)) (+ 1)))
|
||||
(term 4))
|
||||
|
||||
(test-equal (Eval (term ((λ x x) 3)))
|
||||
(term 3))
|
||||
|
||||
(test-equal (reduction-step-count (term (λ x x)))
|
||||
0)
|
||||
(test-equal (reduction-step-count (term ((λ x x) 1)))
|
||||
1)
|
||||
(test-equal (reduction-step-count (term ((λ x x) 1)))
|
||||
1)
|
||||
(test-equal (reduction-step-count (term ((cons 1) nil)))
|
||||
0)
|
||||
(test-equal (reduction-step-count (term (hd ((cons 1) nil))))
|
||||
1)
|
||||
(test-equal (reduction-step-count (term (hd nil)))
|
||||
1)
|
||||
(test-equal (reduction-step-count (term ((λ x x) (hd ((cons 1) nil)))))
|
||||
2)
|
||||
|
||||
(test-equal (type-check (term 5))
|
||||
(term int))
|
||||
(test-equal (type-check (term (5 5)))
|
||||
#f)
|
||||
|
||||
(test-equal (judgment-holds (typeof ((cons ((cons 1) nil)) nil) τ) τ)
|
||||
(list (term (list (list int)))))
|
||||
(test-equal (judgment-holds (typeof ((cons nil) nil) τ) τ)
|
||||
(list (term (list (list γ1)))))
|
||||
(test-equal (judgment-holds (typeof ((set (new 1)) 2) τ) τ)
|
||||
(list (term int)))
|
||||
(test-equal (judgment-holds (typeof (get (new 1)) τ) τ)
|
||||
(list (term int)))
|
||||
(test-equal (judgment-holds (typeof (let ([id (λ y y)])
|
||||
((id id) 1))
|
||||
τ)
|
||||
τ)
|
||||
(list (term int)))
|
||||
(test-equal (judgment-holds (typeof (let ([r (new nil)])
|
||||
(let ([n ((set r) ((cons 5) nil))])
|
||||
((hd (get r)) 1)))
|
||||
τ)
|
||||
τ)
|
||||
(list))
|
||||
|
||||
(test-->> red (term (· ((λ x x) 7))) (term (· 7)))
|
||||
(test-->> red (term (· (((λ x (λ x x)) 2) 1))) (term (· 1)))
|
||||
(test-->> red (term (· (((λ x (λ y x)) 2) 1))) (term (· 2)))
|
||||
(test-->> red
|
||||
(term (· ((λ x ((cons x) nil)) 11)))
|
||||
(term (· ((cons 11) nil))))
|
||||
(test-->> red
|
||||
(term (· ((λ x ((cons x) nil)) 11)))
|
||||
(term (· ((cons 11) nil))))
|
||||
(test-->> red
|
||||
(term (· ((cons ((λ x x) 11)) nil)))
|
||||
(term (· ((cons 11) nil))))
|
||||
(test-->> red
|
||||
(term (· (cons ((λ x x) 1))))
|
||||
(term (· (cons 1))))
|
||||
(test-->> red
|
||||
(term (· ((cons ((λ x x) 1)) nil)))
|
||||
(term (· ((cons 1) nil))))
|
||||
(test-->> red
|
||||
(term (· (hd ((λ x ((cons x) nil)) 11))))
|
||||
(term (· 11)))
|
||||
(test-->> red
|
||||
(term (· (tl ((λ x ((cons x) nil)) 11))))
|
||||
(term (· nil)))
|
||||
(test-->> red
|
||||
(term (· (tl nil)))
|
||||
"error")
|
||||
(test-->> red
|
||||
(term (· (hd nil)))
|
||||
"error")
|
||||
(test-->> red
|
||||
(term (· ((+ 1) (hd nil))))
|
||||
"error")
|
||||
(test-->> red
|
||||
(term (· ((+ ((+ 1) 2)) ((+ 3) 4))))
|
||||
(term (· 10)))
|
||||
(test-->> red
|
||||
(term (· ((λ f (f 3)) (cons 1))))
|
||||
(term (· ((cons 1) 3))))
|
||||
(test-->> red
|
||||
(term (· ((λ f (f 3)) (+ 1))))
|
||||
(term (· 4)))
|
||||
(test-->> red
|
||||
(term (· (let ([f (+ 2)]) ((+ (f 3)) (f 4)))))
|
||||
(term (· 11)))
|
||||
(test-->> red
|
||||
(term (· (get (new 1))))
|
||||
(term ((r 1 ·) 1)))
|
||||
(test-->> red
|
||||
(term (· ((set (new 1)) 2)))
|
||||
(term ((r 2 ·) 1)))
|
||||
(test-->> red
|
||||
#:equiv consistent-with?
|
||||
(term (· (let ([r (new 1)])
|
||||
(let ([o ((set r) 2)])
|
||||
(get r)))))
|
||||
(term ((r 2 ·) 2)))
|
||||
(test-->> red
|
||||
#:equiv consistent-with?
|
||||
(term (· (let ([r (new nil)])
|
||||
(let ([n ((set r) ((cons 5) nil))])
|
||||
((hd (get r)) 1)))))
|
||||
(term ((r ((cons 5) nil) ·) (5 1))))
|
||||
|
||||
(test-equal (Eval (term ((λ x x) 3)))
|
||||
3)
|
||||
(test-equal (Eval (term ((cons 1) nil)))
|
||||
'list)
|
||||
(test-equal (Eval (term (cons 1)))
|
||||
'λ)
|
||||
(test-equal (Eval (term (λ x x)))
|
||||
'λ)
|
||||
(test-equal (type-check (term 5))
|
||||
(term int))
|
||||
(test-equal (type-check (term (5 5)))
|
||||
#f)
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user