type-constraints.rkt (8321B)
1 #lang racket/base 2 3 (provide add-constraints 4 add-constraints/var? 5 lookup 6 lookup-Xs/keep-unsolved 7 inst-type 8 inst-type/orig 9 inst-type/cs 10 inst-types/cs 11 inst-type/cs/orig 12 inst-types/cs/orig 13 ) 14 15 (require syntax/parse 16 syntax/stx 17 (for-meta -1 "typecheck.rkt") 18 "stx-utils.rkt" 19 ) 20 21 ;; add-constraints : 22 ;; (Listof Id) (Listof (List Id Type)) (Stx-Listof (Stx-List Stx Stx)) -> (Listof (List Id Type)) 23 ;; Adds a new set of constaints to a substituion, using the type 24 ;; unification algorithm for local type inference. 25 (define (add-constraints Xs substs new-cs [orig-cs new-cs]) 26 (define Xs* (stx->list Xs)) 27 (define (X? X) 28 (member X Xs* free-identifier=?)) 29 (add-constraints/var? Xs* X? substs new-cs orig-cs)) 30 31 (define (add-constraints/var? Xs* var? substs new-cs [orig-cs new-cs]) 32 (define Xs (stx->list Xs*)) 33 (define Ys (stx-map stx-car substs)) 34 (define-syntax-class var 35 [pattern x:id #:when (var? #'x)]) 36 (syntax-parse new-cs 37 [() substs] 38 [([a:var b] . rst) 39 (cond 40 [(member #'a Ys free-identifier=?) 41 ;; There are two cases. 42 ;; Either #'a already maps to #'b or an equivalent type, 43 ;; or #'a already maps to a type that conflicts with #'b. 44 ;; In either case, whatever #'a maps to must be equivalent 45 ;; to #'b, so add that to the constraints. 46 (add-constraints/var? 47 Xs 48 var? 49 substs 50 (cons (list (lookup #'a substs) #'b) 51 #'rst) 52 orig-cs)] 53 [(and (identifier? #'b) (var? #'b) (free-identifier=? #'a #'b)) 54 ;; #'a and #'b are equal, drop this constraint 55 (add-constraints/var? Xs var? substs #'rst orig-cs)] 56 [else 57 (define entry (occurs-check (list #'a #'b) orig-cs)) 58 (add-constraints/var? 59 Xs 60 var? 61 ;; Add the mapping #'a -> #'b to the substitution, 62 (add-substitution-entry entry substs) 63 ;; and substitute that in each of the constraints. 64 (cs-substitute-entry entry #'rst) 65 orig-cs)])] 66 [([a b:var] . rst) 67 (add-constraints/var? Xs 68 var? 69 substs 70 #'([b a] . rst) 71 orig-cs)] 72 [([a b] . rst) 73 ;; If #'a and #'b are base types, check that they're equal. 74 ;; Identifers not within Xs count as base types. 75 ;; If #'a and #'b are constructed types, check that the 76 ;; constructors are the same, add the sub-constraints, and 77 ;; recur. 78 ;; Otherwise, raise an error. 79 (cond 80 [(identifier? #'a) 81 ;; #'a is an identifier, but not a var, so it is considered 82 ;; a base type. We also know #'b is not a var, so #'b has 83 ;; to be the same "identifier base type" as #'a. 84 (unless (and (identifier? #'b) (free-identifier=? #'a #'b)) 85 (type-error #:src (get-orig #'b) 86 #:msg (format "couldn't unify ~~a and ~~a\n expected: ~a\n given: ~a" 87 (string-join (map type->str (stx-map stx-car orig-cs)) ", ") 88 (string-join (map type->str (stx-map stx-cadr orig-cs)) ", ")) 89 #'a #'b)) 90 (add-constraints/var? Xs 91 var? 92 substs 93 #'rst 94 orig-cs)] 95 [else 96 (syntax-parse #'[a b] 97 [_ 98 #:when (typecheck? #'a #'b) 99 (add-constraints/var? Xs 100 var? 101 substs 102 #'rst 103 orig-cs)] 104 [((~Any tycons1 τ1 ...) (~Any tycons2 τ2 ...)) 105 #:when (typecheck? #'tycons1 #'tycons2) 106 #:when (stx-length=? #'[τ1 ...] #'[τ2 ...]) 107 (add-constraints/var? Xs 108 var? 109 substs 110 #'((τ1 τ2) ... . rst) 111 orig-cs)] 112 [else 113 (type-error #:src (get-orig #'b) 114 #:msg (format "couldn't unify ~~a and ~~a\n expected: ~a\n given: ~a" 115 (string-join (map type->str (stx-map stx-car orig-cs)) ", ") 116 (string-join (map type->str (stx-map stx-cadr orig-cs)) ", ")) 117 #'a #'b)])])])) 118 119 (define (datum=? x y) 120 (equal? (syntax->datum x) (syntax->datum y))) 121 122 ;; add-substitution-entry : (List Id Type) (Listof (List Id Type)) -> (Listof (List Id Type)) 123 ;; Adds the mapping a -> b to the substitution and substitutes for it in the other entries 124 (define (add-substitution-entry entry substs) 125 (match-define (list a b) entry) 126 (cons entry 127 (for/list ([subst (in-list substs)]) 128 (list (first subst) 129 (inst-type/orig (list b) (list a) (second subst) datum=?))))) 130 131 ;; cs-substitute-entry : (List Id Type) (Stx-Listof (Stx-List Stx Stx)) -> (Listof (List Stx Stx)) 132 ;; substitute a -> b in each of the constraints 133 (define (cs-substitute-entry entry cs) 134 (match-define (list a b) entry) 135 (for/list ([c (in-list (stx->list cs))]) 136 (list (inst-type/orig (list b) (list a) (stx-car c) datum=?) 137 (inst-type/orig (list b) (list a) (stx-cadr c) datum=?)))) 138 139 ;; occurs-check : (List Id Type) (Stx-Listof (Stx-List Stx Stx)) -> (List Id Type) 140 (define (occurs-check entry orig-cs) 141 (match-define (list a b) entry) 142 (cond [(stx-contains-id? b a) 143 (type-error #:src (get-orig b) 144 #:msg (format (string-append 145 "couldn't unify ~~a and ~~a because one contains the other\n" 146 " expected: ~a\n" 147 " given: ~a") 148 (string-join (map type->str (stx-map stx-car orig-cs)) ", ") 149 (string-join (map type->str (stx-map stx-cadr orig-cs)) ", ")) 150 a b)] 151 [else entry])) 152 153 (define (lookup x substs) 154 (syntax-parse substs 155 [((y:id τ) . rst) 156 #:when (free-identifier=? #'y x) 157 #'τ] 158 [(_ . rst) (lookup x #'rst)] 159 [() #f])) 160 161 ;; lookup-Xs/keep-unsolved : (Stx-Listof Id) Constraints -> (Listof Type-Stx) 162 ;; looks up each X in the constraints, returning the X if it's unconstrained 163 (define (lookup-Xs/keep-unsolved Xs cs) 164 (for/list ([X (in-stx-list Xs)]) 165 (or (lookup X cs) X))) 166 167 ;; instantiate polymorphic types 168 ;; inst-type : (Listof Type) (Listof Id) Type -> Type 169 ;; Instantiates ty with the tys-solved substituted for the Xs, where the ith 170 ;; identifier in Xs is associated with the ith type in tys-solved 171 (define (inst-type tys-solved Xs ty) 172 (substs tys-solved Xs ty)) 173 ;; inst-type/orig : (Listof Type) (Listof Id) Type (Id Id -> Bool) -> Type 174 ;; like inst-type, but also substitutes within the orig property 175 (define (inst-type/orig tys-solved Xs ty [var=? free-identifier=?]) 176 (add-orig (inst-type tys-solved Xs ty) 177 (substs (stx-map get-orig tys-solved) Xs (get-orig ty) var=?))) 178 179 ;; inst-type/cs : (Stx-Listof Id) Constraints Type-Stx -> Type-Stx 180 ;; Instantiates ty, substituting each identifier in Xs with its mapping in cs. 181 (define (inst-type/cs Xs cs ty) 182 (define tys-solved (lookup-Xs/keep-unsolved Xs cs)) 183 (inst-type tys-solved Xs ty)) 184 ;; inst-types/cs : (Stx-Listof Id) Constraints (Stx-Listof Type-Stx) -> (Listof Type-Stx) 185 ;; the plural version of inst-type/cs 186 (define (inst-types/cs Xs cs tys) 187 (stx-map (lambda (t) (inst-type/cs Xs cs t)) tys)) 188 189 ;; inst-type/cs/orig : 190 ;; (Stx-Listof Id) Constraints Type-Stx (Id Id -> Bool) -> Type-Stx 191 ;; like inst-type/cs, but also substitutes within the orig property 192 (define (inst-type/cs/orig Xs cs ty [var=? free-identifier=?]) 193 (define tys-solved (lookup-Xs/keep-unsolved Xs cs)) 194 (inst-type/orig tys-solved Xs ty var=?)) 195 ;; inst-types/cs/orig : 196 ;; (Stx-Listof Id) Constraints (Stx-Listof Type-Stx) (Id Id -> Bool) -> (Listof Type-Stx) 197 ;; the plural version of inst-type/cs/orig 198 (define (inst-types/cs/orig Xs cs tys [var=? free-identifier=?]) 199 (stx-map (lambda (t) (inst-type/cs/orig Xs cs t var=?)) tys)) 200