X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Finterpreter%2Fpreds.c;h=7c5a7a848bf75bd70502ceed2cb645eef0b0cae0;hb=4ba55934c50379cba5650ddd84d9326a55722047;hp=1c95a58511fe81da7d4e042100f5044c0d7e7421;hpb=4847ea83e1d0f4fa8596b71ba64519bdb004de7d;p=ghc-hetmet.git diff --git a/ghc/interpreter/preds.c b/ghc/interpreter/preds.c index 1c95a58..7c5a7a8 100644 --- a/ghc/interpreter/preds.c +++ b/ghc/interpreter/preds.c @@ -9,52 +9,51 @@ * included in the distribution. * * $RCSfile: preds.c,v $ - * $Revision: 1.8 $ - * $Date: 1999/10/20 02:16:04 $ + * $Revision: 1.11 $ + * $Date: 2000/03/13 11:37:16 $ * ------------------------------------------------------------------------*/ /* -------------------------------------------------------------------------- * Local function prototypes: * ------------------------------------------------------------------------*/ -static Cell local assumeEvid Args((Cell,Int)); +static Cell local assumeEvid ( Cell,Int ); #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 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 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 Args((List,Cell,Int,Int)); -static Bool local instCompare Args((Inst, 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 instComp_ Args((Inst,Inst)); +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: @@ -213,16 +212,16 @@ Cell ev; { 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 @@ -244,6 +243,7 @@ Int o; 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 @@ -251,24 +251,42 @@ Int d; { 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= 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; } @@ -277,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); @@ -286,36 +307,6 @@ Int 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: @@ -370,14 +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 : + 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*/ @@ -385,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); @@ -411,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 @@ -428,6 +475,17 @@ 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 } @@ -444,9 +502,11 @@ Int d; { 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); @@ -473,16 +533,15 @@ Int d; { } 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 @@ -494,7 +553,6 @@ Int d; { Int beta = fst(hd(ins)); Cell e = inst(in).builder; Cell es = inst(in).specifics; - Cell es_ = es; #if EXPLAIN_INSTANCE_RESOLUTION if (showInstRes) { @@ -645,7 +703,17 @@ List qs; { /* returning equiv minimal subset */ while (0