Rough draft of syntax classes for tc-app.
original commit: dda1d6021157cfb07cefdb9aac6093d8bbbae0b7
This commit is contained in:
Eric Dobson
Sam Tobin-Hochstadt
parent
274b4a3845
commit
cf3cdb4d9d
|
|
@ -29,7 +29,8 @@
|
|||
|
||||
(define-signature tc-app^
|
||||
([cond-contracted tc/app (syntax? . -> . tc-results?)]
|
||||
[cond-contracted tc/app/check (syntax? tc-results? . -> . tc-results?)]))
|
||||
[cond-contracted tc/app/check (syntax? tc-results? . -> . tc-results?)]
|
||||
[cond-contracted tc/app-regular (syntax? . -> . tc-results?)]))
|
||||
|
||||
(define-signature tc-apply^
|
||||
([cond-contracted tc/apply (syntax? syntax? . -> . tc-results?)]))
|
||||
|
|
|
|||
|
|
@ -3,6 +3,7 @@
|
|||
(require "../utils/utils.rkt"
|
||||
"tc-app/signatures.rkt"
|
||||
syntax/parse racket/match
|
||||
syntax/parse/experimental/reflect
|
||||
(typecheck signatures check-below tc-funapp)
|
||||
(types utils abbrev)
|
||||
(rep type-rep filter-rep object-rep rep-utils)
|
||||
|
|
@ -19,13 +20,17 @@
|
|||
(define (tc/app/internal form expected)
|
||||
(or
|
||||
(tc/app-annotated form expected)
|
||||
(syntax-parse form
|
||||
[(#%plain-app .
|
||||
(~or (~reflect v (tc/app-list expected) #:attributes (check))
|
||||
(~reflect v (tc/app-apply expected) #:attributes (check))
|
||||
(~reflect v (tc/app-eq expected) #:attributes (check))))
|
||||
((attribute v.check))]
|
||||
[_ #f])
|
||||
(tc/app-hetero form expected)
|
||||
(tc/app-list form expected)
|
||||
(tc/app-apply form expected)
|
||||
(tc/app-values form expected)
|
||||
(tc/app-keywords form expected)
|
||||
(tc/app-objects form expected)
|
||||
(tc/app-eq form expected)
|
||||
(tc/app-lambda form expected)
|
||||
(tc/app-special form expected)
|
||||
(tc/app-regular form expected)))
|
||||
|
|
|
|||
|
|
@ -3,6 +3,7 @@
|
|||
(require "../../utils/utils.rkt"
|
||||
"signatures.rkt"
|
||||
syntax/parse racket/match
|
||||
syntax/parse/experimental/reflect
|
||||
(typecheck signatures tc-funapp check-below tc-subst)
|
||||
(types abbrev utils)
|
||||
(rep type-rep)
|
||||
|
|
@ -18,20 +19,21 @@
|
|||
(import tc-expr^ tc-apply^)
|
||||
(export tc-app-apply^)
|
||||
|
||||
(define (tc/app-apply form expected)
|
||||
(syntax-parse form
|
||||
#:literals (#%plain-app k:apply apply values)
|
||||
;; rewrite this so that it takes advantages of all the special cases
|
||||
[(#%plain-app k:apply . args)
|
||||
(tc/app-apply (syntax/loc form (#%plain-app apply . args)) expected)]
|
||||
;; (apply values l) gets special handling
|
||||
;; Needs to be above the general apply checking
|
||||
[(#%plain-app apply values e)
|
||||
(match (single-value #'e)
|
||||
[(tc-result1: (ListDots: dty dbound)) (values->tc-results (make-ValuesDots null dty dbound) #f)]
|
||||
[(tc-result1: (List: ts)) (ret ts)]
|
||||
[_ (tc/apply #'values #'(e))])]
|
||||
;; handle apply specially
|
||||
[(#%plain-app apply f . args) (tc/apply #'f #'args)]
|
||||
[_ #f]))
|
||||
(define-syntax-class (tc/app-apply* expected)
|
||||
#:attributes (check)
|
||||
#:literals (k:apply apply values)
|
||||
(pattern ((~or apply k:apply) values e)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match (single-value #'e)
|
||||
[(tc-result1: (ListDots: dty dbound)) (values->tc-results (make-ValuesDots null dty dbound) #f)]
|
||||
[(tc-result1: (List: ts)) (ret ts)]
|
||||
[_ (tc/apply #'values #'(e))])))
|
||||
(pattern ((~or apply k:apply) f . args)
|
||||
#:attr check
|
||||
(lambda () (tc/apply #'f #'args))))
|
||||
|
||||
|
||||
(define tc/app-apply (reify-syntax-class tc/app-apply*))
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -3,6 +3,7 @@
|
|||
(require "../../utils/utils.rkt"
|
||||
"signatures.rkt"
|
||||
syntax/parse racket/match
|
||||
syntax/parse/experimental/reflect
|
||||
(typecheck signatures tc-funapp check-below)
|
||||
(types abbrev union utils)
|
||||
(rep type-rep)
|
||||
|
|
@ -22,18 +23,22 @@
|
|||
(pattern eq?) (pattern equal?) (pattern eqv?) (pattern =) (pattern string=?) (pattern symbol=?)
|
||||
(pattern member) (pattern memq) (pattern memv))
|
||||
|
||||
(define (tc/app-eq form expected)
|
||||
(syntax-parse form
|
||||
#:literals (#%plain-app)
|
||||
[(#%plain-app eq?:comparator v1 v2)
|
||||
;; make sure the whole expression is type correct
|
||||
(match* ((tc/funapp #'eq? #'(v1 v2) (single-value #'eq?)
|
||||
(map single-value (syntax->list #'(v1 v2))) expected)
|
||||
;; check thn and els with the eq? info
|
||||
(tc/eq #'eq? #'v1 #'v2))
|
||||
[((tc-result1: t) (tc-result1: t* f o))
|
||||
(ret t f o)])]
|
||||
[_ #f]))
|
||||
|
||||
(define-syntax-class (tc/app-eq* expected)
|
||||
#:attributes (check)
|
||||
(pattern (eq?:comparator v1 v2)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
;; make sure the whole expression is type correct
|
||||
(match* ((tc/funapp #'eq? #'(v1 v2) (single-value #'eq?)
|
||||
(map single-value (syntax->list #'(v1 v2))) expected)
|
||||
;; check thn and els with the eq? info
|
||||
(tc/eq #'eq? #'v1 #'v2))
|
||||
[((tc-result1: t) (tc-result1: t* f o))
|
||||
(ret t f o)]))))
|
||||
|
||||
(define tc/app-eq (reify-syntax-class tc/app-eq*))
|
||||
|
||||
|
||||
;; typecheck eq? applications
|
||||
;; identifier expr expr -> tc-results
|
||||
|
|
|
|||
|
|
@ -4,6 +4,7 @@
|
|||
(require "../../utils/utils.rkt"
|
||||
"signatures.rkt"
|
||||
syntax/parse racket/match
|
||||
syntax/parse/experimental/reflect
|
||||
(only-in '#%kernel [reverse k:reverse])
|
||||
(typecheck signatures tc-funapp check-below)
|
||||
(types abbrev utils union substitute)
|
||||
|
|
@ -19,89 +20,99 @@
|
|||
(only-in '#%kernel [reverse k:reverse])))
|
||||
|
||||
|
||||
(import tc-expr^)
|
||||
(import tc-expr^ tc-app^)
|
||||
(export tc-app-list^)
|
||||
|
||||
|
||||
(define (tc/app-list form expected)
|
||||
(syntax-parse form
|
||||
#:literals (#%plain-app
|
||||
reverse k:reverse list list*
|
||||
cons map andmap ormap)
|
||||
[(#%plain-app map f arg0 arg ...)
|
||||
(match* ((single-value #'arg0) (map single-value (syntax->list #'(arg ...))))
|
||||
;; if the argument is a ListDots
|
||||
[((tc-result1: (ListDots: t0 bound0))
|
||||
(list (tc-result1: (or (and (ListDots: t bound) (app (λ _ #f) var))
|
||||
;; a devious hack - just generate #f so the test below succeeds
|
||||
;; have to explicitly bind `var' since otherwise `var' appears
|
||||
;; on only one side of the or
|
||||
;; NOTE: safe to include these, `map' will error if any list is
|
||||
;; not the same length as all the others
|
||||
(and (Listof: t var) (app (λ _ #f) bound))))
|
||||
...))
|
||||
(=> fail)
|
||||
(unless (for/and ([b bound]) (or (not b) (eq? bound0 b))) (fail))
|
||||
(match (extend-tvars (list bound0)
|
||||
;; just check that the function applies successfully to the element type
|
||||
(tc/funapp #'f #'(arg0 arg ...) (tc-expr #'f) (cons (ret t0) (map ret t)) expected))
|
||||
[(tc-result1: t) (ret (make-ListDots t bound0))]
|
||||
[(tc-results: ts)
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
"Expected one value, but got ~a" (-values ts))])]
|
||||
;; otherwise, if it's not a ListDots, defer to the regular function typechecking
|
||||
[(res0 res) #f])]
|
||||
;; ormap/andmap of ... argument
|
||||
[(#%plain-app (~or andmap ormap) f arg)
|
||||
;; check the arguments
|
||||
(match-let* ([arg-ty (single-value #'arg)]
|
||||
[ft (tc-expr #'f)])
|
||||
(match (match arg-ty
|
||||
;; if the argument is a ListDots
|
||||
[(tc-result1: (ListDots: t bound))
|
||||
;; just check that the function applies successfully to the element type
|
||||
(tc/funapp #'f #'(arg) ft (list (ret (substitute Univ bound t))) expected)]
|
||||
;; otherwise ...
|
||||
[_ #f])
|
||||
[(tc-result1: t) (ret (Un (-val #f) t))]
|
||||
;; if it's not a ListDots, defer to the regular function typechecking
|
||||
[_ #f]))]
|
||||
;; special case for `list'
|
||||
[(#%plain-app list . args)
|
||||
(match expected
|
||||
[(tc-result1: (Listof: elem-ty))
|
||||
(for ([i (in-list (syntax->list #'args))])
|
||||
(tc-expr/check i (ret elem-ty)))
|
||||
expected]
|
||||
[(tc-result1: (List: (? (lambda (ts) (= (length (syntax->list #'args))
|
||||
(length ts)))
|
||||
ts)))
|
||||
(for ([ac (in-list (syntax->list #'args))]
|
||||
[exp (in-list ts)])
|
||||
(tc-expr/check ac (ret exp)))
|
||||
expected]
|
||||
[_
|
||||
(let ([tys (map tc-expr/t (syntax->list #'args))])
|
||||
(ret (apply -lst* tys)))])]
|
||||
;; special case for `list*'
|
||||
[(#%plain-app list* . args)
|
||||
(match-let* ([(list tys ... last) (map tc-expr/t (syntax->list #'args))])
|
||||
(ret (foldr -pair last tys)))]
|
||||
;; special case for `reverse' to propagate expected type info
|
||||
[(#%plain-app (~or reverse k:reverse) arg)
|
||||
(match expected
|
||||
[(tc-result1: (Listof: _))
|
||||
(tc-expr/check #'arg expected)]
|
||||
[(tc-result1: (List: ts))
|
||||
(tc-expr/check #'arg (ret (-Tuple (reverse ts))))
|
||||
expected]
|
||||
[_
|
||||
(match (single-value #'arg)
|
||||
[(tc-result1: (List: ts))
|
||||
(cond-check-below (ret (-Tuple (reverse ts))) expected)]
|
||||
[arg-ty
|
||||
(tc/funapp #'reverse #'(arg) (single-value #'reverse) (list arg-ty) expected)])])]
|
||||
[_ #f]))
|
||||
(define-syntax-class (tc/app-list* expected)
|
||||
#:attributes (check)
|
||||
#:literals (reverse k:reverse list list*
|
||||
cons map andmap ormap)
|
||||
(pattern (~and form (map f arg0 arg ...))
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match* ((single-value #'arg0) (map single-value (syntax->list #'(arg ...))))
|
||||
;; if the argument is a ListDots
|
||||
[((tc-result1: (ListDots: t0 bound0))
|
||||
(list (tc-result1: (or (and (ListDots: t bound) (app (λ _ #f) var))
|
||||
;; a devious hack - just generate #f so the test below succeeds
|
||||
;; have to explicitly bind `var' since otherwise `var' appears
|
||||
;; on only one side of the or
|
||||
;; NOTE: safe to include these, `map' will error if any list is
|
||||
;; not the same length as all the others
|
||||
(and (Listof: t var) (app (λ _ #f) bound))))
|
||||
...))
|
||||
(=> fail)
|
||||
(unless (for/and ([b bound]) (or (not b) (eq? bound0 b))) (fail))
|
||||
(match (extend-tvars (list bound0)
|
||||
;; just check that the function applies successfully to the element type
|
||||
(tc/funapp #'f #'(arg0 arg ...) (tc-expr #'f) (cons (ret t0) (map ret t)) expected))
|
||||
[(tc-result1: t) (ret (make-ListDots t bound0))]
|
||||
[(tc-results: ts)
|
||||
(tc-error/expr #:return (ret (Un))
|
||||
"Expected one value, but got ~a" (-values ts))])]
|
||||
;; otherwise, if it's not a ListDots, defer to the regular function typechecking
|
||||
;; TODO fix double typechecking
|
||||
[(res0 res) (tc/app-regular #'(#%plain-app . form) expected)])))
|
||||
;; ormap/andmap of ... argument
|
||||
(pattern (~and form ((~or andmap ormap) f arg))
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match-let* ([arg-ty (single-value #'arg)]
|
||||
[ft (tc-expr #'f)])
|
||||
(match (match arg-ty
|
||||
;; if the argument is a ListDots
|
||||
[(tc-result1: (ListDots: t bound))
|
||||
;; just check that the function applies successfully to the element type
|
||||
(tc/funapp #'f #'(arg) ft (list (ret (substitute Univ bound t))) expected)]
|
||||
;; otherwise ...
|
||||
[_ #f])
|
||||
[(tc-result1: t) (ret (Un (-val #f) t))]
|
||||
;; if it's not a ListDots, defer to the regular function typechecking
|
||||
;; TODO fix double typechecking
|
||||
[_ (tc/app-regular #'(#%plain-app . form) expected)]))))
|
||||
;; special case for `list'
|
||||
(pattern (list . args)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match expected
|
||||
[(tc-result1: (Listof: elem-ty))
|
||||
(for ([i (in-list (syntax->list #'args))])
|
||||
(tc-expr/check i (ret elem-ty)))
|
||||
expected]
|
||||
[(tc-result1: (List: (? (lambda (ts) (= (length (syntax->list #'args))
|
||||
(length ts)))
|
||||
ts)))
|
||||
(for ([ac (in-list (syntax->list #'args))]
|
||||
[exp (in-list ts)])
|
||||
(tc-expr/check ac (ret exp)))
|
||||
expected]
|
||||
[_
|
||||
(let ([tys (map tc-expr/t (syntax->list #'args))])
|
||||
(ret (apply -lst* tys)))])))
|
||||
;; special case for `list*'
|
||||
(pattern (list* . args)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match-let* ([(list tys ... last) (map tc-expr/t (syntax->list #'args))])
|
||||
(ret (foldr -pair last tys)))))
|
||||
;; special case for `reverse' to propagate expected type info
|
||||
(pattern ((~or reverse k:reverse) arg)
|
||||
#:attr check
|
||||
(lambda ()
|
||||
(match expected
|
||||
[(tc-result1: (Listof: _))
|
||||
(tc-expr/check #'arg expected)]
|
||||
[(tc-result1: (List: ts))
|
||||
(tc-expr/check #'arg (ret (-Tuple (reverse ts))))
|
||||
expected]
|
||||
[_
|
||||
(match (single-value #'arg)
|
||||
[(tc-result1: (List: ts))
|
||||
(cond-check-below (ret (-Tuple (reverse ts))) expected)]
|
||||
[arg-ty
|
||||
(tc/funapp #'reverse #'(arg) (single-value #'reverse) (list arg-ty) expected)])]))))
|
||||
|
||||
|
||||
(define tc/app-list (reify-syntax-class tc/app-list*))
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user