Move tc-literal to seperate file, as it doesn't belong in tc-expr.
(cherry picked from commit adbc516edf)
This commit is contained in:
Eric Dobson
Ryan Culpepper
parent
d5f288e0c2
commit
0503bcd7c6
|
|
@ -7,7 +7,6 @@
|
||||||
|
|
||||||
(define-signature tc-expr^
|
(define-signature tc-expr^
|
||||||
([cond-contracted tc-expr (syntax? . -> . tc-results/c)]
|
([cond-contracted tc-expr (syntax? . -> . tc-results/c)]
|
||||||
[cond-contracted tc-literal (->* (syntax?) ((or/c #f Type/c)) Type/c)]
|
|
||||||
[cond-contracted tc-expr/check (syntax? tc-results/c . -> . tc-results/c)]
|
[cond-contracted tc-expr/check (syntax? tc-results/c . -> . tc-results/c)]
|
||||||
[cond-contracted tc-expr/check/t (syntax? tc-results/c . -> . Type/c)]
|
[cond-contracted tc-expr/check/t (syntax? tc-results/c . -> . Type/c)]
|
||||||
[cond-contracted tc-exprs ((listof syntax?) . -> . tc-results/c)]
|
[cond-contracted tc-exprs ((listof syntax?) . -> . tc-results/c)]
|
||||||
|
|
@ -23,6 +22,9 @@
|
||||||
(define-signature tc-if^
|
(define-signature tc-if^
|
||||||
([cond-contracted tc/if-twoarm ((syntax? syntax? syntax?) (tc-results/c) . ->* . tc-results/c)]))
|
([cond-contracted tc/if-twoarm ((syntax? syntax? syntax?) (tc-results/c) . ->* . tc-results/c)]))
|
||||||
|
|
||||||
|
(define-signature tc-literal^
|
||||||
|
([cond-contracted tc-literal (->* (syntax?) ((or/c Type/c #f)) Type/c)]))
|
||||||
|
|
||||||
(define-signature tc-lambda^
|
(define-signature tc-lambda^
|
||||||
([cond-contracted tc/lambda (syntax? syntax? syntax? . -> . tc-results/c)]
|
([cond-contracted tc/lambda (syntax? syntax? syntax? . -> . tc-results/c)]
|
||||||
[cond-contracted tc/lambda/check (syntax? syntax? syntax? tc-results/c . -> . tc-results/c)]
|
[cond-contracted tc/lambda/check (syntax? syntax? syntax? tc-results/c . -> . tc-results/c)]
|
||||||
|
|
|
||||||
|
|
@ -19,7 +19,7 @@
|
||||||
(provide tc-app-combined@)
|
(provide tc-app-combined@)
|
||||||
|
|
||||||
(define-compound-unit/infer tc-app-combined@
|
(define-compound-unit/infer tc-app-combined@
|
||||||
(import tc-expr^ tc-lambda^ tc-let^ tc-apply^)
|
(import tc-expr^ tc-lambda^ tc-let^ tc-apply^ tc-literal^)
|
||||||
(export tc-app^)
|
(export tc-app^)
|
||||||
|
|
||||||
(link tc-app-main@
|
(link tc-app-main@
|
||||||
|
|
|
||||||
|
|
@ -15,7 +15,7 @@
|
||||||
(rep type-rep rep-utils)
|
(rep type-rep rep-utils)
|
||||||
(for-template racket/unsafe/ops racket/base))
|
(for-template racket/unsafe/ops racket/base))
|
||||||
|
|
||||||
(import tc-expr^ tc-app^)
|
(import tc-expr^ tc-app^ tc-literal^)
|
||||||
(export tc-app-hetero^)
|
(export tc-app-hetero^)
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -20,109 +20,9 @@
|
||||||
|
|
||||||
(require (for-template racket/base racket/private/class-internal))
|
(require (for-template racket/base racket/private/class-internal))
|
||||||
|
|
||||||
(import tc-if^ tc-lambda^ tc-app^ tc-let^ check-subforms^)
|
(import tc-if^ tc-lambda^ tc-app^ tc-let^ check-subforms^ tc-literal^)
|
||||||
(export tc-expr^)
|
(export tc-expr^)
|
||||||
|
|
||||||
;; return the type of a literal value
|
|
||||||
;; racket-value [type] -> type
|
|
||||||
(define (tc-literal v-stx [expected #f])
|
|
||||||
(define-syntax-class exp
|
|
||||||
(pattern (~and i (~or :number :str :bytes))
|
|
||||||
#:fail-unless expected #f
|
|
||||||
#:fail-unless (subtype (-val (syntax-e #'i)) expected) #f))
|
|
||||||
(syntax-parse v-stx
|
|
||||||
[i:exp expected]
|
|
||||||
[i:boolean (-val (syntax-e #'i))]
|
|
||||||
[i:identifier (-val (syntax-e #'i))]
|
|
||||||
;; Numbers
|
|
||||||
[0 -Zero]
|
|
||||||
[1 -One]
|
|
||||||
[(~var i (3d (conjoin byte? positive?))) -PosByte]
|
|
||||||
[(~var i (3d byte?)) -Byte]
|
|
||||||
[(~var i (3d (conjoin portable-index? positive?))) -PosIndex]
|
|
||||||
[(~var i (3d (conjoin portable-fixnum? positive?))) -PosFixnum]
|
|
||||||
[(~var i (3d (conjoin portable-fixnum? negative?))) -NegFixnum]
|
|
||||||
[(~var i (3d exact-positive-integer?)) -PosInt]
|
|
||||||
[(~var i (3d (conjoin exact-integer? negative?))) -NegInt]
|
|
||||||
[(~var i (3d (conjoin number? exact? rational? positive?))) -PosRat]
|
|
||||||
[(~var i (3d (conjoin number? exact? rational? negative?))) -NegRat]
|
|
||||||
[(~var i (3d (lambda (x) (eqv? x 0.0)))) -FlonumPosZero]
|
|
||||||
[(~var i (3d (lambda (x) (eqv? x -0.0)))) -FlonumNegZero]
|
|
||||||
[(~var i (3d (lambda (x) (eqv? x +nan.0)))) -FlonumNan]
|
|
||||||
[(~var i (3d(lambda (x) (eqv? x +inf.0)))) (-val +inf.0)]
|
|
||||||
[(~var i (3d (lambda (x) (eqv? x -inf.0)))) (-val -inf.0)]
|
|
||||||
[(~var i (3d (conjoin flonum? positive?))) -PosFlonum]
|
|
||||||
[(~var i (3d (conjoin flonum? negative?))) -NegFlonum]
|
|
||||||
[(~var i (3d flonum?)) -Flonum] ; for nan
|
|
||||||
[(~var i (3d (lambda (x) (eqv? x 0.0f0)))) -SingleFlonumPosZero]
|
|
||||||
[(~var i (3d (lambda (x) (eqv? x -0.0f0)))) -SingleFlonumNegZero]
|
|
||||||
[(~var i (3d (lambda (x) (eqv? x +nan.f)))) -SingleFlonumNan]
|
|
||||||
[(~var i (3d(lambda (x) (eqv? x +inf.f)))) (-val +inf.f)]
|
|
||||||
[(~var i (3d (lambda (x) (eqv? x -inf.f)))) (-val -inf.f)]
|
|
||||||
[(~var i (3d (conjoin single-flonum? positive?))) -PosSingleFlonum]
|
|
||||||
[(~var i (3d (conjoin single-flonum? negative?))) -NegSingleFlonum]
|
|
||||||
[(~var i (3d single-flonum?)) -SingleFlonum] ; for nan
|
|
||||||
[(~var i (3d inexact-real?)) -InexactReal] ; catch-all, just in case
|
|
||||||
[(~var i (3d real?)) -Real] ; catch-all, just in case
|
|
||||||
;; a complex number can't have a float imaginary part and an exact real part
|
|
||||||
[(~var i (3d (conjoin number? exact?)))
|
|
||||||
-ExactNumber]
|
|
||||||
[(~var i (3d (conjoin number? (lambda (x) (and (flonum? (imag-part x))
|
|
||||||
(flonum? (real-part x)))))))
|
|
||||||
-FloatComplex]
|
|
||||||
[(~var i (3d (conjoin number? (lambda (x) (and (single-flonum? (imag-part x))
|
|
||||||
(single-flonum? (real-part x)))))))
|
|
||||||
-SingleFlonumComplex]
|
|
||||||
;; can't have real and imaginary parts that are both inexact, but not the same precision
|
|
||||||
[(~var i (3d number?)) -Number] ; otherwise, Number
|
|
||||||
|
|
||||||
[i:str -String]
|
|
||||||
[i:char -Char]
|
|
||||||
[i:keyword (-val (syntax-e #'i))]
|
|
||||||
[i:bytes -Bytes]
|
|
||||||
[i:byte-pregexp -Byte-PRegexp]
|
|
||||||
[i:byte-regexp -Byte-Regexp]
|
|
||||||
[i:pregexp -PRegexp]
|
|
||||||
[i:regexp -Regexp]
|
|
||||||
[(~and i ()) (-val '())]
|
|
||||||
[(i . r)
|
|
||||||
(match (and expected (restrict expected (-pair Univ Univ) 'orig))
|
|
||||||
[(Pair: a-ty d-ty)
|
|
||||||
(-pair
|
|
||||||
(tc-literal #'i a-ty)
|
|
||||||
(tc-literal #'r d-ty))]
|
|
||||||
[t
|
|
||||||
(-pair (tc-literal #'i) (tc-literal #'r))])]
|
|
||||||
[(~var i (3d vector?))
|
|
||||||
(match (and expected (restrict expected (-vec Univ) 'orig))
|
|
||||||
[(Vector: t)
|
|
||||||
(make-Vector (apply Un
|
|
||||||
t ;; so that this isn't (Un) when we get no elems
|
|
||||||
(for/list ([l (in-vector (syntax-e #'i))])
|
|
||||||
(tc-literal l t))))]
|
|
||||||
[(HeterogeneousVector: ts)
|
|
||||||
(make-HeterogeneousVector
|
|
||||||
(for/list ([l (in-vector (syntax-e #'i))]
|
|
||||||
[t (in-list ts)])
|
|
||||||
check-below (tc-literal l t) t))]
|
|
||||||
[_ (make-HeterogeneousVector (for/list ([l (syntax-e #'i)])
|
|
||||||
(generalize (tc-literal l #f))))])]
|
|
||||||
[(~var i (3d hash?))
|
|
||||||
(match expected
|
|
||||||
[(Hashtable: k v)
|
|
||||||
(let* ([h (syntax-e #'i)]
|
|
||||||
[ks (hash-map h (lambda (x y) (tc-literal x k)))]
|
|
||||||
[vs (hash-map h (lambda (x y) (tc-literal y v)))])
|
|
||||||
(check-below (apply Un ks) k)
|
|
||||||
(check-below (apply Un vs) v)
|
|
||||||
expected)]
|
|
||||||
[_ (let* ([h (syntax-e #'i)]
|
|
||||||
[ks (hash-map h (lambda (x y) (tc-literal x)))]
|
|
||||||
[vs (hash-map h (lambda (x y) (tc-literal y)))])
|
|
||||||
(make-Hashtable (generalize (apply Un ks)) (generalize (apply Un vs))))])]
|
|
||||||
[_ Univ]))
|
|
||||||
|
|
||||||
|
|
||||||
;; do-inst : syntax type -> type
|
;; do-inst : syntax type -> type
|
||||||
(define (do-inst stx ty)
|
(define (do-inst stx ty)
|
||||||
(define inst (syntax-property stx 'type-inst))
|
(define inst (syntax-property stx 'type-inst))
|
||||||
|
|
|
||||||
117
collects/typed-racket/typecheck/tc-literal.rkt
Normal file
117
collects/typed-racket/typecheck/tc-literal.rkt
Normal file
|
|
@ -0,0 +1,117 @@
|
||||||
|
#lang racket/unit
|
||||||
|
|
||||||
|
(require "../utils/utils.rkt"
|
||||||
|
racket/match
|
||||||
|
(typecheck signatures check-below)
|
||||||
|
(types abbrev numeric-tower utils subtype union generalize)
|
||||||
|
(rep type-rep)
|
||||||
|
(only-in (infer infer) restrict)
|
||||||
|
(utils tc-utils stxclass-util)
|
||||||
|
syntax/parse
|
||||||
|
unstable/function)
|
||||||
|
|
||||||
|
(import)
|
||||||
|
(export tc-literal^)
|
||||||
|
|
||||||
|
;; return the type of a literal value
|
||||||
|
;; tc-literal: racket-value-syntax [type] -> type
|
||||||
|
(define (tc-literal v-stx [expected #f])
|
||||||
|
(define-syntax-class exp
|
||||||
|
(pattern (~and i (~or :number :str :bytes))
|
||||||
|
#:fail-unless expected #f
|
||||||
|
#:fail-unless (subtype (-val (syntax-e #'i)) expected) #f))
|
||||||
|
(syntax-parse v-stx
|
||||||
|
[i:exp expected]
|
||||||
|
[i:boolean (-val (syntax-e #'i))]
|
||||||
|
[i:identifier (-val (syntax-e #'i))]
|
||||||
|
;; Numbers
|
||||||
|
[0 -Zero]
|
||||||
|
[1 -One]
|
||||||
|
[(~var i (3d (conjoin byte? positive?))) -PosByte]
|
||||||
|
[(~var i (3d byte?)) -Byte]
|
||||||
|
[(~var i (3d (conjoin portable-index? positive?))) -PosIndex]
|
||||||
|
[(~var i (3d (conjoin portable-fixnum? positive?))) -PosFixnum]
|
||||||
|
[(~var i (3d (conjoin portable-fixnum? negative?))) -NegFixnum]
|
||||||
|
[(~var i (3d exact-positive-integer?)) -PosInt]
|
||||||
|
[(~var i (3d (conjoin exact-integer? negative?))) -NegInt]
|
||||||
|
[(~var i (3d (conjoin number? exact? rational? positive?))) -PosRat]
|
||||||
|
[(~var i (3d (conjoin number? exact? rational? negative?))) -NegRat]
|
||||||
|
[(~var i (3d (lambda (x) (eqv? x 0.0)))) -FlonumPosZero]
|
||||||
|
[(~var i (3d (lambda (x) (eqv? x -0.0)))) -FlonumNegZero]
|
||||||
|
[(~var i (3d (lambda (x) (eqv? x +nan.0)))) -FlonumNan]
|
||||||
|
[(~var i (3d(lambda (x) (eqv? x +inf.0)))) (-val +inf.0)]
|
||||||
|
[(~var i (3d (lambda (x) (eqv? x -inf.0)))) (-val -inf.0)]
|
||||||
|
[(~var i (3d (conjoin flonum? positive?))) -PosFlonum]
|
||||||
|
[(~var i (3d (conjoin flonum? negative?))) -NegFlonum]
|
||||||
|
[(~var i (3d flonum?)) -Flonum] ; for nan
|
||||||
|
[(~var i (3d (lambda (x) (eqv? x 0.0f0)))) -SingleFlonumPosZero]
|
||||||
|
[(~var i (3d (lambda (x) (eqv? x -0.0f0)))) -SingleFlonumNegZero]
|
||||||
|
[(~var i (3d (lambda (x) (eqv? x +nan.f)))) -SingleFlonumNan]
|
||||||
|
[(~var i (3d(lambda (x) (eqv? x +inf.f)))) (-val +inf.f)]
|
||||||
|
[(~var i (3d (lambda (x) (eqv? x -inf.f)))) (-val -inf.f)]
|
||||||
|
[(~var i (3d (conjoin single-flonum? positive?))) -PosSingleFlonum]
|
||||||
|
[(~var i (3d (conjoin single-flonum? negative?))) -NegSingleFlonum]
|
||||||
|
[(~var i (3d single-flonum?)) -SingleFlonum] ; for nan
|
||||||
|
[(~var i (3d inexact-real?)) -InexactReal] ; catch-all, just in case
|
||||||
|
[(~var i (3d real?)) -Real] ; catch-all, just in case
|
||||||
|
;; a complex number can't have a float imaginary part and an exact real part
|
||||||
|
[(~var i (3d (conjoin number? exact?)))
|
||||||
|
-ExactNumber]
|
||||||
|
[(~var i (3d (conjoin number? (lambda (x) (and (flonum? (imag-part x))
|
||||||
|
(flonum? (real-part x)))))))
|
||||||
|
-FloatComplex]
|
||||||
|
[(~var i (3d (conjoin number? (lambda (x) (and (single-flonum? (imag-part x))
|
||||||
|
(single-flonum? (real-part x)))))))
|
||||||
|
-SingleFlonumComplex]
|
||||||
|
;; can't have real and imaginary parts that are both inexact, but not the same precision
|
||||||
|
[(~var i (3d number?)) -Number] ; otherwise, Number
|
||||||
|
|
||||||
|
[i:str -String]
|
||||||
|
[i:char -Char]
|
||||||
|
[i:keyword (-val (syntax-e #'i))]
|
||||||
|
[i:bytes -Bytes]
|
||||||
|
[i:byte-pregexp -Byte-PRegexp]
|
||||||
|
[i:byte-regexp -Byte-Regexp]
|
||||||
|
[i:pregexp -PRegexp]
|
||||||
|
[i:regexp -Regexp]
|
||||||
|
[(~and i ()) (-val '())]
|
||||||
|
[(i . r)
|
||||||
|
(match (and expected (restrict expected (-pair Univ Univ) 'orig))
|
||||||
|
[(Pair: a-ty d-ty)
|
||||||
|
(-pair
|
||||||
|
(tc-literal #'i a-ty)
|
||||||
|
(tc-literal #'r d-ty))]
|
||||||
|
[t
|
||||||
|
(-pair (tc-literal #'i) (tc-literal #'r))])]
|
||||||
|
[(~var i (3d vector?))
|
||||||
|
(match (and expected (restrict expected (-vec Univ) 'orig))
|
||||||
|
[(Vector: t)
|
||||||
|
(make-Vector (apply Un
|
||||||
|
t ;; so that this isn't (Un) when we get no elems
|
||||||
|
(for/list ([l (in-vector (syntax-e #'i))])
|
||||||
|
(tc-literal l t))))]
|
||||||
|
[(HeterogeneousVector: ts)
|
||||||
|
(make-HeterogeneousVector
|
||||||
|
(for/list ([l (in-vector (syntax-e #'i))]
|
||||||
|
[t (in-list ts)])
|
||||||
|
check-below (tc-literal l t) t))]
|
||||||
|
[_ (make-HeterogeneousVector (for/list ([l (syntax-e #'i)])
|
||||||
|
(generalize (tc-literal l #f))))])]
|
||||||
|
[(~var i (3d hash?))
|
||||||
|
(match expected
|
||||||
|
[(Hashtable: k v)
|
||||||
|
(let* ([h (syntax-e #'i)]
|
||||||
|
[ks (hash-map h (lambda (x y) (tc-literal x k)))]
|
||||||
|
[vs (hash-map h (lambda (x y) (tc-literal y v)))])
|
||||||
|
(check-below (apply Un ks) k)
|
||||||
|
(check-below (apply Un vs) v)
|
||||||
|
expected)]
|
||||||
|
[_ (let* ([h (syntax-e #'i)]
|
||||||
|
[ks (hash-map h (lambda (x y) (tc-literal x)))]
|
||||||
|
[vs (hash-map h (lambda (x y) (tc-literal y)))])
|
||||||
|
(make-Hashtable (generalize (apply Un ks)) (generalize (apply Un vs))))])]
|
||||||
|
[_ Univ]))
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -9,10 +9,11 @@
|
||||||
"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-expr-unit.rkt" "check-subforms-unit.rkt")
|
"tc-expr-unit.rkt" "check-subforms-unit.rkt")
|
||||||
|
|
||||||
(provide-signature-elements tc-expr^ check-subforms^)
|
(provide-signature-elements tc-expr^ check-subforms^ tc-literal^)
|
||||||
|
|
||||||
(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@
|
||||||
check-subforms@ tc-apply@))
|
check-subforms@ tc-apply@ tc-literal@))
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue
Block a user