From bfe5fbfe0000ef3eaf4c5844e9236961a5a6d352 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Tue, 26 May 2015 18:04:49 -0400 Subject: [PATCH] add stlc+box --- tapl/stlc+box.rkt | 38 +++++++ tapl/stlc+cons.rkt | 3 +- tapl/tests/stlc+box.rkt | 214 ++++++++++++++++++++++++++++++++++++++++ tapl/typecheck.rkt | 18 +++- 4 files changed, 270 insertions(+), 3 deletions(-) create mode 100644 tapl/stlc+box.rkt create mode 100644 tapl/tests/stlc+box.rkt diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt new file mode 100644 index 0000000..cbf2a5a --- /dev/null +++ b/tapl/stlc+box.rkt @@ -0,0 +1,38 @@ +#lang racket/base +(require + (for-syntax racket/base syntax/parse syntax/stx racket/syntax racket/string + "stx-utils.rkt" "typecheck.rkt") + (for-meta 2 racket/base syntax/parse racket/syntax) + "typecheck.rkt") +(require (prefix-in stlc: (only-in "stlc+cons.rkt" #%app λ)) + (except-in "stlc+cons.rkt" #%app λ)) +(provide (rename-out [stlc:#%app #%app] [stlc:λ λ])) +(provide (all-from-out "stlc+cons.rkt")) +(provide ref deref :=) + +;; Simply-Typed Lambda Calculus, plus mutable references +;; Types: +;; - types from stlc+cons.rkt +;; - Ref constructor +;; Terms: +;; - terms from stlc+cons.rkt + +(define-type-constructor Ref) + +(define-syntax (ref stx) + (syntax-parse stx + [(_ e) + #:with (e- τ) (infer+erase #'e) + (⊢ #'(box e-) #'(Ref τ))])) +(define-syntax (deref stx) + (syntax-parse stx + [(_ e) + #:with (e- ((~literal Ref) τ)) (infer+erase #'e) + (⊢ #'(unbox e-) #'τ)])) +(define-syntax (:= stx) + (syntax-parse stx + [(_ e_ref e) + #:with (e_ref- ((~literal Ref) τ1)) (infer+erase #'e_ref) + #:with (e- τ2) (infer+erase #'e) + #:when (τ= #'τ1 #'τ2) + (⊢ #'(set-box! e_ref- e-) #'Unit)])) \ No newline at end of file diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt index 77f3b1a..c04dc55 100644 --- a/tapl/stlc+cons.rkt +++ b/tapl/stlc+cons.rkt @@ -14,9 +14,10 @@ ;; Simply-Typed Lambda Calculus, plus cons ;; Types: ;; - types from stlc+var.rkt +;; - List constructor ;; Terms: ;; - terms from stlc+var.rkt -;; - define constants only +;; - define, constants only ;; TODO: enable HO use of list primitives diff --git a/tapl/tests/stlc+box.rkt b/tapl/tests/stlc+box.rkt new file mode 100644 index 0000000..1cf2132 --- /dev/null +++ b/tapl/tests/stlc+box.rkt @@ -0,0 +1,214 @@ +#lang s-exp "../stlc+box.rkt" +(require "rackunit-typechecking.rkt") + +(define x (ref 10)) +(check-type x : (Ref Int)) +(check-type (deref x) : Int ⇒ 10) +(check-type (:= x 20) : Unit) ; x still 10 because check-type does not evaluate +(check-type (begin (:= x 20) (deref x)) : Int ⇒ 20) +(check-type x : (Ref Int)) +(check-type (deref (ref 20)) : Int ⇒ 20) +(check-type (deref x) : Int ⇒ 20) + +(check-type ((λ ([b : (Ref Int)]) (deref b)) (ref 10)) : Int ⇒ 10) +(check-type ((λ ([b : (Ref Int)]) (begin (begin (:= b 20) (deref b)))) (ref 10)) : Int ⇒ 20) + +;; previous tests: ------------------------------------------------------------ +(typecheck-fail (cons 1 2)) +(typecheck-fail (cons 1 nil)) +(check-type (cons 1 (nil {Int})) : (List Int)) +(typecheck-fail nil) +(typecheck-fail (nil Int)) +(typecheck-fail (nil (Int))) +; passes bc ⇒-rhs is only used for its runtime value +(check-type (nil {Int}) : (List Int) ⇒ (nil {Bool})) +(check-not-type (nil {Bool}) : (List Int)) +(check-type (nil {Bool}) : (List Bool)) +(check-type (nil {(→ Int Int)}) : (List (→ Int Int))) +(define fn-lst (cons (λ ([x : Int]) (+ 10 x)) (nil {(→ Int Int)}))) +(check-type fn-lst : (List (→ Int Int))) +(check-type (isnil fn-lst) : Bool ⇒ #f) +(typecheck-fail (isnil (head fn-lst))) ; head lst is not List +(check-type (isnil (tail fn-lst)) : Bool ⇒ #t) +(check-type (head fn-lst) : (→ Int Int)) +(check-type ((head fn-lst) 25) : Int ⇒ 35) +(check-type (tail fn-lst) : (List (→ Int Int)) ⇒ (nil {(→ Int Int)})) + +;; previous tests: ------------------------------------------------------------ +;; define-type-alias +(define-type-alias Integer Int) +(define-type-alias ArithBinOp (→ Int Int Int)) + +(check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer) +(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int) +(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Integer) +(check-type + : ArithBinOp) +(check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int)) + +;; records (ie labeled tuples) +(check-type "Stephen" : String) +(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× ["name" String] ["phone" Int] ["male?" Bool])) +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") + : String ⇒ "Stephen") +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") + : String ⇒ "Stephen") +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone") + : Int ⇒ 781) +(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?") + : Bool ⇒ #t) +(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× ["my-name" String] ["phone" Int] ["male?" Bool])) +(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× ["name" String] ["my-phone" Int] ["male?" Bool])) +(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : + (× ["name" String] ["phone" Int] ["is-male?" Bool])) + + +(check-type (var "coffee" = (void) as (∨ ["coffee" Unit])) : (∨ ["coffee" Unit])) +(check-not-type (var "coffee" = (void) as (∨ ["coffee" Unit])) : (∨ ["coffee" Unit] ["tea" Unit])) +(typecheck-fail ((λ ([x : (∨ ["coffee" Unit] ["tea" Unit])]) x) + (var "coffee" = (void) as (∨ ["coffee" Unit])))) +(check-type (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit])) : (∨ ["coffee" Unit] ["tea" Unit])) +(check-type (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit] ["coke" Unit])) + : (∨ ["coffee" Unit] ["tea" Unit] ["coke" Unit])) + +(typecheck-fail + (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit])) + ["coffee" x => 1])) ; not enough clauses +(typecheck-fail + (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit])) + ["coffee" x => 1] + ["teaaaaaa" x => 2])) ; wrong clause +(typecheck-fail + (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit])) + ["coffee" x => 1] + ["tea" x => 2] + ["coke" x => 3])) ; too many clauses +(typecheck-fail + (case (var "coffee" = (void) as (∨ ["coffee" Unit] ["tea" Unit])) + ["coffee" x => "1"] + ["tea" x => 2])) ; mismatched branch types +(check-type + (case (var "coffee" = 1 as (∨ ["coffee" Int] ["tea" Unit])) + ["coffee" x => x] + ["tea" x => 2]) : Int ⇒ 1) +(define-type-alias Drink (∨ ["coffee" Int] ["tea" Unit] ["coke" Bool])) +(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) +(check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int)) +(check-type + (case ((λ ([d : Drink]) d) + (var "coffee" = 1 as (∨ ["coffee" Int] ["tea" Unit] ["coke" Bool]))) + ["coffee" x => (+ (+ x x) (+ x x))] + ["tea" x => 2] + ["coke" y => 3]) + : Int ⇒ 4) + +(check-type + (case ((λ ([d : Drink]) d) (var "coffee" = 1 as Drink)) + ["coffee" x => (+ (+ x x) (+ x x))] + ["tea" x => 2] + ["coke" y => 3]) + : Int ⇒ 4) + +;; previous tests: ------------------------------------------------------------ +;; tests for tuples ----------------------------------------------------------- +(check-type (tup 1 2 3) : (× Int Int Int)) +(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int))) +(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int))) +(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int))) +(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int))) +(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit))) + +(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1) +(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2") +(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f) +(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large +(typecheck-fail (proj 1 2)) ; not tuple + +;; ext-stlc.rkt tests --------------------------------------------------------- +;; should still pass + +;; new literals and base types +(check-type "one" : String) ; literal now supported +(check-type #f : Bool) ; literal now supported + +(check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type + +;; Unit +(check-type (void) : Unit) +(check-type void : (→ Unit)) +(typecheck-fail ((λ ([x : Unit]) x) 2)) +(typecheck-fail ((λ ([x : Unit])) void)) +(check-type ((λ ([x : Unit]) x) (void)) : Unit) + +;; begin +(typecheck-fail (begin)) +(check-type (begin 1) : Int) +(typecheck-fail (begin 1 2 3)) +(check-type (begin (void) 1) : Int ⇒ 1) + +;;ascription +(typecheck-fail (ann 1 : Bool)) +(check-type (ann 1 : Int) : Int ⇒ 1) +(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10) + +; let +(check-type (let () (+ 1 1)) : Int ⇒ 2) +(check-type (let ([x 10]) (+ 1 2)) : Int) +(typecheck-fail (let ([x #f]) (+ x 1))) +(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30) +(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier + +(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21) +(typecheck-fail (let* ([x #t] [y (+ x 1)]) 1)) + +; letrec +(typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y)) +(typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x)) + +(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3) + +;; recursive +(check-type + (letrec ([(countdown : (→ Int String)) + (λ ([i : Int]) + (if (= i 0) + "liftoff" + (countdown (- i 1))))]) + (countdown 10)) : String ⇒ "liftoff") + +;; mutually recursive +(check-type + (letrec ([(is-even? : (→ Int Bool)) + (λ ([n : Int]) + (or (zero? n) + (is-odd? (sub1 n))))] + [(is-odd? : (→ Int Bool)) + (λ ([n : Int]) + (and (not (zero? n)) + (is-even? (sub1 n))))]) + (is-odd? 11)) : Bool ⇒ #t) + +;; tests from stlc+lit-tests.rkt -------------------------- +; most should pass, some failing may now pass due to added types/forms +(check-type 1 : Int) +;(check-not-type 1 : (Int → Int)) +;(typecheck-fail "one") ; literal now supported +;(typecheck-fail #f) ; literal now supported +(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) +(check-not-type (λ ([x : Int]) x) : Int) +(check-type (λ ([x : Int]) x) : (→ Int Int)) +(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) +(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) +(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool now valid type, but arg has wrong type +;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type +(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type +(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + : (→ (→ Int Int Int) Int Int Int)) +(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3) +(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int +(typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int +(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args +(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) + diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index eafeb9e..3e36616 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -90,11 +90,25 @@ #:with (x ...) #'(b.x ...) #:with (τ ...) #'(b.τ ...) #:with - (lam xs+ (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2 e+))) + ;; if e is (begin e1 ...), (e1 ...) will be spliced into expanded λ + ;; (and begin will be dropped), so must handle that + (lam xs+ (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2 e_body+ ... e+))) (expand/df #`(λ (x ...) (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...) #,e))) - (list #'xs+ #'e+ (typeof #'e+))] +; #:with tmp +; (expand/df +; #`(λ (x ...) +; (let-syntax ([x (make-rename-transformer (⊢ #'x #'τ))] ...) #,e))) +; #:when (printf "~a\n" (syntax->datum #'tmp)) +; #:with (lam xs+ (lr-stxs+vs1 stxs1 vs1 (lr-stxs+vs2 stxs2 vs2 e+))) #'tmp + + ;; if e is (begin ...), types (ie syntax properties) of all begins + ;; will be accumulated on e+, so only get the first type + #:with τ_e (if (null? (syntax->list #'(e_body+ ...))) + (typeof #'e+) + (stx-car (typeof #'e+))) + (list #'xs+ #'(begin e_body+ ... e+) #'τ_e)] [([x τ] ...) (infer/type-ctxt+erase #'([x : τ] ...) e)])) ; all xs are bound in the same scope (define (infers/type-ctxt+erase ctxt es)