2 /* --------------------------------------------------------------------------
3 * Part of the type checker dealing with predicates and entailment
5 * Hugs 98 is Copyright (c) Mark P Jones, Alastair Reid and the Yale
6 * Haskell Group 1994-99, and is distributed as Open Source software
7 * under the Artistic License; see the file "Artistic" that is included
8 * in the distribution for details.
10 * $RCSfile: preds.c,v $
12 * $Date: 1999/03/01 14:46:50 $
13 * ------------------------------------------------------------------------*/
15 /* --------------------------------------------------------------------------
16 * Local function prototypes:
17 * ------------------------------------------------------------------------*/
19 static Cell local assumeEvid Args((Cell,Int));
20 static List local makePredAss Args((List,Int));
21 static List local copyPreds Args((List));
22 static Void local qualify Args((List,Cell));
23 static Void local qualifyBinding Args((List,Cell));
24 static Cell local qualifyExpr Args((Int,List,Cell));
25 static Void local overEvid Args((Cell,Cell));
27 static Void local cutoffExceeded Args((Cell,Int,Cell,Int,List));
28 static Cell local scFind Args((Cell,Cell,Int,Cell,Int,Int));
29 static Cell local scEntail Args((List,Cell,Int,Int));
30 static Cell local entail Args((List,Cell,Int,Int));
31 static Cell local inEntail Args((List,Cell,Int,Int));
33 static Cell local lacksNorm Args((Type,Int,Cell));
36 static List local scSimplify Args((List));
37 static Void local elimTauts Args((Void));
38 static Bool local anyGenerics Args((Type,Int));
39 static List local elimOuterPreds Args((List));
40 static List local elimPredsUsing Args((List,List));
41 static Void local reducePreds Args((Void));
42 static Void local normPreds Args((Int));
44 static Bool local resolveDefs Args((List));
45 static Bool local resolveVar Args((Int));
46 static Class local classConstraining Args((Int,Cell,Int));
48 /* --------------------------------------------------------------------------
49 * Predicate assignments:
51 * A predicate assignment is represented by a list of triples (pi,o,ev)
52 * where o is the offset for types in pi, with evidence required at the
53 * node pointed to by ev (which is taken as a dictionary parameter if
54 * no other evidence is available). Note that the ev node will be
55 * overwritten at a later stage if evidence for that predicate is found
57 * ------------------------------------------------------------------------*/
59 static List preds; /* Current predicate assignment */
61 static Cell local assumeEvid(pi,o) /* Add predicate pi (offset o) to */
62 Cell pi; /* preds with new dict var nd */
64 Cell nd = inventDictVar();
65 preds = cons(triple(pi,mkInt(o),nd),preds);
69 static List local makePredAss(qs,o) /* Make list of predicate assumps. */
70 List qs; /* from qs (offset o), w/ new dict */
71 Int o; { /* vars for each predicate */
73 for (; nonNull(qs); qs=tl(qs))
74 result = cons(triple(hd(qs),mkInt(o),inventDictVar()),result);
78 static List local copyPreds(qs) /* Copy list of predicates */
81 for (; nonNull(qs); qs=tl(qs)) {
83 result = cons(copyPred(fst3(pi),intOf(snd3(pi))),result);
88 static Void local qualify(qs,alt) /* Add extra dictionary args to */
89 List qs; /* qualify alt by predicates in qs */
90 Cell alt; { /* :: ([Pat],Rhs) */
92 for (ds=NIL; nonNull(qs); qs=tl(qs))
93 ds = cons(thd3(hd(qs)),ds);
94 fst(alt) = revOnto(ds,fst(alt));
97 static Void local qualifyBinding(qs,b) /* Add extra dict args to each */
98 List qs; /* alternative in function binding */
100 if (!isVar(fst(b))) /* check for function binding */
101 internal("qualifyBinding");
102 map1Proc(qualify,qs,snd(snd(b)));
105 static Cell local qualifyExpr(l,ps,e) /* Add dictionary params to expr */
109 if (nonNull(ps)) { /* Qualify input expression with */
110 if (whatIs(e)!=LAMBDA) /* additional dictionary params */
111 e = ap(LAMBDA,pair(NIL,pair(mkInt(l),e)));
117 static Void local overEvid(dv,ev) /* Overwrite dict var dv with */
118 Cell dv; /* evidence ev */
124 /* --------------------------------------------------------------------------
125 * Predicate entailment:
127 * Entailment plays a prominent role in the theory of qualified types, and
128 * so, unsurprisingly, in the implementation too. For practical reasons,
129 * we break down entailment into two pieces. The first, scEntail, uses
130 * only the information provided by class declarations, while the second,
131 * entail, also uses the information in instance declarations.
133 * scEntail uses the following auxiliary function to do its work:
135 * scFind (e : pi') pi : Find evidence for predicate pi using only
136 * equality of predicates, superclass entailment,
137 * and the evidence e for pi'.
139 * scFind (e : pi') pi =
144 * if (pi.class.level < pi'.class.level)
145 * get superclass entailment pi' ||- P
146 * for each (sc, pi0) in P
147 * if (ev := scFind (sc e : pi0) pi) /= NIL
152 * This code assumes that the class hierarchy is acyclic, and that
153 * each class has been assigned a `level', which is its height in
154 * the hierachy. The first of the assumptions guarantees that the
155 * algorithm will terminate. The comparison of levels is an
156 * optimization that cuts down the search space: given that superclass
157 * entailments can only be used to descend the hierarchy, there is no
158 * way we can reach a higher level than the one that we start with,
159 * and hence there is no point in looking if we reach such a position.
161 * scEntail extends scFind to work on whole predicate assignments:
163 * scEntail P pi : Find evidence for predicate pi using the evidence
164 * provided by the predicate assignment P, and using
165 * only superclass entailments.
169 * for each (v:pi') in P
170 * if (ev := scFind (v:pi') pi) /= NIL
174 * ------------------------------------------------------------------------*/
176 Int cutoff = 16; /* Used to limit depth of recursion*/
178 static Void local cutoffExceeded(pi,o,pi1,o1,ps)
179 Cell pi, pi1; /* Display error msg when cutoff */
184 "\n*** The type checker has reached the cutoff limit while trying to\n"
186 "*** determine whether:\n*** " ETHEN ERRPRED(copyPred(pi,o));
187 ps = (isNull(pi1)) ? copyPreds(ps) : singleton(copyPred(pi1,o1));
189 "\n*** can be deduced from:\n*** " ETHEN ERRCONTEXT(ps);
191 "\n*** This may indicate that the problem is undecidable. However,\n"
193 "*** you may still try to increase the cutoff limit using the -c\n"
195 "*** option and then try again. (The current setting is -c%d)\n",
200 static Cell local scFind(e,pi1,o1,pi,o,d)/* Use superclass entailment to */
201 Cell e; /* find evidence for (pi,o) using */
202 Cell pi1; /* the evidence e for (pi1,o1). */
207 Class h1 = getHead(pi1);
208 Class h = getHead(pi);
210 if (h==h1 && samePred(pi1,o1,pi,o))
213 if (isClass(h1) && (!isClass(h) || cclass(h).level<cclass(h1).level)) {
214 Int beta = newKindedVars(cclass(h1).kinds);
215 List scs = cclass(h1).supers;
216 List dsels = cclass(h1).dsels;
217 if (!matchPred(pi1,o1,cclass(h1).head,beta))
221 cutoffExceeded(pi,o,pi1,o1,NIL);
223 for (; nonNull(scs); scs=tl(scs), dsels=tl(dsels)) {
224 Cell ev = scFind(ap(hd(dsels),e),hd(scs),beta,pi,o,d);
233 static Cell local scEntail(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/
234 List ps; /* Using superclasses and equality.*/
238 for (; nonNull(ps); ps=tl(ps)) {
240 Cell ev = scFind(thd3(pi1),fst3(pi1),intOf(snd3(pi1)),pi,o,d);
247 /* --------------------------------------------------------------------------
248 * Now we reach the main entailment routine:
250 * entail P pi : Find evidence for predicate pi using the evidence
251 * provided by the predicate assignment P.
255 * if (ev := scEntail P pi) /= NIL
258 * if there is an instance entailment i : Q ||- pi
260 * if (ev := entail P pi') /= NIL
268 * The form of evidence expressions produced by scEntail can be described
271 * e = v | sc e (v = evidence var, sc = superclass sel)
273 * while entail extends this to include dictionary expressions given by:
275 * d = e | mki d1 ... dn (mki = dictionary constructor)
277 * A full grammar for evidence expressions is:
279 * d = v | sc d | mki d1 ... dn
281 * and this includes evidence expressions of the form sc (mki d1 ... dn)
282 * that can never be produced by either of the entail functions described
283 * above. This is good, from a practical perspective, because t means
284 * that we won't waste effort building a dictionary (mki d1 ... dn) only
285 * to extract just one superclass component and throw the rest away.
286 * Moreover, conditions on instance decls already guarantee that any
287 * expression of this form can be rewritten in the form mki' d1' ... dn'.
288 * (Minor point: they don't guarantee that such rewritings will lead to
289 * smaller terms, and hence to termination. However, we have already
290 * accepted the benefits of an undecidable entailment relation over
291 * guarantees of termination, and this additional quirk is unlikely
292 * to cause any further concern, except in pathological cases.)
293 * ------------------------------------------------------------------------*/
295 static Cell local entail(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/
296 List ps; /* Uses superclasses, equality, */
297 Cell pi; /* tautology, and construction */
300 Cell ev = scEntail(ps,pi,o,d);
301 return nonNull(ev) ? ev : inEntail(ps,pi,o,d);
304 static Cell local inEntail(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/
305 List ps; /* using a top-level instance */
306 Cell pi; /* entailment */
310 if (isAp(pi) && isExt(fun(pi))) { /* Lacks predicates */
313 l = lacksNorm(arg(pi),o,e);
314 if (isNull(l) || isInt(l))
318 for (; nonNull(qs); qs=tl(qs)) {
319 Cell qi = fst3(hd(qs));
320 if (isAp(qi) && fun(qi)==e) {
321 Cell lq = lacksNorm(arg(qi),intOf(snd3(hd(qs))),e);
322 if (isAp(lq) && intOf(fst(l))==intOf(fst(lq))) {
323 Int f = intOf(snd(l)) - intOf(snd(lq));
324 return (f==0) ? thd3(hd(qs)) : ap2(nameAddEv,
335 Inst in = findInstFor(pi,o); /* Class predicates */
339 Cell e = inst(in).builder;
340 Cell es = inst(in).specifics;
342 cutoffExceeded(pi,o,NIL,0,ps);
343 for (; nonNull(es); es=tl(es)) {
344 Cell ev = entail(ps,hd(es),beta,d);
358 Cell provePred(ks,ps,pi) /* Find evidence for predicate pi */
359 Kinds ks; /* assuming ps. If ps is null, */
360 List ps; /* then we get to decide whether */
361 Cell pi; { /* is tautological, and we can use */
362 Int beta; /* the evidence as a dictionary. */
365 beta = newKindedVars(ks); /* (ks provides kinds for any */
366 ps = makePredAss(ps,beta); /* vars that appear in pi.) */
367 ev = entail(ps,pi,beta,0);
373 static Cell local lacksNorm(t,o,e) /* Normalize lacks pred (t,o)\l */
374 Type t; /* returning NIL (unsatisfiable), */
375 Int o; /* Int (tautological) or pair (v,a)*/
376 Cell e; { /* such that, if e is evid for v\l,*/
377 Text l = extText(e); /* then (e+a) is evid for (t,o)\l. */
383 return pair(mkInt(tyvNum(tyv)),mkInt(a));
385 Cell h = getDerefHead(t,o);
386 if (h==typeNoRow && argCount==0)
388 else if (isExt(h) && argCount==2) {
389 Text l1 = extText(h);
392 else if (strcmp(textToStr(l1),textToStr(l))<0)
403 /* --------------------------------------------------------------------------
404 * Predicate set Simplification:
406 * Calculate a minimal equivalent subset of a given set of predicates.
407 * ------------------------------------------------------------------------*/
409 static List local scSimplify(qs) /* Simplify predicates in qs, */
410 List qs; { /* returning equiv minimal subset */
415 Cell ev = scEntail(tl(qs),fst3(pi),intOf(snd3(pi)),0);
417 overEvid(thd3(pi),ev); /* Overwrite dict var with evidence*/
418 qs = tl(qs); /* ... and discard predicate */
420 else { /* Otherwise, retain predicate */
423 qs = appendOnto(tmp,qs);
429 List simpleContext(ps,o) /* Simplify context of skeletons */
430 List ps; /* skeletons, offset o, using */
431 Int o; { /* superclass hierarchy */
432 return copyPreds(scSimplify(makePredAss(ps,o)));
435 /* --------------------------------------------------------------------------
436 * Context splitting --- tautological and locally tautological predicates:
437 * ------------------------------------------------------------------------*/
439 static Void local elimTauts() { /* Remove tautological constraints */
440 if (haskell98) { /* from preds */
441 reducePreds(); /* (or context reduce for Hask98) */
445 while (nonNull(ps)) {
447 Cell ev = entail(NIL,fst3(pi),intOf(snd3(pi)),0);
449 overEvid(thd3(pi),ev);
462 static Int numFixedVars = 0; /* Number of fixed vars found */
464 static Bool local anyGenerics(t,o) /* Test for generic vars, and count*/
465 Type t; /* fixed variables */
467 Type h = getDerefHead(t,o); /* This code is careful to expand */
468 Int a = argCount; /* synonyms; mark* & copy* do not. */
469 if (isSynonym(h) && a>=tycon(h).arity) {
470 expandSyn(h,a,&t,&o);
471 return anyGenerics(t,o);
475 for (; 0<a--; t=fun(t)) { /* cycle through any arguments */
477 if (anyGenerics(arg(t),o))
482 if (tyv->offs == FIXED_TYVAR) {
494 static List local elimOuterPreds(sps) /* Simplify and defer any remaining*/
495 List sps; { /* preds that contain no generics. */
498 for (preds=scSimplify(preds); nonNull(preds); ) {
501 if (anyGenerics(fst3(pi),intOf(snd3(pi)))) { /* Retain predicate*/
505 else { /* Defer predicate */
515 static List local elimPredsUsing(ps,sps)/* Try to discharge or defer preds,*/
516 List ps; /* splitting if necessary to match */
517 List sps; { /* context ps. sps = savePreds. */
519 while (nonNull(preds)) { /* Pick a predicate from preds */
521 Cell pi = fst3(hd(p));
522 Int o = intOf(snd3(hd(p)));
523 Cell ev = entail(ps,pi,o,0);
526 if (nonNull(ev)) /* Discharge if ps ||- (pi,o) */
527 overEvid(thd3(hd(p)),ev);
528 else if (!anyGenerics(pi,o)) { /* Defer if no generics */
532 else { /* Try to split generics and fixed */
534 if (numFixedVars>0 && nonNull(in=findInstFor(pi,o))) {
535 List qs = inst(in).specifics;
536 for (ev=inst(in).builder; nonNull(qs); qs=tl(qs))
537 ev = ap(ev,assumeEvid(hd(qs),typeOff));
538 overEvid(thd3(hd(p)),ev);
540 else { /* No worthwhile progress possible */
546 preds = rems; /* Return any remaining predicates */
550 static Void local reducePreds() { /* Context reduce predicates: uggh!*/
551 List rems = NIL; /* (A last resort for defaulting) */
552 while (nonNull(preds)) { /* Pick a predicate from preds */
554 Cell pi = fst3(hd(p));
555 Int o = intOf(snd3(hd(p)));
556 Inst in = findInstFor(pi,o);
559 List qs = inst(in).specifics;
560 Cell ev = inst(in).builder;
561 for (; nonNull(qs); qs=tl(qs))
562 ev = ap(ev,assumeEvid(hd(qs),typeOff));
563 overEvid(thd3(hd(p)),ev);
565 else { /* No worthwhile progress possible */
570 preds = scSimplify(rems); /* Return any remaining predicates */
573 static Void local normPreds(line) /* Normalize each element of preds */
574 Int line; { /* in some appropriate manner */
578 while (nonNull(ps)) {
579 Cell pi = fst3(hd(ps));
580 Cell ev = thd3(hd(ps));
581 if (isAp(pi) && isExt(fun(pi))) {
582 Cell r = lacksNorm(arg(pi),intOf(snd3(hd(ps))),fun(pi));
584 ERRMSG(line) "Cannot satisfy constraint " ETHEN
585 ERRPRED(copyPred(pi,intOf(snd3(hd(ps)))));
597 else if (intOf(snd(r))!=0) {
598 Cell nd = inventDictVar();
599 Cell ev1 = ap2(nameAddEv,snd(r),nd);
600 pi = ap(fun(pi),aVar);
601 hd(ps) = triple(pi,fst(r),nd);
607 fst3(hd(ps)) = ap(fun(pi),fst(r));
620 /* --------------------------------------------------------------------------
621 * Mechanisms for dealing with defaults:
622 * ------------------------------------------------------------------------*/
624 static Bool local resolveDefs(vs) /* Attempt to resolve defaults */
625 List vs; { /* for variables vs subject to */
626 List pvs = NIL; /* constraints in preds */
628 Bool defaulted = FALSE;
630 #ifdef DEBUG_DEFAULTS
631 Printf("Attempt to resolve variables ");
633 Printf(" with context ");
634 printContext(stdout,copyPreds(preds));
638 resetGenerics(); /* find type variables in ps */
639 for (; nonNull(qs); qs=tl(qs)) {
640 Cell pi = fst3(hd(qs));
641 Int o = intOf(snd3(hd(qs)));
642 for (; isAp(pi); pi=fun(pi))
643 pvs = genvarType(arg(pi),o,pvs);
646 for (; nonNull(pvs); pvs=tl(pvs)) { /* now try defaults */
647 Int vn = intOf(hd(pvs));
649 #ifdef DEBUG_DEFAULTS
650 Printf("is var %d included in ",vn);
655 if (!intIsMember(vn,vs))
656 defaulted |= resolveVar(vn);
657 #ifdef DEBUG_DEFAULTS
659 Printf("Yes, so no ambiguity!\n");
666 static Bool local resolveVar(vn) /* Determine whether an ambig. */
667 Int vn; { /* variable vn can be resolved */
668 List ps = preds; /* by default in the context of */
669 List cs = NIL; /* the predicates in ps */
670 Bool aNumClass = FALSE;
672 if (tyvar(vn)->bound == SKOLEM)
675 /* According to the Haskell definition, we can only default an ambiguous
676 * variable if the set of classes that constrain it:
677 * (a) includes at least one numeric class.
678 * (b) includes only numeric or standard classes.
679 * In addition, we will not allow a variable to be defaulted unless it
680 * appears only in predicates of the form (Class var).
683 #ifdef DEBUG_DEFAULTS
684 Printf("Trying to default variable %d\n",vn);
687 for (; nonNull(ps); ps=tl(ps)) {
689 Class c = classConstraining(vn,fst3(pi),intOf(snd3(pi)));
691 if (c==classRealFrac || c==classRealFloat ||
692 c==classFractional || c==classFloating ||
693 c==classReal || c==classIntegral || c==classNum)
695 else if (c!=classEq && c!=classOrd && c!=classShow &&
696 c!=classRead && c!=classIx && c!=classEnum &&
703 { Type t = arg(fst3(pi));/* Check for single var as arg */
704 Int o = intOf(snd3(pi));
707 if (!tyv || tyvNum(tyv)!=vn)
710 if (!cellIsMember(c,cs))
715 /* Now find the first class (if any) in the list of defaults that
716 * is an instance of all of the required classes.
718 * If we get this far, then cs only mentions classes from the list
719 * above, all of which have only a single parameter of kind *.
723 List ds = defaultDefns; /* N.B. guaranteed to be monotypes */
724 #ifdef DEBUG_DEFAULTS
725 Printf("Default conditions met, looking for type\n");
727 for (; nonNull(ds); ds=tl(ds)) {
729 while (nonNull(cs1) && nonNull(entail(NIL,ap(hd(cs1),hd(ds)),0,0)))
733 #ifdef DEBUG_DEFAULTS
734 Printf("Default type for variable %d is ",vn);
735 printType(stdout,hd(ds));
743 #ifdef DEBUG_DEFAULTS
744 Printf("No default permitted/found\n");
749 static Class local classConstraining(vn,pi,o)
750 Int vn; /* Return class constraining var*/
751 Cell pi; /* vn in predicate pi, or NIL if*/
752 Int o; { /* vn is not involved */
753 for (; isAp(pi); pi=fun(pi))
754 if (!doesntOccurIn(tyvar(vn),arg(pi),o))
759 /*-------------------------------------------------------------------------*/