X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Finterpreter%2Fpreds.c;h=7c5a7a848bf75bd70502ceed2cb645eef0b0cae0;hb=9aa6d18bd696e8861fb8c3e065e49a989d2d67ac;hp=6a88cb8c4b925934165aa4bd0e41f5b74d65af72;hpb=438596897ebbe25a07e1c82085cfbc5bdb00f09e;p=ghc-hetmet.git diff --git a/ghc/interpreter/preds.c b/ghc/interpreter/preds.c index 6a88cb8..7c5a7a8 100644 --- a/ghc/interpreter/preds.c +++ b/ghc/interpreter/preds.c @@ -1,43 +1,59 @@ -/* -*- mode: hugs-c; -*- */ + /* -------------------------------------------------------------------------- - * preds.c: Copyright (c) Mark P Jones 1991-1998. All rights reserved. - * See NOTICE for details and conditions of use etc... - * Hugs version 1.3c, March 1998 + * Part of the type checker dealing with predicates and entailment + * + * 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. * - * Part of type checker dealing with predicates and entailment. + * $RCSfile: preds.c,v $ + * $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 Cell local scFind Args((Cell,Cell,Int,Cell,Int)); -static Cell local scEntail Args((List,Cell,Int)); -static Cell local entail Args((List,Cell,Int)); -static Cell local inEntail Args((List,Cell,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: @@ -60,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 */ @@ -167,47 +210,104 @@ Cell ev; { * * ------------------------------------------------------------------------*/ -static Cell local scFind(e,pi1,o1,pi,o) /* Use superclass entailment to */ +Int cutoff = 64; /* Used to limit depth of recursion*/ + +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 = copyPreds(ps); + ERRTEXT + "\n*** can be deduced from:\n*** " ETHEN ERRCONTEXT(ps); + ERRTEXT + "\n*** This may indicate that the problem is undecidable. However,\n" + ETHEN ERRTEXT + "*** you may still try to increase the cutoff limit using the -c\n" + ETHEN ERRTEXT + "*** option and then try again. (The current setting is -c%d)\n", + cutoff + EEND; +} + +static Cell local scFind(e,pi1,o1,pi,o,d)/* Use superclass entailment to */ Cell e; /* find evidence for (pi,o) using */ Cell pi1; /* the evidence e for (pi1,o1). */ Int o1; Cell pi; -Int o; { +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,ps); + for (; nonNull(ps); ps=tl(ps)) { Cell pi1 = hd(ps); - Cell ev = scFind(thd3(pi1),fst3(pi1),intOf(snd3(pi1)),pi,o); + Cell ev = scFind(thd3(pi1),fst3(pi1),intOf(snd3(pi1)),pi,o,d); if (nonNull(ev)) return ev; } return NIL; } + /* -------------------------------------------------------------------------- * Now we reach the main entailment routine: * @@ -256,18 +356,67 @@ Int o; { * to cause any further concern, except in pathological cases.) * ------------------------------------------------------------------------*/ -static Cell local entail(ps,pi,o) /* Calc evidence for (pi,o) from ps*/ +static Cell local entail(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/ List ps; /* Uses superclasses, equality, */ Cell pi; /* tautology, and construction */ -Int o; { - Cell ev = scEntail(ps,pi,o); - return nonNull(ev) ? ev : inEntail(ps,pi,o); +Int o; +Int 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) /* Calc evidence for (pi,o) from ps*/ +static Cell local inEntail(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/ List ps; /* using a top-level instance */ Cell pi; /* entailment */ -Int o; { +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); @@ -294,26 +443,209 @@ Int o; { } else { #endif - Inst in = findInstFor(pi,o); /* Class predicates */ + + in = findInstFor(pi,o); /* Class predicates */ if (nonNull(in)) { Int beta = typeOff; - Cell d = inst(in).builder; - Cell ds = inst(in).specifics; - for (; nonNull(ds); ds=tl(ds)) { - Cell ev = entail(ps,hd(ds),beta); + Cell e = inst(in).builder; + 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)) - d = ap(d,ev); + e = ap(e,ev); else return NIL; } - return 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 */ @@ -323,7 +655,7 @@ Cell pi; { /* is tautological, and we can use */ emptySubstitution(); beta = newKindedVars(ks); /* (ks provides kinds for any */ ps = makePredAss(ps,beta); /* vars that appear in pi.) */ - ev = entail(ps,pi,beta); + ev = entail(ps,pi,beta,0); emptySubstitution(); return ev; } @@ -371,7 +703,17 @@ List qs; { /* returning equiv minimal subset */ while (0offs == FIXED_TYVAR) { numFixedVars++; return FALSE; } else return TRUE; + } else return FALSE; } @@ -452,9 +799,11 @@ List sps; { /* preds that contain no generics. */ 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; @@ -474,13 +823,16 @@ List sps; { /* context ps. sps = savePreds. */ Cell p = preds; Cell pi = fst3(hd(p)); Int o = intOf(snd3(hd(p))); - Cell ev = entail(ps,pi,o); + 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 */ @@ -507,7 +859,15 @@ static Void local reducePreds() { /* Context reduce predicates: uggh!*/ 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; @@ -582,11 +942,11 @@ List vs; { /* for variables vs subject to */ Bool defaulted = FALSE; #ifdef DEBUG_DEFAULTS - printf("Attempt to resolve variables "); + Printf("Attempt to resolve variables "); printExp(stdout,vs); - printf(" with context "); + Printf(" with context "); printContext(stdout,copyPreds(preds)); - printf("\n"); + Printf("\n"); #endif resetGenerics(); /* find type variables in ps */ @@ -601,16 +961,16 @@ List vs; { /* for variables vs subject to */ Int vn = intOf(hd(pvs)); #ifdef DEBUG_DEFAULTS - printf("is var %d included in ",vn); + Printf("is var %d included in ",vn); printExp(stdout,vs); - printf("?\n"); + Printf("?\n"); #endif if (!intIsMember(vn,vs)) defaulted |= resolveVar(vn); #ifdef DEBUG_DEFAULTS else - printf("Yes, so no ambiguity!\n"); + Printf("Yes, so no ambiguity!\n"); #endif } @@ -635,7 +995,7 @@ Int vn; { /* variable vn can be resolved */ */ #ifdef DEBUG_DEFAULTS - printf("Trying to default variable %d\n",vn); + Printf("Trying to default variable %d\n",vn); #endif for (; nonNull(ps); ps=tl(ps)) { @@ -648,9 +1008,6 @@ Int vn; { /* variable vn can be resolved */ aNumClass = TRUE; else if (c!=classEq && c!=classOrd && c!=classShow && c!=classRead && c!=classIx && c!=classEnum && -#if EVAL_INSTANCES - c!=classEval && -#endif c!=classBounded) return FALSE; @@ -676,18 +1033,18 @@ Int vn; { /* variable vn can be resolved */ if (aNumClass) { List ds = defaultDefns; /* N.B. guaranteed to be monotypes */ #ifdef DEBUG_DEFAULTS - printf("Default conditions met, looking for type\n"); + Printf("Default conditions met, looking for type\n"); #endif for (; nonNull(ds); ds=tl(ds)) { List cs1 = cs; - while (nonNull(cs1) && nonNull(entail(NIL,ap(hd(cs1),hd(ds)),0))) + while (nonNull(cs1) && nonNull(entail(NIL,ap(hd(cs1),hd(ds)),0,0))) cs1 = tl(cs1); if (isNull(cs1)) { bindTv(vn,hd(ds),0); #ifdef DEBUG_DEFAULTS - printf("Default type for variable %d is ",vn); + Printf("Default type for variable %d is ",vn); printType(stdout,hd(ds)); - printf("\n"); + Printf("\n"); #endif return TRUE; } @@ -695,7 +1052,7 @@ Int vn; { /* variable vn can be resolved */ } #ifdef DEBUG_DEFAULTS - printf("No default permitted/found\n"); + Printf("No default permitted/found\n"); #endif return FALSE; }