suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Remove trailing whitespace.

Browse Source 
original commit: 3b036388d64c33a63bad18e53341b54bac719b1a
This commit is contained in:
Vincent St-Amour 2011-05-18 15:02:28 -04:00
parent 794bfe775b
commit 7e441e8e31
74 changed files with 740 additions and 740 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/typed-scheme/base-env/annotate-classes.rkt
View File

@ -70,7 +70,7 @@
(define-splicing-syntax-class annotated-star-rest
#:attributes (name ann-name ty formal-ty)
#:literals (:)
#:literals (:)
(pattern (~seq name:id : ty s:star)
#:with formal-ty #'(ty s)
#:with ann-name (syntax-property #'name 'type-label #'ty)))

34
collects/typed-scheme/base-env/base-env-indexing-abs.rkt
View File

@ -1,9 +1,9 @@
#lang racket
(require
"../utils/utils.rkt"
"../utils/utils.rkt"
(for-template '#%paramz racket/base racket/list
racket/tcp
racket/tcp
(only-in rnrs/lists-6 fold-left)
'#%paramz
(only-in '#%kernel [apply kernel:apply])
@ -12,17 +12,17 @@
(only-in racket/match/runtime match:error matchable? match-equality-test)
racket/unsafe/ops)
(utils tc-utils)
(types union convenience)
(types union convenience)
(rename-in (types abbrev numeric-tower) [-Number N] [-Boolean B] [-Symbol Sym]))
(provide indexing)
(define-syntax-rule (indexing index-type)
(make-env
[build-list (-poly (a) (index-type (-Index . -> . a) . -> . (-lst a)))]
[make-list (-poly (a) (index-type a . -> . (-lst a)))]
[string-ref (-> -String index-type -Char)]
[substring (->opt -String index-type [index-type] -String)]
[make-string (cl-> [(index-type) -String] [(index-type -Char) -String])]
@ -57,10 +57,10 @@
[(-Bytes -Output-Port index-type index-type) -Index])]
[list-ref (-poly (a) ((-lst a) index-type . -> . a))]
[list-tail (-poly (a) ((-lst a) index-type . -> . (-lst a)))]
[regexp-match
(let ([?outp (-opt -Output-Port)]
[N index-type]
@ -100,7 +100,7 @@
[?N (-opt index-type)]
[optlist (lambda (t) (-opt (-lst (-opt t))))])
(->opt -Pattern -Input-Port [index-type ?N ?outp] (optlist -Bytes)))]
[regexp-match-positions
(let ([?outp (-opt -Output-Port)]
[N index-type]
@ -118,8 +118,8 @@
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -Bytes)])
(->opt -Pattern (Un -String -InpBts) [index-type ?N ?outp] (-lst (-pair -Index -Index))))]
[take (-poly (a) ((-lst a) index-type . -> . (-lst a)))]
[drop (-poly (a) ((-lst a) index-type . -> . (-lst a)))]
[take-right (-poly (a) ((-lst a) index-type . -> . (-lst a)))]
@ -128,7 +128,7 @@
(-poly (a) ((list (-lst a)) index-type . ->* . (-values (list (-lst a) (-lst a)))))]
[split-at-right
(-poly (a) ((list (-lst a)) index-type . ->* . (-values (list (-lst a) (-lst a)))))]
[vector-ref (-poly (a) ((-vec a) index-type . -> . a))]
[unsafe-vector-ref (-poly (a) ((-vec a) index-type . -> . a))]
[unsafe-vector*-ref (-poly (a) ((-vec a) index-type . -> . a))]
@ -160,21 +160,21 @@
[integer->integer-bytes (-Integer index-type Univ [Univ -Bytes index-type] . ->opt . -Bytes)]
[integer-bytes->integer (-Bytes Univ [Univ index-type index-type] . ->opt . -Integer)]
[peek-char
(cl->* [->opt [-Input-Port index-type] (Un -Char (-val eof))])]
[peek-byte
(cl->* [->opt [-Input-Port index-type] (Un -Byte (-val eof))])]
;; string.rkt
[real->decimal-string (-Real [index-type] . ->opt . -String)]
[random (cl-> [(index-type) -Nat] [() -Real])]
[raise-type-error
(cl->*
[-> Sym -String Univ (Un)]
[->* (list Sym -String index-type) Univ (Un)])]
))

84
collects/typed-scheme/base-env/base-env.rkt
View File

