commit a12e85d4bc691b5ba7572915895543a61c7f3f6d
parent b687cffb0a4c52580d7b81cba6834a7314bbc3f7
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 31 Jul 2015 17:33:45 -0400
fix type constructor pattern matching and extraction
- tests passing up to stlc+reco+var tup and proj (not but variants)
Diffstat:
9 files changed, 280 insertions(+), 191 deletions(-)
diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
@@ -78,7 +78,7 @@
(define-syntax (begin/tc stx)
(syntax-parse stx
[(_ e_unit ... e)
- #:with ((e_unit- τ_unit) ...) (infers+erase #'(e_unit ...))
+ #:with ([e_unit- τ_unit] ...) (infers+erase #'(e_unit ...))
#:with (e- τ) (infer+erase #'e)
#:fail-unless (stx-andmap Unit? #'(τ_unit ...))
(string-append
diff --git a/tapl/notes.txt b/tapl/notes.txt
@@ -1,3 +1,21 @@
+2015-07-31
+Problem: pattern-expander not being recognized
+Solution: syntax-parse pattern directives must begin with ~ prefix
+
+2015-07-30:
+Problem: How to match against an "expanded" type when I have an unexpanded pat?
+- use the 'orig syntax?
+ - this would probably work but now 'orig is used for more than debugging/msgs
+ - so dont do this
+ - also, wont work because you're only matching part of the type
+- use pattern expanders!
+ - a declared literal in define-type-constructor is defined as *both*:
+ - and macro that applies a temporary id (defined as void)
+ - a pattern-expander that expands into the expanded form:
+ ((~literal #%plain-app) (~literal tmp-id) . args)
+
+Note to self: when getting weird macro pattern matching errors, always check if you're accidentally using a pattern variable!
+
2015-07-28
Problem: How to handle mixed types, ie combining expanded and unexpanded types.
Problem: When to eval, ie expand, types into canonical form
diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt
@@ -1,13 +1,13 @@
#lang racket/base
(require "typecheck.rkt")
(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin tup proj let type=?))
- (except-in "stlc+tup.rkt" #%app begin tup proj let type=?))
+ (except-in "stlc+tup.rkt" #%app begin tup proj let type=? ×))
(provide (rename-out [stlc:#%app #%app] [stlc:let let] [stlc:begin begin]
[define/tc define]))
(provide (except-out (all-from-out "stlc+tup.rkt")
stlc:#%app stlc:let stlc:begin stlc:tup stlc:proj
(for-syntax stlc:type=?)))
-(provide tup proj var case)
+(provide tup proj); var case)
(provide (for-syntax type=?))
@@ -30,44 +30,65 @@
; extend to:
; 1) accept strings (ie, record labels)
(define (type=? τ1 τ2)
+; (printf "t1 = ~a\n" (syntax->datum τ1))
+; (printf "t2 = ~a\n" (syntax->datum τ2))
(syntax-parse (list τ1 τ2)
[(s1:str s2:str) (string=? (syntax-e #'s1) (syntax-e #'s2))]
[_ (stlc:type=? τ1 τ2)]))
(current-type=? type=?)
- (current-typecheck-relation (current-type=?)))
+ (current-typecheck-relation (current-type=?))
+
+ (define (same-types? τs)
+ (define τs-lst (syntax->list τs))
+ (or (null? τs-lst)
+ (andmap (λ (τ) ((current-type=?) (car τs-lst) τ)) (cdr τs-lst)))))
(provide define-type-alias)
(define-syntax define-type-alias
(syntax-parser
[(_ alias:id τ:type)
; must eval, otherwise undefined types will be allowed
- #'(define-syntax alias (syntax-parser [x:id #'τ.norm]))]))
+ ;#'(define-syntax alias (syntax-parser [x:id #'τ.norm]))]))
+ #'(define-syntax alias (syntax-parser [x:id #'τ]))]))
+
+;(define-type-constructor [: str τ] #:lits (:))
-(define-type-constructor : #:arity 2)
+; re-define tuples as records
+(define-type-constructor
+ (× [~$ label τ_fld] ...) #:lits (~$)
+ #:declare label str
+ #:declare τ_fld type
+ )
+; (× τ ...)
+; #:declare τ type)
;; records
(define-syntax (tup stx)
(syntax-parse stx #:datum-literals (=)
[(_ [l:str = e] ...)
- #:with ((e- τ) ...) (infers+erase #'(e ...))
- (⊢ #'(list (list l e-) ...) #'(× [: l τ] ...))]
- [(_ e ...)
+ #:with ([e- τ] ...) (infers+erase #'(e ...))
+ (⊢ (list (list l e-) ...) : (× [~$ l τ] ...))]
+ #;[(_ e ...)
#'(stlc:tup e ...)]))
(define-syntax (proj stx)
(syntax-parse stx #:literals (quote)
[(_ rec l:str ~!)
- #:with (rec- τ_rec) (infer+erase #'rec)
- #:fail-unless (×? #'τ_rec) (format "not record type: ~a" (syntax->datum #'τ_rec))
- #:with (['l_τ:str τ] ...) (stx-map :-args (×-args #'τ_rec))
+ #:with [rec- τ_rec] (infer+erase #'rec)
+; #:when (printf "inferred type: ~a\n" (syntax->datum #'τ_rec))
+; #:when (printf "inferred type eval ~a\n" (syntax->datum ((current-type-eval) #'τ_rec)))
+ #:with ('l_τ:str ...) (×-get label from τ_rec)
+ #:with (τ ...) (×-get τ_fld from τ_rec)
+; #:fail-unless (×? #'τ_rec) (format "not record type: ~a" (syntax->datum #'τ_rec))
+; #:with (['l_τ:str τ] ...) (stx-map :-args (×-args #'τ_rec))
#:with (l_match:str τ_match) (str-stx-assoc #'l #'([l_τ τ] ...))
- (⊢ #'(cadr (assoc l rec)) #'τ_match)]
- [(_ e ...) #'(stlc:proj e ...)]))
+ (⊢ (cadr (assoc l rec)) : τ_match)]
+ #;[(_ e ...) #'(stlc:proj e ...)]))
-(define-type-constructor ∨)
+#;(define-type-constructor (∨ [: label τ] ...))
-(define-syntax (var stx)
+#;(define-syntax (var stx)
(syntax-parse stx #:datum-literals (as =) #:literals (quote)
[(_ l:str = e as τ:type)
#:when (∨? #'τ.norm)
@@ -76,7 +97,7 @@
#:with (e- τ_e) (infer+erase #'e)
#:when (typecheck? #'τ_e #'τ_match)
(⊢ #'(list l e) #'τ.norm)]))
-(define-syntax (case stx)
+#;(define-syntax (case stx)
(syntax-parse stx #:datum-literals (of =>) #:literals (quote)
[(_ e [l:str x => e_l] ...)
#:fail-when (null? (syntax->list #'(l ...))) "no clauses"
diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt
@@ -14,18 +14,17 @@
;; - terms from ext-stlc.rkt
;; - tup and proj
-(define-type-constructor ×)
+(define-type-constructor (× τ ...) #:declare τ type)
(define-syntax (tup stx)
(syntax-parse stx
[(_ e ...)
- #:with ((e- τ) ...) (infers+erase #'(e ...))
- (⊢ #'(list e- ...) #'(× τ ...))]))
+ #:with ([e- τ] ...) (infers+erase #'(e ...))
+ (⊢ (list e- ...) : (× τ ...))]))
(define-syntax (proj stx)
(syntax-parse stx
- [(_ tup n:integer)
- #:with (tup- τ_tup) (infer+erase #'tup)
- #:fail-unless (×? #'τ_tup) "not tuple type"
- #:fail-unless (< (syntax-e #'n) (×-num-args #'τ_tup)) "proj index too large"
- (⊢ #'(list-ref tup n) (×-ref #'τ_tup (syntax-e #'n)))]))
+ [(_ e_tup n:integer)
+ #:with [e_tup- τs_tup] (×-match+erase #'e_tup)
+ #:fail-unless (< (syntax-e #'n) (stx-length #'τs_tup)) "proj index too large"
+ (⊢ (list-ref e_tup- n) : #,(stx-list-ref #'τs_tup (syntax-e #'n)))]))
\ No newline at end of file
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
@@ -61,6 +61,9 @@
(define-syntax (app/tc stx)
(syntax-parse stx
[(_ e_fn e_arg ...)
+; #:with [e_fn- τ_fn] (infer+erase #'e_fn)
+; #:with (τ_in ...) (→-get τ_in from #'τ_fn)
+; #:with τ_out (→-get τ_out from #'τ_fn)
#:with [e_fn- (τ_in ... τ_out)] (→-match+erase #'e_fn)
#:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
diff --git a/tapl/tests/ext-stlc-tests.rkt b/tapl/tests/ext-stlc-tests.rkt
@@ -112,9 +112,10 @@
#:with-msg
"Arguments to function.+have wrong type.+Given:.+Int.+Expected:.+Bool")
;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
-(typecheck-fail (λ ([f : Int]) (f 1 2))
- #:with-msg
- "Expected type with pattern: \\(→ τ_in ... τ_out\\), got: Int")
+(typecheck-fail
+ (λ ([f : Int]) (f 1 2))
+ #:with-msg
+ "Expected type of expression f to match pattern \\(→ τ_in ... τ_out\\), got: Int")
(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
: (→ (→ Int Int Int) Int Int Int))
diff --git a/tapl/tests/stlc+reco+var-tests.rkt b/tapl/tests/stlc+reco+var-tests.rkt
@@ -12,10 +12,13 @@
(check-type + : ArithBinOp)
(check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int))
-;; records (ie labeled tuples)
+; records (ie labeled tuples)
(check-type "Stephen" : String)
+(check-type (tup) : (×))
+(check-type (tup ["name" = "Stephen"]) : (× [~$ "name" String]))
+(check-type (proj (tup ["name" = "Stephen"]) "name") : String ⇒ "Stephen")
(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "phone" Int] [: "male?" Bool]))
+ (× [~$ "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")
@@ -25,157 +28,157 @@
(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]))
+ (× [~$ "my-name" String] [~$ "phone" Int] [~$ "male?" Bool]))
(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "my-phone" Int] [: "male?" Bool]))
+ (× [~$ "name" String] [~$ "my-phone" Int] [~$ "male?" Bool]))
(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) :
- (× [: "name" String] [: "phone" Int] [: "is-male?" Bool]))
+ (× [~$ "name" String] [~$ "phone" Int] [~$ "is-male?" Bool]))
;; variants
-(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
+;(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 tuple tests: ------------------------------------------------------------
+;; wont work anymore
+;(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)
-
+;(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/tests/stlc+tup-tests.rkt b/tapl/tests/stlc+tup-tests.rkt
@@ -12,8 +12,11 @@
(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
+(typecheck-fail (proj (tup 1 "2" #f) 3) #:with-msg "index too large")
+(typecheck-fail
+ (proj 1 2)
+ #:with-msg
+ "Expected type of expression 1 to match pattern \\(× τ ...\\), got: Int")
;; ext-stlc.rkt tests ---------------------------------------------------------
;; should still pass
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -2,8 +2,10 @@
(require
(for-syntax (except-in racket extends)
syntax/parse racket/syntax syntax/stx
- "stx-utils.rkt")
+ "stx-utils.rkt"
+ syntax/parse/debug)
(for-meta 2 racket/base syntax/parse racket/syntax)
+ (for-meta 3 racket/base syntax/parse racket/syntax)
racket/provide)
(provide
(for-syntax (all-defined-out)) (all-defined-out)
@@ -118,11 +120,13 @@
(format "Type error: expected ~a type, got ~a"
(type->str #'τ) (type->str ty))
#'args]
- [_ #f])])))
+ [_ #f])]))
+)
(define-syntax define-type-constructor
(syntax-parser
[(_ (τ:id . pat)
+ ; lits must have ~ prefix (for syntax-parse compat) for now
(~optional (~seq #:lits (lit ...)) #:defaults ([(lit 1) null]))
decls ...
#;(~optional (~seq (~seq #:decl tvar (~datum as) cls) ...)
@@ -133,15 +137,43 @@
#:with τ-match+erase (format-id #'τ "~a-match+erase" #'τ)
#:with pat-class (generate-temporary #'τ) ; syntax-class name
#:with tycon (generate-temporary #'τ) ; need a runtime id for expansion
+ #:with (lit-tmp ...) (generate-temporaries #'(lit ...))
#`(begin
- (define lit void) ...
+ ;; list can't be function, ow it will use typed #%app
+ ;; define lit as macro that expands into #%app,
+ ;; so it will use the #%app here (racket's #%app)
+ (define lit-tmp void) ...
+ (define-syntax lit (syntax-parser [(_ . xs) #'(lit-tmp . xs)])) ...
+ (provide lit ...)
(provide τ)
(begin-for-syntax
- (define-syntax-class pat-class #:literals (lit ...)
+ (define-syntax lit
+ (pattern-expander
+ (syntax-parser
+ [(_ . xs)
+ ;#:when (displayln "pattern expanding")
+ #'((~literal #%plain-app) (~literal lit-tmp) . xs)]))) ...
+ (define-syntax-class pat-class
;; dont check is-type? here; should already be types
;; only check is-type? for user-entered types, eg tycon call
;; thus, dont include decls here, only want shape
- (pattern pat))
+ #;(pattern (~and pre (~do (printf "trying to match: ~a\n"(syntax->datum #'pre))) pat (~do (displayln "no")))) ; uses "lit" pattern expander
+ (pattern pat)
+ #;(pattern any
+ #:when (printf "trying to match: ~a\n" (syntax->datum #'any))
+ #:when (printf "orig: ~a\n" (type->str #'any))
+ #:when (printf "against pattern: ~a\n" (syntax->datum (quote-syntax pat)))
+ #:when (displayln #`(#,(stx-cdr (stx-car #'any))))
+ #:when (pretty-print (debug-parse #`(#,(stx-cdr (stx-car #'any))) pat))
+ #:with pat #'any) ;#`(#,(stx-cdr (stx-car #'any))))
+ #;(pattern any
+ #:when (displayln "match failed")
+ #:when (displayln "pat: ")
+ #:when (displayln (quote-syntax pat))
+ #:when (displayln #'any)
+ #:when (displayln "orig")
+ #:when (displayln (type->str #'any))
+ #:with pat #'any))
(define (τ-match ty)
(or (match-type ty tycon pat-class)
;; error msg should go in specific macro def?
@@ -167,12 +199,12 @@
[(_ attr from ty)
#:with args (generate-temporary)
#:with args.attr (format-id #'args "~a.~a" #'args #'attr)
- #'(syntax-parse ((current-type-eval) ty)
- [((~literal #%plain-type) ((~literal #%plain-app) t . args))
+ #'(syntax-parse ((current-type-eval) #'ty)
+ [((~literal #%plain-type) ((~literal #%plain-app) (~literal tycon) . args))
#:declare args pat-class ; check shape of arguments
- #:fail-unless (typecheck? #'t #'tycon) ; check tycons match
- (format "Type error: expected ~a type, got ~a"
- (type->str #'τ) (type->str ty))
+; #:fail-unless (typecheck? #'t #'tycon) ; check tycons match
+; (format "Type error: expected ~a type, got ~a"
+; (type->str #'τ) (type->str #'ty))
(attribute args.attr)])])))
(define tycon (λ _ (raise (exn:fail:type:runtime
(format "~a: Cannot use type at run time" 'τ)
@@ -182,12 +214,21 @@
[(_ . (~and pat !~ args)) ; first check shape
; this inner syntax-parse gets the ~! to register
; otherwise, apparently #:declare's get subst into pat (before ~!)
- (syntax-parse #'args
+ (syntax-parse #'args #:literals (lit ...)
[pat #,@#'(decls ...) ; then check declarations (eg, valid type)
#'(#%type (tycon . args))])]
- [_ (type-error #:src stx
- #:msg "Improper usage of type constructor ~a: ~a, expected pattern ~a"
- #'τ stx (quote-syntax (τ . pat)))])))]))
+ [_
+ (type-error #:src stx
+ #:msg (string-append
+ "Improper usage of type constructor ~a: ~a, expected pattern ~a, "
+ #;(format
+ "where: ~a"
+ (string-join
+ (stx-map
+ (λ (typ clss) (format "~a is a ~a" typ clss))
+ #'(ty (... ...)) #'(cls (... ...)))
+ ", ")))
+ #'τ stx (quote-syntax (τ . pat)))])))]))
;; TODO: refine this to enable specifying arity information
;; type constructors currently must have 1+ arguments
