Fix abstraction of implications.

Fix contract for lookup-typed/lexical.
Default cases for printing.
Abstract out indexing functions for Nat/Integer split.

svn: r17272
This commit is contained in:
Sam Tobin-Hochstadt 2009-12-11 23:00:37 +00:00
parent dde2c1fb18
commit d0c8a19ce8
13 changed files with 176 additions and 109 deletions

View File

@ -4,7 +4,7 @@
"type-environments.ss"
"type-env.ss"
unstable/mutated-vars
(only-in scheme/contract ->* ->)
(only-in scheme/contract ->* -> or/c any/c)
(utils tc-utils)
(only-in (rep type-rep) Type/c)
(typecheck tc-metafunctions)
@ -12,7 +12,7 @@
(provide lexical-env with-lexical-env with-lexical-env/extend with-update-type/lexical)
(p/c
[lookup-type/lexical ((identifier?) (env?) . ->* . Type/c)]
[lookup-type/lexical ((identifier?) (env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type/c #f))]
[update-type/lexical (((identifier? Type/c . -> . Type/c) identifier?) (env?) . ->* . env?)])
;; the current lexical environment

View File

@ -22,7 +22,8 @@
;; add a single type to the mapping
;; identifier type -> void
(define (register-type id type)
;(printf "register-type ~a~n" (syntax-e id))
#;(when (eq? (syntax-e id) 'vector-ref)
(printf "register-type ~a~n" id))
(module-identifier-mapping-put! the-mapping id type))
;; add a single type to the mapping

View File

@ -10,7 +10,10 @@
#%top-interaction
lambda
#%app))
(require "private/base-env.ss" "private/base-special-env.ss"
(require "private/base-env.ss"
"private/base-special-env.ss"
"private/base-env-numeric.ss"
"private/base-env-indexing-old.ss"
(for-syntax "private/base-types-extra.ss"))
(provide (rename-out [with-handlers: with-handlers] [real? number?])
(for-syntax (all-from-out "private/base-types-extra.ss")))

View File

@ -0,0 +1,113 @@
#lang scheme
(require
"../utils/utils.ss"
scheme/tcp
scheme/unsafe/ops
(only-in rnrs/lists-6 fold-left)
'#%paramz
"extra-procs.ss"
(utils tc-utils )
(types union convenience)
(only-in '#%kernel [apply kernel:apply])
scheme/promise scheme/system
(only-in string-constants/private/only-once maybe-print-message)
(only-in scheme/match/runtime match:error matchable? match-equality-test)
(for-template scheme)
(rename-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym] [-Nat -Nat*]))
(provide indexing)
(define-syntax-rule (indexing -Nat)
(make-env
[build-list (-poly (a) (-Nat (-Nat* . -> . a) . -> . (-lst a)))]
[string-ref (-> -String -Nat -Char)]
[substring (->opt -String -Nat [-Nat] -String)]
[make-string (cl-> [(-Nat) -String] [(-Nat -Char) -String])]
[string-set! (-String -Nat -Char . -> . -Void)]
[list-ref (-poly (a) ((-lst a) -Nat . -> . a))]
[list-tail (-poly (a) ((-lst a) -Nat . -> . (-lst a)))]
[regexp-match
(let ([?outp (-opt -Output-Port)]
[N -Nat]
[?N (-opt -Nat)]
[optlist (lambda (t) (-opt (-lst (-opt t))))]
[-StrRx (Un -String -Regexp -PRegexp)]
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -Bytes)])
(cl->*
(-StrRx -String [N ?N ?outp] . ->opt . (optlist -String))
(-BtsRx -String [N ?N ?outp] . ->opt . (optlist -Bytes))
(-Pattern -InpBts [N ?N ?outp] . ->opt . (optlist -Bytes))))]
[regexp-match*
(let ([N -Nat]
[?N (-opt -Nat)]
[-StrRx (Un -String -Regexp -PRegexp)]
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -Bytes)])
(cl->*
(-StrRx -String [N ?N] . ->opt . (-lst -String))
(-BtsRx -String [N ?N] . ->opt . (-lst -Bytes))
(-Pattern -InpBts [N ?N] . ->opt . (-lst -Bytes))))]
[regexp-try-match
(let ([?outp (-opt -Output-Port)]
[?N (-opt -Nat)]
[optlist (lambda (t) (-opt (-lst (-opt t))))])
(->opt -Pattern -Input-Port [-Nat ?N ?outp] (optlist -Bytes)))]
[regexp-match-positions
(let ([?outp (-opt -Output-Port)]
[N -Nat]
[?N (-opt -Nat)]
[optlist (lambda (t) (-opt (-lst (-opt t))))]
[-StrRx (Un -String -Regexp -PRegexp)]
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -Bytes)])
(->opt -Pattern (Un -String -InpBts) [N ?N ?outp] (optlist (-pair -Nat -Nat))))]
[regexp-match-positions*
(let ([?outp (-opt -Output-Port)]
[?N (-opt -Nat)]
[optlist (lambda (t) (-opt (-lst (-opt t))))]
[-StrRx (Un -String -Regexp -PRegexp)]
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -Bytes)])
(->opt -Pattern (Un -String -InpBts) [-Nat ?N ?outp] (-lst (-pair -Nat -Nat))))]
[take (-poly (a) ((-lst a) -Nat . -> . (-lst a)))]
[drop (-poly (a) ((-lst a) -Nat . -> . (-lst a)))]
[take-right (-poly (a) ((-lst a) -Nat . -> . (-lst a)))]
[drop-right (-poly (a) ((-lst a) -Nat . -> . (-lst a)))]
[split-at
(-poly (a) ((list (-lst a)) -Nat . ->* . (-values (list (-lst a) (-lst a)))))]
[split-at-right
(-poly (a) ((list (-lst a)) -Nat . ->* . (-values (list (-lst a) (-lst a)))))]
[vector-ref (-poly (a) ((-vec a) -Nat . -> . a))]
[build-vector (-poly (a) (-Nat (-Nat . -> . a) . -> . (-vec a)))]
[vector-set! (-poly (a) (-> (-vec a) -Nat a -Void))]
[vector-copy! (-poly (a) ((-vec a) -Nat (-vec a) [-Nat -Nat] . ->opt . -Void))]
[make-vector (-poly (a) (cl-> [(-Nat) (-vec -Integer)]
[(-Nat a) (-vec a)]))]
[peek-char
(cl->* [->opt [-Input-Port -Nat] (Un -Char (-val eof))])]
[peek-byte
(cl->* [->opt [-Input-Port -Nat] (Un -Byte (-val eof))])]
;; string.ss
[real->decimal-string (N [-Nat] . ->opt . -String)]
[random (cl-> [(-Nat) -Nat*] [() -Real])]
[raise-type-error
(cl->
[(Sym -String Univ) (Un)]
[(Sym -String -Nat (-lst Univ)) (Un)])]
))

