2 /* --------------------------------------------------------------------------
3 * Provides an implementation for the `current substitution' used during
4 * type and kind inference in both static analysis and type checking.
6 * Hugs 98 is Copyright (c) Mark P Jones, Alastair Reid and the Yale
7 * Haskell Group 1994-99, and is distributed as Open Source software
8 * under the Artistic License; see the file "Artistic" that is included
9 * in the distribution for details.
11 * $RCSfile: subst.c,v $
13 * $Date: 1999/04/27 10:07:07 $
14 * ------------------------------------------------------------------------*/
23 /*#define DEBUG_TYPES*/
25 static Int numTyvars; /* no. type vars currently in use */
26 static Int maxTyvars = 0;
27 static Int nextGeneric; /* number of generics found so far */
30 Tyvar tyvars[NUM_TYVARS]; /* storage for type variables */
32 Tyvar *tyvars = 0; /* storage for type variables */
34 Int typeOff; /* offset of result type */
35 Type typeIs; /* skeleton of result type */
36 Int typeFree; /* freedom in instantiated type */
37 List predsAre; /* list of predicates in type */
38 List genericVars; /* list of generic vars */
39 List btyvars = NIL; /* explicitly scoped type vars */
41 /* --------------------------------------------------------------------------
42 * local function prototypes:
43 * ------------------------------------------------------------------------*/
45 static Void local expandSubst Args((Int));
46 static Int local findBtyvsInt Args((Text));
47 static Type local makeTupleType Args((Int));
48 static Kind local makeSimpleKind Args((Int));
49 static Kind local makeVarKind Args((Int));
50 static Void local expandSyn1 Args((Tycon, Type *, Int *));
51 static Type local dropRank1Body Args((Type,Int,Int));
52 static Type local liftRank1Body Args((Type,Int));
54 static Bool local varToVarBind Args((Tyvar *,Tyvar *));
55 static Bool local varToTypeBind Args((Tyvar *,Type,Int));
57 static Bool local inserter Args((Type,Int,Type,Int));
58 static Int local remover Args((Text,Type,Int));
59 static Int local tailVar Args((Type,Int));
61 static Bool local kvarToVarBind Args((Tyvar *,Tyvar *));
62 static Bool local kvarToTypeBind Args((Tyvar *,Type,Int));
64 /* --------------------------------------------------------------------------
65 * The substitution, types, and kinds:
67 * In early versions of Gofer, the `substitution' data structure was only
68 * used by the type checker, so it made sense to include support for it in
69 * type.c. This changed when kinds and kind inference where introduced,
70 * which required access to the substitution during static analysis. The
71 * links between type.c and static.c that were intially used to accomplish
72 * this have now been avoided by making the substitution visible as an
73 * independent data structure in storage.c.
75 * In the same way that values have types, type constructors (and more
76 * generally, expressions built from such constructors) have kinds.
77 * The syntax of kinds in the current implementation is very simple:
79 * kind ::= STAR -- the kind of types
80 * | kind => kind -- constructors
81 * | variables -- either INTCELL or OFFSET
83 * For various reasons, this implementation uses structure sharing, instead
84 * of a copying approach. In principal, this is fast and avoids the need to
85 * build new type expressions. Unfortunately, this implementation will not
86 * be able to handle *very* large expressions.
88 * The substitution is represented by an array of type variables each of
90 * bound a (skeletal) type expression, or NIL if the variable
91 * is not bound, or SKOLEM for a Skolem constant (i.e., an
92 * uninstantiable variable).
93 * offs offset of skeleton in bound. If isNull(bound), then offs is
94 * used to indicate whether that variable is generic (i.e. free
95 * in the current assumption set) or fixed (i.e. bound in the
96 * current assumption set). Generic variables are assigned
97 * offset numbers whilst copying type expressions (t,o) to
98 * obtain their most general form.
99 * kind kind of value bound to type variable (`type variable' is
100 * rather inaccurate -- `constructor variable' would be better).
101 * ------------------------------------------------------------------------*/
103 Void emptySubstitution() { /* clear current substitution */
106 if (maxTyvars!=NUM_TYVARS) {
121 static Void local expandSubst(n) /* add further n type variables to */
122 Int n; { /* current substituion */
124 if (numTyvars+n>NUM_TYVARS) {
125 ERRMSG(0) "Too many type variables in type checker"
129 if (numTyvars+n>maxTyvars) { /* need to expand substitution */
130 Int newMax = maxTyvars+NUM_TYVARS;
134 if (numTyvars+n>newMax) { /* safety precaution */
135 ERRMSG(0) "Substitution expanding too quickly"
139 /* It would be better to realloc() here, but that isn't portable
140 * enough for calloc()ed arrays. The following code could cause
141 * a space leak if an interrupt occurs while we're copying the
142 * array ... we won't worry about this for the time being because
143 * we don't expect to have to go through this process much (if at
144 * all) in normal use of the type checker.
147 newTvs = (Tyvar *)calloc(newMax,sizeof(Tyvar));
149 ERRMSG(0) "Too many variables (%d) in type checker", newMax
152 for (i=0; i<numTyvars;++i) { /* copy substitution */
153 newTvs[i].offs = tyvars[i].offs;
154 newTvs[i].bound = tyvars[i].bound;
155 newTvs[i].kind = tyvars[i].kind;
157 maxTyvars = 0; /* protection from SIGINT? */
158 if (tyvars) free(tyvars);
165 Int newTyvars(n) /* allocate new type variables */
166 Int n; { /* all of kind STAR */
167 Int beta = numTyvars;
170 for (numTyvars+=n; n>0; n--) {
171 tyvars[numTyvars-n].offs = UNUSED_GENERIC;
172 tyvars[numTyvars-n].bound = NIL;
173 tyvars[numTyvars-n].kind = STAR;
175 Printf("new type variable: _%d ::: ",numTyvars-n);
176 printKind(stdout,tyvars[numTyvars-n].kind);
183 Int newKindedVars(k) /* allocate new variables with */
184 Kind k; { /* specified kinds */
185 Int beta = numTyvars; /* if k = k0 -> k1 -> ... -> kn */
186 for (; isPair(k); k=snd(k)) { /* then allocate n vars with kinds */
187 expandSubst(1); /* k0, k1, ..., k(n-1) */
188 tyvars[numTyvars].offs = UNUSED_GENERIC;
189 tyvars[numTyvars].bound = NIL;
190 tyvars[numTyvars].kind = fst(k);
192 Printf("new type variable: _%d ::: ",numTyvars);
193 printKind(stdout,tyvars[numTyvars].kind);
201 Void instantiate(type) /* instantiate type, if nonNull */
207 if (nonNull(typeIs)) { /* instantiate type expression ? */
209 if (isPolyType(typeIs)) { /* Polymorphic type scheme ? */
210 Kinds ks = polySigOf(typeIs);
211 typeOff = newKindedVars(ks);
212 typeIs = monotypeOf(typeIs);
213 for (; isAp(ks); ks=arg(ks))
217 if (whatIs(typeIs)==QUAL) { /* Qualified type? */
218 predsAre = fst(snd(typeIs));
219 typeIs = snd(snd(typeIs));
224 /* --------------------------------------------------------------------------
225 * Bound type variables:
226 * ------------------------------------------------------------------------*/
228 Pair findBtyvs(t) /* Look for bound tyvar */
231 for (; nonNull(bts); bts=tl(bts)) {
233 for (; nonNull(bts1); bts1=tl(bts1))
234 if (t==textOf(fst(hd(bts1))))
240 static Int local findBtyvsInt(t) /* Look for bound type variable */
241 Text t; { /* expecting to find an integer */
242 Pair p = findBtyvs(t);
244 internal("findBtyvsInt");
245 return intOf(snd(p));
248 Void markBtyvs() { /* Mark explicitly scoped vars */
250 for (; nonNull(bts); bts=tl(bts)) {
252 for (; nonNull(bts1); bts1=tl(bts1))
253 markTyvar(intOf(snd(hd(bts1))));
257 Type localizeBtyvs(t) /* Localize type to eliminate refs */
258 Type t; { /* to explicitly scoped vars */
261 case POLYTYPE : snd(snd(t)) = localizeBtyvs(snd(snd(t)));
264 case QUAL : fst(snd(t)) = localizeBtyvs(fst(snd(t)));
265 snd(snd(t)) = localizeBtyvs(snd(snd(t)));
268 case AP : fst(t) = localizeBtyvs(fst(t));
269 snd(t) = localizeBtyvs(snd(t));
273 case VAROPCELL: return mkInt(findBtyvsInt(textOf(t)));
278 /* --------------------------------------------------------------------------
279 * Dereference or bind types in subsitution:
280 * ------------------------------------------------------------------------*/
282 Tyvar *getTypeVar(t,o) /* get number of type variable */
283 Type t; /* represented by (t,o) [if any]. */
286 case INTCELL : return tyvar(intOf(t));
287 case OFFSET : return tyvar(o+offsetOf(t));
289 case VAROPCELL : return tyvar(findBtyvsInt(textOf(t)));
294 Void tyvarType(vn) /* load type held in type variable */
295 Int vn; { /* vn into (typeIs,typeOff) */
298 while ((tyv=tyvar(vn)), isBound(tyv))
299 switch(whatIs(tyv->bound)) {
300 case INTCELL : vn = intOf(tyv->bound);
303 case OFFSET : vn = offsetOf(tyv->bound)+(tyv->offs);
307 case VAROPCELL : vn = findBtyvsInt(textOf(tyv->bound));
310 default : typeIs = tyv->bound;
318 Void bindTv(vn,t,o) /* set type variable vn to (t,o) */
322 Tyvar *tyv = tyvar(vn);
326 Printf("binding type variable: _%d to ",vn);
327 printType(stdout,debugType(t,o));
332 Cell getDerefHead(t,o) /* get value at head of type exp. */
342 if ((tyv=getTypeVar(t,o)) && isBound(tyv)) {
352 /* --------------------------------------------------------------------------
353 * Expand type synonyms:
354 * ------------------------------------------------------------------------*/
356 Void expandSyn(h,ar,at,ao) /* Expand type synonym with: */
357 Tycon h; /* head h */
358 Int ar; /* ar args (NB. ar>=tycon(h).arity)*/
359 Type *at; /* original expression (*at,*ao) */
360 Int *ao; { /* expansion returned in (*at,*ao) */
361 ar -= tycon(h).arity; /* calculate surplus arguments */
364 else { /* if there are more args than the */
365 Type t = *at; /* arity, we have to do a little */
366 Int o = *ao; /* bit of work to isolate args that*/
367 Type args = NIL; /* will not be changed by expansion*/
369 while (ar-- > 0) { /* find part to expand, and the */
370 Tyvar *tyv; /* unused arguments */
371 args = cons(arg(t),args);
375 expandSyn1(h,&t,&o); /* do the expansion */
376 bindTv((i=newTyvars(1)),t,o); /* and embed the results back in */
377 tyvar(i)->kind = getKind(t,o); /* (*at, *ao) as required */
378 *at = applyToArgs(mkInt(i),args);
382 static Void local expandSyn1(h,at,ao) /* Expand type synonym with: */
383 Tycon h; /* head h, tycon(h).arity args, */
384 Type *at; /* original expression (*at,*ao) */
385 Int *ao; { /* expansion returned in (*at,*ao) */
386 Int n = tycon(h).arity;
392 *ao = newKindedVars(tycon(h).kind);
393 for (; 0<n--; t=fun(t)) {
396 internal("expandSyn1");
397 bindTv(*ao+n,arg(t),o);
401 /* --------------------------------------------------------------------------
402 * Marking fixed variables in type expressions:
403 * ------------------------------------------------------------------------*/
405 Void clearMarks() { /* Set all unbound type vars to */
406 Int i; /* unused generic variables */
407 for (i=0; i<numTyvars; ++i)
408 if (!isBound(tyvar(i)))
409 tyvar(i)->offs = UNUSED_GENERIC;
414 Void markAllVars() { /* Set all unbound type vars to */
415 Int i; /* be fixed vars */
416 for (i=0; i<numTyvars; ++i)
417 if (!isBound(tyvar(i)))
418 tyvar(i)->offs = FIXED_TYVAR;
423 Void resetGenerics() { /* Reset all generic vars to unused*/
425 for (i=0; i<numTyvars; ++i)
426 if (!isBound(tyvar(i)) && tyvar(i)->offs>=GENERIC)
427 tyvar(i)->offs = UNUSED_GENERIC;
432 Void markTyvar(vn) /* mark fixed vars in type bound to*/
433 Int vn; { /* given type variable */
434 Tyvar *tyv = tyvar(vn);
437 markType(tyv->bound, tyv->offs);
439 (tyv->offs) = FIXED_TYVAR;
442 Void markType(t,o) /* mark fixed vars in type (t,o) */
454 case AP : markType(fst(t),o);
458 case OFFSET : markTyvar(o+offsetOf(t));
461 case INTCELL : markTyvar(intOf(t));
465 case VAROPCELL : markTyvar(findBtyvsInt(textOf(t)));
468 case RANK2 : markType(snd(snd(t)),o);
471 default : internal("markType");
475 Void markPred(pi) /* Marked fixed type vars in pi */
478 Int o = intOf(snd3(pi));
480 for (; isAp(cl); cl=fun(cl))
484 /* --------------------------------------------------------------------------
485 * Copy type expression from substitution to make a single type expression:
486 * ------------------------------------------------------------------------*/
488 Type copyTyvar(vn) /* calculate most general form of */
489 Int vn; { /* type bound to given type var */
490 Tyvar *tyv = tyvar(vn);
492 if ((tyv->bound)==SKOLEM) {
494 } else if (tyv->bound) {
495 return copyType(tyv->bound,tyv->offs);
499 case FIXED_TYVAR : return mkInt(vn);
501 case UNUSED_GENERIC : (tyv->offs) = GENERIC + nextGeneric++;
502 if (nextGeneric>=NUM_OFFSETS) {
504 "Too many quantified type variables"
507 genericVars = cons(mkInt(vn),genericVars);
509 default : return mkOffset(tyv->offs - GENERIC);
513 Type copyType(t,o) /* calculate most general form of */
514 Type t; /* type expression (t,o) */
517 case AP : { Type l = copyType(fst(t),o);/* ensure correct */
518 Type r = copyType(snd(t),o);/* eval. order */
521 case OFFSET : return copyTyvar(o+offsetOf(t));
522 case INTCELL : return copyTyvar(intOf(t));
524 case VAROPCELL : return copyTyvar(findBtyvsInt(textOf(t)));
530 Cell copyPred(pi,o) /* Copy single predicate (or part */
531 Cell pi; /* thereof) ... */
534 Cell temp = copyPred(fun(pi),o);/* to ensure correct order of eval.*/
535 return ap(temp,copyType(arg(pi),o));
542 Type debugTyvar(vn) /* expand type structure in full */
543 Int vn; { /* detail */
544 Tyvar *tyv = tyvar(vn);
547 return debugType(tyv->bound,tyv->offs);
555 case AP : { Type l = debugType(fst(t),o);
556 Type r = debugType(snd(t),o);
559 case OFFSET : return debugTyvar(o+offsetOf(t));
560 case INTCELL : return debugTyvar(intOf(t));
562 case VAROPCELL : return debugTyvar(findBtyvsInt(textOf(t)));
567 #endif /*DEBUG_TYPES*/
569 Kind copyKindvar(vn) /* build kind attatched to variable*/
571 Tyvar *tyv = tyvar(vn);
573 return copyKind(tyv->bound,tyv->offs);
574 return STAR; /* any unbound variable defaults to*/
575 } /* the kind of all types */
577 Kind copyKind(k,o) /* build kind expression from */
578 Kind k; /* given skeleton */
581 case AP : { Kind l = copyKind(fst(k),o); /* ensure correct */
582 Kind r = copyKind(snd(k),o); /* eval. order */
585 case OFFSET : return copyKindvar(o+offsetOf(k));
586 case INTCELL : return copyKindvar(intOf(k));
591 /* --------------------------------------------------------------------------
592 * Droping and lifting of type schemes that appear in rank 2 position:
593 * ------------------------------------------------------------------------*/
595 Type dropRank2(t,alpha,n) /* Drop a (potentially) rank2 type */
599 if (whatIs(t)==RANK2) {
600 Cell r = fst(snd(t));
603 for (t=snd(snd(t)); i>0; i--) {
604 Type a = arg(fun(t));
606 a = dropRank1(a,alpha,n);
610 t = ap(RANK2,pair(r,revOnto(as,t)));
615 Type dropRank1(t,alpha,n) /* Copy rank1 argument type t to */
616 Type t; /* make a rank1 type scheme */
619 if (n>0 && isPolyType(t))
620 t = mkPolyType(polySigOf(t),dropRank1Body(monotypeOf(t),alpha,n));
624 static Type local dropRank1Body(t,alpha,n)
629 case OFFSET : { Int m = offsetOf(t);
630 return (m>=n) ? mkOffset(m-n) : mkInt(alpha+m);
633 case POLYTYPE : return mkPolyType(polySigOf(t),
634 dropRank1Body(monotypeOf(t),alpha,n));
636 case QUAL : return ap(QUAL,dropRank1Body(snd(t),alpha,n));
638 case RANK2 : return ap(RANK2,pair(fst(snd(t)),
639 dropRank1Body(snd(snd(t)),
643 case AP : return ap(dropRank1Body(fun(t),alpha,n),
644 dropRank1Body(arg(t),alpha,n));
650 Void liftRank2Args(as,alpha,m)
657 for (m=nextGeneric; nonNull(as); as=tl(as)) {
658 Type ta = arg(fun(as));
659 ta = isPolyType(ta) ? liftRank1Body(ta,m) : copyType(ta,alpha);
665 Type liftRank2(t,alpha,m)
669 if (whatIs(t)==RANK2) {
670 Cell r = fst(snd(t));
677 for (i=intOf(r); i>0; i--) {
678 Type a = arg(fun(t));
679 a = isPolyType(a) ? liftRank1Body(a,m) : copyType(a,alpha);
683 t = ap(RANK2,pair(r,revOnto(as,copyType(t,alpha))));
686 t = copyType(t,alpha);
690 Type liftRank1(t,alpha,m)
694 if (m>0 && isPolyType(t)) {
699 t = liftRank1Body(t,nextGeneric);
704 static Type local liftRank1Body(t,n)
708 case OFFSET : return mkOffset(n+offsetOf(t));
710 case INTCELL : return copyTyvar(intOf(t));
713 case VAROPCELL : return copyTyvar(findBtyvsInt(textOf(t)));
715 case POLYTYPE : return mkPolyType(polySigOf(t),
716 liftRank1Body(monotypeOf(t),n));
718 case QUAL : return ap(QUAL,liftRank1Body(snd(t),n));
720 case RANK2 : return ap(RANK2,pair(fst(snd(t)),
721 liftRank1Body(snd(snd(t)),n)));
723 case AP : return ap(liftRank1Body(fun(t),n),
724 liftRank1Body(arg(t),n));
730 /* --------------------------------------------------------------------------
731 * Support for `kind preserving substitutions' from unification:
732 * ------------------------------------------------------------------------*/
734 Bool eqKind(k1,k2) /* check that two (mono)kinds are */
735 Kind k1, k2; { /* equal */
737 || (isPair(k1) && isPair(k2)
738 && eqKind(fst(k1),fst(k2))
739 && eqKind(snd(k1),snd(k2)));
742 Kind getKind(c,o) /* Find kind of constr during type */
743 Cell c; /* checking process */
745 if (isAp(c)) /* application */
746 return snd(getKind(fst(c),o));
748 case TUPLE : return simpleKind(tupleOf(c)); /*(,)::* -> * -> * */
749 case OFFSET : return tyvar(o+offsetOf(c))->kind;
750 case INTCELL : return tyvar(intOf(c))->kind;
752 case VAROPCELL : return tyvar(findBtyvsInt(textOf(c)))->kind;
753 case TYCON : return tycon(c).kind;
755 case EXT : return extKind;
759 Printf("getKind c = %d, whatIs=%d\n",c,whatIs(c));
762 return STAR;/* not reached */
765 /* --------------------------------------------------------------------------
766 * Find generic variables in a type:
767 * ------------------------------------------------------------------------*/
769 Type genvarTyvar(vn,vs) /* calculate list of generic vars */
770 Int vn; /* thru variable vn, prepended to */
771 List vs; { /* list vs */
772 Tyvar *tyv = tyvar(vn);
775 return genvarType(tyv->bound,tyv->offs,vs);
776 else if (tyv->offs == UNUSED_GENERIC) {
777 tyv->offs += GENERIC + nextGeneric++;
778 return cons(mkInt(vn),vs);
780 else if (tyv->offs>=GENERIC && !intIsMember(vn,vs))
781 return cons(mkInt(vn),vs);
786 List genvarType(t,o,vs) /* calculate list of generic vars */
787 Type t; /* in type expression (t,o) */
788 Int o; /* results are prepended to vs */
791 case AP : return genvarType(snd(t),o,genvarType(fst(t),o,vs));
792 case OFFSET : return genvarTyvar(o+offsetOf(t),vs);
793 case INTCELL : return genvarTyvar(intOf(t),vs);
795 case VAROPCELL : return genvarTyvar(findBtyvsInt(textOf(t)),vs);
800 /* --------------------------------------------------------------------------
802 * ------------------------------------------------------------------------*/
804 Bool doesntOccurIn(lookFor,t,o) /* Return TRUE if var lookFor */
805 Tyvar *lookFor; /* isn't referenced in (t,o) */
812 if (tyv) /* type variable */
814 else if (isAp(t)) { /* application */
815 if (doesntOccurIn(lookFor,snd(t),o))
820 else /* no variable found */
826 /* --------------------------------------------------------------------------
827 * Unification algorithm:
828 * ------------------------------------------------------------------------*/
830 char *unifyFails = 0; /* Unification error message */
831 static Int bindAbove = 0; /* Used to restrict var binding */
833 #define bindOnlyAbove(beta) bindAbove=beta
834 #define noBind() bindAbove=MAXPOSINT
835 #define unrestrictBind() bindAbove=0
837 static Bool local varToVarBind(tyv1,tyv2)/* Make binding tyv1 := tyv2 */
838 Tyvar *tyv1, *tyv2; {
839 if (tyv1!=tyv2) { /* If vars are same, nothing to do!*/
841 /* Check that either tyv1 or tyv2 is in allowed range for binding */
842 /* and is not a Skolem constant, and swap vars if nec. so we can */
845 if (tyvNum(tyv1)<bindAbove || tyv1->bound==SKOLEM) {
846 if (tyvNum(tyv2)<bindAbove || tyv2->bound==SKOLEM) {
847 unifyFails = "types do not match";
856 if (!eqKind(tyv1->kind,tyv2->kind)) {
857 unifyFails = "constructor variable kinds do not match";
861 tyv1->offs = tyvNum(tyv2);
863 Printf("vv binding tyvar: _%d to _%d\n",tyvNum(tyv1),tyvNum(tyv2));
869 static Bool local varToTypeBind(tyv,t,o)/* Make binding tyv := (t,o) */
871 Type t; /* guaranteed not to be a v'ble or */
872 Int o; { /* have synonym as outermost constr*/
873 if (tyvNum(tyv)<bindAbove) { /* Check that tyv is in range */
874 unifyFails = "types do not match";
877 else if (tyv->bound == SKOLEM) { /* Check that it is not Skolemized */
878 unifyFails = "cannot instantiate Skolem constant";
881 else if (!doesntOccurIn(tyv,t,o)) /* Carry out occurs check */
882 unifyFails = "unification would give infinite type";
883 else if (!eqKind(tyv->kind,getKind(t,o)))
884 unifyFails = "kinds do not match";
889 Printf("vt binding type variable: _%d to ",tyvNum(tyv));
890 printType(stdout,debugType(t,o));
898 Bool unify(t1,o1,t2,o2) /* Main unification routine */
899 Type t1,t2; /* unify (t1,o1) with (t2,o2) */
908 return varToVarBind(tyv1,tyv2); /* t1, t2 variables */
910 Cell h2 = getDerefHead(t2,o2); /* t1 variable, t2 not */
911 if (isSynonym(h2) && argCount>=tycon(h2).arity) {
912 expandSyn(h2,argCount,&t2,&o2);
916 return varToTypeBind(tyv1,t2,o2);
921 Cell h1 = getDerefHead(t1,o1); /* t2 variable, t1 not */
922 if (isSynonym(h1) && argCount>=tycon(h1).arity) {
923 expandSyn(h1,argCount,&t1,&o1);
927 return varToTypeBind(tyv2,t1,o1);
929 else { /* t1, t2 not vars */
930 Type h1 = getDerefHead(t1,o1);
932 Type h2 = getDerefHead(t2,o2);
936 Printf("tt unifying types: ");
937 printType(stdout,debugType(t1,o1));
939 printType(stdout,debugType(t2,o2));
942 if (isOffset(h1) || isInt(h1)) h1=NIL; /* represent var by NIL*/
943 if (isOffset(h2) || isInt(h2)) h2=NIL;
946 if (isExt(h1) || isExt(h2)) {
947 if (a1==2 && isExt(h1) && a2==2 && isExt(h2)) {
948 if (extText(h1)==extText(h2)) {
949 return unify(arg(fun(t1)),o1,arg(fun(t2)),o2) &&
950 unify(arg(t1),o1,arg(t2),o2);
952 return inserter(t1,o1,t2,o2) &&
953 unify(arg(t1),o1,aVar,
954 remover(extText(h1),t2,o2));
957 unifyFails = "rows are not compatible";
962 if (nonNull(h1) && h1==h2) {/* Assuming well-formed types, both*/
963 if (a1!=a2) { /* t1, t2 must have same no of args*/
964 unifyFails = "incompatible constructors";
968 if (!unify(arg(t1),o1,arg(t2),o2))
979 /* Types do not match -- look for type synonyms to expand */
981 if (isSynonym(h1) && a1>=tycon(h1).arity) {
982 expandSyn(h1,a1,&t1,&o1);
986 if (isSynonym(h2) && a2>=tycon(h2).arity) {
987 expandSyn(h2,a2,&t2,&o2);
992 if ((isNull(h1) && a1<=a2) || /* last attempt -- maybe */
993 (isNull(h2) && a2<=a1)) { /* one head is a variable? */
998 if (tyv1) { /* unify heads! */
1000 return varToVarBind(tyv1,tyv2);
1002 return varToTypeBind(tyv1,t2,o2);
1005 return varToTypeBind(tyv2,t1,o1);
1007 /* at this point, neither t1 nor t2 is a variable. In */
1008 /* addition, they must both be APs unless one of the */
1009 /* head variables has been bound during unification of */
1010 /* the arguments. */
1012 if (!isAp(t1) || !isAp(t2)) { /* might not be APs*/
1016 if (!unify(arg(t1),o1,arg(t2),o2)) /* o/w must be APs */
1028 static Bool local inserter(r1,o1,r,o) /* Insert first field in (r1,o1) */
1029 Type r1; /* into row (r,o), both of which */
1030 Int o1; /* are known to begin with an EXT */
1033 Text labt = extText(fun(fun(r1))); /* Find the text of the label */
1035 Printf("inserting ");
1036 printType(stdout,debugType(r1,o1));
1038 printType(stdout,debugType(r,o));
1045 Int beta; /* Test for common tail */
1046 if (tailVar(arg(r1),o1)==tyvNum(tyv)) {
1047 unifyFails = "distinct rows have common tail";
1050 beta = newTyvars(1); /* Extend row with new field */
1051 tyvar(beta)->kind = ROW;
1052 return varToTypeBind(tyv,ap(fun(r1),mkInt(beta)),o1);
1054 else if (isAp(r) && isAp(fun(r)) && isExt(fun(fun(r)))) {
1055 if (labt==extText(fun(fun(r))))/* Compare existing fields */
1056 return unify(arg(fun(r1)),o1,extField(r),o);
1057 r = extRow(r); /* Or skip to next field */
1059 else { /* Nothing else will match */
1060 unifyFails = "field mismatch";
1066 static Int local remover(l,r,o) /* Make a new row by copying (r,o) */
1067 Text l; /* but removing the l field (which */
1068 Type r; /* MUST exist) */
1071 Int beta = newTyvars(1);
1072 tyvar(beta)->kind = ROW;
1074 Printf("removing %s from",textToStr(l));
1075 printType(stdout,debugType(r,o));
1079 if (tyv || !isAp(r) || !isAp(fun(r)) || !isExt(fun(fun(r))))
1080 internal("remover");
1081 if (l==extText(fun(fun(r))))
1084 r = ap(fun(r),mkInt(remover(l,extRow(r),o)));
1090 static Int local tailVar(r,o) /* Find var at tail end of a row */
1099 else if (isAp(r) && isAp(fun(r)) && isExt(fun(fun(r)))) {
1110 Bool typeMatches(type,mt) /* test if type matches monotype mt*/
1111 Type type, mt; { /* imported from STG Hugs */
1113 if (isPolyType(type) || whatIs(type)==QUAL)
1115 emptySubstitution();
1117 result = unify(mt,0,type,0);
1119 emptySubstitution();
1125 /* --------------------------------------------------------------------------
1126 * Matching predicates:
1128 * There are (at least) four situations where we need to match up pairs
1131 * 1) Testing to see if two predicates are the same (ignoring differences
1132 * caused by the use of type synonyms, for example).
1134 * 2) Matching a predicate with the head of its class so that we can
1135 * find the corresponding superclass predicates. If the predicates
1136 * have already been kind-checked, and the classes are known to be
1137 * the same, then this should never fail.
1139 * 3) Matching a predicate against the head of an instance to see if
1140 * that instance is applicable.
1142 * 4) Matching two instance heads to see if there is an overlap.
1144 * For (1), we need a matching process that does not bind any variables.
1145 * For (2) and (3), we need to use one-way matching, only allowing
1146 * variables in the class or instance head to be instantiated. For
1147 * (4), we need two-way unification.
1149 * Another situation in which both one-way and two-way unification might
1150 * be used is in an implementation of improvement. Here, a one-way match
1151 * would be used to determine applicability of a rule for improvement
1152 * that would then be followed by unification with another predicate.
1153 * One possible syntax for this might be:
1155 * instance P => pi [improves pi'] where ...
1157 * The intention here is that any predicate matching pi' can be unified
1158 * with pi to get more accurate types. A simple example of this is:
1160 * instance Collection [a] a improves Collection [a] b where ...
1162 * As soon as we know what the collection type is (in this case, a list),
1163 * we will also know what the element type is. To ensure that the rule
1164 * for improvement is valid, the compilation system will also need to use
1165 * a one-way matching process to ensure that pi is a (substitution) instance
1166 * of pi'. Another extension would be to allow more than one predicate pi'
1167 * in an improving rule. Read the paper on simplification and improvement
1168 * for technical background. Watch this space for implementation news!
1169 * ------------------------------------------------------------------------*/
1171 Bool samePred(pi1,o1,pi,o) /* Test to see if predicates are */
1172 Cell pi1; /* the same, with no binding of */
1173 Int o1; /* the variables in either one. */
1174 Cell pi; /* Assumes preds are kind correct */
1175 Int o; { /* with the same class. */
1178 result = unifyPred(pi1,o1,pi,o);
1183 Bool matchPred(pi1,o1,pi,o) /* One way match predicate (pi1,o1)*/
1184 Cell pi1; /* against (pi,o), allowing only */
1185 Int o1; /* vars in 2nd pred to be bound. */
1186 Cell pi; /* Assumes preds are kind correct */
1187 Int o; { /* with the same class and that no */
1188 Bool result; /* vars have been alloc'd since o. */
1190 result = unifyPred(pi1,o1,pi,o);
1195 Bool unifyPred(pi1,o1,pi,o) /* Unify two predicates */
1196 Cell pi1; /* Assumes preds are kind correct */
1197 Int o1; /* with the same class. */
1200 for (; isAp(pi1); pi1=fun(pi1), pi=fun(pi))
1201 if (!unify(arg(pi1),o1,arg(pi),o))
1207 static Cell trexShow = NIL; /* Used to test for show on records*/
1208 static Cell trexEq = NIL; /* Used to test for eq on records */
1211 Inst findInstFor(pi,o) /* Find matching instance for pred */
1212 Cell pi; /* (pi,o), or otherwise NIL. If a */
1213 Int o; { /* match is found, then tyvars from*/
1214 Class c = getHead(pi); /* typeOff have been initialized to*/
1215 List ins; /* allow direct use of specifics. */
1220 for (ins=cclass(c).instances; nonNull(ins); ins=tl(ins)) {
1222 Int beta = newKindedVars(inst(in).kinds);
1223 if (matchPred(pi,o,inst(in).head,beta)) {
1233 { Bool wantShow = (c==findQualClass(trexShow));
1234 Bool wantEither = wantShow || (c==findQualClass(trexEq));
1236 if (wantEither) { /* Generate instances of */
1237 Type t = arg(pi); /* ShowRecRow and EqRecRow */
1238 Tyvar *tyv; /* on the fly */
1244 for (ins=cclass(c).instances; nonNull(ins); ins=tl(ins))
1245 if (getHead(arg(inst(hd(ins)).head))==e) {
1250 in = (wantShow ? addRecShowInst(c,e) : addRecEqInst(c,e));
1251 typeOff = newKindedVars(extKind);
1252 bindTv(typeOff,arg(fun(t)),o);
1253 bindTv(typeOff+1,arg(t),o);
1263 /* --------------------------------------------------------------------------
1264 * Compare type schemes:
1265 * ------------------------------------------------------------------------*/
1267 Bool sameSchemes(s,s1) /* Test to see whether two type */
1268 Type s; /* schemes are the same */
1273 Bool b = isPolyType(s); /* Check quantifiers are the same */
1274 Bool b1 = isPolyType(s1);
1276 if (b && b1 && eqKind(polySigOf(s),polySigOf(s1))) {
1277 Kind k = polySigOf(s);
1279 s1 = monotypeOf(s1);
1280 o = newKindedVars(k);
1281 for (; isAp(k); k=arg(k))
1288 b = (whatIs(s)==QUAL); /* Check that contexts are the same*/
1289 b1 = (whatIs(s1)==QUAL);
1292 List ps = fst(snd(s));
1293 List ps1 = fst(snd(s1));
1295 while (nonNull(ps) && nonNull(ps1)) {
1298 if (getHead(pi)!=getHead(pi1)
1299 || !unifyPred(pi,o,pi1,o))
1305 if (nonNull(ps) || nonNull(ps1))
1314 b = (whatIs(s)==RANK2); /* Check any rank 2 annotations */
1315 b1 = (whatIs(s1)==RANK2);
1317 if (b && b1 && intOf(fst(snd(s)))==intOf(fst(snd(s1)))) {
1318 nr2 = intOf(fst(snd(s)));
1326 for (; nr2>0; nr2--) { /* Deal with rank 2 arguments */
1327 Type t = arg(fun(s));
1328 Type t1 = arg(fun(s1));
1330 b1 = isPolyType(t1);
1333 t = dropRank1(t,o,m);
1334 t1 = dropRank1(t1,o,m);
1335 if (!sameSchemes(t,t1))
1343 b = unify(t,o,t1,o);
1352 noBind(); /* Ensure body types are the same */
1353 b = unify(s,o,s1,o);
1358 /* --------------------------------------------------------------------------
1359 * Unify kind expressions:
1360 * ------------------------------------------------------------------------*/
1362 static Bool local kvarToVarBind(tyv1,tyv2)/* Make binding tyv1 := tyv2 */
1363 Tyvar *tyv1, *tyv2; { /* for kind variable bindings */
1366 tyv1->offs = tyvNum(tyv2);
1368 Printf("vv binding kvar: _%d to _%d\n",tyvNum(tyv1),tyvNum(tyv2));
1374 static Bool local kvarToTypeBind(tyv,t,o)/* Make binding tyv := (t,o) */
1375 Tyvar *tyv; /* for kind variable bindings */
1376 Type t; /* guaranteed not to be a v'ble or */
1377 Int o; { /* have synonym as outermost constr*/
1378 if (doesntOccurIn(tyv,t,o)) {
1382 Printf("vt binding kind variable: _%d to ",tyvNum(tyv));
1383 printType(stdout,debugType(t,o));
1388 unifyFails = "unification would give infinite kind";
1392 Bool kunify(k1,o1,k2,o2) /* Unify kind expr (k1,o1) with */
1393 Kind k1,k2; /* (k2,o2) */
1402 return kvarToVarBind(kyv1,kyv2); /* k1, k2 variables */
1404 return kvarToTypeBind(kyv1,k2,o2); /* k1 variable, k2 not */
1408 return kvarToTypeBind(kyv2,k1,o1); /* k2 variable, k1 not */
1411 Printf("unifying kinds: ");
1412 printType(stdout,debugType(k1,o1));
1414 printType(stdout,debugType(k2,o2));
1417 if (k1==STAR && k2==STAR) /* k1, k2 not vars */
1420 else if (k1==ROW && k2==ROW)
1423 else if (isAp(k1) && isAp(k2))
1424 return kunify(fst(k1),o1,fst(k2),o2) &&
1425 kunify(snd(k1),o1,snd(k2),o2);
1431 /* --------------------------------------------------------------------------
1432 * Tuple type constructors: are generated as necessary. The most common
1433 * n-tuple constructors (n<MAXTUPCON) are held in a cache to avoid
1434 * repeated generation of the constructor types.
1435 * ------------------------------------------------------------------------*/
1437 #define MAXTUPCON 10
1438 static Type tupleConTypes[MAXTUPCON];
1440 Void typeTuple(e) /* find type for tuple constr, using*/
1441 Cell e; { /* tupleConTypes to cache previously*/
1442 Int n = tupleOf(e); /* calculated tuple constr. types. */
1443 typeOff = newTyvars(n);
1445 typeIs = makeTupleType(n);
1446 else if (tupleConTypes[n])
1447 typeIs = tupleConTypes[n];
1449 typeIs = tupleConTypes[n] = makeTupleType(n);
1452 static Type local makeTupleType(n) /* construct type for tuple constr. */
1453 Int n; { /* t1 -> ... -> tn -> (t1,...,tn) */
1454 Type h = mkTuple(n);
1458 h = ap(h,mkOffset(i));
1460 h = fn(mkOffset(n),h);
1464 /* --------------------------------------------------------------------------
1465 * Two forms of kind expression are used quite frequently:
1466 * * -> * -> ... -> * -> * for kinds of ->, [], ->, (,) etc...
1467 * v1 -> v2 -> ... -> vn -> vn+1 skeletons for constructor kinds
1468 * Expressions of these forms are produced by the following functions which
1469 * use a cache to avoid repeated construction of commonly used values.
1470 * A similar approach is used to store the types of tuple constructors in the
1471 * main type checker.
1472 * ------------------------------------------------------------------------*/
1474 #define MAXKINDFUN 10
1475 static Kind simpleKindCache[MAXKINDFUN];
1476 static Kind varKindCache[MAXKINDFUN];
1478 static Kind local makeSimpleKind(n) /* construct * -> ... -> * (n args)*/
1486 Kind simpleKind(n) /* return (possibly cached) simple */
1487 Int n; { /* function kind */
1489 return makeSimpleKind(n);
1490 else if (nonNull(simpleKindCache[n]))
1491 return simpleKindCache[n];
1493 return simpleKindCache[0] = STAR;
1495 return simpleKindCache[n] = ap(STAR,simpleKind(n-1));
1498 static Kind local makeVarKind(n) /* construct v0 -> .. -> vn */
1500 Kind k = mkOffset(n);
1502 k = ap(mkOffset(n),k);
1506 Void varKind(n) /* return (possibly cached) var */
1507 Int n; { /* function kind */
1508 typeOff = newKindvars(n+1);
1510 typeIs = makeVarKind(n);
1511 else if (nonNull(varKindCache[n]))
1512 typeIs = varKindCache[n];
1514 typeIs = varKindCache[n] = makeVarKind(n);
1517 /* --------------------------------------------------------------------------
1518 * Substitutution control:
1519 * ------------------------------------------------------------------------*/
1521 Void substitution(what)
1526 case RESET : emptySubstitution();
1531 case MARK : for (i=0; i<MAXTUPCON; ++i)
1532 mark(tupleConTypes[i]);
1533 for (i=0; i<MAXKINDFUN; ++i) {
1534 mark(simpleKindCache[i]);
1535 mark(varKindCache[i]);
1537 for (i=0; i<numTyvars; ++i)
1538 mark(tyvars[i].bound);
1549 case INSTALL : substitution(RESET);
1550 for (i=0; i<MAXTUPCON; ++i)
1551 tupleConTypes[i] = NIL;
1552 for (i=0; i<MAXKINDFUN; ++i) {
1553 simpleKindCache[i] = NIL;
1554 varKindCache[i] = NIL;
1557 trexShow = mkQCon(findText("Trex"),
1558 findText("ShowRecRow"));
1559 trexEq = mkQCon(findText("Trex"),
1560 findText("EqRecRow"));
1566 /*-------------------------------------------------------------------------*/