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: 2000/03/13 11:37:16 $
14 * ------------------------------------------------------------------------*/
16 /* --------------------------------------------------------------------------
17 * Local function prototypes:
18 * ------------------------------------------------------------------------*/
20 static Cell local assumeEvid ( Cell,Int );
22 static Cell local findIPEvid ( Text );
23 static Void local removeIPEvid ( Text );
25 static List local makePredAss ( List,Int );
26 static List local copyPreds ( List );
27 static Void local qualify ( List,Cell );
28 static Void local qualifyBinding ( List,Cell );
29 static Cell local qualifyExpr ( Int,List,Cell );
30 static Void local overEvid ( Cell,Cell );
32 static Void local cutoffExceeded ( Cell,Int,List );
33 static Cell local scFind ( Cell,Cell,Int,Cell,Int,Int );
34 static Cell local scEntail ( List,Cell,Int,Int );
35 static Cell local entail ( List,Cell,Int,Int );
36 static Cell local inEntail ( List,Cell,Int,Int );
38 static Cell local inEntails ( List,Cell,Int,Int );
39 static Bool local instCompare ( Inst, Inst );
42 static Cell local lacksNorm ( Type,Int,Cell );
45 static List local scSimplify ( List );
46 static Void local elimTauts ( Void );
47 static Bool local anyGenerics ( Type,Int );
48 static List local elimOuterPreds ( List );
49 static List local elimPredsUsing ( List,List );
50 static Void local reducePreds ( Void );
51 static Void local normPreds ( Int );
53 static Bool local resolveDefs ( List );
54 static Bool local resolveVar ( Int );
55 static Class local classConstraining ( Int,Cell,Int );
56 static Bool local instComp_ ( Inst,Inst );
58 /* --------------------------------------------------------------------------
59 * Predicate assignments:
61 * A predicate assignment is represented by a list of triples (pi,o,ev)
62 * where o is the offset for types in pi, with evidence required at the
63 * node pointed to by ev (which is taken as a dictionary parameter if
64 * no other evidence is available). Note that the ev node will be
65 * overwritten at a later stage if evidence for that predicate is found
67 * ------------------------------------------------------------------------*/
69 static List preds; /* Current predicate assignment */
71 static Cell local assumeEvid(pi,o) /* Add predicate pi (offset o) to */
72 Cell pi; /* preds with new dict var nd */
74 Cell nd = inventDictVar();
75 preds = cons(triple(pi,mkInt(o),nd),preds);
80 static Cell local findIPEvid(t)
83 for (; nonNull(ps); ps=tl(ps)) {
85 if (ipMatch(fst3(p), t))
91 static Void local removeIPEvid(t)
95 for (; nonNull(ps); ps = tl(ps))
96 if (ipMatch(fst3(hd(ps)), t)) {
106 static List local makePredAss(qs,o) /* Make list of predicate assumps. */
107 List qs; /* from qs (offset o), w/ new dict */
108 Int o; { /* vars for each predicate */
110 for (; nonNull(qs); qs=tl(qs))
111 result = cons(triple(hd(qs),mkInt(o),inventDictVar()),result);
115 static List local copyPreds(qs) /* Copy list of predicates */
118 for (; nonNull(qs); qs=tl(qs)) {
120 result = cons(copyPred(fst3(pi),intOf(snd3(pi))),result);
125 static Void local qualify(qs,alt) /* Add extra dictionary args to */
126 List qs; /* qualify alt by predicates in qs */
127 Cell alt; { /* :: ([Pat],Rhs) */
129 for (ds=NIL; nonNull(qs); qs=tl(qs))
130 ds = cons(thd3(hd(qs)),ds);
131 fst(alt) = revOnto(ds,fst(alt));
134 static Void local qualifyBinding(qs,b) /* Add extra dict args to each */
135 List qs; /* alternative in function binding */
137 if (!isVar(fst(b))) /* check for function binding */
138 internal("qualifyBinding");
139 map1Proc(qualify,qs,snd(snd(b)));
142 static Cell local qualifyExpr(l,ps,e) /* Add dictionary params to expr */
146 if (nonNull(ps)) { /* Qualify input expression with */
147 if (whatIs(e)!=LAMBDA) /* additional dictionary params */
148 e = ap(LAMBDA,pair(NIL,pair(mkInt(l),e)));
154 static Void local overEvid(dv,ev) /* Overwrite dict var dv with */
155 Cell dv; /* evidence ev */
161 /* --------------------------------------------------------------------------
162 * Predicate entailment:
164 * Entailment plays a prominent role in the theory of qualified types, and
165 * so, unsurprisingly, in the implementation too. For practical reasons,
166 * we break down entailment into two pieces. The first, scEntail, uses
167 * only the information provided by class declarations, while the second,
168 * entail, also uses the information in instance declarations.
170 * scEntail uses the following auxiliary function to do its work:
172 * scFind (e : pi') pi : Find evidence for predicate pi using only
173 * equality of predicates, superclass entailment,
174 * and the evidence e for pi'.
176 * scFind (e : pi') pi =
181 * if (pi.class.level < pi'.class.level)
182 * get superclass entailment pi' ||- P
183 * for each (sc, pi0) in P
184 * if (ev := scFind (sc e : pi0) pi) /= NIL
189 * This code assumes that the class hierarchy is acyclic, and that
190 * each class has been assigned a `level', which is its height in
191 * the hierachy. The first of the assumptions guarantees that the
192 * algorithm will terminate. The comparison of levels is an
193 * optimization that cuts down the search space: given that superclass
194 * entailments can only be used to descend the hierarchy, there is no
195 * way we can reach a higher level than the one that we start with,
196 * and hence there is no point in looking if we reach such a position.
198 * scEntail extends scFind to work on whole predicate assignments:
200 * scEntail P pi : Find evidence for predicate pi using the evidence
201 * provided by the predicate assignment P, and using
202 * only superclass entailments.
206 * for each (v:pi') in P
207 * if (ev := scFind (v:pi') pi) /= NIL
211 * ------------------------------------------------------------------------*/
213 Int cutoff = 64; /* Used to limit depth of recursion*/
215 static Void local cutoffExceeded(pi,o,ps)
216 Cell pi; /* Display error msg when cutoff */
221 "\n*** The type checker has reached the cutoff limit while trying to\n"
223 "*** determine whether:\n*** " ETHEN ERRPRED(copyPred(pi,o));
226 "\n*** can be deduced from:\n*** " ETHEN ERRCONTEXT(ps);
228 "\n*** This may indicate that the problem is undecidable. However,\n"
230 "*** you may still try to increase the cutoff limit using the -c\n"
232 "*** option and then try again. (The current setting is -c%d)\n",
237 static Cell local scFind(e,pi1,o1,pi,o,d)/* Use superclass entailment to */
238 Cell e; /* find evidence for (pi,o) using */
239 Cell pi1; /* the evidence e for (pi1,o1). */
244 Class h1 = getHead(pi1);
245 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 if (isClass(h1) && (!isClass(h) || cclass(h).level<cclass(h1).level)) {
255 Int beta = newKindedVars(cclass(h1).kinds);
256 List scs = cclass(h1).supers;
257 List dsels = cclass(h1).dsels;
259 if (!matchPred(pi1,o1,cclass(h1).head,beta))
262 for (; nonNull(scs); scs=tl(scs), dsels=tl(dsels))
263 ps = cons(triple(hd(scs),mkInt(beta),ap(hd(dsels),e)),ps);
266 #if EXPLAIN_INSTANCE_RESOLUTION
269 for (i = 0; i < d; i++)
271 fputs("scEntail(scFind): ", stdout);
272 printContext(stdout,copyPreds(ps));
273 fputs(" ||- ", stdout);
274 printPred(stdout, copyPred(pi, o));
279 ev = scEntail(ps,pi,o,d);
280 #if EXPLAIN_INSTANCE_RESOLUTION
281 if (showInstRes && nonNull(ev)) {
283 for (i = 0; i < d; i++)
285 fputs("scSat.\n", stdout);
293 static Cell local scEntail(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/
294 List ps; /* Using superclasses and equality.*/
299 cutoffExceeded(pi,o,ps);
301 for (; nonNull(ps); ps=tl(ps)) {
303 Cell ev = scFind(thd3(pi1),fst3(pi1),intOf(snd3(pi1)),pi,o,d);
311 /* --------------------------------------------------------------------------
312 * Now we reach the main entailment routine:
314 * entail P pi : Find evidence for predicate pi using the evidence
315 * provided by the predicate assignment P.
319 * if (ev := scEntail P pi) /= NIL
322 * if there is an instance entailment i : Q ||- pi
324 * if (ev := entail P pi') /= NIL
332 * The form of evidence expressions produced by scEntail can be described
335 * e = v | sc e (v = evidence var, sc = superclass sel)
337 * while entail extends this to include dictionary expressions given by:
339 * d = e | mki d1 ... dn (mki = dictionary constructor)
341 * A full grammar for evidence expressions is:
343 * d = v | sc d | mki d1 ... dn
345 * and this includes evidence expressions of the form sc (mki d1 ... dn)
346 * that can never be produced by either of the entail functions described
347 * above. This is good, from a practical perspective, because t means
348 * that we won't waste effort building a dictionary (mki d1 ... dn) only
349 * to extract just one superclass component and throw the rest away.
350 * Moreover, conditions on instance decls already guarantee that any
351 * expression of this form can be rewritten in the form mki' d1' ... dn'.
352 * (Minor point: they don't guarantee that such rewritings will lead to
353 * smaller terms, and hence to termination. However, we have already
354 * accepted the benefits of an undecidable entailment relation over
355 * guarantees of termination, and this additional quirk is unlikely
356 * to cause any further concern, except in pathological cases.)
357 * ------------------------------------------------------------------------*/
359 static Cell local entail(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/
360 List ps; /* Uses superclasses, equality, */
361 Cell pi; /* tautology, and construction */
366 #if EXPLAIN_INSTANCE_RESOLUTION
369 for (i = 0; i < d; i++)
371 fputs("entail: ", stdout);
372 printContext(stdout,copyPreds(ps));
373 fputs(" ||- ", stdout);
374 printPred(stdout, copyPred(pi, o));
379 ev = scEntail(ps,pi,o,d);
381 #if EXPLAIN_INSTANCE_RESOLUTION
384 for (i = 0; i < d; i++)
386 fputs("scSat.\n", stdout);
392 multiInstRes ? inEntails(ps,pi,o,d) :
397 #if EXPLAIN_INSTANCE_RESOLUTION
398 if (nonNull(ev) && showInstRes) {
400 for (i = 0; i < d; i++)
402 fputs("inSat.\n", stdout);
409 static Cell local inEntail(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/
410 List ps; /* using a top-level instance */
411 Cell pi; /* entailment */
418 cutoffExceeded(pi,o,ps);
421 if (isAp(pi) && isExt(fun(pi))) { /* Lacks predicates */
424 l = lacksNorm(arg(pi),o,e);
425 if (isNull(l) || isInt(l))
429 for (; nonNull(qs); qs=tl(qs)) {
430 Cell qi = fst3(hd(qs));
431 if (isAp(qi) && fun(qi)==e) {
432 Cell lq = lacksNorm(arg(qi),intOf(snd3(hd(qs))),e);
433 if (isAp(lq) && intOf(fst(l))==intOf(fst(lq))) {
434 Int f = intOf(snd(l)) - intOf(snd(lq));
435 return (f==0) ? thd3(hd(qs)) : ap2(nameAddEv,
447 in = findInstFor(pi,o); /* Class predicates */
450 Cell e = inst(in).builder;
451 List es = inst(in).specifics;
453 for (; nonNull(es); es=tl(es))
454 fs = cons(triple(hd(es),mkInt(beta),NIL),fs);
457 #if EXPLAIN_INSTANCE_RESOLUTION
459 for (i = 0; i < d; i++)
461 fputs("try ", stdout);
462 printContext(stdout, copyPreds(fs));
463 fputs(" => ", stdout);
464 printPred(stdout, copyPred(inst(in).head,beta));
468 for (es=inst(in).specifics; nonNull(es); es=tl(es)) {
470 ev = entail(ps,hd(es),beta,d);
478 #if EXPLAIN_INSTANCE_RESOLUTION
481 for (i = 0; i < d; i++)
483 fputs("No instance found for ", stdout);
484 printPred(stdout, copyPred(pi, o));
496 static Cell local inEntails(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/
497 List ps; /* using a top-level instance */
498 Cell pi; /* entailment */
503 Cell ins; /* Class predicates */
508 cutoffExceeded(pi,o,ps);
511 if (isAp(pi) && isExt(fun(pi))) { /* Lacks predicates */
514 l = lacksNorm(arg(pi),o,e);
515 if (isNull(l) || isInt(l))
519 for (; nonNull(qs); qs=tl(qs)) {
520 Cell qi = fst3(hd(qs));
521 if (isAp(qi) && fun(qi)==e) {
522 Cell lq = lacksNorm(arg(qi),intOf(snd3(hd(qs))),e);
523 if (isAp(lq) && intOf(fst(l))==intOf(fst(lq))) {
524 Int f = intOf(snd(l)) - intOf(snd(lq));
525 return (f==0) ? thd3(hd(qs)) : ap2(nameAddEv,
537 #if EXPLAIN_INSTANCE_RESOLUTION
539 for (i = 0; i < d; i++)
541 fputs("inEntails: ", stdout);
542 printContext(stdout,copyPreds(ps));
543 fputs(" ||- ", stdout);
544 printPred(stdout, copyPred(pi, o));
549 ins = findInstsFor(pi,o);
550 for (; nonNull(ins); ins=tl(ins)) {
553 Int beta = fst(hd(ins));
554 Cell e = inst(in).builder;
555 Cell es = inst(in).specifics;
557 #if EXPLAIN_INSTANCE_RESOLUTION
559 for (i = 0; i < d; i++)
561 fputs("try ", stdout);
562 printContext(stdout, es);
563 fputs(" => ", stdout);
564 printPred(stdout, inst(in).head);
569 for (; nonNull(es); es=tl(es)) {
570 Cell ev = entail(ps,hd(es),beta,d);
578 #if EXPLAIN_INSTANCE_RESOLUTION
580 for (i = 0; i < d; i++)
584 #if EXPLAIN_INSTANCE_RESOLUTION
586 fprintf(stdout, "Sat\n");
589 if (instCompare (in_, in)) {
590 ERRMSG(0) "Multiple satisfiable instances for "
592 ERRPRED(copyPred(pi, o));
593 ERRTEXT "\nin_ " ETHEN ERRPRED(inst(in_).head);
594 ERRTEXT "\nin " ETHEN ERRPRED(inst(in).head);
605 #if EXPLAIN_INSTANCE_RESOLUTION
607 fprintf(stdout, "not Sat\n");
612 #if EXPLAIN_INSTANCE_RESOLUTION
614 for (i = 0; i < d; i++)
616 fprintf(stdout, "not Sat.\n");
622 #if EXPLAIN_INSTANCE_RESOLUTION
624 for (i = 0; i < d; i++)
626 fprintf(stdout, "all not Sat.\n");
635 static Bool local instComp_(ia,ib) /* See if ia is an instance of ib */
637 Int alpha = newKindedVars(inst(ia).kinds);
638 Int beta = newKindedVars(inst(ib).kinds);
639 return matchPred(inst(ia).head,alpha,inst(ib).head,beta);
642 static Bool local instCompare (ia, ib)
645 return instComp_(ia, ib) && instComp_(ib, ia);
649 Cell provePred(ks,ps,pi) /* Find evidence for predicate pi */
650 Kinds ks; /* assuming ps. If ps is null, */
651 List ps; /* then we get to decide whether */
652 Cell pi; { /* is tautological, and we can use */
653 Int beta; /* the evidence as a dictionary. */
656 beta = newKindedVars(ks); /* (ks provides kinds for any */
657 ps = makePredAss(ps,beta); /* vars that appear in pi.) */
658 ev = entail(ps,pi,beta,0);
664 static Cell local lacksNorm(t,o,e) /* Normalize lacks pred (t,o)\l */
665 Type t; /* returning NIL (unsatisfiable), */
666 Int o; /* Int (tautological) or pair (v,a)*/
667 Cell e; { /* such that, if e is evid for v\l,*/
668 Text l = extText(e); /* then (e+a) is evid for (t,o)\l. */
674 return pair(mkInt(tyvNum(tyv)),mkInt(a));
676 Cell h = getDerefHead(t,o);
677 if (h==typeNoRow && argCount==0)
679 else if (isExt(h) && argCount==2) {
680 Text l1 = extText(h);
683 else if (strcmp(textToStr(l1),textToStr(l))<0)
694 /* --------------------------------------------------------------------------
695 * Predicate set Simplification:
697 * Calculate a minimal equivalent subset of a given set of predicates.
698 * ------------------------------------------------------------------------*/
700 static List local scSimplify(qs) /* Simplify predicates in qs, */
701 List qs; { /* returning equiv minimal subset */
707 #if EXPLAIN_INSTANCE_RESOLUTION
709 fputs("scSimplify: ", stdout);
710 printContext(stdout,copyPreds(tl(qs)));
711 fputs(" ||- ", stdout);
712 printPred(stdout, copyPred(fst3(pi),intOf(snd3(pi))));
716 ev = scEntail(tl(qs),fst3(pi),intOf(snd3(pi)),0);
718 overEvid(thd3(pi),ev); /* Overwrite dict var with evidence*/
719 qs = tl(qs); /* ... and discard predicate */
721 else { /* Otherwise, retain predicate */
724 qs = appendOnto(tmp,qs);
730 List simpleContext(ps,o) /* Simplify context of skeletons */
731 List ps; /* skeletons, offset o, using */
732 Int o; { /* superclass hierarchy */
733 return copyPreds(scSimplify(makePredAss(ps,o)));
736 /* --------------------------------------------------------------------------
737 * Context splitting --- tautological and locally tautological predicates:
738 * ------------------------------------------------------------------------*/
740 static Void local elimTauts() { /* Remove tautological constraints */
741 if (haskell98) { /* from preds */
742 reducePreds(); /* (or context reduce for Hask98) */
746 while (nonNull(ps)) {
748 Cell ev = entail(NIL,fst3(pi),intOf(snd3(pi)),0);
750 overEvid(thd3(pi),ev);
763 static Int numFixedVars = 0; /* Number of fixed vars found */
765 static Bool local anyGenerics(t,o) /* Test for generic vars, and count*/
766 Type t; /* fixed variables */
768 Type h = getDerefHead(t,o); /* This code is careful to expand */
769 Int a = argCount; /* synonyms; mark* & copy* do not. */
770 if (isSynonym(h) && a>=tycon(h).arity) {
771 expandSyn(h,a,&t,&o);
772 return anyGenerics(t,o);
776 for (; 0<a--; t=fun(t)) { /* cycle through any arguments */
778 if (anyGenerics(arg(t),o))
783 if (tyv->offs == FIXED_TYVAR) {
795 static List local elimOuterPreds(sps) /* Simplify and defer any remaining*/
796 List sps; { /* preds that contain no generics. */
799 for (preds=scSimplify(preds); nonNull(preds); ) {
802 if (anyGenerics(fst3(pi),intOf(snd3(pi)))
804 || isIP(fun(fst3(pi)))) {
805 tl(preds) = qs; /* Retain predicate*/
808 else { /* Defer predicate */
818 static List local elimPredsUsing(ps,sps)/* Try to discharge or defer preds,*/
819 List ps; /* splitting if necessary to match */
820 List sps; { /* context ps. sps = savePreds. */
822 while (nonNull(preds)) { /* Pick a predicate from preds */
824 Cell pi = fst3(hd(p));
825 Int o = intOf(snd3(hd(p)));
826 Cell ev = entail(ps,pi,o,0);
829 if (nonNull(ev)) { /* Discharge if ps ||- (pi,o) */
830 overEvid(thd3(hd(p)),ev);
831 } else if (isIP(fun(pi))) {
834 } else if (!isAp(pi) || !anyGenerics(pi,o)) {
835 tl(p) = sps; /* Defer if no generics */
838 else { /* Try to split generics and fixed */
840 if (numFixedVars>0 && nonNull(in=findInstFor(pi,o))) {
841 List qs = inst(in).specifics;
842 for (ev=inst(in).builder; nonNull(qs); qs=tl(qs))
843 ev = ap(ev,assumeEvid(hd(qs),typeOff));
844 overEvid(thd3(hd(p)),ev);
846 else { /* No worthwhile progress possible */
852 preds = rems; /* Return any remaining predicates */
856 static Void local reducePreds() { /* Context reduce predicates: uggh!*/
857 List rems = NIL; /* (A last resort for defaulting) */
858 while (nonNull(preds)) { /* Pick a predicate from preds */
860 Cell pi = fst3(hd(p));
861 Int o = intOf(snd3(hd(p)));
866 ins = findInstsFor(pi,o);
867 in = nonNull(ins) && isNull(tl(ins)) ? snd(hd(ins)) : NIL;
870 in = findInstFor(pi,o);
873 List qs = inst(in).specifics;
874 Cell ev = inst(in).builder;
875 for (; nonNull(qs); qs=tl(qs))
876 ev = ap(ev,assumeEvid(hd(qs),typeOff));
877 overEvid(thd3(hd(p)),ev);
879 else { /* No worthwhile progress possible */
884 preds = scSimplify(rems); /* Return any remaining predicates */
887 static Void local normPreds(line) /* Normalize each element of preds */
888 Int line; { /* in some appropriate manner */
892 while (nonNull(ps)) {
893 Cell pi = fst3(hd(ps));
894 Cell ev = thd3(hd(ps));
895 if (isAp(pi) && isExt(fun(pi))) {
896 Cell r = lacksNorm(arg(pi),intOf(snd3(hd(ps))),fun(pi));
898 ERRMSG(line) "Cannot satisfy constraint " ETHEN
899 ERRPRED(copyPred(pi,intOf(snd3(hd(ps)))));
911 else if (intOf(snd(r))!=0) {
912 Cell nd = inventDictVar();
913 Cell ev1 = ap2(nameAddEv,snd(r),nd);
914 pi = ap(fun(pi),aVar);
915 hd(ps) = triple(pi,fst(r),nd);
921 fst3(hd(ps)) = ap(fun(pi),fst(r));
934 /* --------------------------------------------------------------------------
935 * Mechanisms for dealing with defaults:
936 * ------------------------------------------------------------------------*/
938 static Bool local resolveDefs(vs) /* Attempt to resolve defaults */
939 List vs; { /* for variables vs subject to */
940 List pvs = NIL; /* constraints in preds */
942 Bool defaulted = FALSE;
944 #ifdef DEBUG_DEFAULTS
945 Printf("Attempt to resolve variables ");
947 Printf(" with context ");
948 printContext(stdout,copyPreds(preds));
952 resetGenerics(); /* find type variables in ps */
953 for (; nonNull(qs); qs=tl(qs)) {
954 Cell pi = fst3(hd(qs));
955 Int o = intOf(snd3(hd(qs)));
956 for (; isAp(pi); pi=fun(pi))
957 pvs = genvarType(arg(pi),o,pvs);
960 for (; nonNull(pvs); pvs=tl(pvs)) { /* now try defaults */
961 Int vn = intOf(hd(pvs));
963 #ifdef DEBUG_DEFAULTS
964 Printf("is var %d included in ",vn);
969 if (!intIsMember(vn,vs))
970 defaulted |= resolveVar(vn);
971 #ifdef DEBUG_DEFAULTS
973 Printf("Yes, so no ambiguity!\n");
980 static Bool local resolveVar(vn) /* Determine whether an ambig. */
981 Int vn; { /* variable vn can be resolved */
982 List ps = preds; /* by default in the context of */
983 List cs = NIL; /* the predicates in ps */
984 Bool aNumClass = FALSE;
986 if (tyvar(vn)->bound == SKOLEM)
989 /* According to the Haskell definition, we can only default an ambiguous
990 * variable if the set of classes that constrain it:
991 * (a) includes at least one numeric class.
992 * (b) includes only numeric or standard classes.
993 * In addition, we will not allow a variable to be defaulted unless it
994 * appears only in predicates of the form (Class var).
997 #ifdef DEBUG_DEFAULTS
998 Printf("Trying to default variable %d\n",vn);
1001 for (; nonNull(ps); ps=tl(ps)) {
1003 Class c = classConstraining(vn,fst3(pi),intOf(snd3(pi)));
1005 if (c==classRealFrac || c==classRealFloat ||
1006 c==classFractional || c==classFloating ||
1007 c==classReal || c==classIntegral || c==classNum)
1009 else if (c!=classEq && c!=classOrd && c!=classShow &&
1010 c!=classRead && c!=classIx && c!=classEnum &&
1014 { Type t = arg(fst3(pi));/* Check for single var as arg */
1015 Int o = intOf(snd3(pi));
1018 if (!tyv || tyvNum(tyv)!=vn)
1021 if (!cellIsMember(c,cs))
1026 /* Now find the first class (if any) in the list of defaults that
1027 * is an instance of all of the required classes.
1029 * If we get this far, then cs only mentions classes from the list
1030 * above, all of which have only a single parameter of kind *.
1034 List ds = defaultDefns; /* N.B. guaranteed to be monotypes */
1035 #ifdef DEBUG_DEFAULTS
1036 Printf("Default conditions met, looking for type\n");
1038 for (; nonNull(ds); ds=tl(ds)) {
1040 while (nonNull(cs1) && nonNull(entail(NIL,ap(hd(cs1),hd(ds)),0,0)))
1043 bindTv(vn,hd(ds),0);
1044 #ifdef DEBUG_DEFAULTS
1045 Printf("Default type for variable %d is ",vn);
1046 printType(stdout,hd(ds));
1054 #ifdef DEBUG_DEFAULTS
1055 Printf("No default permitted/found\n");
1060 static Class local classConstraining(vn,pi,o)
1061 Int vn; /* Return class constraining var*/
1062 Cell pi; /* vn in predicate pi, or NIL if*/
1063 Int o; { /* vn is not involved */
1064 for (; isAp(pi); pi=fun(pi))
1065 if (!doesntOccurIn(tyvar(vn),arg(pi),o))
1070 /*-------------------------------------------------------------------------*/