X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Finterpreter%2Fpreds.c;h=7c5a7a848bf75bd70502ceed2cb645eef0b0cae0;hb=fe69f3c1d6062b90635963aa414c33951bf18427;hp=c159bb293196a74bc553881dff5f1564954e40de;hpb=ecd09ad02c4ef8e28eebef72cf6f99ab47059a5e;p=ghc-hetmet.git diff --git a/ghc/interpreter/preds.c b/ghc/interpreter/preds.c index c159bb2..7c5a7a8 100644 --- a/ghc/interpreter/preds.c +++ b/ghc/interpreter/preds.c @@ -9,42 +9,51 @@ * included in the distribution. * * $RCSfile: preds.c,v $ - * $Revision: 1.6 $ - * $Date: 1999/10/15 21:40:54 $ + * $Revision: 1.11 $ + * $Date: 2000/03/13 11:37:16 $ * ------------------------------------------------------------------------*/ /* -------------------------------------------------------------------------- * Local function prototypes: * ------------------------------------------------------------------------*/ -static Cell local assumeEvid Args((Cell,Int)); -static List local makePredAss Args((List,Int)); -static List local copyPreds Args((List)); -static Void local qualify Args((List,Cell)); -static Void local qualifyBinding Args((List,Cell)); -static Cell local qualifyExpr Args((Int,List,Cell)); -static Void local overEvid Args((Cell,Cell)); - -static Void local cutoffExceeded Args((Cell,Int,Cell,Int,List)); -static Cell local scFind Args((Cell,Cell,Int,Cell,Int,Int)); -static Cell local scEntail Args((List,Cell,Int,Int)); -static Cell local entail Args((List,Cell,Int,Int)); -static Cell local inEntail Args((List,Cell,Int,Int)); +static Cell local assumeEvid ( Cell,Int ); +#if IPARAM +static Cell local findIPEvid ( Text ); +static Void local removeIPEvid ( Text ); +#endif +static List local makePredAss ( List,Int ); +static List local copyPreds ( List ); +static Void local qualify ( List,Cell ); +static Void local qualifyBinding ( List,Cell ); +static Cell local qualifyExpr ( Int,List,Cell ); +static Void local overEvid ( Cell,Cell ); + +static Void local cutoffExceeded ( Cell,Int,List ); +static Cell local scFind ( Cell,Cell,Int,Cell,Int,Int ); +static Cell local scEntail ( List,Cell,Int,Int ); +static Cell local entail ( List,Cell,Int,Int ); +static Cell local inEntail ( List,Cell,Int,Int ); +#if MULTI_INST +static Cell local inEntails ( List,Cell,Int,Int ); +static Bool local instCompare ( Inst, Inst ); +#endif #if TREX -static Cell local lacksNorm Args((Type,Int,Cell)); +static Cell local lacksNorm ( Type,Int,Cell ); #endif -static List local scSimplify Args((List)); -static Void local elimTauts Args((Void)); -static Bool local anyGenerics Args((Type,Int)); -static List local elimOuterPreds Args((List)); -static List local elimPredsUsing Args((List,List)); -static Void local reducePreds Args((Void)); -static Void local normPreds Args((Int)); +static List local scSimplify ( List ); +static Void local elimTauts ( Void ); +static Bool local anyGenerics ( Type,Int ); +static List local elimOuterPreds ( List ); +static List local elimPredsUsing ( List,List ); +static Void local reducePreds ( Void ); +static Void local normPreds ( Int ); -static Bool local resolveDefs Args((List)); -static Bool local resolveVar Args((Int)); -static Class local classConstraining Args((Int,Cell,Int)); +static Bool local resolveDefs ( List ); +static Bool local resolveVar ( Int ); +static Class local classConstraining ( Int,Cell,Int ); +static Bool local instComp_ ( Inst,Inst ); /* -------------------------------------------------------------------------- * Predicate assignments: @@ -67,6 +76,33 @@ Int o; { return nd; } +#if IPARAM +static Cell local findIPEvid(t) +Text t; { + List ps = preds; + for (; nonNull(ps); ps=tl(ps)) { + Cell p = hd(ps); + if (ipMatch(fst3(p), t)) + return p; + } + return NIL; +} + +static Void local removeIPEvid(t) +Text t; { + List ps = preds; + List *prev = &preds; + for (; nonNull(ps); ps = tl(ps)) + if (ipMatch(fst3(hd(ps)), t)) { + *prev = tl(ps); + return; + } else { + prev = &tl(ps); + } +} +#endif + + static List local makePredAss(qs,o) /* Make list of predicate assumps. */ List qs; /* from qs (offset o), w/ new dict */ Int o; { /* vars for each predicate */ @@ -174,18 +210,18 @@ Cell ev; { * * ------------------------------------------------------------------------*/ -Int cutoff = 16; /* Used to limit depth of recursion*/ +Int cutoff = 64; /* Used to limit depth of recursion*/ -static Void local cutoffExceeded(pi,o,pi1,o1,ps) -Cell pi, pi1; /* Display error msg when cutoff */ -Int o, o1; +static Void local cutoffExceeded(pi,o,ps) +Cell pi; /* Display error msg when cutoff */ +Int o; List ps; { clearMarks(); ERRMSG(0) "\n*** The type checker has reached the cutoff limit while trying to\n" ETHEN ERRTEXT "*** determine whether:\n*** " ETHEN ERRPRED(copyPred(pi,o)); - ps = (isNull(pi1)) ? copyPreds(ps) : singleton(copyPred(pi1,o1)); + ps = copyPreds(ps); ERRTEXT "\n*** can be deduced from:\n*** " ETHEN ERRCONTEXT(ps); ERRTEXT @@ -207,27 +243,50 @@ Int o; Int d; { Class h1 = getHead(pi1); Class h = getHead(pi); + Cell ev = NIL; - if (h==h1 && samePred(pi1,o1,pi,o)) + /* the h==h1 test is just an optimization, and I'm not + sure it will work with IPs, so I'm being conservative + and commenting it out */ + if (/* h==h1 && */ samePred(pi1,o1,pi,o)) return e; if (isClass(h1) && (!isClass(h) || cclass(h).level= cutoff) - cutoffExceeded(pi,o,pi1,o1,NIL); + for (; nonNull(scs); scs=tl(scs), dsels=tl(dsels)) + ps = cons(triple(hd(scs),mkInt(beta),ap(hd(dsels),e)),ps); + ps = rev(ps); - for (; nonNull(scs); scs=tl(scs), dsels=tl(dsels)) { - Cell ev = scFind(ap(hd(dsels),e),hd(scs),beta,pi,o,d); - if (nonNull(ev)) - return ev; - } +#if EXPLAIN_INSTANCE_RESOLUTION + if (showInstRes) { + int i; + for (i = 0; i < d; i++) + fputc(' ', stdout); + fputs("scEntail(scFind): ", stdout); + printContext(stdout,copyPreds(ps)); + fputs(" ||- ", stdout); + printPred(stdout, copyPred(pi, o)); + fputc('\n', stdout); + } +#endif + improve1(0,ps,pi,o); + ev = scEntail(ps,pi,o,d); +#if EXPLAIN_INSTANCE_RESOLUTION + if (showInstRes && nonNull(ev)) { + int i; + for (i = 0; i < d; i++) + fputc(' ', stdout); + fputs("scSat.\n", stdout); + } +#endif + return ev; } - return NIL; } @@ -236,6 +295,9 @@ List ps; /* Using superclasses and equality.*/ Cell pi; Int o; Int d; { + if (d++ >= cutoff) + cutoffExceeded(pi,o,ps); + for (; nonNull(ps); ps=tl(ps)) { Cell pi1 = hd(ps); Cell ev = scFind(thd3(pi1),fst3(pi1),intOf(snd3(pi1)),pi,o,d); @@ -245,6 +307,7 @@ Int d; { return NIL; } + /* -------------------------------------------------------------------------- * Now we reach the main entailment routine: * @@ -298,8 +361,49 @@ List ps; /* Uses superclasses, equality, */ Cell pi; /* tautology, and construction */ Int o; Int d; { - Cell ev = scEntail(ps,pi,o,d); - return nonNull(ev) ? ev : inEntail(ps,pi,o,d); + Cell ev = NIL; + +#if EXPLAIN_INSTANCE_RESOLUTION + if (showInstRes) { + int i; + for (i = 0; i < d; i++) + fputc(' ', stdout); + fputs("entail: ", stdout); + printContext(stdout,copyPreds(ps)); + fputs(" ||- ", stdout); + printPred(stdout, copyPred(pi, o)); + fputc('\n', stdout); + } +#endif + + ev = scEntail(ps,pi,o,d); + if (nonNull(ev)) { +#if EXPLAIN_INSTANCE_RESOLUTION + if (showInstRes) { + int i; + for (i = 0; i < d; i++) + fputc(' ', stdout); + fputs("scSat.\n", stdout); + } +#endif + } else { + ev = +#if MULTI_INST + multiInstRes ? inEntails(ps,pi,o,d) : + inEntail(ps,pi,o,d); +#else + inEntail(ps,pi,o,d); +#endif +#if EXPLAIN_INSTANCE_RESOLUTION + if (nonNull(ev) && showInstRes) { + int i; + for (i = 0; i < d; i++) + fputc(' ', stdout); + fputs("inSat.\n", stdout); + } +#endif + } + return ev; } static Cell local inEntail(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/ @@ -307,6 +411,12 @@ List ps; /* using a top-level instance */ Cell pi; /* entailment */ Int o; Int d; { + int i; + Inst in; + + if (d++ >= cutoff) + cutoffExceeded(pi,o,ps); + #if TREX if (isAp(pi) && isExt(fun(pi))) { /* Lacks predicates */ Cell e = fun(pi); @@ -333,16 +443,31 @@ Int d; { } else { #endif - Inst in = findInstFor(pi,o); /* Class predicates */ + in = findInstFor(pi,o); /* Class predicates */ if (nonNull(in)) { Int beta = typeOff; Cell e = inst(in).builder; - Cell es = inst(in).specifics; - if (d++ >= cutoff) - cutoffExceeded(pi,o,NIL,0,ps); - for (; nonNull(es); es=tl(es)) { - Cell ev = entail(ps,hd(es),beta,d); + List es = inst(in).specifics; + List fs = NIL; + for (; nonNull(es); es=tl(es)) + fs = cons(triple(hd(es),mkInt(beta),NIL),fs); + fs = rev(fs); + improve(0,ps,fs); +#if EXPLAIN_INSTANCE_RESOLUTION + if (showInstRes) { + for (i = 0; i < d; i++) + fputc(' ', stdout); + fputs("try ", stdout); + printContext(stdout, copyPreds(fs)); + fputs(" => ", stdout); + printPred(stdout, copyPred(inst(in).head,beta)); + fputc('\n', stdout); + } +#endif + for (es=inst(in).specifics; nonNull(es); es=tl(es)) { + Cell ev; + ev = entail(ps,hd(es),beta,d); if (nonNull(ev)) e = ap(e,ev); else @@ -350,12 +475,177 @@ Int d; { } return e; } +#if EXPLAIN_INSTANCE_RESOLUTION + else { + if (showInstRes) { + for (i = 0; i < d; i++) + fputc(' ', stdout); + fputs("No instance found for ", stdout); + printPred(stdout, copyPred(pi, o)); + fputc('\n', stdout); + } + } +#endif + return NIL; +#if TREX + } +#endif +} + +#if MULTI_INST +static Cell local inEntails(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/ +List ps; /* using a top-level instance */ +Cell pi; /* entailment */ +Int o; +Int d; { + int i; + int k = 0; + Cell ins; /* Class predicates */ + Inst in, in_; + Cell e_; + + if (d++ >= cutoff) + cutoffExceeded(pi,o,ps); + +#if TREX + if (isAp(pi) && isExt(fun(pi))) { /* Lacks predicates */ + Cell e = fun(pi); + Cell l; + l = lacksNorm(arg(pi),o,e); + if (isNull(l) || isInt(l)) + return l; + else { + List qs = ps; + for (; nonNull(qs); qs=tl(qs)) { + Cell qi = fst3(hd(qs)); + if (isAp(qi) && fun(qi)==e) { + Cell lq = lacksNorm(arg(qi),intOf(snd3(hd(qs))),e); + if (isAp(lq) && intOf(fst(l))==intOf(fst(lq))) { + Int f = intOf(snd(l)) - intOf(snd(lq)); + return (f==0) ? thd3(hd(qs)) : ap2(nameAddEv, + mkInt(f), + thd3(hd(qs))); + } + } + } + return NIL; + } + } + else { +#endif + +#if EXPLAIN_INSTANCE_RESOLUTION + if (showInstRes) { + for (i = 0; i < d; i++) + fputc(' ', stdout); + fputs("inEntails: ", stdout); + printContext(stdout,copyPreds(ps)); + fputs(" ||- ", stdout); + printPred(stdout, copyPred(pi, o)); + fputc('\n', stdout); + } +#endif + + ins = findInstsFor(pi,o); + for (; nonNull(ins); ins=tl(ins)) { + in = snd(hd(ins)); + if (nonNull(in)) { + Int beta = fst(hd(ins)); + Cell e = inst(in).builder; + Cell es = inst(in).specifics; + +#if EXPLAIN_INSTANCE_RESOLUTION + if (showInstRes) { + for (i = 0; i < d; i++) + fputc(' ', stdout); + fputs("try ", stdout); + printContext(stdout, es); + fputs(" => ", stdout); + printPred(stdout, inst(in).head); + fputc('\n', stdout); + } +#endif + + for (; nonNull(es); es=tl(es)) { + Cell ev = entail(ps,hd(es),beta,d); + if (nonNull(ev)) + e = ap(e,ev); + else { + e = NIL; + break; + } + } +#if EXPLAIN_INSTANCE_RESOLUTION + if (showInstRes) + for (i = 0; i < d; i++) + fputc(' ', stdout); +#endif + if (nonNull(e)) { +#if EXPLAIN_INSTANCE_RESOLUTION + if (showInstRes) + fprintf(stdout, "Sat\n"); +#endif + if (k > 0) { + if (instCompare (in_, in)) { + ERRMSG(0) "Multiple satisfiable instances for " + ETHEN + ERRPRED(copyPred(pi, o)); + ERRTEXT "\nin_ " ETHEN ERRPRED(inst(in_).head); + ERRTEXT "\nin " ETHEN ERRPRED(inst(in).head); + ERRTEXT "\n" + EEND; + } + } + if (k++ == 0) { + e_ = e; + in_ = in; + } + continue; + } else { +#if EXPLAIN_INSTANCE_RESOLUTION + if (showInstRes) + fprintf(stdout, "not Sat\n"); +#endif + continue; + } + } +#if EXPLAIN_INSTANCE_RESOLUTION + if (showInstRes) { + for (i = 0; i < d; i++) + fputc(' ', stdout); + fprintf(stdout, "not Sat.\n"); + } +#endif + } + if (k > 0) + return e_; +#if EXPLAIN_INSTANCE_RESOLUTION + if (showInstRes) { + for (i = 0; i < d; i++) + fputc(' ', stdout); + fprintf(stdout, "all not Sat.\n"); + } +#endif return NIL; #if TREX } #endif } +static Bool local instComp_(ia,ib) /* See if ia is an instance of ib */ +Inst ia, ib;{ + Int alpha = newKindedVars(inst(ia).kinds); + Int beta = newKindedVars(inst(ib).kinds); + return matchPred(inst(ia).head,alpha,inst(ib).head,beta); +} + +static Bool local instCompare (ia, ib) +Inst ia, ib; +{ + return instComp_(ia, ib) && instComp_(ib, ia); +} +#endif + Cell provePred(ks,ps,pi) /* Find evidence for predicate pi */ Kinds ks; /* assuming ps. If ps is null, */ List ps; /* then we get to decide whether */ @@ -413,7 +703,17 @@ List qs; { /* returning equiv minimal subset */ while (0