1 2 -- ==========================================================-- 3 -- === A type-checker -- v5 File: TypeCheck5.m (1) ===-- 4 -- === Corrected version for 0.210a ===-- 5 -- ==========================================================-- 6 7 module TypeCheck5 where 8 import BaseDefs 9 import Utils 10 import MyUtils 11 12 import List(nub) -- 1.3 13 14 -- ==========================================================-- 15 -- === Formatting of results ===-- 16 -- ==========================================================-- 17 18 tcMapAnnExpr :: (a -> b) -> 19 AnnExpr c a -> 20 AnnExpr c b 21 22 tcMapAnnExpr f (ann, node) 23 = (f ann, mapAnnExpr' node) 24 where 25 mapAnnExpr' (AVar v) = AVar v 26 mapAnnExpr' (ANum n) = ANum n 27 mapAnnExpr' (AConstr c) = AConstr c 28 mapAnnExpr' (AAp ae1 ae2) 29 = AAp (tcMapAnnExpr f ae1) (tcMapAnnExpr f ae2) 30 mapAnnExpr' (ALet recFlag annDefs mainExpr) 31 = ALet recFlag (map mapAnnDefn annDefs) (tcMapAnnExpr f mainExpr) 32 mapAnnExpr' (ACase switchExpr annAlts) 33 = ACase (tcMapAnnExpr f switchExpr) (map mapAnnAlt annAlts) 34 mapAnnExpr' (ALam vs e) = ALam vs (tcMapAnnExpr f e) 35 36 mapAnnDefn (naam, expr) 37 = (naam, tcMapAnnExpr f expr) 38 39 mapAnnAlt (naam, (pars, resExpr)) 40 = (naam, (pars, tcMapAnnExpr f resExpr)) 41 42 43 -- ======================================================-- 44 -- 45 tcSubstAnnTree :: Subst -> 46 AnnExpr Naam TExpr -> 47 AnnExpr Naam TExpr 48 49 tcSubstAnnTree phi tree = tcMapAnnExpr (tcSub_type phi) tree 50 51 52 -- ======================================================-- 53 -- 54 tcTreeToEnv :: AnnExpr Naam TExpr -> 55 TypeEnv 56 57 tcTreeToEnv tree 58 = t2e tree 59 where 60 t2e (nodeType, node) = t2e' node 61 62 t2e' (AVar v) = [] 63 t2e' (ANum n) = [] 64 t2e' (AConstr c) = [] 65 t2e' (AAp ae1 ae2) = (t2e ae1) ++ (t2e ae2) 66 t2e' (ALam cs e) = t2e e 67 t2e' (ALet rf dl me) 68 = (concat (map aFN dl)) ++ (t2e me) 69 t2e' (ACase sw alts) 70 = (t2e sw) ++ (concat (map (t2e.second.second) alts)) 71 72 aFN (naam, (tijp, body)) 73 = (naam, tijp):(t2e' body) 74 75 76 77 -- ======================================================-- 78 -- 79 tcShowtExpr :: TExpr -> 80 [Char] 81 82 tcShowtExpr t 83 = pretty' False t 84 where 85 pretty' b (TVar tvname) = [' ', toEnum (96+(lookup tvname tvdict))] 86 pretty' b (TCons "int" []) = " int" 87 pretty' b (TCons "bool" []) = " bool" 88 pretty' b (TCons "char" []) = " char" 89 pretty' True (TArr t1 t2) 90 = " (" ++ (pretty' True t1) ++ " -> " ++ 91 (pretty' False t2) ++ ")" 92 pretty' False (TArr t1 t2) 93 = (pretty' True t1) ++ " -> " ++ 94 (pretty' False t2) 95 pretty' b (TCons notArrow cl) 96 = " (" ++ notArrow ++ 97 concat (map (pretty' True) cl) ++ ")" 98 lookup tvname [] 99 = panic "tcShowtExpr: Type name lookup failed" 100 lookup tvname (t:ts) | t==tvname = 1 101 | otherwise = 1 + (lookup tvname ts) 102 tvdict = nub (tvdict' t) 103 tvdict' (TVar t) = [t] 104 tvdict' (TCons c ts) = concat (map tvdict' ts) 105 tvdict' (TArr t1 t2) = tvdict' t1 ++ tvdict' t2 106 107 108 -- ======================================================-- 109 -- 110 tcPretty :: (Naam, TExpr) -> 111 [Char] 112 113 tcPretty (naam, tipe) 114 = "\n " ++ (ljustify 25 (naam ++ " :: ")) ++ 115 (tcShowtExpr tipe) 116 117 118 -- ======================================================-- 119 tcCheck :: TcTypeEnv -> 120 TypeNameSupply -> 121 AtomicProgram -> 122 ([Char], Reply (AnnExpr Naam TExpr, TypeEnv) Message) 123 124 tcCheck baseTypes ns (tdefs, expr) 125 = if good tcResult 126 then (fullEnvWords, Ok (rootTree, fullEnv)) 127 else ("", Fail "No type") 128 where 129 tcResult = tc (tdefs++builtInTypes) 130 (baseTypes++finalConstrTypes) finalNs expr 131 132 good (Ok x) = True 133 good (Fail x2) = False 134 135 (rootSubst, rootType, annoTree) = f tcResult where f (Ok x) = x 136 137 rootTree = tcSubstAnnTree rootSubst annoTree 138 139 rootEnv = tcTreeToEnv rootTree 140 141 fullEnv = rootEnv ++ map f finalConstrTypes 142 where 143 f (naam, (Scheme vs t)) = (naam, t) 144 145 fullEnvWords = concat (map tcPretty fullEnv) 146 147 (finalNs, constrTypes) = 148 mapAccuml tcConstrTypeSchemes ns (tdefs++builtInTypes) 149 finalConstrTypes = concat constrTypes 150 151 builtInTypes 152 = [ ("bool", [], [("True", []), ("False", [])]) ] 153 154 155 156 -- ==========================================================-- 157 -- === 9.2 Representation of type expressions ===-- 158 -- ==========================================================-- 159 160 -- ======================================================-- 161 --tcArrow :: TExpr -> 162 -- TExpr -> 163 -- TExpr 164 -- 165 --tcArrow t1 t2 = TArr t1 t2 166 167 168 169 -- ======================================================-- 170 tcInt :: TExpr 171 172 tcInt = TCons "int" [] 173 174 175 176 -- ======================================================-- 177 tcBool :: TExpr 178 179 tcBool = TCons "bool" [] 180 181 182 183 -- ======================================================-- 184 tcTvars_in :: TExpr -> 185 [TVName] 186 187 tcTvars_in t = tvars_in' t [] 188 where 189 tvars_in' (TVar x) l = x:l 190 tvars_in' (TCons y ts) l = foldr tvars_in' l ts 191 tvars_in' (TArr t1 t2) l = tvars_in' t1 (tvars_in' t2 l) 192 193 194 -- ==========================================================-- 195 -- === 9.41 Substitutions ===-- 196 -- ==========================================================-- 197 198 -- ======================================================-- 199 tcApply_sub :: Subst -> 200 TVName -> 201 TExpr 202 203 tcApply_sub phi tvn 204 = if TVar tvn == lookUpResult 205 then TVar tvn 206 else tcSub_type phi lookUpResult 207 where 208 lookUpResult = utLookupDef phi tvn (TVar tvn) 209 210 211 -- ======================================================-- 212 tcSub_type :: Subst -> 213 TExpr -> 214 TExpr 215 216 tcSub_type phi (TVar tvn) = tcApply_sub phi tvn 217 218 tcSub_type phi (TCons tcn ts) = TCons tcn (map (tcSub_type phi) ts) 219 220 tcSub_type phi (TArr t1 t2) = TArr (tcSub_type phi t1) (tcSub_type phi t2) 221 222 223 -- ======================================================-- 224 tcScomp :: Subst -> 225 Subst -> 226 Subst 227 228 tcScomp sub2 sub1 = sub1 ++ sub2 229 230 231 232 -- ======================================================-- 233 tcId_subst :: Subst 234 235 tcId_subst = [] 236 237 238 239 -- ======================================================-- 240 tcDelta :: TVName -> 241 TExpr -> 242 Subst 243 -- all TVar -> TVar substitutions lead downhill 244 tcDelta tvn (TVar tvn2) 245 | tvn == tvn2 = [] 246 | tvn > tvn2 = [(tvn, TVar tvn2)] 247 | tvn < tvn2 = [(tvn2, TVar tvn)] 248 249 tcDelta tvn non_var_texpr = [(tvn, non_var_texpr)] 250 251 252 -- ==========================================================-- 253 -- === 9.42 Unification ===-- 254 -- ==========================================================-- 255 256 -- ======================================================-- 257 tcExtend :: Subst -> 258 TVName -> 259 TExpr -> 260 Reply Subst Message 261 262 tcExtend phi tvn t 263 | t == TVar tvn 264 = Ok phi 265 | tvn `notElem` (tcTvars_in t) 266 = Ok ((tcDelta tvn t) `tcScomp` phi) 267 | otherwise 268 = myFail 269 ( "Type error in source program:\n\n" ++ 270 "Circular substitution:\n " ++ 271 tcShowtExpr (TVar tvn) ++ 272 "\n going to\n" ++ 273 " " ++ 274 tcShowtExpr t ++ 275 "\n") 276 277 278 279 -- ======================================================-- 280 tcUnify :: Subst -> 281 (TExpr, TExpr) -> 282 Reply Subst Message 283 284 tcUnify phi (TVar tvn, t) 285 = if phitvn == TVar tvn 286 then tcExtend phi tvn phit 287 else tcUnify phi (phitvn, phit) 288 where 289 phitvn = tcApply_sub phi tvn 290 phit = tcSub_type phi t 291 292 tcUnify phi (p@(TCons _ _), q@(TVar _)) 293 = tcUnify phi (q, p) 294 295 tcUnify phi (p@(TArr _ _), q@(TVar _)) 296 = tcUnify phi (q, p) 297 298 tcUnify phi (TArr t1 t2, TArr t1' t2') 299 = tcUnifyl phi [(t1, t1'), (t2, t2')] 300 301 tcUnify phi (TCons tcn ts, TCons tcn' ts') 302 | tcn == tcn' 303 = tcUnifyl phi (ts `zip` ts') 304 305 tcUnify phi (t1, t2) 306 = myFail 307 ( "Type error in source program:\n\n" ++ 308 "Cannot unify\n " ++ 309 tcShowtExpr t1 ++ 310 "\n with\n " ++ 311 tcShowtExpr t2 ++ 312 "\n" 313 ) 314 315 316 317 -- ======================================================-- 318 tcUnifyl :: Subst -> 319 [(TExpr, TExpr)] -> 320 Reply Subst Message 321 322 tcUnifyl phi eqns 323 = foldr unify' (Ok phi) eqns 324 where 325 unify' eqn (Ok phi) = tcUnify phi eqn 326 unify' eqn (Fail m) = Fail m 327 328 329 330 -- ==========================================================-- 331 -- === 9.42.2 Merging of substitutions ===-- 332 -- ==========================================================-- 333 334 -- ======================================================-- 335 tcMergeSubs :: Subst -> 336 Subst 337 338 tcMergeSubs phi 339 = if newBinds == [] 340 then unifiedOlds 341 else tcMergeSubs (unifiedOlds ++ newBinds) 342 where 343 (newBinds, unifiedOlds) = tcMergeSubsMain phi 344 345 346 347 -- ======================================================-- 348 tcMergeSubsMain :: Subst -> 349 (Subst, Subst) -- pair of new binds, unified olds 350 351 tcMergeSubsMain phi 352 = (concat newUnifiersChecked, 353 zip oldVars (tcOldUnified newUnifiersChecked oldGroups)) 354 where 355 oldVars = nub (utDomain phi) 356 oldGroups = map (utLookupAll phi) oldVars 357 newUnifiers = map (tcUnifySet tcId_subst) oldGroups 358 newUnifiersChecked = map tcCheckUnifier newUnifiers 359 360 361 362 -- ======================================================-- 363 tcCheckUnifier :: Reply Subst Message -> Subst 364 365 tcCheckUnifier (Ok r) = r 366 tcCheckUnifier (Fail m) 367 = panic ("tcCheckUnifier: " ++ m) 368 369 370 371 -- ======================================================-- 372 tcOldUnified :: [Subst] -> [[TExpr]] -> [TExpr] 373 374 tcOldUnified [] [] = [] 375 tcOldUnified (u:us) (og:ogs) 376 = (tcSub_type u (head og)): tcOldUnified us ogs 377 378 379 -- ==========================================================-- 380 -- === 9.5 Keeping track of types ===-- 381 -- ==========================================================-- 382 383 -- ======================================================-- 384 tcUnknowns_scheme :: TypeScheme -> 385 [TVName] 386 387 tcUnknowns_scheme (Scheme scvs t) = tcTvars_in t `tcBar` scvs 388 389 390 391 -- ======================================================-- 392 tcBar :: (Eq a) => [a] -> 393 [a] -> 394 [a] 395 396 tcBar xs ys = [ x | x <- xs, not (x `elem` ys)] 397 398 399 400 -- ======================================================-- 401 tcSub_scheme :: Subst -> 402 TypeScheme -> 403 TypeScheme 404 405 tcSub_scheme phi (Scheme scvs t) 406 = Scheme scvs (tcSub_type (tcExclude phi scvs) t) 407 where 408 tcExclude phi scvs = [(n,e) | (n,e) <- phi, not (n `elem` scvs)] 409 410 411 412 -- ==========================================================-- 413 -- === 9.53 Association lists ===-- 414 -- ==========================================================-- 415 416 -- ======================================================-- 417 tcCharVal :: AList Naam b -> Naam -> b 418 419 tcCharVal al k 420 = utLookupDef al k (panic ("tcCharVal: no such variable: " ++ k)) 421 422 423 -- ======================================================-- 424 tcUnknowns_te :: TcTypeEnv -> 425 [TVName] 426 427 tcUnknowns_te gamma = concat (map tcUnknowns_scheme (utRange gamma)) 428 429 430 431 -- ======================================================-- 432 tcSub_te :: Subst -> 433 TcTypeEnv -> 434 TcTypeEnv 435 436 tcSub_te phi gamma = [(x, tcSub_scheme phi st) | (x, st) <- gamma] 437 438 439 -- ==========================================================-- 440 -- === 9.6 New variables ===-- 441 -- ==========================================================-- 442 443 -- ======================================================-- 444 tcNext_name :: TypeNameSupply -> 445 TVName 446 447 tcNext_name ns@(f, s) = ns 448 449 450 451 -- ======================================================-- 452 tcDeplete :: TypeNameSupply -> 453 TypeNameSupply 454 455 tcDeplete (f, s) = (f, tcNSSucc s) 456 457 458 459 -- ======================================================-- 460 tcSplit :: TypeNameSupply -> 461 (TypeNameSupply, TypeNameSupply) 462 463 tcSplit (f, s) = ((f2, [0]), (tcNSSucc f2, [0])) 464 where f2 = tcNSDouble f 465 466 467 468 -- ======================================================-- 469 tcName_sequence :: TypeNameSupply -> 470 [TVName] 471 472 tcName_sequence ns = tcNext_name ns: tcName_sequence (tcDeplete ns) 473 474 475 -- ======================================================-- 476 tcNSSucc :: [Int] -> 477 [Int] 478 479 tcNSSucc [] = [1] 480 tcNSSucc (n:ns) | n < tcNSslimit = n+1: ns 481 | otherwise = 0: tcNSSucc ns 482 483 484 -- ======================================================-- 485 tcNSDouble :: [Int] -> 486 [Int] 487 488 tcNSDouble [] = [] 489 tcNSDouble (n:ns) 490 = 2*n': ns' 491 where n' | n > tcNSdlimit = n - tcNSdlimit 492 | otherwise = n 493 ns' | n' == n = tcNSDouble ns 494 | otherwise = tcNSSucc (tcNSDouble ns) 495 496 497 tcNSdlimit :: Int 498 tcNSdlimit = 2^30 499 500 tcNSslimit :: Int 501 tcNSslimit = tcNSdlimit + (tcNSdlimit - 1) 502 503 504 -- ==========================================================-- 505 -- === 9.7 The type-checker ===-- 506 -- ==========================================================-- 507 508 509 -- ======================================================-- 510 tc :: [TypeDef] -> 511 TcTypeEnv -> 512 TypeNameSupply -> 513 CExpr -> 514 Reply TypeInfo Message 515 516 tc tds gamma ns (ENum n) 517 = Ok (tcId_subst, TCons "int" [], (TCons "int" [], ANum n)) 518 519 tc tds gamma ns (EVar x) 520 = tcvar tds gamma ns x 521 522 tc tds gamma ns (EConstr c) 523 = tcvar tds gamma ns c 524 525 tc tds gamma ns (EAp e1 e2) 526 = tcap tds gamma ns e1 e2 527 528 tc tds gamma ns (ELam [] e) 529 = tc tds gamma ns e 530 tc tds gamma ns (ELam [x] e) 531 = tclambda tds gamma ns x e 532 tc tds gamma ns (ELam (x:y:xs) e) 533 = tclambda tds gamma ns x (ELam (y:xs) e) 534 535 tc tds gamma ns (ELet recursive dl e) 536 = if not recursive 537 then tclet tds gamma ns xs es e 538 else tcletrec tds gamma ns xs es e 539 where 540 (xs, es) = unzip2 dl 541 542 tc tds gamma ns (ECase switch alts) 543 = tccase tds gamma ns switch constructors arglists exprs 544 where 545 (constructors, alters) = unzip2 alts 546 (arglists, exprs) = unzip2 alters 547 548 549 -- ==========================================================-- 550 -- === 0.00 Type-checking case-expressions ===-- 551 -- ==========================================================-- 552 553 tcConstrTypeSchemes :: TypeNameSupply -> 554 TypeDef -> 555 (TypeNameSupply, AList Naam TypeScheme) 556 557 tcConstrTypeSchemes ns (tn, stvs, cal) 558 = (finalNameSupply, map2nd enScheme cAltsCurried) 559 where 560 -- associates new type vars with each poly var 561 -- in the type 562 newTVs = tcNewTypeVars (tn, stvs, cal) ns 563 564 -- the actual type variables themselves 565 tVs = map second newTVs 566 567 -- the types of the constructor functions 568 cAltsCurried = map2nd (foldr TArr tdSignature) cAltsXLated 569 cAltsXLated = map2nd (map (tcTDefSubst newTVs)) cal 570 tdSignature = TCons tn (map TVar tVs) 571 enScheme texp = Scheme ((nub.tcTvars_in) texp) texp 572 573 -- the revised name supply 574 finalNameSupply = applyNtimes ( length tVs + 2) tcDeplete ns 575 576 -- apply a function n times to an arg 577 applyNtimes n func arg 578 | n ==0 = arg 579 | otherwise = applyNtimes (n-1) func (func arg) 580 581 582 583 -- ======================================================-- 584 -- 585 tccase :: [TypeDef] -> -- constructor type definitions 586 TcTypeEnv -> -- current type bindings 587 TypeNameSupply -> -- name supply 588 CExpr -> -- switch expression 589 [Naam] -> -- constructors 590 [[Naam]] -> -- argument lists 591 [CExpr] -> -- resulting expressions 592 Reply TypeInfo Message 593 594 595 tccase tds gamma ns sw cs als res 596 -- get the type definition in use, & an association of 597 -- variables therein to type vars & pass 598 -- Also, reorder the argument lists 599 -- and resulting expressions so as to reflect the 600 -- sequence of constructors in the definition 601 = if length tdCNames /= length (nub cs) 602 then myFail 603 "Error in source program: missing alternatives in CASE" 604 else tccase1 tds gamma ns1 sw reOals reOres newTVs tdInUse 605 where 606 tdInUse = tcGetTypeDef tds cs 607 newTVs = tcNewTypeVars tdInUse ns2 608 (ns1, ns2) = tcSplit ns 609 merge = zip cs (zip als res) 610 tdCNames = map first (tcK33 tdInUse) 611 (reOals, reOres) = unzip2 (tcReorder tdCNames merge) 612 613 614 615 -- ======================================================-- 616 -- 617 tcReorder :: [Naam] -> [(Naam,b)] -> [b] 618 619 tcReorder [] uol = [] 620 tcReorder (k:ks) uol 621 = (utLookupDef uol k 622 (myFail 623 ("Error in source program: undeclared constructor '" ++ k ++ 624 "' in CASE") ) ) 625 : tcReorder ks uol 626 627 628 -- ======================================================-- 629 -- Projection functions and similar rubbish. 630 tcDeOksel (Ok x) = x 631 tcDeOksel (Fail m) = panic ("tcDeOkSel: " ++ m) 632 tcOk13sel (Ok (a, b, c)) = a 633 tcOk13sel (Fail m) = panic ("tcOk13sel: " ++ m) 634 tcOk23sel (Ok (a, b, c)) = b 635 tcOk23sel (Fail m) = panic ("tcOk23sel: " ++ m) 636 tcOk33sel (Ok (a, b, c)) = c 637 tcOk33sel (Fail m) = panic ("tcOk33sel: " ++ m) 638 tcK31sel (a, b, c) = a 639 tcK33 (a,b,c) = c 640 641 642 643 -- ======================================================-- 644 -- 645 tccase1 :: [TypeDef] -> 646 TcTypeEnv -> 647 TypeNameSupply -> 648 CExpr -> 649 [[Naam]] -> 650 [CExpr] -> 651 AList Naam TVName -> 652 TypeDef -> 653 Reply TypeInfo Message 654 655 tccase1 tds gamma ns sw reOals reOres newTVs tdInUse 656 -- calculate all the gammas for the RHS's 657 -- call tc for each RHS, so as to gather all the 658 -- sigmas and types for each RHS, then pass on 659 = tccase2 tds gamma ns2 sw reOals newTVs tdInUse rhsTcs 660 where 661 rhsGammas = tcGetAllGammas newTVs (tcK33 tdInUse) reOals 662 rhsTcs = rhsTc1 ns1 rhsGammas reOres 663 rhsTc1 nsl [] [] = [] 664 rhsTc1 nsl (g:gs) (r:rs) 665 = tc tds (g++gamma) nsl1 r : rhsTc1 nsl2 gs rs 666 where (nsl1, nsl2) = tcSplit nsl 667 (ns1, ns2) = tcSplit ns 668 669 670 -- ======================================================-- 671 -- 672 tccase2 :: [TypeDef] -> 673 TcTypeEnv -> 674 TypeNameSupply -> 675 CExpr -> 676 [[Naam]] -> 677 AList Naam TVName -> 678 TypeDef -> 679 [Reply TypeInfo Message] -> 680 Reply TypeInfo Message 681 682 tccase2 tds gamma ns sw reOals newTVs tdInUse rhsTcs 683 -- get the unifiers for T1 to Tk and hence the unifier for all 684 -- type variables in the type definition. Also compute the 685 -- unifier of the result types. 686 = tccase3 tds gamma ns sw reOals newTVs tdInUse rhsTcs 687 phi_1_to_n tau_1_to_n phi_rhs 688 where 689 phi_1_to_n = map tcOk13sel rhsTcs 690 tau_1_to_n = map tcOk23sel rhsTcs 691 phi_rhs = tcDeOksel (tcUnifySet tcId_subst tau_1_to_n) 692 693 694 695 -- ======================================================-- 696 -- 697 tccase3 :: [TypeDef] -> -- tds 698 TcTypeEnv -> -- gamma 699 TypeNameSupply -> -- ns 700 CExpr -> -- sw 701 [[Naam]] -> -- reOals 702 AList Naam TVName -> -- newTVs 703 TypeDef -> -- tdInUse 704 [Reply TypeInfo Message] -> -- rhsTcs 705 [Subst] -> -- phi_1_to_n 706 [TExpr] -> -- tau_1_to_n 707 Subst -> -- phi_rhs 708 Reply TypeInfo Message 709 710 tccase3 tds gamma ns sw reOals newTVs tdInUse rhsTcs 711 phi_1_to_n tau_1_to_n phi_rhs 712 -- make up substitutions for each of the unknown tvars 713 -- merge the substitutions into one 714 -- apply the substitution to the typedef's signature to get the 715 -- most general allowable input type 716 -- call tc to get the type of the switch expression 717 -- check that this is an instance of the deduced input type 718 -- gather the new bindings from the RHSs and switch expression 719 -- return Ok (the big substitution, the result type, gathered bindings) 720 = Ok (phi_Big, tau_final, 721 (tau_final, ACase tree_s 722 (zip tdCNames (zip reOals annotatedRHSs)))) 723 where 724 phi_sTau_sTree_s = tc tds gamma ns sw 725 phi_s = tcOk13sel phi_sTau_sTree_s 726 tau_s = tcOk23sel phi_sTau_sTree_s 727 tree_s = tcOk33sel phi_sTau_sTree_s 728 729 phi = tcMergeSubs (concat phi_1_to_n ++ phi_rhs ++ phi_s) 730 731 tau_lhs = tcSub_type phi tdSignature 732 733 phi_lhs = tcUnify tcId_subst (tau_lhs, tau_s) -- reverse these? 734 735 phi_Big = tcMergeSubs (tcDeOksel phi_lhs ++ phi) 736 737 tau_final = tcSub_type phi_Big (head (map tcOk23sel rhsTcs)) 738 739 annotatedRHSs = map tcOk33sel rhsTcs 740 tVs = map second newTVs 741 tdSignature = TCons (tcK31sel tdInUse) (map TVar tVs) 742 tdCNames = map first (tcK33 tdInUse) 743 744 745 -- ======================================================-- 746 -- 747 tcUnifySet :: Subst -> 748 [TExpr] -> 749 Reply Subst Message 750 751 tcUnifySet sub (e1:[]) = Ok sub 752 tcUnifySet sub (e1:e2:[]) 753 = tcUnify sub (e1, e2) 754 tcUnifySet sub (e1:e2:e3:es) 755 = tcUnifySet newSub (e2:e3:es) 756 where 757 newSub = tcDeOksel (tcUnify sub (e1, e2)) 758 759 760 -- ======================================================-- 761 -- 762 tcNewTypeVars :: TypeDef -> 763 TypeNameSupply -> 764 AList Naam TVName 765 766 tcNewTypeVars (t, vl, c) ns = zip vl (tcName_sequence ns) 767 768 769 770 -- ======================================================-- 771 -- 772 tcGetGammaN :: AList Naam TVName -> 773 ConstrAlt -> 774 [Naam] -> 775 AList Naam TypeScheme 776 777 tcGetGammaN tvl (cname, cal) cparams 778 = zip cparams (map (Scheme [] . tcTDefSubst tvl) cal) 779 780 781 782 -- ======================================================-- 783 -- 784 tcTDefSubst :: AList Naam TVName -> 785 TDefExpr -> 786 TExpr 787 788 tcTDefSubst nameMap (TDefVar n) 789 = f result 790 where 791 f (Just tvn) = TVar tvn 792 f Nothing = TCons n [] 793 result = utLookup nameMap n 794 795 tcTDefSubst nameMap (TDefCons c al) 796 = TCons c (map (tcTDefSubst nameMap) al) 797 798 799 -- ======================================================-- 800 -- 801 tcGetAllGammas :: AList Naam TVName -> 802 [ConstrAlt] -> 803 [[Naam]] -> 804 [AList Naam TypeScheme] 805 806 tcGetAllGammas tvl [] [] = [] 807 -- note param lists cparamss must be ordered in 808 -- accordance with calts 809 tcGetAllGammas tvl (calt:calts) (cparams:cparamss) = 810 tcGetGammaN tvl calt cparams : 811 tcGetAllGammas tvl calts cparamss 812 813 814 -- ======================================================-- 815 -- 816 tcGetTypeDef :: [TypeDef] -> -- type definitions 817 [Naam] -> -- list of constructors used here 818 TypeDef 819 820 tcGetTypeDef tds cs 821 = if length tdefset == 0 822 then myFail "Undeclared constructors in use" 823 else if length tdefset > 1 824 then myFail "CASE expression contains mixed constructors" 825 else head tdefset 826 where 827 tdefset = nub 828 [ (tname, ftvs, cl) | 829 (tname, ftvs, cl) <- tds, 830 usedc <- cs, 831 usedc `elem` (map first cl) ] 832 833 834 -- ==========================================================-- 835 -- === 9.71 Type-checking lists of expressions ===-- 836 -- ==========================================================-- 837 838 -- ======================================================-- 839 -- 840 tcl :: [TypeDef] -> 841 TcTypeEnv -> 842 TypeNameSupply -> 843 [CExpr] -> 844 Reply (Subst, [TExpr], [AnnExpr Naam TExpr]) Message 845 846 tcl tds gamma ns [] 847 = Ok (tcId_subst, [], []) 848 tcl tds gamma ns (e:es) 849 = tcl1 tds gamma ns0 es (tc tds gamma ns1 e) 850 where 851 (ns0, ns1) = tcSplit ns 852 853 854 -- ======================================================-- 855 -- 856 tcl1 tds gamma ns es (Fail m) = Fail m 857 tcl1 tds gamma ns es (Ok (phi, t, annotatedE)) 858 = tcl2 phi t (tcl tds (tcSub_te phi gamma) ns es) annotatedE 859 860 861 -- ======================================================-- 862 -- 863 tcl2 phi t (Fail m) annotatedE = Fail m 864 tcl2 phi t (Ok (psi, ts, annotatedEs)) annotatedE 865 = Ok (psi `tcScomp` phi, (tcSub_type psi t):ts, 866 annotatedE:annotatedEs) 867 868 869 -- ==========================================================-- 870 -- === 9.72 Type-checking variables ===-- 871 -- ==========================================================-- 872 873 -- ======================================================-- 874 -- 875 tcvar :: [TypeDef] -> 876 TcTypeEnv -> 877 TypeNameSupply -> 878 Naam -> 879 Reply TypeInfo Message 880 881 tcvar tds gamma ns x = Ok (tcId_subst, finalType, (finalType, AVar x)) 882 where 883 scheme = tcCharVal gamma x 884 finalType = tcNewinstance ns scheme 885 886 887 -- ======================================================-- 888 -- 889 tcNewinstance :: TypeNameSupply -> 890 TypeScheme -> 891 TExpr 892 893 tcNewinstance ns (Scheme scvs t) = tcSub_type phi t 894 where 895 al = scvs `zip` (tcName_sequence ns) 896 phi = tcAl_to_subst al 897 898 899 -- ======================================================-- 900 -- 901 tcAl_to_subst :: AList TVName TVName -> 902 Subst 903 904 tcAl_to_subst al = map2nd TVar al 905 906 907 -- ==========================================================-- 908 -- === 9.73 Type-checking applications ===-- 909 -- ==========================================================-- 910 911 -- ======================================================-- 912 -- 913 tcap :: [TypeDef] -> 914 TcTypeEnv -> 915 TypeNameSupply -> 916 CExpr -> 917 CExpr -> 918 Reply TypeInfo Message 919 920 tcap tds gamma ns e1 e2 = tcap1 tvn (tcl tds gamma ns' [e1, e2]) 921 where 922 tvn = tcNext_name ns 923 ns' = tcDeplete ns 924 925 926 -- ======================================================-- 927 -- 928 tcap1 tvn (Fail m) 929 = Fail m 930 tcap1 tvn (Ok (phi, [t1, t2], [ae1, ae2])) 931 = tcap2 tvn (tcUnify phi (t1, t2 `TArr` (TVar tvn))) [ae1, ae2] 932 933 934 -- ======================================================-- 935 -- 936 tcap2 tvn (Fail m) [ae1, ae2] 937 = Fail m 938 tcap2 tvn (Ok phi) [ae1, ae2] 939 = Ok (phi, finalType, (finalType, AAp ae1 ae2)) 940 where 941 finalType = tcApply_sub phi tvn 942 943 944 -- ==========================================================-- 945 -- === 9.74 Type-checking lambda abstractions ===-- 946 -- ==========================================================-- 947 948 -- ======================================================-- 949 -- 950 tclambda :: [TypeDef] -> 951 TcTypeEnv -> 952 TypeNameSupply -> 953 Naam -> 954 CExpr -> 955 Reply TypeInfo Message 956 957 tclambda tds gamma ns x e = tclambda1 tvn x (tc tds gamma' ns' e) 958 where 959 ns' = tcDeplete ns 960 gamma' = tcNew_bvar (x, tvn): gamma 961 tvn = tcNext_name ns 962 963 964 -- ======================================================-- 965 -- 966 tclambda1 tvn x (Fail m) = Fail m 967 968 tclambda1 tvn x (Ok (phi, t, annotatedE)) = 969 Ok (phi, finalType, (finalType, ALam [x] annotatedE)) 970 where 971 finalType = (tcApply_sub phi tvn) `TArr` t 972 973 974 -- ======================================================-- 975 -- 976 tcNew_bvar (x, tvn) = (x, Scheme [] (TVar tvn)) 977 978 979 -- ==========================================================-- 980 -- === 9.75 Type-checking let-expressions ===-- 981 -- ==========================================================-- 982 983 -- ======================================================-- 984 -- 985 tclet :: [TypeDef] -> 986 TcTypeEnv -> 987 TypeNameSupply -> 988 [Naam] -> 989 [CExpr] -> 990 CExpr -> 991 Reply TypeInfo Message 992 993 tclet tds gamma ns xs es e 994 = tclet1 tds gamma ns0 xs e rhsTypes 995 where 996 (ns0, ns1) = tcSplit ns 997 rhsTypes = tcl tds gamma ns1 es 998 999 1000 -- ======================================================-- 1001 -- 1002 tclet1 tds gamma ns xs e (Fail m) = Fail m 1003 1004 tclet1 tds gamma ns xs e (Ok (phi, ts, rhsAnnExprs)) 1005 = tclet2 phi xs False (tc tds gamma'' ns1 e) rhsAnnExprs 1006 where 1007 gamma'' = tcAdd_decls gamma' ns0 xs ts 1008 gamma' = tcSub_te phi gamma 1009 (ns0, ns1) = tcSplit ns 1010 1011 1012 -- ======================================================-- 1013 -- 1014 tclet2 phi xs recFlag (Fail m) rhsAnnExprs = Fail m 1015 1016 tclet2 phi xs recFlag (Ok (phi', t, annotatedE)) rhsAnnExprs 1017 = Ok (phi' `tcScomp` phi, t, (t, ALet recFlag (zip xs rhsAnnExprs) annotatedE)) 1018 1019 1020 -- ======================================================-- 1021 -- 1022 tcAdd_decls :: TcTypeEnv -> 1023 TypeNameSupply -> 1024 [Naam] -> 1025 [TExpr] -> 1026 TcTypeEnv 1027 1028 tcAdd_decls gamma ns xs ts = (xs `zip` schemes) ++ gamma 1029 where 1030 schemes = map (tcGenbar unknowns ns) ts 1031 unknowns = tcUnknowns_te gamma 1032 1033 1034 -- ======================================================-- 1035 -- 1036 tcGenbar unknowns ns t = Scheme (map second al) t' 1037 where 1038 al = scvs `zip` (tcName_sequence ns) 1039 scvs = (nub (tcTvars_in t)) `tcBar` unknowns 1040 t' = tcSub_type (tcAl_to_subst al) t 1041 1042 1043 1044 -- ==========================================================-- 1045 -- === 9.76 Type-checking letrec-expressions ===-- 1046 -- ==========================================================-- 1047 1048 -- ======================================================-- 1049 -- 1050 tcletrec :: [TypeDef] -> 1051 TcTypeEnv -> 1052 TypeNameSupply -> 1053 [Naam] -> 1054 [CExpr] -> 1055 CExpr -> 1056 Reply TypeInfo Message 1057 1058 tcletrec tds gamma ns xs es e 1059 = tcletrec1 tds gamma ns0 xs nbvs e 1060 (tcl tds (nbvs ++ gamma) ns1 es) 1061 where 1062 (ns0, ns') = tcSplit ns 1063 (ns1, ns2) = tcSplit ns' 1064 nbvs = tcNew_bvars xs ns2 1065 1066 1067 -- ======================================================-- 1068 -- 1069 tcNew_bvars xs ns = map tcNew_bvar (xs `zip` (tcName_sequence ns)) 1070 1071 1072 1073 -- ======================================================-- 1074 -- 1075 tcletrec1 tds gamma ns xs nbvs e (Fail m) = (Fail m) 1076 1077 tcletrec1 tds gamma ns xs nbvs e (Ok (phi, ts, rhsAnnExprs)) 1078 = tcletrec2 tds gamma' ns xs nbvs' e (tcUnifyl phi (ts `zip` ts')) rhsAnnExprs 1079 where 1080 ts' = map tcOld_bvar nbvs' 1081 nbvs' = tcSub_te phi nbvs 1082 gamma' = tcSub_te phi gamma 1083 1084 1085 -- ======================================================-- 1086 -- 1087 tcOld_bvar (x, Scheme [] t) = t 1088 1089 1090 -- ======================================================-- 1091 -- 1092 tcletrec2 tds gamma ns xs nbvs e (Fail m) rhsAnnExprs = (Fail m) 1093 1094 tcletrec2 tds gamma ns xs nbvs e (Ok phi) rhsAnnExprs 1095 = tclet2 phi xs True (tc tds gamma'' ns1 e) rhsAnnExprs 1096 where 1097 ts = map tcOld_bvar nbvs' 1098 nbvs' = tcSub_te phi nbvs 1099 gamma' = tcSub_te phi gamma 1100 gamma'' = tcAdd_decls gamma' ns0 (map first nbvs) ts 1101 (ns0, ns1) = tcSplit ns 1102 subnames = map first nbvs 1103 1104 1105 -- ==========================================================-- 1106 -- === End TypeCheck5.m (1) ===-- 1107 -- ==========================================================--