add stlc+box

This commit is contained in:
Stephen Chang 2015-05-26 18:04:49 -04:00
parent 3ebd1aba5f
commit bfe5fbfe00
4 changed files with 270 additions and 3 deletions

38
tapl/stlc+box.rkt Normal file
View File

@ -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)]))

View File

@ -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

214
tapl/tests/stlc+box.rkt Normal file
View File

@ -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)

View File

@ -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)