/* -------------------------------------------------------------------------- * This is the Hugs type checker * * The Hugs 98 system is Copyright (c) Mark P Jones, Alastair Reid, the * Yale Haskell Group, and the OGI School of Science & Engineering at OHSU, * 1994-2003, All rights reserved. It is distributed as free software under * the license in the file "License", which is included in the distribution. * * $RCSfile: type.c,v $ * $Revision: 1.81 $ * $Date: 2005/12/10 11:25:13 $ * ------------------------------------------------------------------------*/ #include "prelude.h"#include "storage.h"#include "connect.h"#include "errors.h"#include "output.h"#include "subst.h"#include "goal.h"#include "opts.h" /* needed for EXPLAIN_INSTANCE_RESOLUTION|MULTI_INST */ Bool catchAmbigs = FALSE; /* TRUE => functions with ambig. */ /* types produce error */ Type typeArrow, typeList; /* Important primitive types */Type typeUnit; Module modulePrelude;Module moduleUserPrelude; Type typeInt; Type typeInt8; Type typeInt16; Type typeInt32; Type typeInt64; Type typeWord;Type typeWord8;Type typeWord16;Type typeWord32;Type typeWord64;Type typeFunPtr;Type typePtr;Type typeAddr;Type typeFloat;Type typeDouble;Type typeChar;Type typeForeignP;Type typeForeign;Type typeStable;Type typeBool;Type typeString;#ifdef DOTNETType typeObject;#endif static Type typeInteger; static Type typeMaybe;static Type typeOrdering; Class classEq, classOrd; /* `standard' classes */Class classIx, classEnum;Class classShow, classRead;Class classBounded; Class classReal, classIntegral; /* `numeric' classes */Class classRealFrac, classRealFloat;Class classFractional, classFloating;Class classNum; List stdDefaults; /* standard default values */ Name nameFromInt, nameFromDouble; /* coercion of numerics */Name nameFromInteger;Name nameEq, nameCompare; /* derivable names */Name nameLe;Name nameShowsPrec;Name nameReadsPrec;Name nameMinBnd, nameMaxBnd;Name nameIndex, nameInRange;Name nameRange;Name nameMult, namePlus;Name nameTrue, nameFalse; /* primitive boolean constructors */Name nameNil, nameCons; /* primitive list constructors */Name nameJust, nameNothing; /* primitive Maybe constructors */Name nameLeft, nameRight; /* primitive Either constructors */Name nameUnit; /* primitive Unit type constructor */Name nameLT, nameEQ; /* Ordering constructors */Name nameGT;Class classMonad; /* Monads */Name nameReturn, nameBind, nameThen; /* for translating do/monad comps */Name nameMFail;Name nameGt; /* for readsPrec */ #if MUDOClass classMonadRec; /* Recursive monads */Name nameMFix;#endif #if IO_MONADType typeIO; /* For the IO monad, IO */Type typeProgIO; /* For the IO monad, IO a */ Name nameIOError, nameUserErr; /* loosely coupled IOError cfuns */Name namePermDenied;Name nameAlreadyExists, nameAlreadyInUse, nameDoesNotExist, nameIsFull;Name nameIllegal;#endif#if IO_HANDLESName nameEOFErr;Name nameProtocolError;#endifName nameArithException;Name nameArrayException;Name nameErrorCall;Name nameIOException;Name nameNoMethodError;Name nameNonTermination;Name namePatternMatchFail;Name nameRecConError;Name nameRecSelError;Name nameRecUpdError; Name nameOverflow;Name nameDivideByZero;Name nameIndexOutOfBounds;Name nameUndefinedElement; #if TREXType typeNoRow; /* Empty row */Type typeRec; /* Record formation */Name nameNoRec; /* Empty record */#endif #if DOTNETName nameNetException;#endif /* -------------------------------------------------------------------------- * Local function prototypes: * ------------------------------------------------------------------------*/ static Void local emptyAssumption Args((Void));static Void local enterBindings Args((Void));static Void local leaveBindings Args((Void));static Int local defType Args((Cell));static Type local useType Args((Cell));static Void local markAssumList Args((List));static Cell local findAssum Args((Text));static Pair local findInAssumList Args((Text,List));static List local intsIntersect Args((List,List));static List local genvarAllAss Args((List));static List local genvarAnyAss Args((List));static Int local newVarsBind Args((Cell));static Void local newDefnBind Args((Cell,Type)); static Void local enterPendingBtyvs Args((Void));static Void local leavePendingBtyvs Args((Void));static Cell local patBtyvs Args((Cell));static Void local doneBtyvs Args((Int));static Void local enterSkolVars Args((Void));static Void local leaveSkolVars Args((Int,Type,Int,Int)); static Void local typeError Args((Int,Cell,Cell,String,Type,Int));static Void local reportTypeError Args((Int,Cell,Cell,String,Type,Type));static Void local cantEstablish Args((Int,String,Cell,Type,List));static Void local tooGeneral Args((Int,Cell,Type,Type)); static Cell local typeExpr Args((Int,Cell)); static Cell local typeAp Args((Int,Cell));static Type local typeExpected Args((Int,String,Cell,Type,Int,Int,Bool));static Void local typeAlt Args((String,Cell,Cell,Type,Int,Int));static Int local funcType Args((Int));static Void local typeCase Args((Int,Int,Cell));static Void local typeComp Args((Int,Type,Cell,List));static Cell local typeMonadComp Args((Int,Cell));#if ZIP_COMPstatic Cell local typeZComp Args((Int,Type,Cell,List));static Void local typeCompy Args((Int,Type,List));static Cell local typeMonadZComp Args((Int,Cell));static List local getPats Args((List));static Cell local tupleUp Args((List));#endifstatic Void local typeDo Args((Int,Cell));#if MUDOstatic Void local typeRecComp Args((Int,Type,Cell,List));static Void local typeMDo Args((Int,Cell));static Void local typeRecursiveDo Args((Int,Cell));#endifstatic Void local typeConFlds Args((Int,Cell));static Void local typeUpdFlds Args((Int,Cell));#if IPARAMstatic Cell local typeWith Args((Int,Cell));#endifstatic Cell local typeFreshPat Args((Int,Cell)); static Void local typeBindings Args((List));static Void local removeTypeSigs Args((Cell)); static Void local monorestrict Args((List));static Void local restrictedBindAss Args((Cell));static Void local restrictedAss Args((Int,Cell,Type)); static Void local unrestricted Args((List));static List local itbscc Args((List));static Void local addEvidParams Args((List,Cell)); static Void local typeClassDefn Args((Class));static Void local typeInstDefn Args((Inst));static Void local typeMember Args((String,Name,Cell,List,Cell,Int)); static Void local typeBind Args((Cell));static Void local typeDefAlt Args((Int,Cell,Pair));static Cell local typeRhs Args((Cell));static Void local guardedType Args((Int,Cell)); static Void local genBind Args((List,Cell));static Void local genAss Args((Int,List,Cell,Type));static Type local genTest Args((Int,Cell,List,Type,Type,Int));static Type local generalize Args((List,Type));static Bool local equalTypes Args((Type,Type)); static Void local typeDefnGroup Args((List));static Void local typeForeignExport Args((Name));static Pair local typeSel Args((Name)); static Name local linkName Args((String));static Tycon local linkTycon Args((String));static Class local linkClass Args((String)); /* -------------------------------------------------------------------------- * Frequently used type skeletons: * ------------------------------------------------------------------------*/ static Type arrow; /* mkOffset(0) -> mkOffset(1) */static Type boundPair; /* (mkOffset(0),mkOffset(0)) */static Type listof; /* [ mkOffset(0) ] */static Type typeVarToVar; /* mkOffset(0) -> mkOffset(0) */ static Cell predNum; /* Num (mkOffset(0)) */static Cell predFractional; /* Fractional (mkOffset(0)) */static Cell predIntegral; /* Integral (mkOffset(0)) */static Kind starToStar; /* Type -> Type */static Cell predMonad; /* Monad (mkOffset(0)) */#if MUDOstatic Cell predMonadRec; /* MonadRec/MonadFix (mkOffset(0)) */#endif /* -------------------------------------------------------------------------- * Assumptions: * * A basic typing statement is a pair (Var,Type) and an assumption contains * an ordered list of basic typing statements in which the type for a given * variable is given by the most recently added assumption about that var. * * In practice, the assumption set is split between a pair of lists, one * holding assumptions for vars defined in bindings, the other for vars * defined in patterns/binding parameters etc. The reason for this * separation is that vars defined in bindings may be overloaded (with the * overloading being unknown until the whole binding is typed), whereas the * vars defined in patterns have no overloading. A form of dependency * analysis (at least as far as calculating dependents within the same group * of value bindings) is required to implement this. Where it is known that * no overloaded values are defined in a binding (i.e., when the `dreaded * monomorphism restriction' strikes), the list used to record dependents * is flagged with a NODEPENDS tag to avoid gathering dependents at that * level. * * To interleave between vars for bindings and vars for patterns, we use * a list of lists of typing statements for each. These lists are always * the same length. The implementation here is very similar to that of the * dependency analysis used in the static analysis component of this system. * * To deal with polymorphic recursion, variables defined in bindings can be * assigned types of the form (POLYREC,(def,use)), where def is a type * variable for the type of the defining occurence, and use is a type * scheme for (recursive) calls/uses of the variable. * ------------------------------------------------------------------------*/ static List defnBounds; /*::[[(Var,Type)]] possibly ovrlded*/static List varsBounds; /*::[[(Var,Type)]] not overloaded */static List depends; /*::[?[Var]] dependents/NODEPENDS */static List skolVars; /*::[[Var]] skolem vars */static List localEvs; /*::[[(Pred,offset,ev)]] */static List savedPs; /*::[[(Pred,offset,ev)]] */static Cell dummyVar; /* Used to put extra tvars into ass*/ #define saveVarsAss() List saveAssump = hd(varsBounds)#define restoreVarsAss() hd(varsBounds) = saveAssump#define addVarAssump(v,t) hd(varsBounds) = cons(pair(v,t),hd(varsBounds))#define findTopBinding(v) findInAssumList(textOf(v),hd(defnBounds)) static Void local emptyAssumption() { /* set empty type assumption */ defnBounds = NIL; varsBounds = NIL; depends = NIL; skolVars = NIL; localEvs = NIL; savedPs = NIL;} static Void local enterBindings() { /* Add new level to assumption sets */ defnBounds = cons(NIL,defnBounds); varsBounds = cons(NIL,varsBounds); depends = cons(NIL,depends);} static Void local leaveBindings() { /* Drop one level of assumptions */ defnBounds = tl(defnBounds); varsBounds = tl(varsBounds); depends = tl(depends);} static Int local defType(a) /* Return type for defining occ. */Cell a; { /* of a var from assumption pair */ return (isPair(a) && fst(a)==POLYREC) ? fst(snd(a)) : a;} static Type local useType(a) /* Return type for use of a var */Cell a; { /* defined in an assumption */ return (isPair(a) && fst(a)==POLYREC) ? snd(snd(a)) : a;} static Void local markAssumList(as) /* Mark all types in assumption set*/List as; { /* :: [(Var, Type)] */ for (; nonNull(as); as=tl(as)) { /* No need to mark generic types; */ Type t = defType(snd(hd(as))); /* the only free variables in those*/ if (!isPolyType(t)) /* must have been free earlier too */ markType(t,0); }} static Cell local findAssum(t) /* Find most recent assumption about*/Text t; { /* variable named t, if any */ List defnBounds1 = defnBounds; /* return translated variable, with */ List varsBounds1 = varsBounds; /* type in typeIs */ List depends1 = depends; while (nonNull(defnBounds1)) { Pair ass = findInAssumList(t,hd(varsBounds1));/* search varsBounds */ if (nonNull(ass)) { typeIs = snd(ass); return fst(ass); } ass = findInAssumList(t,hd(defnBounds1)); /* search defnBounds */ if (nonNull(ass)) { Cell v = fst(ass); typeIs = snd(ass); if (hd(depends1)!=NODEPENDS && /* save dependent? */ isNull(v=varIsMember(t,hd(depends1)))) /* N.B. make new copy of variable and store this on list of*/ /* dependents, and in the assumption so that all uses of */ /* the variable will be at the same node, if we need to */ /* overwrite the call of a function with a translation... */ hd(depends1) = cons(v=mkVar(t),hd(depends1)); return v; } defnBounds1 = tl(defnBounds1); /* look in next level*/ varsBounds1 = tl(varsBounds1); /* of assumption set */ depends1 = tl(depends1); } return NIL;} static Pair local findInAssumList(t,as)/* Search for assumption for var */Text t; /* named t in list of assumptions as*/List as; { for (; nonNull(as); as=tl(as)) if (textOf(fst(hd(as)))==t) return hd(as); return NIL;} static List local intsIntersect(as,bs) /* calculate intersection of lists */List as, bs; { /* of integers (as sets) */ List ts = NIL; /* destructively modifies as */ while (nonNull(as)) if (intIsMember(intOf(hd(as)),bs)) { List temp = tl(as); tl(as) = ts; ts = as; as = temp; } else as = tl(as); return ts;} static List local genvarAllAss(as) /* calculate generic vars that are */List as; { /* in every type in assumptions as */ List vs = genvarTyvar(intOf(defType(snd(hd(as)))),NIL); for (as=tl(as); nonNull(as) && nonNull(vs); as=tl(as)) vs = intsIntersect(vs,genvarTyvar(intOf(defType(snd(hd(as)))),NIL)); return vs;} static List local genvarAnyAss(as) /* calculate generic vars that are */List as; { /* in any type in assumptions as */ List vs = genvarTyvar(intOf(defType(snd(hd(as)))),NIL); for (as=tl(as); nonNull(as); as=tl(as)) vs = genvarTyvar(intOf(defType(snd(hd(as)))),vs); return vs;} static Int local newVarsBind(v) /* make new assump for pattern var */Cell v; { Int beta = newTyvars(1); addVarAssump(v,mkInt(beta));#if DEBUG_TYPES Printf("variable, assume "); printExp(stdout,v); Printf(" :: _%d\n",beta);#endif return beta;} static Void local newDefnBind(v,type) /* make new assump for defn var */Cell v; /* and set type if given (nonNull) */Type type; { Int beta = newTyvars(1); Cell ta = mkInt(beta); instantiate(type); if (nonNull(type) && isPolyType(type)) ta = pair(POLYREC,pair(ta,type)); hd(defnBounds) = cons(pair(v,ta), hd(defnBounds));#if DEBUG_TYPES Printf("definition, assume "); printExp(stdout,v); Printf(" :: _%d\n",beta);#endif bindTv(beta,typeIs,typeOff); /* Bind beta to new type skeleton */} /* -------------------------------------------------------------------------- * Predicates: * ------------------------------------------------------------------------*/ #include "preds.c" /* -------------------------------------------------------------------------- * Bound and skolemized type variables: * ------------------------------------------------------------------------*/ static List pendingBtyvs = NIL; static Void local enterPendingBtyvs() { enterBtyvs(); pendingBtyvs = cons(NIL,pendingBtyvs);} static Void local leavePendingBtyvsQuietly() { pendingBtyvs = tl(pendingBtyvs); leaveBtyvs();} static Void local leavePendingBtyvs() { List pts = hd(pendingBtyvs); pendingBtyvs = tl(pendingBtyvs); for (; nonNull(pts); pts=tl(pts)) { Int line = intOf(fst(hd(pts))); List vs = snd(hd(pts)); Int i = 0; clearMarks(); for (; nonNull(vs); vs=tl(vs)) { Cell v = fst(hd(vs)); Cell t = copyTyvar(intOf(snd(hd(vs)))); if (!isOffset(t)) { ERRMSG(line) "Type annotation uses variable " ETHEN ERREXPR(v); ERRTEXT " where a more specific type " ETHEN ERRTYPE(t); ERRTEXT " was inferred" EEND; } else if (offsetOf(t)!=i) { List us = snd(hd(pts)); Int j = offsetOf(t); if (j>=i) internal("leavePendingBtyvs"); for (; j>0; j--) us = tl(us); ERRMSG(line) "Type annotation uses distinct variables " ETHEN ERREXPR(v); ERRTEXT " and " ETHEN ERREXPR(fst(hd(us))); ERRTEXT " where a single variable was inferred" EEND; } else i++; } } leaveBtyvs();} static Cell local patBtyvs(p) /* Strip bound type vars from pat */Cell p; { if (whatIs(p)==BIGLAM) {Lines 1–500 of 3355. Load more
/* -------------------------------------------------------------------------- * This is the Hugs type checker * * The Hugs 98 system is Copyright (c) Mark P Jones, Alastair Reid, the * Yale Haskell Group, and the OGI School of Science & Engineering at OHSU, * 1994-2003, All rights reserved. It is distributed as free software under * the license in the file "License", which is included in the distribution. * * $RCSfile: type.c,v $ * $Revision: 1.81 $ * $Date: 2005/12/10 11:25:13 $ * ------------------------------------------------------------------------*/ #include "prelude.h" #include "storage.h" #include "connect.h" #include "errors.h" #include "output.h" #include "subst.h" #include "goal.h" #include "opts.h" /* needed for EXPLAIN_INSTANCE_RESOLUTION|MULTI_INST */ Bool catchAmbigs = FALSE; /* TRUE => functions with ambig. */ /* types produce error */ Type typeArrow, typeList; /* Important primitive types */ Type typeUnit; Module modulePrelude; Module moduleUserPrelude; Type typeInt; Type typeInt8; Type typeInt16; Type typeInt32; Type typeInt64; Type typeWord; Type typeWord8; Type typeWord16; Type typeWord32; Type typeWord64; Type typeFunPtr; Type typePtr; Type typeAddr; Type typeFloat; Type typeDouble; Type typeChar; Type typeForeignP; Type typeForeign; Type typeStable; Type typeBool; Type typeString; #ifdef DOTNET Type typeObject; #endif static Type typeInteger; static Type typeMaybe; static Type typeOrdering; Class classEq, classOrd; /* `standard' classes */ Class classIx, classEnum; Class classShow, classRead; Class classBounded; Class classReal, classIntegral; /* `numeric' classes */ Class classRealFrac, classRealFloat; Class classFractional, classFloating; Class classNum; List stdDefaults; /* standard default values */ Name nameFromInt, nameFromDouble; /* coercion of numerics */ Name nameFromInteger; Name nameEq, nameCompare; /* derivable names */ Name nameLe; Name nameShowsPrec; Name nameReadsPrec; Name nameMinBnd, nameMaxBnd; Name nameIndex, nameInRange; Name nameRange; Name nameMult, namePlus; Name nameTrue, nameFalse; /* primitive boolean constructors */ Name nameNil, nameCons; /* primitive list constructors */ Name nameJust, nameNothing; /* primitive Maybe constructors */ Name nameLeft, nameRight; /* primitive Either constructors */ Name nameUnit; /* primitive Unit type constructor */ Name nameLT, nameEQ; /* Ordering constructors */ Name nameGT; Class classMonad; /* Monads */ Name nameReturn, nameBind, nameThen; /* for translating do/monad comps */ Name nameMFail; Name nameGt; /* for readsPrec */ #if MUDO Class classMonadRec; /* Recursive monads */ Name nameMFix; #endif #if IO_MONAD Type typeIO; /* For the IO monad, IO */ Type typeProgIO; /* For the IO monad, IO a */ Name nameIOError, nameUserErr; /* loosely coupled IOError cfuns */ Name namePermDenied; Name nameAlreadyExists, nameAlreadyInUse, nameDoesNotExist, nameIsFull; Name nameIllegal; #endif #if IO_HANDLES Name nameEOFErr; Name nameProtocolError; #endif Name nameArithException; Name nameArrayException; Name nameErrorCall; Name nameIOException; Name nameNoMethodError; Name nameNonTermination; Name namePatternMatchFail; Name nameRecConError; Name nameRecSelError; Name nameRecUpdError; Name nameOverflow; Name nameDivideByZero; Name nameIndexOutOfBounds; Name nameUndefinedElement; #if TREX Type typeNoRow; /* Empty row */ Type typeRec; /* Record formation */ Name nameNoRec; /* Empty record */ #endif #if DOTNET Name nameNetException; #endif /* -------------------------------------------------------------------------- * Local function prototypes: * ------------------------------------------------------------------------*/ static Void local emptyAssumption Args((Void)); static Void local enterBindings Args((Void)); static Void local leaveBindings Args((Void)); static Int local defType Args((Cell)); static Type local useType Args((Cell)); static Void local markAssumList Args((List)); static Cell local findAssum Args((Text)); static Pair local findInAssumList Args((Text,List)); static List local intsIntersect Args((List,List)); static List local genvarAllAss Args((List)); static List local genvarAnyAss Args((List)); static Int local newVarsBind Args((Cell)); static Void local newDefnBind Args((Cell,Type)); static Void local enterPendingBtyvs Args((Void)); static Void local leavePendingBtyvs Args((Void)); static Cell local patBtyvs Args((Cell)); static Void local doneBtyvs Args((Int)); static Void local enterSkolVars Args((Void)); static Void local leaveSkolVars Args((Int,Type,Int,Int)); static Void local typeError Args((Int,Cell,Cell,String,Type,Int)); static Void local reportTypeError Args((Int,Cell,Cell,String,Type,Type)); static Void local cantEstablish Args((Int,String,Cell,Type,List)); static Void local tooGeneral Args((Int,Cell,Type,Type)); static Cell local typeExpr Args((Int,Cell)); static Cell local typeAp Args((Int,Cell)); static Type local typeExpected Args((Int,String,Cell,Type,Int,Int,Bool)); static Void local typeAlt Args((String,Cell,Cell,Type,Int,Int)); static Int local funcType Args((Int)); static Void local typeCase Args((Int,Int,Cell)); static Void local typeComp Args((Int,Type,Cell,List)); static Cell local typeMonadComp Args((Int,Cell)); #if ZIP_COMP static Cell local typeZComp Args((Int,Type,Cell,List)); static Void local typeCompy Args((Int,Type,List)); static Cell local typeMonadZComp Args((Int,Cell)); static List local getPats Args((List)); static Cell local tupleUp Args((List)); #endif static Void local typeDo Args((Int,Cell)); #if MUDO static Void local typeRecComp Args((Int,Type,Cell,List)); static Void local typeMDo Args((Int,Cell)); static Void local typeRecursiveDo Args((Int,Cell)); #endif static Void local typeConFlds Args((Int,Cell)); static Void local typeUpdFlds Args((Int,Cell)); #if IPARAM static Cell local typeWith Args((Int,Cell)); #endif static Cell local typeFreshPat Args((Int,Cell)); static Void local typeBindings Args((List)); static Void local removeTypeSigs Args((Cell)); static Void local monorestrict Args((List)); static Void local restrictedBindAss Args((Cell)); static Void local restrictedAss Args((Int,Cell,Type)); static Void local unrestricted Args((List)); static List local itbscc Args((List)); static Void local addEvidParams Args((List,Cell)); static Void local typeClassDefn Args((Class)); static Void local typeInstDefn Args((Inst)); static Void local typeMember Args((String,Name,Cell,List,Cell,Int)); static Void local typeBind Args((Cell)); static Void local typeDefAlt Args((Int,Cell,Pair)); static Cell local typeRhs Args((Cell)); static Void local guardedType Args((Int,Cell)); static Void local genBind Args((List,Cell)); static Void local genAss Args((Int,List,Cell,Type)); static Type local genTest Args((Int,Cell,List,Type,Type,Int)); static Type local generalize Args((List,Type)); static Bool local equalTypes Args((Type,Type)); static Void local typeDefnGroup Args((List)); static Void local typeForeignExport Args((Name)); static Pair local typeSel Args((Name)); static Name local linkName Args((String)); static Tycon local linkTycon Args((String)); static Class local linkClass Args((String)); /* -------------------------------------------------------------------------- * Frequently used type skeletons: * ------------------------------------------------------------------------*/ static Type arrow; /* mkOffset(0) -> mkOffset(1) */ static Type boundPair; /* (mkOffset(0),mkOffset(0)) */ static Type listof; /* [ mkOffset(0) ] */ static Type typeVarToVar; /* mkOffset(0) -> mkOffset(0) */ static Cell predNum; /* Num (mkOffset(0)) */ static Cell predFractional; /* Fractional (mkOffset(0)) */ static Cell predIntegral; /* Integral (mkOffset(0)) */ static Kind starToStar; /* Type -> Type */ static Cell predMonad; /* Monad (mkOffset(0)) */ #if MUDO static Cell predMonadRec; /* MonadRec/MonadFix (mkOffset(0)) */ #endif /* -------------------------------------------------------------------------- * Assumptions: * * A basic typing statement is a pair (Var,Type) and an assumption contains * an ordered list of basic typing statements in which the type for a given * variable is given by the most recently added assumption about that var. * * In practice, the assumption set is split between a pair of lists, one * holding assumptions for vars defined in bindings, the other for vars * defined in patterns/binding parameters etc. The reason for this * separation is that vars defined in bindings may be overloaded (with the * overloading being unknown until the whole binding is typed), whereas the * vars defined in patterns have no overloading. A form of dependency * analysis (at least as far as calculating dependents within the same group * of value bindings) is required to implement this. Where it is known that * no overloaded values are defined in a binding (i.e., when the `dreaded * monomorphism restriction' strikes), the list used to record dependents * is flagged with a NODEPENDS tag to avoid gathering dependents at that * level. * * To interleave between vars for bindings and vars for patterns, we use * a list of lists of typing statements for each. These lists are always * the same length. The implementation here is very similar to that of the * dependency analysis used in the static analysis component of this system. * * To deal with polymorphic recursion, variables defined in bindings can be * assigned types of the form (POLYREC,(def,use)), where def is a type * variable for the type of the defining occurence, and use is a type * scheme for (recursive) calls/uses of the variable. * ------------------------------------------------------------------------*/ static List defnBounds; /*::[[(Var,Type)]] possibly ovrlded*/ static List varsBounds; /*::[[(Var,Type)]] not overloaded */ static List depends; /*::[?[Var]] dependents/NODEPENDS */ static List skolVars; /*::[[Var]] skolem vars */ static List localEvs; /*::[[(Pred,offset,ev)]] */ static List savedPs; /*::[[(Pred,offset,ev)]] */ static Cell dummyVar; /* Used to put extra tvars into ass*/ #define saveVarsAss() List saveAssump = hd(varsBounds) #define restoreVarsAss() hd(varsBounds) = saveAssump #define addVarAssump(v,t) hd(varsBounds) = cons(pair(v,t),hd(varsBounds)) #define findTopBinding(v) findInAssumList(textOf(v),hd(defnBounds)) static Void local emptyAssumption() { /* set empty type assumption */ defnBounds = NIL; varsBounds = NIL; depends = NIL; skolVars = NIL; localEvs = NIL; savedPs = NIL; } static Void local enterBindings() { /* Add new level to assumption sets */ defnBounds = cons(NIL,defnBounds); varsBounds = cons(NIL,varsBounds); depends = cons(NIL,depends); } static Void local leaveBindings() { /* Drop one level of assumptions */ defnBounds = tl(defnBounds); varsBounds = tl(varsBounds); depends = tl(depends); } static Int local defType(a) /* Return type for defining occ. */ Cell a; { /* of a var from assumption pair */ return (isPair(a) && fst(a)==POLYREC) ? fst(snd(a)) : a; } static Type local useType(a) /* Return type for use of a var */ Cell a; { /* defined in an assumption */ return (isPair(a) && fst(a)==POLYREC) ? snd(snd(a)) : a; } static Void local markAssumList(as) /* Mark all types in assumption set*/ List as; { /* :: [(Var, Type)] */ for (; nonNull(as); as=tl(as)) { /* No need to mark generic types; */ Type t = defType(snd(hd(as))); /* the only free variables in those*/ if (!isPolyType(t)) /* must have been free earlier too */ markType(t,0); } } static Cell local findAssum(t) /* Find most recent assumption about*/ Text t; { /* variable named t, if any */ List defnBounds1 = defnBounds; /* return translated variable, with */ List varsBounds1 = varsBounds; /* type in typeIs */ List depends1 = depends; while (nonNull(defnBounds1)) { Pair ass = findInAssumList(t,hd(varsBounds1));/* search varsBounds */ if (nonNull(ass)) { typeIs = snd(ass); return fst(ass); } ass = findInAssumList(t,hd(defnBounds1)); /* search defnBounds */ if (nonNull(ass)) { Cell v = fst(ass); typeIs = snd(ass); if (hd(depends1)!=NODEPENDS && /* save dependent? */ isNull(v=varIsMember(t,hd(depends1)))) /* N.B. make new copy of variable and store this on list of*/ /* dependents, and in the assumption so that all uses of */ /* the variable will be at the same node, if we need to */ /* overwrite the call of a function with a translation... */ hd(depends1) = cons(v=mkVar(t),hd(depends1)); return v; } defnBounds1 = tl(defnBounds1); /* look in next level*/ varsBounds1 = tl(varsBounds1); /* of assumption set */ depends1 = tl(depends1); } return NIL; } static Pair local findInAssumList(t,as)/* Search for assumption for var */ Text t; /* named t in list of assumptions as*/ List as; { for (; nonNull(as); as=tl(as)) if (textOf(fst(hd(as)))==t) return hd(as); return NIL; } static List local intsIntersect(as,bs) /* calculate intersection of lists */ List as, bs; { /* of integers (as sets) */ List ts = NIL; /* destructively modifies as */ while (nonNull(as)) if (intIsMember(intOf(hd(as)),bs)) { List temp = tl(as); tl(as) = ts; ts = as; as = temp; } else as = tl(as); return ts; } static List local genvarAllAss(as) /* calculate generic vars that are */ List as; { /* in every type in assumptions as */ List vs = genvarTyvar(intOf(defType(snd(hd(as)))),NIL); for (as=tl(as); nonNull(as) && nonNull(vs); as=tl(as)) vs = intsIntersect(vs,genvarTyvar(intOf(defType(snd(hd(as)))),NIL)); return vs; } static List local genvarAnyAss(as) /* calculate generic vars that are */ List as; { /* in any type in assumptions as */ List vs = genvarTyvar(intOf(defType(snd(hd(as)))),NIL); for (as=tl(as); nonNull(as); as=tl(as)) vs = genvarTyvar(intOf(defType(snd(hd(as)))),vs); return vs; } static Int local newVarsBind(v) /* make new assump for pattern var */ Cell v; { Int beta = newTyvars(1); addVarAssump(v,mkInt(beta)); #if DEBUG_TYPES Printf("variable, assume "); printExp(stdout,v); Printf(" :: _%d\n",beta); #endif return beta; } static Void local newDefnBind(v,type) /* make new assump for defn var */ Cell v; /* and set type if given (nonNull) */ Type type; { Int beta = newTyvars(1); Cell ta = mkInt(beta); instantiate(type); if (nonNull(type) && isPolyType(type)) ta = pair(POLYREC,pair(ta,type)); hd(defnBounds) = cons(pair(v,ta), hd(defnBounds)); #if DEBUG_TYPES Printf("definition, assume "); printExp(stdout,v); Printf(" :: _%d\n",beta); #endif bindTv(beta,typeIs,typeOff); /* Bind beta to new type skeleton */ } /* -------------------------------------------------------------------------- * Predicates: * ------------------------------------------------------------------------*/ #include "preds.c" /* -------------------------------------------------------------------------- * Bound and skolemized type variables: * ------------------------------------------------------------------------*/ static List pendingBtyvs = NIL; static Void local enterPendingBtyvs() { enterBtyvs(); pendingBtyvs = cons(NIL,pendingBtyvs); } static Void local leavePendingBtyvsQuietly() { pendingBtyvs = tl(pendingBtyvs); leaveBtyvs(); } static Void local leavePendingBtyvs() { List pts = hd(pendingBtyvs); pendingBtyvs = tl(pendingBtyvs); for (; nonNull(pts); pts=tl(pts)) { Int line = intOf(fst(hd(pts))); List vs = snd(hd(pts)); Int i = 0; clearMarks(); for (; nonNull(vs); vs=tl(vs)) { Cell v = fst(hd(vs)); Cell t = copyTyvar(intOf(snd(hd(vs)))); if (!isOffset(t)) { ERRMSG(line) "Type annotation uses variable " ETHEN ERREXPR(v); ERRTEXT " where a more specific type " ETHEN ERRTYPE(t); ERRTEXT " was inferred" EEND; } else if (offsetOf(t)!=i) { List us = snd(hd(pts)); Int j = offsetOf(t); if (j>=i) internal("leavePendingBtyvs"); for (; j>0; j--) us = tl(us); ERRMSG(line) "Type annotation uses distinct variables " ETHEN ERREXPR(v); ERRTEXT " and " ETHEN ERREXPR(fst(hd(us))); ERRTEXT " where a single variable was inferred" EEND; } else i++; } } leaveBtyvs(); } static Cell local patBtyvs(p) /* Strip bound type vars from pat */ Cell p; { if (whatIs(p)==BIGLAM) {