Changeset 21052 in project
 Timestamp:
 10/26/10 03:45:50 (11 years ago)
 Location:
 release/4/miniML
 Files:

 1 edited
 1 copied
Legend:
 Unmodified
 Added
 Removed

release/4/miniML/branches/tiger/miniML.scm
r20827 r21052 74 74 (Let0 (i v b) `(Let0 (,i = ,v) ,b))))) 75 75 76 (definerecordtype tyvar 77 (maketyvar repres level imperative) 78 tyvar? 79 (repres tyvarrepres tyvarrepresset!) ;; representative, for unionfind 80 (level tyvarlevel tyvarlevelset!) ;; binding level, for generalization 81 (imperative tyvarimperative) ;; imperative type variables must not be generalized 82 ;; for use w/ref and side effects 83 ) 84 85 (definedatatype simpletype simpletype? 86 (Tvar (tv tyvar?)) 87 (Tcon (p path?) (ts (lambda (x) (every simpletype? x))))) 88 89 90 (definerecordprinter (simpletype x out) 91 (fprintf out "#<simpletype ~S>" 92 (cases simpletype x 93 (Tvar (tv) `(Tvar repres: ,(tyvarrepres tv) 94 level: ,(tyvarlevel tv) 95 imperative: ,(tyvarimperative tv))) 96 (Tcon (p ts) `(Tcon ,p . ,ts))))) 97 76 77 78 (define tyvar? symbol?) 79 (define (tylist? x) (every ty? x)) 80 (define (tyvarlist? x) (every tyvar? x)) 81 (define (fieldlist? x) (every symbol? x)) 82 83 84 (definedatatype ty ty? 85 (Nil) 86 (Tvar (tv tyvar?)) 87 (Tapp (p path?) (ts tylist?)) 88 (Tpoly (tvs tyvarlist?) (t ty?))) 89 90 91 (define tycon tycon? 92 (Tprim (s string?)) 93 (Trecd (lst fieldlist?)) 94 (Tlam (ts tyvarlist?) (t ty?)) 95 (Tuniq (tc tycon?) (u symbol?))) 96 98 97 99 98 (definerecordtype valtype … … 104 103 ) 105 104 105 106 106 (define (makevaltype q b) 107 107 (if (not (list? q)) (error 'makevaltype "invalid quantified variables list" q)) … … 124 124 ) 125 125 126 127 (definerecordtype kind 128 (makekind arity) 129 kind? 130 (arity kindarity) 131 ) 132 133 134 (define (substtype ty subst) 135 (cond ((simpletype? ty) 136 (cases simpletype ty 137 (Tvar (tv) 138 (or (and (tyvarrepres tv) (substtype (tyvarrepres tv) subst)) ty)) 139 (Tcon (p ts) 140 (Tcon (substpath p subst) (map (lambda (x) (substtype x subst)) ts))) 126 ;; Substitution of paths in type constructors 127 128 (define (substtypepath t subst) 129 (cond ((ty? t) 130 (cases ty t 131 (Tapp (p ts) (Tapp (substpath p subst) 132 (map (lambda (x) (substtypepath x subst)) ts))) 133 134 (Tpoly (tvs t) (Tpoly tvs (substtypepath t subst))) 135 136 (else t) 141 137 )) 142 (else (error 'substtype "invalid type" ty))138 (else (error 'substtypepath "invalid type" ty)) 143 139 )) 144 140 145 141 (define (substvaltype vty subst) 146 142 (makevaltype (valtypequantif vty) 147 (substtype (valtypebody vty) subst)))143 (substtypepath (valtypebody vty) subst))) 148 144 149 145 (define (substdeftype def subst) 150 146 (makedeftype (deftypeparams def) 151 (substtype (deftypebody def) subst))) 152 153 (define (substkind kind subst) kind) 147 (substtypepath (deftypebody def) subst))) 154 148 155 149 … … 161 155 (makemodenv coresyntax)) 162 156 163 164 ;; The typechecker for miniML (HindleyMilner type inference) 165 166 (define (typerepr ty) 167 (assert (simpletype? ty)) 168 (cases simpletype ty 169 (Tvar (tv) 170 (or (and (tyvarrepres tv) 171 (let ((r (typerepr (tyvarrepres tv)))) 172 (tyvarrepresset! tv r) 173 r)) 174 ty)) 175 (else ty))) 176 177 178 (define currentlevel (makeparameter 0)) 179 (define (begindef) (currentlevel (+ 1 (currentlevel)))) 180 (define (enddef) (currentlevel ( (currentlevel) 1))) 181 (define (newvar . rest) (maketyvar #f (currentlevel) 182 (if (null? rest) #f (car rest)))) 183 (define (unknown) (Tvar (newvar))) 184 185 (define (substvars ty subst) 186 (let ((tyvar (typerepr ty))) 187 (assert (simpletype? tyvar)) 188 (cases simpletype tyvar 189 (Tvar (var) (let ((v (assq var subst))) 190 (or (and v (cadr v)) tyvar) )) 191 (Tcon (p ts) 192 (let ((ts1 (map (lambda (t) (substvars t subst)) ts))) 193 (Tcon p ts1)))))) 194 195 196 (define (cannotexpand path) 197 (makepropertycondition 'Cannot_expand 'message path)) 198 (define cannotexpand? 199 (conditionpredicate 'Cannot_expand)) 200 157 ;; Substitution of type variables 158 159 (define (substtypevar t subst) 160 (cond ((ty? t) 161 (cases ty t 162 163 (Nil () t) 164 165 (Tvar (tv) (cond ((assoc tv subst) => (lambda (ti) (cdr ti))) 166 (else t))) 167 168 (Tapp (tc us) (cases tycon tc 169 (Tlam (as t) 170 (substtypevar (substtypevar t (zip as us)) subst)) 171 (else 172 (Tapp tc (map (lambda (tt) (substtypevar tt subst)) us))))) 173 174 (Tpoly (as u) (let* ((gs (listtabulate (length tvs) (lambda (i) (gensym 'g)))) 175 (u1 (substtypevar u (zip as (map Tvar gs))))) 176 (Poly gs (substtypevar u1 subst)))) 177 178 (else t) 179 )) 180 (else (error 'substtypevar "invalid type" ty)) 181 )) 182 183 (define (cannotexpand path) (makepropertycondition 'Cannot_expand 'message path)) 184 185 (define cannotexpand? (conditionpredicate 'Cannot_expand)) 186 187 ;; Find a type constructor identifier in the given environment, and 188 ;; perform type parameter substitution 201 189 202 190 (define (expandmanifest env path args) … … 205 193 (if (not m) 206 194 (signal (cannotexpand path)) 207 (subst vars(deftypebody m)208 209 210 211 212 ;; Expand abbreviations in ty1 and ty2 until their top constructor match 213 (define ( scrapetypes env ty1 ty2)214 (assert ( simpletype? ty1))215 (assert ( simpletype? ty2))216 (let ((repr1 (typerepr ty1))217 (repr2 (typerepr ty2)))195 (substtypevar (deftypebody m) 196 (zip (deftypeparams m) args ) 197 ))))) 198 199 ;; Expand type paths in ty1 and ty2 until their top constructors match 200 201 (define (expandtypepaths env ty1 ty2) 202 (assert (ty? ty1)) 203 (assert (ty? ty2)) 204 (let ((repr1 ty1) 205 (repr2 ty2)) 218 206 (cases simpletype repr1 219 (T con(path1 args1)207 (Tapp (path1 args1) 220 208 (cases simpletype repr2 221 (T con(path2 args2)209 (Tapp (path2 args2) 222 210 (if (pathequal? path1 path2) 223 211 (list repr1 repr2) … … 232 220 (else (abort exn))) 233 221 (let ((m2 (expandmanifest env path2 args2))) 234 ( scrapetypes env repr1 m2))))222 (expandtypepaths env repr1 m2)))) 235 223 (else (abort exn))) 236 224 ) 237 225 (let ((m1 (expandmanifest env path1 args1))) 238 ( scrapetypes env m1 repr2)))226 (expandtypepaths env m1 repr2))) 239 227 )) 240 228 (else … … 247 235 (begin 248 236 (let ((m1 (expandmanifest env path1 args1))) 249 ( scrapetypes env m1 repr2)))237 (expandtypepaths env m1 repr2))) 250 238 )))) 251 239 (else 252 240 (cases simpletype repr2 253 (Tcon(path args)254 (handleexceptions255 256 257 (cond ((cannotexpand? exn)258 259 260 261 (scrapetypes env repr1 m2))))262 263 264 (list repr1 repr2)))))241 (Tapp (path args) 242 (handleexceptions 243 exn 244 (begin 245 (cond ((cannotexpand? exn) 246 (list repr1 repr2)) 247 (else (abort exn)))) 248 (let ((m2 (expandmanifest env path args))) 249 (expandtypepaths env repr1 m2)))) 250 251 (else 252 (list repr1 repr2))))) 265 253 )) 266 254 267 (define (occurcheck var ty) 268 (cases simpletype (typerepr ty) 269 (Tvar (var1) (if (eq? var var1) (error 'occurcheck "cycle in unification"))) 270 (Tcon (p tl) (foreach (lambda (t) (occurcheck var t)) tl)))) 271 272 (define (updatelevels levelmax ty) 273 (cases simpletype (typerepr ty) 274 (Tvar (v) (if (< levelmax (tyvarlevel v)) 275 (tyvarlevelset! v levelmax))) 276 (Tcon (p tl) (foreach (lambda (t) (updatelevels levelmax t)) tl)))) 277 278 (define (unify env t1 t2) 279 (let* ((rs (scrapetypes env t1 t2)) 255 (define (unify env ty1 ty2) 256 (let* ((rs (expandtypepaths env ty1 ty2)) 280 257 (r1 (car rs)) 281 258 (r2 (cadr rs))) 282 283 (assert (simpletype? r1)) 284 (assert (simpletype? r2)) 285 (if (equal? r1 r2) '() 286 (cases simpletype r1 287 (Tvar (v) 288 (begin 289 (occurcheck v r2) 290 (updatelevels (tyvarlevel v) r2) 291 (tyvarrepresset! v r2))) 292 (else 293 (cases simpletype r2 294 (Tvar (v) 295 (begin 296 (occurcheck v r1) 297 (updatelevels (tyvarlevel v) r1) 298 (tyvarrepresset! v r1))) 299 (else 300 (cases simpletype r1 301 (Tcon (path1 args1) 302 (cases simpletype r2 303 (Tcon (path2 args2) 304 (if (pathequal? path1 path2) 305 (foreach (lambda (t1 t2) (unify env t1 t2)) args1 args2) 306 (error 'unify "type constructor mismatch in unification" t1 t2))) 307 (else (error 'unify "type constructor mismatch in unification" t1 t2)) 308 )) 309 (else (error 'unify "type constructor mismatch in unification" t1 t2)))) 310 )) 311 )))) 312 313 (define (generalize ty) 314 (define (genvars vars ty) 315 (cases simpletype ty 316 (Tvar (v) 317 (if (and (< (currentlevel) (tyvarlevel v)) 318 (not (tyvarimperative v)) 319 (member v vars)) 320 (cons v vars) 321 vars)) 322 (Tcon (path tl) 323 (fold genvars tl vars)))) 324 325 (makevaltype (genvars '() ty) ty)) 326 327 (define (trivialscheme ty) 328 (makevaltype '() ty)) 329 330 (define (instance vty) 331 (let ((vars (valtypequantif vty))) 332 (if (null? vars) 333 (valtypebody vty) 334 (substvars (valtypebody vty) 335 (map (lambda (v) (list v (unknown))) vars) )))) 259 260 261 )) 262 263 264 336 265 337 266 (define identarrow (identcreate ">")) … … 372 301 ((bool) (Tcon pathbool '())) 373 302 (else (error 'consttype "invalid constant" c))))) 303 374 304 375 305 (define (infertype env t) … … 825 755 826 756 757 # 758 (definerecordtype tyvar 759 (maketyvar repres level imperative) 760 tyvar? 761 (repres tyvarrepres tyvarrepresset!) ;; representative, for unionfind 762 (level tyvarlevel tyvarlevelset!) ;; binding level, for generalization 763 (imperative tyvarimperative) ;; imperative type variables must not be generalized 764 ;; for use w/ref and side effects 765 ) 766 767 (definerecordprinter (simpletype x out) 768 (fprintf out "#<simpletype ~S>" 769 (cases simpletype x 770 (Tvar (tv) `(Tvar repres: ,(tyvarrepres tv) 771 level: ,(tyvarlevel tv) 772 imperative: ,(tyvarimperative tv))) 773 (Tcon (p ts) `(Tcon ,p . ,ts))))) 774 775 776 (definerecordtype kind 777 (makekind arity) 778 kind? 779 (arity kindarity) 780 ) 781 782 # 783 827 784 828 785
Note: See TracChangeset
for help on using the changeset viewer.