ghc/tests/programs/jules_xref/jules_xref.stdin

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