From 468cf075d6f62d1e3fdefafde1bdac51585334e7 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Fri, 4 Mar 2016 16:13:12 -0500 Subject: [PATCH] mlish: add vectors, sequences, and iteration - add ary and ack test - fix bug in uparrow-s (in typecheck.rkt) extra #' --- tapl/mlish.rkt | 87 +++++++++++++++++++++++++++++--- tapl/stlc+sub.rkt | 5 +- tapl/tests/mlish-tests.rkt | 1 - tapl/tests/mlish/ack.mlish | 24 +++++++++ tapl/tests/mlish/ary.mlish | 20 ++++++++ tapl/tests/mlish/chameneos.mlish | 3 ++ tapl/tests/stlc+sub-tests.rkt | 8 +-- tapl/typecheck.rkt | 7 +-- 8 files changed, 139 insertions(+), 16 deletions(-) create mode 100644 tapl/tests/mlish/ack.mlish create mode 100644 tapl/tests/mlish/ary.mlish diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt index adc9af1..d50b742 100644 --- 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 index 8910e43..47346bc 100644 --- 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 index 6a04ce6..f860053 100644 --- 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 new file mode 100644 index 0000000..8d8526b --- /dev/null +++ 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 new file mode 100644 index 0000000..4601751 --- /dev/null +++ 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 index 2688477..2ae8df3 100644 --- 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 index 1c6e534..752ed5c 100644 --- 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 index 009a1cd..142c4f2 100644 --- 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 (... ...)))