Split out tc-expression to a separate file.
This commit is contained in:
Eric Dobson
parent
6d841adb9a
commit
d68a1ebc35
|
|
@ -31,6 +31,9 @@
|
||||||
(define-signature tc-send^
|
(define-signature tc-send^
|
||||||
([cond-contracted tc/send ((syntax? syntax? syntax? syntax?) ((or/c tc-results/c #f)) . ->* . full-tc-results/c)]))
|
([cond-contracted tc/send ((syntax? syntax? syntax? syntax?) ((or/c tc-results/c #f)) . ->* . full-tc-results/c)]))
|
||||||
|
|
||||||
|
(define-signature tc-expression^
|
||||||
|
([cond-contracted tc/#%expression (syntax? (or/c tc-results/c #f) . ->* . full-tc-results/c)]))
|
||||||
|
|
||||||
(define-signature tc-lambda^
|
(define-signature tc-lambda^
|
||||||
([cond-contracted tc/lambda (syntax? syntax? syntax? . -> . full-tc-results/c)]
|
([cond-contracted tc/lambda (syntax? syntax? syntax? . -> . full-tc-results/c)]
|
||||||
[cond-contracted tc/lambda/check (syntax? syntax? syntax? tc-results/c . -> . full-tc-results/c)]
|
[cond-contracted tc/lambda/check (syntax? syntax? syntax? tc-results/c . -> . full-tc-results/c)]
|
||||||
|
|
|
||||||
|
|
@ -23,102 +23,12 @@
|
||||||
(only-in racket/private/class-internal find-method/who)))
|
(only-in racket/private/class-internal find-method/who)))
|
||||||
|
|
||||||
(import tc-if^ tc-lambda^ tc-app^ tc-let^ tc-send^ check-subforms^ tc-literal^
|
(import tc-if^ tc-lambda^ tc-app^ tc-let^ tc-send^ check-subforms^ tc-literal^
|
||||||
check-class^)
|
check-class^ tc-expression^)
|
||||||
(export tc-expr^)
|
(export tc-expr^)
|
||||||
|
|
||||||
(define-literal-set tc-expr-literals #:for-label
|
(define-literal-set tc-expr-literals #:for-label
|
||||||
(find-method/who))
|
(find-method/who))
|
||||||
|
|
||||||
;; do-inst : tc-results? syntax? -> tc-results?
|
|
||||||
;; Perform a type instantiation, delegating to the appropriate helper
|
|
||||||
;; function depending on if the argument is a row or not
|
|
||||||
(define (do-inst tc-res inst)
|
|
||||||
(define inst-type
|
|
||||||
(if (row-syntax? inst) do-row-inst do-normal-inst))
|
|
||||||
(define (error-case tys)
|
|
||||||
(tc-error/expr
|
|
||||||
"Cannot instantiate expression that produces ~a values"
|
|
||||||
(if (null? tys) 0 "multiple")))
|
|
||||||
(match tc-res
|
|
||||||
[(tc-results: tys fs os)
|
|
||||||
(match tys
|
|
||||||
[(list ty)
|
|
||||||
(ret (list (inst-type ty inst)) fs os)]
|
|
||||||
[_
|
|
||||||
(error-case tys)])]
|
|
||||||
[(tc-results: tys fs os dty dbound)
|
|
||||||
(match tys
|
|
||||||
[(list ty)
|
|
||||||
(ret (list (inst-type ty inst)) fs os dty dbound)]
|
|
||||||
[_
|
|
||||||
(error-case tys)])]))
|
|
||||||
|
|
||||||
;; row-syntax? Syntax -> Boolean
|
|
||||||
;; This checks if the syntax object resulted from a row instantiation
|
|
||||||
(define (row-syntax? stx)
|
|
||||||
(define lst (stx->list stx))
|
|
||||||
(and lst (pair? lst)
|
|
||||||
(eq? (syntax-e (car lst)) '#:row)))
|
|
||||||
|
|
||||||
;; do-normal-inst : Type Syntax -> Type
|
|
||||||
;; Instantiate a normal polymorphic type
|
|
||||||
(define (do-normal-inst ty inst)
|
|
||||||
(cond
|
|
||||||
[(not (or (Poly? ty) (PolyDots? ty)))
|
|
||||||
(tc-error/expr #:return (Un) "Cannot instantiate non-polymorphic type ~a"
|
|
||||||
(cleanup-type ty))]
|
|
||||||
[(and (Poly? ty)
|
|
||||||
(not (= (syntax-length inst) (Poly-n ty))))
|
|
||||||
(tc-error/expr #:return (Un)
|
|
||||||
"Wrong number of type arguments to polymorphic type ~a:\nexpected: ~a\ngot: ~a"
|
|
||||||
(cleanup-type ty) (Poly-n ty) (syntax-length inst))]
|
|
||||||
[(and (PolyDots? ty) (not (>= (syntax-length inst) (sub1 (PolyDots-n ty)))))
|
|
||||||
;; we can provide 0 arguments for the ... var
|
|
||||||
(tc-error/expr #:return (Un)
|
|
||||||
"Wrong number of type arguments to polymorphic type ~a:\nexpected at least: ~a\ngot: ~a"
|
|
||||||
(cleanup-type ty) (sub1 (PolyDots-n ty)) (syntax-length inst))]
|
|
||||||
[(PolyDots? ty)
|
|
||||||
;; In this case, we need to check the last thing. If it's a dotted var, then we need to
|
|
||||||
;; use instantiate-poly-dotted, otherwise we do the normal thing.
|
|
||||||
;; In the case that the list is empty we also do the normal thing
|
|
||||||
(match (syntax->list inst)
|
|
||||||
[(list ty-stxs ... (app syntax-e (cons bound-ty-stx (? identifier? bound-id))))
|
|
||||||
(unless (bound-index? (syntax-e bound-id))
|
|
||||||
(tc-error/stx bound-id "~a is not a type variable bound with ..." (syntax-e bound-id)))
|
|
||||||
(if (= (length ty-stxs) (sub1 (PolyDots-n ty)))
|
|
||||||
(let* ([last-id (syntax-e bound-id)]
|
|
||||||
[last-ty (extend-tvars (list last-id) (parse-type bound-ty-stx))])
|
|
||||||
(instantiate-poly-dotted ty (map parse-type ty-stxs) last-ty last-id))
|
|
||||||
(tc-error/expr #:return (Un) "Wrong number of fixed type arguments to polymorphic type ~a:\nexpected: ~a\ngot: ~a"
|
|
||||||
ty (sub1 (PolyDots-n ty)) (length ty-stxs)))]
|
|
||||||
[stx-list
|
|
||||||
(instantiate-poly ty (map parse-type stx-list))])]
|
|
||||||
[else
|
|
||||||
(instantiate-poly ty (stx-map parse-type inst))]))
|
|
||||||
|
|
||||||
;; do-row-inst : Type ClassRow -> Type
|
|
||||||
;; Instantiate a row polymorphic function type
|
|
||||||
(define (do-row-inst ty row-stx)
|
|
||||||
;; At this point, we know `stx` represents a row so we can parse it.
|
|
||||||
;; The parsing is done here because if `inst` did the parsing, it's
|
|
||||||
;; too early and ends up with an empty type environment.
|
|
||||||
(define row
|
|
||||||
(syntax-parse row-stx
|
|
||||||
[(#:row (~var clauses (row-clauses parse-type)))
|
|
||||||
(attribute clauses.row)]))
|
|
||||||
(cond
|
|
||||||
[(not (PolyRow? ty))
|
|
||||||
(tc-error/expr #:return (Un) "Cannot instantiate non-row-polymorphic type ~a"
|
|
||||||
(cleanup-type ty))]
|
|
||||||
[else
|
|
||||||
(match-define (PolyRow: _ constraints _) ty)
|
|
||||||
(check-row-constraints
|
|
||||||
row constraints
|
|
||||||
(λ (name)
|
|
||||||
(tc-error/expr
|
|
||||||
(~a "Cannot instantiate row with member " name
|
|
||||||
" that the given row variable requires to be absent"))))
|
|
||||||
(instantiate-poly ty (list row))]))
|
|
||||||
|
|
||||||
;; typecheck an identifier
|
;; typecheck an identifier
|
||||||
;; the identifier has variable effect
|
;; the identifier has variable effect
|
||||||
|
|
@ -245,18 +155,7 @@
|
||||||
;; application
|
;; application
|
||||||
[(#%plain-app . _) (tc/app/check form expected)]
|
[(#%plain-app . _) (tc/app/check form expected)]
|
||||||
;; #%expression
|
;; #%expression
|
||||||
[((~and exp #%expression) e)
|
[(#%expression e) (tc/#%expression form expected)]
|
||||||
#:when (type-inst-property #'exp)
|
|
||||||
(do-inst (tc-expr #'e) (type-inst-property #'exp))]
|
|
||||||
[((~and exp:type-ascription^ #%expression) e)
|
|
||||||
(add-scoped-tvars #'e (parse-literal-alls (attribute exp.value)))
|
|
||||||
(tc-expr/check #'e (parse-tc-results (attribute exp.value)))]
|
|
||||||
[((~and exp #%expression) e)
|
|
||||||
#:when (external-check-property #'exp)
|
|
||||||
((external-check-property #'exp) #'e)
|
|
||||||
(tc-expr/check #'e expected)]
|
|
||||||
[(#%expression e)
|
|
||||||
(tc-expr/check #'e expected)]
|
|
||||||
;; syntax
|
;; syntax
|
||||||
;; for now, we ignore the rhs of macros
|
;; for now, we ignore the rhs of macros
|
||||||
[(letrec-syntaxes+values stxs vals . body)
|
[(letrec-syntaxes+values stxs vals . body)
|
||||||
|
|
@ -420,13 +319,7 @@
|
||||||
;; top-level variable reference - occurs at top level
|
;; top-level variable reference - occurs at top level
|
||||||
[(#%top . id) (tc-id #'id)]
|
[(#%top . id) (tc-id #'id)]
|
||||||
;; #%expression
|
;; #%expression
|
||||||
[((~and exp #%expression) e)
|
[(#%expression e) (tc/#%expression form #f)]
|
||||||
#:when (type-inst-property #'exp)
|
|
||||||
(do-inst (tc-expr #'e) (type-inst-property #'exp))]
|
|
||||||
[((~and exp:type-ascription^ #%expression) e)
|
|
||||||
(add-scoped-tvars #'e (parse-literal-alls (attribute exp.value)))
|
|
||||||
(tc-expr/check #'e (parse-tc-results (attribute exp.value)))]
|
|
||||||
[(#%expression e) (tc-expr #'e)]
|
|
||||||
;; #%variable-reference
|
;; #%variable-reference
|
||||||
[(#%variable-reference . _)
|
[(#%variable-reference . _)
|
||||||
(ret -Variable-Reference)]
|
(ret -Variable-Reference)]
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,129 @@
|
||||||
|
#lang racket/unit
|
||||||
|
|
||||||
|
(require
|
||||||
|
"../utils/utils.rkt"
|
||||||
|
(typecheck tc-expr-unit signatures tc-app-helper)
|
||||||
|
(types tc-result tc-error utils abbrev classes)
|
||||||
|
(rep type-rep)
|
||||||
|
(utils tc-utils)
|
||||||
|
(env index-env tvar-env scoped-tvar-env)
|
||||||
|
(private syntax-properties type-annotation parse-type)
|
||||||
|
unstable/syntax
|
||||||
|
racket/format
|
||||||
|
racket/match
|
||||||
|
syntax/stx
|
||||||
|
syntax/parse)
|
||||||
|
|
||||||
|
|
||||||
|
(import tc-expr^)
|
||||||
|
(export tc-expression^)
|
||||||
|
|
||||||
|
;; Typecheck an (#%expression e) form
|
||||||
|
(define (tc/#%expression form expected)
|
||||||
|
(syntax-parse form
|
||||||
|
[(exp:type-inst^ e)
|
||||||
|
(do-inst (tc-expr #'e) (attribute exp.value))]
|
||||||
|
[(exp:type-ascription^ e)
|
||||||
|
(add-scoped-tvars #'e (parse-literal-alls (attribute exp.value)))
|
||||||
|
(tc-expr/check #'e (parse-tc-results (attribute exp.value)))]
|
||||||
|
[(exp:external-check^ e)
|
||||||
|
((attribute exp.value) #'e)
|
||||||
|
(if expected
|
||||||
|
(tc-expr/check #'e expected)
|
||||||
|
(tc-expr #'e))]
|
||||||
|
[(_ e)
|
||||||
|
(if expected
|
||||||
|
(tc-expr/check #'e expected)
|
||||||
|
(tc-expr #'e))]))
|
||||||
|
|
||||||
|
;; do-inst : tc-results? syntax? -> tc-results?
|
||||||
|
;; Perform a type instantiation, delegating to the appropriate helper
|
||||||
|
;; function depending on if the argument is a row or not
|
||||||
|
(define (do-inst tc-res inst)
|
||||||
|
(define inst-type
|
||||||
|
(if (row-syntax? inst) do-row-inst do-normal-inst))
|
||||||
|
(define (error-case tys)
|
||||||
|
(tc-error/expr
|
||||||
|
"Cannot instantiate expression that produces ~a values"
|
||||||
|
(if (null? tys) 0 "multiple")))
|
||||||
|
(match tc-res
|
||||||
|
[(tc-results: tys fs os)
|
||||||
|
(match tys
|
||||||
|
[(list ty)
|
||||||
|
(ret (list (inst-type ty inst)) fs os)]
|
||||||
|
[_
|
||||||
|
(error-case tys)])]
|
||||||
|
[(tc-results: tys fs os dty dbound)
|
||||||
|
(match tys
|
||||||
|
[(list ty)
|
||||||
|
(ret (list (inst-type ty inst)) fs os dty dbound)]
|
||||||
|
[_
|
||||||
|
(error-case tys)])]))
|
||||||
|
|
||||||
|
;; row-syntax? Syntax -> Boolean
|
||||||
|
;; This checks if the syntax object resulted from a row instantiation
|
||||||
|
(define (row-syntax? stx)
|
||||||
|
(define lst (stx->list stx))
|
||||||
|
(and lst (pair? lst)
|
||||||
|
(eq? (syntax-e (car lst)) '#:row)))
|
||||||
|
|
||||||
|
;; do-normal-inst : Type Syntax -> Type
|
||||||
|
;; Instantiate a normal polymorphic type
|
||||||
|
(define (do-normal-inst ty inst)
|
||||||
|
(cond
|
||||||
|
[(not (or (Poly? ty) (PolyDots? ty)))
|
||||||
|
(tc-error/expr #:return -Bottom "Cannot instantiate non-polymorphic type ~a"
|
||||||
|
(cleanup-type ty))]
|
||||||
|
[(and (Poly? ty)
|
||||||
|
(not (= (syntax-length inst) (Poly-n ty))))
|
||||||
|
(tc-error/expr #:return -Bottom
|
||||||
|
"Wrong number of type arguments to polymorphic type ~a:\nexpected: ~a\ngot: ~a"
|
||||||
|
(cleanup-type ty) (Poly-n ty) (syntax-length inst))]
|
||||||
|
[(and (PolyDots? ty) (not (>= (syntax-length inst) (sub1 (PolyDots-n ty)))))
|
||||||
|
;; we can provide 0 arguments for the ... var
|
||||||
|
(tc-error/expr #:return -Bottom
|
||||||
|
"Wrong number of type arguments to polymorphic type ~a:\nexpected at least: ~a\ngot: ~a"
|
||||||
|
(cleanup-type ty) (sub1 (PolyDots-n ty)) (syntax-length inst))]
|
||||||
|
[(PolyDots? ty)
|
||||||
|
;; In this case, we need to check the last thing. If it's a dotted var, then we need to
|
||||||
|
;; use instantiate-poly-dotted, otherwise we do the normal thing.
|
||||||
|
;; In the case that the list is empty we also do the normal thing
|
||||||
|
(match (syntax->list inst)
|
||||||
|
[(list ty-stxs ... (app syntax-e (cons bound-ty-stx (? identifier? bound-id))))
|
||||||
|
(unless (bound-index? (syntax-e bound-id))
|
||||||
|
(tc-error/stx bound-id "~a is not a type variable bound with ..." (syntax-e bound-id)))
|
||||||
|
(if (= (length ty-stxs) (sub1 (PolyDots-n ty)))
|
||||||
|
(let* ([last-id (syntax-e bound-id)]
|
||||||
|
[last-ty (extend-tvars (list last-id) (parse-type bound-ty-stx))])
|
||||||
|
(instantiate-poly-dotted ty (map parse-type ty-stxs) last-ty last-id))
|
||||||
|
(tc-error/expr #:return -Bottom "Wrong number of fixed type arguments to polymorphic type ~a:\nexpected: ~a\ngot: ~a"
|
||||||
|
ty (sub1 (PolyDots-n ty)) (length ty-stxs)))]
|
||||||
|
[stx-list
|
||||||
|
(instantiate-poly ty (map parse-type stx-list))])]
|
||||||
|
[else
|
||||||
|
(instantiate-poly ty (stx-map parse-type inst))]))
|
||||||
|
|
||||||
|
;; do-row-inst : Type ClassRow -> Type
|
||||||
|
;; Instantiate a row polymorphic function type
|
||||||
|
(define (do-row-inst ty row-stx)
|
||||||
|
;; At this point, we know `stx` represents a row so we can parse it.
|
||||||
|
;; The parsing is done here because if `inst` did the parsing, it's
|
||||||
|
;; too early and ends up with an empty type environment.
|
||||||
|
(define row
|
||||||
|
(syntax-parse row-stx
|
||||||
|
[(#:row (~var clauses (row-clauses parse-type)))
|
||||||
|
(attribute clauses.row)]))
|
||||||
|
(cond
|
||||||
|
[(not (PolyRow? ty))
|
||||||
|
(tc-error/expr #:return -Bottom "Cannot instantiate non-row-polymorphic type ~a"
|
||||||
|
(cleanup-type ty))]
|
||||||
|
[else
|
||||||
|
(match-define (PolyRow: _ constraints _) ty)
|
||||||
|
(check-row-constraints
|
||||||
|
row constraints
|
||||||
|
(λ (name)
|
||||||
|
(tc-error/expr
|
||||||
|
(~a "Cannot instantiate row with member " name
|
||||||
|
" that the given row variable requires to be absent"))))
|
||||||
|
(instantiate-poly ty (list row))]))
|
||||||
|
|
||||||
|
|
@ -7,7 +7,7 @@
|
||||||
"tc-app-combined.rkt"
|
"tc-app-combined.rkt"
|
||||||
"tc-if.rkt" "tc-lambda-unit.rkt"
|
"tc-if.rkt" "tc-lambda-unit.rkt"
|
||||||
"tc-let-unit.rkt" "tc-apply.rkt"
|
"tc-let-unit.rkt" "tc-apply.rkt"
|
||||||
"tc-literal.rkt"
|
"tc-literal.rkt" "tc-expression.rkt"
|
||||||
"tc-send.rkt"
|
"tc-send.rkt"
|
||||||
"tc-expr-unit.rkt" "check-subforms-unit.rkt"
|
"tc-expr-unit.rkt" "check-subforms-unit.rkt"
|
||||||
"check-class-unit.rkt")
|
"check-class-unit.rkt")
|
||||||
|
|
@ -17,4 +17,4 @@
|
||||||
(define-values/invoke-unit/infer
|
(define-values/invoke-unit/infer
|
||||||
(link tc-if@ tc-lambda@ tc-app-combined@ tc-let@ tc-expr@
|
(link tc-if@ tc-lambda@ tc-app-combined@ tc-let@ tc-expr@
|
||||||
tc-send@ check-subforms@ tc-apply@ tc-literal@
|
tc-send@ check-subforms@ tc-apply@ tc-literal@
|
||||||
check-class@))
|
check-class@ tc-expression@))
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue
Block a user