ghc/interpreter/preds.c

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