@ -1,9 +1,9 @@
#lang s-exp "env-lang.rkt"
(require
(for-template
(for-template
(except-in racket -> ->* one-of/c)
racket/unsafe/ops
racket/tcp
@ -13,7 +13,7 @@
'#%paramz
"extra-procs.rkt"
(only-in '#%kernel [apply kernel:apply])
(only-in racket/private/pre-base new-apply-proc)
(only-in racket/private/pre-base new-apply-proc)
scheme/promise scheme/system
racket/function
racket/mpair
@ -31,7 +31,7 @@
make-HeterogenousVector))
[raise (Univ . -> . (Un))]
[raise-syntax-error (cl->*
[raise-syntax-error (cl->*
(-> (Un (-val #f) -Symbol)
-String
(Un))
@ -45,11 +45,11 @@
Univ
(Un)))]
[car (-poly (a b)
[car (-poly (a b)
(cl->*
(->acc (list (-pair a b)) a (list -car))
(->* (list (-lst a)) a)))]
[cdr (-poly (a b)
[cdr (-poly (a b)
(cl->*
(->acc (list (-pair a b)) b (list -cdr))
(->* (list (-lst a)) (-lst a))))]
@ -147,7 +147,7 @@
[-> (-lst a) (-lst a)]))]
[first (-poly (a b)
[first (-poly (a b)
(cl->*
(->acc (list (-pair a (-lst b))) a (list -car))
(->* (list (-lst a)) a)))]
@ -164,7 +164,7 @@
[eighth (-poly (a) ((-lst a) . -> . a))]
[ninth (-poly (a) ((-lst a) . -> . a))]
[tenth (-poly (a) ((-lst a) . -> . a))]
[rest (-poly (a b)
[rest (-poly (a b)
(cl->*
(->acc (list (-pair a (-lst b))) (-lst b) (list -cdr))
(->* (list (-lst a)) (-lst a))))]
@ -245,11 +245,11 @@
[list? (make-pred-ty (-lst Univ))]
[list (-poly (a) (->* '() a (-lst a)))]
[procedure? (make-pred-ty top-func)]
[map (-polydots (c a b)
[map (-polydots (c a b)
(cl->*
(-> (-> a c) (-pair a (-lst a)) (-pair c (-lst c)))
((list
((list a) (b b) . ->... . c)
((list
((list a) (b b) . ->... . c)
(-lst a))
((-lst b) b) . ->... .(-lst c))))]
[for-each (-polydots (c a b) ((list ((list a) (b b) . ->... . Univ) (-lst a))
@ -282,8 +282,8 @@
[remq* (-poly (a) (cl-> [((-lst a) (-lst a)) (-lst a)]))]
[remv* (-poly (a) (cl-> [((-lst a) (-lst a)) (-lst a)]))]
(error
(make-Function (list
(error
(make-Function (list
(make-arr (list Sym -String) (Un) #:rest Univ)
(make-arr (list -String) (Un) #:rest Univ)
(make-arr (list Sym) (Un)))))
@ -396,12 +396,12 @@
[with-input-from-file
(-poly (a) (->key -Pathlike (-> a) #:mode (one-of/c 'binary 'text) #f a))]
[with-output-to-file
(-poly (a) (->key -Pathlike (-> a)
(-poly (a) (->key -Pathlike (-> a)
#:exists (one-of/c 'error 'append 'update 'can-update
'replace 'truncate
'must-truncate 'truncate/replace)
#f
#:mode (one-of/c 'binary 'text) #f
#:mode (one-of/c 'binary 'text) #f
a))]
@ -416,15 +416,15 @@
[kernel:apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
[time-apply (-poly (a b c)
(cl->*
(->
(->
(-> a)
(-Tuple (list))
(-values (list (-pair a (-val '())) -Nat -Nat -Nat)))
(->
(->
(-> b a)
(-Tuple (list b))
(-values (list (-pair a (-val '())) -Nat -Nat -Nat)))
(->
(->
(-> b c a)
(-Tuple (list b c))
(-values (list (-pair a (-val '())) -Nat -Nat -Nat)))))]
@ -521,7 +521,7 @@
[call-with-input-file (-poly (a) (-Pathlike (-Input-Port . -> . a) #:mode (Un (-val 'binary) (-val 'text)) #f . ->key . a))]
[call-with-output-file (-poly (a) (-Pathlike (-Output-Port . -> . a)
#:exists (one-of/c error 'append 'update 'replace 'truncate 'truncate/replace) #f
#:mode (Un (-val 'binary) (-val 'text)) #f
#:mode (Un (-val 'binary) (-val 'text)) #f
. ->key . a))]
[current-output-port (-Param -Output-Port -Output-Port)]
@ -571,7 +571,7 @@
[build-path (cl->*
((list -Pathlike*) -Pathlike* . ->* . -Path)
((list -SomeSystemPathlike*) -SomeSystemPathlike* . ->* . -SomeSystemPath))]
[build-path/convention-type
[build-path/convention-type
((list -PathConventionType -SomeSystemPathlike*) -SomeSystemPathlike* . ->* . -SomeSystemPath)]
[absolute-path? (-> -SomeSystemPath B)]
@ -583,18 +583,18 @@
(-> -Pathlike -Pathlike -Path)
(-> -SomeSystemPathlike -SomeSystemPathlike -SomeSystemPath))]
[path->directory-path
[path->directory-path
(cl->* (-> -Pathlike -Path)
(-> -SomeSystemPathlike -SomeSystemPath))]
[resolve-path (-> -Path -Path)]
[cleanse-path
[cleanse-path
(cl->* (-> -Pathlike -Path)
(-> -SomeSystemPathlike -SomeSystemPath))]
[expand-user-path (-> -Path -Path)]
[simplify-path
(cl->*
(cl->*
(-Pathlike . -> . -Path)
(-Pathlike B . -> . -Path)
(-SomeSystemPathlike B . -> . -SomeSystemPath))]
@ -616,12 +616,12 @@
(Un -SomeSystemPath (-val 'up) (-val 'same))
B))))]
[path-replace-suffix
[path-replace-suffix
(cl->*
(-> -Pathlike (Un -String -Bytes) -Path)
(-> -SomeSystemPathlike (Un -String -Bytes) -SomeSystemPath))]
[path-add-suffix
[path-add-suffix
(cl->*
(-> -Pathlike (Un -String -Bytes) -Path)
(-> -SomeSystemPathlike (Un -String -Bytes) -SomeSystemPath))]
@ -776,14 +776,14 @@
[syntax-source (-> (-Syntax Univ) Univ)]
[syntax-position (-> (-Syntax Univ) (-opt N))]
[datum->syntax
[datum->syntax
(let* ([Pre Syntax-Sexp]
[I (-Syntax Sym)]
[A Any-Syntax]
[S (-Syntax Univ)]
[ctxt (-opt S)]
[srclist (-Tuple (list
Univ
Univ
(-opt -Integer)
(-opt -Integer)
(-opt -Integer)
@ -840,7 +840,7 @@
[parse-command-line
(let ([mode-sym (one-of/c 'once-each 'once-any 'multi 'final 'help-labels)])
(-polydots (b a)
(cl->* (-Pathlike
(cl->* (-Pathlike
(Un (-lst -String) (-vec -String))
(-lst (-pair mode-sym (-lst (-lst Univ))))
((list Univ) [a a] . ->... . b)
@ -852,8 +852,8 @@
((list
((list a) (b b) . ->... . Univ)
(-lst a))
((-lst b) b)
. ->... .
((-lst b) b)
. ->... .
-Index))]
[filter-map (-polydots (c a b)
((list
@ -864,7 +864,7 @@
[add-between (-poly (a b) ((-lst a) b . -> . (-lst (Un a b))))]
[last-pair (-poly (a) ((-mu x (Un a (-val '()) (-pair a x)))
. -> .
. -> .
(Un (-pair a a) (-pair a (-val '())))))]
[remove-duplicates
(-poly (a)
@ -929,15 +929,15 @@
[file-name-from-path (-Pathlike . -> . (-opt -Path))]
[path-only (-SomeSystemPathlike . -> . (-opt -Path))]
[some-system-path->string (-SomeSystemPath . -> . -String)]
[string->some-system-path
[string->some-system-path
(-String (Un (-val 'unix) (-val 'windows)) . -> . -SomeSystemPath)]
;; scheme/file
[fold-files
(-poly
(a)
[fold-files
(-poly
(a)
(let ([funarg* (-Path (one-of/c 'file 'dir 'link) a . -> . (-values (list a Univ)))]
[funarg (-Path (one-of/c 'file 'dir 'link) a . -> . a)])
(cl->*
@ -955,11 +955,11 @@
[unsafe-vector-length ((make-VectorTop) . -> . -Index)]
[unsafe-vector*-length ((make-VectorTop) . -> . -Index)]
[unsafe-car (-poly (a b)
[unsafe-car (-poly (a b)
(cl->*
(->acc (list (-pair a b)) a (list -car))
(->* (list (-lst a)) a)))]
[unsafe-cdr (-poly (a b)
[unsafe-cdr (-poly (a b)
(cl->*
(->acc (list (-pair a b)) b (list -cdr))
(->* (list (-lst a)) (-lst a))))]
@ -971,7 +971,7 @@
((list a) (b b) . ->... . Univ)
(-vec a))
((-vec b) b)
. ->... .
. ->... .
-Index))]
[vector-filter (-poly (a b) (cl->*
((make-pred-ty (list a) Univ b)
@ -983,7 +983,7 @@
[vector-filter-not
(-poly (a b) (cl->* ((a . -> . Univ) (-vec a) . -> . (-vec a))))]
[vector-copy
(-poly (a)
(-poly (a)
(cl->* ((-vec a) . -> . (-vec a))
((-vec a) -Integer . -> . (-vec a))
((-vec a) -Integer -Integer . -> . (-vec a))))]
@ -1023,14 +1023,14 @@
[write-special (cl-> [(Univ) -Boolean]
[(Univ -Output-Port) -Boolean])]
;; Need event type before we can include these
;;write-special-avail*
;;write-special-avail*
;;write-bytes-avail-evt
;;write-special-evt
[port-writes-atomic? (-Output-Port . -> . -Boolean)]
[port-writes-special? (-Output-Port . -> . -Boolean)]
;; probably the most useful cases
[curry (-poly (a b c)
[curry (-poly (a b c)
(cl->* ((a b . -> . c) a . -> . (b . -> . c))
((a b . -> . c) . -> . (a . -> . (b . -> . c)))))]
;; mutable pairs

18
collects/typed-scheme/base-env/base-special-env.rkt
View File

@ -4,10 +4,10 @@
(require
"../utils/utils.rkt"
racket/promise
string-constants/string-constant
string-constants/string-constant
(for-syntax racket/base syntax/parse (only-in racket/syntax syntax-local-eval)
(utils tc-utils)
(env init-envs)
(env init-envs)
(except-in (rep filter-rep object-rep type-rep) make-arr)
(types convenience union)
(only-in (types convenience) [make-arr* make-arr])))
@ -42,7 +42,7 @@
[(syntax-parse (local-expand #'`(,@'() 1) 'expression null)
#:context #'qq-append
[(_ qqa . _) #'qqa])
(-poly (a b)
(-poly (a b)
(cl->*
(-> (-lst a) (-val '()) (-lst a))
(-> (-lst a) (-lst b) (-lst (*Un a b)))))]
@ -53,9 +53,9 @@
[(let-values ([_ (m-s '(_) '())]) . _)
#'m-s])
(-poly (a b)
(let ([seq-vals
(let ([seq-vals
(lambda (a)
(-values (list
(-values (list
(-> Univ (-values a))
(-> Univ Univ)
Univ
@ -139,7 +139,7 @@
[(i-n _ ...)
#'i-n])
(->opt [-Input-Port -Symbol] (-seq -Bytes))]
;; from the expansion of `with-syntax'
[(syntax-parse (local-expand #'(with-syntax ([x 1]) #'(x)) 'expression null)
#:literals (let-values #%plain-app #%plain-lambda if letrec-syntaxes+values)
@ -151,11 +151,11 @@
_))))
#'apply-pattern-substitute])
(->* (list (-Syntax Univ) Univ) Univ Any-Syntax)]
[(syntax-parse (local-expand #'(with-syntax ([x 1]) #'(x)) 'expression null)
#:literals (let-values #%plain-app #%plain-lambda if letrec-syntaxes+values)
[(let-values _ (let-values _
(let-values _ (if _ _ (let-values _
[(let-values _ (let-values _
(let-values _ (if _ _ (let-values _
(if _ (let-values _ (letrec-syntaxes+values _ _ (#%plain-app with-syntax-fail _))) _))))))
#'with-syntax-fail])
(-> (-Syntax Univ) (Un))]

16
collects/typed-scheme/base-env/base-structs.rkt
View File

@ -1,12 +1,12 @@
#lang racket/base
(require
(require
"../utils/utils.rkt"
(utils tc-utils)
(env init-envs)
(env init-envs)
(except-in (rep filter-rep object-rep type-rep) make-arr)
(types convenience union)
(only-in (types convenience) [make-arr* make-arr])
(only-in (types convenience) [make-arr* make-arr])
(typecheck tc-structs))
(require (for-template racket/base))
@ -38,7 +38,7 @@
(define (initialize-structs)
(define-hierarchy srcloc
([source : Univ]
@ -47,24 +47,24 @@
[position : (*Un -Integer (-val #f))]
[span : (*Un -Integer (-val #f))]))
(define-hierarchy date
(define-hierarchy date
([second : -Number]
[minute : -Number]
[hour : -Number]
[day : -Number]
[month : -Number]
[month : -Number]
[year : -Number]
[weekday : -Number]
[year-day : -Number]
[dst? : -Boolean]
[time-zone-offset : -Number]))
(define-hierarchy arity-at-least
([value : -Nat]))
(define-hierarchy exn
([message : -String] [continuation-marks : -Cont-Mark-Set])
(define-hierarchy exn:break ([continuation : top-func]))
(define-hierarchy exn:fail ()

4
collects/typed-scheme/base-env/base-types-extra.rkt
View File

@ -5,8 +5,8 @@
(define-syntax (define-other-types stx)
(syntax-case stx ()
[(_ nm ...)
#'(begin (define-syntax nm
(lambda (stx)
#'(begin (define-syntax nm
(lambda (stx)
(raise-syntax-error 'type-check "type name used out of context" stx))) ...
(provide nm) ...)]))

8
collects/typed-scheme/base-env/colon.rkt
View File

@ -15,19 +15,19 @@
;; explicitly parenthesized
(syntax-parse stx #:literals (: t:->)
[(: id : x ...)
#:fail-unless (= 1 (length
#:fail-unless (= 1 (length
(for/list ([i (syntax->list #'(x ...))]
#:when (and (identifier? i)
(free-identifier=? i #'t:->)))
i))) #f
i))) #f
(syntax/loc stx (: id (x ...)))]
[(: id : . more)
(syntax/loc stx (: id . more))]
[_ stx]))
(define (err str . sub)
(apply raise-syntax-error '|type declaration| str stx sub))
(apply raise-syntax-error '|type declaration| str stx sub))
(syntax-parse stx*
[_
[_
#:when (eq? 'expression (syntax-local-context))
(err "must be used in a definition context")]
[(_ i:id ty)

4
collects/typed-scheme/base-env/env-lang.rkt
View File

@ -4,7 +4,7 @@
(require (for-syntax scheme/base syntax/parse)
(utils tc-utils)
(env init-envs)
(env init-envs)
(r:infer infer)
(only-in (r:infer infer-dummy) infer-param)
(except-in (rep object-rep filter-rep type-rep) make-arr)
@ -33,5 +33,5 @@
(provide (rename-out [-#%module-begin #%module-begin])
require
(except-out (all-from-out scheme/base) #%module-begin)
types rep private utils
types rep private utils
(types-out convenience union filter-ops))

72
collects/typed-scheme/base-env/prims.rkt
View File

@ -4,7 +4,7 @@
This file defines two sorts of primitives. All of them are provided into any module using the typed racket language.
1. macros for defining type annotated code.
1. macros for defining type annotated code.
this includes: lambda:, define:, etc
potentially, these macros should be replacements for the mzscheme ones in the user program
however, it's nice to be able to use both when the sugar is more limited
@ -35,7 +35,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
"base-types-extra.rkt"
racket/flonum ; for for/flvector and for*/flvector
mzlib/etc
(for-syntax
(for-syntax
syntax/parse
racket/syntax
racket/base
@ -45,7 +45,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
"../private/parse-type.rkt"
"annotate-classes.rkt"
"internal.rkt"
"../utils/tc-utils.rkt"
"../utils/tc-utils.rkt"
"../env/type-name-env.rkt"
"../private/type-contract.rkt"
"for-clauses.rkt")
@ -84,9 +84,9 @@ This file defines two sorts of primitives. All of them are provided into any mod
[(_ lib:expr (~or sc:simple-clause strc:struct-clause oc:opaque-clause) ...)
(unless (< 0 (length (syntax->list #'(sc ... strc ... oc ...))))
(raise-syntax-error #f "at least one specification is required" stx))
#'(begin
#'(begin
(require/opaque-type oc.ty oc.pred lib . oc.opt) ...
(require/typed #:internal sc.nm sc.ty lib) ...
(require/typed #:internal sc.nm sc.ty lib) ...
(require-typed-struct strc.nm (strc.body ...) lib) ...)]
[(_ nm:opt-rename ty lib (~optional [~seq #:struct-maker parent]) ...)
#`(require/typed #:internal nm ty lib #,@(if (attribute parent)
@ -100,15 +100,15 @@ This file defines two sorts of primitives. All of them are provided into any mod
(let ([prop-name (if (attribute parent)
'typechecker:contract-def/maker
'typechecker:contract-def)])
(quasisyntax/loc stx
(begin
(quasisyntax/loc stx
(begin
#,(syntax-property (if (eq? (syntax-local-context) 'top-level)
(let ([typ (parse-type #'ty)])
#`(define cnt*
#,(type->contract
typ
#`(define cnt*
#,(type->contract
typ
;; this is for a `require/typed', so the value is not from the typed side
#:typed-side #f
#:typed-side #f
(lambda () (tc-error/stx #'ty "Type ~a could not be converted to a contract." typ)))))
(syntax-property #'(define cnt* #f)
prop-name #'ty))
@ -118,18 +118,18 @@ This file defines two sorts of primitives. All of them are provided into any mod
'typechecker:ignore #t)))))]))
(define-syntax (define-predicate stx)
(syntax-parse stx
[(_ name:id ty:expr)
(syntax-parse stx
[(_ name:id ty:expr)
#`(begin
#,(syntax-property (if (eq? (syntax-local-context) 'top-level)
(let ([typ (parse-type #'ty)])
#`(define name
#,(type->contract
typ
#`(define name
#,(type->contract
typ
;; must be a flat contract
#:flat #t
;; this is for a `require/typed', so the value is not from the typed side
#:typed-side #f
#:typed-side #f
(lambda () (tc-error/stx #'ty "Type ~a could not be converted to a predicate." typ)))))
(syntax-property #'(define name #f)
'typechecker:flat-contract-def #'ty))
@ -149,7 +149,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
[(_ ty:id pred:id lib (~optional ne:name-exists-kw) ...)
(register-type-name #'ty (make-Opaque #'pred (syntax-local-certifier)))
(quasisyntax/loc stx
(begin
(begin
#,(syntax-property #'(define pred-cnt (any/c . c-> . boolean?))
'typechecker:ignore #t)
#,(internal #'(require/typed-internal pred (Any -> Boolean : (Opaque pred))))
@ -160,7 +160,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
'typechecker:ignore #t)))]))
(define-syntax (plambda: stx)
(syntax-parse stx
(syntax-parse stx
[(plambda: (tvars:id ...) formals . body)
(quasisyntax/loc stx
(#%expression
@ -202,7 +202,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
(define-syntax (inst stx)
(syntax-parse stx #:literals (:)
[(_ arg : . tys)
(syntax/loc stx (inst arg . tys))]
(syntax/loc stx (inst arg . tys))]
[(_ arg tys ... ty ddd b:id)
#:when (eq? (syntax-e #'ddd) '...)
(syntax-property #'arg 'type-inst #'(tys ... (ty . b)))]
@ -266,7 +266,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
(define-syntax (define-type-alias stx)
(syntax-parse stx
[(_ tname:id rest)
[(_ tname:id rest)
#`(begin
#,(ignore #'(define-syntax tname (lambda (stx) (raise-syntax-error 'type-check "type name used out of context" stx))))
#,(internal (syntax/loc stx (define-type-alias-internal tname rest))))]
@ -276,7 +276,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
(define-syntax (define-typed-struct/exec stx)
(syntax-parse stx #:literals (:)
[(_ nm ((~describe "field specification" [fld:optionally-annotated-name]) ...) [proc : proc-ty])
(with-syntax*
(with-syntax*
([proc* (syntax-property #'(ann proc : proc-ty) 'typechecker:with-type #t)]
[d-s (syntax-property (syntax/loc stx (define-struct nm (fld.name ...)
#:property prop:procedure proc*))
@ -307,11 +307,11 @@ This file defines two sorts of primitives. All of them are provided into any mod
#:with super #f))
(syntax-parse stx
[(_ () nm:struct-name . rest)
(internal (quasisyntax/loc stx
(internal (quasisyntax/loc stx
(define-typed-struct-internal
#,(syntax-property #'nm 'struct-info (attribute nm.value)) . rest)))]
[(_ (vars:id ...) nm:struct-name . rest)
(internal (quasisyntax/loc stx
(internal (quasisyntax/loc stx
(define-typed-struct-internal (vars ...)
#,(syntax-property #'nm 'struct-info (attribute nm.value)) . rest)))]))
@ -326,7 +326,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
#:attributes (name super)
(pattern (name:id super:id))
(pattern name:id
#:with super #f))
#:with super #f))
(define-splicing-syntax-class struct-name/new
#:description "struct name (with optional super-struct name)"
(pattern (~seq name:id super:id)
@ -336,9 +336,9 @@ This file defines two sorts of primitives. All of them are provided into any mod
#:with super #f
#:attr old-spec #'name
#:with new-spec #'(name)))
(define (mutable? opts)
(define (mutable? opts)
(if (memq '#:mutable (syntax->datum opts)) '(#:mutable) '()))
(values
(values
(lambda (stx)
(syntax-parse stx
[(_ nm:struct-name (fs:fld-spec ...) . opts)
@ -359,7 +359,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
(let ([mutable (mutable? #'opts)]
[cname (datum->syntax #f (syntax-e #'nm.name))])
(with-syntax ([d-s (syntax-property (quasisyntax/loc stx
(struct #,@(attribute nm.new-spec) (fs.fld ...)
(struct #,@(attribute nm.new-spec) (fs.fld ...)
#:extra-constructor-name #,cname
. opts))
'typechecker:ignore #t)]
@ -368,7 +368,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
[(_ (vars:id ...) nm:struct-name/new (fs:fld-spec ...) . opts)
(let ([cname (datum->syntax #f (syntax-e #'nm.name))]
[mutable (mutable? #'opts)])
(with-syntax ([d-s (syntax-property (quasisyntax/loc stx
(with-syntax ([d-s (syntax-property (quasisyntax/loc stx
(struct #,@(attribute nm.new-spec) (fs.fld ...)
#:extra-constructor-name #,cname
. opts))
@ -384,7 +384,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
(quasisyntax/loc stx
(begin
(require (only-in lib struct-info))
(define-syntax nm (make-struct-info
(define-syntax nm (make-struct-info
(lambda ()
(list #'struct-info
#'maker
@ -396,7 +396,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
#,(ignore #'(require/contract pred (any/c . c-> . boolean?) lib))
#,(internal #'(require/typed-internal pred (Any -> Boolean : nm)))
(require/typed maker nm lib #:struct-maker #f)
(require/typed lib
(require/typed lib
[sel (nm -> ty)]) ...)))]
[(_ (nm parent) ([fld : ty] ...) lib)
(and (identifier? #'nm) (identifier? #'parent))
@ -404,7 +404,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
[(mut ...) (map (lambda _ #'#f) (syntax->list #'(sel ...)))])
#`(begin
(require (only-in lib struct-info))
(define-syntax nm (make-struct-info
(define-syntax nm (make-struct-info
(lambda ()
(list #'struct-info
#'maker
@ -416,13 +416,13 @@ This file defines two sorts of primitives. All of them are provided into any mod
#,(ignore #'(require/contract pred (any/c . c-> . boolean?) lib))
#,(internal #'(require/typed-internal pred (Any -> Boolean : nm)))
(require/typed maker nm lib #:struct-maker parent)
(require/typed lib
(require/typed lib
[sel (nm -> ty)]) ...))]))
(define-syntax (do: stx)
(syntax-parse stx #:literals (:)
[(_ : ty
((var:optionally-annotated-name rest ...) ...)
[(_ : ty
((var:optionally-annotated-name rest ...) ...)
(stop?:expr ret ...)
c:expr ...)
(syntax/loc
@ -640,7 +640,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
(define-syntaxes (let/cc: let/ec:)
(let ()
(define ((mk l/c) stx)
(define ((mk l/c) stx)
(syntax-parse stx
[(_ (~var k (param-annotated-name (lambda (s) #`(#,s -> (U))))) . body)
(quasisyntax/loc stx (#,l/c k.ann-name . body))]))

4
collects/typed-scheme/base-env/type-env-lang.rkt
View File

@ -19,8 +19,8 @@
(define-syntax nm (lambda (stx) (raise-syntax-error 'type-check "type name used out of context" stx))) ...
(provide nm) ...
;(define-syntax provider (lambda (stx) #'(begin (provide nm) ...)))
;(provide provider)
(begin-for-syntax
;(provide provider)
(begin-for-syntax
;(printf "running base-types\n")
(initialize-type-name-env
(list (list #'nm ty) ...))))))]

14
collects/typed-scheme/core.rkt
View File

@ -10,10 +10,10 @@
(types utils convenience)
(typecheck typechecker provide-handling tc-toplevel)
(env type-name-env type-alias-env)
(r:infer infer)
(r:infer infer)
(rep type-rep)
(except-in (utils utils tc-utils) infer)
(only-in (r:infer infer-dummy) infer-param)
(only-in (r:infer infer-dummy) infer-param)
"tc-setup.rkt")
(provide mb-core ti-core wt-core)
@ -26,10 +26,10 @@
(let ([pmb-form (syntax/loc stx (#%plain-module-begin forms ...))])
(parameterize ([optimize? (or (and (not (attribute opt?)) (optimize?))
(and (attribute opt?) (syntax-e (attribute opt?))))])
(tc-setup
(tc-setup
stx pmb-form 'module-begin new-mod tc-module after-code
(with-syntax*
(;; pmb = #%plain-module-begin
(;; pmb = #%plain-module-begin
[(pmb . body2) new-mod]
;; add in syntax property on useless expression to draw check-syntax arrows
[check-syntax-help (syntax-property #'(void) 'disappeared-use (type-name-references))]
@ -48,8 +48,8 @@
;; use the regular %#module-begin from `racket/base' for top-level printing
#`(#%module-begin optimized-body ... #,after-code check-syntax-help)))))]))
(define (ti-core stx)
(syntax-parse stx
(define (ti-core stx)
(syntax-parse stx
[(_ . ((~datum module) . rest))
#'(module . rest)]
[(_ . form)
@ -66,7 +66,7 @@
[(tc-results: t)
(format "- : ~a\n" (cons 'Values t))]
[x (int-err "bad type result: ~a" x)])])
(if ty-str
(if ty-str
#`(let ([type '#,ty-str])
(begin0 #,body2 (display type)))
body2))]))]))

18
collects/typed-scheme/env/global-env.rkt vendored
View File

@ -3,7 +3,7 @@
;; Top-level type environment
;; maps identifiers to their types, updated by mutation
(require "../utils/utils.rkt"
(require "../utils/utils.rkt"
syntax/id-table
(utils tc-utils)
(types utils))
@ -51,7 +51,7 @@
;; given an identifier, return the type associated with it
;; if none found, calls lookup-fail
;; identifier -> type
;; identifier -> type
(define (lookup-type id [fail-handler (lambda () (lookup-type-fail id))])
(let ([v (free-id-table-ref the-mapping id fail-handler)])
(if (box? v) (unbox v) v)))
@ -71,20 +71,20 @@
(void))
(define (check-all-registered-types)
(free-id-table-for-each
the-mapping
(lambda (id e)
(when (box? e)
(free-id-table-for-each
the-mapping
(lambda (id e)
(when (box? e)
(let ([bnd (identifier-binding id)])
(tc-error/expr #:stx id
"Declaration for ~a provided, but ~a ~a"
"Declaration for ~a provided, but ~a ~a"
(syntax-e id) (syntax-e id)
(cond [(eq? bnd 'lexical) "is a lexical binding"] ;; should never happen
[(not bnd) "has no definition"]
[(not bnd) "has no definition"]
[else "is defined in another module"]))))
(void))))
;; map over the-mapping, producing a list
;; (id type -> T) -> listof[T]
;; (id type -> T) -> listof[T]
(define (type-env-map f)
(free-id-table-map the-mapping f))

24
collects/typed-scheme/env/init-envs.rkt vendored
View File

@ -1,15 +1,15 @@
#lang scheme/base
(provide (all-defined-out))
(require "../utils/utils.rkt"
"global-env.rkt"
"global-env.rkt"
"type-name-env.rkt"
"type-alias-env.rkt"
unstable/struct racket/dict
(rep type-rep object-rep filter-rep rep-utils)
(for-template (rep type-rep object-rep filter-rep)
(for-template (rep type-rep object-rep filter-rep)
(types union)
mzlib/pconvert mzlib/shared scheme/base)
(types union convenience)
(types union convenience)
mzlib/pconvert racket/match mzlib/shared)
(define (initialize-type-name-env initial-type-names)
@ -27,7 +27,7 @@
[(Name: stx) `(make-Name (quote-syntax ,stx))]
[(fld: t acc mut) `(make-fld ,(sub t) (quote-syntax ,acc) ,mut)]
[(Struct: name parent flds proc poly? pred-id cert maker-id)
`(make-Struct ,(sub name) ,(sub parent)
`(make-Struct ,(sub name) ,(sub parent)
,(sub flds) ,(sub proc) ,(sub poly?)
(quote-syntax ,pred-id) (syntax-local-certifier)
(quote-syntax ,maker-id))]
@ -46,7 +46,7 @@
`(quote-syntax ,i)
i))]
[(NotTypeFilter: t p i)
`(make-NotTypeFilter ,(sub t) ,(sub p)
`(make-NotTypeFilter ,(sub t) ,(sub p)
,(if (identifier? i)
`(quote-syntax ,i)
i))]
@ -64,32 +64,32 @@
`(,(gen-constructor tag) ,@(map sub vals))]
[_ (basic v)]))
(define (bound-in-this-module id)
(define (bound-in-this-module id)
(let ([binding (identifier-binding id)])
(if (and (list? binding) (module-path-index? (car binding)))
(let-values ([(mp base) (module-path-index-split (car binding))])
(not mp))
#f)))
(define (tname-env-init-code)
(define (tname-env-init-code)
(define (f id ty)
(if (bound-in-this-module id)
#`(register-type-name #'#,id #,(datum->syntax #'here (print-convert ty)))
#f))
(parameterize ((current-print-convert-hook converter)
(show-sharing #f)
(booleans-as-true/false #f))
(booleans-as-true/false #f))
(with-syntax ([registers (filter (lambda (x) x) (type-name-env-map f))])
#'(begin-for-syntax . registers))))
(define (talias-env-init-code)
(define (talias-env-init-code)
(define (f id ty)
(if (bound-in-this-module id)
#`(register-resolved-type-alias #'#,id #,(datum->syntax #'here (print-convert ty)))
#f))
(parameterize ((current-print-convert-hook converter)
(show-sharing #f)
(booleans-as-true/false #f))
(booleans-as-true/false #f))
(with-syntax ([registers (filter (lambda (x) x) (type-alias-env-map f))])
#'(begin-for-syntax . registers))))
@ -97,12 +97,12 @@
(define (f id ty)
(if (and (bound-in-this-module id)
;; if there are no syntax provides, then we only need this identifier if it's provided
#;(or syntax-provide? (dict-ref provide-tbl id #f)))
#;(or syntax-provide? (dict-ref provide-tbl id #f)))
#`(register-type #'#,id #,(datum->syntax #'here (print-convert ty)))
#f))
(parameterize ((current-print-convert-hook converter)
(show-sharing #f)
(booleans-as-true/false #f))
(booleans-as-true/false #f))
(with-syntax ([registers (filter values (type-env-map f))])
#'(begin-for-syntax . registers))))

2
collects/typed-scheme/env/tvar-env.rkt vendored
View File

@ -1,6 +1,6 @@
#lang racket/base
;; this implements the Delta environment from the TOPLAS paper
;; this implements the Delta environment from the TOPLAS paper
;; (as well as every other paper on System F)
;; this environment maps type variables names (symbols)

6
collects/typed-scheme/env/type-alias-env.rkt vendored
View File

@ -17,7 +17,7 @@
(define-struct (resolved alias-def) (ty) #:inspector #f)
;; a mapping from id -> alias-def (where id is the name of the type)
(define the-mapping
(define the-mapping
(make-module-identifier-mapping))
(define (mapping-put! id v) (module-identifier-mapping-put! the-mapping id v))
@ -38,12 +38,12 @@
(match (module-identifier-mapping-get the-mapping id (lambda () (return (k))))
[(struct unresolved (stx #f))
(resolve-type-alias id parse-type)]
[(struct unresolved (stx #t))
[(struct unresolved (stx #t))
(tc-error/stx stx "Recursive Type Alias Reference")]
[(struct resolved (t)) t])))
(define (resolve-type-alias id parse-type)
(define v (module-identifier-mapping-get the-mapping id))
(define v (module-identifier-mapping-get the-mapping id))
(match v
[(struct unresolved (stx _))
(set-unresolved-in-process! v #t)

4
collects/typed-scheme/env/type-name-env.rkt vendored
View File

@ -15,7 +15,7 @@
type-name-env-map)
;; a mapping from id -> type (where id is the name of the type)
(define the-mapping
(define the-mapping
(make-module-identifier-mapping))
(define (mapping-put! id v) (module-identifier-mapping-put! the-mapping id v))
@ -34,7 +34,7 @@
;; given an identifier, return the type associated with it
;; optional argument is failure continuation - default calls lookup-fail
;; identifier (-> error) -> type
;; identifier (-> error) -> type
(define (lookup-type-name id [k (lambda () (lookup-type-fail id))])
(begin0
(module-identifier-mapping-get the-mapping id k)

4
collects/typed-scheme/infer/constraints.rkt
View File

@ -43,7 +43,7 @@
dmap)))]))
;; a stupid impl
(define (meet S T)
(define (meet S T)
(let ([s* (restrict S T)])
(if (and (subtype s* S)
(subtype s* T))
@ -71,7 +71,7 @@
([(map1 dmap1) (in-pairs (remove-duplicates maps1))]
[(map2 dmap2) (in-pairs (remove-duplicates maps2))])
(with-handlers ([exn:infer? (lambda (_) #f)])
(cons
(cons
(hash-union map1 map2 #:combine c-meet)
(dmap-meet dmap1 dmap2)))))])
(when (null? maps)

6
collects/typed-scheme/infer/dmap.rkt
View File

@ -1,6 +1,6 @@
#lang scheme/unit
(require "../utils/utils.rkt"
(require "../utils/utils.rkt"
"signatures.rkt" "constraint-structs.rkt"
(utils tc-utils) racket/contract
unstable/sequence unstable/hash racket/match)
@ -16,7 +16,7 @@
(struct dcon-exact (fixed2 rest2))))
(unless (and rest2 (= (length fixed1) (length fixed2)))
(fail! fixed1 fixed2))
(make-dcon-exact
(make-dcon-exact
(for/list ([c1 fixed1]
[c2 fixed2])
(c-meet c1 c2 (c-X c1)))
@ -27,7 +27,7 @@
[((struct dcon (fixed1 #f)) (struct dcon (fixed2 #f)))
(unless (= (length fixed1) (length fixed2))
(fail! fixed1 fixed2))
(make-dcon
(make-dcon
(for/list ([c1 fixed1]
[c2 fixed2])
(c-meet c1 c2 (c-X c1)))

84
collects/typed-scheme/infer/infer-unit.rkt
View File

@ -1,7 +1,7 @@
#lang racket/unit
(require racket/require (path-up "utils/utils.rkt")
(except-in
(except-in
(combine-in
(utils tc-utils)
(rep free-variance type-rep filter-rep rep-utils)
@ -10,7 +10,7 @@
(env type-name-env index-env tvar-env))
make-env -> ->* one-of/c)
"constraint-structs.rkt"
"signatures.rkt"
"signatures.rkt"
racket/match
mzlib/etc
racket/trace racket/contract
@ -20,7 +20,7 @@
(import dmap^ constraints^ promote-demote^)
(export infer^)
(define (empty-set) '())
(define (empty-set) '())
(define current-seen (make-parameter (empty-set)))
@ -42,9 +42,9 @@
(define (mover cset dbound vars f)
(map/cset
(lambda (cmap dmap)
(cons (hash-remove* cmap (cons dbound vars))
(dmap-meet
(singleton-dmap
(cons (hash-remove* cmap (cons dbound vars))
(dmap-meet
(singleton-dmap
dbound
(f cmap dmap))
(make-dmap (hash-remove (dmap-map dmap) dbound)))))
@ -53,20 +53,20 @@
;; dbound : index variable
;; vars : listof[type variable] - temporary variables
;; cset : the constraints being manipulated
;; takes the constraints on vars and creates a dmap entry contstraining dbound to be |vars|
;; takes the constraints on vars and creates a dmap entry contstraining dbound to be |vars|
;; with the constraints that cset places on vars
(define/cond-contract (move-vars-to-dmap cset dbound vars)
(cset? symbol? (listof symbol?) . -> . cset?)
(mover cset dbound vars
(λ (cmap dmap)
(make-dcon (for/list ([v vars])
(hash-ref cmap v
(hash-ref cmap v
(λ () (int-err "No constraint for new var ~a" v))))
#f))))
;; dbound : index variable
;; cset : the constraints being manipulated
;;
;;
(define/cond-contract (move-rest-to-dmap cset dbound #:exact [exact? #f])
((cset? symbol?) (#:exact boolean?) . ->* . cset?)
(mover cset dbound null
@ -78,7 +78,7 @@
;; dbound : index variable
;; cset : the constraints being manipulated
;;
;;
(define/cond-contract (move-dotted-rest-to-dmap cset dbound)
(cset? symbol? . -> . cset?)
(mover cset dbound null
@ -154,7 +154,7 @@
(match* (s t)
[(e e) (empty-cset X Y)]
[(e (Empty:)) (empty-cset X Y)]
;; FIXME - do something here
;; FIXME - do something here
[(_ _) (fail! s t)]))
(define (cgen/arr V X Y s-arr t-arr)
@ -163,7 +163,7 @@
;; the simplest case - no rests, drests, keywords
[((arr: ss s #f #f '())
(arr: ts t #f #f '()))
(cset-meet* (list
(cset-meet* (list
;; contravariant
(cgen/list V X Y ts ss)
;; covariant
@ -171,8 +171,8 @@
;; just a rest arg, no drest, no keywords
[((arr: ss s s-rest #f '())
(arr: ts t t-rest #f '()))
(let ([arg-mapping
(cond
(let ([arg-mapping
(cond
;; both rest args are present, so make them the same length
[(and s-rest t-rest)
(cgen/list V X Y (cons t-rest (extend ss ts t-rest)) (cons s-rest (extend ts ss s-rest)))]
@ -220,7 +220,7 @@
(let* ([arg-mapping (cgen/list V X Y ts ss)]
[darg-mapping (cgen V X Y t-dty s-dty)]
[ret-mapping (cg s t)])
(cset-meet*
(cset-meet*
(list arg-mapping darg-mapping ret-mapping)))]
;; bounds are different
[((arr: ss s #f (cons s-dty (? (λ (db) (memq db Y)) dbound)) '())
@ -231,7 +231,7 @@
;; just add dbound as something that can be constrained
[darg-mapping (move-dotted-rest-to-dmap (cgen V (cons dbound X) Y t-dty s-dty) dbound)]
[ret-mapping (cg s t)])
(cset-meet*
(cset-meet*
(list arg-mapping darg-mapping ret-mapping)))]
[((arr: ss s #f (cons s-dty dbound) '())
(arr: ts t #f (cons t-dty (? (λ (db) (memq db Y)) dbound*)) '()))
@ -240,7 +240,7 @@
;; just add dbound as something that can be constrained
[darg-mapping (move-dotted-rest-to-dmap (cgen V (cons dbound* X) Y t-dty s-dty) dbound*)]
[ret-mapping (cg s t)])
(cset-meet*
(cset-meet*
(list arg-mapping darg-mapping ret-mapping)))]
;; * <: ...
[((arr: ss s s-rest #f '())
@ -347,22 +347,22 @@
[_ (void)])
;; constrain v to be above S (but don't mention V)
(singleton (var-promote S V) v Univ)]
;; constrain b1 to be below T, but don't mention the new vars
[((Poly: v1 b1) T) (cgen (append v1 V) X Y b1 T)]
;; constrain *each* element of es to be below T, and then combine the constraints
[((Union: es) T) (cset-meet* (cons empty (for/list ([e es]) (cg e T))))]
;; find *an* element of es which can be made to be a supertype of S
;; FIXME: we're using multiple csets here, but I don't think it makes a difference
;; FIXME: we're using multiple csets here, but I don't think it makes a difference
;; not using multiple csets will break for: ???
[(S (Union: es))
[(S (Union: es))
(cset-combine
(filter values
(for/list ([e es])
(for/list ([e es])
(with-handlers ([exn:infer? (λ _ #f)]) (cg S e)))))]
;; two structs with the same name and parent
;; just check pairwise on the fields
[((Struct: nm p flds proc _ _ _ _) (Struct: nm p flds* proc* _ _ _ _))
@ -372,7 +372,7 @@
[proc* (fail! S T)]
[else empty])])
(cset-meet proc-c (cgen/flds V X Y flds flds*)))]
;; two struct names, need to resolve b/c one could be a parent
[((Name: n) (Name: n*))
(if (free-identifier=? n n*)
@ -422,11 +422,11 @@
[((ListDots: s-dty s-dbound) (ListDots: t-dty (? (λ (db) (memq db Y)) t-dbound)))
;; s-dbound can't be in Y, due to previous rule
(move-dotted-rest-to-dmap (cgen V (cons t-dbound X) Y s-dty t-dty) t-dbound)]
;; this constrains `dbound' to be |ts| - |ss|
[((ListDots: s-dty dbound) (List: ts))
(unless (memq dbound Y) (fail! S T))
(let* ([vars (var-store-take dbound s-dty (length ts))]
;; new-tys are dummy plain type variables, standing in for the elements of dbound that need to be generated
[new-tys (for/list ([var vars])
@ -435,32 +435,32 @@
[new-cset (cgen/list V (append vars X) Y new-tys ts)])
;; now take all the dummy types, and use them to constrain dbound appropriately
(move-vars-to-dmap new-cset dbound vars))]
;; if we have two mu's, we rename them to have the same variable
;; and then compare the bodies
;; This relies on (B 0) only unifying with itself, and thus only hitting the first case of this `match'
[((Mu-unsafe: s) (Mu-unsafe: t))
[((Mu-unsafe: s) (Mu-unsafe: t))
(cg s t)]
;; other mu's just get unfolded
[(s (? Mu? t)) (cg s (unfold t))]
[((? Mu? s) t) (cg (unfold s) t)]
;; resolve applications
[((App: _ _ _) _) (cg (resolve-once S) T)]
[(_ (App: _ _ _)) (cg S (resolve-once T))]
;; values are covariant
[((Values: ss) (Values: ts))
(unless (= (length ss) (length ts))
(fail! ss ts))
(cgen/list V X Y ss ts)]
;; this constrains `dbound' to be |ts| - |ss|
[((ValuesDots: ss s-dty dbound) (Values: ts))
(unless (>= (length ts) (length ss)) (fail! ss ts))
(unless (memq dbound Y) (fail! S T))
(let* ([vars (var-store-take dbound s-dty (- (length ts) (length ss)))]
;; new-tys are dummy plain type variables, standing in for the elements of dbound that need to be generated
[new-tys (for/list ([var vars])
@ -469,10 +469,10 @@
[new-cset (cgen/list V (append vars X) Y (append ss new-tys) ts)])
;; now take all the dummy types, and use them to constrain dbound appropriately
(move-vars-to-dmap new-cset dbound vars))]
;; identical bounds - just unify pairwise
[((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound))
(when (memq dbound Y) (fail! ss ts))
(when (memq dbound Y) (fail! ss ts))
(cgen/list V X Y (cons s-dty ss) (cons t-dty ts))]
[((ValuesDots: ss s-dty (? (λ (db) (memq db Y)) s-dbound)) (ValuesDots: ts t-dty t-dbound))
;; What should we do if both are in Y?
@ -531,7 +531,7 @@
;; check each element
[((Result: s f-s o-s)
(Result: t f-t o-t))
(cset-meet* (list (cg s t)
(cset-meet* (list (cg s t)
(cgen/filter-set V X Y f-s f-t)
(cgen/object V X Y o-s o-t)))]
[(_ _)
@ -553,11 +553,11 @@
[(c S X T)
(let ([var (hash-ref h (or variable X) Constant)])
;(printf "variance was: ~a\nR was ~a\nX was ~a\nS T ~a ~a\n" var R (or variable X) S T)
(evcase var
(evcase var
[Constant S]
[Covariant S]
[Contravariant T]
[Invariant
[Invariant
(let ([gS (generalize S)])
;(printf "Inv var: ~a ~a ~a ~a\n" v S gS T)
(if (subtype gS T)
@ -603,7 +603,7 @@
S)))
(match (car (cset-maps C))
[(cons cmap (dmap dm))
(let ([subst (hash-union
(let ([subst (hash-union
(for/hash ([(k dc) (in-hash dm)])
(match dc
[(dcon fixed #f)
@ -670,7 +670,7 @@
;; if R is #f, we don't care about the substituion
;; just return a boolean result
(define (infer X Y S T R [expected #f])
(with-handlers ([exn:infer? (lambda _ #f)])
(with-handlers ([exn:infer? (lambda _ #f)])
(let* ([expected-cset (if expected
(cgen null X Y R expected)
(empty-cset '() '()))]
@ -697,7 +697,7 @@
#:expected-cset expected-cset)]
[new-vars (var-store-take dotted-var T-dotted (length rest-S))]
[new-Ts (for/list ([v new-vars])
(substitute (make-F v) dotted-var
(substitute (make-F v) dotted-var
(substitute-dots (map make-F new-vars) #f dotted-var T-dotted)))]
[cs-dotted (cgen/list null (append new-vars X) (list dotted-var) rest-S new-Ts
#:expected-cset expected-cset)]

2
collects/typed-scheme/infer/infer.rkt
View File

@ -7,7 +7,7 @@
(only-in scheme/unit provide-signature-elements
define-values/invoke-unit/infer link)
(utils unit-utils))
(provide-signature-elements restrict^ infer^)
(define-values/invoke-unit/infer

2
collects/typed-scheme/infer/promote-demote.rkt
View File

@ -34,7 +34,7 @@
(make-Param (var-demote in V)
(vp out))]
[#:arr dom rng rest drest kws
(cond
(cond
[(apply V-in? V (get-filters rng))
(make-top-arr)]
[(and drest (memq (cdr drest) V))

8
collects/typed-scheme/infer/restrict.rkt
View File

@ -12,20 +12,20 @@
;; NEW IMPL
;; restrict t1 to be a subtype of t2
(define (restrict* t1 t2)
(define (restrict* t1 t2)
;; we don't use union map directly, since that might produce too many elements
(define (union-map f l)
(match l
[(Union: es)
[(Union: es)
(let ([l (map f es)])
(apply Un l))]))
(cond
[(subtype t1 t2) t1] ;; already a subtype
[(subtype t1 t2) t1] ;; already a subtype
[(match t2
[(Poly: vars t)
(let ([subst (infer vars null (list t1) (list t) t1)])
(and subst (restrict* t1 (subst-all subst t1))))]
[_ #f])]
[_ #f])]
[(Union? t1) (union-map (lambda (e) (restrict* e t2)) t1)]
[(needs-resolving? t1) (restrict* (resolve-once t1) t2)]
[(needs-resolving? t2) (restrict* t1 (resolve-once t2))]

14
collects/typed-scheme/infer/signatures.rkt
View File

@ -1,6 +1,6 @@
#lang racket/base
(require racket/unit racket/contract racket/require
"constraint-structs.rkt"
"constraint-structs.rkt"
(path-up "utils/utils.rkt" "utils/unit-utils.rkt" "rep/type-rep.rkt"))
(provide (all-defined-out))
@ -31,9 +31,9 @@
(define-signature infer^
([cond-contracted infer ((;; variables from the forall
(listof symbol?)
(listof symbol?)
;; indexes from the forall
(listof symbol?)
(listof symbol?)
;; actual argument types from call site
(listof Type?)
;; domain
@ -41,12 +41,12 @@
;; range
(or/c #f Type?))
;; optional expected type
((or/c #f Type?))
((or/c #f Type?))
. ->* . any)]
[cond-contracted infer/vararg ((;; variables from the forall
(listof symbol?)
(listof symbol?)
;; indexes from the forall
(listof symbol?)
(listof symbol?)
;; actual argument types from call site
(listof Type?)
;; domain
@ -57,7 +57,7 @@
(or/c #f Type?))
;; [optional] expected type
((or/c #f Type?)) . ->* . any)]
[cond-contracted infer/dots (((listof symbol?)
[cond-contracted infer/dots (((listof symbol?)
symbol?
(listof Type?) (listof Type?) Type? Type? (listof symbol?))
(#:expected (or/c #f Type?)) . ->* . any)]))

2
collects/typed-scheme/language-info.rkt
View File

@ -10,7 +10,7 @@
;; options currently always empty
(define (configure options)
(namespace-require 'scheme/base)
(eval '(begin
(eval '(begin
(require (for-syntax typed-scheme/utils/tc-utils scheme/base))
(begin-for-syntax (set-box! typed-context? #t)))
(current-namespace))

4
collects/typed-scheme/main.rkt
View File

@ -1,12 +1,12 @@
#lang s-exp "minimal.rkt"
(providing (libs (except scheme/base #%module-begin #%top-interaction with-handlers lambda #%app for for*)
(except "base-env/prims.rkt")
(except "base-env/base-types.rkt")
(except "base-env/base-types-extra.rkt"))
(basics #%module-begin
(basics #%module-begin
#%top-interaction
lambda
#%app))

4
collects/typed-scheme/minimal.rkt
View File

@ -10,12 +10,12 @@
(define-syntax (providing stx)
(syntax-case stx (libs from basics except)
[(form (libs (except lb ex ...) ...) (basics b ...) (from spec id ...) ...)
(datum->syntax
(datum->syntax
stx
(syntax->datum
(with-syntax ([(b* ...) (generate-temporaries #'(b ...))]
[ts ts-mod])
(syntax/loc
(syntax/loc
stx
(begin
(require (except-in ts b ...))

6
collects/typed-scheme/no-check.rkt
View File

@ -1,6 +1,6 @@
#lang scheme/base
(require
(require
(except-in "base-env/prims.rkt"
require/typed require/opaque-type require-typed-struct)
"base-env/base-types-extra.rkt"
@ -37,9 +37,9 @@
#:with opt #'(#:name-exists)))
(syntax-parse stx
[(_ lib (~or sc:simple-clause strc:struct-clause oc:opaque-clause) ...)
#'(begin
#'(begin
(require/opaque-type oc.ty oc.pred lib . oc.opt) ...
(require/typed sc.nm sc.ty lib) ...
(require/typed sc.nm sc.ty lib) ...
(require-typed-struct strc.nm (strc.body ...) lib) ...)]
[(_ nm:opt-rename ty lib (~optional [~seq #:struct-maker parent]) ...)
#'(require (only-in lib nm.spec))]))

30
collects/typed-scheme/optimizer/float-complex.rkt
View File

@ -57,7 +57,7 @@
(list
#`((real-binding) #,(skip-0s #'(c1.real-binding c2.real-binding cs.real-binding ...)))
#`((imag-binding) #,(skip-0s #'(c1.imag-binding c2.imag-binding cs.imag-binding ...)))))))))
(pattern (#%plain-app (~and op (~literal -))
c1:unboxed-float-complex-opt-expr
c2:unboxed-float-complex-opt-expr
@ -84,7 +84,7 @@
(list
#`((real-binding) #,(skip-0s #'(c1.real-binding c2.real-binding cs.real-binding ...)))
#`((imag-binding) #,(skip-0s #'(c1.imag-binding c2.imag-binding cs.imag-binding ...)))))))))
(pattern (#%plain-app (~and op (~literal *))
c1:unboxed-float-complex-opt-expr
c2:unboxed-float-complex-opt-expr
@ -133,7 +133,7 @@
#`(unsafe-fl- (unsafe-fl* #,o1 #,(car e1))
(unsafe-fl* #,o2 #,(car e2))))))
res)))))))))
(pattern (#%plain-app (~and op (~literal /))
c1:unboxed-float-complex-opt-expr
c2:unboxed-float-complex-opt-expr
@ -213,17 +213,17 @@
(begin (log-optimization "unboxed unary float complex" #'op)
#`(#,@(append (syntax->list #'(c.bindings ...))
(list #'((imag-binding) (unsafe-fl- 0.0 c.imag-binding)))))))
(pattern (#%plain-app (~and op (~literal magnitude)) c:unboxed-float-complex-opt-expr)
#:with real-binding (unboxed-gensym "unboxed-real-")
#:with imag-binding #f
#:with (bindings ...)
(begin (log-optimization "unboxed unary float complex" #'op)
#`(c.bindings ...
((real-binding) (unsafe-flsqrt
(unsafe-fl+ (unsafe-fl* c.real-binding c.real-binding)
((real-binding) (unsafe-flsqrt
(unsafe-fl+ (unsafe-fl* c.real-binding c.real-binding)
(unsafe-fl* c.imag-binding c.imag-binding)))))))
(pattern (#%plain-app (~and op (~or (~literal real-part) (~literal unsafe-flreal-part)))
c:unboxed-float-complex-opt-expr)
#:with real-binding #'c.real-binding
@ -238,7 +238,7 @@
#:with (bindings ...)
(begin (log-optimization "unboxed unary float complex" #'op)
#'(c.bindings ...)))
;; special handling of reals inside complex operations
;; must be after any cases that we are supposed to handle
(pattern e:float-arg-expr
@ -247,7 +247,7 @@
#:when (log-optimization "float-coerce-expr in complex ops" #'e)
#:with (bindings ...)
#`(((real-binding) e.opt)))
;; we can eliminate boxing that was introduced by the user
(pattern (#%plain-app (~and op (~or (~literal make-rectangular)
@ -281,7 +281,7 @@
#:with (bindings ...)
(begin (log-optimization "leave var unboxed" #'v)
#'()))
;; else, do the unboxing here
;; we can unbox literals right away
@ -309,7 +309,7 @@
#`(((real-binding) #,(datum->syntax
#'here
(exact->inexact (syntax->datum #'n)))))))
(pattern e:expr
#:when (subtypeof? #'e -FloatComplex)
#:with e* (unboxed-gensym)
@ -375,7 +375,7 @@
(free-identifier=? #'op #'unsafe-flreal-part))
#'c*.real-binding
#'c*.imag-binding))))
(pattern (#%plain-app op:float-complex-unary-op n:float-complex-expr)
#:with opt
(begin (log-optimization "unary float complex" #'op)
@ -400,13 +400,13 @@
#:with opt
(begin (log-optimization "call to fun with unboxed args" #'op)
#'e*.opt))
(pattern e:float-complex-arith-opt-expr
#:with opt #'e.opt))
(define-syntax-class float-complex-arith-opt-expr
#:commit
(pattern (#%plain-app op:float-complex->float-op e:expr ...)
#:when (subtypeof? this-syntax -Flonum)
#:with exp*:unboxed-float-complex-opt-expr this-syntax
@ -430,7 +430,7 @@
(reset-unboxed-gensym)
#'(let*-values (exp*.bindings ...)
(unsafe-make-flrectangular exp*.real-binding exp*.imag-binding))))
(pattern v:id
#:with unboxed-info (dict-ref unboxed-vars-table #'v #f)
#:when (syntax->datum #'unboxed-info)

2
collects/typed-scheme/optimizer/float.rkt
View File

@ -106,7 +106,7 @@
#:with opt
(begin (log-optimization "unary float" #'op)
#'(unsafe-fl/ 1.0 f.opt)))
;; we can optimize exact->inexact if we know we're giving it an Integer
(pattern (#%plain-app (~and op (~literal exact->inexact)) n:int-expr)
#:with opt

4
collects/typed-scheme/optimizer/optimizer.rkt
View File

@ -33,7 +33,7 @@
(pattern e:sequence-opt-expr #:with opt #'e.opt)
(pattern e:box-opt-expr #:with opt #'e.opt)
(pattern e:struct-opt-expr #:with opt #'e.opt)
;; boring cases, just recur down
(pattern ((~and op (~or (~literal #%plain-lambda) (~literal define-values)))
formals e:expr ...)
@ -68,7 +68,7 @@
(opt-clauses ...)
#,@(syntax-map (optimize) #'(e-body ...))))
(pattern (kw:identifier expr ...)
#:when
#:when
(for/or ([k (list #'if #'begin #'begin0 #'set! #'#%plain-app #'#%app #'#%expression
#'#%variable-reference #'with-continuation-mark)])
(free-identifier=? k #'kw))

2
collects/typed-scheme/optimizer/pair.rkt
View File

@ -54,7 +54,7 @@
(begin (log-optimization "mutable pair" #'op)
#`(op.unsafe p.opt #,@(syntax-map (optimize) #'(e ...))))))
;; if the equivalent sequence of cars and cdrs is guaranteed not to fail,
;; we can optimize

8
collects/typed-scheme/optimizer/unboxed-let.rkt
View File

@ -168,11 +168,11 @@
;; if not, recur on the subforms
(define (look-at exp)
(ormap rec (syntax->list exp)))
(define (rec exp)
(syntax-parse exp
#:literal-sets (kernel-literals)
;; can be used in a complex arithmetic expr, can be a direct child
[exp:float-complex-arith-opt-expr
#:when (not (identifier? #'exp))
@ -195,7 +195,7 @@
(or (look-at #'(e-rhs ... e-body ...))
(ormap (lambda (x) (could-be-unboxed-in? x exp))
(syntax->list #'rebindings)))]
;; recur down
[((~and op (~or (~literal #%plain-lambda) (~literal define-values)))
formals e:expr ...)
@ -207,7 +207,7 @@
(list #'if #'begin #'begin0 #'set! #'#%plain-app #'#%app #'#%expression
#'#%variable-reference #'with-continuation-mark))
(look-at #'(expr ...))]
;; not used, not worth unboxing
[_ #f]))

72
collects/typed-scheme/private/parse-type.rkt
View File

@ -6,7 +6,7 @@
(utils tc-utils stxclass-util)
syntax/stx (prefix-in c: scheme/contract)
syntax/parse
(env type-env-structs tvar-env type-name-env type-alias-env lexical-env index-env)
(env type-env-structs tvar-env type-name-env type-alias-env lexical-env index-env)
racket/match
(for-template scheme/base "../base-env/colon.ss")
;; needed at this phase for tests
@ -16,8 +16,8 @@
(define-struct poly (name vars) #:prefab)
(provide/cond-contract [parse-type (syntax? . c:-> . Type/c)]
[parse-type/id (syntax? c:any/c . c:-> . Type/c)]
[parse-tc-results (syntax? . c:-> . tc-results?)]
[parse-type/id (syntax? c:any/c . c:-> . Type/c)]
[parse-tc-results (syntax? . c:-> . tc-results?)]
[parse-tc-results/id (syntax? c:any/c . c:-> . tc-results?)])
(provide star ddd/bound)
@ -57,11 +57,11 @@
[(ty)
(parse-type #'ty)]
[(x ...)
#:fail-unless (= 1 (length
#:fail-unless (= 1 (length
(for/list ([i (syntax->list #'(x ...))]
#:when (and (identifier? i)
(free-identifier=? i #'t:->)))
i)))
i)))
#f
(parse-type s)]))
@ -75,7 +75,7 @@
(extend-indexes v
(extend-tvars vars
(make-PolyDots (append vars (list v)) (parse-all-body #'t)))))]
[((~and kw t:All) (vars:id ...) . t)
[((~and kw t:All) (vars:id ...) . t)
(let* ([vars (map syntax-e (syntax->list #'(vars ...)))])
(add-type-name-reference #'kw)
(extend-tvars vars
@ -105,7 +105,7 @@
#:attr pe (make-CdrPE)))
(define-splicing-syntax-class simple-latent-filter
#:description "latent filter"
#:description "latent filter"
(pattern (~seq t:expr (~describe "@" (~datum @)) pe:path-elem ...)
#:attr type (parse-type #'t)
#:attr path (attribute pe.pe))
@ -148,8 +148,8 @@
(attribute o.object)
-no-obj)))
(define (parse-type stx)
(parameterize ([current-orig-stx stx])
(define (parse-type stx)
(parameterize ([current-orig-stx stx])
(syntax-parse
stx
#:literals (t:Class t:Refinement t:Instance t:List t:List* cons t:pred t:-> : case-lambda t:case->
@ -199,17 +199,17 @@
[((~and kw cons) fst rst)
(add-type-name-reference #'kw)
(-pair (parse-type #'fst) (parse-type #'rst))]
[((~and kw t:pred) t)
[((~and kw t:pred) t)
(add-type-name-reference #'kw)
(make-pred-ty (parse-type #'t))]
(make-pred-ty (parse-type #'t))]
[((~and kw (~or case-lambda t:case->)) tys ...)
(add-type-name-reference #'kw)
(make-Function
(make-Function
(for/list ([ty (syntax->list #'(tys ...))])
(let ([t (parse-type ty)])
(match t
[(Function: (list arr)) arr]
[_ (tc-error/stx
[_ (tc-error/stx
ty
"Component of case-lambda type was not a function clause")]))))]
#;[((~and kw t:Vectorof) t)
@ -233,22 +233,22 @@
(-pair (parse-type #'(quote t1)) (parse-type #'(quote t2)))]
[((~and kw quote) t)
(add-type-name-reference #'kw)
(-val (syntax->datum #'t))]
[((~and kw t:All) . rest)
(-val (syntax->datum #'t))]
[((~and kw t:All) . rest)
(parse-all-type stx parse-type)]
[((~and kw t:Opaque) p?)
[((~and kw t:Opaque) p?)
(add-type-name-reference #'kw)
(make-Opaque #'p? (syntax-local-certifier))]
[((~and kw t:Parameter) t)
[((~and kw t:Parameter) t)
(let ([ty (parse-type #'t)])
(add-type-name-reference #'kw)
(-Param ty ty))]
[((~and kw t:Parameter) t1 t2)
[((~and kw t:Parameter) t1 t2)
(add-type-name-reference #'kw)
(-Param (parse-type #'t1) (parse-type #'t2))]
;; curried function notation
[((~and dom:non-keyword-ty (~not t:->)) ...
(~and kw t:->)
(~and kw t:->)
(~and (~seq rest-dom ...) (~seq (~or _ (~between t:-> 1 +inf.0)) ...)))
(add-type-name-reference #'kw)
(let ([doms (for/list ([d (syntax->list #'(dom ...))])
@ -280,7 +280,7 @@
(add-type-name-reference #'kw)
(let* ([bnd (syntax-e #'bound)])
(unless (bound-index? bnd)
(tc-error/stx #'bound
(tc-error/stx #'bound
"Used a type variable (~a) not bound with ... as a bound on a ..."
bnd))
(make-Function
@ -300,7 +300,7 @@
(extend-tvars (list var) (parse-type #'rest))
var))))]
#| ;; has to be below the previous one
[(dom:expr ... (~and kw t:->) rng)
[(dom:expr ... (~and kw t:->) rng)
(add-type-name-reference #'kw)
(->* (map parse-type (syntax->list #'(dom ...)))
(parse-values-type #'rng))] |#
@ -314,9 +314,9 @@
doms
(parse-values-type #'rng)
#:kws (attribute kws.Keyword)))))]
[id:identifier
(cond
(cond
;; if it's a type variable, we just produce the corresponding reference (which is in the HT)
[(bound-tvar? (syntax-e #'id))
(make-F (syntax-e #'id))]
@ -341,29 +341,29 @@
(tc-error/delayed "Incorrect use of -> type constructor")
Err]
[else
(tc-error/delayed
(tc-error/delayed
"Unbound type name ~a"
(syntax-e #'id))
Err])]
Err])]
[(t:Opaque . rest)
(tc-error "Opaque: bad syntax")]
[(t:U . rest)
(tc-error "Union: bad syntax")]
#;[(t:Vectorof . rest)
(tc-error "Vectorof: bad syntax")]
[((~and (~datum mu) t:Rec) . rest)
[((~and (~datum mu) t:Rec) . rest)
(tc-error "mu: bad syntax")]
[(t:Rec . rest)
[(t:Rec . rest)
(tc-error "Rec: bad syntax")]
[(t ... t:-> . rest)
(tc-error "->: bad syntax")]
[(id arg args ...)
(let loop
(let loop
([rator (parse-type #'id)]
[args (map parse-type (syntax->list #'(arg args ...)))])
(match rator
[(Name: n)
(when (and (current-poly-struct)
(when (and (current-poly-struct)
(free-identifier=? n (poly-name (current-poly-struct)))
(not (or (ormap Error? args)
(andmap type-equal? args (poly-vars (current-poly-struct))))))
@ -383,7 +383,7 @@
(unless (Poly? ty)
(tc-error "not a polymorphic type: ~a" (syntax-e #'id)))
(unless (= (length (syntax->list #'(arg args ...))) (Poly-n ty))
(tc-error "wrong number of arguments to type constructor ~a: expected ~a, got ~a"
(tc-error "wrong number of arguments to type constructor ~a: expected ~a, got ~a"
(syntax-e #'id)
(Poly-n ty)
(length (syntax->list #'(arg args ...)))))
@ -393,7 +393,7 @@
[_ (tc-error "not a valid type: ~a" (syntax->datum stx))])))
(define (parse-list-type stx)
(parameterize ([current-orig-stx stx])
(parameterize ([current-orig-stx stx])
(syntax-parse stx #:literals (t:List)
[((~and kw t:List) tys ... dty :ddd/bound)
(add-type-name-reference #'kw)
@ -415,12 +415,12 @@
(extend-tvars (list var)
(parse-type #'dty))
var)))]
[((~and kw t:List) tys ...)
[((~and kw t:List) tys ...)
(add-type-name-reference #'kw)
(-Tuple (map parse-type (syntax->list #'(tys ...))))])))
(define (parse-values-type stx)
(parameterize ([current-orig-stx stx])
(parameterize ([current-orig-stx stx])
(syntax-parse stx #:literals (values t:All)
[((~and kw values) tys ... dty :ddd/bound)
(add-type-name-reference #'kw)
@ -428,7 +428,7 @@
(unless (bound-index? var)
(if (bound-tvar? var)
(tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." var)
(tc-error/stx #'bound "Type variable ~a is unbound" var)))
(tc-error/stx #'bound "Type variable ~a is unbound" var)))
(make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
(extend-tvars (list var)
(parse-type #'dty))
@ -440,7 +440,7 @@
(extend-tvars (list var)
(parse-type #'dty))
var))]
[((~and kw values) tys ...)
[((~and kw values) tys ...)
(add-type-name-reference #'kw)
(-values (map parse-type (syntax->list #'(tys ...))))]
[t
@ -450,7 +450,7 @@
(syntax-parse stx #:literals (values)
[((~and kw values) t ...)
(add-type-name-reference #'kw)
(ret (map parse-type (syntax->list #'(t ...)))
(ret (map parse-type (syntax->list #'(t ...)))
(map (lambda (x) (make-NoFilter)) (syntax->list #'(t ...)))
(map (lambda (x) (make-NoObject)) (syntax->list #'(t ...))))]
[t (ret (parse-type #'t) (make-NoFilter) (make-NoObject))]))

22
collects/typed-scheme/private/type-annotation.rkt
View File

@ -1,6 +1,6 @@
#lang scheme/base
(require "../utils/utils.rkt"
(require "../utils/utils.rkt"
(rep type-rep)
(utils tc-utils)
(env global-env)
@ -29,7 +29,7 @@
[(a . b) (begin
(printf/log "Annotation Sexp Pair \n")
(print-size #'a)
(print-size #'b))]
(print-size #'b))]
[_ (printf/log "Annotation Sexp \n")]))
;; get the type annotation of this syntax
@ -37,7 +37,7 @@
;; is let-binding really necessary? - remember to record the bugs!
(define (type-annotation stx #:infer [let-binding #f])
(define (pt prop)
(when (and (identifier? stx)
(when (and (identifier? stx)
let-binding
(lookup-type stx (lambda () #f)))
(maybe-finish-register-type stx)
@ -47,7 +47,7 @@
(parse-type/id stx prop)))
;(unless let-binding (error 'ohno))
;(printf "in type-annotation:~a\n" (syntax->datum stx))
(cond
(cond
[(syntax-property stx type-label-symbol) => pt]
[(syntax-property stx type-ascrip-symbol) => pt]
;; this is so that : annotation works in internal def ctxts
@ -66,18 +66,18 @@
(parse-tc-results prop)
(parse-tc-results/id stx prop)))
(cond
[(syntax-property stx type-ascrip-symbol)
[(syntax-property stx type-ascrip-symbol)
=>
(lambda (prop)
(if (pair? prop)
(pt (car prop))
(pt prop)))]
(pt prop)))]
[else #f]))
(define (remove-ascription stx)
(syntax-property stx type-ascrip-symbol
(syntax-property stx type-ascrip-symbol
(cond
[(syntax-property stx type-ascrip-symbol)
[(syntax-property stx type-ascrip-symbol)
=>
(lambda (prop)
(if (pair? prop)
@ -124,14 +124,14 @@
(tc-expr/check expr (ret anns))
(let ([ty (tc-expr expr)])
(match ty
[(tc-results: tys fs os)
[(tc-results: tys fs os)
(if (not (= (length stxs) (length tys)))
(begin
(tc-error/delayed
(tc-error/delayed
"Expression should produce ~a values, but produces ~a values of types ~a"
(length stxs) (length tys) (stringify tys))
(ret (map (lambda _ (Un)) stxs)))
(combine-results
(combine-results
(for/list ([stx stxs] [ty tys] [a anns] [f fs] [o os])
(cond [a (check-type stx ty a) (ret a f o)]
;; mutated variables get generalized, so that we don't infer too small a type

26
collects/typed-scheme/private/type-contract.rkt
View File

@ -12,7 +12,7 @@
(types resolve utils)
(prefix-in t: (types convenience abbrev))
(private parse-type)
racket/match unstable/match syntax/struct syntax/stx mzlib/trace racket/syntax scheme/list
racket/match unstable/match syntax/struct syntax/stx mzlib/trace racket/syntax scheme/list
(only-in scheme/contract -> ->* case-> cons/c flat-rec-contract provide/contract any/c)
(for-template scheme/base racket/contract racket/set (utils any-wrap)
(prefix-in t: (types numeric-predicates))
@ -33,10 +33,10 @@
(let ([typ (if maker?
((map fld-t (Struct-flds (lookup-type-name (Name-id typ)))) #f . t:->* . typ)
typ)])
(with-syntax ([cnt (type->contract
typ
(with-syntax ([cnt (type->contract
typ
;; this is for a `require/typed', so the value is not from the typed side
#:typed-side #f
#:typed-side #f
#:flat flat?
(lambda () (tc-error/stx prop "Type ~a could not be converted to a contract." typ)))])
(syntax/loc stx (define-values (n) cnt))))]
@ -66,7 +66,7 @@
[(Function: (list (top-arr:))) #'procedure?]
[(Function: arrs)
(when flat? (exit (fail)))
(let ()
(let ()
(define ((f [case-> #f]) a)
(define-values (dom* opt-dom* rngs* rst)
(match a
@ -76,7 +76,7 @@
[(conv) (match-lambda [(Keyword: kw kty _) (list kw (t->c/neg kty))])])
(values (append (map t->c/neg dom) (append-map conv mand-kws))
(append-map conv opt-kws)
(map t->c rngs)
(map t->c rngs)
(and rst (t->c/neg rst))))]
;; functions with filters or objects
[(arr: dom (Values: (list (Result: rngs _ _) ...)) rst #f '())
@ -87,7 +87,7 @@
(and rst (t->c/neg rst)))
(exit (fail)))]
[_ (exit (fail))]))
(with-syntax
(with-syntax
([(dom* ...) (if method? (cons #'any/c dom*) dom*)]
[(opt-dom* ...) opt-dom*]
[rng* (match rngs*
@ -177,10 +177,10 @@
[(Base: sym cnt _ _) #`(flat-named-contract '#,sym (flat-contract-predicate #,cnt))]
[(Refinement: par p? cert)
#`(and/c #,(t->c par) (flat-contract #,(cert p?)))]
[(Union: elems)
[(Union: elems)
(let-values ([(vars notvars) (partition F? elems)])
(unless (>= 1 (length vars)) (exit (fail)))
(with-syntax
(with-syntax
([cnts (append (map t->c vars) (map t->c notvars))])
#'(or/c . cnts)))]
[(and t (Function: _)) (t->c/fun t)]
@ -231,12 +231,12 @@
#'(class/c (name fcn-cnt) ... (init [by-name-init by-name-cnt] ...)))]
[(Value: '()) #'null?]
[(Struct: nm par (list (fld: flds acc-ids mut?) ...) proc poly? pred? cert maker-id)
(cond
(cond
[(assf (λ (t) (type-equal? t ty)) structs-seen)
=>
cdr]
[proc (exit (fail))]
[poly?
[poly?
(with-syntax* ([(rec blame val) (generate-temporaries '(rec blame val))]
[maker maker-id]
[cnt-name nm])
@ -280,11 +280,11 @@
[(Syntax: t) #`(syntax/c #,(t->c t))]
[(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))]
[(Param: in out) #`(parameter/c #,(t->c out))]
[(Hashtable: k v)
[(Hashtable: k v)
(if flat?
#`(hash/c #,(t->c k #:flat #t) #,(t->c v #:flat #t) #:flat? #t #:immutable 'dont-care)
#`(hash/c #,(t->c k) #,(t->c v) #:immutable 'dont-care))]
[else
[else
(exit (fail))]))))

20
collects/typed-scheme/private/with-types.rkt
View File

@ -1,7 +1,7 @@
#lang racket/base
(require racket/require
(for-template
(for-template
(except-in racket/base for for*)
"../base-env/prims.rkt"
(prefix-in c: (combine-in racket/contract/region racket/contract/base)))
@ -14,7 +14,7 @@
"private/parse-type.rkt"
"private/type-contract.rkt"
"typecheck/typechecker.rkt"
"env/type-env-structs.rkt"
"env/type-env-structs.rkt"
"env/global-env.rkt"
"env/tvar-env.rkt"
"infer/infer.rkt"
@ -42,11 +42,11 @@
(define ex-cnts (for/list ([t (in-list ex-types)]
[stx (in-list (syntax->list extys))])
(type->contract t #:typed-side #t (no-contract t))))
(define region-tc-result
(define region-tc-result
(and expr? (parse-tc-results resty)))
(define region-cnts
(define region-cnts
(if region-tc-result
(match region-tc-result
(match region-tc-result
[(tc-result1: t)
(list (type->contract t #:typed-side #t (no-contract t #'region-ty-stx)))]
[(tc-results: ts)
@ -58,7 +58,7 @@
(for ([i (in-list (syntax->list fvids))]
[ty (in-list fv-types)])
(register-type i ty))
(define expanded-body
(define expanded-body
(if expr?
(with-syntax ([body body])
(local-expand #'(let () . body) ctx null))
@ -76,7 +76,7 @@
;; this is a parameter to avoid dependency issues
[current-type-names
(lambda ()
(append
(append
(type-name-env-map (lambda (id ty)
(cons (syntax-e id) ty)))
(type-alias-env-map (lambda (id ty)
@ -85,7 +85,7 @@
[type-name-references null]
;; for error reporting
[orig-module-stx stx]
[expanded-module-stx expanded-body])
[expanded-module-stx expanded-body])
(tc-expr/check expanded-body (if expr? region-tc-result (ret ex-types))))
(report-all-errors)
(set-box! typed-context? old-context)
@ -104,7 +104,7 @@
(begin check-syntax-help
(c:with-contract typed-region
#:results (region-cnt ...)
#:freevars ([fv.id cnt] ...)
#:freevars ([fv.id cnt] ...)
body)))
(syntax/loc stx
(begin
@ -138,4 +138,4 @@
(with-type-helper stx #'body #'(fv.id ...) #'(fv.ty ...) #'(id ...) #'(ty ...) #f #f (syntax-local-context))]
[(_ :result-ty fv:free-vars . body)
(with-type-helper stx #'body #'(fv.id ...) #'(fv.ty ...) #'() #'() #'ty #t (syntax-local-context))]))

6
collects/typed-scheme/rep/free-variance.rkt
View File

@ -27,7 +27,7 @@
;; frees = HT[Idx,Variance] where Idx is either Symbol or Number
;; (listof frees) -> frees
(define (combine-frees freess)
(define (combine-frees freess)
(define ((combine-var v) w)
(cond
[(eq? v w) v]
@ -46,7 +46,7 @@
;; appropriately so that things that expect to see
;; it as "free" will -- fixes the case where the
;; dotted pre-type base doesn't use the bound).
(define (fix-bound vs bound)
(define (fix-bound vs bound)
(hash-set vs bound Dotted))
;; frees -> frees
@ -70,7 +70,7 @@
#:when (>= k n))
(values k v)))
(define-syntax (unless-in-table stx)
(define-syntax (unless-in-table stx)
(syntax-case stx ()
[(_ table val . body)
(quasisyntax/loc stx

8
collects/typed-scheme/rep/interning.rkt
View File

@ -27,7 +27,7 @@
(hash-set! table key new)
new))))))))]))
(define (make-count!)
(define (make-count!)
(let ([state 0])
(lambda () (begin0 state (set! state (add1 state))))))
@ -37,9 +37,9 @@
(define identifier-table (make-module-identifier-mapping))
(define (hash-id id)
(module-identifier-mapping-get
identifier-table
id
(module-identifier-mapping-get
identifier-table
id
(lambda () (let ([c (id-count!)])
(module-identifier-mapping-put! identifier-table id c)
c))))

52
collects/typed-scheme/rep/type-rep.rkt
View File

@ -1,7 +1,7 @@
#lang scheme/base
(require "../utils/utils.rkt")
(require (utils tc-utils)
(require (utils tc-utils)
"rep-utils.rkt" "object-rep.rkt" "filter-rep.rkt" "free-variance.rkt"
mzlib/trace racket/match mzlib/etc
scheme/contract
@ -29,7 +29,7 @@
(def-type Scope ([t (or/c Type/c Scope?)]) [#:key (Type-key t)])
(define (scope-depth k)
(flat-named-contract
(flat-named-contract
(format "Scope of depth ~a" k)
(lambda (sc)
(define (f k sc)
@ -74,7 +74,7 @@
(let ([t (free-idxs* scope)]
[base-count (sub1 n)]
[extras (max 0 (- n num-rands))])
(append
(append
;; variances of the fixed arguments
(for/list ([i (in-range base-count)])
(hash-ref t i))
@ -436,7 +436,7 @@
(add-scopes (sub1 n) (*Scope t))))
(define (remove-scopes n sc)
(if (zero? n)
(if (zero? n)
sc
(match sc
[(Scope: sc*) (remove-scopes (sub1 n) sc*)]
@ -476,19 +476,19 @@
#:PathElem (sub-pe st))
e))
;; abstract-many : Names Type -> Scope^n
;; where n is the length of names
;; abstract-many : Names Type -> Scope^n
;; where n is the length of names
(define (abstract-many names ty)
(define (nameTo name count type)
(let loop ([outer 0] [ty type])
(define (sb t) (loop outer t))
(type-case
(type-case
(#:Type sb #:Filter (sub-f sb) #:Object (sub-o sb))
ty
[#:F name* (if (eq? name name*) (*B (+ count outer)) ty)]
;; necessary to avoid infinite loops
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
;; functions
;; functions
[#:arr dom rng rest drest kws
(*arr (map sb dom)
(sb rng)
@ -506,10 +506,10 @@
(*ListDots (sb dty)
(if (eq? dbound name) (+ count outer) dbound))]
[#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))]
[#:PolyDots n body*
[#:PolyDots n body*
(let ([body (remove-scopes n body*)])
(*PolyDots n (*Scope (loop (+ n outer) body))))]
[#:Poly n body*
[#:Poly n body*
(let ([body (remove-scopes n body*)])
(*Poly n (*Scope (loop (+ n outer) body))))])))
(let ([n (length names)])
@ -523,20 +523,20 @@
;(trace abstract-many)
;; instantiate-many : List[Type] Scope^n -> Type
;; where n is the length of types
;; instantiate-many : List[Type] Scope^n -> Type
;; where n is the length of types
;; all of the types MUST be Fs
(define (instantiate-many images sc)
(define (replace image count type)
(let loop ([outer 0] [ty type])
(define (sb t) (loop outer t))
(define sf (sub-f sb))
(type-case
(define (sb t) (loop outer t))
(define sf (sub-f sb))
(type-case
(#:Type sb #:Filter sf #:Object (sub-o sb))
ty
[#:B idx (if (= (+ count outer) idx)
image
ty)]
ty)]
;; necessary to avoid infinite loops
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
;; functions
@ -557,7 +557,7 @@
(*ListDots (sb dty)
(if (eqv? dbound (+ count outer)) (F-n image) dbound))]
[#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))]
[#:PolyDots n body*
[#:PolyDots n body*
(let ([body (remove-scopes n body*)])
(*PolyDots n (*Scope (loop (+ n outer) body))))]
[#:Poly n body*
@ -580,7 +580,7 @@
#;(trace instantiate-many abstract-many)
;; the 'smart' constructor
(define (Mu* name body)
(define (Mu* name body)
(let ([v (*Mu (abstract name body))])
(hash-set! name-table v name)
v))
@ -663,19 +663,19 @@
(syntax-case stx ()
[(_ nps bp)
#'(? Poly?
(app (lambda (t)
(app (lambda (t)
(let* ([n (Poly-n t)]
[syms (build-list n (lambda _ (gensym)))])
(list syms (Poly-body* syms t))))
(list nps bp)))])))
;; This match expander uses the names from the hashtable
;; This match expander uses the names from the hashtable
(define-match-expander Poly-names:
(lambda (stx)
(syntax-case stx ()
[(_ nps bp)
#'(? Poly?
(app (lambda (t)
(app (lambda (t)
(let* ([n (Poly-n t)]
[syms (hash-ref name-table t (lambda _ (build-list n (lambda _ (gensym)))))])
(list syms (Poly-body* syms t))))
@ -688,19 +688,19 @@
(syntax-case stx ()
[(_ nps bp)
#'(? PolyDots?
(app (lambda (t)
(app (lambda (t)
(let* ([n (PolyDots-n t)]
[syms (build-list n (lambda _ (gensym)))])
(list syms (PolyDots-body* syms t))))
(list nps bp)))])))
;; This match expander uses the names from the hashtable
;; This match expander uses the names from the hashtable
(define-match-expander PolyDots-names:
(lambda (stx)
(syntax-case stx ()
[(_ nps bp)
#'(? PolyDots?
(app (lambda (t)
(app (lambda (t)
(let* ([n (PolyDots-n t)]
[syms (hash-ref name-table t (lambda _ (build-list n (lambda _ (gensym)))))])
(list syms (PolyDots-body* syms t))))
@ -711,7 +711,7 @@
(provide
Mu-name: Poly-names:
PolyDots-names:
Type-seq
Type-seq
Mu-unsafe: Poly-unsafe:
PolyDots-unsafe:
Mu? Poly? PolyDots?
@ -724,7 +724,7 @@
remove-dups
sub-f sub-o sub-pe
Values: Values? Values-rs
(rename-out [Mu:* Mu:]
(rename-out [Mu:* Mu:]
[Poly:* Poly:]
[PolyDots:* PolyDots:]
[Mu* make-Mu]

2
collects/typed-scheme/tc-setup.rkt
View File

@ -43,7 +43,7 @@
;; this is a parameter to avoid dependency issues
[current-type-names
(lambda ()
(append
(append
(type-name-env-map (lambda (id ty)
(cons (syntax-e id) ty)))
(type-alias-env-map (lambda (id ty)

10
collects/typed-scheme/typecheck/check-below.rkt
View File

@ -23,7 +23,7 @@
;; (Results Results -> Result)
;; (Type Results -> Type)
;; (Type Type -> Type))
(define (check-below tr1 expected)
(define (check-below tr1 expected)
(define (filter-better? f1 f2)
(match* (f1 f2)
[(f f) #t]
@ -35,14 +35,14 @@
(match* (o1 o2)
[(o o) #t]
[(o (or (NoObject:) (Empty:))) #t]
[(_ _) #f]))
[(_ _) #f]))
(match* (tr1 expected)
;; these two have to be first so that errors can be allowed in cases where multiple values are expected
[((tc-result1: (? (lambda (t) (type-equal? t (Un))))) (tc-results: ts2 (NoFilter:) (NoObject:)))
(ret ts2)]
[((tc-result1: (? (lambda (t) (type-equal? t (Un))))) _)
expected]
[((tc-results: ts fs os) (tc-results: ts2 (NoFilter:) (NoObject:)))
(unless (= (length ts) (length ts2))
(tc-error/expr "Expected ~a values, but got ~a" (length ts2) (length ts)))
@ -52,12 +52,12 @@
(ret ts2 fs os)
(ret ts2))]
[((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (Top:) (Top:)) (Empty:)))
(cond
(cond
[(not (subtype t1 t2))
(tc-error/expr "Expected ~a, but got ~a" t2 t1)])
expected]
[((tc-result1: t1 f1 o1) (tc-result1: t2 f2 o2))
(cond
(cond
[(not (subtype t1 t2))
(tc-error/expr "Expected ~a, but got ~a" t2 t1)]
[(and (not (filter-better? f1 f2))

16
collects/typed-scheme/typecheck/check-subforms-unit.rkt
View File

@ -3,7 +3,7 @@
(require "../utils/utils.rkt"
syntax/kerncase
syntax/parse
racket/match
racket/match
"signatures.rkt" "tc-metafunctions.rkt"
(types utils convenience union subtype)
(utils tc-utils)
@ -16,13 +16,13 @@
;; syntax -> any
(define (check-subforms/with-handlers form [expected #f])
(define handler-tys '())
(define body-ty #f)
(define body-ty #f)
(define (get-result-ty t)
(match t
[(Function:
(list
(arr: _
(Values: (list (Result: rngs _ _) ...))
[(Function:
(list
(arr: _
(Values: (list (Result: rngs _ _) ...))
_ _ (list (Keyword: _ _ #t) ...))))
(apply Un rngs)]
[_ (int-err "Internal error in get-result-ty: not a function type: \n~a" t)]))
@ -39,8 +39,8 @@
#:when (syntax-property form 'typechecker:exn-handler)
(let ([t (tc-expr form)])
(match t
[(tc-result1:
(and t
[(tc-result1:
(and t
(Function: (list (arr: (list _) _ _ _ (list (Keyword: _ _ #f) ...)) ...))))
(set! handler-tys (cons (get-result-ty t) handler-tys))]
[(tc-results: t)

2
collects/typed-scheme/typecheck/def-export.rkt
View File

@ -15,7 +15,7 @@
[(def-export export-id:identifier id:identifier cnt-id:identifier #:alias)
#'(define-syntax export-id
(if (unbox typed-context?)
(begin
(begin
(add-alias #'export-id #'id)
(renamer #'id #:alt #'cnt-id))
(renamer #'cnt-id)))]))

4
collects/typed-scheme/typecheck/find-annotation.rkt
View File

@ -40,7 +40,7 @@
(pattern (case-lambda [_ expr] ...))
(pattern (set! _ e)
#:with (expr ...) #'(e))
(pattern _
(pattern _
#:with (expr ...) #'()))
;; expr id -> type or #f
@ -60,7 +60,7 @@
(or (type-annotation #'v) (lookup-type/lexical #'v #:fail (lambda _ #f)))]
[c:lv-clause
#:with (#%plain-app reverse n:id) #'c.e
#:with (v) #'(c.v ...)
#:with (v) #'(c.v ...)
#:fail-unless (free-identifier=? name #'n) #f
(or (type-annotation #'v) (lookup-type/lexical #'v #:fail (lambda _ #f)))]
[_ #f]))

14
collects/typed-scheme/typecheck/provide-handling.rkt
View File

@ -1,6 +1,6 @@
#lang scheme/base
(require "../utils/utils.rkt"
(require "../utils/utils.rkt"
(only-in srfi/1/list s:member)
syntax/kerncase syntax/boundmap
(env type-name-env type-alias-env)
@ -18,8 +18,8 @@
(provide remove-provides provide? generate-prov get-alternate)
(define (provide? form)
(syntax-parse form
(define (provide? form)
(syntax-parse form
#:literals (#%provide)
[(#%provide . rest) form]
[_ #f]))
@ -36,8 +36,8 @@
;; provs: provides in this module
;; pos-blame-id: a #%variable-reference for the module
;; internal-id : the id being provided
;; if `internal-id' is defined in this module, we will produce a (begin def ... provide) block
;; internal-id : the id being provided
;; if `internal-id' is defined in this module, we will produce a (begin def ... provide) block
;; and a name to provide instead of internal-id
;; anything already recorded in the mapping is given an empty (begin) and the already-recorded id
@ -84,7 +84,7 @@
[export-id new-id]
[module-source pos-blame-id]
[the-contract (generate-temporary 'generated-contract)])
#`(begin
#`(begin
(define the-contract #,cnt)
(define-syntax cnt-id
(make-provide/contract-transformer
@ -99,7 +99,7 @@
(with-syntax* ([id internal-id]
[error-id (generate-temporary #'id)]
[export-id new-id])
#'(begin
#'(begin
(define-syntax (error-id stx)
(tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id)))
(def-export export-id id error-id)))

2
collects/typed-scheme/typecheck/signatures.rkt
View File

@ -30,7 +30,7 @@
[cond-contracted tc/rec-lambda/check (syntax? syntax? syntax? syntax? (listof Type/c) tc-results? . -> . tc-results?)]))
(define-signature tc-app^
([cond-contracted tc/app (syntax? . -> . tc-results?)]
([cond-contracted tc/app (syntax? . -> . tc-results?)]
[cond-contracted tc/app/check (syntax? tc-results? . -> . tc-results?)]))
(define-signature tc-apply^

14
collects/typed-scheme/typecheck/tc-app-helper.rkt
View File

@ -25,7 +25,7 @@
[(and rest (< (length t-a) (length dom)))
(tc-error/expr #:return (ret t-r)
"Wrong number of arguments, expected at least ~a and got ~a" (length dom) (length t-a))])
(for ([dom-t (if rest (in-sequence-forever dom rest) (in-list dom))]
(for ([dom-t (if rest (in-sequence-forever dom rest) (in-list dom))]
[a (in-list (syntax->list args-stx))]
[arg-t (in-list t-a)])
(parameterize ([current-orig-stx a]) (check-below arg-t dom-t))))
@ -39,7 +39,7 @@
(values (if (>= nm dom-count) (make-Empty) oa)
ta))])
(define-values (t-r f-r o-r)
(for/lists (t-r f-r o-r)
(for/lists (t-r f-r o-r)
([r (in-list results)])
(open-Result r o-a t-a)))
(ret t-r f-r o-r)))]
@ -74,7 +74,7 @@
(#:expected (c:or/c #f tc-results?) #:return tc-results?
#:msg-thunk (c:-> string? string?))
. c:->* . tc-results?)
(define arguments-str
(stringify-domain arg-tys
(if (not tail-bound) tail-ty #f)
@ -274,8 +274,8 @@
(define (poly-fail f-stx args-stx t argtypes #:name [name #f] #:expected [expected #f])
(match t
[(or (Poly-names:
msg-vars
[(or (Poly-names:
msg-vars
(Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests (list (Keyword: _ _ #f) ...)) ...)))
(PolyDots-names:
msg-vars
@ -286,7 +286,7 @@
(if (and (andmap null? msg-doms)
(null? argtypes))
(tc-error/expr #:return (ret (Un))
(string-append
(string-append
"Could not infer types for applying polymorphic "
fcn-string
"\n"))
@ -308,7 +308,7 @@
(if (and (andmap null? msg-doms)
(null? argtypes))
(tc-error/expr #:return (ret (Un))
(string-append
(string-append
"Could not infer types for applying polymorphic "
fcn-string
"\n"))

100
collects/typed-scheme/typecheck/tc-app.rkt
View File

@ -4,7 +4,7 @@
"signatures.rkt" "tc-metafunctions.rkt" "check-below.rkt"
"tc-app-helper.rkt" "find-annotation.rkt" "tc-funapp.rkt"
"tc-subst.rkt" (prefix-in c: racket/contract)
syntax/parse racket/match racket/trace scheme/list
syntax/parse racket/match racket/trace scheme/list
unstable/sequence unstable/list
;; fixme - don't need to be bound in this phase - only to make tests work
scheme/bool
@ -37,12 +37,12 @@
;; comparators that inform the type system
(define-syntax-class comparator
#:literals (eq? equal? eqv? = string=? symbol=? memq member memv)
(pattern eq?) (pattern equal?) (pattern eqv?) (pattern =) (pattern string=?) (pattern symbol=?)
(pattern eq?) (pattern equal?) (pattern eqv?) (pattern =) (pattern string=?) (pattern symbol=?)
(pattern member) (pattern memq) (pattern memv))
;; typecheck eq? applications
;; identifier expr expr -> tc-results
(define (tc/eq comparator v1 v2)
(define (tc/eq comparator v1 v2)
(define (eq?-able e) (or (boolean? e) (keyword? e) (symbol? e) (eof-object? e)))
(define (eqv?-able e) (or (eq?-able e) (number? e)))
(define (equal?-able e) #t)
@ -71,7 +71,7 @@
(and (? (lambda _ (free-identifier=? #'memq comparator)))
(tc-result1: (app untuple (list (and ts (Value: (? eq?-able))) ...))))))
(let ([ty (apply Un ts)])
(ret (Un (-val #f) t)
(ret (Un (-val #f) t)
(-FS (-filter-at ty o)
(-not-filter-at ty o))))]
[(_ _) (ret -Boolean)]))
@ -91,7 +91,7 @@
[('() '())
(void)]
[(_ '())
(if error?
(if error?
(tc-error/expr #:return (ret (Un))
"Unexpected keyword argument ~a" (car actual-kws))
#f)]
@ -104,7 +104,7 @@
#f)]
[_ (loop actual-kws actuals rst)])]
[((cons k kws-rest) (cons (Keyword: k* t req?) form-rest))
(cond [(eq? k k*) ;; we have a match
(cond [(eq? k k*) ;; we have a match
(if (subtype (car actuals) t)
;; success
(loop kws-rest (cdr actuals) form-rest)
@ -115,7 +115,7 @@
t (car actuals) k)
(loop kws-rest (cdr actuals) form-rest)))]
[req? ;; this keyword argument was required
(if error?
(if error?
(begin (tc-error/delayed "Missing keyword argument ~a" k*)
(loop kws-rest (cdr actuals) form-rest))
#f)]
@ -124,13 +124,13 @@
(define (tc-keywords form arities kws kw-args pos-args expected)
(match arities
[(list (and a (arr: dom rng rest #f ktys)))
[(list (and a (arr: dom rng rest #f ktys)))
(tc-keywords/internal a kws kw-args #t)
(tc/funapp (car (syntax-e form)) kw-args
(ret (make-Function (list (make-arr* dom rng #:rest rest))))
(map tc-expr (syntax->list pos-args)) expected)]
[(list (and a (arr: doms rngs rests (and drests #f) ktyss)) ...)
(let ([new-arities
(let ([new-arities
(for/list ([a (in-list arities)]
;; find all the arities where the keywords match
#:when (tc-keywords/internal a kws kw-args #f))
@ -167,7 +167,7 @@
(match t
[(tc-result1: (? Mu? t*)) (loop (ret (unfold t*)))]
[(tc-result1: (Union: '())) (ret (Un))]
[(tc-result1: (and c (Class: pos-tys (list (and tnflds (list tnames _ _)) ...) _)))
[(tc-result1: (and c (Class: pos-tys (list (and tnflds (list tnames _ _)) ...) _)))
(unless (= (length pos-tys)
(length (syntax->list pos-args)))
(tc-error/delayed "expected ~a positional arguments, but got ~a"
@ -178,7 +178,7 @@
(tc-expr/check pa (ret pt)))
(for ([n names]
#:when (not (memq n tnames)))
(tc-error/delayed
(tc-error/delayed
"unknown named argument ~a for class\nlegal named arguments are ~a"
n (stringify tnames)))
(for-each (match-lambda
@ -202,7 +202,7 @@
;; let loop
(define (let-loop-check form lam lp actuals args body expected)
(syntax-parse #`(#,args #,body #,actuals)
(syntax-parse #`(#,args #,body #,actuals)
#:literals (#%plain-app if null? pair? null)
[((val acc ...)
((~and inner-body (if (#%plain-app (~or pair? null?) val*) thn els)))
@ -231,10 +231,10 @@
#:when (free-identifier=? #'val #'e3)
(let ([ts (for/list ([ac (syntax->list #'(actuals ...))]
[f (syntax->list #'(acc ...))])
(or
(or
(type-annotation f #:infer #t)
(generalize (tc-expr/t ac))))]
[acc-ty (or
[acc-ty (or
(type-annotation #'val #:infer #t)
(match expected
[(tc-result1: (and t (Listof: _))) t]
@ -277,7 +277,7 @@
[(tc-result1: (Param: a b))
(check-below vt a)
(loop (cddr args))]
[(tc-result1: t)
[(tc-result1: t)
(tc-error/expr #:return (or expected (ret Univ)) "expected Parameter, but got ~a" t)
(loop (cddr args))]))))]
;; use the additional but normally ignored first argument to make-sequence to provide a better instantiation
@ -286,7 +286,7 @@
(match (single-value #'op)
[(tc-result1: (and t Poly?))
(tc-expr/check #'quo (ret Univ))
(tc/funapp #'op #'(quo arg)
(tc/funapp #'op #'(quo arg)
(ret (instantiate-poly t (extend (list Univ Univ)
(map type-annotation (syntax->list #'(i ...)))
Univ)))
@ -296,9 +296,9 @@
[(#%plain-app (~and op (~or (~literal unsafe-struct-ref) (~literal unsafe-struct*-ref))) s e:expr)
(let ([e-t (single-value #'e)])
(match (single-value #'s)
[(tc-result1:
[(tc-result1:
(and t (or (Struct: _ _ (list (fld: flds _ muts) ...) _ _ _ _ _)
(? needs-resolving?
(? needs-resolving?
(app resolve-once
(Struct: _ _ (list (fld: flds _ muts) ...) _ _ _ _ _))))))
(let ([ival (or (syntax-parse #'e [((~literal quote) i:number) (syntax-e #'i)] [_ #f])
@ -329,8 +329,8 @@
(let ([e-t (single-value #'e)])
(match (single-value #'s)
[(tc-result1: (and t (or (Struct: _ _ (list (fld: flds _ _) ...) _ _ _ _ _)
(? needs-resolving?
(app resolve-once
(? needs-resolving?
(app resolve-once
(Struct: _ _ (list (fld: flds _ _) ...) _ _ _ _ _))))))
(let ([ival (or (syntax-parse #'e [((~literal quote) i:number) (syntax-e #'i)] [_ #f])
(match e-t
@ -369,11 +369,11 @@
[_ #f]))])
(cond [(not ival)
(check-below e-t -Integer)
(if expected
(if expected
(check-below (ret (apply Un es)) expected)
(ret (apply Un es)))]
[(and (integer? ival) (exact? ival) (<= 0 ival (sub1 (length es))))
(if expected
(if expected
(check-below (ret (list-ref es ival)) expected)
(ret (list-ref es ival)))]
[(not (and (integer? ival) (exact? ival)))
@ -402,7 +402,7 @@
"expected statically known index for heterogeneous vector, but got ~a" (match e-t [(tc-result1: t) t]))]
[(and (integer? ival) (exact? ival) (<= 0 ival (sub1 (length es))))
(tc-expr/check #'val (ret (list-ref es ival)))
(if expected
(if expected
(check-below (ret -Void) expected)
(ret -Void))]
[(not (and (integer? ival) (exact? ival)))
@ -428,7 +428,7 @@
expected]
[(tc-result1: (HeterogenousVector: ts))
(unless (= (length ts) (length (syntax->list #'(args ...))))
(tc-error/expr "expected vector with ~a elements, but got ~a"
(tc-error/expr "expected vector with ~a elements, but got ~a"
(length ts)
(make-HeterogenousVector (map tc-expr/t (syntax->list #'(args ...))))))
(for ([e (in-list (syntax->list #'(args ...)))]
@ -533,7 +533,7 @@
[(#%plain-app values . args)
(match expected
[(tc-results: ets efs eos)
(match-let ([(list (tc-result1: ts fs os) ...)
(match-let ([(list (tc-result1: ts fs os) ...)
(for/list ([arg (syntax->list #'args)]
[et ets] [ef efs] [eo eos])
(single-value arg (ret et ef eo)))])
@ -541,13 +541,13 @@
(ret ts fs os)
(tc-error/expr #:return expected "wrong number of values: expected ~a but got ~a"
(length ets) (length (syntax->list #'args)))))]
[_ (match-let ([(list (tc-result1: ts fs os) ...)
[_ (match-let ([(list (tc-result1: ts fs os) ...)
(for/list ([arg (syntax->list #'args)])
(single-value arg))])
(ret ts fs os))])]
;; special case for keywords
[(#%plain-app
(#%plain-app cpce s-kp fn kpe kws num)
(#%plain-app cpce s-kp fn kpe kws num)
kw-list
(#%plain-app list . kw-arg-list)
. pos-args)
@ -555,7 +555,7 @@
#:declare s-kp (id-from 'struct:keyword-procedure 'racket/private/kw)
#:declare kpe (id-from 'keyword-procedure-extract 'racket/private/kw)
(match (tc-expr #'fn)
[(tc-result1: (Poly: vars
[(tc-result1: (Poly: vars
(Function: (list (and ar (arr: dom rng (and rest #f) (and drest #f) kw-formals))))))
(=> fail)
(unless (null? (fv/list kw-formals))
@ -565,7 +565,7 @@
(let* ([subst (infer vars null argtys-t dom rng (and expected (tc-results->values expected)))])
(tc-keywords form (list (subst-all subst ar))
(type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected))])]
[(tc-result1: (Function: arities))
[(tc-result1: (Function: arities))
(tc-keywords form arities (type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected)]
[(tc-result1: (Poly: _ (Function: _)))
(tc-error/expr #:return (ret (Un))
@ -574,19 +574,19 @@
"Cannot apply expression of type ~a, since it is not a function type" t)])]
;; even more special case for match
[(#%plain-app (letrec-values ([(lp) (~and lam (#%plain-lambda args . body))]) lp*) . actuals)
#:fail-unless expected #f
#:fail-unless expected #f
#:fail-unless (not (andmap type-annotation (syntax->list #'(lp . args)))) #f
#:fail-unless (free-identifier=? #'lp #'lp*) #f
(let-loop-check form #'lam #'lp #'actuals #'args #'body expected)]
;; special cases for classes
[(#%plain-app make-object cl . args)
[(#%plain-app make-object cl . args)
(check-do-make-object #'cl #'args #'() #'())]
[(#%plain-app do-make-object cl (#%plain-app list . pos-args) (#%plain-app list (#%plain-app cons 'names named-args) ...))
(check-do-make-object #'cl #'pos-args #'(names ...) #'(named-args ...))]
[(#%plain-app (~and map-expr (~literal 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))
[((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
@ -621,9 +621,9 @@
;; if it's not a ListDots, defer to the regular function typechecking
[_ (tc/funapp #'fun #'(f arg) (single-value #'fun) (list ft arg-ty) expected)]))]
;; special case for `delay'
[(#%plain-app
mp1
(#%plain-lambda ()
[(#%plain-app
mp1
(#%plain-lambda ()
(#%plain-app mp2 (#%plain-app call-with-values (#%plain-lambda () e) list))))
#:declare mp1 (id-from 'make-promise 'scheme/promise)
#:declare mp2 (id-from 'make-promise 'scheme/promise)
@ -633,7 +633,7 @@
(begin
;(printf "calling list: ~a ~a\n" (syntax->datum #'args) expected)
(match expected
[(tc-result1: (Mu: var (Union: (or
[(tc-result1: (Mu: var (Union: (or
(list (Pair: elem-ty (F: var)) (Value: '()))
(list (Value: '()) (Pair: elem-ty (F: var)))))))
;(printf "special case 1 ~a\n" elem-ty)
@ -642,7 +642,7 @@
expected]
[(tc-result1: (app untuple (? (lambda (ts) (and ts (= (length (syntax->list #'args))
(length ts))))
ts)))
ts)))
;(printf "special case 2 ~a\n" ts)
(for ([ac (in-list (syntax->list #'args))]
[exp (in-list ts)])
@ -668,7 +668,7 @@
[_
(match (single-value #'arg)
[(tc-result1: (List: ts))
(if expected
(if expected
(check-below (ret (-Tuple (reverse ts))) expected)
(ret (-Tuple (reverse ts))))]
[arg-ty
@ -676,39 +676,39 @@
;; inference for ((lambda
[(#%plain-app (#%plain-lambda (x ...) . body) args ...)
#:fail-unless (= (length (syntax->list #'(x ...)))
(length (syntax->list #'(args ...))))
(length (syntax->list #'(args ...))))
#f
#:fail-when (andmap type-annotation (syntax->list #'(x ...))) #f
(tc/let-values #'((x) ...) #'(args ...) #'body
(tc/let-values #'((x) ...) #'(args ...) #'body
#'(let-values ([(x) args] ...) . body)
expected)]
;; inference for ((lambda with dotted rest
;; inference for ((lambda with dotted rest
[(#%plain-app (#%plain-lambda (x ... . rst:id) . body) args ...)
#:fail-unless (<= (length (syntax->list #'(x ...)))
(length (syntax->list #'(args ...)))) #f
;; FIXME - remove this restriction - doesn't work because the annotation
;; FIXME - remove this restriction - doesn't work because the annotation
;; on rst is not a normal annotation, may have * or ...
#:fail-when (type-annotation #'rst) #f
#:fail-when (andmap type-annotation (syntax->list #'(x ...))) #f
(let-values ([(fixed-args varargs) (split-at (syntax->list #'(args ...)) (length (syntax->list #'(x ...))))])
(with-syntax ([(fixed-args ...) fixed-args]
[varg #`(#%plain-app list #,@varargs)])
(tc/let-values #'((x) ... (rst)) #`(fixed-args ... varg) #'body
(tc/let-values #'((x) ... (rst)) #`(fixed-args ... varg) #'body
#'(let-values ([(x) fixed-args] ... [(rst) varg]) . body)
expected)))]
[(#%plain-app f . args)
(let* ([f-ty (single-value #'f)])
(match f-ty
[(tc-result1:
(and t (Function:
(list (and a (arr: (? (lambda (d)
(= (length d)
[(tc-result1:
(and t (Function:
(list (and a (arr: (? (lambda (d)
(= (length d)
(length (syntax->list #'args))))
dom)
(Values: (list (Result: v (FilterSet: (Top:) (Top:)) (Empty:))))
#f #f (list (Keyword: _ _ #f) ...)))))))
;(printf "f dom: ~a ~a\n" (syntax->datum #'f) dom)
(let ([arg-tys (map (lambda (a t) (tc-expr/check a (ret t)))
(let ([arg-tys (map (lambda (a t) (tc-expr/check a (ret t)))
(syntax->list #'args)
dom)])
(tc/funapp #'f #'args f-ty arg-tys expected))]
@ -719,8 +719,8 @@
;(trace tc/app/internal)
;; syntax -> tc-results
(define (tc/app form) (tc/app/internal form #f))
(define (tc/app form) (tc/app/internal form #f))
;; syntax tc-results? -> tc-results?
(define (tc/app/check form expected)
(define t (tc/app/internal form expected))

34
collects/typed-scheme/typecheck/tc-apply.rkt
View File

@ -22,12 +22,12 @@
(export tc-apply^)
(define (do-ret t)
(match t
(match t
[(Values: (list (Result: ts _ _) ...)) (ret ts)]
[(ValuesDots: (list (Result: ts _ _) ...) dty dbound) (ret ts (for/list ([t ts]) (-FS null null)) (for/list ([t ts]) (make-Empty)) dty dbound)]
[_ (int-err "do-ret fails: ~a" t)]))
(define (tc/apply f args)
(define (tc/apply f args)
(define f-ty (single-value f))
;; produces the first n-1 elements of the list, and the last element
(define (split l) (let-values ([(f r) (split-at l (sub1 (length l)))])
@ -49,13 +49,13 @@
[arg-tys (map (match-lambda [(tc-result1: t _ _) t]) arg-tres)]
[(tc-result1: tail-ty) (single-value tail)])
(let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests])
(cond
;; we've run out of cases to try, so error out
(cond
;; we've run out of cases to try, so error out
[(null? doms*)
(domain-mismatches f args t doms rests drests rngs arg-tres tail-ty #f
#:return (ret (Un))
#:msg-thunk (lambda (dom)
(string-append
(string-append
"Bad arguments to function in apply:\n"
dom)))]
;; this case of the function type has a rest argument
@ -87,12 +87,12 @@
[t (values t #f)])])
(let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests])
(cond [(null? doms*)
(match f-ty
(match f-ty
[(tc-result1: (and t (Poly-names: _ (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1)))))
(domain-mismatches f args t doms rests drests rngs arg-tres tail-ty tail-bound
#:return (ret (Un))
#:msg-thunk (lambda (dom)
(string-append
(string-append
"Bad arguments to polymorphic function in apply:\n"
dom)))])]
;; the actual work, when we have a * function and a list final argument
@ -101,7 +101,7 @@
(<= (length (car doms*))
(length arg-tys))
(infer/vararg vars null
(cons tail-ty arg-tys)
(cons tail-ty arg-tys)
(cons (make-Listof (car rests*))
(car doms*))
(car rests*)
@ -109,7 +109,7 @@
=> (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
;; actual work, when we have a * function and ... final arg
[(and (car rests*)
tail-bound
tail-bound
(<= (length (car doms*))
(length arg-tys))
(infer/vararg vars null
@ -120,12 +120,12 @@
(car rngs*)))
=> (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg
[(and (car drests*)
[(and (car drests*)
tail-bound
(eq? tail-bound (cdr (car drests*)))
(= (length (car doms*))
(length arg-tys))
(infer vars null (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*))
(infer vars null (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*))
(car rngs*)))
=> (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
;; if nothing matches, around the loop again
@ -144,12 +144,12 @@
(let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests])
(define (finish substitution) (do-ret (subst-all substitution (car rngs*))))
(cond [(null? doms*)
(match f-ty
(match f-ty
[(tc-result1: (and t (PolyDots-names: _ (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1)))))
(domain-mismatches f args t doms rests drests rngs arg-tres tail-ty tail-bound
#:return (ret (Un))
#:msg-thunk (lambda (dom)
(string-append
(string-append
"Bad arguments to polymorphic function in apply:\n"
dom)))])]
;; the actual work, when we have a * function and a list final argument
@ -158,7 +158,7 @@
(<= (length (car doms*))
(length arg-tys))
(infer/vararg fixed-vars (list dotted-var)
(cons tail-ty arg-tys)
(cons tail-ty arg-tys)
(cons (make-Listof (car rests*))
(car doms*))
(car rests*)
@ -166,7 +166,7 @@
=> finish]
;; actual work, when we have a * function and ... final arg
[(and (car rests*)
tail-bound
tail-bound
(<= (length (car doms*))
(length arg-tys))
(infer/vararg fixed-vars (list dotted-var)
@ -181,7 +181,7 @@
tail-bound
(eq? tail-bound (cdr (car drests*)))
(= (length (car doms*))
(length arg-tys))
(length arg-tys))
(infer fixed-vars (list dotted-var)
(cons (make-ListDots tail-ty tail-bound) arg-tys)
(cons (make-ListDots (car (car drests*)) (cdr (car drests*))) (car doms*))
@ -194,7 +194,7 @@
(= (length (car doms*))
(length arg-tys))
(extend-tvars (list tail-bound (cdr (car drests*)))
(extend-indexes (cdr (car drests*))
(extend-indexes (cdr (car drests*))
;; don't need to add tail-bound - it must already be an index
(infer fixed-vars (list dotted-var)
(cons (make-ListDots tail-ty tail-bound) arg-tys)

26
collects/typed-scheme/typecheck/tc-envops.rkt
View File

@ -1,7 +1,7 @@
#lang scheme/base
(require (rename-in "../utils/utils.rkt" [infer infer-in]))
(require (rename-in (types subtype convenience remove-intersect union)
(require (rename-in (types subtype convenience remove-intersect union)
[-> -->]
[->* -->*]
[one-of/c -one-of/c])
@ -9,7 +9,7 @@
(rep type-rep object-rep)
(utils tc-utils)
(types resolve)
(only-in (env type-env-structs lexical-env)
(only-in (env type-env-structs lexical-env)
env? update-type/lexical env-map env-props replace-props)
scheme/contract racket/match
mzlib/trace unstable/struct
@ -30,34 +30,34 @@
(make-Pair t (update s (-filter u x rst)))]
[((Pair: t s) (NotTypeFilter: u (list rst ... (CdrPE:)) x))
(make-Pair t (update s (-not-filter u x rst)))]
;; syntax ops
[((Syntax: t) (TypeFilter: u (list rst ... (SyntaxPE:)) x))
(make-Syntax (update t (-filter u x rst)))]
[((Syntax: t) (NotTypeFilter: u (list rst ... (SyntaxPE:)) x))
(make-Syntax (update t (-not-filter u x rst)))]
;; struct ops
[((Struct: nm par flds proc poly pred cert maker-id)
(TypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x))
(make-Struct nm par
(list-update flds idx
(match-lambda [(fld: e acc-id #f)
[((Struct: nm par flds proc poly pred cert maker-id)
(TypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x))
(make-Struct nm par
(list-update flds idx
(match-lambda [(fld: e acc-id #f)
(make-fld
(update e (-filter u x rst))
acc-id #f)]
[_ (int-err "update on mutable struct field")]))
proc poly pred cert maker-id)]
[((Struct: nm par flds proc poly pred cert maker-id)
[((Struct: nm par flds proc poly pred cert maker-id)
(NotTypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x))
(make-Struct nm par (list-update flds idx
(match-lambda [(fld: e acc-id #f)
(make-Struct nm par (list-update flds idx
(match-lambda [(fld: e acc-id #f)
(make-fld
(update e (-not-filter u x rst))
acc-id #f)]
[_ (int-err "update on mutable struct field")]))
proc poly pred cert maker-id)]
;; otherwise
[(t (TypeFilter: u (list) _))
(restrict t u)]

60
collects/typed-scheme/typecheck/tc-expr-unit.rkt
View File

@ -11,7 +11,7 @@
(only-in (infer infer) restrict)
(except-in (utils tc-utils stxclass-util))
(env lexical-env type-env-structs tvar-env index-env)
racket/private/class-internal
racket/private/class-internal
(except-in syntax/parse id)
unstable/function
(only-in srfi/1 split-at))
@ -29,7 +29,7 @@
#:fail-unless expected #f
#:attr datum (syntax-e #'i)
#:fail-unless (subtype (-val (attribute datum)) expected) #f))
(syntax-parse v-stx
(syntax-parse v-stx
[i:exp expected]
[i:boolean (-val (syntax-e #'i))]
[i:identifier (-val (syntax-e #'i))]
@ -89,11 +89,11 @@
[(~var i (3d vector?))
(match expected
[(Vector: t)
(make-Vector (apply Un
(make-Vector (apply Un
(for/list ([l (in-vector (syntax-e #'i))])
(tc-literal l t))))]
[(HeterogenousVector: ts)
(make-HeterogenousVector
(make-HeterogenousVector
(for/list ([l (in-vector (syntax-e #'i))]
[t (in-list ts)])
(tc-literal l t)))]
@ -174,7 +174,7 @@
(--> identifier? tc-results?)
(let* ([ty (lookup-type/lexical id)])
(ret ty
(make-FilterSet (-not-filter (-val #f) id)
(make-FilterSet (-not-filter (-val #f) id)
(-filter (-val #f) id))
(make-Path null id))))
@ -195,12 +195,12 @@
(define (tc-expr/check form expected)
(parameterize ([current-orig-stx form])
;; the argument must be syntax
(unless (syntax? form)
(unless (syntax? form)
(int-err "bad form input to tc-expr: ~a" form))
;; typecheck form
(let loop ([form* form] [expected expected] [checked? #f])
(cond [(type-ascription form*)
=>
(cond [(type-ascription form*)
=>
(lambda (ann)
(let* ([r (tc-expr/check/internal form* ann)]
[r* (check-below r expected)])
@ -234,10 +234,10 @@
(parameterize ([current-orig-stx form])
;(printf "form: ~a\n" (syntax-object->datum form))
;; the argument must be syntax
(unless (syntax? form)
(unless (syntax? form)
(int-err "bad form input to tc-expr: ~a" form))
(let (;; a local version of ret that does the checking
[ret
[ret
(lambda args
(define te (apply ret args))
(check-below te expected))])
@ -247,7 +247,7 @@
[stx
#:when (syntax-property form 'typechecker:with-handlers)
(check-subforms/with-handlers/check form expected)]
[stx
[stx
#:when (syntax-property form 'typechecker:ignore-some)
(let ([ty (check-subforms/ignore form)])
(unless ty
@ -280,8 +280,8 @@
[(with-continuation-mark e1 e2 e3)
(begin (tc-expr/check/type #'e1 Univ)
(tc-expr/check/type #'e2 Univ)
(tc-expr/check #'e3 expected))]
;; application
(tc-expr/check #'e3 expected))]
;; application
[(#%plain-app . _) (tc/app/check form expected)]
;; #%expression
[(#%expression e) (tc-expr/check #'e expected)]
@ -328,29 +328,29 @@
;; syntax[expr] -> type
(define (tc-expr form)
;; do the actual typechecking of form
;; internal-tc-expr : syntax -> Type
;; internal-tc-expr : syntax -> Type
(define (internal-tc-expr form)
(syntax-parse form
#:literal-sets (kernel-literals)
#:literals (#%app lambda find-method/who)
;;
;;
[stx
#:when (syntax-property form 'typechecker:with-handlers)
(let ([ty (check-subforms/with-handlers form)])
(unless ty
(int-err "internal error: with-handlers"))
ty)]
[stx
[stx
#:when (syntax-property form 'typechecker:ignore-some)
(let ([ty (check-subforms/ignore form)])
(unless ty
(int-err "internal error: ignore-some"))
ty)]
;; data
[(quote #f) (ret (-val #f) false-filter)]
[(quote #t) (ret (-val #t) true-filter)]
[(quote val) (ret (tc-literal #'val) true-filter)]
;; syntax
[(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)) true-filter)]
@ -361,9 +361,9 @@
(tc-expr #'e3))]
;; lambda
[(#%plain-lambda formals . body)
(tc/lambda form #'(formals) #'(body))]
(tc/lambda form #'(formals) #'(body))]
[(case-lambda [formals . body] ...)
(tc/lambda form #'(formals ...) #'(body ...))]
(tc/lambda form #'(formals ...) #'(body ...))]
;; send
[(let-values (((_) meth))
(let-values (((_ _) (~and find-app (#%plain-app find-method/who _ rcvr _))))
@ -373,14 +373,14 @@
[(let-values ([(name ...) expr] ...) . body)
(tc/let-values #'((name ...) ...) #'(expr ...) #'body form)]
[(letrec-values ([(name ...) expr] ...) . body)
(tc/letrec-values #'((name ...) ...) #'(expr ...) #'body form)]
(tc/letrec-values #'((name ...) ...) #'(expr ...) #'body form)]
;; mutation!
[(set! id val)
(match-let* ([(tc-result1: id-t) (tc-expr #'id)]
[(tc-result1: val-t) (tc-expr #'val)])
(unless (subtype val-t id-t)
(tc-error/expr "Mutation only allowed with compatible types:\n~a is not a subtype of ~a" val-t id-t))
(ret -Void))]
(ret -Void))]
;; top-level variable reference - occurs at top level
[(#%top . id) (tc-id #'id)]
;; #%expression
@ -390,18 +390,18 @@
(tc-error/expr #:return (ret (Un)) "#%variable-reference is not supported by Typed Racket")]
;; identifiers
[x:identifier (tc-id #'x)]
;; application
;; application
[(#%plain-app . _) (tc/app form)]
;; if
[(if tst thn els) (tc/if-twoarm #'tst #'thn #'els)]
[(if tst thn els) (tc/if-twoarm #'tst #'thn #'els)]
;; syntax
;; for now, we ignore the rhs of macros
[(letrec-syntaxes+values stxs vals . body)
(tc-expr (syntax/loc form (letrec-values vals . body)))]
;; begin
[(begin e . es) (tc-exprs (syntax->list #'(e . es)))]
[(begin0 e . es)
@ -409,11 +409,11 @@
(tc-expr #'e))]
;; other
[_ (tc-error/expr #:return (ret (Un)) "cannot typecheck unknown form : ~a\n" (syntax->datum form))]))
(parameterize ([current-orig-stx form])
;(printf "form: ~a\n" (syntax->datum form))
;; the argument must be syntax
(unless (syntax? form)
(unless (syntax? form)
(int-err "bad form input to tc-expr: ~a" form))
;; typecheck form
(let ([ty (cond [(type-ascription form) => (lambda (ann)
@ -443,7 +443,7 @@
[(tc-result1: t) (int-err "non-symbol methods not supported by Typed Racket: ~a" t)])]
[(tc-result1: t) (tc-error/expr #:return (or expected (ret (Un))) "send: expected a class instance, got ~a" t)]))
(define (single-value form [expected #f])
(define (single-value form [expected #f])
(define t (if expected (tc-expr/check form expected) (tc-expr form)))
(match t
[(tc-result1: _ _ _) t]

26
collects/typed-scheme/typecheck/tc-funapp.rkt
View File

@ -46,7 +46,7 @@
(tc/funapp1 f-stx args-stx a argtys expected)]
[((tc-result1: (and t (Function: (and arrs (list (arr: doms rngs rests (and drests #f) kws) ...)))))
(and argtys (list (tc-result1: argtys-t) ...)))
(or
(or
;; find the first function where the argument types match
(for/first ([dom doms] [rng rngs] [rest rests] [a arrs]
#:when (subtypes/varargs argtys-t dom rest))
@ -60,13 +60,13 @@
(string-append "No function domains matched in function application:\n"
dom))))]
;; any kind of dotted polymorphic function without mandatory keyword args
[((tc-result1: (and t (PolyDots:
[((tc-result1: (and t (PolyDots:
(and vars (list fixed-vars ... dotted-var))
(Function: (list (and arrs (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...))) ...)))))
(list (tc-result1: argtys-t) ...))
(handle-clauses (doms rngs rests drests arrs) f-stx args-stx
;; only try inference if the argument lengths are appropriate
(lambda (dom _ rest drest a)
(lambda (dom _ rest drest a)
(cond [rest (<= (length dom) (length argtys))]
[drest (and (<= (length dom) (length argtys))
(eq? dotted-var (cdr drest)))]
@ -74,11 +74,11 @@
;; only try to infer the free vars of the rng (which includes the vars in filters/objects)
;; note that we have to use argtys-t here, since argtys is a list of tc-results
(lambda (dom rng rest drest a)
(cond
(cond
[drest
(infer/dots fixed-vars dotted-var argtys-t dom (car drest) rng (fv rng)
(infer/dots fixed-vars dotted-var argtys-t dom (car drest) rng (fv rng)
#:expected (and expected (tc-results->values expected)))]
[rest
[rest
(infer/vararg fixed-vars (list dotted-var) argtys-t dom rest rng
(and expected (tc-results->values expected)))]
;; no rest or drest
@ -86,10 +86,10 @@
(and expected (tc-results->values expected)))]))
t argtys expected)]
;; regular polymorphic functions without dotted rest, and without mandatory keyword args
[((tc-result1:
[((tc-result1:
(and t
(Poly:
vars
(Poly:
vars
(Function: (list (and arrs (arr: doms rngs rests (and drests #f) (list (Keyword: _ _ #f) ...))) ...)))))
(list (tc-result1: argtys-t) ...))
(handle-clauses (doms rngs rests arrs) f-stx args-stx
@ -105,11 +105,11 @@
;; parameters are functions too
[((tc-result1: (Param: in out)) (list)) (ret out)]
[((tc-result1: (Param: in out)) (list (tc-result1: t)))
(if (subtype t in)
(if (subtype t in)
(ret -Void true-filter)
(tc-error/expr #:return (ret -Void true-filter)
"Wrong argument to parameter - expected ~a and got ~a" in t))]
[((tc-result1: (Param: _ _)) _)
[((tc-result1: (Param: _ _)) _)
(tc-error/expr #:return (ret (Un))
"Wrong number of arguments to parameter - expected 0 or 1, got ~a"
(length argtys))]
@ -118,12 +118,12 @@
(tc/funapp f-stx args-stx (ret (resolve-once t) f o) argtys expected)]
;; a union of functions can be applied if we can apply all of the elements
[((tc-result1: (Union: (and ts (list (Function: _) ...)))) _)
(ret (for/fold ([result (Un)]) ([fty ts])
(ret (for/fold ([result (Un)]) ([fty ts])
(match (tc/funapp f-stx args-stx (ret fty) argtys expected)
[(tc-result1: t) (Un result t)])))]
;; error type is a perfectly good fcn type
[((tc-result1: (Error:)) _) (ret (make-Error))]
;; otherwise fail
[((tc-result1: f-ty) _)
[((tc-result1: f-ty) _)
(tc-error/expr #:return (ret (Un))
"Cannot apply expression of type ~a, since it is not a function type" f-ty)]))

6
collects/typed-scheme/typecheck/tc-if.rkt
View File

@ -10,10 +10,10 @@
(typecheck tc-envops tc-metafunctions)
(types type-table)
syntax/kerncase
racket/trace
racket/trace
racket/match)
;; if typechecking
;; if typechecking
(import tc-expr^)
(export tc-if^)
@ -45,7 +45,7 @@
[env-els (env+ (lexical-env) (list fs-) flag-)]
[new-thn-props (filter (λ (e) (and (atomic-filter? e) (not (memq e (env-props (lexical-env))))))
(env-props env-thn))]
[new-els-props (filter (λ (e) (and (atomic-filter? e) (not (memq e (env-props (lexical-env))))))
[new-els-props (filter (λ (e) (and (atomic-filter? e) (not (memq e (env-props (lexical-env))))))
(env-props env-els))]
[(tc-results: ts fs2 os2) (with-lexical-env env-thn (tc thn (unbox flag+)))]
[(tc-results: us fs3 os3) (with-lexical-env env-els (tc els (unbox flag-)))])

26
collects/typed-scheme/typecheck/tc-let-unit.rkt
View File

@ -8,12 +8,12 @@
(env lexical-env type-alias-env global-env type-env-structs)
(rep type-rep)
syntax/free-vars
;racket/trace
;racket/trace
racket/match (prefix-in c: racket/contract)
(except-in racket/contract -> ->* one-of/c)
syntax/kerncase syntax/parse unstable/syntax
(for-template
(for-template
racket/base
"internal-forms.rkt"))
@ -32,13 +32,13 @@
(listof (listof identifier?)) (listof tc-results?) (listof tc-results?)
syntax? (listof syntax?) syntax? (listof syntax?) (or/c #f tc-results?))
(#:abstract any/c)
. c:->* .
. c:->* .
tc-results?)
(with-cond-contract t/p ([types (listof (listof Type/c))] ; types that may contain undefined (letrec)
[expected-types (listof (listof Type/c))] ; types that may not contain undefined (what we got from the user)
[props (listof (listof Filter?))])
(define-values (types expected-types props)
(for/lists (t e p)
(for/lists (t e p)
([r (in-list results)]
[e-r (in-list expected-results)]
[names (in-list namess)])
@ -69,7 +69,7 @@
(append p1 p2)
(for-each expr->type
clauses
exprs
exprs
expected-results)
(let ([subber (lambda (proc lst)
(for/list ([i (in-list lst)])
@ -91,8 +91,8 @@
expected-types ; types w/o undefined
(append p1 p2)
;; typecheck the body
(if expected
(check-below
(if expected
(check-below
(run (tc-exprs/check (syntax->list body) (erase-filter expected)))
expected)
(run (tc-exprs (syntax->list body))))))))
@ -126,7 +126,7 @@
names
exprs)
(let loop ([names names] [exprs exprs] [flat-names orig-flat-names] [clauses clauses])
(cond
(cond
;; after everything, check the body expressions
[(null? names)
;(if expected (tc-exprs/check (syntax->list body) expected) (tc-exprs (syntax->list body)))
@ -137,7 +137,7 @@
;; then check this expression separately
(with-lexical-env/extend
(list (car names))
(list (match (get-type/infer (car names) (car exprs) (lambda (e) (tc-expr/maybe-expected/t e (car names)))
(list (match (get-type/infer (car names) (car exprs) (lambda (e) (tc-expr/maybe-expected/t e (car names)))
tc-expr/check)
[(tc-results: ts) ts]))
(loop (cdr names) (cdr exprs) (apply append (cdr names)) (cdr clauses)))]
@ -216,7 +216,7 @@
[(#%plain-lambda () _)
#:fail-unless (and expected (syntax-property e 'typechecker:called-in-tail-position)) #f
(tc-expr/check e (ret (-> (tc-results->values expected))))]
[_
[_
#:fail-unless (and expected (syntax-property e 'typechecker:called-in-tail-position)) #f
(tc-expr/check e expected)]
[_ (tc-expr e)]))
@ -229,8 +229,8 @@
;; the types of the exprs
#;[inferred-types (map (tc-expr-t/maybe-expected expected) exprs)]
;; the annotated types of the name (possibly using the inferred types)
[types (for/list ([name names] [e exprs])
(get-type/infer name e (tc-expr-t/maybe-expected expected)
[types (for/list ([name names] [e exprs])
(get-type/infer name e (tc-expr-t/maybe-expected expected)
tc-expr/check))]
;; the clauses for error reporting
[clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])])

22
collects/typed-scheme/typecheck/tc-metafunctions.rkt
View File

@ -1,7 +1,7 @@
#lang racket/base
(require "../utils/utils.rkt"
(rename-in (types subtype convenience remove-intersect union utils filter-ops)
(rename-in (types subtype convenience remove-intersect union utils filter-ops)
[-> -->]
[->* -->*]
[one-of/c -one-of/c])
@ -17,7 +17,7 @@
(define keys (for/list ([(nm k) (in-indexed arg-names)]) k))
(match results
[(tc-results: ts fs os dty dbound)
(make-ValuesDots
(make-ValuesDots
(for/list ([t ts] [f fs] [o os])
(make-Result t (abstract-filter arg-names keys f) (abstract-object arg-names keys o)))
dty dbound)]
@ -34,7 +34,7 @@
(define-match-expander lookup:
(syntax-rules ()
[(_ i) (app lookup (? values i))]))
(match o
(match o
[(Path: p (lookup: idx)) (make-Path p idx)]
[_ (make-Empty)]))
@ -58,7 +58,7 @@
(define (rec f) (abo xs idxs f))
(define (sb-t t) t)
(filter-case (#:Type sb-t #:Filter rec) f
[#:TypeFilter
[#:TypeFilter
t p (lookup: idx)
(-filter t idx p)]
[#:NotTypeFilter
@ -78,9 +78,9 @@
(define/cond-contract (resolve atoms prop)
((listof Filter/c)
((listof Filter/c)
Filter/c
. -> .
. -> .
Filter/c)
(for/fold ([prop prop])
([a (in-list atoms)])
@ -104,18 +104,18 @@
(define/cond-contract (combine-props new-props old-props flag)
((listof Filter/c) (listof Filter/c) (box/c boolean?)
. -> .
. -> .
(values (listof (or/c ImpFilter? OrFilter? AndFilter?)) (listof (or/c TypeFilter? NotTypeFilter?))))
(define (atomic-prop? p) (or (TypeFilter? p) (NotTypeFilter? p)))
(define-values (new-atoms new-formulas) (partition atomic-prop? (flatten-props new-props)))
(let loop ([derived-props null]
(let loop ([derived-props null]
[derived-atoms new-atoms]
[worklist (append old-props new-formulas)])
(if (null? worklist)
(values derived-props derived-atoms)
(let* ([p (car worklist)]
[p (resolve derived-atoms p)])
(match p
(match p
[(AndFilter: ps) (loop derived-props derived-atoms (append ps (cdr worklist)))]
[(ImpFilter: a c)
;(printf "combining ~a with ~a\n" p (append derived-props derived-atoms))
@ -123,10 +123,10 @@
(implied-atomic? a p))
(loop derived-props derived-atoms (cons c (cdr worklist)))
(loop (cons p derived-props) derived-atoms (cdr worklist)))]
[(OrFilter: ps)
[(OrFilter: ps)
(let ([new-or
(let or-loop ([ps ps] [result null])
(cond
(cond
[(null? ps) (apply -or result)]
[(for/or ([other-p (in-list (append derived-props derived-atoms))])
(opposite? (car ps) other-p))

34
collects/typed-scheme/typecheck/tc-structs.rkt
View File

@ -1,6 +1,6 @@
#lang scheme/base
(require "../utils/utils.rkt"
(require "../utils/utils.rkt"
(except-in (rep type-rep free-variance) Dotted)
(private parse-type)
(types convenience utils union resolve abbrev substitute type-table)
@ -9,8 +9,8 @@
"def-binding.rkt"
syntax/kerncase
syntax/struct
mzlib/trace
mzlib/trace
racket/function
racket/match
(only-in racket/contract
@ -36,7 +36,7 @@
(identifier? #'a)
#t]
[_ #f]))
(kernel-syntax-case* stx #f
(kernel-syntax-case* stx #f
(define-typed-struct-internal values)
[(#%define-values () (begin (quote-syntax (define-typed-struct-internal (ids ...) nm/par . rest)) (#%plain-app values)))
(and (andmap identifier? (syntax->list #'(ids ...)))
@ -72,7 +72,7 @@
(values (reverse getters) (reverse setters))
(loop (cddr l) (cons (car l) getters) (cons (cadr l) setters)))))
(match (build-struct-names nm flds #f (not setters?) nm)
[(list sty maker pred getters/setters ...)
[(list sty maker pred getters/setters ...)
(if setters?
(let-values ([(getters setters) (split getters/setters)])
(values sty maker pred getters setters))
@ -89,8 +89,8 @@
;; construct all the various types for structs, and then register the approriate names
;; identifier listof[identifier] type listof[fld] listof[Type] boolean -> Type listof[Type] listof[Type]
(define/cond-contract (mk/register-sty nm flds parent parent-fields types
#:wrapper [wrapper values]
(define/cond-contract (mk/register-sty nm flds parent parent-fields types
#:wrapper [wrapper values]
#:type-wrapper [type-wrapper values]
#:pred-wrapper [pred-wrapper values]
#:mutable [setters? #f]
@ -101,7 +101,7 @@
#:constructor-return [cret #f]
#:poly? [poly? #f]
#:type-only [type-only #f])
(c->* (identifier? (listof identifier?) (or/c Type/c #f) (listof fld?) (listof Type/c))
(c->* (identifier? (listof identifier?) (or/c Type/c #f) (listof fld?) (listof Type/c))
(#:wrapper procedure?
#:type-wrapper procedure?
#:pred-wrapper procedure?
@ -131,7 +131,7 @@
(if type-only
(register-type-name nm (wrapper sty))
(register-struct-types nm sty fld-names external-fld-types
external-fld-types/no-parent setters?
external-fld-types/no-parent setters?
#:wrapper wrapper
#:type-wrapper type-wrapper
#:pred-wrapper pred-wrapper
@ -180,7 +180,7 @@
(define parent-count (- (length external-fld-types) (length external-fld-types/no-parent)))
;; the list of names w/ types
(define bindings
(list*
(list*
(cons struct-type-id
(make-StructType sty))
(cons (or maker* maker)
@ -192,14 +192,14 @@
(append
(for/list ([g (in-list getters)] [t (in-list external-fld-types/no-parent)] [i (in-naturals parent-count)])
(let* ([path (make-StructPE name i)]
[func (if setters?
[func (if setters?
(->* (list name) t)
(->acc (list name) t (list path)))])
(add-struct-fn! g path #f)
(cons g (wrapper func))))
(if setters?
(for/list ([g (in-list setters)] [t (in-list external-fld-types/no-parent)] [i (in-naturals parent-count)])
(add-struct-fn! g (make-StructPE name i) #t)
(add-struct-fn! g (make-StructPE name i) #t)
(cons g (wrapper (->* (list name t) -Void))))
null))))
(register-type-name nm (wrapper sty))
@ -227,7 +227,7 @@
;; parse the field types
(map parse-type tys))))
;; instantiate the parent if necessary, with new-tvars
(define concrete-parent
(define concrete-parent
(if (Poly? parent)
(instantiate-poly parent new-tvars)
parent))
@ -248,7 +248,7 @@
;; typecheck a non-polymophic struct and register the approriate types
;; tc/struct : (U identifier (list identifier identifier)) Listof[identifier] Listof[syntax] -> void
(define/cond-contract (tc/struct nm/par flds tys [proc-ty #f]
(define/cond-contract (tc/struct nm/par flds tys [proc-ty #f]
#:maker [maker #f] #:constructor-return [cret #f] #:mutable [mutable #f]
#:predicate [pred #f]
#:type-only [type-only #f])
@ -264,7 +264,7 @@
(define-values (nm parent-name parent name name-tvar) (parse-parent nm/par))
;; parse the field types, and determine if the type is recursive
(define types (map parse-type tys))
(define proc-ty-parsed
(define proc-ty-parsed
(if proc-ty
(parse-type proc-ty)
#f))
@ -293,8 +293,8 @@
#:mutable #t)))
;; syntax for tc/builtin-struct
(define-syntax (d-s stx)
(syntax-case stx (:)
(define-syntax (d-s stx)
(syntax-case stx (:)
[(_ (nm par) ([fld : ty] ...) (par-ty ...))
#'(tc/builtin-struct #'nm #'par
(list #'fld ...)

18
collects/typed-scheme/typecheck/tc-subst.rkt
View File

@ -1,12 +1,12 @@
#lang scheme/base
(require "../utils/utils.rkt")
(require (rename-in (types subtype convenience remove-intersect union utils filter-ops)
(require (rename-in (types subtype convenience remove-intersect union utils filter-ops)
[-> -->]
[->* -->*]
[one-of/c -one-of/c])
(rep type-rep filter-rep rep-utils) scheme/list
scheme/contract racket/match unstable/match
scheme/contract racket/match unstable/match
(for-syntax scheme/base)
"tc-metafunctions.rkt")
@ -26,7 +26,7 @@
(define/cond-contract (subst-filter-set fs k o polarity [t #f])
(->* ((or/c FilterSet? NoFilter?) name-ref/c Object? boolean?) ((or/c #f Type/c)) FilterSet?)
(define extra-filter (if t (make-TypeFilter t null k) -top))
(define (add-extra-filter f)
(define (add-extra-filter f)
(define f* (-and extra-filter f))
(match f*
[(Bot:) f*]
@ -41,7 +41,7 @@
(-> Type/c name-ref/c Object? boolean? Type/c)
(define (st t) (subst-type t k o polarity))
(define/cond-contract (sf fs) (FilterSet? . -> . FilterSet?) (subst-filter-set fs k o polarity))
(type-case (#:Type st
(type-case (#:Type st
#:Filter sf
#:Object (lambda (f) (subst-object f k o polarity)))
t
@ -71,13 +71,13 @@
[(Path: p* i*) (make-Path (append p p*) i*)])
t)]))
;; this is the substitution metafunction
;; this is the substitution metafunction
(define/cond-contract (subst-filter f k o polarity)
(-> Filter/c name-ref/c Object? boolean? Filter/c)
(define (ap f) (subst-filter f k o polarity))
(define (tf-matcher t p i k o polarity maker)
(match o
[(or (Empty:) (NoObject:))
[(or (Empty:) (NoObject:))
(cond [(name-ref=? i k)
(if polarity -top -bot)]
[(index-free-in? k t) (if polarity -top -bot)]
@ -103,7 +103,7 @@
(tf-matcher t p i k o polarity -not-filter)]))
(define (index-free-in? k type)
(let/ec
(let/ec
return
(define (for-object o)
(object-case (#:Type for-type)
@ -151,8 +151,8 @@
(match tc
[(ValuesDots: (list (and rs (Result: ts fs os)) ...) dty dbound)
(if formals
(let-values ([(ts fs os)
(for/lists (ts fs os) ([r (in-list rs)])
(let-values ([(ts fs os)
(for/lists (ts fs os) ([r (in-list rs)])
(open-Result r (map (lambda (i) (make-Path null i)) formals)))])
(ret ts fs os
(for/fold ([dty dty]) ([(o k) (in-indexed (in-list formals))])

98
collects/typed-scheme/typecheck/tc-toplevel.rkt
View File

@ -2,7 +2,7 @@
(require (rename-in "../utils/utils.rkt" [infer r:infer])
syntax/kerncase
unstable/list racket/syntax syntax/parse
unstable/list racket/syntax syntax/parse
mzlib/etc
racket/match
"signatures.rkt"
@ -19,14 +19,14 @@
"provide-handling.rkt"
"def-binding.rkt"
(prefix-in c: racket/contract)
racket/dict
racket/dict
(for-template
"internal-forms.rkt"
syntax/location
mzlib/contract
scheme/base))
(c:provide/contract
(c:provide/contract
[type-check (syntax? . c:-> . syntax?)]
[tc-module (syntax? . c:-> . syntax?)]
[tc-toplevel-form (syntax? . c:-> . c:any/c)])
@ -36,18 +36,18 @@
(define (tc-toplevel/pass1 form)
(parameterize ([current-orig-stx form])
(syntax-parse form
#:literals (values define-type-alias-internal define-typed-struct-internal define-type-internal
#:literals (values define-type-alias-internal define-typed-struct-internal define-type-internal
define-typed-struct/exec-internal :-internal assert-predicate-internal
require/typed-internal declare-refinement-internal
define-values quote-syntax #%plain-app begin)
;#:literal-sets (kernel-literals)
;; forms that are handled in other ways
[stx
#:when (or (syntax-property form 'typechecker:ignore)
[stx
#:when (or (syntax-property form 'typechecker:ignore)
(syntax-property form 'typechecker:ignore-some))
(list)]
;; type aliases have already been handled by an earlier pass
[(define-values () (begin (quote-syntax (define-type-alias-internal nm ty)) (#%plain-app values)))
(list)]
@ -63,52 +63,52 @@
(register-type #'pred new-t))
(list)]
[t (tc-error "cannot declare refinement for non-predicate ~a" t)])]
;; require/typed
[(define-values () (begin (quote-syntax (require/typed-internal nm ty)) (#%plain-app values)))
(let ([t (parse-type #'ty)])
(register-type #'nm t)
(list (make-def-binding #'nm t)))]
[(define-values () (begin (quote-syntax (require/typed-internal nm ty #:struct-maker parent)) (#%plain-app values)))
(let* ([t (parse-type #'ty)]
[flds (map fld-t (Struct-flds (lookup-type-name (Name-id t))))]
[mk-ty (flds #f . ->* . t)])
(register-type #'nm mk-ty)
(list (make-def-binding #'nm mk-ty)))]
;; define-typed-struct
[(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...))) (#%plain-app values)))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)))]
[(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...) #:mutable)) (#%plain-app values)))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)) #:mutable #t)]
[(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...)
#:maker m #:constructor-return t #:predicate p))
[(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...)
#:maker m #:constructor-return t #:predicate p))
(#%plain-app values)))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...))
#:maker #'m #:constructor-return #'t #:predicate #'p)]
[(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...)
#:maker m #:constructor-return t))
#:maker m #:constructor-return t))
(#%plain-app values)))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...))
#:maker #'m #:constructor-return #'t)]
[(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...)
#:maker m))
#:maker m))
(#%plain-app values)))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...))
#:maker #'m)]
[(define-values () (begin (quote-syntax (define-typed-struct-internal nm ([fld : ty] ...)
#:maker m #:mutable))
#:maker m #:mutable))
(#%plain-app values)))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...))
#:maker #'m #:mutable #t)]
[(define-values () (begin (quote-syntax (define-typed-struct-internal (vars ...) nm ([fld : ty] ...)
#:maker m))
#:maker m))
(#%plain-app values)))
(tc/poly-struct (syntax->list #'(vars ...)) #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...))
#:maker #'m)]
[(define-values () (begin (quote-syntax (define-typed-struct-internal (vars ...) nm ([fld : ty] ...)
#:maker m #:mutable))
#:maker m #:mutable))
(#%plain-app values)))
(tc/poly-struct (syntax->list #'(vars ...)) #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...))
#:maker #'m #:mutable #t)]
@ -123,26 +123,26 @@
;; error in other cases
[(define-values () (begin (quote-syntax (define-typed-struct-internal . _)) (#%plain-app values)))
(int-err "unknown structure form")]
;; executable structs - this is a big hack
[(define-values () (begin (quote-syntax (define-typed-struct/exec-internal nm ([fld : ty] ...) proc-ty)) (#%plain-app values)))
(tc/struct #'nm (syntax->list #'(fld ...)) (syntax->list #'(ty ...)) #'proc-ty)]
;; predicate assertion - needed for define-type b/c or doesn't work
[(define-values () (begin (quote-syntax (assert-predicate-internal ty pred)) (#%plain-app values)))
(register-type #'pred (make-pred-ty (parse-type #'ty)))]
;; top-level type annotation
[(define-values () (begin (quote-syntax (:-internal id:identifier ty)) (#%plain-app values)))
(register-type/undefined #'id (parse-type #'ty))]
;; values definitions
[(define-values (var ...) expr)
(let* ([vars (syntax->list #'(var ...))])
(cond
;; if all the variables have types, we stick them into the environment
[(andmap (lambda (s) (syntax-property s 'type-label)) vars)
[(andmap (lambda (s) (syntax-property s 'type-label)) vars)
(let ([ts (map (λ (x) (get-type x #:infer #f)) vars)])
(for-each register-type-if-undefined vars ts)
(map make-def-binding vars ts))]
@ -158,15 +158,15 @@
(register-type i t)
(free-id-table-set! unann-defs i #t)
(make-def-binding i t))])]))]
;; to handle the top-level, we have to recur into begins
[(begin . rest)
(apply append (filter list? (map tc-toplevel/pass1 (syntax->list #'rest))))]
;; define-syntaxes just get noted
[(define-syntaxes (var:id ...) . rest)
(map make-def-stx-binding (syntax->list #'(var ...)))]
;; otherwise, do nothing in this pass
;; handles expressions, provides, requires, etc and whatnot
[_ (list)])))
@ -180,24 +180,24 @@
;; syntax -> void
(define (tc-toplevel/pass2 form)
(parameterize ([current-orig-stx form])
(kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal define-type-internal
(kernel-syntax-case* form #f (define-type-alias-internal define-typed-struct-internal define-type-internal
require/typed-internal values)
;; these forms we have been instructed to ignore
[stx
[stx
(syntax-property form 'typechecker:ignore)
(void)]
;; this is a form that we mostly ignore, but we check some interior parts
[stx
[stx
(syntax-property form 'typechecker:ignore-some)
(check-subforms/ignore form)]
;; these forms should always be ignored
[(#%require . _) (void)]
[(#%provide . _) (void)]
[(define-syntaxes . _) (void)]
[(define-values-for-syntax . _) (void)]
;; FIXME - we no longer need these special cases
;; these forms are handled in pass1
[(define-values () (begin (quote-syntax (require/typed-internal . rest)) (#%plain-app values)))
@ -205,8 +205,8 @@
[(define-values () (begin (quote-syntax (define-type-alias-internal . rest)) (#%plain-app values)))
(void)]
[(define-values () (begin (quote-syntax (define-typed-struct-internal . rest)) (#%plain-app values)))
(void)]
(void)]
;; definitions just need to typecheck their bodies
[(define-values (var ...) expr)
(let* ([vars (syntax->list #'(var ...))]
@ -215,7 +215,7 @@
(free-id-table-ref unann-defs v (lambda _ #f)))
(tc-expr/check #'expr (ret ts)))
(void))]
;; to handle the top-level, we have to recur into begins
[(begin) (void)]
[(begin . rest)
@ -224,7 +224,7 @@
(tc-toplevel/pass2 (car l))
(begin (tc-toplevel/pass2 (car l))
(loop (cdr l)))))]
;; otherwise, the form was just an expression
[_ (tc-expr form)])))
@ -233,7 +233,7 @@
;; new implementation of type-check
(define-syntax-rule (internal-syntax-pred nm)
(lambda (form)
(kernel-syntax-case* form #f
(kernel-syntax-case* form #f
(nm values)
[(define-values () (begin (quote-syntax (nm . rest)) (#%plain-app values)))
#t]
@ -254,7 +254,7 @@
(for-each register-type-name names))
(define (parse-type-alias form)
(kernel-syntax-case* form #f
(kernel-syntax-case* form #f
(define-type-alias-internal values)
[(define-values () (begin (quote-syntax (define-type-alias-internal nm ty)) (#%plain-app values)))
(values #'nm #'ty)]
@ -264,23 +264,23 @@
(begin-with-definitions
(define forms (syntax->list forms0))
(define-values (type-aliases struct-defs stx-defs0 val-defs0 provs reqs)
(filter-multiple
(filter-multiple
forms
(internal-syntax-pred define-type-alias-internal)
(lambda (e) (or ((internal-syntax-pred define-typed-struct-internal) e)
((internal-syntax-pred define-typed-struct/exec-internal) e)))
parse-syntax-def
parse-def
parse-def
provide?
define/fixup-contract?))
(for-each (compose register-type-alias parse-type-alias) type-aliases)
(for-each (compose register-type-alias parse-type-alias) type-aliases)
;; add the struct names to the type table
(for-each (compose add-type-name! names-of-struct) struct-defs)
;; resolve all the type aliases, and error if there are cycles
(resolve-type-aliases parse-type)
;; do pass 1, and collect the defintions
(define defs (apply append (filter list? (map tc-toplevel/pass1 forms))))
;; separate the definitions into structures we'll handle for provides
;; separate the definitions into structures we'll handle for provides
(define def-tbl
(for/fold ([h (make-immutable-free-id-table)])
([def (in-list defs)])
@ -299,7 +299,7 @@
(for/fold ([h h]) ([f (syntax->list #'(form ...))])
(parameterize ([current-orig-stx f])
(syntax-parse f
[i:id
[i:id
(when (def-stx-binding? (dict-ref def-tbl #'i #f))
(set! syntax-provide? #t))
(dict-set h #'i #'i)]
@ -314,7 +314,7 @@
;; compute the new provides
(with-syntax*
([the-variable-reference (generate-temporary #'blame)]
[(new-provs ...)
[(new-provs ...)
(generate-prov def-tbl provide-tbl #'the-variable-reference)])
#`(begin
#,(if (null? (syntax-e #'(new-provs ...)))
@ -336,7 +336,7 @@
;; used only from #%top-interaction
;; syntax -> void
(define (tc-toplevel-form form)
(tc-toplevel/pass1 form)
(tc-toplevel/pass1 form)
(begin0 (tc-toplevel/pass2 form)
(report-all-errors)))

10
collects/typed-scheme/typed-reader.rkt
View File

@ -9,7 +9,7 @@
(let ([ch (peek-char port)])
(unless (eof-object? ch)
;; Consult current readtable:
(let-values ([(like-ch/sym proc dispatch-proc)
(let-values ([(like-ch/sym proc dispatch-proc)
(readtable-mapping (current-readtable) ch)])
;; If like-ch/sym is whitespace, then ch is whitespace
(when (and (char? like-ch/sym)
@ -28,7 +28,7 @@
(raise-read-eof-error "unexpected EOF in type annotation" src l c p 1))]
[else v]))))
(define (parse port read-one src)
(define (parse port read-one src)
(skip-whitespace port)
(let ([name (read-one)])
(begin0
@ -48,11 +48,11 @@
(datum->syntax name `(inst ,name : ,@elems)))]
;; arbitrary property annotation
[(PROP) (skip-whitespace port)
(let* ([prop-name (syntax-e (read-one))])
(let* ([prop-name (syntax-e (read-one))])
(skip-whitespace port)
(syntax-property name prop-name (read-one)))]
;; otherwise error
[else
[else
(let-values ([(l c p) (port-next-location port)])
(raise-read-error (format "typed expression ~a must be followed by :, ::, or @"
(syntax->datum name)) src l c p 1))])))
@ -68,7 +68,7 @@
;; `read-syntax' mode
(datum->syntax
#f
(parse port
(parse port
(lambda () (read-syntax src port ))
src)
(let-values ([(l c p) (port-next-location port)])

2
collects/typed-scheme/typed-scheme.rkt
View File

@ -22,7 +22,7 @@
((dynamic-require 'typed-scheme/base-env/base-env-numeric 'init)))
(define-syntax-rule (drivers [name sym] ...)
(begin
(begin
(define-syntax (name stx)
(do-standard-inits)
((dynamic-require 'typed-scheme/core 'sym) stx))

22
collects/typed-scheme/types/abbrev.rkt
View File

@ -192,7 +192,7 @@
;; convenient syntax
(define-syntax -v
(define-syntax -v
(syntax-rules ()
[(_ x) (make-F 'x)]))
@ -219,11 +219,11 @@
(define top-func (make-Function (list (make-top-arr))))
(define/cond-contract (make-arr* dom rng
(define/cond-contract (make-arr* dom rng
#:rest [rest #f] #:drest [drest #f] #:kws [kws null]
#:filters [filters -no-filter] #:object [obj -no-obj])
(c:->* ((listof Type/c) (or/c Values? ValuesDots? Type/c))
(#:rest (or/c #f Type/c)
(#:rest (or/c #f Type/c)
#:drest (or/c #f (cons/c Type/c symbol?))
#:kws (listof Keyword?)
#:filters FilterSet?
@ -238,7 +238,7 @@
(define-syntax-class c
(pattern x:id #:fail-unless (eq? ': (syntax-e #'x)) #f))
(syntax-parse stx
[(_ dom rng)
[(_ dom rng)
#'(make-Function (list (make-arr* dom rng)))]
[(_ dom rst rng)
#'(make-Function (list (make-arr* dom rng #:rest rst)))]
@ -290,7 +290,7 @@
[(_ [(dom ...) rng] ...)
#'(cl->* (dom ... . -> . rng) ...)]))
(define-syntax (->key stx)
(define-syntax (->key stx)
(syntax-parse stx
[(_ ty:expr ... (~seq k:keyword kty:expr opt:boolean) ... rng)
#'(make-Function
@ -307,7 +307,7 @@
(define/cond-contract (-filter t i [p null])
(c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)
(if (or (type-equal? Univ t) (and (identifier? i) (is-var-mutated? i)))
(if (or (type-equal? Univ t) (and (identifier? i) (is-var-mutated? i)))
-top
(make-TypeFilter t p i)))
@ -334,19 +334,19 @@
(c:-> (listof Type/c) Type/c Type/c Type/c)
(c:-> (listof Type/c) Type/c Type/c integer? Type/c)
(c:-> (listof Type/c) Type/c Type/c integer? (listof PathElem?) Type/c))
(case-lambda
(case-lambda
[(in out t n p)
(define xs (for/list ([(_ i) (in-indexed (in-list in))]) i))
(make-Function
(list
(make-arr*
in out
(make-arr*
in out
#:filters (-FS (-filter t (list-ref xs n) p) (-not-filter t (list-ref xs n) p)))))]
[(in out t n)
(make-pred-ty in out t n null)]
[(in out t)
(make-pred-ty in out t 0 null)]
[(t)
[(t)
(make-pred-ty (list Univ) -Boolean t 0 null)]))
(define true-filter (-FS -top -bot))
@ -355,7 +355,7 @@
(define false-lfilter (-FS -bot -top))
(define (opt-fn args opt-args result)
(apply cl->* (for/list ([i (in-range (add1 (length opt-args)))])
(apply cl->* (for/list ([i (in-range (add1 (length opt-args)))])
(make-Function (list (make-arr* (append args (take opt-args i)) result))))))
(define-syntax-rule (->opt args ... [opt ...] res)

12
collects/typed-scheme/types/filter-ops.rkt
View File

@ -94,7 +94,7 @@
[(and p (NotTypeFilter: t1 f1 x) (? (lambda _ (not or?))))
(hash-update! ntf-map
(list f1 (hash-name-ref x))
(match-lambda [(NotTypeFilter: t2 _ _)
(match-lambda [(NotTypeFilter: t2 _ _)
(-not-filter (Un t1 t2) x f1)]
[p (int-err "got something that isn't a nottypefilter ~a" p)])
p)
@ -119,7 +119,7 @@
(apply mk others)
(match-let ([(AndFilter: elems) (car ands)])
(apply -and (for/list ([a (in-list elems)])
(apply -or a (append (cdr ands) others)))))))
(apply -or a (append (cdr ands) others)))))))
(let loop ([fs args] [result null])
(if (null? fs)
(match result
@ -130,7 +130,7 @@
[(and t (Top:)) t]
[(OrFilter: fs*) (loop (append fs* (cdr fs)) result)]
[(Bot:) (loop (cdr fs) result)]
[t
[t
(cond [(for/or ([f (in-list (append (cdr fs) result))])
(opposite? f t))
-top]
@ -157,13 +157,13 @@
(if (filter-equal? f1 f2)
f1
(apply mk (compact (list f1 f2) #f))))]
[_
[_
;; first, remove anything implied by the atomic propositions
;; We commonly see: (And (Or P Q) (Or P R) (Or P S) ... P), which this fixes
(let-values ([(atomic not-atomic) (partition atomic-filter? result)])
(define not-atomic*
(define not-atomic*
(for/list ([p (in-list not-atomic)]
#:when
#:when
(not (for/or ([a (in-list atomic)])
(implied-atomic? p a))))
p))

42
collects/typed-scheme/types/printer.rkt
View File

@ -5,7 +5,7 @@
"types/abbrev.rkt" "types/numeric-tower.rkt" "types/subtype.rkt"
"utils/utils.rkt" "utils/tc-utils.rkt"))
;; do we attempt to find instantiations of polymorphic types to print?
;; do we attempt to find instantiations of polymorphic types to print?
;; FIXME - currently broken
(define print-poly-types? #t)
;; do we use simple type aliases in printing
@ -17,7 +17,7 @@
;; does t have a type name associated with it currently?
;; has-name : Type -> Maybe[Symbol]
(define (has-name? t)
(define (has-name? t)
(and print-aliases
(for/first ([(n t*) (in-pairs (in-list ((current-type-names))))]
#:when (and (Type? t*) (type-equal? t t*)))
@ -56,13 +56,13 @@
(match c
[(NoObject:) (fp "-")]
[(Empty:) (fp "-")]
[(Path: pes i) (fp "~a" (append pes (list i)))]
[(Path: pes i) (fp "~a" (append pes (list i)))]
[else (fp "(Unknown Object: ~a)" (struct->vector c))]))
;; print out a type
;; print-type : Type Port Boolean -> Void
(define (print-type c port write?)
(define (fp . args) (apply fprintf port args))
(define (fp . args) (apply fprintf port args))
(define (fp/filter fmt ret . rest)
(if (print-complex-filters?)
(apply fp fmt ret rest)
@ -83,7 +83,7 @@
(when rest
(fp "~a ~a " rest (if (special-dots-printing?) "...*" "*")))
(when drest
(fp "~a ...~a~a "
(fp "~a ...~a~a "
(car drest) (if (special-dots-printing?) "" " ") (cdr drest)))
(match rng
[(Values: (list (Result: t (FilterSet: (Top:) (Top:)) (Empty:))))
@ -91,18 +91,18 @@
[(Values: (list (Result: t
(FilterSet: (TypeFilter: ft pth id)
(NotTypeFilter: ft pth id))
(Empty:))))
(Empty:))))
(if (null? pth)
(fp "-> ~a : ~a" t ft)
(begin (fp "-> ~a : ~a @" t ft)
(for ([pe pth]) (fp " ~a" pe))))]
[(Values: (list (Result: t fs (Empty:))))
[(Values: (list (Result: t fs (Empty:))))
(fp/filter "-> ~a : ~a" t fs)]
[(Values: (list (Result: t lf lo)))
(fp/filter "-> ~a : ~a ~a" t lf lo)]
[_
(fp "-> ~a" rng)])
(fp ")")]
(fp ")")]
[else (fp "(Unknown Function Type: ~a)" (struct->vector a))]))
(define (tuple? t)
(match t
@ -127,7 +127,7 @@
[(ChannelTop:) (fp "Channel")]
[(VectorTop:) (fp "Vector")]
[(MPairTop:) (fp "MPair")]
[(App: rator rands stx)
[(App: rator rands stx)
(fp "~a" (list* rator rands))]
;; special cases for lists
[(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
@ -152,19 +152,19 @@
(fp " ~a" proc))
(fp ")")]
[(Function: arities)
(let ()
(let ()
(match arities
[(list) (fp "(case-lambda)")]
[(list a) (print-arr a)]
[(list a b ...) (fp "(case-lambda ")
(print-arr a)
(for-each
(print-arr a)
(for-each
(lambda (e) (fp " ") (print-arr e))
b)
(fp ")")]))]
[(arr: _ _ _ _ _) (fp "(arr ") (print-arr c) (fp ")")]
[(Vector: e) (fp "(Vectorof ~a)" e)]
[(HeterogenousVector: e) (fp "(Vector")
[(HeterogenousVector: e) (fp "(Vector")
(for ([i (in-list e)])
(fp " ~a" i))
(fp ")")]
@ -175,21 +175,21 @@
[(Set: e) (fp "(Setof ~a)" e)]
[(Union: elems) (fp "~a" (cons 'U elems))]
[(Pair: l r) (fp "(Pairof ~a ~a)" l r)]
[(ListDots: dty dbound)
[(ListDots: dty dbound)
(fp "(List ~a ...~a~a)" dty (if (special-dots-printing?) "" " ") dbound)]
[(F: nm) (fp "~a" nm)]
[(F: nm) (fp "~a" nm)]
;; FIXME
[(Values: (list v)) (fp "~a" v)]
[(Values: (list v ...)) (fp "~s" (cons 'values v))]
[(ValuesDots: v dty dbound) (fp "~s" (cons 'values (append v (list dty '... dbound))))]
[(Param: in out)
[(Param: in out)
(if (equal? in out)
(fp "(Parameterof ~a)" in)
(fp "(Parameterof ~a)" in)
(fp "(Parameterof ~a ~a)" in out))]
[(Hashtable: k v) (fp "(HashTable ~a ~a)" k v)]
#;[(Poly-unsafe: n b) (fp "(unsafe-poly ~a ~a ~a)" (Type-seq c) n b)]
[(Poly-names: names body)
[(Poly-names: names body)
#;(fprintf (current-error-port) "POLY SEQ: ~a\n" (Type-seq body))
(fp "(All ~a ~a)" names body)]
#;[(PolyDots-unsafe: n b) (fp "(unsafe-polydots ~a ~a ~a)" (Type-seq c) n b)]
@ -211,8 +211,8 @@
;; FIXME - this should not be used
#;
[(Scope: sc) (fp "(Scope ~a)" sc)]
[(B: idx) (fp "(B ~a)" idx)]
[(B: idx) (fp "(B ~a)" idx)]
[(Syntax: t) (fp "(Syntaxof ~a)" t)]
[(Instance: t) (fp "(Instance ~a)" t)]
[(Class: pf nf ms) (fp "(Class)")]

24
collects/typed-scheme/types/remove-intersect.rkt
View File

@ -1,6 +1,6 @@
#lang scheme/base
(require "../utils/utils.rkt"
(require "../utils/utils.rkt"
(rep type-rep rep-utils)
(types union subtype resolve convenience utils)
racket/match mzlib/trace)
@ -10,7 +10,7 @@
(define (overlap t1 t2)
(let ([ks (Type-key t1)] [kt (Type-key t2)])
(cond
(cond
[(and (symbol? ks) (symbol? kt) (not (eq? ks kt))) #f]
[(and (symbol? ks) (pair? kt) (not (memq ks kt))) #f]
[(and (symbol? kt) (pair? ks) (not (memq kt ks))) #f]
@ -18,20 +18,20 @@
(for/and ([i (in-list ks)]) (not (memq i kt))))
#f]
[else
(match (list t1 t2)
(match (list t1 t2)
[(list (Univ:) _) #t]
[(list _ (Univ:)) #t]
[(list (F: _) _) #t]
[(list _ (F: _)) #t]
[(list (Name: n) (Name: n*))
[(list (Name: n) (Name: n*))
(or (free-identifier=? n n*)
(overlap (resolve-once t1) (resolve-once t2)))]
[(list (? Mu?) _) (overlap (unfold t1) t2)]
[(list _ (? Mu?)) (overlap t1 (unfold t2))]
[(list (Refinement: t _ _) t2) (overlap t t2)]
[(list t1 (Refinement: t _ _)) (overlap t1 t)]
[(list (Union: e) t)
(ormap (lambda (t*) (overlap t* t)) e)]
[(list t (Union: e))
@ -45,7 +45,7 @@
(overlap t t*)]
[(or (list (Syntax: _) _)
(list _ (Syntax: _)))
#f]
#f]
[(list (Base: _ _ _ _) _) #f]
[(list _ (Base: _ _ _ _)) #f]
[(list (Value: (? pair? v)) (Pair: _ _)) #t]
@ -61,7 +61,7 @@
#f]
[(list (Struct: n _ flds _ _ _ _ _)
(Struct: n _ flds* _ _ _ _ _))
(for/and ([f flds] [f* flds*])
(for/and ([f flds] [f* flds*])
(match* (f f*)
[((fld: t _ _) (fld: t* _ _)) (overlap t t*)]))]
[(list (Struct: n #f _ _ _ _ _ _)
@ -80,8 +80,8 @@
[p2 (if (Name? p*) (resolve-name p*) p*)])
(or (and p2 (overlap t1 p2))
(and p1 (overlap t2 p1))
(and (= (length flds) (length flds*))
(for/and ([f flds] [f* flds*])
(and (= (length flds) (length flds*))
(for/and ([f flds] [f* flds*])
(match* (f f*)
[((fld: t _ _) (fld: t* _ _)) (overlap t t*)])))))]
[(list (== (-val eof))
@ -102,9 +102,9 @@
[(list (or (App: _ _ _) (Name: _)) t)
;; must be different, since they're not subtypes
;; and n must refer to a distinct struct type
old]
old]
[(list (Union: l) rem)
(apply Un (map (lambda (e) (*remove e rem)) l))]
(apply Un (map (lambda (e) (*remove e rem)) l))]
[(list (? Mu? old) t) (*remove (unfold old) t)]
[(list (Poly: vs b) t) (make-Poly vs (*remove b rem))]
[_ old])))

12
collects/typed-scheme/types/resolve.rkt
View File

@ -1,7 +1,7 @@
#lang scheme/base
(require "../utils/utils.rkt")
(require (rep type-rep rep-utils)
(require (rep type-rep rep-utils)
(env type-name-env)
(utils tc-utils)
(types utils)
@ -23,7 +23,7 @@
(define (resolve-app rator rands stx)
(parameterize ([current-orig-stx stx]
[already-resolving? #t])
(match rator
[(Poly-unsafe: n _)
@ -31,8 +31,8 @@
(tc-error "wrong number of arguments to polymorphic type: expected ~a and got ~a"
n (length rands)))
(instantiate-poly rator rands)]
[(Name: n)
(when (and (current-poly-struct)
[(Name: n)
(when (and (current-poly-struct)
(free-identifier=? n (poly-name (current-poly-struct)))
(not (or (ormap Error? rands)
(andmap type-equal? rands (poly-vars (current-poly-struct))))))
@ -50,11 +50,11 @@
(define (resolve-once t)
(define seq (Rep-seq t))
(define r (hash-ref resolver-cache seq #f))
(define r (hash-ref resolver-cache seq #f))
(or r
(let ([r* (match t
[(Mu: _ _) (unfold t)]
[(App: r r* s)
[(App: r r* s)
(resolve-app r r* s)]
[(Name: _) (resolve-name t)])])
(when r*

6
collects/typed-scheme/types/substitute.rkt
View File

@ -80,7 +80,7 @@
[#:ValuesDots types dty dbound
(if (eq? name dbound)
(make-Values
(append
(append
(map sb types)
;; We need to recur first, just to expand out any dotted usages of this.
(let ([expanded (sb dty)])
@ -93,7 +93,7 @@
[#:arr dom rng rest drest kws
(if (and (pair? drest)
(eq? name (cdr drest)))
(make-arr (append
(make-arr (append
(map sb dom)
;; We need to recur first, just to expand out any dotted usages of this.
(let ([expanded (sb (car drest))])
@ -149,7 +149,7 @@
[(i-subst imgs)
(substitute-dots imgs #f v t)]
[(i-subst/starred imgs rest)
(substitute-dots imgs rest v t)]
(substitute-dots imgs rest v t)]
[(i-subst/dotted null dty dbound)
(substitute-dotted dty dbound v t)]
[(i-subst/dotted imgs dty dbound)

32
collects/typed-scheme/types/subtype.rkt
View File

@ -75,7 +75,7 @@
(define (subtypes* A ss ts)
(cond [(and (null? ss) (null? ts) A)]
[(or (null? ss) (null? ts)) (fail! ss ts)]
[(subtype* A (car ss) (car ts))
[(subtype* A (car ss) (car ts))
=>
(lambda (A*) (subtypes* A* (cdr ss) (cdr ts)))]
[else (fail! (car ss) (car ts))]))
@ -100,11 +100,11 @@
A-last)))]))
(define (kw-subtypes* A0 t-kws s-kws)
(let loop ([A A0] [t t-kws] [s s-kws])
(let loop ([A A0] [t t-kws] [s s-kws])
(match* (t s)
[((list (Keyword: kt tt rt) rest-t) (list (Keyword: ks ts rs) rest-s))
(cond [(eq? kt ks)
(if
(if
;; if s is optional, t must be as well
(or rs (not rt))
(loop (subtype* A tt ts) rest-t rest-s)
@ -162,12 +162,12 @@
(subtypes* t-dom s-dom)
(kw-subtypes* t-kws s-kws)
(subtype* s-rng t-rng))]
[(_ _)
[(_ _)
(fail! s t)])))
(define (subtypes/varargs args dom rst)
(with-handlers
([exn:subtype? (lambda _ #f)])
([exn:subtype? (lambda _ #f)])
(subtypes*/varargs (empty-set) args dom rst)))
(define (subtypes*/varargs A0 argtys dom rst)
@ -240,7 +240,7 @@
(parameterize ([match-equality-test =t]
[current-seen A])
(let ([ks (Type-key s)] [kt (Type-key t)])
(cond
(cond
[(or (seen? s t) (type-equal? s t)) A]
[(and (symbol? ks) (symbol? kt) (not (eq? ks kt))) (fail! s t)]
[(and (symbol? ks) (pair? kt) (not (memq ks kt))) (fail! s t)]
@ -258,12 +258,12 @@
;; (Un) is bot
[(_ (Union: (list))) (fail! s t)]
[((Union: (list)) _) A0]
;; value types
;; value types
[((Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
;; values are subtypes of their "type"
[((Value: v) (Base: _ _ pred _)) (if (pred v) A0 (fail! s t))]
;; tvars are equal if they are the same variable
[((F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
[((F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
;; Avoid needing to resolve things that refer to different structs.
;; Saves us from non-termination
;; Must happen *before* the sequence cases, which sometimes call `resolve' in match expanders
@ -278,7 +278,7 @@
(fail! s t)]
[((or (? Struct? s1) (NameStruct: s1)) (Base: _ _ _ _))
(fail! s t)]
;; same for all values.
;; same for all values.
[((Value: (? (negate struct?) _)) (or (? Struct? s1) (NameStruct: s1)))
(fail! s t)]
[((or (? Struct? s1) (NameStruct: s1)) (Value: (? (negate struct?) _)))
@ -316,7 +316,7 @@
(when (null? arr1) (fail! s t))
(let loop-arities ([A* A0]
[arr2 arr2])
(cond
(cond
[(null? arr2) A*]
[(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))]
[else (fail! s t)]))]
@ -330,9 +330,9 @@
[((ListDots: s-dty dbound) (Listof: t-elem))
(subtype* A0 (substitute Univ dbound s-dty) t-elem)]
;; quantification over two types preserves subtyping
[((Poly: ns b1) (Poly: ms b2))
[((Poly: ns b1) (Poly: ms b2))
(=> unmatch)
(unless (= (length ns) (length ms))
(unless (= (length ns) (length ms))
(unmatch))
(subtype* A0 b1 (subst-all (make-simple-substitution ms (map make-F ns)) b2))]
[((Refinement: par _ _) t)
@ -340,7 +340,7 @@
;; use unification to see if we can use the polytype here
[((Poly: vs b) s)
(=> unmatch)
(if (unify vs (list b) (list s)) A0 (unmatch))]
(if (unify vs (list b) (list s)) A0 (unmatch))]
[(s (Poly: vs b))
(=> unmatch)
(if (null? (fv b)) (subtype* A0 s b) (unmatch))]
@ -360,7 +360,7 @@
(fail! s t))]
[(s (Union: es)) (or (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)
(fail! s t))]
;; subtyping on immutable structs is covariant
;; subtyping on immutable structs is covariant
[((Struct: nm _ flds proc _ _ _ _) (Struct: nm _ flds* proc* _ _ _ _))
(let ([A (cond [(and proc proc*) (subtype* proc proc*)]
[proc* (fail! proc proc*)]
@ -381,7 +381,7 @@
[((MPair: _ _) (MPairTop:)) A0]
[((Hashtable: _ _) (HashtableTop:)) A0]
;; subtyping on structs follows the declared hierarchy
[((Struct: nm (? Type? parent) flds proc _ _ _ _) other)
[((Struct: nm (? Type? parent) flds proc _ _ _ _) other)
;(dprintf "subtype - hierarchy : ~a ~a ~a\n" nm parent other)
(subtype* A0 parent other)]
;; Promises are covariant
@ -403,7 +403,7 @@
(subtype* A0 t t*)]
[((Class: '() '() (list (and s (list names meths )) ...))
(Class: '() '() (list (and s* (list names* meths*)) ...)))
(for/fold ([A A0])
(for/fold ([A A0])
([n names*] [m meths*])
(cond [(assq n s) => (lambda (spec) (subtype* A (cadr spec) m))]
[else (fail! s t)]))]

10
collects/typed-scheme/types/union.rkt
View File

@ -24,22 +24,22 @@
;; Union constructor
;; Normalizes representation by sorting types.
(define Un
(case-lambda
(case-lambda
[() empty-union]
[(t) t]
[args
;; a is a Type (not a union type)
;; b is a List[Type]
(define (union2 a b)
(define (union2 a b)
(define b* (make-union* b))
(cond
(cond
[(subtype a b*) (list b*)]
[(subtype b* a) (list a)]
[(subtype b* a) (list a)]
[else (cons a b)]))
(let ([types (remove-dups (sort (apply append (map flat args)) type<?))])
(cond
[(null? types) (make-union* null)]
[(null? (cdr types)) (car types)]
[(null? (cdr types)) (car types)]
;; FIXME: this sort is unneccessary
[else (make-union* (sort (foldr union2 '() (remove-subtypes types)) type<?))]))]))

18
collects/typed-scheme/types/utils.rkt
View File

@ -15,7 +15,7 @@
instantiate-poly
instantiate-poly-dotted
tc-result?
tc-result-equal?
tc-result-equal?
effects-equal?
tc-result-t
unfold
@ -35,7 +35,7 @@
(define (instantiate-poly t types)
(match t
[(Poly: ns body)
[(Poly: ns body)
(unless (= (length types) (length ns))
(int-err "instantiate-poly: wrong number of types: expected ~a, got ~a" (length ns) (length types)))
(subst-all (make-simple-substitution ns types) body)]
@ -52,7 +52,7 @@
(match t
[(PolyDots: (list fixed ... dotted) body)
(unless (= (length fixed) (length types))
(int-err "instantiate-poly-dotted: wrong number of types: expected ~a, got ~a, types were ~a"
(int-err "instantiate-poly-dotted: wrong number of types: expected ~a, got ~a, types were ~a"
(length fixed) (length types) types))
(let ([body* (subst-all (make-simple-substitution fixed types) body)])
(substitute-dotted image var dotted body*))]
@ -72,7 +72,7 @@
(syntax-parser
[(_ tp fp op)
#'(struct tc-results ((list (struct tc-result (tp fp op)) (... ...)) #f))]
[(_ tp fp op dty dbound)
[(_ tp fp op dty dbound)
#'(struct tc-results ((list (struct tc-result (tp fp op)) (... ...)) (cons dty dbound)))]
[(_ tp)
#'(struct tc-results ((list (struct tc-result (tp _ _)) (... ...)) #f))]))
@ -134,7 +134,7 @@
;(trace ret)
(provide/cond-contract
[ret
[ret
(->i ([t (or/c Type/c (listof Type/c))])
([f (t) (if (list? t)
(listof FilterSet/c)
@ -157,8 +157,8 @@
;; equality - good
(define tc-result-equal? equal?)
(define (effects-equal? fs1 fs2)
(and
(define (effects-equal? fs1 fs2)
(and
(= (length fs1) (length fs2))
(andmap eq? fs1 fs2)))
@ -175,7 +175,7 @@
return)
;; error for unbound variables
(define (lookup-fail e)
(define (lookup-fail e)
(match (identifier-binding e)
['lexical (tc-error/expr "untyped lexical variable ~a" (syntax-e e))]
[#f (tc-error/expr "untyped top-level identifier ~a" (syntax-e e))]
@ -183,7 +183,7 @@
(let-values ([(x y) (module-path-index-split nominal-source-mod)])
(cond [(and (not x) (not y))
(tc-error/expr "untyped identifier ~a" (syntax-e e))]
[else
[else
(tc-error/expr "untyped identifier ~a imported from module <~a>" (syntax-e e) x)]))]))
(define (lookup-type-fail i)

6
collects/typed-scheme/utils/any-wrap.rkt
View File

@ -11,7 +11,7 @@
(define (t v)
(match v
[(? (lambda (e) (and (any-wrap? e) (not wrap?)))) (any-wrap-val v)]
[(? (lambda (e)
[(? (lambda (e)
(or (number? e) (string? e) (char? e) (symbol? e)
(keyword? e) (bytes? e) (boolean? e) (void? e))))
v]
@ -31,9 +31,9 @@
(apply make-prefab-struct k (for/list ([i (in-vector vals 1)]) i)))]
[_ (if wrap? (make-any-wrap v) v)]))
t)
(define any-wrap/c
(make-contract
(make-contract
#:name 'Any
#:projection (compose traverse blame-original?)))

14
collects/typed-scheme/utils/require-contract.rkt
View File

@ -3,7 +3,7 @@
(require scheme/contract
syntax/location
(for-syntax scheme/base
syntax/parse
syntax/parse
(prefix-in tr: "../private/typed-renaming.rkt")))
(provide require/contract define-ignored)
@ -12,7 +12,7 @@
(syntax-case stx ()
[(_ name expr)
(syntax-case (local-expand/capture-lifts #'expr
'expression
'expression
null #;(list #'define-values))
(begin define-values)
[(begin (define-values (n) e) e*)
@ -38,8 +38,8 @@
(syntax-parse stx
[(require/contract nm:renameable cnt lib)
#`(begin (require (only-in lib [nm nm.r]))
(define-ignored nm
(contract cnt
(define-ignored nm
(contract cnt
(get-alternate nm.r)
'(interface for #,(syntax->datum #'nm))
(current-contract-region)
@ -47,9 +47,9 @@
(quote-srcloc nm))))]
[(require/contract (orig-nm:renameable nm:id) cnt lib)
#`(begin (require (only-in lib [orig-nm orig-nm.r]))
(define-ignored nm
(contract cnt
(get-alternate orig-nm.r)
(define-ignored nm
(contract cnt
(get-alternate orig-nm.r)
'#,(syntax->datum #'nm)
(current-contract-region)
(quote nm)

12
collects/typed-scheme/utils/stxclass-util.rkt
View File

@ -12,21 +12,21 @@
(syntax-parse stx
[(_ arg:expr attr:id pat)
(let* ([i (generate-temporary)]
[get-i (datum->syntax
i
(string->symbol
(string-append (symbol->string (syntax-e i))
[get-i (datum->syntax
i
(string->symbol
(string-append (symbol->string (syntax-e i))
"."
(symbol->string #'attr.datum))))])
(quasisyntax/loc stx
(syntax-parse arg
(syntax-parse arg
[#,i #:declare #,i pat #'#,get-i])))]))
(define (atom? v)
(or (number? v) (string? v) (boolean? v) (symbol? v) (keyword? v) (char? v) (bytes? v) (regexp? v)))
(define-syntax-class (3d pred)
(pattern s
(pattern s
#:attr datum (syntax-e #'s)
#:fail-unless (pred (attribute datum)) #f))

4
collects/typed-scheme/utils/tc-utils.rkt
View File

@ -107,7 +107,7 @@ don't depend on any other portion of the system
(raise-typecheck-error (apply format msg rest) (list stx)))))
;; produce a type error, using the current syntax
(define (tc-error msg . rest)
(define (tc-error msg . rest)
(let* ([ostx (current-orig-stx)]
[ostxs (if (list? ostx) ostx (list ostx))]
[stxs (map locate-stx ostxs)])
@ -136,7 +136,7 @@ don't depend on any other portion of the system
(define-struct (exn:fail:tc exn:fail) ())
;; raise an internal error - typechecker bug!
(define (int-err msg . args)
(define (int-err msg . args)
(raise (make-exn:fail:tc (string-append "Internal Typechecker Error: "
(apply format msg args)
(format "\nwhile typechecking\n~aoriginally\n~a"

38
collects/typed-scheme/utils/utils.rkt
View File

@ -1,12 +1,12 @@
#lang racket/base
#|
This file is for utilities that are of general interest,
This file is for utilities that are of general interest,
at least theoretically.
|#
(require (for-syntax racket/base syntax/parse racket/string)
racket/contract racket/require-syntax
racket/contract racket/require-syntax
racket/provide-syntax racket/unit (prefix-in d: unstable/debug)
racket/pretty mzlib/pconvert syntax/parse)
@ -17,7 +17,7 @@ at least theoretically.
;; optimization
optimize?
;; timing
start-timing do-time
start-timing do-time
;; logging
printf/log show-input?
;; struct printing
@ -39,14 +39,14 @@ at least theoretically.
(syntax-parse stx
[(form id:identifier ...)
(with-syntax ([(id* ...)
(map (lambda (id)
(datum->syntax
(map (lambda (id)
(datum->syntax
id
`(lib
,(datum->syntax
,(datum->syntax
#f
(string-join
(list "typed-scheme"
(list "typed-scheme"
(symbol->string (syntax-e #'nm))
(string-append (symbol->string (syntax-e id)) ".rkt"))
"/")
@ -60,14 +60,14 @@ at least theoretically.
(syntax-parse stx
[(_ id:identifier ...)
(with-syntax ([(id* ...)
(map (lambda (id)
(datum->syntax
(map (lambda (id)
(datum->syntax
id
`(lib
,(datum->syntax
,(datum->syntax
#f
(string-join
(list "typed-scheme"
(list "typed-scheme"
(symbol->string (syntax-e #'nm))
(string-append (symbol->string (syntax-e id)) ".rkt"))
"/")
@ -97,9 +97,9 @@ at least theoretically.
(define-for-syntax logging? #f)
(define-syntax (printf/log stx)
(if logging?
(if logging?
(syntax-case stx ()
[(_ fmt . args)
[(_ fmt . args)
#'(log-debug (format fmt . args))])
#'(void)))
@ -108,7 +108,7 @@ at least theoretically.
(define last-time (make-parameter #f))
(define-syntaxes (start-timing do-time)
(if timing?
(if timing?
(values
(syntax-rules ()
[(_ msg)
@ -151,13 +151,13 @@ at least theoretically.
(pretty-print (print-convert s))))
(define custom-printer (make-parameter #t))
(define-syntax (define-struct/printer stx)
(syntax-parse stx
[(form name (flds ...) printer:expr)
#`(define-struct name (flds ...)
#`(define-struct name (flds ...)
#:property prop:custom-print-quotable 'never
#:property prop:custom-write
#:property prop:custom-write
(lambda (a b c) (if (custom-printer) (printer a b c) (pseudo-printer a b c)))
#:transparent)]))
@ -205,7 +205,7 @@ at least theoretically.
(define-syntax define/cond-contract
(if enable-contracts?
(make-rename-transformer #'define/contract)
(lambda (stx)
(lambda (stx)
(syntax-parse stx
[(_ head cnt . body)
#'(define head . body)]))))
@ -221,7 +221,7 @@ at least theoretically.
(syntax-case stx ()
[(_ nm cnt)
(if enable-contracts?
(list #'[contracted (nm cnt)])
(list #'[contracted (nm cnt)])
(list #'nm))]))
(define (list-update l i f)