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