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

add first steps in real solving

Browse Source 
original commit: b0918cd8b90972bd0b134e2e67f20020444be65e
This commit is contained in:
Sam Tobin-Hochstadt 2010-04-22 16:25:14 -04:00
commit 8ab2ccb53f
8 changed files with 97 additions and 64 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
collects/typed-scheme/module-info.ss → collects/typed-scheme/language-info.ss
View File

@ -1,10 +1,10 @@
#lang scheme/base
(require typed-scheme/typed-reader)
(provide module-info configure)
(provide get-info configure)
(define ((module-info arg) key default)
(define ((get-info arg) key default)
(case key
[(configure-runtime) `(#(typed-scheme/module-info configure ()))]
[(configure-runtime) `(#(typed-scheme/language-info configure ()))]
[else default]))
;; options currently always empty

6
collects/typed-scheme/typecheck/tc-app.ss
View File

@ -467,9 +467,9 @@
kw-list
(#%plain-app list . kw-arg-list)
. pos-args)
#:declare cpce (id-from 'checked-procedure-check-and-extract 'scheme/private/kw)
#:declare s-kp (id-from 'struct:keyword-procedure 'scheme/private/kw)
#:declare kpe (id-from 'keyword-procedure-extract 'scheme/private/kw)
#:declare cpce (id-from 'checked-procedure-check-and-extract 'racket/private/kw)
#: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
(Function: (list (and ar (arr: dom rng (and rest #f) (and drest #f) kw-formals))))))

2
collects/typed-scheme/typecheck/tc-envops.ss
View File

@ -65,7 +65,7 @@
;; sets the flag box to #f if anything becomes (U)
(d/c (env+ env fs flag)
(env? (listof Filter/c) (box/c #t). -> . env?)
(define-values (imps atoms) (debug combine-props fs (env-props env)))
(define-values (imps atoms) (debug combine-props fs (env-props env) flag))
(for/fold ([Γ (replace-props env imps)]) ([f atoms])
(match f
[(Bot:) (set-box! flag #f) (env-map (lambda (x) (cons (car x) (Un))) Γ)]

21
collects/typed-scheme/typecheck/tc-metafunctions.ss
View File

@ -90,7 +90,21 @@
(provide combine-props tc-results->values)
(define (combine-props new-props old-props)
(define (resolve atoms prop)
(for/fold ([prop prop])
([a (in-list atoms)])
(match prop
[(AndFilter: ps)
(let loop ([ps ps] [result null])
(if (null? ps)
(-and result)
(let ([p (car ps)])
(cond [(opposite? a p) -bot]
[(implied-atomic? p a) (loop (cdr ps) result)]
[else (loop (cdr ps) (cons p result))]))))]
[_ prop])))
(define (combine-props new-props old-props flag)
(define (atomic-prop? p) (or (TypeFilter? p) (NotTypeFilter? p)))
(define-values (new-atoms new-formulas) (partition atomic-prop? new-props))
(let loop ([derived-props null]
@ -98,9 +112,12 @@
[worklist (append old-props new-formulas)])
(if (null? worklist)
(values derived-props derived-atoms)
(let ([p (car worklist)])
(let* ([p (car worklist)]
[p (resolve derived-atoms p)])
(match p
[(AndFilter: ps) (loop derived-props derived-atoms (append ps (cdr worklist)))]
[(TypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))]
[(NotTypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))]
[(Top:) (loop derived-props derived-atoms (cdr worklist))]
[(Bot:) (set-box! flag #f) (values derived-props derived-atoms)]
[_ (loop (cons p derived-props) derived-atoms (cdr worklist))])))))

49
collects/typed-scheme/types/abbrev.ss
View File

@ -279,55 +279,6 @@
[(Path: p i) (-not-filter t i p)]
[_ -top]))
(define (opposite? f1 f2)
(match* (f1 f2)
[((TypeFilter: t1 p1 i1)
(NotTypeFilter: t2 p1 i2))
(and (type-equal? t1 t2)
(free-identifier=? i1 i2))]
[((NotTypeFilter: t2 p1 i2)
(TypeFilter: t1 p1 i1))
(and (type-equal? t1 t2)
(free-identifier=? i1 i2))]
[(_ _) #f]))
(define (-or . args)
(let loop ([fs args] [result null])
(if (null? fs)
(match result
[(list) -bot]
[(list f) f]
[(list f1 f2)
(if (opposite? f1 f2)
-top
(if (filter-equal? f1 f2)
f1
(make-OrFilter (list f1 f2))))]
[_ (make-OrFilter result)])
(match (car fs)
[(and t (Top:)) t]
[(OrFilter: fs*) (loop (cdr fs) (append fs* result))]
[(Bot:) (loop (cdr fs) result)]
[t (loop (cdr fs) (cons t result))]))))
(define (-and . args)
(let loop ([fs args] [result null])
(if (null? fs)
(match result
[(list) -top]
[(list f) f]
;; don't think this is useful here
[(list f1 f2) (if (opposite? f1 f2)
-bot
(if (filter-equal? f1 f2)
f1
(make-AndFilter (list f1 f2))))]
[_ (make-AndFilter result)])
(match (car fs)
[(and t (Bot:)) t]
[(AndFilter: fs*) (loop (cdr fs) (append fs* result))]
[(Top:) (loop (cdr fs) result)]
[t (loop (cdr fs) (cons t result))]))))
(d/c (-not-filter t i [p null])
(c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)

65
collects/typed-scheme/types/convenience.ss
View File

@ -68,3 +68,68 @@
(define Syntax-Sexp (-Sexpof Any-Syntax))
(define Ident (-Syntax -Symbol))
(define (opposite? f1 f2)
(match* (f1 f2)
[((TypeFilter: t1 p1 i1)
(NotTypeFilter: t2 p1 i2))
(and (free-identifier=? i1 i2)
(subtype t1 t2))]
[((NotTypeFilter: t2 p1 i2)
(TypeFilter: t1 p1 i1))
(and (free-identifier=? i1 i2)
(subtype t1 t2))]
[(_ _) #f]))
;; is f1 implied by f2?
(define (implied-atomic? f1 f2)
(if (filter-equal? f1 f2)
#t
(match* (f1 f2)
[((TypeFilter: t1 p1 i1)
(TypeFilter: t2 p1 i2))
(and (free-identifier=? i1 i2)
(subtype t1 t2))]
[((NotTypeFilter: t2 p1 i2)
(NotTypeFilter: t1 p1 i1))
(and (free-identifier=? i1 i2)
(subtype t1 t2))]
[(_ _) #f])))
(define (-or . args)
(let loop ([fs args] [result null])
(if (null? fs)
(match result
[(list) -bot]
[(list f) f]
[(list f1 f2)
(if (opposite? f1 f2)
-top
(if (filter-equal? f1 f2)
f1
(make-OrFilter (list f1 f2))))]
[_ (make-OrFilter result)])
(match (car fs)
[(and t (Top:)) t]
[(OrFilter: fs*) (loop (cdr fs) (append fs* result))]
[(Bot:) (loop (cdr fs) result)]
[t (loop (cdr fs) (cons t result))]))))
(define (-and . args)
(let loop ([fs args] [result null])
(if (null? fs)
(match result
[(list) -top]
[(list f) f]
;; don't think this is useful here
[(list f1 f2) (if (opposite? f1 f2)
-bot
(if (filter-equal? f1 f2)
f1
(make-AndFilter (list f1 f2))))]
[_ (make-AndFilter result)])
(match (car fs)
[(and t (Bot:)) t]
[(AndFilter: fs*) (loop (cdr fs) (append fs* result))]
[(Top:) (loop (cdr fs) result)]
[t (loop (cdr fs) (cons t result))]))))

6
collects/typed/scheme/base/lang/reader.ss
View File

@ -5,14 +5,14 @@ typed/scheme/base
#:read r:read
#:read-syntax r:read-syntax
#:info make-info
#:module-info make-module-info
#:language-info make-language-info
(define (make-info key default use-default)
(case key
[else (use-default key default)]))
(define make-module-info
`#(typed-scheme/module-info module-info ()))
(define make-language-info
`#(typed-scheme/language-info get-info ()))
(require (prefix-in r: typed-scheme/typed-reader))

6
collects/typed/scheme/lang/reader.ss
View File

@ -5,14 +5,14 @@ typed/scheme
#:read r:read
#:read-syntax r:read-syntax
#:info make-info
#:module-info make-module-info
#:language-info make-language-info
(define (make-info key default use-default)
(case key
[else (use-default key default)]))
(define make-module-info
`#(typed-scheme/module-info module-info ()))
(define make-language-info
`#(typed-scheme/language-info get-info ()))
(require (prefix-in r: typed-scheme/typed-reader))