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/11/17 16:57:43 $
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));
25 static List local makePredAss Args((List,Int));
26 static List local copyPreds Args((List));
27 static Void local qualify Args((List,Cell));
28 static Void local qualifyBinding Args((List,Cell));
29 static Cell local qualifyExpr Args((Int,List,Cell));
30 static Void local overEvid Args((Cell,Cell));
32 static Void local cutoffExceeded Args((Cell,Int,List));
33 static Cell local scFind Args((Cell,Cell,Int,Cell,Int,Int));
34 static Cell local scEntail Args((List,Cell,Int,Int));
35 static Cell local entail Args((List,Cell,Int,Int));
36 static Cell local inEntail Args((List,Cell,Int,Int));
38 static Cell local inEntails Args((List,Cell,Int,Int));
39 static Bool local instCompare Args((Inst, Inst));
42 static Cell local lacksNorm Args((Type,Int,Cell));
45 static List local scSimplify Args((List));
46 static Void local elimTauts Args((Void));
47 static Bool local anyGenerics Args((Type,Int));
48 static List local elimOuterPreds Args((List));
49 static List local elimPredsUsing Args((List,List));
50 static Void local reducePreds Args((Void));
51 static Void local normPreds Args((Int));
53 static Bool local resolveDefs Args((List));
54 static Bool local resolveVar Args((Int));
55 static Class local classConstraining Args((Int,Cell,Int));
56 static Bool local instComp_ Args((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 Cell es = inst(in).specifics;
452 #if EXPLAIN_INSTANCE_RESOLUTION
454 for (i = 0; i < d; i++)
456 fputs("try ", stdout);
457 printContext(stdout, es);
458 fputs(" => ", stdout);
459 printPred(stdout, inst(in).head);
463 /* would need to lift es to triples, so be lazy, and just
464 use improve1 in the loop */
465 /* improve(0,ps,es); */
466 for (; nonNull(es); es=tl(es)) {
468 improve1(0,ps,hd(es),beta);
469 ev = entail(ps,hd(es),beta,d);
477 #if EXPLAIN_INSTANCE_RESOLUTION
480 for (i = 0; i < d; i++)
482 fputs("No instance found for ", stdout);
483 printPred(stdout, copyPred(pi, o));
495 static Cell local inEntails(ps,pi,o,d) /* Calc evidence for (pi,o) from ps*/
496 List ps; /* using a top-level instance */
497 Cell pi; /* entailment */
502 Cell ins; /* Class predicates */
507 cutoffExceeded(pi,o,ps);
510 if (isAp(pi) && isExt(fun(pi))) { /* Lacks predicates */
513 l = lacksNorm(arg(pi),o,e);
514 if (isNull(l) || isInt(l))
518 for (; nonNull(qs); qs=tl(qs)) {
519 Cell qi = fst3(hd(qs));
520 if (isAp(qi) && fun(qi)==e) {
521 Cell lq = lacksNorm(arg(qi),intOf(snd3(hd(qs))),e);
522 if (isAp(lq) && intOf(fst(l))==intOf(fst(lq))) {
523 Int f = intOf(snd(l)) - intOf(snd(lq));
524 return (f==0) ? thd3(hd(qs)) : ap2(nameAddEv,
536 #if EXPLAIN_INSTANCE_RESOLUTION
538 for (i = 0; i < d; i++)
540 fputs("inEntails: ", stdout);
541 printContext(stdout,copyPreds(ps));
542 fputs(" ||- ", stdout);
543 printPred(stdout, copyPred(pi, o));
548 ins = findInstsFor(pi,o);
549 for (; nonNull(ins); ins=tl(ins)) {
552 Int beta = fst(hd(ins));
553 Cell e = inst(in).builder;
554 Cell es = inst(in).specifics;
556 #if EXPLAIN_INSTANCE_RESOLUTION
558 for (i = 0; i < d; i++)
560 fputs("try ", stdout);
561 printContext(stdout, es);
562 fputs(" => ", stdout);
563 printPred(stdout, inst(in).head);
568 for (; nonNull(es); es=tl(es)) {
569 Cell ev = entail(ps,hd(es),beta,d);
577 #if EXPLAIN_INSTANCE_RESOLUTION
579 for (i = 0; i < d; i++)
583 #if EXPLAIN_INSTANCE_RESOLUTION
585 fprintf(stdout, "Sat\n");
588 if (instCompare (in_, in)) {
589 ERRMSG(0) "Multiple satisfiable instances for "
591 ERRPRED(copyPred(pi, o));
592 ERRTEXT "\nin_ " ETHEN ERRPRED(inst(in_).head);
593 ERRTEXT "\nin " ETHEN ERRPRED(inst(in).head);
604 #if EXPLAIN_INSTANCE_RESOLUTION
606 fprintf(stdout, "not Sat\n");
611 #if EXPLAIN_INSTANCE_RESOLUTION
613 for (i = 0; i < d; i++)
615 fprintf(stdout, "not Sat.\n");
621 #if EXPLAIN_INSTANCE_RESOLUTION
623 for (i = 0; i < d; i++)
625 fprintf(stdout, "all not Sat.\n");
634 static Bool local instComp_(ia,ib) /* See if ia is an instance of ib */
636 Int alpha = newKindedVars(inst(ia).kinds);
637 Int beta = newKindedVars(inst(ib).kinds);
638 return matchPred(inst(ia).head,alpha,inst(ib).head,beta);
641 static Bool local instCompare (ia, ib)
644 return instComp_(ia, ib) && instComp_(ib, ia);
648 Cell provePred(ks,ps,pi) /* Find evidence for predicate pi */
649 Kinds ks; /* assuming ps. If ps is null, */
650 List ps; /* then we get to decide whether */
651 Cell pi; { /* is tautological, and we can use */
652 Int beta; /* the evidence as a dictionary. */
655 beta = newKindedVars(ks); /* (ks provides kinds for any */
656 ps = makePredAss(ps,beta); /* vars that appear in pi.) */
657 ev = entail(ps,pi,beta,0);
663 static Cell local lacksNorm(t,o,e) /* Normalize lacks pred (t,o)\l */
664 Type t; /* returning NIL (unsatisfiable), */
665 Int o; /* Int (tautological) or pair (v,a)*/
666 Cell e; { /* such that, if e is evid for v\l,*/
667 Text l = extText(e); /* then (e+a) is evid for (t,o)\l. */
673 return pair(mkInt(tyvNum(tyv)),mkInt(a));
675 Cell h = getDerefHead(t,o);
676 if (h==typeNoRow && argCount==0)
678 else if (isExt(h) && argCount==2) {
679 Text l1 = extText(h);
682 else if (strcmp(textToStr(l1),textToStr(l))<0)
693 /* --------------------------------------------------------------------------
694 * Predicate set Simplification:
696 * Calculate a minimal equivalent subset of a given set of predicates.
697 * ------------------------------------------------------------------------*/
699 static List local scSimplify(qs) /* Simplify predicates in qs, */
700 List qs; { /* returning equiv minimal subset */
706 #if EXPLAIN_INSTANCE_RESOLUTION
708 fputs("scSimplify: ", stdout);
709 printContext(stdout,copyPreds(tl(qs)));
710 fputs(" ||- ", stdout);
711 printPred(stdout, copyPred(fst3(pi),intOf(snd3(pi))));
715 ev = scEntail(tl(qs),fst3(pi),intOf(snd3(pi)),0);
717 overEvid(thd3(pi),ev); /* Overwrite dict var with evidence*/
718 qs = tl(qs); /* ... and discard predicate */
720 else { /* Otherwise, retain predicate */
723 qs = appendOnto(tmp,qs);
729 List simpleContext(ps,o) /* Simplify context of skeletons */
730 List ps; /* skeletons, offset o, using */
731 Int o; { /* superclass hierarchy */
732 return copyPreds(scSimplify(makePredAss(ps,o)));
735 /* --------------------------------------------------------------------------
736 * Context splitting --- tautological and locally tautological predicates:
737 * ------------------------------------------------------------------------*/
739 static Void local elimTauts() { /* Remove tautological constraints */
740 if (haskell98) { /* from preds */
741 reducePreds(); /* (or context reduce for Hask98) */
745 while (nonNull(ps)) {
747 Cell ev = entail(NIL,fst3(pi),intOf(snd3(pi)),0);
749 overEvid(thd3(pi),ev);
762 static Int numFixedVars = 0; /* Number of fixed vars found */
764 static Bool local anyGenerics(t,o) /* Test for generic vars, and count*/
765 Type t; /* fixed variables */
767 Type h = getDerefHead(t,o); /* This code is careful to expand */
768 Int a = argCount; /* synonyms; mark* & copy* do not. */
769 if (isSynonym(h) && a>=tycon(h).arity) {
770 expandSyn(h,a,&t,&o);
771 return anyGenerics(t,o);
775 for (; 0<a--; t=fun(t)) { /* cycle through any arguments */
777 if (anyGenerics(arg(t),o))
782 if (tyv->offs == FIXED_TYVAR) {
794 static List local elimOuterPreds(sps) /* Simplify and defer any remaining*/
795 List sps; { /* preds that contain no generics. */
798 for (preds=scSimplify(preds); nonNull(preds); ) {
801 if (anyGenerics(fst3(pi),intOf(snd3(pi)))
803 || isIP(fun(fst3(pi)))) {
804 tl(preds) = qs; /* Retain predicate*/
807 else { /* Defer predicate */
817 static List local elimPredsUsing(ps,sps)/* Try to discharge or defer preds,*/
818 List ps; /* splitting if necessary to match */
819 List sps; { /* context ps. sps = savePreds. */
821 while (nonNull(preds)) { /* Pick a predicate from preds */
823 Cell pi = fst3(hd(p));
824 Int o = intOf(snd3(hd(p)));
825 Cell ev = entail(ps,pi,o,0);
828 if (nonNull(ev)) { /* Discharge if ps ||- (pi,o) */
829 overEvid(thd3(hd(p)),ev);
830 } else if (!isAp(pi) || isIP(fun(pi)) || !anyGenerics(pi,o)) {
831 tl(p) = sps; /* Defer if no generics */
834 else { /* Try to split generics and fixed */
836 if (numFixedVars>0 && nonNull(in=findInstFor(pi,o))) {
837 List qs = inst(in).specifics;
838 for (ev=inst(in).builder; nonNull(qs); qs=tl(qs))
839 ev = ap(ev,assumeEvid(hd(qs),typeOff));
840 overEvid(thd3(hd(p)),ev);
842 else { /* No worthwhile progress possible */
848 preds = rems; /* Return any remaining predicates */
852 static Void local reducePreds() { /* Context reduce predicates: uggh!*/
853 List rems = NIL; /* (A last resort for defaulting) */
854 while (nonNull(preds)) { /* Pick a predicate from preds */
856 Cell pi = fst3(hd(p));
857 Int o = intOf(snd3(hd(p)));
862 ins = findInstsFor(pi,o);
863 in = nonNull(ins) && isNull(tl(ins)) ? snd(hd(ins)) : NIL;
866 in = findInstFor(pi,o);
869 List qs = inst(in).specifics;
870 Cell ev = inst(in).builder;
871 for (; nonNull(qs); qs=tl(qs))
872 ev = ap(ev,assumeEvid(hd(qs),typeOff));
873 overEvid(thd3(hd(p)),ev);
875 else { /* No worthwhile progress possible */
880 preds = scSimplify(rems); /* Return any remaining predicates */
883 static Void local normPreds(line) /* Normalize each element of preds */
884 Int line; { /* in some appropriate manner */
888 while (nonNull(ps)) {
889 Cell pi = fst3(hd(ps));
890 Cell ev = thd3(hd(ps));
891 if (isAp(pi) && isExt(fun(pi))) {
892 Cell r = lacksNorm(arg(pi),intOf(snd3(hd(ps))),fun(pi));
894 ERRMSG(line) "Cannot satisfy constraint " ETHEN
895 ERRPRED(copyPred(pi,intOf(snd3(hd(ps)))));
907 else if (intOf(snd(r))!=0) {
908 Cell nd = inventDictVar();
909 Cell ev1 = ap2(nameAddEv,snd(r),nd);
910 pi = ap(fun(pi),aVar);
911 hd(ps) = triple(pi,fst(r),nd);
917 fst3(hd(ps)) = ap(fun(pi),fst(r));
930 /* --------------------------------------------------------------------------
931 * Mechanisms for dealing with defaults:
932 * ------------------------------------------------------------------------*/
934 static Bool local resolveDefs(vs) /* Attempt to resolve defaults */
935 List vs; { /* for variables vs subject to */
936 List pvs = NIL; /* constraints in preds */
938 Bool defaulted = FALSE;
940 #ifdef DEBUG_DEFAULTS
941 Printf("Attempt to resolve variables ");
943 Printf(" with context ");
944 printContext(stdout,copyPreds(preds));
948 resetGenerics(); /* find type variables in ps */
949 for (; nonNull(qs); qs=tl(qs)) {
950 Cell pi = fst3(hd(qs));
951 Int o = intOf(snd3(hd(qs)));
952 for (; isAp(pi); pi=fun(pi))
953 pvs = genvarType(arg(pi),o,pvs);
956 for (; nonNull(pvs); pvs=tl(pvs)) { /* now try defaults */
957 Int vn = intOf(hd(pvs));
959 #ifdef DEBUG_DEFAULTS
960 Printf("is var %d included in ",vn);
965 if (!intIsMember(vn,vs))
966 defaulted |= resolveVar(vn);
967 #ifdef DEBUG_DEFAULTS
969 Printf("Yes, so no ambiguity!\n");
976 static Bool local resolveVar(vn) /* Determine whether an ambig. */
977 Int vn; { /* variable vn can be resolved */
978 List ps = preds; /* by default in the context of */
979 List cs = NIL; /* the predicates in ps */
980 Bool aNumClass = FALSE;
982 if (tyvar(vn)->bound == SKOLEM)
985 /* According to the Haskell definition, we can only default an ambiguous
986 * variable if the set of classes that constrain it:
987 * (a) includes at least one numeric class.
988 * (b) includes only numeric or standard classes.
989 * In addition, we will not allow a variable to be defaulted unless it
990 * appears only in predicates of the form (Class var).
993 #ifdef DEBUG_DEFAULTS
994 Printf("Trying to default variable %d\n",vn);
997 for (; nonNull(ps); ps=tl(ps)) {
999 Class c = classConstraining(vn,fst3(pi),intOf(snd3(pi)));
1001 if (c==classRealFrac || c==classRealFloat ||
1002 c==classFractional || c==classFloating ||
1003 c==classReal || c==classIntegral || c==classNum)
1005 else if (c!=classEq && c!=classOrd && c!=classShow &&
1006 c!=classRead && c!=classIx && c!=classEnum &&
1010 { Type t = arg(fst3(pi));/* Check for single var as arg */
1011 Int o = intOf(snd3(pi));
1014 if (!tyv || tyvNum(tyv)!=vn)
1017 if (!cellIsMember(c,cs))
1022 /* Now find the first class (if any) in the list of defaults that
1023 * is an instance of all of the required classes.
1025 * If we get this far, then cs only mentions classes from the list
1026 * above, all of which have only a single parameter of kind *.
1030 List ds = defaultDefns; /* N.B. guaranteed to be monotypes */
1031 #ifdef DEBUG_DEFAULTS
1032 Printf("Default conditions met, looking for type\n");
1034 for (; nonNull(ds); ds=tl(ds)) {
1036 while (nonNull(cs1) && nonNull(entail(NIL,ap(hd(cs1),hd(ds)),0,0)))
1039 bindTv(vn,hd(ds),0);
1040 #ifdef DEBUG_DEFAULTS
1041 Printf("Default type for variable %d is ",vn);
1042 printType(stdout,hd(ds));
1050 #ifdef DEBUG_DEFAULTS
1051 Printf("No default permitted/found\n");
1056 static Class local classConstraining(vn,pi,o)
1057 Int vn; /* Return class constraining var*/
1058 Cell pi; /* vn in predicate pi, or NIL if*/
1059 Int o; { /* vn is not involved */
1060 for (; isAp(pi); pi=fun(pi))
1061 if (!doesntOccurIn(tyvar(vn),arg(pi),o))
1066 /*-------------------------------------------------------------------------*/