View File

@ -0,0 +1,11 @@
#lang scheme
(require
(rename-in "../utils/utils.ss" [infer r:infer])
(for-syntax (types abbrev) (env init-envs) (r:infer infer-dummy infer)
"base-env-indexing-abs.ss"))
(define-for-syntax e (parameterize ([infer-param infer]) (indexing -Integer)))
(begin-for-syntax (initialize-type-env e))

View File

@ -0,0 +1,11 @@
#lang scheme
(require
(rename-in "../utils/utils.ss" [infer r:infer])
(for-syntax (types abbrev) (env init-envs) (r:infer infer-dummy infer)
"base-env-indexing-abs.ss"))
(define-for-syntax e (parameterize ([infer-param infer]) (indexing -Nat)))
(begin-for-syntax (initialize-type-env e))

View File

@ -11,10 +11,7 @@
scheme/promise scheme/system
(only-in string-constants/private/only-once maybe-print-message)
(only-in scheme/match/runtime match:error matchable? match-equality-test)
(for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym]))
;; require the split-out files
"base-env-numeric.ss"
)
(for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym])))
[raise (Univ . -> . (Un))]
@ -91,8 +88,12 @@
[pair? (make-pred-ty (-pair Univ Univ)) #;(-poly (a b) (make-pred-ty (-pair a b)))]
[empty? (make-pred-ty (-val null))]
[empty (-val null)]
[string? (make-pred-ty -String)]
[string (->* '() -Char -String)]
[string-length (-String . -> . -Nat)]
[unsafe-string-length (-String . -> . -Nat)]
[symbol? (make-pred-ty Sym)]
[keyword? (make-pred-ty -Keyword)]
[list? (make-pred-ty (-lst Univ))]
@ -159,7 +160,6 @@
[sleep (N . -> . -Void)]
[build-list (-poly (a) (-Nat (-Nat . -> . a) . -> . (-lst a)))]
[reverse (-poly (a) (-> (-lst a) (-lst a)))]
[append (-poly (a) (->* (list) (-lst a) (-lst a)))]
[length (-poly (a) (-> (-lst a) -Nat))]
@ -207,8 +207,6 @@
[string-copy (-> -String -String)]
[string->immutable-string (-> -String -String)]
[string-ref (-> -String -Nat -Char)]
[substring (->opt -String -Nat [-Nat] -String)]
[string->path (-> -String -Path)]
[file-exists? (-> -Pathlike B)]
@ -224,7 +222,6 @@
#:mode (one-of/c 'binary 'text) #f
a))]
[random (cl-> [(-Nat) -Nat] [() -Real])]
[assq (-poly (a b) (a (-lst (-pair a b)) . -> . (-opt (-pair a b))))]
[assv (-poly (a b) (a (-lst (-pair a b)) . -> . (-opt (-pair a b))))]
@ -232,9 +229,6 @@
[assf (-poly (a b) ((a . -> . Univ) (-lst (-pair a b))
. -> . (-opt (-pair a b))))]
[list-ref (-poly (a) ((-lst a) -Nat . -> . a))]
[list-tail (-poly (a) ((-lst a) -Nat . -> . (-lst a)))]
[apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
[kernel:apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
[time-apply (-polydots (b a)
@ -275,55 +269,11 @@
[regexp-quote (cl->*
(-String [-Boolean] . ->opt . -String)
(-Bytes [-Boolean] . ->opt . -Bytes))]
[regexp-match
(let ([?outp (-opt -Output-Port)]
[N -Nat]
[?N (-opt -Nat)]
[optlist (lambda (t) (-opt (-lst (-opt t))))]
[-StrRx (Un -String -Regexp -PRegexp)]
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -Bytes)])
(cl->*
(-StrRx -String [N ?N ?outp] . ->opt . (optlist -String))
(-BtsRx -String [N ?N ?outp] . ->opt . (optlist -Bytes))
(-Pattern -InpBts [N ?N ?outp] . ->opt . (optlist -Bytes))))]
[regexp-match*
(let ([N -Nat]
[?N (-opt -Nat)]
[-StrRx (Un -String -Regexp -PRegexp)]
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -Bytes)])
(cl->*
(-StrRx -String [N ?N] . ->opt . (-lst -String))
(-BtsRx -String [N ?N] . ->opt . (-lst -Bytes))
(-Pattern -InpBts [N ?N] . ->opt . (-lst -Bytes))))]
[regexp-try-match
(let ([?outp (-opt -Output-Port)]
[?N (-opt -Nat)]
[optlist (lambda (t) (-opt (-lst (-opt t))))])
(->opt -Pattern -Input-Port [-Nat ?N ?outp] (optlist -Bytes)))]
[regexp-match-exact?
(-Pattern (Un -String -Bytes -Input-Port) . -> . B)]
[regexp-match-positions
(let ([?outp (-opt -Output-Port)]
[N -Nat]
[?N (-opt -Nat)]
[optlist (lambda (t) (-opt (-lst (-opt t))))]
[-StrRx (Un -String -Regexp -PRegexp)]
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -Bytes)])
(->opt -Pattern (Un -String -InpBts) [N ?N ?outp] (optlist (-pair -Nat -Nat))))]
[regexp-match-positions*
(let ([?outp (-opt -Output-Port)]
[?N (-opt -Nat)]
[optlist (lambda (t) (-opt (-lst (-opt t))))]
[-StrRx (Un -String -Regexp -PRegexp)]
[-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)]
[-InpBts (Un -Input-Port -Bytes)])
(->opt -Pattern (Un -String -InpBts) [-Nat ?N ?outp] (-lst (-pair -Nat -Nat))))]
#;
[regexp-match-peek-positions*]
#;
@ -344,11 +294,6 @@
;; errors
[raise-type-error
(cl->
[(Sym -String Univ) (Un)]
[(Sym -String -Nat (-lst Univ)) (Un)])]
;; this is a hack
[match:error ((list) Univ . ->* . (Un))]
@ -359,12 +304,7 @@
[bitwise-not (null -Integer . ->* . -Integer)]
[bitwise-xor (null -Integer . ->* . -Integer)]
[make-string (cl-> [(-Nat) -String] [(-Nat -Char) -String])]
[abs (-Real . -> . -Real)]
[substring (->opt -String [-Nat] -String)]
[string-length (-String . -> . -Nat)]
[unsafe-string-length (-String . -> . -Nat)]
[string-set! (-String -Nat -Char . -> . -Void)]
[file-exists? (-Pathlike . -> . B)]
[string->symbol (-String . -> . Sym)]
@ -374,21 +314,14 @@
;; vectors
[vector? (make-pred-ty (-vec Univ))]
[vector-ref (-poly (a) ((-vec a) -Nat . -> . a))]
[build-vector (-poly (a) (-Nat (-Nat . -> . a) . -> . (-vec a)))]
[vector-set! (-poly (a) (-> (-vec a) -Nat a -Void))]
[vector->list (-poly (a) (-> (-vec a) (-lst a)))]
[list->vector (-poly (a) (-> (-lst a) (-vec a)))]
[vector-length (-poly (a) ((-vec a) . -> . -Nat))]
[make-vector (-poly (a) (cl-> [(-Nat) (-vec -Integer)]
[(-Nat a) (-vec a)]))]
[vector (-poly (a) (->* (list) a (-vec a)))]
[vector-immutable (-poly (a) (->* (list) a (-vec a)))]
[vector->vector-immutable (-poly (a) (-> (-vec a) (-vec a)))]
[vector-fill! (-poly (a) (-> (-vec a) a -Void))]
[vector-copy! (-poly (a) ((-vec a) -Nat (-vec a) [-Nat -Nat] . ->opt . -Void))]
;; [vector->values no good type here]
@ -457,10 +390,6 @@
[regexp-replace*
(cl->* (-Pattern -String -String . -> . -String)
(-Pattern (Un -Bytes -String) (Un -Bytes -String) . -> . -Bytes))]
[peek-char
(cl->* [->opt [-Input-Port -Nat] (Un -Char (-val eof))])]
[peek-byte
(cl->* [->opt [-Input-Port -Nat] (Un -Byte (-val eof))])]
[read-char
(cl->* [->opt [-Input-Port] (Un -Char (-val eof))])]
[read-byte
@ -575,14 +504,6 @@
((list a) (b b) . ->... . (-opt c))
(-lst a))
((-lst b) b) . ->... . (-lst c)))]
[take (-poly (a) ((-lst a) -Nat . -> . (-lst a)))]
[drop (-poly (a) ((-lst a) -Nat . -> . (-lst a)))]
[take-right (-poly (a) ((-lst a) -Nat . -> . (-lst a)))]
[drop-right (-poly (a) ((-lst a) -Nat . -> . (-lst a)))]
[split-at
(-poly (a) ((list (-lst a)) -Nat . ->* . (-values (list (-lst a) (-lst a)))))]
[split-at-right
(-poly (a) ((list (-lst a)) -Nat . ->* . (-values (list (-lst a) (-lst a)))))]
[last (-poly (a) ((-lst a) . -> . a))]
[add-between (-poly (a b) ((-lst a) b . -> . (-lst (Un a b))))]
@ -623,8 +544,6 @@
[generate-temporaries ((Un (-Syntax Univ) (-lst Univ)) . -> . (-lst (-Syntax Sym)))]
[check-duplicate-identifier ((-lst (-Syntax Sym)) . -> . (-opt (-Syntax Sym)))]
;; string.ss
[real->decimal-string (N [-Nat] . ->opt . -String)]
[current-continuation-marks (-> -Cont-Mark-Set)]

