New type parser, written using syntax/parse.
- uses keywords with bindings - : macro in separate file so it can be used earlier - internal function in separate file FilterSet/c and LatentFilterSet/c contracts Avoid returning #f when `look-for-in-orig' fails Add type for unsafe-cdr svn: r15923 original commit: 63d318fd4b7e7244af10fff21db74f0d09db5006
This commit is contained in:
Sam Tobin-Hochstadt
parent
dc68f722ee
commit
cf872c4e38
1
collects/tests/typed-scheme/succeed/null-program.ss
Normal file
1
collects/tests/typed-scheme/succeed/null-program.ss
Normal file
|
|
@ -0,0 +1 @@
|
|||
#lang typed-scheme
|
||||
|
|
@ -2,6 +2,7 @@
|
|||
(provide -foldl)
|
||||
|
||||
(pdefine: (a b) (-foldl [f : (a b -> b)] [e : b] [l : (Listof a)]) : b
|
||||
(if (null? l) e
|
||||
(if (null? l)
|
||||
e
|
||||
(foldl f (f (car l) e) (cdr l))))
|
||||
|
||||
|
|
|
|||
|
|
@ -5,9 +5,9 @@
|
|||
(rep type-rep)
|
||||
(rename-in (types comparison subtype union utils convenience)
|
||||
[Un t:Un] [-> t:->])
|
||||
(private base-types base-types-extra)
|
||||
(for-template (private base-types base-types-extra))
|
||||
(private parse-type)
|
||||
(private base-types base-types-extra colon)
|
||||
(for-template (private base-types base-types-extra base-env colon))
|
||||
(private parse-type2)
|
||||
(schemeunit))
|
||||
|
||||
(provide parse-type-tests)
|
||||
|
|
@ -20,9 +20,10 @@
|
|||
;; the table is phase 0, so they don't compare correctly
|
||||
|
||||
;; The solution is to add the identifiers to the table at phase 0.
|
||||
;; We do this by going through the table, constructing new identifiers based on the symbol of the old identifier.
|
||||
;; This relies on the identifiers being bound at phase 0 in this module (which they are, because we have a
|
||||
;; phase 0 require of "base-env.ss").
|
||||
;; We do this by going through the table, constructing new identifiers based on the symbol
|
||||
;; of the old identifier.
|
||||
;; This relies on the identifiers being bound at phase 0 in this module (which they are,
|
||||
;; because we have a phase 0 require of "base-env.ss").
|
||||
(for ([pr (type-alias-env-map cons)])
|
||||
(let ([nm (car pr)]
|
||||
[ty (cdr pr)])
|
||||
|
|
@ -64,6 +65,7 @@
|
|||
"parse-type tests"
|
||||
[Number N]
|
||||
[Any Univ]
|
||||
[(List Number String) (-Tuple (list N -String))]
|
||||
[(All (Number) Number) (-poly (a) a)]
|
||||
[(Number . Number) (-pair N N)]
|
||||
[(Listof Boolean) (make-Listof B)]
|
||||
|
|
@ -72,6 +74,8 @@
|
|||
[(-> (values Number Boolean Number)) (t:-> (-values (list N B N)))]
|
||||
[(Number -> Number) (t:-> N N)]
|
||||
[(Number -> Number) (t:-> N N)]
|
||||
;; requires transformer time stuff that doesn't work
|
||||
#;[(Refinement even?) (make-Refinement #'even?)]
|
||||
[(Number Number Number Boolean -> Number) (N N N B . t:-> . N)]
|
||||
[(Number Number Number * -> Boolean) ((list N N) N . ->* . B)]
|
||||
;[((. Number) -> Number) (->* (list) N N)] ;; not legal syntax
|
||||
|
|
|
|||
|
|
@ -3,10 +3,12 @@
|
|||
(require "test-utils.ss" "planet-requires.ss"
|
||||
(for-syntax scheme/base)
|
||||
(for-template scheme/base))
|
||||
(require (private base-env prims type-annotation)
|
||||
(require (private base-env prims type-annotation base-types-extra)
|
||||
(typecheck typechecker)
|
||||
(rep type-rep filter-rep object-rep)
|
||||
(types utils union convenience)
|
||||
(rename-in (types utils union convenience)
|
||||
[Un t:Un]
|
||||
[-> t:->])
|
||||
(utils tc-utils mutated-vars)
|
||||
(env type-name-env type-environments init-envs)
|
||||
(schemeunit)
|
||||
|
|
@ -16,7 +18,7 @@
|
|||
(typecheck typechecker)
|
||||
(env type-env)
|
||||
(private base-env))
|
||||
(for-template (private base-env base-types)))
|
||||
(for-template (private base-env base-types base-types-extra)))
|
||||
|
||||
|
||||
(require (for-syntax syntax/kerncase stxclass))
|
||||
|
|
@ -128,10 +130,10 @@
|
|||
(tc-e/t 3 -Integer)
|
||||
(tc-e/t "foo" -String)
|
||||
(tc-e (+ 3 4) -Integer)
|
||||
[tc-e/t (lambda: () 3) (-> -Integer : (-LFS (list) (list (make-LBot))))]
|
||||
[tc-e/t (lambda: ([x : Number]) 3) (-> N -Integer : (-LFS (list) (list (make-LBot))))]
|
||||
[tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (-> N B -Integer : (-LFS (list) (list (make-LBot))))]
|
||||
[tc-e/t (lambda () 3) (-> -Integer : (-LFS (list) (list (make-LBot))))]
|
||||
[tc-e/t (lambda: () 3) (t:-> -Integer : (-LFS (list) (list (make-LBot))))]
|
||||
[tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Integer : (-LFS (list) (list (make-LBot))))]
|
||||
[tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Integer : (-LFS (list) (list (make-LBot))))]
|
||||
[tc-e/t (lambda () 3) (t:-> -Integer : (-LFS (list) (list (make-LBot))))]
|
||||
[tc-e (values 3 4) #:ret (ret (list -Integer -Integer) (list (-FS (list) (list (make-Bot))) (-FS (list) (list (make-Bot)))))]
|
||||
[tc-e (cons 3 4) (-pair -Integer -Integer)]
|
||||
[tc-e (cons 3 #{'() : (Listof -Integer)}) (make-Listof -Integer)]
|
||||
|
|
@ -141,13 +143,13 @@
|
|||
[tc-e/t #(3 4 5) (make-Vector -Integer)]
|
||||
[tc-e/t '(2 3 4) (-lst* -Integer -Integer -Integer)]
|
||||
[tc-e/t '(2 3 #t) (-lst* -Integer -Integer (-val #t))]
|
||||
[tc-e/t #(2 3 #t) (make-Vector (Un -Integer (-val #t)))]
|
||||
[tc-e/t #(2 3 #t) (make-Vector (t:Un -Integer (-val #t)))]
|
||||
[tc-e/t '(#t #f) (-lst* (-val #t) (-val #f))]
|
||||
[tc-e/t (plambda: (a) ([l : (Listof a)]) (car l))
|
||||
(make-Poly '(a) (-> (make-Listof (-v a)) (-v a)))]
|
||||
(make-Poly '(a) (t:-> (make-Listof (-v a)) (-v a)))]
|
||||
[tc-e/t (plambda: (a) ([l : (Listof a)]) (car l))
|
||||
(make-Poly '(a) (-> (make-Listof (-v a)) (-v a)))]
|
||||
[tc-e/t (case-lambda: [([a : Number] [b : Number]) (+ a b)]) (-> N N N)]
|
||||
(make-Poly '(a) (t:-> (make-Listof (-v a)) (-v a)))]
|
||||
[tc-e/t (case-lambda: [([a : Number] [b : Number]) (+ a b)]) (t:-> N N N)]
|
||||
[tc-e (let: ([x : Number 5]) x) #:proc (get-let-name x 0 (-path -Number #'x))]
|
||||
[tc-e (let-values ([(x) 4]) (+ x 1)) -Integer]
|
||||
[tc-e (let-values ([(#{x : Number} #{y : Boolean}) (values 3 #t)]) (and (= x 1) (not y)))
|
||||
|
|
@ -194,7 +196,7 @@
|
|||
[tc-e/t '#t (-val #t)]
|
||||
[tc-e '#f #:ret (ret (-val #f) (-FS (list (make-Bot)) null))]
|
||||
[tc-e/t (if #f 'a 3) -Integer]
|
||||
[tc-e/t (if #f #f #t) (Un (-val #t))]
|
||||
[tc-e/t (if #f #f #t) (t:Un (-val #t))]
|
||||
[tc-e (when #f 3) -Void]
|
||||
[tc-e/t '() (-val '())]
|
||||
[tc-e/t (let: ([x : (Listof Number) '(1)])
|
||||
|
|
@ -236,7 +238,7 @@
|
|||
[tc-e (let ([x 1]) (boolean? x)) #:ret (ret -Boolean (-FS (list (make-Bot)) null))]
|
||||
[tc-e (boolean? number?) #:ret (ret -Boolean (-FS (list (make-Bot)) null))]
|
||||
|
||||
[tc-e (let: ([x : (Option Number) #f]) x) #:proc (get-let-name x 0 (-path (Un N (-val #f)) #'x))]
|
||||
[tc-e (let: ([x : (Option Number) #f]) x) #:proc (get-let-name x 0 (-path (t:Un N (-val #f)) #'x))]
|
||||
[tc-e (let: ([x : Any 12]) (not (not x)))
|
||||
#:proc (get-let-name x 0 (ret -Boolean (-FS (list (make-NotTypeFilter (-val #f) null #'x)) (list (make-TypeFilter (-val #f) null #'x)))))]
|
||||
|
||||
|
|
@ -303,7 +305,7 @@
|
|||
[tc-e (let* ([sym 'squarf]
|
||||
[x (if (= 1 2) 3 sym)])
|
||||
x)
|
||||
#:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) (-path (Un (-val 'squarf) -Integer) #'x)])]
|
||||
#:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) (-path (t:Un (-val 'squarf) -Integer) #'x)])]
|
||||
|
||||
[tc-e/t (if #t 1 2) -Integer]
|
||||
|
||||
|
|
@ -324,7 +326,7 @@
|
|||
(if (eq? x 5)
|
||||
"foo"
|
||||
x))
|
||||
(Un -String (-val 5))]
|
||||
(t:Un -String (-val 5))]
|
||||
|
||||
[tc-e (let* ([sym 'squarf]
|
||||
[x (if (= 1 2) 3 sym)])
|
||||
|
|
@ -380,7 +382,7 @@
|
|||
(if (and (list? x) (not (null? x)))
|
||||
x
|
||||
'foo))
|
||||
(Un (-val 'foo) (-pair Univ (-lst Univ)))]
|
||||
(t:Un (-val 'foo) (-pair Univ (-lst Univ)))]
|
||||
|
||||
[tc-e (cadr (cadr (list 1 (list 1 2 3) 3))) -Integer]
|
||||
|
||||
|
|
@ -390,7 +392,7 @@
|
|||
[tc-e (let: ([x : Any 1]) (and (number? x) (boolean? x)))
|
||||
#:ret (ret B (-FS (list (make-Bot)) null))]
|
||||
[tc-e (let: ([x : Any 1]) (and (number? x) x))
|
||||
#:proc (get-let-name x 0 (ret (Un N (-val #f)) (-FS (list (make-TypeFilter N null #'x) (make-NotTypeFilter (-val #f) null #'x)) null)))]
|
||||
#:proc (get-let-name x 0 (ret (t:Un N (-val #f)) (-FS (list (make-TypeFilter N null #'x) (make-NotTypeFilter (-val #f) null #'x)) null)))]
|
||||
[tc-e (let: ([x : Any 1]) (and x (boolean? x)))
|
||||
#:proc (get-let-name x 0 (ret -Boolean (-FS (list (make-NotTypeFilter (-val #f) null #'x) (make-TypeFilter -Boolean null #'x)) null)))]
|
||||
|
||||
|
|
@ -442,30 +444,30 @@
|
|||
;; T-AbsPred
|
||||
[tc-e/t (let ([p? (lambda: ([x : Any]) (number? x))])
|
||||
(lambda: ([x : Any]) (if (p? x) (add1 x) 12)))
|
||||
(-> Univ N)]
|
||||
(t:-> Univ N)]
|
||||
[tc-e/t (let ([p? (lambda: ([x : Any]) (not (number? x)))])
|
||||
(lambda: ([x : Any]) (if (p? x) 12 (add1 x))))
|
||||
(-> Univ N : (-LFS null (list (make-LTypeFilter -Number null 0))))]
|
||||
(t:-> Univ N : (-LFS null (list (make-LTypeFilter -Number null 0))))]
|
||||
[tc-e/t (let* ([z 1]
|
||||
[p? (lambda: ([x : Any]) (number? z))])
|
||||
(lambda: ([x : Any]) (if (p? x) 11 12)))
|
||||
(-> Univ -Integer : (-LFS null (list (make-LBot))))]
|
||||
(t:-> Univ -Integer : (-LFS null (list (make-LBot))))]
|
||||
[tc-e/t (let* ([z 1]
|
||||
[p? (lambda: ([x : Any]) (number? z))])
|
||||
(lambda: ([x : Any]) (if (p? x) x 12)))
|
||||
(-> Univ Univ : (-LFS (list (-not-filter (-val #f))) (list (-filter (-val #f)))) : (make-LPath null 0))]
|
||||
(t:-> Univ Univ : (-LFS (list (-not-filter (-val #f))) (list (-filter (-val #f)))) : (make-LPath null 0))]
|
||||
[tc-e/t (let* ([z (ann 1 : Any)]
|
||||
[p? (lambda: ([x : Any]) (not (number? z)))])
|
||||
(lambda: ([x : Any]) (if (p? x) x 12)))
|
||||
(-> Univ Univ)]
|
||||
(t:-> Univ Univ)]
|
||||
[tc-e/t (let* ([z 1]
|
||||
[p? (lambda: ([x : Any]) (not (number? z)))])
|
||||
(lambda: ([x : Any]) (if (p? x) x 12)))
|
||||
(-> Univ -Integer : (-LFS null (list (make-LBot))))]
|
||||
(t:-> Univ -Integer : (-LFS null (list (make-LBot))))]
|
||||
[tc-e/t (let* ([z 1]
|
||||
[p? (lambda: ([x : Any]) z)])
|
||||
(lambda: ([x : Any]) (if (p? x) x 12)))
|
||||
(-> Univ Univ)]
|
||||
(t:-> Univ Univ)]
|
||||
|
||||
[tc-e (not 1) #:ret (ret B (-FS (list (make-Bot)) null))]
|
||||
|
||||
|
|
@ -540,8 +542,8 @@
|
|||
(+ a b a* b*))
|
||||
-Integer]
|
||||
|
||||
[tc-e (raise-type-error 'foo "bar" 5) (Un)]
|
||||
[tc-e (raise-type-error 'foo "bar" 7 (list 5)) (Un)]
|
||||
[tc-e (raise-type-error 'foo "bar" 5) (t:Un)]
|
||||
[tc-e (raise-type-error 'foo "bar" 7 (list 5)) (t:Un)]
|
||||
|
||||
#;[tc-e
|
||||
(let ((x '(1 3 5 7 9)))
|
||||
|
|
@ -601,7 +603,7 @@
|
|||
|
||||
[tc-err (apply append (list 1) (list 2) (list 3) (list (list 1) "foo"))]
|
||||
[tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list 1))) (-lst -Integer)]
|
||||
[tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list "foo"))) (-lst (Un -String -Integer))]
|
||||
[tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list "foo"))) (-lst (t:Un -String -Integer))]
|
||||
[tc-err (plambda: (b ...) [y : b ... b] (apply append (map list y)))]
|
||||
[tc-e/t (plambda: (b ...) [y : (Listof Integer) ... b] (apply append y))
|
||||
(-polydots (b) (->... (list) ((-lst -Integer) b) (-lst -Integer)))]
|
||||
|
|
@ -628,15 +630,15 @@
|
|||
|
||||
;; instantiating dotted terms
|
||||
[tc-e/t (inst (plambda: (a ...) [xs : a ... a] 3) Integer Boolean Integer)
|
||||
(-Integer B -Integer . -> . -Integer : (-LFS null (list (make-LBot))))]
|
||||
(-Integer B -Integer . t:-> . -Integer : (-LFS null (list (make-LBot))))]
|
||||
[tc-e/t (inst (plambda: (a ...) [xs : (a ... a -> Integer) ... a] 3) Integer Boolean Integer)
|
||||
((-Integer B -Integer . -> . -Integer)
|
||||
(-Integer B -Integer . -> . -Integer)
|
||||
(-Integer B -Integer . -> . -Integer)
|
||||
. -> . -Integer : (-LFS null (list (make-LBot))))]
|
||||
((-Integer B -Integer . t:-> . -Integer)
|
||||
(-Integer B -Integer . t:-> . -Integer)
|
||||
(-Integer B -Integer . t:-> . -Integer)
|
||||
. t:-> . -Integer : (-LFS null (list (make-LBot))))]
|
||||
|
||||
[tc-e/t (plambda: (z x y ...) () (inst map z x y ... y))
|
||||
(-polydots (z x y) (-> ((list ((list x) (y y) . ->... . z) (-lst x)) ((-lst y) y) . ->... . (-lst z))))]
|
||||
(-polydots (z x y) (t:-> ((list ((list x) (y y) . ->... . z) (-lst x)) ((-lst y) y) . ->... . (-lst z))))]
|
||||
|
||||
;; error tests
|
||||
[tc-err (#%variable-reference number?)]
|
||||
|
|
@ -702,20 +704,20 @@
|
|||
((inst (inst x (All (t) (t -> t)))
|
||||
(All (t) t))
|
||||
x))
|
||||
((-poly (a) a) . -> . (-poly (a) a))]
|
||||
((-poly (a) a) . t:-> . (-poly (a) a))]
|
||||
|
||||
;; We need to make sure that even if a isn't free in the dotted type, that it gets replicated
|
||||
;; appropriately.
|
||||
[tc-e/t (inst (plambda: (a ...) [ys : Number ... a]
|
||||
(apply + ys))
|
||||
Boolean String Number)
|
||||
(N N N . -> . N)]
|
||||
(N N N . t:-> . N)]
|
||||
|
||||
[tc-e (assq 'foo #{'((a b) (foo bar)) :: (Listof (List Symbol Symbol))})
|
||||
(Un (-val #f) (-pair Sym (-pair Sym (-val null))))]
|
||||
(t:Un (-val #f) (-pair Sym (-pair Sym (-val null))))]
|
||||
|
||||
[tc-e/t (ann (lambda (x) x) (All (a) (a -> a)))
|
||||
(-poly (a) (a . -> . a))]
|
||||
(-poly (a) (a . t:-> . a))]
|
||||
[tc-e (apply values (list 1 2 3)) #:ret (ret (list -Integer -Integer -Integer))]
|
||||
|
||||
[tc-e/t (ann (if #t 3 "foo") Integer) -Integer]
|
||||
|
|
|
|||
|
|
@ -10,5 +10,7 @@
|
|||
#%top-interaction
|
||||
lambda
|
||||
#%app))
|
||||
(require "private/base-env.ss" "private/base-special-env.ss")
|
||||
(provide (rename-out [with-handlers: with-handlers]))
|
||||
(require "private/base-env.ss" "private/base-special-env.ss"
|
||||
(for-syntax "private/base-types-extra.ss"))
|
||||
(provide (rename-out [with-handlers: with-handlers])
|
||||
(for-syntax (all-from-out "private/base-types-extra.ss")))
|
||||
|
|
|
|||
|
|
@ -4,6 +4,7 @@
|
|||
scheme/list
|
||||
scheme/tcp
|
||||
scheme
|
||||
scheme/unsafe/ops
|
||||
(only-in rnrs/lists-6 fold-left)
|
||||
'#%paramz
|
||||
(only-in '#%kernel [apply kernel:apply])
|
||||
|
|
@ -730,4 +731,10 @@
|
|||
(Univ -Output-Port . -> . -Void))]
|
||||
[pretty-format
|
||||
(cl->* (Univ . -> . -Void)
|
||||
(Univ -Integer . -> . -Void))]
|
||||
(Univ -Integer . -> . -Void))]
|
||||
|
||||
;; unsafe
|
||||
|
||||
[unsafe-cdr (-poly (a b)
|
||||
(cl->*
|
||||
(->acc (list (-pair a b)) b (list -cdr))))]
|
||||
|
|
@ -5,14 +5,15 @@
|
|||
(define-syntax (define-other-types stx)
|
||||
(syntax-case stx ()
|
||||
[(_ nm ...)
|
||||
#'(begin (define-syntax nm (lambda (stx) (raise-syntax-error 'type-check "type name used out of context" stx))) ...
|
||||
#'(begin (define-syntax nm
|
||||
(lambda (stx)
|
||||
(raise-syntax-error 'type-check "type name used out of context" stx))) ...
|
||||
(provide nm) ...)]))
|
||||
|
||||
;; special types names that are not bound to particular types
|
||||
|
||||
;; special type names that are not bound to particular types
|
||||
(define-other-types
|
||||
-> U mu All Opaque
|
||||
Parameter Tuple Class Values Instance
|
||||
Parameter Tuple Class Values Instance Refinement
|
||||
pred)
|
||||
|
||||
(provide (rename-out [All ∀]
|
||||
|
|
|
|||
49
collects/typed-scheme/private/colon.ss
Normal file
49
collects/typed-scheme/private/colon.ss
Normal file
|
|
@ -0,0 +1,49 @@
|
|||
#lang scheme/base
|
||||
|
||||
(require (for-syntax scheme/base syntax/parse "internal.ss")
|
||||
"../typecheck/internal-forms.ss"
|
||||
(prefix-in t: "base-types-extra.ss")
|
||||
(for-template (prefix-in t: "base-types-extra.ss"))
|
||||
(for-syntax (prefix-in t: "base-types-extra.ss")))
|
||||
|
||||
(provide :)
|
||||
|
||||
(define-syntax (: stx)
|
||||
(define-syntax-class arr
|
||||
(pattern x:id
|
||||
#:fail-unless (eq? (syntax-e #'x '->)) #f
|
||||
#:fail-unless (printf "id: ~a ~a~n"
|
||||
(identifier-binding #'All-kw)
|
||||
(identifier-transformer-binding #'All-kw))
|
||||
#f
|
||||
#:fail-unless (printf "kw: ~a ~a~n"
|
||||
(identifier-binding #'t:All)
|
||||
(identifier-transformer-binding #'t:All))
|
||||
#f
|
||||
#:fail-when #t #f))
|
||||
(define stx*
|
||||
;; make it possible to add another colon after the id for clarity
|
||||
;; and in that case, a `->' on the RHS does not need to be
|
||||
;; explicitly parenthesized
|
||||
(syntax-parse stx #:literals (: t:->)
|
||||
[(: id : x ...)
|
||||
#:fail-unless (= 1 (length
|
||||
(for/list ([i (syntax->list #'(x ...))]
|
||||
#:when (and (identifier? i)
|
||||
(free-identifier=? i #'t:->)))
|
||||
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))
|
||||
(syntax-parse stx*
|
||||
[(_ i:id ty)
|
||||
(syntax-property (internal (syntax/loc stx (:-internal i ty)))
|
||||
'disappeared-use #'i)]
|
||||
[(_ i:id x ...)
|
||||
(case (length (syntax->list #'(x ...)))
|
||||
[(1) (err "can only annotate identifiers with types" #'i)]
|
||||
[(0) (err "missing type")]
|
||||
[else (err "bad syntax (multiple types after identifier)")])]))
|
||||
|
|
@ -1,18 +1,52 @@
|
|||
#lang scheme/base
|
||||
|
||||
(require "parse-type2.ss")
|
||||
(provide (all-from-out "parse-type2.ss"))
|
||||
|
||||
#|
|
||||
|
||||
(require (except-in "../utils/utils.ss" extend))
|
||||
(require (except-in (rep type-rep) make-arr)
|
||||
(rename-in (types convenience union utils) [make-arr* make-arr])
|
||||
(utils tc-utils stxclass-util)
|
||||
(utils tc-utils)
|
||||
syntax/stx (prefix-in c: scheme/contract)
|
||||
stxclass stxclass/util
|
||||
(except-in stxclass) stxclass/util
|
||||
(env type-environments type-name-env type-alias-env lexical-env)
|
||||
(prefix-in t: "base-types-extra.ss")
|
||||
scheme/match
|
||||
(for-syntax scheme/base stxclass stxclass/util)
|
||||
(for-template scheme/base "base-types-extra.ss"))
|
||||
|
||||
(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
|
||||
#:with datum (syntax-e #'s)
|
||||
#:when (pred #'datum)))
|
||||
|
||||
(define-syntax (parse/get stx)
|
||||
(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))
|
||||
"."
|
||||
(symbol->string #'attr.datum))))])
|
||||
(quasisyntax/loc stx
|
||||
(syntax-parse arg
|
||||
[#,i #:declare #,i pat #'#,get-i])))]))
|
||||
|
||||
|
||||
|
||||
(define-pred-stxclass atom atom?)
|
||||
(define-pred-stxclass byte-pregexp byte-pregexp?)
|
||||
(define-pred-stxclass byte-regexp byte-regexp?)
|
||||
(define-pred-stxclass regexp regexp?)
|
||||
(define-pred-stxclass bytes bytes?)
|
||||
|
||||
(p/c [parse-type (syntax? . c:-> . Type/c)]
|
||||
[parse-type/id (syntax? c:any/c . c:-> . Type/c)]
|
||||
[parse-tc-results (syntax? . c:-> . tc-results?)]
|
||||
|
|
@ -584,3 +618,4 @@
|
|||
(define parse-tc-results/id (parse/id parse-tc-results))
|
||||
|
||||
(define parse-type/id (parse/id parse-type))
|
||||
|#
|
||||
|
|
@ -20,6 +20,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
|
|||
|
||||
|
||||
(provide (all-defined-out)
|
||||
:
|
||||
(rename-out [define-typed-struct define-struct:]
|
||||
[define-typed-struct/exec define-struct/exec:]))
|
||||
|
||||
|
|
@ -34,27 +35,22 @@ This file defines two sorts of primitives. All of them are provided into any mod
|
|||
syntax/struct
|
||||
syntax/stx
|
||||
scheme/struct-info
|
||||
(private internal)
|
||||
(except-in (utils utils tc-utils))
|
||||
(env type-name-env)
|
||||
"type-contract.ss"))
|
||||
|
||||
(require (utils require-contract)
|
||||
"colon.ss"
|
||||
(typecheck internal-forms)
|
||||
(except-in mzlib/contract ->)
|
||||
(only-in mzlib/contract [-> c->])
|
||||
mzlib/struct
|
||||
"base-types.ss")
|
||||
"base-types.ss"
|
||||
"base-types-extra.ss")
|
||||
|
||||
(define-for-syntax (ignore stx) (syntax-property stx 'typechecker:ignore #t))
|
||||
|
||||
(define-for-syntax (internal stx)
|
||||
(quasisyntax/loc stx
|
||||
(define-values ()
|
||||
(begin
|
||||
(quote-syntax #,stx)
|
||||
(#%plain-app values)))))
|
||||
|
||||
|
||||
|
||||
(define-syntax (require/typed stx)
|
||||
(define-syntax-class opt-rename
|
||||
|
|
@ -169,9 +165,9 @@ This file defines two sorts of primitives. All of them are provided into any mod
|
|||
[(pdefine: tvars (nm . formals) : ret-ty . body)
|
||||
(with-syntax* ([(tys ...) (types-of-formals #'formals stx)]
|
||||
[type (syntax/loc #'ret-ty (All tvars (tys ... -> ret-ty)))])
|
||||
(syntax/loc stx
|
||||
(define: nm : type
|
||||
(plambda: tvars formals . body))))]))
|
||||
(syntax/loc stx
|
||||
(define: nm : type
|
||||
(plambda: tvars formals . body))))]))
|
||||
|
||||
(define-syntax (ann stx)
|
||||
(syntax-case stx (:)
|
||||
|
|
@ -180,30 +176,6 @@ This file defines two sorts of primitives. All of them are provided into any mod
|
|||
[(_ arg ty)
|
||||
(syntax-property #'arg 'type-ascription #'ty)]))
|
||||
|
||||
(define-syntax (: stx)
|
||||
(define stx*
|
||||
;; make it possible to add another colon after the id for clarity
|
||||
;; and in that case, a `->' on the RHS does not need to be
|
||||
;; explicitly parenthesized
|
||||
(syntax-case stx (:)
|
||||
[(: id : x ...)
|
||||
(ormap (lambda (x) (eq? '-> (syntax-e x))) (syntax->list #'(x ...)))
|
||||
(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))
|
||||
(syntax-case stx* ()
|
||||
[(_ id ty)
|
||||
(identifier? #'id)
|
||||
(syntax-property (internal (syntax/loc stx (:-internal id ty)))
|
||||
'disappeared-use #'id)]
|
||||
[(_ id x ...)
|
||||
(case (length (syntax->list #'(x ...)))
|
||||
[(1) (err "can only annotate identifiers with types" #'id)]
|
||||
[(0) (err "missing type")]
|
||||
[else (err "bad syntax (multiple types after identifier)")])]))
|
||||
|
||||
(define-syntax (inst stx)
|
||||
(syntax-case stx (:)
|
||||
[(_ arg : . tys)
|
||||
|
|
|
|||
|
|
@ -42,7 +42,7 @@
|
|||
(parse-type prop)
|
||||
(parse-type/id stx prop)))
|
||||
;(unless let-binding (error 'ohno))
|
||||
;(printf "let-binding: ~a~n" let-binding)
|
||||
;(printf "in type-annotation:~a~n" (syntax->datum stx))
|
||||
(cond
|
||||
[(syntax-property stx type-label-symbol) => pt]
|
||||
[(syntax-property stx type-ascrip-symbol) => pt]
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@
|
|||
(λ (e)
|
||||
(and (LatentFilter? e) (not (LFilterSet? e))))))
|
||||
|
||||
(provide Filter/c LatentFilter/c index/c)
|
||||
(provide Filter/c LatentFilter/c FilterSet/c LatentFilterSet/c index/c)
|
||||
|
||||
(df Bot () [#:fold-rhs #:base])
|
||||
|
||||
|
|
@ -86,3 +86,13 @@
|
|||
[else (listof LatentFilter/c)])])
|
||||
()
|
||||
[result LFilterSet?])])
|
||||
|
||||
(define FilterSet/c
|
||||
(flat-named-contract
|
||||
'FilterSet
|
||||
(λ (e) (or (FilterSet? e) (NoFilter? e)))))
|
||||
|
||||
(define LatentFilterSet/c
|
||||
(flat-named-contract
|
||||
'LatentFilterSet
|
||||
(λ (e) (or (LFilterSet? e)))))
|
||||
|
|
@ -20,6 +20,18 @@
|
|||
(import tc-if^ tc-lambda^ tc-app^ tc-let^ check-subforms^)
|
||||
(export tc-expr^)
|
||||
|
||||
(define-syntax-class (3d pred)
|
||||
(pattern s
|
||||
#:with datum (syntax-e #'s)
|
||||
#:when (pred #'datum)))
|
||||
|
||||
|
||||
(define-pred-stxclass atom atom?)
|
||||
(define-pred-stxclass byte-pregexp byte-pregexp?)
|
||||
(define-pred-stxclass byte-regexp byte-regexp?)
|
||||
(define-pred-stxclass regexp regexp?)
|
||||
(define-pred-stxclass bytes bytes?)
|
||||
|
||||
|
||||
;; return the type of a literal value
|
||||
;; scheme-value -> type
|
||||
|
|
|
|||
|
|
@ -227,7 +227,8 @@
|
|||
[(tc-result1: (and t (Poly-names: ns expected*)))
|
||||
(let* ([tvars (let ([p (syntax-property form 'typechecker:plambda)])
|
||||
(when (and (pair? p) (eq? '... (car (last p))))
|
||||
(tc-error "Expected a polymorphic function without ..., but given function had ..."))
|
||||
(tc-error
|
||||
"Expected a polymorphic function without ..., but given function had ..."))
|
||||
(or (and p (map syntax-e (syntax->list p)))
|
||||
ns))]
|
||||
[literal-tvars tvars]
|
||||
|
|
@ -271,10 +272,11 @@
|
|||
(tc/mono-lambda/type formals bodies #f))])
|
||||
;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty)
|
||||
(make-Poly literal-tvars ty))])]
|
||||
[_
|
||||
(unless (check-below (tc/plambda form formals bodies #f) expected)
|
||||
(tc-error/expr #:return expected "Expected a value of type ~a, but got a polymorphic function." expected))
|
||||
expected]))
|
||||
[(tc-result1: t)
|
||||
(unless (check-below (tc/plambda form formals bodies #f) t)
|
||||
(tc-error/expr #:return expected
|
||||
"Expected a value of type ~a, but got a polymorphic function." t))
|
||||
t]))
|
||||
|
||||
;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic
|
||||
;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> tc-result
|
||||
|
|
|
|||
|
|
@ -59,7 +59,7 @@
|
|||
[_ (make-LEmpty)]))
|
||||
|
||||
(d/c (abstract-filter ids keys fs)
|
||||
(-> (listof identifier?) (listof index/c) FilterSet? LFilterSet?)
|
||||
(-> (listof identifier?) (listof index/c) FilterSet/c LatentFilterSet/c)
|
||||
(match fs
|
||||
[(FilterSet: f+ f-)
|
||||
(lcombine
|
||||
|
|
@ -89,7 +89,7 @@
|
|||
(make-FilterSet (apply append f+) (apply append f-))]))
|
||||
|
||||
(d/c (apply-filter lfs t o)
|
||||
(-> LFilterSet? Type/c Object? FilterSet?)
|
||||
(-> LatentFilterSet/c Type/c Object? FilterSet/c)
|
||||
(match lfs
|
||||
[(LFilterSet: lf+ lf-)
|
||||
(combine
|
||||
|
|
@ -113,7 +113,7 @@
|
|||
[((LNotTypeFilter: t pi* _) _ (Path: pi x)) (list (make-NotTypeFilter t (append pi* pi) x))]))
|
||||
|
||||
(define/contract (split-lfilters lf idx)
|
||||
(LFilterSet? index/c . -> . LFilterSet?)
|
||||
(LatentFilterSet/c index/c . -> . LatentFilterSet/c)
|
||||
(define (idx= lf)
|
||||
(match lf
|
||||
[(LBot:) #t]
|
||||
|
|
@ -129,7 +129,7 @@
|
|||
(lambda (stx) #'(FilterSet: (list (Bot:)) _)))
|
||||
|
||||
(d/c (combine-filter f1 f2 f3 t2 t3 o2 o3)
|
||||
(FilterSet? FilterSet? FilterSet? Type? Type? Object? Object? . -> . tc-results?)
|
||||
(FilterSet/c FilterSet/c FilterSet/c Type? Type? Object? Object? . -> . tc-results?)
|
||||
(define (mk f) (ret (Un t2 t3) f (make-Empty)))
|
||||
(match* (f1 f2 f3)
|
||||
[((T-FS:) f _) (ret t2 f o2)]
|
||||
|
|
|
|||
|
|
@ -168,7 +168,7 @@
|
|||
|
||||
|
||||
;; this structure represents the result of typechecking an expression
|
||||
(d-s/c tc-result ([t Type/c] [f FilterSet?] [o Object?]) #:transparent)
|
||||
(d-s/c tc-result ([t Type/c] [f FilterSet/c] [o Object?]) #:transparent)
|
||||
(d-s/c tc-results ([ts (listof tc-result?)] [drest (or/c (cons/c Type/c symbol?) #f)]) #:transparent)
|
||||
|
||||
(define-match-expander tc-result:
|
||||
|
|
@ -178,9 +178,12 @@
|
|||
|
||||
(define-match-expander tc-results:
|
||||
(syntax-parser
|
||||
[(_ tp fp op) #'(struct tc-results ((list (struct tc-result (tp fp op)) (... ...)) #f))]
|
||||
[(_ 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))]))
|
||||
[(_ tp fp op)
|
||||
#'(struct tc-results ((list (struct tc-result (tp fp op)) (... ...)) #f))]
|
||||
[(_ 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))]))
|
||||
|
||||
(define-match-expander tc-result1:
|
||||
(syntax-parser
|
||||
|
|
@ -209,7 +212,7 @@
|
|||
(let ([mk (lambda (t) (make-FilterSet null null))])
|
||||
(make-tc-results
|
||||
(cond [(Type? t)
|
||||
(list (make-tc-result t (mk t) (make-Empty)))]
|
||||
(list (make-tc-result t (mk t) (make-Empty)))]
|
||||
[else
|
||||
(for/list ([i t])
|
||||
(make-tc-result i (mk t) (make-Empty)))])
|
||||
|
|
@ -236,12 +239,14 @@
|
|||
(list (make-tc-result t f o)))
|
||||
(cons dty dbound))]))
|
||||
|
||||
;(trace ret)
|
||||
|
||||
(p/c
|
||||
[ret
|
||||
(->d ([t (or/c Type/c (listof Type/c))])
|
||||
([f (if (list? t)
|
||||
(listof (or/c FilterSet? NoFilter?))
|
||||
FilterSet?)]
|
||||
(listof FilterSet/c)
|
||||
FilterSet/c)]
|
||||
[o (if (list? t)
|
||||
(listof Object?)
|
||||
Object?)]
|
||||
|
|
|
|||
|
|
@ -1,8 +1,8 @@
|
|||
#lang scheme/base
|
||||
|
||||
(require stxclass (for-syntax stxclass scheme/base stxclass/util))
|
||||
(require syntax/parse (for-syntax syntax/parse scheme/base stxclass/util))
|
||||
|
||||
(provide (all-defined-out))
|
||||
(provide (except-out (all-defined-out) define-pred-stxclass))
|
||||
|
||||
(define-syntax (parse/get stx)
|
||||
(syntax-parse stx
|
||||
|
|
@ -24,7 +24,12 @@
|
|||
(define-syntax-class (3d pred)
|
||||
(pattern s
|
||||
#:with datum (syntax-e #'s)
|
||||
#:when (pred #'datum)))
|
||||
#:fail-unless (pred #'datum) #f))
|
||||
|
||||
(define-syntax-rule (define-pred-stxclass name pred)
|
||||
(define-syntax-class name #:attributes ()
|
||||
(pattern x
|
||||
#:fail-unless (pred (syntax-e #'x)) #f)))
|
||||
|
||||
(define-pred-stxclass atom atom?)
|
||||
(define-pred-stxclass byte-pregexp byte-pregexp?)
|
||||
|
|
|
|||
|
|
@ -54,7 +54,7 @@ don't depend on any other portion of the system
|
|||
;(printf "exp: ~a~n" (syntax-object->datum emodule))
|
||||
;(printf "stx (locate): ~a~n" (syntax-object->datum stx))
|
||||
(if (and (not (print-syntax?)) omodule emodule stx)
|
||||
(look-for-in-orig omodule emodule stx)
|
||||
(or (look-for-in-orig omodule emodule stx) stx)
|
||||
stx))
|
||||
|
||||
(define (raise-typecheck-error msg stxs)
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user