/* --------------------------------------------------------------------------
* Part of the type checker dealing with predicates and entailment
*
- * Hugs 98 is Copyright (c) Mark P Jones, Alastair Reid and the Yale
- * Haskell Group 1994-99, and is distributed as Open Source software
- * under the Artistic License; see the file "Artistic" that is included
- * in the distribution for details.
+ * The Hugs 98 system is Copyright (c) Mark P Jones, Alastair Reid, the
+ * Yale Haskell Group, and the Oregon Graduate Institute of Science and
+ * Technology, 1994-1999, All rights reserved. It is distributed as
+ * free software under the license in the file "License", which is
+ * included in the distribution.
*
* $RCSfile: preds.c,v $
- * $Revision: 1.5 $
- * $Date: 1999/04/27 10:06:59 $
+ * $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:
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 */
*
* ------------------------------------------------------------------------*/
-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
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<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;
}
+
/* --------------------------------------------------------------------------
* 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 : 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*/
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
+ }
+#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 */
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 */
for (preds=scSimplify(preds); nonNull(preds); ) {
Cell pi = hd(preds);
Cell nx = tl(preds);
- if (anyGenerics(fst3(pi),intOf(snd3(pi)))) { /* Retain predicate*/
- tl(preds) = qs;
- qs = preds;
+ if (anyGenerics(fst3(pi),intOf(snd3(pi)))
+ || !isAp(fst3(pi))
+ || isIP(fun(fst3(pi)))) {
+ tl(preds) = qs; /* Retain predicate*/
+ qs = preds;
}
else { /* Defer predicate */
tl(preds) = sps;
Cell ev = entail(ps,pi,o,0);
preds = tl(preds);
- if (nonNull(ev)) /* Discharge if ps ||- (pi,o) */
+ if (nonNull(ev)) { /* Discharge if ps ||- (pi,o) */
overEvid(thd3(hd(p)),ev);
- else if (!anyGenerics(pi,o)) { /* Defer if no generics */
- tl(p) = sps;
+ } 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;
}
else { /* Try to split generics and fixed */
Cell p = preds;
Cell pi = fst3(hd(p));
Int o = intOf(snd3(hd(p)));
- Inst in = findInstFor(pi,o);
+ Inst in = NIL;
+#if MULTI_INST
+ List ins = NIL;
+ if (multiInstRes) {
+ ins = findInstsFor(pi,o);
+ in = nonNull(ins) && isNull(tl(ins)) ? snd(hd(ins)) : NIL;
+ } else
+#endif
+ in = findInstFor(pi,o);
preds = tl(preds);
if (nonNull(in)) {
List qs = inst(in).specifics;
projects / ghc-hetmet.git / blobdiff