2 /* --------------------------------------------------------------------------
3 * Provides an implementation for the `current substitution' used during
4 * type and kind inference in both static analysis and type checking.
6 * The Hugs 98 system is Copyright (c) Mark P Jones, Alastair Reid, the
7 * Yale Haskell Group, and the Oregon Graduate Institute of Science and
8 * Technology, 1994-1999, All rights reserved. It is distributed as
9 * free software under the license in the file "License", which is
10 * included in the distribution.
12 * $RCSfile: subst.c,v $
14 * $Date: 2000/03/09 10:19:33 $
15 * ------------------------------------------------------------------------*/
24 /*#define DEBUG_TYPES*/
26 static Int numTyvars; /* no. type vars currently in use */
27 static Int maxTyvars = 0;
28 static Int nextGeneric; /* number of generics found so far */
31 Tyvar tyvars[NUM_TYVARS]; /* storage for type variables */
33 Tyvar *tyvars = 0; /* storage for type variables */
35 Int typeOff; /* offset of result type */
36 Type typeIs; /* skeleton of result type */
37 Int typeFree; /* freedom in instantiated type */
38 List predsAre; /* list of predicates in type */
39 List genericVars; /* list of generic vars */
40 List btyvars = NIL; /* explicitly scoped type vars */
42 /* --------------------------------------------------------------------------
43 * local function prototypes:
44 * ------------------------------------------------------------------------*/
46 static Void local expandSubst Args((Int));
47 static Int local findBtyvsInt Args((Text));
48 static Type local makeTupleType Args((Int));
49 static Kind local makeSimpleKind Args((Int));
50 static Kind local makeVarKind Args((Int));
51 static Void local expandSyn1 Args((Tycon, Type *, Int *));
52 static List local listTyvar Args((Int,List));
53 static List local listTyvars Args((Type,Int,List));
54 static Cell local dupTyvar Args((Int,List));
55 static Cell local dupTyvars Args((Cell,Int,List));
56 static Pair local copyNoMark Args((Cell,Int));
57 static Type local dropRank1Body Args((Type,Int,Int));
58 static Type local liftRank1Body Args((Type,Int));
59 static Bool local matchTypeAbove Args((Type,Int,Type,Int,Int));
61 static Bool local varToVarBind Args((Tyvar *,Tyvar *));
62 static Bool local varToTypeBind Args((Tyvar *,Type,Int));
64 static Bool local inserter Args((Type,Int,Type,Int));
65 static Int local remover Args((Text,Type,Int));
66 static Int local tailVar Args((Type,Int));
69 static Bool local improveAgainst Args((Int,List,Cell,Int));
70 static Bool local instImprove Args((Int,Class,Cell,Int));
71 static Bool local pairImprove Args((Int,Class,Cell,Int,Cell,Int,Int));
73 static Bool local ipImprove Args((Int,Cell,Int,Cell,Int));
76 static Bool local kvarToVarBind Args((Tyvar *,Tyvar *));
77 static Bool local kvarToTypeBind Args((Tyvar *,Type,Int));
79 /* --------------------------------------------------------------------------
80 * The substitution, types, and kinds:
82 * In early versions of Gofer, the `substitution' data structure was only
83 * used by the type checker, so it made sense to include support for it in
84 * type.c. This changed when kinds and kind inference where introduced,
85 * which required access to the substitution during static analysis. The
86 * links between type.c and static.c that were intially used to accomplish
87 * this have now been avoided by making the substitution visible as an
88 * independent data structure in storage.c.
90 * In the same way that values have types, type constructors (and more
91 * generally, expressions built from such constructors) have kinds.
92 * The syntax of kinds in the current implementation is very simple:
94 * kind ::= STAR -- the kind of types
95 * | kind => kind -- constructors
96 * | variables -- either INTCELL or OFFSET
98 * For various reasons, this implementation uses structure sharing, instead
99 * of a copying approach. In principal, this is fast and avoids the need to
100 * build new type expressions. Unfortunately, this implementation will not
101 * be able to handle *very* large expressions.
103 * The substitution is represented by an array of type variables each of
105 * bound a (skeletal) type expression, or NIL if the variable
106 * is not bound, or SKOLEM for a Skolem constant (i.e., an
107 * uninstantiable variable).
108 * offs offset of skeleton in bound. If isNull(bound), then offs is
109 * used to indicate whether that variable is generic (i.e. free
110 * in the current assumption set) or fixed (i.e. bound in the
111 * current assumption set). Generic variables are assigned
112 * offset numbers whilst copying type expressions (t,o) to
113 * obtain their most general form.
114 * kind kind of value bound to type variable (`type variable' is
115 * rather inaccurate -- `constructor variable' would be better).
116 * ------------------------------------------------------------------------*/
118 Void emptySubstitution() { /* clear current substitution */
121 if (maxTyvars!=NUM_TYVARS) {
136 static Void local expandSubst(n) /* add further n type variables to */
137 Int n; { /* current substituion */
139 if (numTyvars+n>NUM_TYVARS) {
140 ERRMSG(0) "Too many type variables in type checker"
144 if (numTyvars+n>maxTyvars) { /* need to expand substitution */
145 Int newMax = maxTyvars+NUM_TYVARS;
149 if (numTyvars+n>newMax) { /* safety precaution */
150 ERRMSG(0) "Substitution expanding too quickly"
154 /* It would be better to realloc() here, but that isn't portable
155 * enough for calloc()ed arrays. The following code could cause
156 * a space leak if an interrupt occurs while we're copying the
157 * array ... we won't worry about this for the time being because
158 * we don't expect to have to go through this process much (if at
159 * all) in normal use of the type checker.
162 newTvs = (Tyvar *)calloc(newMax,sizeof(Tyvar));
164 ERRMSG(0) "Too many variables (%d) in type checker", newMax
167 for (i=0; i<numTyvars;++i) { /* copy substitution */
168 newTvs[i].offs = tyvars[i].offs;
169 newTvs[i].bound = tyvars[i].bound;
170 newTvs[i].kind = tyvars[i].kind;
172 maxTyvars = 0; /* protection from SIGINT? */
173 if (tyvars) free(tyvars);
180 Int newTyvars(n) /* allocate new type variables */
181 Int n; { /* all of kind STAR */
182 Int beta = numTyvars;
185 for (numTyvars+=n; n>0; n--) {
186 tyvars[numTyvars-n].offs = UNUSED_GENERIC;
187 tyvars[numTyvars-n].bound = NIL;
188 tyvars[numTyvars-n].kind = STAR;
190 Printf("new type variable: _%d ::: ",numTyvars-n);
191 printKind(stdout,tyvars[numTyvars-n].kind);
198 Int newKindedVars(k) /* allocate new variables with */
199 Kind k; { /* specified kinds */
200 Int beta = numTyvars; /* if k = k0 -> k1 -> ... -> kn */
201 for (; isPair(k); k=snd(k)) { /* then allocate n vars with kinds */
202 expandSubst(1); /* k0, k1, ..., k(n-1) */
203 tyvars[numTyvars].offs = UNUSED_GENERIC;
204 tyvars[numTyvars].bound = NIL;
205 tyvars[numTyvars].kind = fst(k);
207 Printf("new type variable: _%d ::: ",numTyvars);
208 printKind(stdout,tyvars[numTyvars].kind);
216 Void instantiate(type) /* instantiate type, if nonNull */
222 if (nonNull(typeIs)) { /* instantiate type expression ? */
224 if (isPolyType(typeIs)) { /* Polymorphic type scheme ? */
225 Kinds ks = polySigOf(typeIs);
226 typeOff = newKindedVars(ks);
227 typeIs = monotypeOf(typeIs);
228 for (; isAp(ks); ks=arg(ks))
232 if (isQualType(typeIs)) { /* Qualified type? */
233 predsAre = fst(snd(typeIs));
234 typeIs = snd(snd(typeIs));
239 /* --------------------------------------------------------------------------
240 * Bound type variables:
241 * ------------------------------------------------------------------------*/
243 Pair findBtyvs(t) /* Look for bound tyvar */
246 for (; nonNull(bts); bts=tl(bts)) {
248 for (; nonNull(bts1); bts1=tl(bts1))
249 if (t==textOf(fst(hd(bts1))))
255 static Int local findBtyvsInt(t) /* Look for bound type variable */
256 Text t; { /* expecting to find an integer */
257 Pair p = findBtyvs(t);
259 internal("findBtyvsInt");
260 return intOf(snd(p));
263 Void markBtyvs() { /* Mark explicitly scoped vars */
265 for (; nonNull(bts); bts=tl(bts)) {
267 for (; nonNull(bts1); bts1=tl(bts1))
268 markTyvar(intOf(snd(hd(bts1))));
272 Type localizeBtyvs(t) /* Localize type to eliminate refs */
273 Type t; { /* to explicitly scoped vars */
276 case POLYTYPE : snd(snd(t)) = localizeBtyvs(snd(snd(t)));
279 case QUAL : fst(snd(t)) = localizeBtyvs(fst(snd(t)));
280 snd(snd(t)) = localizeBtyvs(snd(snd(t)));
283 case AP : fst(t) = localizeBtyvs(fst(t));
284 snd(t) = localizeBtyvs(snd(t));
288 case VAROPCELL: return mkInt(findBtyvsInt(textOf(t)));
293 /* --------------------------------------------------------------------------
294 * Dereference or bind types in subsitution:
295 * ------------------------------------------------------------------------*/
297 Tyvar *getTypeVar(t,o) /* get number of type variable */
298 Type t; /* represented by (t,o) [if any]. */
301 case INTCELL : return tyvar(intOf(t));
302 case OFFSET : return tyvar(o+offsetOf(t));
304 case VAROPCELL : return tyvar(findBtyvsInt(textOf(t)));
309 Void tyvarType(vn) /* load type held in type variable */
310 Int vn; { /* vn into (typeIs,typeOff) */
313 while ((tyv=tyvar(vn)), isBound(tyv))
314 switch(whatIs(tyv->bound)) {
315 case INTCELL : vn = intOf(tyv->bound);
318 case OFFSET : vn = offsetOf(tyv->bound)+(tyv->offs);
322 case VAROPCELL : vn = findBtyvsInt(textOf(tyv->bound));
325 default : typeIs = tyv->bound;
333 Void bindTv(vn,t,o) /* set type variable vn to (t,o) */
337 Tyvar *tyv = tyvar(vn);
341 Printf("binding type variable: _%d to ",vn);
342 printType(stdout,debugType(t,o));
347 Cell getDerefHead(t,o) /* get value at head of type exp. */
357 if ((tyv=getTypeVar(t,o)) && isBound(tyv)) {
367 /* --------------------------------------------------------------------------
368 * Expand type synonyms:
369 * ------------------------------------------------------------------------*/
371 Void expandSyn(h,ar,at,ao) /* Expand type synonym with: */
372 Tycon h; /* head h */
373 Int ar; /* ar args (NB. ar>=tycon(h).arity)*/
374 Type *at; /* original expression (*at,*ao) */
375 Int *ao; { /* expansion returned in (*at,*ao) */
376 ar -= tycon(h).arity; /* calculate surplus arguments */
379 else { /* if there are more args than the */
380 Type t = *at; /* arity, we have to do a little */
381 Int o = *ao; /* bit of work to isolate args that*/
382 Type args = NIL; /* will not be changed by expansion*/
384 while (ar-- > 0) { /* find part to expand, and the */
385 Tyvar *tyv; /* unused arguments */
386 args = cons(arg(t),args);
390 expandSyn1(h,&t,&o); /* do the expansion */
391 bindTv((i=newTyvars(1)),t,o); /* and embed the results back in */
392 tyvar(i)->kind = getKind(t,o); /* (*at, *ao) as required */
393 *at = applyToArgs(mkInt(i),args);
397 static Void local expandSyn1(h,at,ao) /* Expand type synonym with: */
398 Tycon h; /* head h, tycon(h).arity args, */
399 Type *at; /* original expression (*at,*ao) */
400 Int *ao; { /* expansion returned in (*at,*ao) */
401 Int n = tycon(h).arity;
407 *ao = newKindedVars(tycon(h).kind);
408 for (; 0<n--; t=fun(t)) {
411 internal("expandSyn1");
412 bindTv(*ao+n,arg(t),o);
416 /* --------------------------------------------------------------------------
417 * Marking fixed variables in type expressions:
418 * ------------------------------------------------------------------------*/
420 Void clearMarks() { /* Set all unbound type vars to */
421 Int i; /* unused generic variables */
422 for (i=0; i<numTyvars; ++i)
423 if (!isBound(tyvar(i)))
424 tyvar(i)->offs = UNUSED_GENERIC;
429 Void markAllVars() { /* Set all unbound type vars to */
430 Int i; /* be fixed vars */
431 for (i=0; i<numTyvars; ++i)
432 if (!isBound(tyvar(i)))
433 tyvar(i)->offs = FIXED_TYVAR;
438 Void resetGenerics() { /* Reset all generic vars to unused*/
440 for (i=0; i<numTyvars; ++i)
441 if (!isBound(tyvar(i)) && tyvar(i)->offs>=GENERIC)
442 tyvar(i)->offs = UNUSED_GENERIC;
447 Void markTyvar(vn) /* mark fixed vars in type bound to*/
448 Int vn; { /* given type variable */
449 Tyvar *tyv = tyvar(vn);
452 markType(tyv->bound, tyv->offs);
454 (tyv->offs) = FIXED_TYVAR;
457 Void markType(t,o) /* mark fixed vars in type (t,o) */
470 case AP : markType(fst(t),o);
474 case OFFSET : markTyvar(o+offsetOf(t));
477 case INTCELL : markTyvar(intOf(t));
481 case VAROPCELL : markTyvar(findBtyvsInt(textOf(t)));
484 case RANK2 : markType(snd(snd(t)),o);
487 default : internal("markType");
491 Void markPred(pi) /* Marked fixed type vars in pi */
494 Int o = intOf(snd3(pi));
496 for (; isAp(cl); cl=fun(cl))
500 /* --------------------------------------------------------------------------
501 * Copy type expression from substitution to make a single type expression:
502 * ------------------------------------------------------------------------*/
504 Type copyTyvar(vn) /* calculate most general form of */
505 Int vn; { /* type bound to given type var */
506 Tyvar *tyv = tyvar(vn);
508 if ((tyv->bound)==SKOLEM) {
510 } else if (tyv->bound) {
511 return copyType(tyv->bound,tyv->offs);
515 case FIXED_TYVAR : return mkInt(vn);
517 case UNUSED_GENERIC : (tyv->offs) = GENERIC + nextGeneric++;
518 if (nextGeneric>=NUM_OFFSETS) {
520 "Too many quantified type variables"
523 genericVars = cons(mkInt(vn),genericVars);
525 default : return mkOffset(tyv->offs - GENERIC);
529 Type copyType(t,o) /* calculate most general form of */
530 Type t; /* type expression (t,o) */
534 case AP : { Type l = copyType(fst(t),o);/* ensure correct */
535 Type r = copyType(snd(t),o);/* eval. order */
538 case OFFSET : return copyTyvar(o+offsetOf(t));
539 case INTCELL : return copyTyvar(intOf(t));
541 case VAROPCELL : return copyTyvar(findBtyvsInt(textOf(t)));
547 Cell copyPred(pi,o) /* Copy single predicate (or part */
548 Cell pi; /* thereof) ... */
551 Cell temp = copyPred(fun(pi),o);/* to ensure correct order of eval.*/
552 return ap(temp,copyType(arg(pi),o));
558 Type zonkTyvar(vn) /* flatten type by chasing all references */
559 Int vn; { /* and collapsing OFFSETS to absolute indexes */
560 Tyvar *tyv = tyvar(vn);
563 return zonkType(tyv->bound,tyv->offs);
568 Type zonkType(t,o) /* flatten type by chasing all references */
569 Type t; /* and collapsing OFFSETS to absolute indexes */
573 case AP : { Type l = zonkType(fst(t),o);/* ensure correct */
574 Type r = zonkType(snd(t),o);/* eval. order */
577 case OFFSET : return zonkTyvar(o+offsetOf(t));
578 case INTCELL : return zonkTyvar(intOf(t));
585 Type debugTyvar(vn) /* expand type structure in full */
586 Int vn; { /* detail */
587 Tyvar *tyv = tyvar(vn);
590 return debugType(tyv->bound,tyv->offs);
599 case AP : { Type l = debugType(fst(t),o);
600 Type r = debugType(snd(t),o);
603 case OFFSET : return debugTyvar(o+offsetOf(t));
604 case INTCELL : return debugTyvar(intOf(t));
606 case VAROPCELL : return debugTyvar(findBtyvsInt(textOf(t)));
611 List debugContext(ps)
615 for (; nonNull(ps); ps=tl(ps)) {
616 p = debugPred(fst3(hd(ps)),intOf(snd3(hd(ps))));
626 return pair(debugPred(fun(pi),o),debugType(arg(pi),o));
630 #endif /*DEBUG_TYPES*/
632 Kind copyKindvar(vn) /* build kind attatched to variable*/
634 Tyvar *tyv = tyvar(vn);
636 return copyKind(tyv->bound,tyv->offs);
637 return STAR; /* any unbound variable defaults to*/
638 } /* the kind of all types */
640 Kind copyKind(k,o) /* build kind expression from */
641 Kind k; /* given skeleton */
644 case AP : { Kind l = copyKind(fst(k),o); /* ensure correct */
645 Kind r = copyKind(snd(k),o); /* eval. order */
648 case OFFSET : return copyKindvar(o+offsetOf(k));
649 case INTCELL : return copyKindvar(intOf(k));
654 /* --------------------------------------------------------------------------
655 * Copy type expression from substitution without marking:
656 * ------------------------------------------------------------------------*/
658 static List local listTyvar(vn,ns)
661 Tyvar *tyv = tyvar(vn);
664 return listTyvars(tyv->bound,tyv->offs,ns);
665 } else if (!intIsMember(vn,ns)) {
666 ns = cons(mkInt(vn),ns);
671 static List local listTyvars(t,o,ns)
676 case AP : return listTyvars(fst(t),o,
679 case OFFSET : return listTyvar(o+offsetOf(t),ns);
680 case INTCELL : return listTyvar(intOf(t),ns);
686 static Cell local dupTyvar(vn,ns)
689 Tyvar *tyv = tyvar(vn);
692 return dupTyvars(tyv->bound,tyv->offs,ns);
695 for (; nonNull(ns) && vn!=intOf(hd(ns)); ns=tl(ns)) {
702 static Cell local dupTyvars(t,o,ns)
707 case AP : { Type l = dupTyvars(fst(t),o,ns);
708 Type r = dupTyvars(snd(t),o,ns);
711 case OFFSET : return dupTyvar(o+offsetOf(t),ns);
712 case INTCELL : return dupTyvar(intOf(t),ns);
717 static Cell local copyNoMark(t,o) /* Copy a type or predicate without*/
718 Cell t; /* changing marks */
720 List ns = listTyvars(t,o,NIL);
721 Cell result = pair(ns,dupTyvars(t,o,ns));
722 for (; nonNull(ns); ns=tl(ns)) {
723 hd(ns) = tyvar(intOf(hd(ns)))->kind;
728 /* --------------------------------------------------------------------------
729 * Droping and lifting of type schemes that appear in rank 2 position:
730 * ------------------------------------------------------------------------*/
732 Type dropRank2(t,alpha,n) /* Drop a (potentially) rank2 type */
736 if (whatIs(t)==RANK2) {
737 Cell r = fst(snd(t));
740 for (t=snd(snd(t)); i>0; i--) {
741 Type a = arg(fun(t));
743 a = dropRank1(a,alpha,n);
747 t = ap(RANK2,pair(r,revOnto(as,t)));
752 Type dropRank1(t,alpha,n) /* Copy rank1 argument type t to */
753 Type t; /* make a rank1 type scheme */
756 if (n>0 && isPolyType(t))
757 t = mkPolyType(polySigOf(t),dropRank1Body(monotypeOf(t),alpha,n));
761 static Type local dropRank1Body(t,alpha,n)
766 case OFFSET : { Int m = offsetOf(t);
767 return (m>=n) ? mkOffset(m-n) : mkInt(alpha+m);
770 case POLYTYPE : return mkPolyType(polySigOf(t),
771 dropRank1Body(monotypeOf(t),alpha,n));
773 case QUAL : return ap(QUAL,dropRank1Body(snd(t),alpha,n));
775 case RANK2 : return ap(RANK2,pair(fst(snd(t)),
776 dropRank1Body(snd(snd(t)),
780 case AP : return ap(dropRank1Body(fun(t),alpha,n),
781 dropRank1Body(arg(t),alpha,n));
787 Void liftRank2Args(as,alpha,m)
794 for (m=nextGeneric; nonNull(as); as=tl(as)) {
795 Type ta = arg(fun(as));
796 ta = isPolyType(ta) ? liftRank1Body(ta,m) : copyType(ta,alpha);
802 Type liftRank2(t,alpha,m)
806 if (whatIs(t)==RANK2) {
807 Cell r = fst(snd(t));
814 for (i=intOf(r); i>0; i--) {
815 Type a = arg(fun(t));
816 a = isPolyType(a) ? liftRank1Body(a,m) : copyType(a,alpha);
820 t = ap(RANK2,pair(r,revOnto(as,copyType(t,alpha))));
823 t = copyType(t,alpha);
827 Type liftRank1(t,alpha,m)
831 if (m>0 && isPolyType(t)) {
836 t = liftRank1Body(t,nextGeneric);
841 static Type local liftRank1Body(t,n)
845 case OFFSET : return mkOffset(n+offsetOf(t));
847 case INTCELL : return copyTyvar(intOf(t));
850 case VAROPCELL : return copyTyvar(findBtyvsInt(textOf(t)));
852 case POLYTYPE : return mkPolyType(polySigOf(t),
853 liftRank1Body(monotypeOf(t),n));
855 case QUAL : return ap(QUAL,liftRank1Body(snd(t),n));
857 case RANK2 : return ap(RANK2,pair(fst(snd(t)),
858 liftRank1Body(snd(snd(t)),n)));
860 case AP : return ap(liftRank1Body(fun(t),n),
861 liftRank1Body(arg(t),n));
867 /* --------------------------------------------------------------------------
868 * Support for `kind preserving substitutions' from unification:
869 * ------------------------------------------------------------------------*/
871 Bool eqKind(k1,k2) /* check that two (mono)kinds are */
872 Kind k1, k2; { /* equal */
874 || (isPair(k1) && isPair(k2)
875 && eqKind(fst(k1),fst(k2))
876 && eqKind(snd(k1),snd(k2)));
879 Kind getKind(c,o) /* Find kind of constr during type */
880 Cell c; /* checking process */
882 if (isAp(c)) /* application */
883 return snd(getKind(fst(c),o));
885 case TUPLE : return simpleKind(tupleOf(c)); /*(,)::* -> * -> * */
886 case OFFSET : return tyvar(o+offsetOf(c))->kind;
887 case INTCELL : return tyvar(intOf(c))->kind;
889 case VAROPCELL : return tyvar(findBtyvsInt(textOf(c)))->kind;
890 case TYCON : return tycon(c).kind;
892 case EXT : return extKind;
896 Printf("getKind c = %d, whatIs=%d\n",c,whatIs(c));
899 return STAR;/* not reached */
902 /* --------------------------------------------------------------------------
903 * Find generic variables in a type:
904 * ------------------------------------------------------------------------*/
906 Type genvarTyvar(vn,vs) /* calculate list of generic vars */
907 Int vn; /* thru variable vn, prepended to */
908 List vs; { /* list vs */
909 Tyvar *tyv = tyvar(vn);
912 return genvarType(tyv->bound,tyv->offs,vs);
913 else if (tyv->offs == UNUSED_GENERIC) {
914 tyv->offs += GENERIC + nextGeneric++;
915 return cons(mkInt(vn),vs);
917 else if (tyv->offs>=GENERIC && !intIsMember(vn,vs))
918 return cons(mkInt(vn),vs);
923 List genvarType(t,o,vs) /* calculate list of generic vars */
924 Type t; /* in type expression (t,o) */
925 Int o; /* results are prepended to vs */
928 case AP : return genvarType(snd(t),o,genvarType(fst(t),o,vs));
929 case OFFSET : return genvarTyvar(o+offsetOf(t),vs);
930 case INTCELL : return genvarTyvar(intOf(t),vs);
932 case VAROPCELL : return genvarTyvar(findBtyvsInt(textOf(t)),vs);
937 /* --------------------------------------------------------------------------
939 * ------------------------------------------------------------------------*/
941 Bool doesntOccurIn(lookFor,t,o) /* Return TRUE if var lookFor */
942 Tyvar *lookFor; /* isn't referenced in (t,o) */
950 if (tyv) /* type variable */
952 else if (isAp(t)) { /* application */
953 if (doesntOccurIn(lookFor,snd(t),o))
958 else /* no variable found */
964 /* --------------------------------------------------------------------------
965 * Unification algorithm:
966 * ------------------------------------------------------------------------*/
968 char *unifyFails = 0; /* Unification error message */
969 static Int bindAbove = 0; /* Used to restrict var binding */
971 #define bindOnlyAbove(beta) bindAbove=beta
972 #define noBind() bindAbove=MAXPOSINT
973 #define unrestrictBind() bindAbove=0
975 static Bool local varToVarBind(tyv1,tyv2)/* Make binding tyv1 := tyv2 */
976 Tyvar *tyv1, *tyv2; {
977 if (tyv1!=tyv2) { /* If vars are same, nothing to do!*/
979 /* Check that either tyv1 or tyv2 is in allowed range for binding */
980 /* and is not a Skolem constant, and swap vars if nec. so we can */
983 if (tyvNum(tyv1)<bindAbove || tyv1->bound==SKOLEM) {
984 if (tyvNum(tyv2)<bindAbove || tyv2->bound==SKOLEM) {
985 unifyFails = "types do not match";
994 if (!eqKind(tyv1->kind,tyv2->kind)) {
995 unifyFails = "constructor variable kinds do not match";
999 tyv1->offs = tyvNum(tyv2);
1001 Printf("vv binding tyvar: _%d to _%d\n",tyvNum(tyv1),tyvNum(tyv2));
1007 static Bool local varToTypeBind(tyv,t,o)/* Make binding tyv := (t,o) */
1009 Type t; /* guaranteed not to be a v'ble or */
1010 Int o; { /* have synonym as outermost constr*/
1011 if (tyvNum(tyv)<bindAbove) { /* Check that tyv is in range */
1012 unifyFails = "types do not match";
1015 else if (tyv->bound == SKOLEM) { /* Check that it is not Skolemized */
1016 unifyFails = "cannot instantiate Skolem constant";
1019 else if (!doesntOccurIn(tyv,t,o)) /* Carry out occurs check */
1020 unifyFails = "unification would give infinite type";
1021 else if (!eqKind(tyv->kind,getKind(t,o)))
1022 unifyFails = "kinds do not match";
1027 Printf("vt binding type variable: _%d to ",tyvNum(tyv));
1028 printType(stdout,debugType(t,o));
1036 Bool unify(t1,o1,t2,o2) /* Main unification routine */
1037 Type t1,t2; /* unify (t1,o1) with (t2,o2) */
1047 return varToVarBind(tyv1,tyv2); /* t1, t2 variables */
1049 Cell h2 = getDerefHead(t2,o2); /* t1 variable, t2 not */
1050 if (isSynonym(h2) && argCount>=tycon(h2).arity) {
1051 expandSyn(h2,argCount,&t2,&o2);
1055 return varToTypeBind(tyv1,t2,o2);
1060 Cell h1 = getDerefHead(t1,o1); /* t2 variable, t1 not */
1061 if (isSynonym(h1) && argCount>=tycon(h1).arity) {
1062 expandSyn(h1,argCount,&t1,&o1);
1066 return varToTypeBind(tyv2,t1,o1);
1068 else { /* t1, t2 not vars */
1069 Type h1 = getDerefHead(t1,o1);
1071 Type h2 = getDerefHead(t2,o2);
1075 Printf("tt unifying types: ");
1076 printType(stdout,debugType(t1,o1));
1078 printType(stdout,debugType(t2,o2));
1081 if (isOffset(h1) || isInt(h1)) h1=NIL; /* represent var by NIL*/
1082 if (isOffset(h2) || isInt(h2)) h2=NIL;
1085 if (isExt(h1) || isExt(h2)) {
1086 if (a1==2 && isExt(h1) && a2==2 && isExt(h2)) {
1087 if (extText(h1)==extText(h2)) {
1088 return unify(arg(fun(t1)),o1,arg(fun(t2)),o2) &&
1089 unify(arg(t1),o1,arg(t2),o2);
1091 return inserter(t1,o1,t2,o2) &&
1092 unify(arg(t1),o1,aVar,
1093 remover(extText(h1),t2,o2));
1096 unifyFails = "rows are not compatible";
1101 if (nonNull(h1) && h1==h2) {/* Assuming well-formed types, both*/
1102 if (a1!=a2) { /* t1, t2 must have same no of args*/
1103 unifyFails = "incompatible constructors";
1107 if (!unify(arg(t1),o1,arg(t2),o2))
1118 /* Types do not match -- look for type synonyms to expand */
1120 if (isSynonym(h1) && a1>=tycon(h1).arity) {
1121 expandSyn(h1,a1,&t1,&o1);
1125 if (isSynonym(h2) && a2>=tycon(h2).arity) {
1126 expandSyn(h2,a2,&t2,&o2);
1131 if ((isNull(h1) && a1<=a2) || /* last attempt -- maybe */
1132 (isNull(h2) && a2<=a1)) { /* one head is a variable? */
1137 if (tyv1) { /* unify heads! */
1139 return varToVarBind(tyv1,tyv2);
1141 return varToTypeBind(tyv1,t2,o2);
1144 return varToTypeBind(tyv2,t1,o1);
1146 /* at this point, neither t1 nor t2 is a variable. In */
1147 /* addition, they must both be APs unless one of the */
1148 /* head variables has been bound during unification of */
1149 /* the arguments. */
1151 if (!isAp(t1) || !isAp(t2)) { /* might not be APs*/
1155 if (!unify(arg(t1),o1,arg(t2),o2)) /* o/w must be APs */
1167 static Bool local inserter(r1,o1,r,o) /* Insert first field in (r1,o1) */
1168 Type r1; /* into row (r,o), both of which */
1169 Int o1; /* are known to begin with an EXT */
1172 Text labt = extText(fun(fun(r1))); /* Find the text of the label */
1174 Printf("inserting ");
1175 printType(stdout,debugType(r1,o1));
1177 printType(stdout,debugType(r,o));
1184 Int beta; /* Test for common tail */
1185 if (tailVar(arg(r1),o1)==tyvNum(tyv)) {
1186 unifyFails = "distinct rows have common tail";
1189 beta = newTyvars(1); /* Extend row with new field */
1190 tyvar(beta)->kind = ROW;
1191 return varToTypeBind(tyv,ap(fun(r1),mkInt(beta)),o1);
1193 else if (isAp(r) && isAp(fun(r)) && isExt(fun(fun(r)))) {
1194 if (labt==extText(fun(fun(r))))/* Compare existing fields */
1195 return unify(arg(fun(r1)),o1,extField(r),o);
1196 r = extRow(r); /* Or skip to next field */
1198 else { /* Nothing else will match */
1199 unifyFails = "field mismatch";
1205 static Int local remover(l,r,o) /* Make a new row by copying (r,o) */
1206 Text l; /* but removing the l field (which */
1207 Type r; /* MUST exist) */
1210 Int beta = newTyvars(1);
1211 tyvar(beta)->kind = ROW;
1213 Printf("removing %s from",textToStr(l));
1214 printType(stdout,debugType(r,o));
1218 if (tyv || !isAp(r) || !isAp(fun(r)) || !isExt(fun(fun(r))))
1219 internal("remover");
1220 if (l==extText(fun(fun(r))))
1223 r = ap(fun(r),mkInt(remover(l,extRow(r),o)));
1229 static Int local tailVar(r,o) /* Find var at tail end of a row */
1238 else if (isAp(r) && isAp(fun(r)) && isExt(fun(fun(r)))) {
1249 Bool typeMatches(type,mt) /* test if type matches monotype mt*/
1250 Type type, mt; { /* imported from STG Hugs */
1252 if (isPolyOrQualType(type))
1254 emptySubstitution();
1256 result = unify(mt,0,type,0);
1258 emptySubstitution();
1262 Bool isProgType(ks,type) /* Test if type is of the form */
1263 List ks; /* IO t for some t. */
1268 emptySubstitution();
1269 alpha = newKindedVars(ks);
1270 beta = newTyvars(1);
1271 bindOnlyAbove(beta);
1272 result = unify(type,alpha,typeProgIO,beta);
1274 emptySubstitution();
1278 /* --------------------------------------------------------------------------
1279 * Matching predicates:
1281 * There are (at least) four situations where we need to match up pairs
1284 * 1) Testing to see if two predicates are the same (ignoring differences
1285 * caused by the use of type synonyms, for example).
1287 * 2) Matching a predicate with the head of its class so that we can
1288 * find the corresponding superclass predicates. If the predicates
1289 * have already been kind-checked, and the classes are known to be
1290 * the same, then this should never fail.
1292 * 3) Matching a predicate against the head of an instance to see if
1293 * that instance is applicable.
1295 * 4) Matching two instance heads to see if there is an overlap.
1297 * For (1), we need a matching process that does not bind any variables.
1298 * For (2) and (3), we need to use one-way matching, only allowing
1299 * variables in the class or instance head to be instantiated. For
1300 * (4), we need two-way unification.
1302 * Another situation in which both one-way and two-way unification might
1303 * be used is in an implementation of improvement. Here, a one-way match
1304 * would be used to determine applicability of a rule for improvement
1305 * that would then be followed by unification with another predicate.
1306 * One possible syntax for this might be:
1308 * instance P => pi [improves pi'] where ...
1310 * The intention here is that any predicate matching pi' can be unified
1311 * with pi to get more accurate types. A simple example of this is:
1313 * instance Collection [a] a improves Collection [a] b where ...
1315 * As soon as we know what the collection type is (in this case, a list),
1316 * we will also know what the element type is. To ensure that the rule
1317 * for improvement is valid, the compilation system will also need to use
1318 * a one-way matching process to ensure that pi is a (substitution) instance
1319 * of pi'. Another extension would be to allow more than one predicate pi'
1320 * in an improving rule. Read the paper on simplification and improvement
1321 * for technical background. Watch this space for implementation news!
1322 * ------------------------------------------------------------------------*/
1324 Bool samePred(pi1,o1,pi,o) /* Test to see if predicates are */
1325 Cell pi1; /* the same, with no binding of */
1326 Int o1; /* the variables in either one. */
1327 Cell pi; /* Assumes preds are kind correct */
1328 Int o; { /* with the same class. */
1331 result = unifyPred(pi1,o1,pi,o);
1336 Bool matchPred(pi1,o1,pi,o) /* One way match predicate (pi1,o1)*/
1337 Cell pi1; /* against (pi,o), allowing only */
1338 Int o1; /* vars in 2nd pred to be bound. */
1339 Cell pi; /* Assumes preds are kind correct */
1340 Int o; { /* with the same class and that no */
1341 Bool result; /* vars have been alloc'd since o. */
1343 result = unifyPred(pi1,o1,pi,o);
1348 Bool unifyPred(pi1,o1,pi,o) /* Unify two predicates */
1349 Cell pi1; /* Assumes preds are kind correct */
1350 Int o1; /* with the same class. */
1353 for (; isAp(pi1); pi1=fun(pi1), pi=fun(pi)) {
1354 if (!isAp(pi) || !unify(arg(pi1),o1,arg(pi),o))
1357 /* pi1 has exhausted its argument chain, we also need to check that
1358 pi has no remaining arguments. However, under this condition,
1359 the pi1 == pi will always return FALSE, giving the desired
1363 if (isIP(pi1) && isIP(pi))
1364 return textOf(pi1)==textOf(pi);
1371 static Cell trexShow = NIL; /* Used to test for show on records*/
1372 static Cell trexEq = NIL; /* Used to test for eq on records */
1375 Inst findInstFor(pi,o) /* Find matching instance for pred */
1376 Cell pi; /* (pi,o), or otherwise NIL. If a */
1377 Int o; { /* match is found, then tyvars from*/
1378 Class c = getHead(pi); /* typeOff have been initialized to*/
1379 List ins; /* allow direct use of specifics. */
1385 for (ins=cclass(c).instances; nonNull(ins); ins=tl(ins)) {
1387 Int beta = newKindedVars(inst(in).kinds);
1388 if (matchPred(pi,o,inst(in).head,beta)) {
1395 Int alpha = newKindedVars(inst(in).kinds);
1397 kspi = copyNoMark(pi,o);
1399 beta = newKindedVars(fst(kspi));
1400 if (matchPred(inst(in).head,alpha,snd(kspi),beta)) {
1411 { Bool wantShow = (c==findQualClass(trexShow));
1412 Bool wantEither = wantShow || (c==findQualClass(trexEq));
1414 if (wantEither) { /* Generate instances of */
1415 Type t = arg(pi); /* ShowRecRow and EqRecRow */
1416 Tyvar *tyv; /* on the fly */
1422 for (ins=cclass(c).instances; nonNull(ins); ins=tl(ins))
1423 if (getHead(arg(inst(hd(ins)).head))==e) {
1428 in = (wantShow ? addRecShowInst(c,e) : addRecEqInst(c,e));
1429 typeOff = newKindedVars(extKind);
1430 bindTv(typeOff,arg(fun(t)),o);
1431 bindTv(typeOff+1,arg(t),o);
1442 List findInstsFor(pi,o) /* Find matching instance for pred */
1443 Cell pi; /* (pi,o), or otherwise NIL. If a */
1444 Int o; { /* match is found, then tyvars from*/
1445 Class c = getHead(pi); /* typeOff have been initialized to*/
1446 List ins; /* allow direct use of specifics. */
1452 for (ins=cclass(c).instances; nonNull(ins); ins=tl(ins)) {
1454 Int beta = newKindedVars(inst(in).kinds);
1455 if (matchPred(pi,o,inst(in).head,beta)) {
1456 res = cons (pair (beta, in), res);
1470 /* --------------------------------------------------------------------------
1472 * ------------------------------------------------------------------------*/
1474 Void improve(line,sps,ps) /* Improve a list of predicates */
1482 for (ps1=ps; nonNull(ps1); ps1=tl(ps1)) {
1483 Cell pi = fst3(hd(ps1));
1484 Int o = intOf(snd3(hd(ps1)));
1485 Cell c = getHead(pi);
1486 if ((isClass(c) && nonNull(cclass(c).xfds)) || isIP(c)) {
1487 improved |= improveAgainst(line,sps,pi,o);
1489 improved |= instImprove(line,c,pi,o);
1490 improved |= improveAgainst(line,tl(ps1),pi,o);
1496 Void improve1(line,sps,pi,o) /* Improve a single predicate */
1502 Cell c = getHead(pi);
1505 if ((isClass(c) && nonNull(cclass(c).xfds)) || isIP(c)) {
1506 improved |= improveAgainst(line,sps,pi,o);
1508 improved |= instImprove(line,c,pi,o);
1513 Bool improveAgainst(line,ps,pi,o)
1518 Bool improved = FALSE;
1519 Cell h = getHead(pi);
1520 for (; nonNull(ps); ps=tl(ps)) {
1522 Cell pi1 = fst3(pr);
1523 Int o1 = intOf(snd3(pr));
1524 Cell h1 = getHead(pi1);
1525 /* it would be nice to optimize for the common case
1527 if (isClass(h) && isClass(h1)) {
1528 improved |= pairImprove(line,h,pi,o,pi1,o1,numTyvars);
1530 improved |= pairImprove(line,h1,pi1,o1,pi,o,numTyvars);
1533 else if (isIP(h1) && textOf(h1) == textOf(h))
1534 improved |= ipImprove(line,pi,o,pi1,o1);
1539 /* should emulate findInsts behavior of shorting out if the
1540 predicate would match a more general signature... */
1542 Bool instImprove(line,c,pi,o)
1547 Bool improved = FALSE;
1548 List ins = cclass(c).instances;
1549 for (; nonNull(ins); ins=tl(ins)) {
1551 Int alpha = newKindedVars(inst(in).kinds);
1552 improved |= pairImprove(line,c,pi,o,inst(in).head,alpha,alpha);
1558 Bool ipImprove(line,pi,o,pi1,o1)
1566 if (!sameType(t,o,t1,o1)) {
1567 if (!unify(t,o,t1,o1)) {
1568 ERRMSG(line) "Mismatching uses of implicit parameter\n"
1571 ETHEN ERRPRED(copyPred(pi1,o1));
1573 ETHEN ERRPRED(copyPred(pi,o));
1583 Bool pairImprove(line,c,pi1,o1,pi2,o2,above) /* Look for improvement of (pi1,o1)*/
1584 Int line; /* against (pi2,o2) */
1591 Bool improved = FALSE;
1592 List xfds = cclass(c).xfds;
1593 for (; nonNull(xfds); xfds=tl(xfds)) {
1594 Cell xfd = hd(xfds);
1597 for (; nonNull(hs); hs=tl(hs)) {
1599 Class d = getHead(h);
1600 alpha = newKindedVars(cclass(d).kinds);
1601 if (matchPred(pi2,o2,h,alpha))
1606 List fds = snd(xfd);
1607 for (; nonNull(fds); fds=tl(fds)) {
1608 List as = fst(hd(fds));
1610 for (; same && nonNull(as); as=tl(as)) {
1611 Int n = offsetOf(hd(as));
1612 same &= matchTypeAbove(nthArg(n,pi1),o1,
1613 mkOffset(n),alpha,above);
1615 if (isNull(as) && same) {
1616 for (as=snd(hd(fds)); same && nonNull(as); as=tl(as)) {
1617 Int n = offsetOf(hd(as));
1618 Type t1 = nthArg(n,pi1);
1619 Type t2 = mkOffset(n);
1620 if (!matchTypeAbove(t1,o1,t2,alpha,above)) {
1621 same &= unify(t1,o1,t2,alpha);
1627 "Constraints are not consistent with functional dependency"
1629 ERRTEXT "\n*** Constraint : "
1630 ETHEN ERRPRED(copyPred(pi1,o1));
1631 ERRTEXT "\n*** And constraint : "
1632 ETHEN ERRPRED(copyPred(pi2,o2));
1633 ERRTEXT "\n*** For class : "
1634 ETHEN ERRPRED(cclass(c).head);
1635 ERRTEXT "\n*** Break dependency : "
1636 ETHEN ERRFD(hd(fds));
1648 /* --------------------------------------------------------------------------
1649 * Compare type schemes:
1650 * ------------------------------------------------------------------------*/
1652 Bool sameSchemes(s,s1) /* Test to see whether two type */
1653 Type s; /* schemes are the same */
1658 Bool b = isPolyType(s); /* Check quantifiers are the same */
1659 Bool b1 = isPolyType(s1);
1661 if (b && b1 && eqKind(polySigOf(s),polySigOf(s1))) {
1662 Kind k = polySigOf(s);
1664 s1 = monotypeOf(s1);
1665 o = newKindedVars(k);
1666 for (; isAp(k); k=arg(k))
1673 b = (whatIs(s)==QUAL); /* Check that contexts are the same*/
1674 b1 = (whatIs(s1)==QUAL);
1677 List ps = fst(snd(s));
1678 List ps1 = fst(snd(s1));
1680 while (nonNull(ps) && nonNull(ps1)) {
1683 if (getHead(pi)!=getHead(pi1)
1684 || !unifyPred(pi,o,pi1,o))
1690 if (nonNull(ps) || nonNull(ps1))
1699 b = (whatIs(s)==RANK2); /* Check any rank 2 annotations */
1700 b1 = (whatIs(s1)==RANK2);
1702 if (b && b1 && intOf(fst(snd(s)))==intOf(fst(snd(s1)))) {
1703 nr2 = intOf(fst(snd(s)));
1711 for (; nr2>0; nr2--) { /* Deal with rank 2 arguments */
1712 Type t = arg(fun(s));
1713 Type t1 = arg(fun(s1));
1714 b = isPolyOrQualType(t);
1715 b1 = isPolyOrQualType(t1);
1718 t = dropRank1(t,o,m);
1719 t1 = dropRank1(t1,o,m);
1720 if (!sameSchemes(t,t1))
1727 if (!sameType(t,o,t1,o)) {
1736 return sameType(s,o,s1,o); /* Ensure body types are the same */
1739 Bool sameType(t1,o1,t,o) /* Test to see if types are */
1740 Type t1; /* the same, with no binding of */
1741 Int o1; /* the variables in either one. */
1742 Cell t; /* Assumes types are kind correct */
1743 Int o; { /* with the same kind. */
1746 result = unify(t1,o1,t,o);
1751 Bool matchType(t1,o1,t,o) /* One way match type (t1,o1) */
1752 Type t1; /* against (t,o), allowing only */
1753 Int o1; /* vars in 2nd type to be bound. */
1754 Type t; /* Assumes types are kind correct */
1755 Int o; { /* and that no vars have been */
1756 Bool result; /* alloc'd since o. */
1758 result = unify(t1,o1,t,o);
1763 static Bool local matchTypeAbove(t1,o1,t,o,a) /* match, allowing only vars */
1764 Type t1; /* allocated since `a' to be bound */
1765 Int o1; /* this is deeply hacky, since it */
1766 Type t; /* relies on careful use of the */
1767 Int o; /* substitution stack */
1771 result = unify(t1,o1,t,o);
1776 /* --------------------------------------------------------------------------
1777 * Unify kind expressions:
1778 * ------------------------------------------------------------------------*/
1780 static Bool local kvarToVarBind(tyv1,tyv2)/* Make binding tyv1 := tyv2 */
1781 Tyvar *tyv1, *tyv2; { /* for kind variable bindings */
1784 tyv1->offs = tyvNum(tyv2);
1786 Printf("vv binding kvar: _%d to _%d\n",tyvNum(tyv1),tyvNum(tyv2));
1792 static Bool local kvarToTypeBind(tyv,t,o)/* Make binding tyv := (t,o) */
1793 Tyvar *tyv; /* for kind variable bindings */
1794 Type t; /* guaranteed not to be a v'ble or */
1795 Int o; { /* have synonym as outermost constr*/
1796 if (doesntOccurIn(tyv,t,o)) {
1800 Printf("vt binding kind variable: _%d to ",tyvNum(tyv));
1801 printType(stdout,debugType(t,o));
1806 unifyFails = "unification would give infinite kind";
1810 Bool kunify(k1,o1,k2,o2) /* Unify kind expr (k1,o1) with */
1811 Kind k1,k2; /* (k2,o2) */
1820 return kvarToVarBind(kyv1,kyv2); /* k1, k2 variables */
1822 return kvarToTypeBind(kyv1,k2,o2); /* k1 variable, k2 not */
1826 return kvarToTypeBind(kyv2,k1,o1); /* k2 variable, k1 not */
1829 Printf("unifying kinds: ");
1830 printType(stdout,debugType(k1,o1));
1832 printType(stdout,debugType(k2,o2));
1835 if (k1==STAR && k2==STAR) /* k1, k2 not vars */
1838 else if (k1==ROW && k2==ROW)
1841 else if (isAp(k1) && isAp(k2))
1842 return kunify(fst(k1),o1,fst(k2),o2) &&
1843 kunify(snd(k1),o1,snd(k2),o2);
1849 /* --------------------------------------------------------------------------
1850 * Tuple type constructors: are generated as necessary. The most common
1851 * n-tuple constructors (n<MAXTUPCON) are held in a cache to avoid
1852 * repeated generation of the constructor types.
1853 * ------------------------------------------------------------------------*/
1855 #define MAXTUPCON 10
1856 static Type tupleConTypes[MAXTUPCON];
1858 Void typeTuple(e) /* find type for tuple constr, using*/
1859 Cell e; { /* tupleConTypes to cache previously*/
1860 Int n = tupleOf(e); /* calculated tuple constr. types. */
1861 typeOff = newTyvars(n);
1863 typeIs = makeTupleType(n);
1864 else if (tupleConTypes[n])
1865 typeIs = tupleConTypes[n];
1867 typeIs = tupleConTypes[n] = makeTupleType(n);
1870 static Type local makeTupleType(n) /* construct type for tuple constr. */
1871 Int n; { /* t1 -> ... -> tn -> (t1,...,tn) */
1872 Type h = mkTuple(n);
1876 h = ap(h,mkOffset(i));
1878 h = fn(mkOffset(n),h);
1882 /* --------------------------------------------------------------------------
1883 * Two forms of kind expression are used quite frequently:
1884 * * -> * -> ... -> * -> * for kinds of ->, [], ->, (,) etc...
1885 * v1 -> v2 -> ... -> vn -> vn+1 skeletons for constructor kinds
1886 * Expressions of these forms are produced by the following functions which
1887 * use a cache to avoid repeated construction of commonly used values.
1888 * A similar approach is used to store the types of tuple constructors in the
1889 * main type checker.
1890 * ------------------------------------------------------------------------*/
1892 #define MAXKINDFUN 10
1893 static Kind simpleKindCache[MAXKINDFUN];
1894 static Kind varKindCache[MAXKINDFUN];
1896 static Kind local makeSimpleKind(n) /* construct * -> ... -> * (n args)*/
1904 Kind simpleKind(n) /* return (possibly cached) simple */
1905 Int n; { /* function kind */
1907 return makeSimpleKind(n);
1908 else if (nonNull(simpleKindCache[n]))
1909 return simpleKindCache[n];
1911 return simpleKindCache[0] = STAR;
1913 return simpleKindCache[n] = ap(STAR,simpleKind(n-1));
1916 static Kind local makeVarKind(n) /* construct v0 -> .. -> vn */
1918 Kind k = mkOffset(n);
1920 k = ap(mkOffset(n),k);
1924 Void varKind(n) /* return (possibly cached) var */
1925 Int n; { /* function kind */
1926 typeOff = newKindvars(n+1);
1928 typeIs = makeVarKind(n);
1929 else if (nonNull(varKindCache[n]))
1930 typeIs = varKindCache[n];
1932 typeIs = varKindCache[n] = makeVarKind(n);
1935 /* --------------------------------------------------------------------------
1936 * Substitutution control:
1937 * ------------------------------------------------------------------------*/
1939 Void substitution(what)
1944 case RESET : emptySubstitution();
1949 case MARK : for (i=0; i<MAXTUPCON; ++i)
1950 mark(tupleConTypes[i]);
1951 for (i=0; i<MAXKINDFUN; ++i) {
1952 mark(simpleKindCache[i]);
1953 mark(varKindCache[i]);
1955 for (i=0; i<numTyvars; ++i)
1956 mark(tyvars[i].bound);
1967 case POSTPREL: break;
1969 case PREPREL : substitution(RESET);
1970 for (i=0; i<MAXTUPCON; ++i)
1971 tupleConTypes[i] = NIL;
1972 for (i=0; i<MAXKINDFUN; ++i) {
1973 simpleKindCache[i] = NIL;
1974 varKindCache[i] = NIL;
1977 trexShow = mkQCon(findText("Trex"),
1978 findText("ShowRecRow"));
1979 trexEq = mkQCon(findText("Trex"),
1980 findText("EqRecRow"));
1986 /*-------------------------------------------------------------------------*/