Switch subtype to use infer.ss for unification.
This commit is contained in:
Sam Tobin-Hochstadt
parent
37c2f7f2c9
commit
606ef69d20
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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<? rename tc-result-equal?)) ;; done
|
||||
|
||||
;; cycle 2
|
||||
|
||||
|
|
|
|||
|
|
@ -1,11 +1,12 @@
|
|||
#lang scheme/base
|
||||
|
||||
(require (except-in "type-rep.ss" sub-eff) "unify.ss" "type-utils.ss"
|
||||
(require (except-in "type-rep.ss" sub-eff) "type-utils.ss"
|
||||
"tc-utils.ss"
|
||||
"effect-rep.ss"
|
||||
"type-comparison.ss"
|
||||
"resolve-type.ss"
|
||||
"type-name-env.ss"
|
||||
(only-in "infer-dummy.ss" unify)
|
||||
mzlib/plt-match
|
||||
mzlib/trace)
|
||||
|
||||
|
|
@ -197,7 +198,7 @@
|
|||
;; use unification to see if we can use the polytype here
|
||||
[(list (Poly: vs b) s)
|
||||
(=> 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))]
|
||||
|
|
|
|||
|
|
@ -5,7 +5,6 @@
|
|||
"effect-rep.ss"
|
||||
"tc-utils.ss"
|
||||
"subtype.ss"
|
||||
"unify.ss"
|
||||
"infer.ss"
|
||||
"union.ss"
|
||||
"type-utils.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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user