/* --------------------------------------------------------------------------
* subst.c: Copyright (c) Mark P Jones 1991-1998. All rights reserved.
* See NOTICE for details and conditions of use etc...
* Hugs version 1.3b, January 1998
*
* Part of type checker dealing with operations on current substitution.
* ------------------------------------------------------------------------*/
static List accumVars; /* holds constrained vars between */
/* unification passes */
static Int lastTyvar; /* last tyvar visited by postUnify()*/
static List lastBounds; /* bounds of lastType */
static List skolVars; /* Current list of skolemized vars */
static List skolVars2; /* Current list of local constr/sel vars */
static Void local checkVars();
static Void local emptySubstitution() { /* clear current substitution */
numTyvars = 0;
#if !FIXED_SUBST
if (maxTyvars!=NUM_TYVARS) {
maxTyvars = 0;
if (tyvars) {
free(tyvars);
tyvars = 0;
}
}
#endif
nextGeneric = 0;
genericVars = NIL;
typeIs = NIL;
accumVars = NIL;
lastBounds = NIL;
lastTyvar = 0;
}
static Void local expandSubst(n) /* add further n type variables to */
Int n; { /* current substituion */
#if FIXED_SUBST
if (numTyvars+n>NUM_TYVARS) {
ERRMSG(0) "Too many type variables in type checker"
EEND;
}
#else
if (numTyvars+n>maxTyvars) { /* need to expand substitution */
Int newMax = maxTyvars+NUM_TYVARS;
Tyvar *newTvs;
Int i;
if (numTyvars+n>newMax) { /* safety precaution */
ERRMSG(0) "Substitution expanding too quickly"
EEND;
}
/* It would be better to realloc() here, but that isn't portable
* enough for calloc()ed arrays. The following code could cause
* a space leak if an interrupt occurs while we're copying the
* array ... we won't worry about this for the time being because
* we don't expect to have to go through this process much (if at
* all) in normal use of the type checker.
*/
newTvs = (Tyvar *)calloc(newMax,sizeof(Tyvar));
if (!newTvs) {
ERRMSG(0) "Too many variables (%d) in type checker", newMax
EEND;
}
for (i=0; i<numTyvars;++i) { /* copy substitution */
newTvs[i].state = tyvars[i].state;
newTvs[i].offs = tyvars[i].offs;
newTvs[i].bound = tyvars[i].bound;
newTvs[i].kind = tyvars[i].kind;
}
maxTyvars = 0; /* protection from SIGINT? */
if (tyvars) free(tyvars);
tyvars = newTvs;
maxTyvars = newMax;
}
#endif
}
static Void local resetState(tyv)
Tyvar *tyv; {
tyv->state = NORMAL;
tyv->bound = NIL;
tyv->offs = UNUSED_GENERIC;
}
static Int local newTyvars(n) /* allocate new type variables */
Int n; { /* all of kind STAR */
Int beta = numTyvars;
expandSubst(n);
for (numTyvars+=n; n>0; n--) {
resetState(tyvar(numTyvars-n));
tyvars[numTyvars-n].kind = STAR;
#ifdef DEBUG_TYPES
printf("new type variable: _%d ::: ",numTyvars-n);
printKind(stdout,tyvars[numTyvars-n].kind);
putchar('\n');
#endif
}
return beta;
}
static Int local newKindedVars(k,inPat) /* allocate new variables with */
Kind k; /* specified kinds */
Bool inPat; { /* if k = k0 -> k1 -> ... -> kn */
Int beta = numTyvars; /* then allocate n vars with kinds */
for (; isPair(k); k=snd(k)) { /* k0, k1, ..., k(n-1) */
expandSubst(1); /* Dealing with quantifiers, if nec*/
resetState(tyvar(numTyvars));
tyvars[numTyvars].kind = fst(k);
#ifdef DEBUG_TYPES
printf("new type variable: _%d ::: ",numTyvars);
printKind(stdout,tyvars[numTyvars].kind);
putchar('\n');
#endif
numTyvars++;
}
return beta;
}
#define deRef(tyv,t,o) while ((tyv=getTypeVar(t,o)) && isBound(tyv)) { \
t = tyv->bound; \
o = tyv->offs; \
}
static Tyvar *local getTypeVar(t,o) /* get number of type variable */
Type t; /* represented by (t,o) [if any]. */
Int o; {
switch (whatIs(t)) {
case INTCELL : return tyvar(intOf(t));
case OFFSET : return tyvar(o+offsetOf(t));
}
return ((Tyvar *)0);
}
static Void local tyvarType(vn) /* load type held in type variable */
Int vn; { /* vn into (typeIs,typeOff) */
Tyvar *tyv;
while ((tyv=tyvar(vn)), isBound(tyv))
switch(whatIs(tyv->bound)) {
case INTCELL : vn = intOf(tyv->bound);
break;
case OFFSET : vn = offsetOf(tyv->bound)+(tyv->offs);
break;
default : typeIs = tyv->bound;
typeOff = tyv->offs;
return;
}
typeIs = var;
typeOff = vn;
}
#define bindTyv(tyv,t,o) tyv->bound = t; tyv->offs = o
static Void local bindTv(vn,t,o) /* set type variable vn to (t,o) */
Int vn;
Type t;
Int o; {
Tyvar *tyv = tyvar(vn);
if (!isNormal(tyv))
internal("bindTv");
bindTyv(tyv,t,o);
#ifdef DEBUG_TYPES
printf("binding type variable: _%d to ",vn);
printType(stdout,debugType(t,o));
putchar('\n');
#endif
}
static Void local expandSyn(h,ar,at,ao) /* Expand type synonym with: */
Tycon h; /* head h */
Int ar; /* ar args (NB. ar>=tycon(h).arity)*/
Type *at; /* original expression (*at,*ao) */
Int *ao; { /* expansion returned in (*at,*ao) */
ar -= tycon(h).arity; /* calculate surplus arguments */
if (ar==0)
expandSyn1(h,at,ao);
else { /* if there are more args than the */
Type t = *at; /* arity, we have to do a little */
Int o = *ao; /* bit of work to isolate args that*/
Type args = NIL; /* will not be changed by expansion*/
Int i;
while (ar-- > 0) { /* find part to expand, and the */
Tyvar *tyv; /* unused arguments */
args = cons(arg(t),args);
t = fun(t);
deRef(tyv,t,o);
}
expandSyn1(h,&t,&o); /* do the expansion */
bindTv((i=newTyvars(1)),t,o); /* and embed the results back in */
tyvar(i)->kind = getKind(t,o); /* (*at, *ao) as required */
*at = applyToArgs(mkInt(i),args);
}
}
static Void local expandSyn1(h,at,ao) /* Expand type synonym with: */
Tycon h; /* head h, tycon(h).arity args, */
Type *at; /* original expression (*at,*ao) */
Int *ao; { /* expansion returned in (*at,*ao) */
Int n = tycon(h).arity;
Type t = *at;
Int o = *ao;
Tyvar *tyv;
*at = tycon(h).defn;
*ao = newKindedVars(tycon(h).kind,FALSE);
for (; 0<n--; t=fun(t)) {
deRef(tyv,t,o);
if (tyv || !isAp(t))
internal("expandSyn1");
bindTv(*ao+n,arg(t),o);
}
}
static Cell local getDerefHead(t,o) /* get value at head of type exp. */
Type t;
Int o; {
Tyvar *tyv;
argCount = 0;
for (;;) {
while (isAp(t)) {
argCount++;
t = fun(t);
}
if ((tyv=getTypeVar(t,o)) && isBound(tyv)) {
t = tyv->bound;
o = tyv->offs;
}
else
break;
}
if (isOffset(t))
return mkInt(offsetOf(t)+o);
else
return t;
}
/* --------------------------------------------------------------------------
* Skolemization:
* ------------------------------------------------------------------------*/
static Void local skolemOffsetsAbove(n,t,o)
Int n;
Type t;
Int o; {
switch(whatIs(t)) {
case AP : skolemOffsetsAbove(n,fst(t),o);
skolemOffsetsAbove(n,snd(t),o);
break;
case OFFSET : if (offsetOf(t) >= n) {
Tyvar *tyv = tyvar(o+offsetOf(t));
if (isBound(tyv))
internal("skolemOffsetsAbove");
if (!isSkolem(tyv)) {
tyv->state = SKOLEM;
hd(skolVars2) = cons(mkInt(o+offsetOf(t)),hd(skolVars2));
}
}
break;
}
}
static Void saveSkolem2() {
skolVars2 = cons(NIL,skolVars2);
}
static Void local restoreSkolem2() {
List vs = hd(skolVars2);
for (; nonNull(vs); vs=tl(vs))
deskolemTyvar(intOf(hd(vs)));
skolVars2 = tl(skolVars2);
}
static Void local skolemTyvar(vn) /* Skolemize type variable */
Int vn; {
Tyvar *tyv = tyvar(vn);
if (isBound(tyv))
skolemType(tyv->bound,tyv->offs);
else if (isUnbound(tyv)) {
tyv->state = SKOLEM;
hd(skolVars) = cons(mkInt(vn),hd(skolVars));
}
}
static Void local skolemType(t,o) /* Skolemize type */
Type t;
Int o; {
switch(whatIs(t)) {
case AP : skolemType(fst(t),o);
skolemType(snd(t),o);
break;
case OFFSET : skolemTyvar(o+offsetOf(t));
break;
case INTCELL : break; /* Must be fresh, don't skolemize */
}
}
static Void local deskolemTyvar(vn) /* Remove skolemization from tyvar */
Int vn; {
Tyvar *tyv = tyvar(vn);
if (!isSkolem(tyv))
internal("deskolemTyvar");
resetState(tyv);
}
static Void saveSkolem() {
skolVars = cons(NIL,skolVars);
}
static Void local restoreSkolem() {
List vs = hd(skolVars);
for (; nonNull(vs); vs=tl(vs))
deskolemTyvar(intOf(hd(vs)));
skolVars = tl(skolVars);
}
/* --------------------------------------------------------------------------
* Count tyvar references in accumulated bounds (used during unification).
* ------------------------------------------------------------------------*/
static Int delta;
#define countWith(n,vn) {delta = n; countTyvar(vn);}
#define countUp(vn) countWith(1,vn)
#define countDown(vn) countWith(-1,vn)
static Void local countTyvar(vn)
Int vn; {
Tyvar *tyv = tyvar(vn);
if (isBound(tyv))
countType(tyv->bound,tyv->offs);
else if (isCloned(tyv))
internal("countTyvar");
else if (!isSkolem(tyv)) {
mkAccum(tyv);
tyv->offs += delta;
if (tyv->offs < 0)
internal("refCount < 0");
}
}
static Void local countType(t,o)
Type t;
Int o; {
switch(whatIs(t)) {
case AP : countType(fst(t),o);
countType(snd(t),o);
break;
case OFFSET : countTyvar(o+offsetOf(t));
break;
case INTCELL : countTyvar(intOf(t));
break;
}
}
/* ----------------------------------------------------------------------
* Accumulating bounds
* ---------------------------------------------------------------------*/
static Void local mkAccum(tyv)
Tyvar *tyv; {
if (!isAccum(tyv)) {
if (!isUnbound(tyv))
internal("mkAccum");
tyv->bound = NIL;
tyv->state = ACCUM;
tyv->offs = 0;
accumVars = cons(mkInt(tyvNum(tyv)),accumVars);
}
}
static Void accumBound(tyv,beta,z)
Tyvar *tyv;
Int beta;
Int z; {
if (z != NONV) {
mkAccum(tyv);
countUp(beta);
tyv->bound = cons(pair(mkInt(beta),mkInt(z)),tyv->bound);
checkVars();
}
}
static Void local deAccum(tyv,decr)
Tyvar *tyv;
Bool decr; {
if (isAccum(tyv)) {
if (decr) {
List bs = tyv->bound;
for (; nonNull(bs); bs=tl(bs))
countDown(intOf(fst(hd(bs))));
}
resetState(tyv);
accumVars = removeCell(mkInt(tyvNum(tyv)),accumVars);
}
}
/* --------------------------------------------------------------------------
* Mark type expression, so that all variables are marked as unused generics
* ------------------------------------------------------------------------*/
static Void local normState() { /* reset state for all unbound vars*/
Int i;
for (i=0; i<numTyvars; ++i) {
Tyvar *tyv = tyvar(i);
if (!isNormal(tyv))
resetState(tyv);
}
}
static Void local clearOffsTyvar(vn)
Int vn; {
Tyvar *tyv = tyvar(vn);
if (isBound(tyv))
clearOffsType(tyv->bound,tyv->offs);
else if (!isAccum(tyv))
tyv->offs = NONV; /* == UNUSED_GENERIC */
}
static Void local clearOffsType(t,o)
Type t;
Int o; {
switch (whatIs(t)) {
case AP : clearOffsType(fst(t),o);
clearOffsType(snd(t),o);
return;
case OFFSET : if (o >= 0) clearOffsTyvar(o+offsetOf(t));
return;
case INTCELL : clearOffsTyvar(intOf(t));
return;
}
}
static Void local clearMarks() { /* set all unbound type vars to */
Int i; /* unused generic variables */
for (i=0; i<numTyvars; ++i) {
Tyvar *tyv = tyvar(i);
if (shouldMark(tyv))
tyv->offs = UNUSED_GENERIC;
}
nextGeneric = 0;
genericVars = NIL;
}
static Void local resetGenericsFrom(n) /* reset all generic vars to unused*/
Int n; { /* for generics >= n */
Int i;
if (n==0) /* reset generic variables list */
genericVars = NIL; /* most common case: reset to zero */
else
for (i=length(genericVars); i>n; i--)
genericVars = tl(genericVars);
for (i=0; i<numTyvars; ++i)
if (shouldMark(tyvar(i)) && tyvar(i)->offs>=GENERIC+n)
tyvar(i)->offs = UNUSED_GENERIC;
nextGeneric = n;
}
static Void local markTyvar(vn) /* mark fixed vars in type bound to*/
Int vn; { /* given type variable */
Tyvar *tyv = tyvar(vn);
if (isBound(tyv))
markType(tyv->bound, tyv->offs);
else if (isAccum(tyv))
internal("markTyvar");
else if (isCloned(tyv)) {
List bs = tyv->bound;
for (; nonNull(bs); bs=tl(bs))
markTyvar(intOf(fst(hd(bs))));
tyv->offs = FIXED_TYVAR;
}
else if (!isSkolem(tyv))
tyv->offs = FIXED_TYVAR;
}
static Void local markType(t,o) /* mark fixed vars in type (t,o) */
Type t;
Int o; {
Int w = whatIs(t);
switch (w) {
case TYCON :
case TUPLE : return;
case AP : markType(fst(t),o);
markType(snd(t),o);
return;
case OFFSET : markTyvar(o+offsetOf(t));
return;
case INTCELL : markTyvar(intOf(t));
return;
default : internal("markType");
}
}
/* --------------------------------------------------------------------------
* Copy type expression from substitution to make a single type expression:
* ------------------------------------------------------------------------*/
static Type local copyTyvar(vn) /* calculate most general form of */
Int vn; { /* type bound to given type var */
Tyvar *tyv = tyvar(vn);
if (isBound(tyv))
return copyType(tyv->bound,tyv->offs);
if (!isNormal(tyv))
return (mkInt(vn));
switch (tyv->offs) {
case FIXED_TYVAR : return mkInt(vn);
case UNUSED_GENERIC : (tyv->offs) = GENERIC + nextGeneric++;
if (nextGeneric>=NUM_OFFSETS) {
ERRMSG(0)
"Too many quantified type variables"
EEND;
}
genericVars = cons(mkInt(vn),genericVars);
default : return mkOffset(tyv->offs - GENERIC);
}
}
static Type local copyType(t,o) /* calculate most general form of */
Type t; /* type expression (t,o) */
Int o; {
switch (whatIs(t)) {
case AP : { Type l = copyType(fst(t),o); /* ensure correct */
Type r = copyType(snd(t),o); /* eval. order */
return ap(l,r);
}
case OFFSET : return copyTyvar(o+offsetOf(t));
case INTCELL : return copyTyvar(intOf(t));
}
return t;
}
static Type local genvarTyvar(vn,vs) /* calculate list of generic vars */
Int vn; /* thru variable vn, prepended to */
List vs; { /* list vs */
Tyvar *tyv = tyvar(vn);
if (isBound(tyv))
return genvarType(tyv->bound,tyv->offs,vs);
else if (!isNormal(tyv))
return vs;
else if (tyv->offs == UNUSED_GENERIC) {
tyv->offs = GENERIC + nextGeneric++;
return cons(mkInt(vn),vs);
}
else if (tyv->offs>=GENERIC && !intIsMember(vn,vs))
return cons(mkInt(vn),vs);
else
return vs;
}
static List local genvarType(t,o,vs) /* calculate list of generic vars */
Type t; /* in type expression (t,o) */
Int o; /* results are prepended to vs */
List vs; {
switch (whatIs(t)) {
case AP : return genvarType(snd(t),o,genvarType(fst(t),o,vs));
case OFFSET : return genvarTyvar(o+offsetOf(t),vs);
case INTCELL : return genvarTyvar(intOf(t),vs);
}
return vs;
}
#ifdef DEBUG_TYPES
static Type local debugTyvar(vn) /* expand type structure in full */
Int vn; { /* detail */
Tyvar *tyv = tyvar(vn);
if (isBound(tyv))
return debugType(tyv->bound,tyv->offs);
return mkInt(vn);
}
static Type local debugType(t,o)
Type t;
Int o; {
switch (whatIs(t)) {
case AP : { Type l = debugType(fst(t),o);
Type r = debugType(snd(t),o);
return ap(l,r);
}
case OFFSET : return debugTyvar(o+offsetOf(t));
case INTCELL : return debugTyvar(intOf(t));
}
return t;
}
#endif /*DEBUG_TYPES*/
/* --------------------------------------------------------------------------
* Compute variance information
* -------------------------------------------------------------------------*/
static Cell local getVariance(h,n)
Type h;
Int n; {
if (isTycon(h))
return skipOver(length(tycon(h).arity)-n,tycon(h).variance);
else if (isTuple(h))
return mkInt(POSV);
else if (isInt(h) || isOffset(h))
return mkInt(INV); /* higer order variance assumption */
else
internal("getVariance");
}
static Int local thisVariance(z)
Cell z; {
if (isPair(z))
return intOf(hd(z));
else if (isInt(z))
return intOf(z);
else
internal("thisVariance");
}
static Cell local nextVariance(z)
Cell z; {
if (isPair(z))
return tl(z);
else if (isInt(z))
return z;
else
internal("nextVariance");
}
static Void local markVarianceTyvar(vn,z) /* mark variance in tyvar */
Int vn;
Int z; {
Tyvar *tyv = tyvar(vn);
if (isBound(tyv))
markVarianceType(tyv->bound, tyv->offs, z);
else if (!isAccum(tyv))
tyv->offs |= z;
}
static Void local markVarianceType(t,o,z) /* mark variance in type */
Type t;
Int o;
Int z; {
switch (whatIs(t)) {
case AP : { Cell z1;
Type h = getHead(t);
if (isInt(h) || (isOffset(h) && o >= 0))
h = getDerefHead(t,o);
z1 = getVariance(h,argCount);
while (isAp(t)) {
Tyvar *tyv;
markVarianceType(arg(t),o,multv(z,thisVariance(z1)));
t = fun(t);
if (isInt(t) || (isOffset(t) && o >= 0))
deRef(tyv,t,o);
z1 = nextVariance(z1);
}
markVarianceType(t,o,z);
}
break;
case OFFSET : if (o >= 0)
markVarianceTyvar(o+offsetOf(t),z);
break;
case INTCELL : markVarianceTyvar(intOf(t),z);
break;
}
}
/* --------------------------------------------------------------------------
* Clone type expression by replacing each tyvar occurrence with a fresh
* copy, and append each new tyvar to the bounds of its origin.
* ------------------------------------------------------------------------*/
static Type local cloneTyvar(vn,z)
Int vn;
Int z; {
Tyvar *tyv = tyvar(vn);
if (isBound(tyv))
return cloneType(tyv->bound,tyv->offs,z);
else {
Int beta;
if (isNormal(tyv)) {
tyv->state = CLONED;
}
if (!isCloned(tyv)) /* Never clone skolemized tyvars */
return mkInt(vn);
else {
beta = newTyvars(1); /* invalidates tyv */
tyv = tyvar(vn);
tyvar(beta)->kind = tyv->kind;
tyv->bound = cons(pair(mkInt(beta),mkInt(z)),tyv->bound);
return fst(hd(tyv->bound));
}
}
}
static Type local cloneType(t,o,z)
Type t;
Int o;
Int z; {
switch (whatIs(t)) {
case TYCON :
case TUPLE : return t;
case AP : { Cell z1;
List args = NIL;
Type h = getHead(t);
if (isInt(h) || (isOffset(h) && o >= 0))
h = getDerefHead(t,o);
z1 = getVariance(h,argCount);
while (isAp(t)) {
Tyvar *tyv;
args = cons(cloneType(arg(t),o,multv(z,thisVariance(z1))),args);
t = fun(t);
if (isInt(t) || (isOffset(t) && o >= 0))
deRef(tyv,t,o);
z1 = nextVariance(z1);
}
t = cloneType(t,o,z);
while (nonNull(args)) {
t = ap(t,hd(args));
args = tl(args);
}
return t;
}
case OFFSET : return (o<0) ? t : cloneTyvar(o+offsetOf(t),z);
case INTCELL : return cloneTyvar(intOf(t),z);
default : internal("cloneType");
}
}
static Type local clone(t,o,z)
Type t;
Int z; {
return cloneType(t,o,z);
}
static Int cloneTv(vn,z)
Int vn;
Int z; {
Type t = clone(var,vn,z);
if (isInt(t))
return intOf(t);
else {
Int beta = newTyvars(1);
bindTv(beta,t,0);
return beta;
}
}
/* --------------------------------------------------------------------------
* Convert a CLONED tyvar to an ACCUM one, i.e. essentially remove the
* tyvars from its bounds and prepare for postunify.
* ------------------------------------------------------------------------*/
static Bool local doAccum(vn)
Int vn; {
Tyvar *tyv = tyvar(vn);
List bs = tyv->bound;
Int saveLastTyvar = lastTyvar;
List saveLastBounds = lastBounds;
resetState(tyv);
lastTyvar = vn;
lastBounds = appendOnto(bs,lastBounds);
for (; nonNull(bs) && bs!=saveLastBounds; bs=tl(bs)) {
Int beta = intOf(fst(hd(bs)));
Int z = intOf(snd(hd(bs)));
if (!accumClonedTyvar(beta,FALSE))
return FALSE;
if (!preUnify(var,beta,var,vn,z))
return FALSE;
}
lastTyvar = saveLastTyvar;
lastBounds = saveLastBounds;
return TRUE;
}
static Bool local accumClonedTyvar(vn,skip)
Int vn;
Bool skip; {
Tyvar *tyv = tyvar(vn);
if (isBound(tyv))
return accumClonedType(tyv->bound,tyv->offs,skip);
else if (isCloned(tyv)) {
if (skip && tyv->offs == FIXED_TYVAR) /* Skip these, since they are reachable */
return TRUE; /* from some other cloned tyvar that will */
else /* be resolved later. */
return doAccum(vn);
}
return TRUE;
}
static Bool local accumClonedType(t,o,skip)
Type t;
Int o;
Bool skip; {
switch (whatIs(t)) {
case AP : if (!accumClonedType(fst(t),o,skip))
return FALSE;
return accumClonedType(snd(t),o,skip);
case INTCELL : return accumClonedTyvar(intOf(t),skip);
case OFFSET : if (o>=0)
return accumClonedTyvar(o+offsetOf(t),skip);
}
return TRUE;
}
static Bool local accumClonedPolyType(t,skip)
Type t;
Bool skip; {
if (isPolyType(t))
t = monoTypeOf(t);
if (whatIs(t) == QUAL)
t = snd(snd(t));
return accumClonedType(t,-1,skip);
}
/* --------------------------------------------------------------------------
* Occurs check:
* ------------------------------------------------------------------------*/
static Tyvar *lookingFor; /* var to look for in occurs check */
static Bool local occursIn(t,o) /* Return TRUE if var lookingFor */
Type t; /* is referenced in (t,o) */
Int o; {
Tyvar *tyv;
for (;;) {
deRef(tyv,t,o);
if (tyv) /* type variable */
return tyv==lookingFor;
else if (isAp(t)) { /* application */
if (occursIn(snd(t),o))
return TRUE;
else
t = fst(t);
}
else /* no variable found */
break;
}
return FALSE;
}
static Bool local occurs(tyv,t,o)
Tyvar *tyv;
Type t;
Int o; {
lookingFor = tyv;
return occursIn(t,o);
}
static Bool local offsetsBetween(lo,hi,t)
Int lo, hi;
Type t; {
switch (whatIs(t)) {
case TYCON :
case TUPLE : return FALSE;
case AP : return offsetsBetween(lo,hi,fun(t)) || offsetsBetween(lo,hi,arg(t));
case OFFSET : return lo < offsetOf(t) && offsetOf(t) <= hi;
default : internal("offsetsBetween");
}
}
/* --------------------------------------------------------------------------
* Unification algorithm:
* ------------------------------------------------------------------------*/
static char *unifyFails = 0; /* unification error message */
static Bool matchMode = FALSE; /* set to TRUE to prevent binding */
/* during matching process */
static Bool local failure(str)
String str; {
unifyFails = str;
checkVars();
return FALSE;
}
static Bool solveAccum(tyv,t,o) /* bind tyv to (t,o) and preUnify */
Tyvar *tyv; /* with accumulated bounds */
Type t;
Int o; {
List bs = NIL;
Int n = 0;
Type h;
if (occurs(tyv,t,o))
return failure("unification would give infinite type");
if (isAccum(tyv)) {
bs = tyv->bound;
n = tyv->offs;
deAccum(tyv,TRUE);
}
bindTyv(tyv,t,o);
if (n > 0)
countWith(n,tyvNum(tyv));
for (; nonNull(bs); bs=tl(bs))
if (!preUnify(var,intOf(fst(hd(bs))),t,o,intOf(snd(hd(bs)))))
return FALSE;
return TRUE;
}
static Bool local varToVarBind(tyv1,tyv2,z) /* Make binding tyv1 := tyv2 */
Tyvar *tyv1;
Tyvar *tyv2;
Int z; {
checkVars();
if (tyv1!=tyv2) {
if (matchMode)
return failure("types do not match");
if (isCloned(tyv1) || isCloned(tyv2))
internal("clones in varToVarBind");
if (!eqKind(tyv1->kind,tyv2->kind))
return failure("constructor variable kinds do not match");
if (!isSkolem(tyv1)) {
if (!isSkolem(tyv2)) {
/* equivalent: return solveAccum(tyv1,var,tyvNum(tyv2)); */
if (isAccum(tyv1)) {
mkAccum(tyv2);
tyv2->bound = appendOnto(tyv1->bound,tyv2->bound);
tyv2->offs = tyv1->offs + tyv2->offs; /* ref-counts */
deAccum(tyv1,FALSE);
}
bindTyv(tyv1,var,tyvNum(tyv2));
checkVars();
}
else
return varToTypeAccum(tyv1,var,tyvNum(tyv2),negv(z));
}
else {
if (!isSkolem(tyv2))
return varToTypeAccum(tyv2,var,tyvNum(tyv1),z);
else {
// Insert subtyping extension here...
return failure("quantified variable prevents unification");
}
}
}
checkVars();
return TRUE;
}
static Bool local varToTypeAccum(tyv,t,o,z) /* Accumulate tyv < (t,o) */
Tyvar *tyv;
Type t; /* guaranteed not bo be a variable, or to */
Int o; /* have synonym as outermost constr */
Int z; { /* Can assume t==mkInt() => t skolemized */
Type h;
checkVars();
if (matchMode)
return failure("types do not match");
if (isCloned(tyv))
internal("clone in varToTypeAccum");
if (!eqKind(tyv->kind,getKind(t,o)))
return failure("kinds do not match");
if (isSkolem(tyv)) {
h = getDerefHead(t,o);
// Insert subtyping extension here...
return failure("quantified variable prevents unification");
}
else { /* var to type bind */
Int alpha = tyvNum(tyv);
Int beta = newTyvars(1); /* invalidates tyv */
tyv = tyvar(alpha);
bindTv(beta,t,o);
accumBound(tyv,beta,z);
return TRUE;
}
return FALSE; /* not reached */
}
#define lub(ts) bestBounds(ts,0,POSV)
#define glb(ts) bestBounds(ts,0,NEGV)
#define raiseArity(tc,a,z) bestBounds(singleton(tc),a,z)
static Bool local preUnify(t1,o1,t2,o2,z) /* break down constraint into a */
Type t1,t2; /* set of simple constraints on */
Int o1,o2; /* variables (result is stored */
Int z; { /* in 'accumVars') */
Tyvar *tyv1, *tyv2;
checkVars();
unifyFails = 0;
if (z==NONV)
return TRUE;
deRef(tyv1,t1,o1);
deRef(tyv2,t2,o2);
un: if (tyv1)
if (tyv2)
return varToVarBind(tyv1,tyv2,z); /* t1, t2 variables */
else {
Cell h2 = getDerefHead(t2,o2); /* t1 variable, t2 not */
if (isSynonym(h2) && argCount>=tycon(h2).arity) {
expandSyn(h2,argCount,&t2,&o2);
deRef(tyv2,t2,o2);
checkVars();
goto un;
}
return varToTypeAccum(tyv1,t2,o2,negv(z));
}
else
if (tyv2) {
Cell h1 = getDerefHead(t1,o1); /* t2 variable, t1 not */
if (isSynonym(h1) && argCount>=tycon(h1).arity) {
expandSyn(h1,argCount,&t1,&o1);
deRef(tyv1,t1,o1);
checkVars();
goto un;
}
return varToTypeAccum(tyv2,t1,o1,z);
}
else { /* t1, t2 not vars */
Type h1 = getDerefHead(t1,o1);
Int a1 = argCount;
Type h2 = getDerefHead(t2,o2);
Int a2 = argCount;
checkVars();
#ifdef DEBUG_TYPES
printf("tt unifying types: ");
printType(stdout,debugType(t1,o1));
printf(" with ");
printType(stdout,debugType(t2,o2));
putchar('\n');
#endif
if (isOffset(h1) || isInt(h1)) h1=NIL; /* represent var by NIL*/
if (isOffset(h2) || isInt(h2)) h2=NIL;
if (nonNull(h1) && h1==h2) {
Cell z1 = getVariance(h1,a1);
if (a1!=a2)
return failure("incompatible constructors");
while (isAp(t1)) {
if (!preUnify(arg(t1),o1,arg(t2),o2,multv(z,thisVariance(z1))))
return FALSE;
checkVars();
t1 = fun(t1);
deRef(tyv1,t1,o1);
t2 = fun(t2);
deRef(tyv2,t2,o2);
z1 = nextVariance(z1);
}
return TRUE;
}
/* Types do not match -- look for type synonyms to expand */
if (isSynonym(h1) && a1>=tycon(h1).arity) {
expandSyn(h1,a1,&t1,&o1);
deRef(tyv1,t1,o1);
checkVars();
goto un;
}
if (isSynonym(h2) && a2>=tycon(h2).arity) {
expandSyn(h2,a2,&t2,&o2);
deRef(tyv2,t2,o2);
checkVars();
goto un;
}
checkVars();
/* See if h1 and h2 are related by subtyping */
if (!matchMode && z != INV &&
isTycon(h1) && isTycon(h2) && tycon(h1).what==tycon(h2).what) {
static String ho_err = "higher order subtyping axiom cannot be derived";
Type ax=NIL,s1,s2,t;
Int o, n, hi, lo;
if ((tycon(h1).what==DATATYPE) == (z==POSV)) {
if (nonNull(ax = findAxiom(h2,h1))) {
instantiate(ax,&s1,&o,0);
s2 = satTycon(h2);
hi = tycon(h2).arity-1;
if (tcMode!=EXPRESSION)
skolemOffsetsAbove(tycon(h2).arity,s1,o);
}
}
else {
if (nonNull(ax = findAxiom(h1,h2))) {
instantiate(ax,&s2,&o,0);
s1 = satTycon(h1);
hi = tycon(h1).arity-1;
if (tcMode!=EXPRESSION)
skolemOffsetsAbove(tycon(h1).arity,s2,o);
}
}
if (isNull(ax) || (n=(tycon(h1).arity-a1)) != (tycon(h2).arity-a2))
return failure(0);
/* If n > 0, try to derive a higher-order subtyping axiom */
lo = hi-n;
for (; n>0; n--, s1=fun(s1), s2=fun(s2))
if (!isOffset(arg(s1)) || arg(s1) != arg(s2))
return failure(ho_err);
if (offsetsBetween(lo,hi,s1) || offsetsBetween(lo,hi,s2))
return failure(ho_err);
/* Check axiom against original types */
return preUnify(t1,o1,s1,o,z) &&
preUnify(s2,o,t2,o2,z);
}
if ((isNull(h1) && a1<=a2) || /* last attempt -- maybe */
(isNull(h2) && a2<=a1)) { /* one head is a variable? */
Cell z1 = nonNull(h1) ? getVariance(h1,a1)
: (nonNull(h2) ? getVariance(h2,a2)
: mkInt(INV));
for (;;) {
deRef(tyv1,t1,o1);
deRef(tyv2,t2,o2);
checkVars();
if (tyv1) /* unify heads! */
if (tyv2)
return varToVarBind(tyv1,tyv2,z);
else
return varToTypeAccum(tyv1,t2,o2,negv(z));
else if (tyv2)
return varToTypeAccum(tyv2,t1,o1,z);
/* at this point, neither t1 nor t2 is a variable. In */
/* addition, they must both be APs unless one of the */
/* head variables has been bound during unification of */
/* the arguments. */
checkVars();
if (!isAp(t1) || !isAp(t2)) /* might not be APs*/
return (t1==t2) ? TRUE : failure(0);
/*must be APs */
if (!preUnify(arg(t1),o1,arg(t2),o2,multv(z,thisVariance(z1))))
return FALSE;
t1 = fun(t1);
t2 = fun(t2);
z1 = nextVariance(z1);
}
}
if (matchMode || z==INV)
return failure(0);
/* One final attempt: handle arity mismatches. Check if a */
/* unique suptyping axiom can be determined on basis of the */
/* arity requirements. One typical example is the subtyping */
/* problem Action < m a, which can be solved by utilizing the */
/* axiom Action < Cmd () (in preference over Action < O s ()) */
/* Todo: handle higher kinds here? */
if (isTycon(h1) && isNull(h2) && a2>0) {
List tcs = raiseArity(h1,a2,z);
if (nonNull(tcs) && isNull(tl(tcs))) {
Type t;
Int o;
instantiate(findAxiom(h1,hd(tcs)),&t,&o,0);
return preUnify(t1,o1,t,o,z) && preUnify(t,o,t2,o2,z);
}
}
if (isTycon(h2) && isNull(h1) && a1>0) {
List tcs = raiseArity(h2,a1,negv(z));
if (nonNull(tcs) && isNull(tl(tcs))) {
Type t;
Int o;
instantiate(findAxiom(h2,hd(tcs)),&t,&o,0);
return preUnify(t1,o1,t,o,z) && preUnify(t,o,t2,o2,z);
}
}
}
return failure(0);
}
static Int local varianceInGoal(tyv) /* variance of tyv in current goal */
Tyvar *tyv; {
Tyvar saved = *tyv;
Int z;
List gs;
resetState(tyv);
if (isNull(goalStack))
internal("varianceInGoal");
for (gs=hd(goalStack); nonNull(gs); gs=tl(gs))
markVarianceTyvar(intOf(hd(gs)),POSV);
z = tyv->offs;
*tyv = saved;
return z;
}
static Bool local allSubtypes(ts,t,z)
List ts;
Type t;
Int z; {
for (; nonNull(ts); ts=tl(ts))
if (!isSubtype(hd(ts),t,z))
break;
return isNull(ts);
}
static List local bestBounds(ts,a,z)
List ts;
Int a;
Int z; {
List ts1;
if (isNull(ts))
return ts;
if (isNull(tl(ts)) && a == 0) /* trivial case */
return ts;
for (ts1=ts; nonNull(ts1); ts1=tl(ts1)) { /* case ts contains the bound */
Type h = hd(ts1);
if (isTuple(h))
return NIL;
if (isInt(h))
break;
if (allSubtypes(ts,h,z) && tycon(h).arity >= a) {
tl(ts1) = NIL;
return ts1;
}
}
if (nonNull(ts1)) { /* case ts contains a skolem var*/
if (ts1==ts && isNull(tl(ts)) && a <= length(tyvar(intOf(hd(ts)))->kind))
return ts;
return NIL; /* todo: search its bounds */
}
else { /* full search is needed */
Int w = tycon(hd(ts)).what;
List bds = NIL;
Tycon tc;
if ((w==DATATYPE) == (z==POSV)) {
Tycon tc2 = lastTycon();
for (tc=TYCMIN; tc<=tc2; tc++)
if (tycon(tc).what == w && tycon(tc).arity >= a) {
for (ts1=ts; nonNull(ts1); ts1=tl(ts1))
if (!findAxiom(tc,hd(ts1)))
break;
if (isNull(ts1))
bds = cons(tc,bds);
}
}
else {
for (ts1=tycon(hd(ts)).axioms; nonNull(ts1); ts1=tl(ts1)) {
tc = getHead(monoType(hd(ts1)));
if (allSubtypes(ts,tc,z) && tycon(tc).arity >= a)
bds = cons(tc,bds);
}
}
for (ts1=bds; nonNull(ts1); ts1=tl(ts1))
if (allSubtypes(bds,hd(ts1),negv(z))) {
tl(ts1) = NIL;
return ts1;
}
return bds;
}
}
static List local matchingArities(ts,loArity,hiArity)
List ts;
Int loArity;
Int hiArity; {
List matching = NIL;
for (; nonNull(ts); ts=tl(ts)) {
Type t = hd(ts);
if (isInt(t)) { /* must be a skolemvar */
Int arity = length(tyvar(intOf(t))->kind);
if (loArity <= arity && hiArity <= arity)
matching = cons(t,matching);
else {
/* Todo: search its bounds */
}
} else if (isTuple(t)) {
Int arity = tupleOf(t);
if (loArity <= arity && hiArity <= arity)
matching = cons(t, matching);
} else {
Int w = tycon(t).what;
Int quickArity = (w==DATATYPE) ? loArity : hiArity;
Int slowArity = (w==DATATYPE) ? hiArity : loArity;
Bool mismatch = FALSE;
if (quickArity > tycon(t).arity) {
List ts1 = tycon(t).axioms;
for (; nonNull(ts1); ts1=tl(ts1))
if (quickArity <= tycon(getHead(monoType(hd(ts1)))).arity)
break;
if (isNull(ts1))
mismatch = TRUE;
}
if (!mismatch && slowArity > tycon(t).arity) {
Tycon tc = TYCMIN, tc2 = lastTycon();
for (; tc <= tc2; tc++)
if (tycon(tc).what==w && slowArity <= tycon(tc).arity && findAxiom(tc,t))
break;
if (tc > tc2)
mismatch = TRUE;
}
if (!mismatch)
matching = cons(t,matching);
}
}
return matching;
}
static Bool local isSubtype(t1,t2,z)
Type t1;
Type t2;
Int z; {
if (t1==t2)
return TRUE;
switch (whatIs(t1)) {
case TUPLE : return FALSE;
case INTCELL : /* insert skolem constraint check here */ return FALSE;
case TYCON : if (isInt(t2)) {
/* insert skolem constraint check here */ return FALSE;
}
else if ((tycon(t1).what==DATATYPE) == (z==POSV))
return nonNull(findAxiom(t2,t1));
else
return nonNull(findAxiom(t1,t2));
}
internal("isSubtype");
}
static Bool local mergeBounds(tyv,t,o) /* Result is (*t,*o) */
Tyvar *tyv;
Type *t;
Int *o; {
List bs, lo=NIL, hi=NIL;
Int loArity = 0, hiArity = 0;
List bds;
Int n,i;
Kind k0 = tyv->kind;
Kind k, loKind = STAR, hiKind = STAR;
if (!isAccum(tyv))
internal("mergeBounds");
for (bs=tyv->bound; nonNull(bs); bs=tl(bs)) {
Type b = fst(hd(bs));
Int z = intOf(snd(hd(bs)));
Type h = getDerefHead(b,0);
if (isInt(h) && !isSkolem(tyvar(intOf(h)))) {
if ((z & POSV) && argCount > loArity) {
loArity = argCount;
loKind = tyvar(intOf(h))->kind;
}
if ((z & NEGV) && argCount > hiArity) {
hiArity = argCount;
hiKind = tyvar(intOf(h))->kind;
}
continue;
}
if ((z & POSV) && !cellIsMember(h,lo))
lo = cons(h,lo);
if ((z & NEGV) && !cellIsMember(h,hi))
hi = cons(h,hi);
}
if (isNull(lo) && isNull(hi)) {
Int alpha = newTyvars(1);
tyvar(alpha)->kind = hiArity > loArity ? hiKind : loKind;
bds = singleton(mkInt(alpha));
} else if (isNull(lo))
bds = glb(hi);
else if (isNull(hi))
bds = lub(lo);
else {
hi = glb(hi);
lo = lub(lo);
bds = NIL;
if (nonNull(lo) && nonNull(hi)) {
if (varianceInGoal(tyv) == NEGV) {
for (; nonNull(hi); hi=tl(hi))
if (allSubtypes(lo,hd(hi),POSV))
bds = cons(hd(hi),bds);
if (length(bds) > 1 && length(lo) == 1)
bds = lo;
}
else {
for (; nonNull(lo); lo=tl(lo))
if (allSubtypes(hi,hd(lo),NEGV))
bds = cons(hd(lo),bds);
if (length(bds) > 1 && length(hi) == 1)
bds = hi;
}
}
}
bds = matchingArities(bds,loArity,hiArity);
if (isNull(bds))
return failure("variable has conflicting bounds");
else if (nonNull(tl(bds)))
return failure("variable has ambiguous bounds");
*t = hd(bds);
switch (whatIs(*t)) {
case TYCON : k = tycon(*t).kind;
break;
case TUPLE : k = simpleKind(tupleOf(*t));
break;
case INTCELL : k = tyvar(intOf(*t))->kind;
break;
default : internal("mergeBounds");
}
*o = newTyvars(0);
for (n=0; isPair(k); k=snd(k),n++) {
if (eqKind(k,k0))
break;
tyvar(newTyvars(1))->kind = fst(k);
}
if (k==STAR && k0!=STAR)
return failure("kind error in higher-order bound");
for (i=0; i<n; ++i)
*t = ap(*t,mkOffset(i));
return TRUE;
}
static Bool local postUnify() { /* solve accumulated constraints */
while (nonNull(accumVars)) {
Tyvar *tyv;
List vs,bs;
Type t;
Int o;
checkVars();
for (vs=accumVars; nonNull(vs); vs=tl(vs)) {/* find unreferenced var */
if (tyvar(intOf(hd(vs)))->offs == 0)
break;
}
lastTyvar = intOf(hd(nonNull(vs) ? vs : accumVars));
tyv = tyvar(lastTyvar);
if (!isAccum(tyv))
internal("postUnify");
bs = lastBounds = tyv->bound;
/* If vs==NIL we have a pending infinite type error, but we */
/* continue until we have a directly recursive constraint */
/* for the sake of a more readable error message. */
if (vs==NIL) {
for (; nonNull(bs); bs=tl(bs))
if (occurs(tyv,var,intOf(fst(hd(bs)))))
return failure("constraints are recursive");
bs = lastBounds;
}
if (isNull(bs)) { /* short-circuit empty or single bounds */
if (nonNull(vs))
deAccum(tyv,TRUE);
else
accumVars = tl(accumVars);
continue;
} else if (isNull(tl(bs))) {
countDown(intOf(fst(hd(bs))));
tyv->bound = NIL;
if (!solveAccum(tyv,var,intOf(fst(hd(bs)))))
return FALSE;
continue;
}
if (!mergeBounds(tyv,&t,&o)) /* general case, result is (t,o) */
return FALSE;
if (!solveAccum(tyvar(lastTyvar),t,o))
return FALSE;
checkVars();
}
return TRUE;
}
static Bool local unify(t1,o1,t2,o2) /* Main unification routine */
Type t1,t2; /* unify (t1,o1) with (t2,o2) */
Int o1,o2; {
lastTyvar = 0;
lastBounds = NIL;
if (!preUnify(t1,o1,t2,o2,POSV))
return FALSE;
return postUnify();
}
static Bool local sameType(t1,o1,t2,o2) /* Compare types without binding */
Type t1,t2;
Int o1,o2; {
Bool result;
matchMode = TRUE;
result = unify(t1,o1,t2,o2);
matchMode = FALSE;
return result;
}
/* --------------------------------------------------------------------------
* Unify kind expressions:
* ------------------------------------------------------------------------*/
static Bool local kvarToVarBind(tyv1,tyv2)/* Make binding tyv1 := tyv2 */
Tyvar *tyv1, *tyv2; { /* for kind variable bindings */
if (tyv1!=tyv2) {
tyv1->bound = var;
tyv1->offs = tyvNum(tyv2);
}
return TRUE;
}
static Bool local kvarToTypeBind(tyv,t,o)/* Make binding tyv := (t,o) */
Tyvar *tyv; /* for kind variable bindings */
Type t; /* guaranteed not to be a v'ble or */
Int o; { /* have synonym as outermost constr*/
if (occurs(tyv,t,o))
return failure("unification would give infinite kind");
tyv->bound = t;
tyv->offs = o;
return TRUE;
}
static Bool local kunify(k1,o1,k2,o2) /* Unify kind expr (k1,o1) with */
Kind k1,k2; /* (k2,o2) */
Int o1,o2; {
Tyvar *kyv1, *kyv2;
deRef(kyv1,k1,o1);
deRef(kyv2,k2,o2);
if (kyv1)
if (kyv2)
return kvarToVarBind(kyv1,kyv2); /* k1, k2 variables */
else
return kvarToTypeBind(kyv1,k2,o2); /* k1 variable, k2 not */
else
if (kyv2)
return kvarToTypeBind(kyv2,k1,o1); /* k2 variable, k1 not */
else
if (k1==STAR && k2==STAR) /* k1, k2 not vars */
return TRUE;
else if (isAp(k1) && isAp(k2))
return kunify(fst(k1),o1,fst(k2),o2) &&
kunify(snd(k1),o1,snd(k2),o2);
return failure(0);
}
/*-------------------------------------------------------------------------*/
static Void local checkVars() {
#if 0
List vs, bs;
Tyvar *tyv, *tyv1, *tyv2;
Int lenBs, beta, beta1, p, z, len = length(accumVars);
for (vs=accumVars; nonNull(vs); vs=tl(vs)) {
beta = intOf(hd(vs));
tyv = tyvar(beta);
if (cellIsMember(hd(vs),tl(vs)))
internal("duplicates in accumVars");
if (!isAccum(tyv))
internal("no accum");
lenBs = length(tyv->bound);
if (tyv->offs < 0)
internal("negative refcount");
for (bs=tyv->bound; nonNull(bs); bs=tl(bs)) {
p = hd(bs);
z = intOf(snd(p));
beta1 = intOf(fst(p));
tyv1 = tyvar(beta1);
if (isAccum(tyv1))
internal("bound has accum");
if ((tyv2=getTypeVar(tyv1->bound,tyv1->offs)) && !isSkolem(tyv2))
internal("var at head");
countDown(beta1);
}
}
for (vs=accumVars; nonNull(vs); vs=tl(vs)) {
beta = intOf(hd(vs));
tyv = tyvar(beta);
if (tyv->offs != 0)
internal("refCount mismatch");
}
for (vs=accumVars; nonNull(vs); vs=tl(vs)) {
beta = intOf(hd(vs));
tyv = tyvar(beta);
for (bs=tyv->bound; nonNull(bs); bs=tl(bs)) {
p = hd(bs);
z = intOf(snd(p));
beta1 = intOf(fst(p));
tyv1 = tyvar(beta1);
countUp(beta1);
}
}
for (vs=skolVars; nonNull(vs); vs=tl(vs)) {
List vs1;
for (vs1=hd(vs); nonNull(vs1); vs1=tl(vs1)) {
beta = intOf(hd(vs1));
tyv = tyvar(beta);
if (!isSkolem(tyv))
internal("no skolem");
}
}
for (vs=skolVars2; nonNull(vs); vs=tl(vs)) {
List vs1;
for (vs1=hd(vs); nonNull(vs1); vs1=tl(vs1)) {
beta = intOf(hd(vs1));
tyv = tyvar(beta);
if (!isSkolem(tyv))
internal("no skolem");
}
}
#endif
}
syntax highlighted by Code2HTML, v. 0.9.1