View File

@ -3,7 +3,6 @@
[Number -Real]
[Complex -Number]
[Integer -Integer]
[Real -Real]
[Exact-Rational -ExactRational]
[Flonum -Flonum]
[Exact-Positive-Integer -ExactPositiveInteger]

View File

@ -11,7 +11,7 @@
(types convenience union)
(only-in (types convenience) [make-arr* make-arr])))
(define-syntax (#%module-begin stx)
(define-syntax (-#%module-begin stx)
(define-syntax-class clause
#:description "[id type]"
(pattern [id:identifier ty]))
@ -29,9 +29,9 @@
[(mb . rest)
#'(mb (begin) . rest)]))
(provide #%module-begin
(provide (rename-out [-#%module-begin #%module-begin])
require
(all-from-out scheme/base)
(except-out (all-from-out scheme/base) #%module-begin)
types rep private utils
(for-syntax
(types-out convenience union)

View File

@ -70,9 +70,9 @@
[#:fold-rhs (*LNotTypeFilter (type-rec-id t) (map pathelem-rec-id p) idx)])
;; implication
(df LImpFilter ([a (non-empty-listof LatentFilter/c)] [c (non-empty-listof LatentFilter/c)])
[#:frees (combine-frees (map free-vars* (append a c)))
(combine-frees (map free-idxs* (append a c)))])
(dlf LImpFilter ([a (non-empty-listof LatentFilter/c)] [c (non-empty-listof LatentFilter/c)])
[#:frees (combine-frees (map free-vars* (append a c)))
(combine-frees (map free-idxs* (append a c)))])
(dlf LFilterSet (thn els)

View File

@ -66,7 +66,7 @@
(apply append (for/list ([f f-]) (abo ids keys f))))]))
(d/c (abo xs idxs f)
(-> (listof identifier?) (listof index/c) Filter/c (or/c '() (list/c LatentFilter/c)))
((listof identifier?) (listof index/c) Filter/c . -> . (or/c null? (list/c LatentFilter/c)))
(define (lookup y)
(for/first ([x xs] [i idxs] #:when (free-identifier=? x y)) i))
(define-match-expander lookup:
@ -76,10 +76,12 @@
[(Bot:) (list (make-LBot))]
[(TypeFilter: t p (lookup: idx)) (list (make-LTypeFilter t p idx))]
[(NotTypeFilter: t p (lookup: idx)) (list (make-LNotTypeFilter t p idx))]
[(ImpFilter: a c)
(match* [(abo a) (abo c)]
[((list a*) (list c*)) (list (make-LImpFilter a* c*))]
[(_ _) null])]
[(ImpFilter: as cs)
(let ([a* (apply append (for/list ([f as]) (abo xs idxs f)))]
[c* (apply append (for/list ([f cs]) (abo xs idxs f)))])
(if (< (length a*) (length as)) ;; if we removed some things, we can't be sure
null
(list (make-LImpFilter a* c*))))]
[_ null]))
(define (merge-filter-sets fs)

View File

@ -46,7 +46,8 @@
[(LNotTypeFilter: type path idx) (fp "(! ~a @ ~a ~a)" type path idx)]
[(LTypeFilter: type path idx) (fp "(~a @ ~a ~a)" type path idx)]
[(LBot:) (fp "LBot")]
[(LImpFilter: a c) (fp "(LImpFilter ~a ~a)" a c)]))
[(LImpFilter: a c) (fp "(LImpFilter ~a ~a)" a c)]
[else (fp "(Unknown Latent Filter: ~a)" (struct->vector c))]))
(define (print-filter c port write?)
(define (fp . args) (apply fprintf port args))
@ -59,14 +60,16 @@
[(NotTypeFilter: type path id) (fp "(! ~a @ ~a ~a)" type path (syntax-e id))]
[(TypeFilter: type path id) (fp "(~a @ ~a ~a)" type path (syntax-e id))]
[(Bot:) (fp "Bot")]
[(ImpFilter: a c) (fp "(ImpFilter ~a ~a)" a c)]))
[(ImpFilter: a c) (fp "(ImpFilter ~a ~a)" a c)]
[else (fp "(Unknown Filter: ~a)" (struct->vector c))]))
(define (print-pathelem c port write?)
(define (fp . args) (apply fprintf port args))
(match c
[(CarPE:) (fp "car")]
[(CdrPE:) (fp "cdr")]
[(StructPE: t i) (fp "(~a ~a)" t i)]))
[(StructPE: t i) (fp "(~a ~a)" t i)]
[else (fp "(Unknown Path Element: ~a)" (struct->vector c))]))
(define (print-latentobject c port write?)
(define (fp . args) (apply fprintf port args))
@ -79,7 +82,8 @@
(match c
[(NoObject:) (fp "-")]
[(Empty:) (fp "")]
[(Path: pes i) (fp "~a" (append pes (list (syntax-e i))))]))
[(Path: pes i) (fp "~a" (append pes (list (syntax-e i))))]
[else (fp "(Unknown Object: ~a)" (struct->vector c))]))
;; print out a type
;; print-type : Type Port Boolean -> Void
@ -121,7 +125,8 @@
(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
[(Pair: a (? tuple?)) #t]

View File

@ -10,7 +10,10 @@
#%top-interaction
lambda
#%app))
(require typed-scheme/private/base-env typed-scheme/private/base-special-env
(for-syntax typed-scheme/private/base-types-extra))
(require typed-scheme/private/base-env
typed-scheme/private/base-special-env
typed-scheme/private/base-env-numeric
typed-scheme/private/base-env-indexing
(for-syntax typed-scheme/private/base-types-extra))
(provide (rename-out [with-handlers: with-handlers])
(for-syntax (all-from-out typed-scheme/private/base-types-extra)))