2 /* --------------------------------------------------------------------------
3 * Part of the type checker dealing with predicates and entailment
5 * The Hugs 98 system is Copyright (c) Mark P Jones, Alastair Reid, the
6 * Yale Haskell Group, and the Oregon Graduate Institute of Science and
7 * Technology, 1994-1999, All rights reserved. It is distributed as
8 * free software under the license in the file "License", which is
9 * included in the distribution.
11 * $RCSfile: preds.c,v $
13 * $Date: 1999/10/20 02:16:04 $
14 * ------------------------------------------------------------------------*/
16 /* --------------------------------------------------------------------------
17 * Local function prototypes:
18 * ------------------------------------------------------------------------*/
20 static Cell local assumeEvid Args((Cell,Int));
22 static Cell local findIPEvid Args((Text));
23 static Void local removeIPEvid Args((Text));
24 static Void local matchupIPs Args((List,List));
26 static List local makePredAss Args((List,Int));
27 static List local copyPreds Args((List));
28 static Void local qualify Args((List,Cell));
29 static Void local qualifyBinding Args((List,Cell));
30 static Cell local qualifyExpr Args((Int,List,Cell));
31 static Void local overEvid Args((Cell,Cell));
33 static Void local cutoffExceeded Args((Cell,Int,Cell,Int,List));
34 static Cell local scFind Args((Cell,Cell,Int,Cell,Int,Int));
35 static Cell local scEntail Args((List,Cell,Int,Int));
36 static Cell local entail Args((List,Cell,Int,Int));
37 static Cell local inEntail Args((List,Cell,Int,Int));
39 static Cell local inEntails Args((List,Cell,Int,Int));
40 static Bool local instCompare Args((Inst, Inst));
43 static Cell local lacksNorm Args((Type,Int,Cell));
46 static List local scSimplify Args((List));
47 static Void local elimTauts Args((Void));
48 static Bool local anyGenerics Args((Type,Int));
49 static List local elimOuterPreds Args((List));
50 static List local elimPredsUsing Args((List,List));
51 static Void local reducePreds Args((Void));
52 static Void local normPreds Args((Int));
54 static Bool local resolveDefs Args((List));
55 static Bool local resolveVar Args((Int));
56 static Class local classConstraining Args((Int,Cell,Int));
57 static Bool local instComp_ Args((Inst,Inst));
59 /* --------------------------------------------------------------------------
60 * Predicate assignments:
62 * A predicate assignment is represented by a list of triples (pi,o,ev)
63 * where o is the offset for types in pi, with evidence required at the
64 * node pointed to by ev (which is taken as a dictionary parameter if
65 * no other evidence is available). Note that the ev node will be
66 * overwritten at a later stage if evidence for that predicate is found
68 * ------------------------------------------------------------------------*/
70 static List preds; /* Current predicate assignment */
72 static Cell local assumeEvid(pi,o) /* Add predicate pi (offset o) to */
73 Cell pi; /* preds with new dict var nd */
75 Cell nd = inventDictVar();
76 preds = cons(triple(pi,mkInt(o),nd),preds);
81 static Cell local findIPEvid(t)
84 for (; nonNull(ps); ps=tl(ps)) {
86 if (ipMatch(fst3(p), t))
92 static Void local removeIPEvid(t)
96 for (; nonNull(ps); ps = tl(ps))
97 if (ipMatch(fst3(hd(ps)), t)) {
107 static List local makePredAss(qs,o) /* Make list of predicate assumps. */
108 List qs; /* from qs (offset o), w/ new dict */
109 Int o; { /* vars for each predicate */
111 for (; nonNull(qs); qs=tl(qs))
112 result = cons(triple(hd(qs),mkInt(o),inventDictVar()),result);
116 static List local copyPreds(qs) /* Copy list of predicates */
119 for (; nonNull(qs); qs=tl(qs)) {
121 result = cons(copyPred(fst3(pi),intOf(snd3(pi))),result);
126 static Void local qualify(qs,alt) /* Add extra dictionary args to */
127 List qs; /* qualify alt by predicates in qs */
128 Cell alt; { /* :: ([Pat],Rhs) */
130 for (ds=NIL; nonNull(qs); qs=tl(qs))
131 ds = cons(thd3(hd(qs)),ds);
132 fst(alt) = revOnto(ds,fst(alt));
135 static Void local qualifyBinding(qs,b) /* Add extra dict args to each */
136 List qs; /* alternative in function binding */
138 if (!isVar(fst(b))) /* check for function binding */
139 internal("qualifyBinding");
140 map1Proc(qualify,qs,snd(snd(b)));
143 static Cell local qualifyExpr(l,ps,e) /* Add dictionary params to expr */
147 if (nonNull(ps)) { /* Qualify input expression with */
148 if (whatIs(e)!=LAMBDA) /* additional dictionary params */
149 e = ap(LAMBDA,pair(NIL,pair(mkInt(l),e)));
155 static Void local overEvid(dv,ev) /* Overwrite dict var dv with */
156 Cell dv; /* evidence ev */
162 /* --------------------------------------------------------------------------
163 * Predicate entailment:
165 * Entailment plays a prominent role in the theory of qualified types, and
166 * so, unsurprisingly, in the implementation too. For practical reasons,
167 * we break down entailment into two pieces. The first, scEntail, uses
168 * only the information provided by class declarations, while the second,
169 * entail, also uses the information in instance declarations.
171 * scEntail uses the following auxiliary function to do its work:
173 * scFind (e : pi') pi : Find evidence for predicate pi using only
174 * equality of predicates, superclass entailment,
175 * and the evidence e for pi'.
177 * scFind (e : pi') pi =
182 * if (pi.class.level < pi'.class.level)
183 * get superclass entailment pi' ||- P
184 * for each (sc, pi0) in P
185 * if (ev := scFind (sc e : pi0) pi) /= NIL
190 * This code assumes that the class hierarchy is acyclic, and that
191 * each class has been assigned a `level', which is its height in
192 * the hierachy. The first of the assumptions guarantees that the
193 * algorithm will terminate. The comparison of levels is an
194 * optimization that cuts down the search space: given that superclass
195 * entailments can only be used to descend the hierarchy, there is no
196 * way we can reach a higher level than the one that we start with,
197 * and hence there is no point in looking if we reach such a position.
199 * scEntail extends scFind to work on whole predicate assignments:
201 * scEntail P pi : Find evidence for predicate pi using the evidence
202 * provided by the predicate assignment P, and using
203 * only superclass entailments.
207 * for each (v:pi') in P
208 * if (ev := scFind (v:pi') pi) /= NIL
212 * ------------------------------------------------------------------------*/
214 Int cutoff = 64; /* Used to limit depth of recursion*/
216 static Void local cutoffExceeded(pi,o,pi1,o1,ps)
217 Cell pi, pi1; /* Display error msg when cutoff */
222 "\n*** The type checker has reached the cutoff limit while trying to\n"
224 "*** determine whether:\n*** " ETHEN ERRPRED(copyPred(pi,o));
225 ps = (isNull(pi1)) ? copyPreds(ps) : singleton(copyPred(pi1,o1));
227 "\n*** can be deduced from:\n*** " ETHEN ERRCONTEXT(ps);
229 "\n*** This may indicate that the problem is undecidable. However,\n"
231 "*** you may still try to increase the cutoff limit using the -c\n"
233 "*** option and then try again. (The current setting is -c%d)\n",
238 static Cell local scFind(e,pi1,o1,pi,o,d)/* Use superclass entailment to */
239 Cell e; /* find evidence for (pi,o) using */
240 Cell pi1; /* the evidence e for (pi1,o1). */
245 Class h1 = getHead(pi1);
246 Class h = getHead(pi);
248 /* the h==h1 test is just an optimization, and I'm not
249 sure it will work with IPs, so I'm being conservative
250 and commenting it out */
251 if (/* h==h1 && */ samePred(pi1,o1,pi,o))
254 /* the cclass.level test is also an optimization */
255 if (isClass(h1) && (!isClass(h) || cclass(h).level<cclass(h1).level)) {
256 Int beta = newKindedVars(cclass(h1).kinds);
257 List scs = cclass(h1).supers;
258 List dsels = cclass(h1).dsels;
259 if (!matchPred(pi1,o1,cclass(h1).head,beta))
263 cutoffExceeded(pi,o,pi1,o1,NIL);
265 for (; nonNull(scs); scs=tl(scs), dsels=tl(dsels)) {
266 Cell ev = scFind(ap(hd(dsels),e),hd(scs),beta,pi,o,d);
275 static Cell local scEntail(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/
276 List ps; /* Using superclasses and equality.*/
280 for (; nonNull(ps); ps=tl(ps)) {
282 Cell ev = scFind(thd3(pi1),fst3(pi1),intOf(snd3(pi1)),pi,o,d);
290 static Cell local ipEntail(ps,ip,o) /* Find evidence for (ip,o) from ps*/
294 Class h = getHead(ip);
296 for (; nonNull(ps); ps=tl(ps)) {
298 Cell pi1 = fst3(pr1);
299 Int o1 = intOf(snd3(pr1));
300 Class h1 = getHead(pi1);
302 if (textOf(h1) == textOf(h)) {
303 if (unify(arg(pi1),o1,arg(ip),o)) {
306 ERRMSG(0) "Mismatching uses of implicit parameter\n" ETHEN
307 ERRPRED(copyPred(pi1,o1));
309 ERRPRED(copyPred(ip,o));
320 /* --------------------------------------------------------------------------
321 * Now we reach the main entailment routine:
323 * entail P pi : Find evidence for predicate pi using the evidence
324 * provided by the predicate assignment P.
328 * if (ev := scEntail P pi) /= NIL
331 * if there is an instance entailment i : Q ||- pi
333 * if (ev := entail P pi') /= NIL
341 * The form of evidence expressions produced by scEntail can be described
344 * e = v | sc e (v = evidence var, sc = superclass sel)
346 * while entail extends this to include dictionary expressions given by:
348 * d = e | mki d1 ... dn (mki = dictionary constructor)
350 * A full grammar for evidence expressions is:
352 * d = v | sc d | mki d1 ... dn
354 * and this includes evidence expressions of the form sc (mki d1 ... dn)
355 * that can never be produced by either of the entail functions described
356 * above. This is good, from a practical perspective, because t means
357 * that we won't waste effort building a dictionary (mki d1 ... dn) only
358 * to extract just one superclass component and throw the rest away.
359 * Moreover, conditions on instance decls already guarantee that any
360 * expression of this form can be rewritten in the form mki' d1' ... dn'.
361 * (Minor point: they don't guarantee that such rewritings will lead to
362 * smaller terms, and hence to termination. However, we have already
363 * accepted the benefits of an undecidable entailment relation over
364 * guarantees of termination, and this additional quirk is unlikely
365 * to cause any further concern, except in pathological cases.)
366 * ------------------------------------------------------------------------*/
368 static Cell local entail(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/
369 List ps; /* Uses superclasses, equality, */
370 Cell pi; /* tautology, and construction */
373 Cell ev = scEntail(ps,pi,o,d);
374 return nonNull(ev) ? ev :
376 multiInstRes ? inEntails(ps,pi,o,d) :
383 static Cell local inEntail(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/
384 List ps; /* using a top-level instance */
385 Cell pi; /* entailment */
389 if (isAp(pi) && isExt(fun(pi))) { /* Lacks predicates */
392 l = lacksNorm(arg(pi),o,e);
393 if (isNull(l) || isInt(l))
397 for (; nonNull(qs); qs=tl(qs)) {
398 Cell qi = fst3(hd(qs));
399 if (isAp(qi) && fun(qi)==e) {
400 Cell lq = lacksNorm(arg(qi),intOf(snd3(hd(qs))),e);
401 if (isAp(lq) && intOf(fst(l))==intOf(fst(lq))) {
402 Int f = intOf(snd(l)) - intOf(snd(lq));
403 return (f==0) ? thd3(hd(qs)) : ap2(nameAddEv,
414 Inst in = findInstFor(pi,o); /* Class predicates */
418 Cell e = inst(in).builder;
419 Cell es = inst(in).specifics;
421 cutoffExceeded(pi,o,NIL,0,ps);
422 for (; nonNull(es); es=tl(es)) {
423 Cell ev = entail(ps,hd(es),beta,d);
438 static Cell local inEntails(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/
439 List ps; /* using a top-level instance */
440 Cell pi; /* entailment */
445 Cell ins; /* Class predicates */
451 if (isAp(pi) && isExt(fun(pi))) { /* Lacks predicates */
454 l = lacksNorm(arg(pi),o,e);
455 if (isNull(l) || isInt(l))
459 for (; nonNull(qs); qs=tl(qs)) {
460 Cell qi = fst3(hd(qs));
461 if (isAp(qi) && fun(qi)==e) {
462 Cell lq = lacksNorm(arg(qi),intOf(snd3(hd(qs))),e);
463 if (isAp(lq) && intOf(fst(l))==intOf(fst(lq))) {
464 Int f = intOf(snd(l)) - intOf(snd(lq));
465 return (f==0) ? thd3(hd(qs)) : ap2(nameAddEv,
477 cutoffExceeded(pi,o,NIL,0,ps);
479 #if EXPLAIN_INSTANCE_RESOLUTION
481 pi_ = copyPred(pi, o);
482 for (i = 0; i < d; i++)
484 fputs("inEntails: ", stdout);
485 printPred(stdout, pi_);
490 ins = findInstsFor(pi,o);
491 for (; nonNull(ins); ins=tl(ins)) {
494 Int beta = fst(hd(ins));
495 Cell e = inst(in).builder;
496 Cell es = inst(in).specifics;
499 #if EXPLAIN_INSTANCE_RESOLUTION
501 for (i = 0; i < d; i++)
503 fputs("try ", stdout);
504 printContext(stdout, es);
505 fputs(" => ", stdout);
506 printPred(stdout, inst(in).head);
511 for (; nonNull(es); es=tl(es)) {
512 Cell ev = entail(ps,hd(es),beta,d);
520 #if EXPLAIN_INSTANCE_RESOLUTION
522 for (i = 0; i < d; i++)
526 #if EXPLAIN_INSTANCE_RESOLUTION
528 fprintf(stdout, "Sat\n");
531 if (instCompare (in_, in)) {
532 ERRMSG(0) "Multiple satisfiable instances for "
534 ERRPRED(copyPred(pi, o));
535 ERRTEXT "\nin_ " ETHEN ERRPRED(inst(in_).head);
536 ERRTEXT "\nin " ETHEN ERRPRED(inst(in).head);
547 #if EXPLAIN_INSTANCE_RESOLUTION
549 fprintf(stdout, "not Sat\n");
554 #if EXPLAIN_INSTANCE_RESOLUTION
556 for (i = 0; i < d; i++)
558 fprintf(stdout, "not Sat.\n");
564 #if EXPLAIN_INSTANCE_RESOLUTION
566 for (i = 0; i < d; i++)
568 fprintf(stdout, "all not Sat.\n");
577 static Bool local instComp_(ia,ib) /* See if ia is an instance of ib */
579 Int alpha = newKindedVars(inst(ia).kinds);
580 Int beta = newKindedVars(inst(ib).kinds);
581 return matchPred(inst(ia).head,alpha,inst(ib).head,beta);
584 static Bool local instCompare (ia, ib)
587 return instComp_(ia, ib) && instComp_(ib, ia);
591 Cell provePred(ks,ps,pi) /* Find evidence for predicate pi */
592 Kinds ks; /* assuming ps. If ps is null, */
593 List ps; /* then we get to decide whether */
594 Cell pi; { /* is tautological, and we can use */
595 Int beta; /* the evidence as a dictionary. */
598 beta = newKindedVars(ks); /* (ks provides kinds for any */
599 ps = makePredAss(ps,beta); /* vars that appear in pi.) */
600 ev = entail(ps,pi,beta,0);
606 static Cell local lacksNorm(t,o,e) /* Normalize lacks pred (t,o)\l */
607 Type t; /* returning NIL (unsatisfiable), */
608 Int o; /* Int (tautological) or pair (v,a)*/
609 Cell e; { /* such that, if e is evid for v\l,*/
610 Text l = extText(e); /* then (e+a) is evid for (t,o)\l. */
616 return pair(mkInt(tyvNum(tyv)),mkInt(a));
618 Cell h = getDerefHead(t,o);
619 if (h==typeNoRow && argCount==0)
621 else if (isExt(h) && argCount==2) {
622 Text l1 = extText(h);
625 else if (strcmp(textToStr(l1),textToStr(l))<0)
636 /* --------------------------------------------------------------------------
637 * Predicate set Simplification:
639 * Calculate a minimal equivalent subset of a given set of predicates.
640 * ------------------------------------------------------------------------*/
642 static List local scSimplify(qs) /* Simplify predicates in qs, */
643 List qs; { /* returning equiv minimal subset */
648 Cell ev = scEntail(tl(qs),fst3(pi),intOf(snd3(pi)),0);
650 overEvid(thd3(pi),ev); /* Overwrite dict var with evidence*/
651 qs = tl(qs); /* ... and discard predicate */
653 else { /* Otherwise, retain predicate */
656 qs = appendOnto(tmp,qs);
662 List simpleContext(ps,o) /* Simplify context of skeletons */
663 List ps; /* skeletons, offset o, using */
664 Int o; { /* superclass hierarchy */
665 return copyPreds(scSimplify(makePredAss(ps,o)));
668 /* --------------------------------------------------------------------------
669 * Context splitting --- tautological and locally tautological predicates:
670 * ------------------------------------------------------------------------*/
672 static Void local elimTauts() { /* Remove tautological constraints */
673 if (haskell98) { /* from preds */
674 reducePreds(); /* (or context reduce for Hask98) */
678 while (nonNull(ps)) {
680 Cell ev = entail(NIL,fst3(pi),intOf(snd3(pi)),0);
682 overEvid(thd3(pi),ev);
695 static Int numFixedVars = 0; /* Number of fixed vars found */
697 static Bool local anyGenerics(t,o) /* Test for generic vars, and count*/
698 Type t; /* fixed variables */
700 Type h = getDerefHead(t,o); /* This code is careful to expand */
701 Int a = argCount; /* synonyms; mark* & copy* do not. */
702 if (isSynonym(h) && a>=tycon(h).arity) {
703 expandSyn(h,a,&t,&o);
704 return anyGenerics(t,o);
708 for (; 0<a--; t=fun(t)) { /* cycle through any arguments */
710 if (anyGenerics(arg(t),o))
715 if (tyv->offs == FIXED_TYVAR) {
727 static List local elimOuterPreds(sps) /* Simplify and defer any remaining*/
728 List sps; { /* preds that contain no generics. */
731 for (preds=scSimplify(preds); nonNull(preds); ) {
734 if (anyGenerics(fst3(pi),intOf(snd3(pi)))
736 || isIP(fun(fst3(pi)))) {
737 tl(preds) = qs; /* Retain predicate*/
740 else { /* Defer predicate */
750 static List local elimPredsUsing(ps,sps)/* Try to discharge or defer preds,*/
751 List ps; /* splitting if necessary to match */
752 List sps; { /* context ps. sps = savePreds. */
754 while (nonNull(preds)) { /* Pick a predicate from preds */
756 Cell pi = fst3(hd(p));
757 Int o = intOf(snd3(hd(p)));
758 Cell ev = entail(ps,pi,o,0);
761 if (nonNull(ev)) { /* Discharge if ps ||- (pi,o) */
762 overEvid(thd3(hd(p)),ev);
763 } else if (!isAp(pi) || isIP(fun(pi)) || !anyGenerics(pi,o)) {
764 tl(p) = sps; /* Defer if no generics */
767 else { /* Try to split generics and fixed */
769 if (numFixedVars>0 && nonNull(in=findInstFor(pi,o))) {
770 List qs = inst(in).specifics;
771 for (ev=inst(in).builder; nonNull(qs); qs=tl(qs))
772 ev = ap(ev,assumeEvid(hd(qs),typeOff));
773 overEvid(thd3(hd(p)),ev);
775 else { /* No worthwhile progress possible */
781 preds = rems; /* Return any remaining predicates */
785 static Void local reducePreds() { /* Context reduce predicates: uggh!*/
786 List rems = NIL; /* (A last resort for defaulting) */
787 while (nonNull(preds)) { /* Pick a predicate from preds */
789 Cell pi = fst3(hd(p));
790 Int o = intOf(snd3(hd(p)));
795 ins = findInstsFor(pi,o);
796 in = nonNull(ins) && isNull(tl(ins)) ? hd(ins) : NIL;
799 in = findInstFor(pi,o);
802 List qs = inst(in).specifics;
803 Cell ev = inst(in).builder;
804 for (; nonNull(qs); qs=tl(qs))
805 ev = ap(ev,assumeEvid(hd(qs),typeOff));
806 overEvid(thd3(hd(p)),ev);
808 else { /* No worthwhile progress possible */
813 preds = scSimplify(rems); /* Return any remaining predicates */
816 static Void local normPreds(line) /* Normalize each element of preds */
817 Int line; { /* in some appropriate manner */
821 while (nonNull(ps)) {
822 Cell pi = fst3(hd(ps));
823 Cell ev = thd3(hd(ps));
824 if (isAp(pi) && isExt(fun(pi))) {
825 Cell r = lacksNorm(arg(pi),intOf(snd3(hd(ps))),fun(pi));
827 ERRMSG(line) "Cannot satisfy constraint " ETHEN
828 ERRPRED(copyPred(pi,intOf(snd3(hd(ps)))));
840 else if (intOf(snd(r))!=0) {
841 Cell nd = inventDictVar();
842 Cell ev1 = ap2(nameAddEv,snd(r),nd);
843 pi = ap(fun(pi),aVar);
844 hd(ps) = triple(pi,fst(r),nd);
850 fst3(hd(ps)) = ap(fun(pi),fst(r));
863 /* --------------------------------------------------------------------------
864 * Mechanisms for dealing with defaults:
865 * ------------------------------------------------------------------------*/
867 static Bool local resolveDefs(vs) /* Attempt to resolve defaults */
868 List vs; { /* for variables vs subject to */
869 List pvs = NIL; /* constraints in preds */
871 Bool defaulted = FALSE;
873 #ifdef DEBUG_DEFAULTS
874 Printf("Attempt to resolve variables ");
876 Printf(" with context ");
877 printContext(stdout,copyPreds(preds));
881 resetGenerics(); /* find type variables in ps */
882 for (; nonNull(qs); qs=tl(qs)) {
883 Cell pi = fst3(hd(qs));
884 Int o = intOf(snd3(hd(qs)));
885 for (; isAp(pi); pi=fun(pi))
886 pvs = genvarType(arg(pi),o,pvs);
889 for (; nonNull(pvs); pvs=tl(pvs)) { /* now try defaults */
890 Int vn = intOf(hd(pvs));
892 #ifdef DEBUG_DEFAULTS
893 Printf("is var %d included in ",vn);
898 if (!intIsMember(vn,vs))
899 defaulted |= resolveVar(vn);
900 #ifdef DEBUG_DEFAULTS
902 Printf("Yes, so no ambiguity!\n");
909 static Bool local resolveVar(vn) /* Determine whether an ambig. */
910 Int vn; { /* variable vn can be resolved */
911 List ps = preds; /* by default in the context of */
912 List cs = NIL; /* the predicates in ps */
913 Bool aNumClass = FALSE;
915 if (tyvar(vn)->bound == SKOLEM)
918 /* According to the Haskell definition, we can only default an ambiguous
919 * variable if the set of classes that constrain it:
920 * (a) includes at least one numeric class.
921 * (b) includes only numeric or standard classes.
922 * In addition, we will not allow a variable to be defaulted unless it
923 * appears only in predicates of the form (Class var).
926 #ifdef DEBUG_DEFAULTS
927 Printf("Trying to default variable %d\n",vn);
930 for (; nonNull(ps); ps=tl(ps)) {
932 Class c = classConstraining(vn,fst3(pi),intOf(snd3(pi)));
934 if (c==classRealFrac || c==classRealFloat ||
935 c==classFractional || c==classFloating ||
936 c==classReal || c==classIntegral || c==classNum)
938 else if (c!=classEq && c!=classOrd && c!=classShow &&
939 c!=classRead && c!=classIx && c!=classEnum &&
943 { Type t = arg(fst3(pi));/* Check for single var as arg */
944 Int o = intOf(snd3(pi));
947 if (!tyv || tyvNum(tyv)!=vn)
950 if (!cellIsMember(c,cs))
955 /* Now find the first class (if any) in the list of defaults that
956 * is an instance of all of the required classes.
958 * If we get this far, then cs only mentions classes from the list
959 * above, all of which have only a single parameter of kind *.
963 List ds = defaultDefns; /* N.B. guaranteed to be monotypes */
964 #ifdef DEBUG_DEFAULTS
965 Printf("Default conditions met, looking for type\n");
967 for (; nonNull(ds); ds=tl(ds)) {
969 while (nonNull(cs1) && nonNull(entail(NIL,ap(hd(cs1),hd(ds)),0,0)))
973 #ifdef DEBUG_DEFAULTS
974 Printf("Default type for variable %d is ",vn);
975 printType(stdout,hd(ds));
983 #ifdef DEBUG_DEFAULTS
984 Printf("No default permitted/found\n");
989 static Class local classConstraining(vn,pi,o)
990 Int vn; /* Return class constraining var*/
991 Cell pi; /* vn in predicate pi, or NIL if*/
992 Int o; { /* vn is not involved */
993 for (; isAp(pi); pi=fun(pi))
994 if (!doesntOccurIn(tyvar(vn),arg(pi),o))
999 /*-------------------------------------------------------------------------*/