* included in the distribution.
*
* $RCSfile: preds.c,v $
- * $Revision: 1.8 $
- * $Date: 1999/10/20 02:16:04 $
+ * $Revision: 1.10 $
+ * $Date: 2000/03/06 08:38:04 $
* ------------------------------------------------------------------------*/
/* --------------------------------------------------------------------------
#if IPARAM
static Cell local findIPEvid Args((Text));
static Void local removeIPEvid Args((Text));
-static Void local matchupIPs Args((List,List));
#endif
static List local makePredAss Args((List,Int));
static List local copyPreds Args((List));
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 Void local cutoffExceeded Args((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));
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
Int d; {
Class h1 = getHead(pi1);
Class h = getHead(pi);
+ Cell ev = NIL;
/* the h==h1 test is just an optimization, and I'm not
sure it will work with IPs, so I'm being conservative
if (/* h==h1 && */ samePred(pi1,o1,pi,o))
return e;
- /* the cclass.level test is also an optimization */
if (isClass(h1) && (!isClass(h) || cclass(h).level<cclass(h1).level)) {
- Int beta = newKindedVars(cclass(h1).kinds);
- List scs = cclass(h1).supers;
- List dsels = cclass(h1).dsels;
- if (!matchPred(pi1,o1,cclass(h1).head,beta))
- internal("scFind");
+ Int beta = newKindedVars(cclass(h1).kinds);
+ List scs = cclass(h1).supers;
+ List dsels = cclass(h1).dsels;
+ List ps = NIL;
+ if (!matchPred(pi1,o1,cclass(h1).head,beta))
+ internal("scFind");
- if (d++ >= 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;
}
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);
return NIL;
}
-#if IPARAM
-static Cell local ipEntail(ps,ip,o) /* Find evidence for (ip,o) from ps*/
-List ps;
-Cell ip;
-Int o; {
- Class h = getHead(ip);
- int i;
- for (; nonNull(ps); ps=tl(ps)) {
- Cell pr1 = hd(ps);
- Cell pi1 = fst3(pr1);
- Int o1 = intOf(snd3(pr1));
- Class h1 = getHead(pi1);
- if (isIP(h1)) {
- if (textOf(h1) == textOf(h)) {
- if (unify(arg(pi1),o1,arg(ip),o)) {
- return thd3(pr1);
- } else {
- ERRMSG(0) "Mismatching uses of implicit parameter\n" ETHEN
- ERRPRED(copyPred(pi1,o1));
- ERRTEXT "\n" ETHEN
- ERRPRED(copyPred(ip,o));
- ERRTEXT "\n"
- EEND;
- }
- }
- }
- }
- return NIL;
-}
-#endif
/* --------------------------------------------------------------------------
* Now we reach the main entailment routine:
Cell pi; /* tautology, and construction */
Int o;
Int d; {
- Cell ev = scEntail(ps,pi,o,d);
- return nonNull(ev) ? ev :
+ 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);
+ multiInstRes ? inEntails(ps,pi,o,d) :
+ inEntail(ps,pi,o,d);
#else
- inEntail(ps,pi,o,d);
+ 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*/
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);
}
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
}
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
}
int k = 0;
Cell ins; /* Class predicates */
Inst in, in_;
- Cell pi_;
Cell e_;
+ if (d++ >= cutoff)
+ cutoffExceeded(pi,o,ps);
+
#if TREX
if (isAp(pi) && isExt(fun(pi))) { /* Lacks predicates */
Cell e = fun(pi);
}
else {
#endif
- if (d++ >= cutoff)
- cutoffExceeded(pi,o,NIL,0,ps);
#if EXPLAIN_INSTANCE_RESOLUTION
if (showInstRes) {
- pi_ = copyPred(pi, o);
for (i = 0; i < d; i++)
fputc(' ', stdout);
fputs("inEntails: ", stdout);
- printPred(stdout, pi_);
+ printContext(stdout,copyPreds(ps));
+ fputs(" ||- ", stdout);
+ printPred(stdout, copyPred(pi, o));
fputc('\n', stdout);
}
#endif
Int beta = fst(hd(ins));
Cell e = inst(in).builder;
Cell es = inst(in).specifics;
- Cell es_ = es;
#if EXPLAIN_INSTANCE_RESOLUTION
if (showInstRes) {
while (0<n--) {
Cell pi = hd(qs);
- Cell ev = scEntail(tl(qs),fst3(pi),intOf(snd3(pi)),0);
+ Cell ev = NIL;
+#if EXPLAIN_INSTANCE_RESOLUTION
+ if (showInstRes) {
+ fputs("scSimplify: ", stdout);
+ printContext(stdout,copyPreds(tl(qs)));
+ fputs(" ||- ", stdout);
+ printPred(stdout, copyPred(fst3(pi),intOf(snd3(pi))));
+ fputc('\n', stdout);
+ }
+#endif
+ ev = scEntail(tl(qs),fst3(pi),intOf(snd3(pi)),0);
if (nonNull(ev)) {
overEvid(thd3(pi),ev); /* Overwrite dict var with evidence*/
qs = tl(qs); /* ... and discard predicate */
if (nonNull(ev)) { /* Discharge if ps ||- (pi,o) */
overEvid(thd3(hd(p)),ev);
- } else if (!isAp(pi) || isIP(fun(pi)) || !anyGenerics(pi,o)) {
+ } else if (isIP(fun(pi))) {
+ tl(p) = rems;
+ rems = p;
+ } else if (!isAp(pi) || !anyGenerics(pi,o)) {
tl(p) = sps; /* Defer if no generics */
sps = p;
}
List ins = NIL;
if (multiInstRes) {
ins = findInstsFor(pi,o);
- in = nonNull(ins) && isNull(tl(ins)) ? hd(ins) : NIL;
+ in = nonNull(ins) && isNull(tl(ins)) ? snd(hd(ins)) : NIL;
} else
#endif
in = findInstFor(pi,o);
projects / ghc-hetmet.git / blobdiff