diff --git a/collects/typed-scheme/private/check-subforms-unit.ss b/collects/typed-scheme/private/check-subforms-unit.ss index 20ff3b8f4c..55d40492c1 100644 --- a/collects/typed-scheme/private/check-subforms-unit.ss +++ b/collects/typed-scheme/private/check-subforms-unit.ss @@ -10,7 +10,6 @@ "type-utils.ss" "utils.ss" ;; doesn't need tests "type-rep.ss" ;; doesn't need tests - "unify.ss" ;; needs tests "type-effect-convenience.ss" ;; maybe needs tests "union.ss" "subtype.ss" ;; has tests diff --git a/collects/typed-scheme/private/infer.ss b/collects/typed-scheme/private/infer.ss index dec53a6473..1279f3785d 100644 --- a/collects/typed-scheme/private/infer.ss +++ b/collects/typed-scheme/private/infer.ss @@ -281,7 +281,8 @@ ;; X : variables to infer ;; S : actual argument types ;; T : formal argument types -;; R : result type or #f +;; R : result type +;; expected : boolean ;; returns a substitution ;; if R is #f, we don't care about the substituion ;; just return a boolean result diff --git a/collects/typed-scheme/private/provide-handling.ss b/collects/typed-scheme/private/provide-handling.ss index 55e5ac850f..b6df48696f 100644 --- a/collects/typed-scheme/private/provide-handling.ss +++ b/collects/typed-scheme/private/provide-handling.ss @@ -8,7 +8,6 @@ "tc-structs.ss" "utils.ss" ;; doesn't need tests "type-rep.ss" ;; doesn't need tests - "unify.ss" ;; needs tests "type-effect-convenience.ss" ;; maybe needs tests "union.ss" "subtype.ss" ;; has tests diff --git a/collects/typed-scheme/private/remove-intersect.ss b/collects/typed-scheme/private/remove-intersect.ss index afdb21bde1..f9b273e80a 100644 --- a/collects/typed-scheme/private/remove-intersect.ss +++ b/collects/typed-scheme/private/remove-intersect.ss @@ -1,6 +1,6 @@ #lang scheme/base -(require "type-rep.ss" "unify.ss" "union.ss" "subtype.ss" +(require "type-rep.ss" "union.ss" "subtype.ss" "type-utils.ss" "resolve-type.ss" "type-effect-convenience.ss" mzlib/plt-match mzlib/trace) diff --git a/collects/typed-scheme/private/signatures.ss b/collects/typed-scheme/private/signatures.ss index d028b717a7..caebec8198 100644 --- a/collects/typed-scheme/private/signatures.ss +++ b/collects/typed-scheme/private/signatures.ss @@ -2,19 +2,6 @@ (require scheme/unit) (provide (all-defined-out)) -;; cycle 1 - -(define-signature type-printer^ - (print-type has-name print-effect)) ;; done - -(define-signature infer^ - (unify1 fv fv/list unfold)) ;; done - -(define-signature subst^ - (subst subst-all)) ;; done - -(define-signature type-equal^ - (type-equal? type-compare type unmatch) - (if (unify1 s b) A0 (unmatch))] + (if (unify vs (list b) (list s)) A0 (unmatch))] [(list s (Poly: vs b)) (=> unmatch) (if (null? (fv b)) (subtype* A0 s b) (unmatch))] diff --git a/collects/typed-scheme/private/tc-app-unit.ss b/collects/typed-scheme/private/tc-app-unit.ss index c5bafb1428..99c9bb89d6 100644 --- a/collects/typed-scheme/private/tc-app-unit.ss +++ b/collects/typed-scheme/private/tc-app-unit.ss @@ -5,7 +5,6 @@ "effect-rep.ss" "tc-utils.ss" "subtype.ss" - "unify.ss" "infer.ss" "union.ss" "type-utils.ss" diff --git a/collects/typed-scheme/private/tc-expr-unit.ss b/collects/typed-scheme/private/tc-expr-unit.ss index 062955adff..05ceccd1bd 100644 --- a/collects/typed-scheme/private/tc-expr-unit.ss +++ b/collects/typed-scheme/private/tc-expr-unit.ss @@ -11,7 +11,6 @@ "type-utils.ss" "utils.ss" ;; doesn't need tests "type-rep.ss" ;; doesn't need tests - "unify.ss" ;; needs tests "type-effect-convenience.ss" ;; maybe needs tests "union.ss" "subtype.ss" ;; has tests diff --git a/collects/typed-scheme/private/unify.ss b/collects/typed-scheme/private/unify.ss deleted file mode 100644 index 6e42fc3f09..0000000000 --- a/collects/typed-scheme/private/unify.ss +++ /dev/null @@ -1,106 +0,0 @@ -#lang scheme/base - -(require "planet-requires.ss" - "type-rep.ss" - "effect-rep.ss" - "type-comparison.ss" - "resolve-type.ss" - "type-utils.ss") -(require mzlib/plt-match - mzlib/trace) - -(provide unify1) - - -;; the types in the constraint list must be well-formed -(define (unify cl) (unify/acc cl '())) - -(define (unify1 t1 t2) (unify (list (list t1 t2)))) - -(define (unify/acc constraint-list acc) - (parameterize ([match-equality-test type-equal?]) - (match constraint-list - ;; done! - [(list) acc] - ;; equal constraints can be discarded - [(list (list t t) rest ...) (unify/acc rest acc)] - ;; name resolution - [(list (list (Name: n) (Name: n*)) rest ...) - (if (free-identifier=? n n*) - (unify/acc rest acc) - #f)] - ;; type application - [(list (list (App: r args _) (App: r* args* _)) rest ...) - (unify/acc (append (map list (cons r args) (cons r* args*)) rest) acc)] - ;; unequal bound variables do not unify - [(list (list (B: _) (B: _)) rest ...) #f] - ;; unify a variable (skipping the occurs check for now) - [(list (list (F: v) t) rest ...) - (unify/acc (map (lambda (p) (map (lambda (e) (subst v t e)) p)) rest) - (cons (list v t) acc))] - [(list (list t (F: v)) rest ...) - (unify/acc (map (lambda (p) (map (lambda (e) (subst v t e)) p)) rest) - (cons (list v t) acc))] - ;; arrow types - just add a whole bunch of new constraints - [(list (list (Function: (list (arr: ts t t-rest #f t-thn-eff t-els-eff) ...)) - (Function: (list (arr: ss s s-rest #f s-thn-eff s-els-eff) ...))) - rest ...) - #;(printf "arrow unification~n") - (let () - (define (compatible-rest t-rest s-rest) - (andmap (lambda (x y) (or (and x y) (and (not x) (not y)))) ;; either both #f or both not #f - t-rest s-rest)) - (define (flatten/zip x y) (map list (apply append x) (apply append y))) - (if (and (= (length ts) (length ss)) - (compatible-rest t-rest s-rest) - (effects-equal? t-thn-eff s-thn-eff) - (effects-equal? t-els-eff s-els-eff)) - (let ([ret-constraints (map list t s)] - ;; remove the #f's before adding to the constraints - [rest-constraints (map list (filter values t-rest) (filter values s-rest))] - ;; transform ((a b c) (d e)) ((1 2 3) (4 5)) into ((a 1) (b 2) (c 3) (d 4) (e 5)) - [arg-constraints (flatten/zip ts ss)]) - #;(printf "constraints ~a~n"(append ret-constraints rest-constraints arg-constraints)) - (unify/acc (append arg-constraints rest-constraints ret-constraints rest) acc)) - (begin #;(printf "failure!~n") #f)))] - ;; aggregate types are simple - [(list (list (Vector: t) (Vector: s)) rest ...) (unify/acc (cons (list t s) rest) acc)] - [(list (list (Pair: t1 t2) (Pair: s1 s2)) rest ...) - (unify/acc (list* (list t1 s1) (list t2 s2) rest) acc)] - [(list (list (Hashtable: t1 t2) (Hashtable: s1 s2)) rest ...) - (unify/acc (list* (list t1 s1) (list t2 s2) rest) acc)] - [(list (list (Param: t1 t2) (Param: s1 s2)) rest ...) - (unify/acc (list* (list t1 s1) (list t2 s2) rest) acc)] - ;; structs - [(list (list (Struct: nm p elems proc _ _ _) (Struct: nm p elems* proc* _ _ _)) rest ...) - (cond [(and proc proc*) - (unify/acc (append rest (map list elems elems*) (list (list proc proc*))) acc)] - [(or proc proc*) #f] - [else (unify/acc (append rest (map list elems elems*)) acc)])] - ;; union types - oh no! - [(list (list (Union: l1) (Union: l2)) rest ...) - (and (= (length l1) (length l2)) - (unify/acc (append (map list l1 l2) rest) acc))] - [(list (or (list (Union: _) _) (list _ (Union: _))) rest ...) - #;(printf "FIXME: union type ~n~a~n---------~n~a~n in unifier~n" - (caar constraint-list) - (cadar constraint-list)) - #f] - ;; mu types - [(list (list (Mu-unsafe: s) (Mu-unsafe: t)) rest ...) - (unify/acc (cons (list s t) rest) acc)] - [(list (list t (? Mu? s)) rest ...) (unify/acc (cons (list t (unfold s)) rest) acc)] - [(list (list (? Mu? s) t) rest ...) (unify/acc (cons (list (unfold s) t) rest) acc)] - #;[((or (($ mu _ _) _) (_ ($ mu _ _))) rest ...) - (printf "FIXME: mu types ~a in unifier~n" constraint-list) - #f] - ;; polymorphic types - don't do that - [(list (or (list _ (? Poly?)) (list _ (? Poly?))) rest ...) - ;(printf "FIXME: poly type in unifier~n") - #f] - ;; nothing else can have type variables - [else #f] - ))) - -;(trace unify/acc) - diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss index da552fea9d..939c49d5c4 100644 --- a/collects/typed-scheme/typed-scheme.ss +++ b/collects/typed-scheme/typed-scheme.ss @@ -13,6 +13,8 @@ "private/type-name-env.ss" "private/type-alias-env.ss" "private/utils.ss" + (only-in "private/infer-dummy.ss" infer-param) + "private/infer.ss" "private/type-effect-convenience.ss" "private/type-contract.ss" scheme/nest @@ -47,7 +49,10 @@ [with-handlers ([(lambda (e) (and catch-errors? (exn:fail? e) (not (exn:fail:syntax? e)))) (lambda (e) (tc-error "Internal error: ~a" e))])] - [parameterize ([delay-errors? #t] + [parameterize (;; a cheat to avoid units + [infer-param infer] + ;; do we report multiple errors + [delay-errors? #t] ;; this parameter is for parsing types [current-tvars initial-tvar-env] ;; this parameter is just for printing types @@ -93,7 +98,9 @@ [(_ . form) (nest ([begin (set-box! typed-context? #t)] - [parameterize (;; this paramter is for parsing types + [parameterize (;; a cheat to avoid units + [infer-param infer] + ;; this paramter is for parsing types [current-tvars initial-tvar-env] ;; this parameter is just for printing types ;; this is a parameter to avoid dependency issues