commit 6fa962f83f4bfe2e1404611f14b66bdb3241affe
parent dbfd52bf0f18f04a3f28cdd08efee672defb7903
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 24 Feb 2016 19:02:51 -0500
all constructor type instantiations (in tests) inferred
- id type names and variant names (for 0arg constructors) supported
Diffstat:
4 files changed, 74 insertions(+), 19 deletions(-)
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -21,7 +21,8 @@
(define (compute-constraint τ1-τ2)
(syntax-parse τ1-τ2
[(X:id τ) #'((X τ))]
- [((~Any τ1 ...) (~Any τ2 ...))
+ [((~Any tycons1 τ1 ...) (~Any tycons2 τ2 ...))
+ #:when (typecheck? #'tycons1 #'tycons2)
(compute-constraints #'((τ1 τ2) ...))]
; should only be monomorphic?
[((~∀ () (~ext-stlc:→ τ1 ...)) (~∀ () (~ext-stlc:→ τ2 ...)))
@@ -50,12 +51,18 @@
(define-syntax (define-type stx)
(syntax-parse stx
+ [(_ Name:id . rst)
+ #:with Name2 (generate-temporary #'Name)
+ #`(begin
+ (define-type (Name2) . #,(subst #'(Name2) #'Name #'rst))
+ (define-type-alias Name (Name2)))]
[(_ (Name:id X:id ...)
;; constructors must have the form (Cons τ ...)
;; but the first ~or clause accepts 0-arg constructors as ids
;; the ~and is required to bind the duplicate Cons ids (see Ryan's email)
(~and (~or (~and IdCons:id (~parse (Cons τ ...) #'(IdCons)))
(Cons τ ...))) ...)
+ #:with NameExpander (format-id #'Name "~~~a" #'Name)
#:with (StructName ...) (generate-temporaries #'(Cons ...))
#:with ((e_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
#:with ((e_arg- ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
@@ -70,7 +77,17 @@
(struct StructName (fld ...) #:reflection-name 'Cons #:transparent) ...
(define-syntax (Cons stx)
(syntax-parse stx
+ ; no args and not poly morphic
[C:id #:when (and (stx-null? #'(X ...)) (stx-null? #'(τ ...))) #'(C)]
+ ; no args but polymorphic, check inferred type
+ [C:id
+ #:when (stx-null? #'(τ ...))
+ #:with τ-expected (syntax-property #'C 'expected-type)
+ #:fail-unless (syntax-e #'τ-expected)
+ (type-error #:src stx #:msg "cannot infer type of ~a; add annotations" #'C)
+ #:with (NameExpander τ-expected-arg (... ...)) #'τ-expected
+; #:when [e- τ_e] (infer+erase #'(C))
+ #'(C {τ-expected-arg (... ...)})]
[_:id
#:when (and (not (stx-null? #'(X ...)))
(not (stx-null? #'(τ ...))))
@@ -85,11 +102,17 @@
(format "and be applied to ~a arguments with type(s): "(stx-length #'(τ ...)))
(string-join (stx-map type->str #'(τ ...)) ", ")))]
[(_ τs e_arg ...)
- #:when (brace? #'τs) ; commit
+ #:when (brace? #'τs) ; commit to this clause
#:with {~! τ_X:type (... ...)} #'τs
- #:with ([e_arg- τ_arg] ...) (stx-map infer+erase #'(e_arg ...))
- #:with (τ_in:type (... ...))
- (stx-map (λ (t) (substs #'(τ_X.norm (... ...)) #'(X ...) t)) #'(τ ...))
+ #:with (τ_in:type (... ...)) ; instantiated types
+ (stx-map
+ (λ (t) (substs #'(τ_X.norm (... ...)) #'(X ...) t))
+ #'(τ ...))
+ #:with ([e_arg- τ_arg] ...)
+ (stx-map
+ (λ (e τ_e)
+ (infer+erase (syntax-property e 'expected-type τ_e)))
+ #'(e_arg ...) #'(τ_in.norm (... ...)))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in.norm (... ...)))
;; need to duplicate #%app err msg here, to attach additional props
(string-append
@@ -112,11 +135,25 @@
(⊢ (StructName e_arg- ...) : τ_out)]
[(C . args) #:when (stx-null? #'(X ...)) #'(C {} . args)] ; no tyvars, no annotations
[(C . args) ; no type annotations, must infer instantiation
- #:with ([arg- τarg] (... ...)) (infers+erase #'args)
- #:with (~Tmp Ys τ+ (... ...)) ((current-type-eval) #'(Tmp (X ...) τ ...))
- #:with cs (compute-constraints #'((τ+ τarg) (... ...)))
- #:with (τ_solved (... ...)) (stx-map (λ (y) (lookup y #'cs)) #'Ys)
- #'(C {τ_solved (... ...)} . args)]))
+ ;; infer instantiation types from args left-to-right, short-circuit if done early
+ #:with (~Tmp Ys . τs+) ((current-type-eval) #'(Tmp (X ...) τ ...))
+ (let loop ([a (stx-car #'args)] [a-rst (stx-cdr #'args)]
+ [τ+ (stx-car #'τs+)] [τ+rst (stx-cdr #'τs+)]
+ [old-cs #'()])
+ (define/with-syntax [a- τ_a] (infer+erase a))
+ (define cs (stx-append old-cs (compute-constraints (list (list τ+ #'τ_a)))))
+ (define maybe-solved (filter syntax-e (stx-map (λ (y) (lookup y cs)) #'Ys)))
+ (if (stx-length=? maybe-solved #'Ys)
+ #`(C #,(syntax-property #`{#,@maybe-solved} 'paren-shape #\{) . args) ; loses 'paren-shape
+ (if (or (stx-null? a-rst) (stx-null? τ+rst))
+ (type-error #:src stx
+ #:msg "could not infer types for constructor ~a; add annotations" #'(C . args))
+ (loop (stx-car a-rst) (stx-cdr a-rst) (stx-car τ+rst) (stx-cdr τ+rst) cs))))]))
+; #:with ([arg- τarg] (... ...)) (infers+erase #'args)
+; #:with (~Tmp Ys τ+ (... ...)) ((current-type-eval) #'(Tmp (X ...) τ ...))
+; #:with cs (compute-constraints #'((τ+ τarg) (... ...)))
+; #:with (τ_solved (... ...)) (stx-map (λ (y) (lookup y #'cs)) #'Ys)
+; #'(C {τ_solved (... ...)} . args)]))
...)]))
(define-syntax (match stx)
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
@@ -27,7 +27,7 @@
(define (stx-assoc v stx) ; v = id
(assoc v (map syntax->list (syntax->list stx)) free-identifier=?))
-(define (stx-length stx) (length (syntax->list stx)))
+(define (stx-length stx) (length (if (syntax? stx) (syntax->list stx) stx)))
(define (stx-length=? stx1 stx2)
(= (stx-length stx1) (stx-length stx2)))
diff --git a/tapl/tests/mlish-tests.rkt b/tapl/tests/mlish-tests.rkt
@@ -1,12 +1,12 @@
#lang s-exp "../mlish.rkt"
(require "rackunit-typechecking.rkt")
-(define-type (IntList)
+(define-type IntList
INil
- (ConsI Int (IntList)))
+ (ConsI Int IntList))
-(check-type INil : (IntList))
-(check-type (ConsI 1 INil) : (IntList))
+(check-type INil : IntList)
+(check-type (ConsI 1 INil) : IntList)
(check-type
(match INil with
[INil -> 1]
@@ -20,9 +20,19 @@
(define-type (List X)
(Nil)
(Cons X (List X)))
+;; annotated
(check-type (Nil {Int}) : (List Int))
+(check-type (Cons {Int} 1 (Nil {Int})) : (List Int))
+(check-type (Cons {Int} 1 (Cons 2 (Nil {Int}))) : (List Int))
+;; partial annotations
(check-type (Cons 1 (Nil {Int})) : (List Int))
(check-type (Cons 1 (Cons 2 (Nil {Int}))) : (List Int))
+(check-type (Cons {Int} 1 Nil) : (List Int))
+(check-type (Cons {Int} 1 (Cons 2 Nil)) : (List Int))
+(check-type (Cons 1 (Cons {Int} 2 Nil)) : (List Int))
+; no annotations
+(check-type (Cons 1 Nil) : (List Int))
+(check-type (Cons 1 (Cons 2 Nil)) : (List Int))
(define-type (Tree X)
(Leaf X)
@@ -30,8 +40,16 @@
(check-type (Leaf 10) : (Tree Int))
(check-type (Node (Leaf 10) (Leaf 11)) : (Tree Int))
+(typecheck-fail Nil #:with-msg "add annotations")
(typecheck-fail (Cons 1 (Nil {Bool}))
#:with-msg "wrong type\\(s\\)")
+(typecheck-fail (Cons {Bool} 1 (Nil {Int}))
+ #:with-msg "wrong type\\(s\\)")
+(typecheck-fail (Cons {Bool} 1 Nil)
+ #:with-msg "wrong type\\(s\\)")
+
+(typecheck-fail (match Nil with [Cons x xs -> 2] [Nil -> 1])
+ #:with-msg "add annotations")
(check-type
(match (Nil {Int}) with
[Cons x xs -> 2]
@@ -45,13 +63,13 @@
: Int ⇒ 1)
(check-type
- (match (Cons 1 (Nil {Int})) with
+ (match (Cons 1 Nil) with
[Nil -> 3]
[Cons y ys -> (+ y 4)])
: Int ⇒ 5)
(check-type
- (match (Cons 1 (Nil {Int})) with
+ (match (Cons 1 Nil) with
[Cons y ys -> (+ y 5)]
[Nil -> 3])
: Int ⇒ 6)
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -648,8 +648,8 @@
(define-syntax ~Any ; matches any tycon
(pattern-expander
(syntax-parser
- [(_ x ...)
- #'((~literal #%plain-app) _
+ [(_ tycons x ...)
+ #'((~literal #%plain-app) tycons
((~literal #%plain-lambda) bvs (~literal void) x ...))])))
(define (merge-type-tags stx)
(define t (syntax-property stx 'type))
