commit 468cf075d6f62d1e3fdefafde1bdac51585334e7
parent 1ad357b55e6f237bd93b2e2622b6fd99ada1d926
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 4 Mar 2016 16:13:12 -0500
mlish: add vectors, sequences, and iteration
- add ary and ack test
- fix bug in uparrow-s (in typecheck.rkt) extra #'
Diffstat:
8 files changed, 139 insertions(+), 16 deletions(-)
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -396,6 +396,21 @@
(mk-app-err-msg stx #:given #'(τ_arg ...) #:expected #'(τ_in ...))
(⊢ (#%app e_fn- e_arg- ...) : τ_out)])
+;; cond
+(define-typed-syntax cond
+ [(_ [(~and test (~not (~datum else))) body] ...
+ (~optional [(~and (~datum else) (~parse else_test #'(ext-stlc:#%datum . #t))) else_body]
+ #:defaults ([else_test #'#f])))
+ #:with (test- ...) (⇑s (test ...) as Bool)
+ #:with ([body- ty_body] ...) (infers+erase #'(body ...))
+ #:when (same-types? #'(ty_body ...))
+ #:with τ_out (stx-car #'(ty_body ...))
+ #:with [last-body- last-ty] (if (attribute else_body)
+ (infer+erase #'else_body)
+ (infer+erase #'(void)))
+ #:when (or (not (attribute else_body))
+ (typecheck? #'last-ty #'τ_out))
+ (⊢ (cond [test- body-] ... [else_test last-body-]) : τ_out)])
;; sync channels
(define-type-constructor Channel)
@@ -411,7 +426,9 @@
[(_ c v)
#:with (c- (ty)) (⇑ c as Channel)
#:with [v- ty_v] (infer+erase #'v)
- #:when (typechecks? #'ty_v #'ty)
+ #:fail-unless (typechecks? #'ty_v #'ty)
+ (format "Cannot send ~a value on ~a channel."
+ (type->str #'ty_v) (type->str #'ty))
(⊢ (channel-put c- v-) : Unit)])
(define-base-type Thread)
@@ -425,12 +442,70 @@
(define-base-type Char)
(define-primop random : (→ Int Int))
(define-primop integer->char : (→ Int Char))
+(define-primop string->number : (→ String Int))
(define-primop string : (→ Char String))
(define-primop sleep : (→ Int Unit))
(define-primop string=? : (→ String String Bool))
-#;(define-typed-syntax rand
- [(_ k)
- #:with [k- ty] (infer+erase #'k)
- #:when (typecheck? #'ty #'Int)
- (⊢ (thread k-) : Int)])
+;; vectors
+(define-type-constructor Vector)
+
+(define-typed-syntax vector
+ [(_ (~and tys {ty}))
+ #:when (brace? #'tys)
+ (⊢ (vector) : (Vector ty))]
+ [(_ v ...)
+ #:with ([v- ty] ...) (infers+erase #'(v ...))
+ #:when (same-types? #'(ty ...))
+ #:with one-ty (stx-car #'(ty ...))
+ (⊢ (vector v- ...) : (Vector one-ty))])
+(define-typed-syntax make-vector
+ [(_ n e)
+ #:with n- (⇑ n as Int)
+ #:with [e- ty] (infer+erase #'e)
+ (⊢ (make-vector n- e-) : (Vector ty))])
+(define-typed-syntax vector-length
+ [(_ e)
+ #:with [e- _] (⇑ e as Vector)
+ (⊢ (vector-length e-) : Int)])
+(define-typed-syntax vector-ref
+ [(_ e n)
+ #:with n- (⇑ n as Int)
+ #:with [e- (ty)] (⇑ e as Vector)
+ (⊢ (vector-ref e- n-) : ty)])
+(define-typed-syntax vector-set!
+ [(_ e n v)
+ #:with n- (⇑ n as Int)
+ #:with [e- (ty)] (⇑ e as Vector)
+ #:with [v- ty_v] (infer+erase #'v)
+ #:when (typecheck? #'ty_v #'ty)
+ (⊢ (vector-set! e- n- v-) : Unit)])
+
+;; sequences and for loops
+
+(define-type-constructor Sequence)
+
+(define-typed-syntax in-range/tc #:export-as in-range
+ [(_ end)
+ #'(in-range/tc (ext-stlc:#%datum . 0) end (ext-stlc:#%datum . 1))]
+ [(_ start end)
+ #'(in-range/tc stat end (ext-stlc:#%datum . 1))]
+ [(_ start end step)
+ #:with (e- ...) (⇑s (start end step) as Int)
+ (⊢ (in-range e- ...) : (Sequence Int))])
+(define-typed-syntax for
+ [(_ ([x:id e]...) body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
+ (⊢ (for ([x- e-] ...) body-) : Unit)])
+(define-typed-syntax for*
+ [(_ ([x:id e]...) body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
+ (⊢ (for* ([x- e-] ...) body-) : Unit)])
+
+(define-typed-syntax printf
+ [(_ str e ...)
+ #:with s- (⇑ str as String)
+ #:with ([e- ty] ...) (infers+erase #'(e ...))
+ (⊢ (printf s- e- ...) : Unit)])
diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
@@ -1,6 +1,7 @@
#lang s-exp "typecheck.rkt"
(extends "stlc+lit.rkt" #:except #%datum +)
-(reuse add1 #:from "ext-stlc.rkt")
+(reuse Bool String add1 #:from "ext-stlc.rkt")
+(require (prefix-in ext: (only-in "ext-stlc.rkt" #%datum)))
(provide (for-syntax subs? current-sub?))
;; Simply-Typed Lambda Calculus, plus subtyping
@@ -29,7 +30,7 @@
[(_ . n:nat) (⊢ (#%datum . n) : Nat)]
[(_ . n:integer) (⊢ (#%datum . n) : Int)]
[(_ . n:number) (⊢ (#%datum . n) : Num)]
- [(_ . x) #'(stlc+lit:#%datum . x)])
+ [(_ . x) #'(ext:#%datum . x)])
(begin-for-syntax
(define (sub? t1 t2)
diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt
@@ -40,7 +40,6 @@
[Cons x xs -> 1])
#:with-msg "match: clauses not exhaustive; missing: Nil")
-
(define (g2 [lst : (List Y)] → (List Y)) lst)
(check-type g2 : (→ (List Y) (List Y)))
(typecheck-fail (g2 1)
diff --git a/tapl/tests/mlish/ack.mlish b/tapl/tests/mlish/ack.mlish
@@ -0,0 +1,24 @@
+#lang s-exp "../../mlish.rkt"
+(require "../rackunit-typechecking.rkt")
+
+;; tests cond with else
+
+(define (ack/else [m : Int] [n : Int] -> Int)
+ (cond [(zero? m) (add1 n)]
+ [(zero? n) (ack/else (sub1 m) 1)]
+ [else (ack/else (sub1 m) (ack/else m (sub1 n)))]))
+
+(check-type (ack/else 0 0) : Int -> 1)
+(check-type (ack/else 1 1) : Int -> 3)
+(check-type (ack/else 2 2) : Int -> 7)
+(check-type (ack/else 3 4) : Int -> 125)
+
+(define (ack [m : Int] [n : Int] -> Int)
+ (cond [(zero? m) (add1 n)]
+ [(zero? n) (ack (sub1 m) 1)]
+ [#t (ack (sub1 m) (ack m (sub1 n)))]))
+
+(check-type (ack 0 0) : Int -> 1)
+(check-type (ack 1 1) : Int -> 3)
+(check-type (ack 2 2) : Int -> 7)
+(check-type (ack 3 4) : Int -> 125)
diff --git a/tapl/tests/mlish/ary.mlish b/tapl/tests/mlish/ary.mlish
@@ -0,0 +1,20 @@
+#lang s-exp "../../mlish.rkt"
+(require "../rackunit-typechecking.rkt")
+
+;; test vectors and for loops
+(define (main [args : (Vector String)] -> (× Int Int))
+ (let* ([n (if (zero? (vector-length args))
+ 1
+ (string->number (vector-ref args 0)))]
+ [x (make-vector n 0)]
+ [y (make-vector n 0)]
+ [last (sub1 n)])
+ (begin
+ (for ([i (in-range n)]) (vector-set! x i (add1 i)))
+ (for* ([k (in-range 1000)][i (in-range last -1 -1)])
+ (vector-set! y i (+ (vector-ref x i) (vector-ref y i))))
+ (tup (vector-ref y 0) (vector-ref y last)))))
+
+(check-type (main (vector "100")) : (× Int Int) -> (tup 1000 100000))
+(check-type (main (vector "1000")) : (× Int Int) -> (tup 1000 1000000))
+(check-type (main (vector "10000")) : (× Int Int) -> (tup 1000 10000000))
diff --git a/tapl/tests/mlish/chameneos.mlish b/tapl/tests/mlish/chameneos.mlish
@@ -10,6 +10,9 @@
(define-type-alias MeetChan (Channel Meet))
(define-type-alias ResultChan (Channel Result))
+(typecheck-fail (channel-put (make-channel {Bool}) 1)
+ #:with-msg "Cannot send Int value on Bool channel")
+
(define (change [c1 : Color] [c2 : Color] -> Color)
(match c1 with
[Red ->
diff --git a/tapl/tests/stlc+sub-tests.rkt b/tapl/tests/stlc+sub-tests.rkt
@@ -38,15 +38,15 @@
;; some change due to more specific types
(check-type 1 : Int)
(check-not-type 1 : (→ Int Int))
-(typecheck-fail "one") ; unsupported literal
-(typecheck-fail #f) ; unsupported literal
+(check-type "one" : String)
+(check-type #f : Bool)
(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 is not valid type
-(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
+(typecheck-fail ((λ ([x : Sym]) x) 1)) ; Sym is not valid type
+(typecheck-fail (λ ([x : Sym]) x)) ; Sym is not 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))
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -114,8 +114,9 @@
#`(begin
(require (rename-in (only-in base-lang x ... old ...) [old new] ...))
(provide (filtered-out
- (let ([excluded (map (compose symbol->string syntax->datum) (syntax->list #'(new ...)))])
- (λ (n) (and (not (member n excluded)) n)))
+ (let* ([excluded (map (compose symbol->string syntax->datum) (syntax->list #'(new ...)))])
+ (λ (name)
+ (and (not (member name excluded)) name)))
(all-from-out base-lang))))]))
(define-syntax add-expected
@@ -234,7 +235,7 @@
[(τ-expander . args) #`(#,e #'args)])
e)
(syntax-parse t
- [(τ-expander . args) #`(#,e #'args)]
+ [(τ-expander . args) #`(#,e args)]
[_ e]))
#'(e- (... ...))
#'(τ_e (... ...)))
