From cf872c4e38195152df74750653d888c4dffced61 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Tue, 8 Sep 2009 19:51:34 +0000 Subject: [PATCH] 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 --- .../typed-scheme/succeed/null-program.ss | 1 + .../tests/typed-scheme/succeed/typed-list.ss | 3 +- .../unit-tests/parse-type-tests.ss | 16 ++-- .../unit-tests/typecheck-tests.ss | 76 ++++++++++--------- collects/typed-scheme/main.ss | 6 +- collects/typed-scheme/private/base-env.ss | 9 ++- .../typed-scheme/private/base-types-extra.ss | 9 ++- collects/typed-scheme/private/colon.ss | 49 ++++++++++++ collects/typed-scheme/private/parse-type.ss | 39 +++++++++- collects/typed-scheme/private/prims.ss | 44 ++--------- .../typed-scheme/private/type-annotation.ss | 2 +- collects/typed-scheme/rep/filter-rep.ss | 12 ++- .../typed-scheme/typecheck/tc-expr-unit.ss | 12 +++ .../typed-scheme/typecheck/tc-lambda-unit.ss | 12 +-- .../typecheck/tc-metafunctions.ss | 8 +- collects/typed-scheme/types/utils.ss | 19 +++-- collects/typed-scheme/utils/stxclass-util.ss | 11 ++- collects/typed-scheme/utils/tc-utils.ss | 2 +- 18 files changed, 219 insertions(+), 111 deletions(-) create mode 100644 collects/tests/typed-scheme/succeed/null-program.ss create mode 100644 collects/typed-scheme/private/colon.ss diff --git a/collects/tests/typed-scheme/succeed/null-program.ss b/collects/tests/typed-scheme/succeed/null-program.ss new file mode 100644 index 00000000..3297b32c --- /dev/null +++ b/collects/tests/typed-scheme/succeed/null-program.ss @@ -0,0 +1 @@ +#lang typed-scheme diff --git a/collects/tests/typed-scheme/succeed/typed-list.ss b/collects/tests/typed-scheme/succeed/typed-list.ss index 738aa8dd..06b4e4b5 100644 --- a/collects/tests/typed-scheme/succeed/typed-list.ss +++ b/collects/tests/typed-scheme/succeed/typed-list.ss @@ -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)))) diff --git a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss index b55ba900..f9c7358c 100644 --- a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss @@ -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 diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss index 7501a64c..c6f2ae32 100644 --- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss @@ -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] diff --git a/collects/typed-scheme/main.ss b/collects/typed-scheme/main.ss index f4454c49..e2f553da 100644 --- a/collects/typed-scheme/main.ss +++ b/collects/typed-scheme/main.ss @@ -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"))) diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 099136e9..74ffe8d3 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.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))] \ No newline at end of file + (Univ -Integer . -> . -Void))] + +;; unsafe + +[unsafe-cdr (-poly (a b) + (cl->* + (->acc (list (-pair a b)) b (list -cdr))))] \ No newline at end of file diff --git a/collects/typed-scheme/private/base-types-extra.ss b/collects/typed-scheme/private/base-types-extra.ss index b31f182f..72c90ef6 100644 --- a/collects/typed-scheme/private/base-types-extra.ss +++ b/collects/typed-scheme/private/base-types-extra.ss @@ -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 ∀] diff --git a/collects/typed-scheme/private/colon.ss b/collects/typed-scheme/private/colon.ss new file mode 100644 index 00000000..15bf2c98 --- /dev/null +++ b/collects/typed-scheme/private/colon.ss @@ -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)")])])) \ No newline at end of file diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss index 1d2a654e..585545af 100644 --- a/collects/typed-scheme/private/parse-type.ss +++ b/collects/typed-scheme/private/parse-type.ss @@ -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)) +|# \ No newline at end of file diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss index f235bcbd..ccace1df 100644 --- a/collects/typed-scheme/private/prims.ss +++ b/collects/typed-scheme/private/prims.ss @@ -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) diff --git a/collects/typed-scheme/private/type-annotation.ss b/collects/typed-scheme/private/type-annotation.ss index d4f548b7..17cb1a37 100644 --- a/collects/typed-scheme/private/type-annotation.ss +++ b/collects/typed-scheme/private/type-annotation.ss @@ -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] diff --git a/collects/typed-scheme/rep/filter-rep.ss b/collects/typed-scheme/rep/filter-rep.ss index f5f6e90b..6720ab4b 100644 --- a/collects/typed-scheme/rep/filter-rep.ss +++ b/collects/typed-scheme/rep/filter-rep.ss @@ -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))))) \ No newline at end of file diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss index f84244ac..b92a1b5f 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.ss +++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss @@ -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 diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.ss b/collects/typed-scheme/typecheck/tc-lambda-unit.ss index 6cfe6e0c..c3f8d228 100644 --- a/collects/typed-scheme/typecheck/tc-lambda-unit.ss +++ b/collects/typed-scheme/typecheck/tc-lambda-unit.ss @@ -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 diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss index 1ece7083..5e2b7919 100644 --- a/collects/typed-scheme/typecheck/tc-metafunctions.ss +++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss @@ -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)] diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss index 225b8a95..2bbf1619 100644 --- a/collects/typed-scheme/types/utils.ss +++ b/collects/typed-scheme/types/utils.ss @@ -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?)] diff --git a/collects/typed-scheme/utils/stxclass-util.ss b/collects/typed-scheme/utils/stxclass-util.ss index fa0e445e..c1c2ce27 100644 --- a/collects/typed-scheme/utils/stxclass-util.ss +++ b/collects/typed-scheme/utils/stxclass-util.ss @@ -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?) diff --git a/collects/typed-scheme/utils/tc-utils.ss b/collects/typed-scheme/utils/tc-utils.ss index 00bc41ca..33e3a263 100644 --- a/collects/typed-scheme/utils/tc-utils.ss +++ b/collects/typed-scheme/utils/tc-utils.ss @@ -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)