ghc/interpreter/preds.c

   1
   2 /* --------------------------------------------------------------------------
   3  * Part of the type checker dealing with predicates and entailment
   4  *
   5  * Hugs 98 is Copyright (c) Mark P Jones, Alastair Reid and the Yale
   6  * Haskell Group 1994-99, and is distributed as Open Source software
   7  * under the Artistic License; see the file "Artistic" that is included
   8  * in the distribution for details.
   9  *
  10  * $RCSfile: preds.c,v $
  11  * $Revision: 1.5 $
  12  * $Date: 1999/04/27 10:06:59 $
  13  * ------------------------------------------------------------------------*/
  14
  15 /* --------------------------------------------------------------------------
  16  * Local function prototypes:
  17  * ------------------------------------------------------------------------*/
  18
  19 static Cell   local assumeEvid        Args((Cell,Int));
  20 static List   local makePredAss       Args((List,Int));
  21 static List   local copyPreds         Args((List));
  22 static Void   local qualify           Args((List,Cell));
  23 static Void   local qualifyBinding    Args((List,Cell));
  24 static Cell   local qualifyExpr       Args((Int,List,Cell));
  25 static Void   local overEvid          Args((Cell,Cell));
  26
  27 static Void   local cutoffExceeded    Args((Cell,Int,Cell,Int,List));
  28 static Cell   local scFind            Args((Cell,Cell,Int,Cell,Int,Int));
  29 static Cell   local scEntail          Args((List,Cell,Int,Int));
  30 static Cell   local entail            Args((List,Cell,Int,Int));
  31 static Cell   local inEntail          Args((List,Cell,Int,Int));
  32 #if TREX
  33 static Cell   local lacksNorm         Args((Type,Int,Cell));
  34 #endif
  35
  36 static List   local scSimplify        Args((List));
  37 static Void   local elimTauts         Args((Void));
  38 static Bool   local anyGenerics       Args((Type,Int));
  39 static List   local elimOuterPreds    Args((List));
  40 static List   local elimPredsUsing    Args((List,List));
  41 static Void   local reducePreds       Args((Void));
  42 static Void   local normPreds         Args((Int));
  43
  44 static Bool   local resolveDefs       Args((List));
  45 static Bool   local resolveVar        Args((Int));
  46 static Class  local classConstraining Args((Int,Cell,Int));
  47
  48 /* --------------------------------------------------------------------------
  49  * Predicate assignments:
  50  *
  51  * A predicate assignment is represented by a list of triples (pi,o,ev)
  52  * where o is the offset for types in pi, with evidence required at the
  53  * node pointed to by ev (which is taken as a dictionary parameter if
  54  * no other evidence is available).  Note that the ev node will be
  55  * overwritten at a later stage if evidence for that predicate is found
  56  * subsequently.
  57  * ------------------------------------------------------------------------*/
  58
  59 static List preds;                      /* Current predicate assignment    */
  60
  61 static Cell local assumeEvid(pi,o)      /* Add predicate pi (offset o) to  */
  62 Cell pi;                                /* preds with new dict var nd      */
  63 Int  o; {
  64     Cell nd = inventDictVar();
  65     preds   = cons(triple(pi,mkInt(o),nd),preds);
  66     return nd;
  67 }
  68
  69 static List local makePredAss(qs,o)     /* Make list of predicate assumps. */
  70 List qs;                                /* from qs (offset o), w/ new dict */
  71 Int  o; {                               /* vars for each predicate         */
  72     List result = NIL;
  73     for (; nonNull(qs); qs=tl(qs))
  74         result = cons(triple(hd(qs),mkInt(o),inventDictVar()),result);
  75     return rev(result);
  76 }
  77
  78 static List local copyPreds(qs)         /* Copy list of predicates         */
  79 List qs; {
  80     List result = NIL;
  81     for (; nonNull(qs); qs=tl(qs)) {
  82         Cell pi = hd(qs);
  83         result  = cons(copyPred(fst3(pi),intOf(snd3(pi))),result);
  84     }
  85     return rev(result);
  86 }
  87
  88 static Void local qualify(qs,alt)       /* Add extra dictionary args to    */
  89 List qs;                                /* qualify alt by predicates in qs */
  90 Cell alt; {                             /* :: ([Pat],Rhs)                  */
  91     List ds;
  92     for (ds=NIL; nonNull(qs); qs=tl(qs))
  93         ds = cons(thd3(hd(qs)),ds);
  94     fst(alt) = revOnto(ds,fst(alt));
  95 }
  96
  97 static Void local qualifyBinding(qs,b)  /* Add extra dict args to each     */
  98 List qs;                                /* alternative in function binding */
  99 Cell b ; {
 100     if (!isVar(fst(b)))                 /* check for function binding      */
 101         internal("qualifyBinding");
 102     map1Proc(qualify,qs,snd(snd(b)));
 103 }
 104
 105 static Cell local qualifyExpr(l,ps,e)   /* Add dictionary params to expr   */
 106 Int  l;
 107 List ps;
 108 Cell e; {
 109     if (nonNull(ps)) {                  /* Qualify input expression with   */
 110         if (whatIs(e)!=LAMBDA)          /* additional dictionary params    */
 111             e = ap(LAMBDA,pair(NIL,pair(mkInt(l),e)));
 112         qualify(ps,snd(e));
 113     }
 114     return e;
 115 }
 116
 117 static Void local overEvid(dv,ev)       /* Overwrite dict var dv with      */
 118 Cell dv;                                /* evidence ev                     */
 119 Cell ev; {
 120     fst(dv) = nameInd;
 121     snd(dv) = ev;
 122 }
 123
 124 /* --------------------------------------------------------------------------
 125  * Predicate entailment:
 126  *
 127  * Entailment plays a prominent role in the theory of qualified types, and
 128  * so, unsurprisingly, in the implementation too.  For practical reasons,
 129  * we break down entailment into two pieces.  The first, scEntail, uses
 130  * only the information provided by class declarations, while the second,
 131  * entail, also uses the information in instance declarations.
 132  *
 133  * scEntail uses the following auxiliary function to do its work:
 134  *
 135  *   scFind (e : pi') pi : Find evidence for predicate pi using only
 136  *                           equality of predicates, superclass entailment,
 137  *                           and the evidence e for pi'.
 138  *
 139  *   scFind (e : pi') pi =
 140  *
 141  *      if pi = pi' then
 142  *          return e
 143  *
 144  *      if (pi.class.level < pi'.class.level)
 145  *          get superclass entailment pi' ||- P
 146  *          for each (sc, pi0) in P
 147  *              if (ev := scFind (sc e : pi0) pi) /= NIL
 148  *                  return ev
 149  *
 150  *      return NIL
 151  *
 152  * This code assumes that the class hierarchy is acyclic, and that
 153  * each class has been assigned a `level', which is its height in
 154  * the hierachy.  The first of the assumptions guarantees that the
 155  * algorithm will terminate.  The comparison of levels is an
 156  * optimization that cuts down the search space: given that superclass
 157  * entailments can only be used to descend the hierarchy, there is no
 158  * way we can reach a higher level than the one that we start with,
 159  * and hence there is no point in looking if we reach such a position.
 160  *
 161  * scEntail extends scFind to work on whole predicate assignments:
 162  *
 163  *   scEntail P pi : Find evidence for predicate pi using the evidence
 164  *                   provided by the predicate assignment P, and using
 165  *                   only superclass entailments.
 166  *
 167  *   scEntail P pi =
 168  *
 169  *       for each (v:pi') in P
 170  *           if (ev := scFind (v:pi') pi) /= NIL
 171  *               return ev;
 172  *       return NIL
 173  *
 174  * ------------------------------------------------------------------------*/
 175
 176 Int cutoff = 16;                        /* Used to limit depth of recursion*/
 177
 178 static Void local cutoffExceeded(pi,o,pi1,o1,ps)
 179 Cell pi, pi1;                           /* Display error msg when cutoff   */
 180 Int  o,  o1;
 181 List ps; {
 182     clearMarks();
 183     ERRMSG(0)
 184         "\n*** The type checker has reached the cutoff limit while trying to\n"
 185     ETHEN ERRTEXT
 186         "*** determine whether:\n***     "     ETHEN ERRPRED(copyPred(pi,o));
 187     ps = (isNull(pi1)) ? copyPreds(ps) : singleton(copyPred(pi1,o1));
 188     ERRTEXT
 189         "\n*** can be deduced from:\n***     " ETHEN ERRCONTEXT(ps);
 190     ERRTEXT
 191         "\n*** This may indicate that the problem is undecidable.  However,\n"
 192     ETHEN ERRTEXT
 193         "*** you may still try to increase the cutoff limit using the -c\n"
 194     ETHEN ERRTEXT
 195         "*** option and then try again.  (The current setting is -c%d)\n",
 196         cutoff
 197     EEND;
 198 }
 199
 200 static Cell local scFind(e,pi1,o1,pi,o,d)/* Use superclass entailment to   */
 201 Cell e;                                 /* find evidence for (pi,o) using  */
 202 Cell pi1;                               /* the evidence e for (pi1,o1).    */
 203 Int  o1;
 204 Cell pi;
 205 Int  o;
 206 Int  d; {
 207     Class h1 = getHead(pi1);
 208     Class h  = getHead(pi);
 209
 210     if (h==h1 && samePred(pi1,o1,pi,o))
 211         return e;
 212
 213     if (isClass(h1) && (!isClass(h) || cclass(h).level<cclass(h1).level)) {
 214         Int  beta  = newKindedVars(cclass(h1).kinds);
 215         List scs   = cclass(h1).supers;
 216         List dsels = cclass(h1).dsels;
 217         if (!matchPred(pi1,o1,cclass(h1).head,beta))
 218             internal("scFind");
 219
 220         if (d++ >= cutoff)
 221             cutoffExceeded(pi,o,pi1,o1,NIL);
 222
 223         for (; nonNull(scs); scs=tl(scs), dsels=tl(dsels)) {
 224             Cell ev = scFind(ap(hd(dsels),e),hd(scs),beta,pi,o,d);
 225             if (nonNull(ev))
 226                 return ev;
 227         }
 228     }
 229
 230     return NIL;
 231 }
 232
 233 static Cell local scEntail(ps,pi,o,d)   /* Calc evidence for (pi,o) from ps*/
 234 List ps;                                /* Using superclasses and equality.*/
 235 Cell pi;
 236 Int  o;
 237 Int  d; {
 238     for (; nonNull(ps); ps=tl(ps)) {
 239         Cell pi1 = hd(ps);
 240         Cell ev  = scFind(thd3(pi1),fst3(pi1),intOf(snd3(pi1)),pi,o,d);
 241         if (nonNull(ev))
 242             return ev;
 243     }
 244     return NIL;
 245 }
 246
 247 /* --------------------------------------------------------------------------
 248  * Now we reach the main entailment routine:
 249  *
 250  *   entail P pi : Find evidence for predicate pi using the evidence
 251  *                 provided by the predicate assignment P.
 252  *
 253  *   entail P pi =
 254  *
 255  *       if (ev := scEntail P pi) /= NIL
 256  *           return ev;
 257  *
 258  *       if there is an instance entailment i : Q ||- pi
 259  *           for each pi' in Q
 260  *               if (ev := entail P pi') /= NIL
 261  *                   i := ap(i,ev)
 262  *               else
 263  *                   return NIL
 264  *           return i
 265  *
 266  *       return NIL;
 267  *
 268  * The form of evidence expressions produced by scEntail can be described
 269  * by the grammar:
 270  *
 271  *    e  =  v  |  sc e            (v = evidence var, sc = superclass sel)
 272  *
 273  * while entail extends this to include dictionary expressions given by:
 274  *
 275  *    d  =  e  |  mki d1 ... dn   (mki = dictionary constructor)
 276  *
 277  * A full grammar for evidence expressions is:
 278  *
 279  *    d   =   v   |   sc d   |   mki d1 ... dn
 280  *
 281  * and this includes evidence expressions of the form  sc (mki d1 ... dn)
 282  * that can never be produced by either of the entail functions described
 283  * above.  This is good, from a practical perspective, because t means
 284  * that we won't waste effort building a dictionary (mki d1 ... dn) only
 285  * to extract just one superclass component and throw the rest away.
 286  * Moreover, conditions on instance decls already guarantee that any
 287  * expression of this form can be rewritten in the form  mki' d1' ... dn'.
 288  * (Minor point: they don't guarantee that such rewritings will lead to
 289  * smaller terms, and hence to termination.  However, we have already
 290  * accepted the benefits of an undecidable entailment relation over
 291  * guarantees of termination, and this additional quirk is unlikely
 292  * to cause any further concern, except in pathological cases.)
 293  * ------------------------------------------------------------------------*/
 294
 295 static Cell local entail(ps,pi,o,d)     /* Calc evidence for (pi,o) from ps*/
 296 List ps;                                /* Uses superclasses, equality,    */
 297 Cell pi;                                /* tautology, and construction     */
 298 Int  o;
 299 Int  d; {
 300     Cell ev = scEntail(ps,pi,o,d);
 301     return nonNull(ev) ? ev : inEntail(ps,pi,o,d);
 302 }
 303
 304 static Cell local inEntail(ps,pi,o,d)   /* Calc evidence for (pi,o) from ps*/
 305 List ps;                                /* using a top-level instance      */
 306 Cell pi;                                /* entailment                      */
 307 Int  o;
 308 Int  d; {
 309 #if TREX
 310     if (isAp(pi) && isExt(fun(pi))) {   /* Lacks predicates                */
 311         Cell e  = fun(pi);
 312         Cell l;
 313         l  = lacksNorm(arg(pi),o,e);
 314         if (isNull(l) || isInt(l))
 315             return l;
 316         else {
 317             List qs = ps;
 318             for (; nonNull(qs); qs=tl(qs)) {
 319                 Cell qi = fst3(hd(qs));
 320                 if (isAp(qi) && fun(qi)==e) {
 321                     Cell lq = lacksNorm(arg(qi),intOf(snd3(hd(qs))),e);
 322                     if (isAp(lq) && intOf(fst(l))==intOf(fst(lq))) {
 323                         Int f = intOf(snd(l)) - intOf(snd(lq));
 324                         return (f==0) ? thd3(hd(qs)) : ap2(nameAddEv,
 325                                                            mkInt(f),
 326                                                            thd3(hd(qs)));
 327                     }
 328                 }
 329             }
 330             return NIL;
 331         }
 332     }
 333     else {
 334 #endif
 335     Inst in = findInstFor(pi,o);        /* Class predicates                */
 336
 337     if (nonNull(in)) {
 338         Int  beta = typeOff;
 339         Cell e    = inst(in).builder;
 340         Cell es   = inst(in).specifics;
 341         if (d++ >= cutoff)
 342             cutoffExceeded(pi,o,NIL,0,ps);
 343         for (; nonNull(es); es=tl(es)) {
 344             Cell ev = entail(ps,hd(es),beta,d);
 345             if (nonNull(ev))
 346                 e = ap(e,ev);
 347             else
 348                 return NIL;
 349         }
 350         return e;
 351     }
 352     return NIL;
 353 #if TREX
 354     }
 355 #endif
 356 }
 357
 358 Cell provePred(ks,ps,pi)                /* Find evidence for predicate pi  */
 359 Kinds ks;                               /* assuming ps.  If ps is null,    */
 360 List  ps;                               /* then we get to decide whether   */
 361 Cell  pi; {                             /* is tautological, and we can use */
 362     Int  beta;                          /* the evidence as a dictionary.   */
 363     Cell ev;
 364     emptySubstitution();
 365     beta = newKindedVars(ks);           /* (ks provides kinds for any      */
 366     ps   = makePredAss(ps,beta);        /*  vars that appear in pi.)       */
 367     ev   = entail(ps,pi,beta,0);
 368     emptySubstitution();
 369     return ev;
 370 }
 371
 372 #if TREX
 373 static Cell local lacksNorm(t,o,e)      /* Normalize lacks pred (t,o)\l    */
 374 Type t;                                 /* returning NIL (unsatisfiable),  */
 375 Int  o;                                 /* Int (tautological) or pair (v,a)*/
 376 Cell e; {                               /* such that, if e is evid for v\l,*/
 377     Text l = extText(e);                /* then (e+a) is evid for (t,o)\l. */
 378     Int  a = 0;
 379     for (;;) {
 380         Tyvar *tyv;
 381         deRef(tyv,t,o);
 382         if (tyv)
 383             return pair(mkInt(tyvNum(tyv)),mkInt(a));
 384         else {
 385             Cell h = getDerefHead(t,o);
 386             if (h==typeNoRow && argCount==0)
 387                 return mkInt(a);
 388             else if (isExt(h) && argCount==2) {
 389                 Text l1 = extText(h);
 390                 if (l1==l)
 391                     return NIL;
 392                 else if (strcmp(textToStr(l1),textToStr(l))<0)
 393                     a++;
 394                 t = arg(t);
 395             }
 396             else
 397                 return NIL;
 398         }
 399     }
 400 }
 401 #endif
 402
 403 /* --------------------------------------------------------------------------
 404  * Predicate set Simplification:
 405  *
 406  * Calculate a minimal equivalent subset of a given set of predicates.
 407  * ------------------------------------------------------------------------*/
 408
 409 static List local scSimplify(qs)        /* Simplify predicates in qs,      */
 410 List qs; {                              /* returning equiv minimal subset  */
 411     Int n = length(qs);
 412
 413     while (0<n--) {
 414         Cell pi = hd(qs);
 415         Cell ev = scEntail(tl(qs),fst3(pi),intOf(snd3(pi)),0);
 416         if (nonNull(ev)) {
 417             overEvid(thd3(pi),ev);      /* Overwrite dict var with evidence*/
 418             qs      = tl(qs);           /* ... and discard predicate       */
 419         }
 420         else {                          /* Otherwise, retain predicate     */
 421             Cell tmp = tl(qs);
 422             tl(qs)   = NIL;
 423             qs       = appendOnto(tmp,qs);
 424         }
 425     }
 426     return qs;
 427 }
 428
 429 List simpleContext(ps,o)                /* Simplify context of skeletons   */
 430 List ps;                                /* skeletons, offset o, using      */
 431 Int  o; {                               /* superclass hierarchy            */
 432     return copyPreds(scSimplify(makePredAss(ps,o)));
 433 }
 434
 435 /* --------------------------------------------------------------------------
 436  * Context splitting --- tautological and locally tautological predicates:
 437  * ------------------------------------------------------------------------*/
 438
 439 static Void local elimTauts() {         /* Remove tautological constraints */
 440     if (haskell98) {                    /* from preds                      */
 441         reducePreds();                  /* (or context reduce for Hask98)  */
 442     } else {
 443         List ps = preds;
 444         preds   = NIL;
 445         while (nonNull(ps)) {
 446             Cell pi = hd(ps);
 447             Cell ev = entail(NIL,fst3(pi),intOf(snd3(pi)),0);
 448             if (nonNull(ev)) {
 449                 overEvid(thd3(pi),ev);
 450                 ps = tl(ps);
 451             }
 452             else {
 453                 List tmp = tl(ps);
 454                 tl(ps)   = preds;
 455                 preds    = ps;
 456                 ps           = tmp;
 457             }
 458         }
 459     }
 460 }
 461
 462 static Int numFixedVars = 0;            /* Number of fixed vars found      */
 463
 464 static Bool local anyGenerics(t,o)      /* Test for generic vars, and count*/
 465 Type t;                                 /* fixed variables                 */
 466 Int  o; {
 467     Type h = getDerefHead(t,o);         /* This code is careful to expand  */
 468     Int  a = argCount;                  /* synonyms; mark* & copy* do not. */
 469     if (isSynonym(h) && a>=tycon(h).arity) {
 470         expandSyn(h,a,&t,&o);
 471         return anyGenerics(t,o);
 472     }
 473     else {
 474         Tyvar* tyv;
 475         for (; 0<a--; t=fun(t)) {       /* cycle through any arguments     */
 476             deRef(tyv,t,o);
 477             if (anyGenerics(arg(t),o))
 478                 return TRUE;
 479         }
 480         deRef(tyv,t,o);
 481         if (tyv) {
 482             if (tyv->offs == FIXED_TYVAR) {
 483                 numFixedVars++;
 484                 return FALSE;
 485             }
 486             else
 487                 return TRUE;
 488         }
 489         else
 490             return FALSE;
 491     }
 492 }
 493
 494 static List local elimOuterPreds(sps)   /* Simplify and defer any remaining*/
 495 List sps; {                             /* preds that contain no generics. */
 496     List qs = NIL;
 497     elimTauts();
 498     for (preds=scSimplify(preds); nonNull(preds); ) {
 499         Cell pi = hd(preds);
 500         Cell nx = tl(preds);
 501         if (anyGenerics(fst3(pi),intOf(snd3(pi)))) {    /* Retain predicate*/
 502             tl(preds) = qs;
 503             qs        = preds;
 504         }
 505         else {                                          /* Defer predicate */
 506             tl(preds) = sps;
 507             sps       = preds;
 508         }
 509         preds = nx;
 510     }
 511     preds = qs;
 512     return sps;
 513 }
 514
 515 static List local elimPredsUsing(ps,sps)/* Try to discharge or defer preds,*/
 516 List ps;                                /* splitting if necessary to match */
 517 List sps; {                             /* context ps.  sps = savePreds.   */
 518     List rems = NIL;
 519     while (nonNull(preds)) {            /* Pick a predicate from preds     */
 520         Cell p  = preds;
 521         Cell pi = fst3(hd(p));
 522         Int  o  = intOf(snd3(hd(p)));
 523         Cell ev = entail(ps,pi,o,0);
 524         preds   = tl(preds);
 525
 526         if (nonNull(ev))                /* Discharge if ps ||- (pi,o)      */
 527             overEvid(thd3(hd(p)),ev);
 528         else if (!anyGenerics(pi,o)) {  /* Defer if no generics            */
 529             tl(p) = sps;
 530             sps   = p;
 531         }
 532         else {                          /* Try to split generics and fixed */
 533             Inst in;
 534             if (numFixedVars>0 && nonNull(in=findInstFor(pi,o))) {
 535                 List qs = inst(in).specifics;
 536                 for (ev=inst(in).builder; nonNull(qs); qs=tl(qs))
 537                     ev = ap(ev,assumeEvid(hd(qs),typeOff));
 538                 overEvid(thd3(hd(p)),ev);
 539             }
 540             else {                      /* No worthwhile progress possible */
 541                 tl(p) = rems;
 542                 rems  = p;
 543             }
 544         }
 545     }
 546     preds = rems;                       /* Return any remaining predicates */
 547     return sps;
 548 }
 549
 550 static Void local reducePreds() {       /* Context reduce predicates: uggh!*/
 551     List rems = NIL;                    /* (A last resort for defaulting)  */
 552     while (nonNull(preds)) {            /* Pick a predicate from preds     */
 553         Cell p  = preds;
 554         Cell pi = fst3(hd(p));
 555         Int  o  = intOf(snd3(hd(p)));
 556         Inst in = findInstFor(pi,o);
 557         preds   = tl(preds);
 558         if (nonNull(in)) {
 559             List qs = inst(in).specifics;
 560             Cell ev = inst(in).builder;
 561             for (; nonNull(qs); qs=tl(qs))
 562                 ev = ap(ev,assumeEvid(hd(qs),typeOff));
 563             overEvid(thd3(hd(p)),ev);
 564         }
 565         else {                          /* No worthwhile progress possible */
 566             tl(p) = rems;
 567             rems  = p;
 568         }
 569     }
 570     preds = scSimplify(rems);           /* Return any remaining predicates */
 571 }
 572
 573 static Void local normPreds(line)       /* Normalize each element of preds */
 574 Int line; {                             /* in some appropriate manner      */
 575 #if TREX
 576     List ps = preds;
 577     List pr = NIL;
 578     while (nonNull(ps)) {
 579         Cell pi = fst3(hd(ps));
 580         Cell ev = thd3(hd(ps));
 581         if (isAp(pi) && isExt(fun(pi))) {
 582             Cell r = lacksNorm(arg(pi),intOf(snd3(hd(ps))),fun(pi));
 583             if (isNull(r)) {
 584                 ERRMSG(line) "Cannot satisfy constraint " ETHEN
 585                 ERRPRED(copyPred(pi,intOf(snd3(hd(ps)))));
 586                 ERRTEXT      "\n"
 587                 EEND;
 588             }
 589             else if (isInt(r)) {
 590                 overEvid(ev,r);
 591                 ps = tl(ps);
 592                 if (isNull(pr))
 593                     preds  = ps;
 594                 else
 595                     tl(pr) = ps;
 596             }
 597             else if (intOf(snd(r))!=0) {
 598                 Cell nd  = inventDictVar();
 599                 Cell ev1 = ap2(nameAddEv,snd(r),nd);
 600                 pi       = ap(fun(pi),aVar);
 601                 hd(ps)   = triple(pi,fst(r),nd);
 602                 overEvid(ev,ev1);
 603                 pr       = ps;
 604                 ps       = tl(ps);
 605             }
 606             else {
 607                 fst3(hd(ps)) = ap(fun(pi),fst(r));
 608                 pr = ps;
 609                 ps = tl(ps);
 610             }
 611         }
 612         else {
 613             pr = ps;
 614             ps = tl(ps);
 615         }
 616     }
 617 #endif
 618 }
 619
 620 /* --------------------------------------------------------------------------
 621  * Mechanisms for dealing with defaults:
 622  * ------------------------------------------------------------------------*/
 623
 624 static Bool local resolveDefs(vs)       /* Attempt to resolve defaults  */
 625 List vs; {                              /* for variables vs subject to  */
 626     List pvs       = NIL;               /* constraints in preds         */
 627     List qs        = preds;
 628     Bool defaulted = FALSE;
 629
 630 #ifdef DEBUG_DEFAULTS
 631     Printf("Attempt to resolve variables ");
 632     printExp(stdout,vs);
 633     Printf(" with context ");
 634     printContext(stdout,copyPreds(preds));
 635     Printf("\n");
 636 #endif
 637
 638     resetGenerics();                    /* find type variables in ps    */
 639     for (; nonNull(qs); qs=tl(qs)) {
 640         Cell pi = fst3(hd(qs));
 641         Int  o  = intOf(snd3(hd(qs)));
 642         for (; isAp(pi); pi=fun(pi))
 643             pvs = genvarType(arg(pi),o,pvs);
 644     }
 645
 646     for (; nonNull(pvs); pvs=tl(pvs)) { /* now try defaults             */
 647         Int vn = intOf(hd(pvs));
 648
 649 #ifdef DEBUG_DEFAULTS
 650         Printf("is var %d included in ",vn);
 651         printExp(stdout,vs);
 652         Printf("?\n");
 653 #endif
 654
 655         if (!intIsMember(vn,vs))
 656             defaulted |= resolveVar(vn);
 657 #ifdef DEBUG_DEFAULTS
 658         else
 659             Printf("Yes, so no ambiguity!\n");
 660 #endif
 661     }
 662
 663     return defaulted;
 664 }
 665
 666 static Bool local resolveVar(vn)        /* Determine whether an ambig.  */
 667 Int  vn; {                              /* variable vn can be resolved  */
 668     List ps        = preds;             /* by default in the context of */
 669     List cs        = NIL;               /* the predicates in ps         */
 670     Bool aNumClass = FALSE;
 671
 672     if (tyvar(vn)->bound == SKOLEM)
 673         return FALSE;
 674
 675     /* According to the Haskell definition, we can only default an ambiguous
 676      * variable if the set of classes that constrain it:
 677      *   (a) includes at least one numeric class.
 678      *   (b) includes only numeric or standard classes.
 679      * In addition, we will not allow a variable to be defaulted unless it
 680      * appears only in predicates of the form (Class var).
 681      */
 682
 683 #ifdef DEBUG_DEFAULTS
 684     Printf("Trying to default variable %d\n",vn);
 685 #endif
 686
 687     for (; nonNull(ps); ps=tl(ps)) {
 688         Cell  pi = hd(ps);
 689         Class c  = classConstraining(vn,fst3(pi),intOf(snd3(pi)));
 690         if (nonNull(c)) {
 691             if (c==classRealFrac   || c==classRealFloat ||
 692                 c==classFractional || c==classFloating  ||
 693                 c==classReal       || c==classIntegral  || c==classNum)
 694                 aNumClass = TRUE;
 695             else if (c!=classEq    && c!=classOrd  && c!=classShow &&
 696                      c!=classRead  && c!=classIx   && c!=classEnum &&
 697                      c!=classBounded)
 698                 return FALSE;
 699
 700             {   Type  t = arg(fst3(pi));/* Check for single var as arg     */
 701                 Int   o = intOf(snd3(pi));
 702                 Tyvar *tyv;
 703                 deRef(tyv,t,o);
 704                 if (!tyv || tyvNum(tyv)!=vn)
 705                     return FALSE;
 706             }
 707             if (!cellIsMember(c,cs))
 708                 cs = cons(c,cs);
 709         }
 710     }
 711
 712     /* Now find the first class (if any) in the list of defaults that
 713      * is an instance of all of the required classes.
 714      *
 715      * If we get this far, then cs only mentions classes from the list
 716      * above, all of which have only a single parameter of kind *.
 717      */
 718
 719     if (aNumClass) {
 720         List ds = defaultDefns;         /* N.B. guaranteed to be monotypes */
 721 #ifdef DEBUG_DEFAULTS
 722         Printf("Default conditions met, looking for type\n");
 723 #endif
 724         for (; nonNull(ds); ds=tl(ds)) {
 725             List cs1 = cs;
 726             while (nonNull(cs1) && nonNull(entail(NIL,ap(hd(cs1),hd(ds)),0,0)))
 727                 cs1 = tl(cs1);
 728             if (isNull(cs1)) {
 729                 bindTv(vn,hd(ds),0);
 730 #ifdef DEBUG_DEFAULTS
 731                 Printf("Default type for variable %d is ",vn);
 732                 printType(stdout,hd(ds));
 733                 Printf("\n");
 734 #endif
 735                 return TRUE;
 736             }
 737         }
 738     }
 739
 740 #ifdef DEBUG_DEFAULTS
 741     Printf("No default permitted/found\n");
 742 #endif
 743     return FALSE;
 744 }
 745
 746 static Class local classConstraining(vn,pi,o)
 747 Int  vn;                                /* Return class constraining var*/
 748 Cell pi;                                /* vn in predicate pi, or NIL if*/
 749 Int  o; {                               /* vn is not involved           */
 750     for (; isAp(pi); pi=fun(pi))
 751         if (!doesntOccurIn(tyvar(vn),arg(pi),o))
 752             return getHead(pi);
 753     return NIL;
 754 }
 755
 756 /*-------------------------------------------------------------------------*/