home *** CD-ROM | disk | FTP | other *** search
/ APDL Public Domain 1 / APDL_PD1A.iso / program / language / gofer / Sources / c / subst < prev    next >
Encoding:
Text File  |  1993-02-12  |  14.3 KB  |  536 lines
  1. /* --------------------------------------------------------------------------
  2.  * subst.c:     Copyright (c) Mark P Jones 1991-1993.   All rights reserved.
  3.  *              See goferite.h for details and conditions of use etc...
  4.  *              Gofer version 2.28 January 1993
  5.  *
  6.  * Part of type checker dealing with operations on current substitution.
  7.  * ------------------------------------------------------------------------*/
  8.  
  9. static Void local emptySubstitution() {    /* clear current substitution       */
  10.     numTyvars   = 0;
  11.     nextGeneric = 0;
  12.     genericVars = NIL;
  13.     typeIs      = NIL;
  14.     predsAre    = NIL;
  15. }
  16.  
  17. static Int local newTyvars(n)            /* allocate new type variables       */
  18. Int n; {                /* all of kind STAR           */
  19.     Int beta = numTyvars;
  20.  
  21.     if (numTyvars+n>NUM_TYVARS) {
  22.     ERROR(0) "Too many type variables in type checker"
  23.     EEND;
  24.     }
  25.     for (numTyvars+=n; n>0; n--) {
  26.     tyvars[numTyvars-n].offs  = UNUSED_GENERIC;
  27.     tyvars[numTyvars-n].bound = NIL;
  28.     tyvars[numTyvars-n].kind  = STAR;
  29. #ifdef DEBUG_TYPES
  30. printf("new type variable: _%d ::: ",numTyvars-n);
  31. printKind(stdout,tyvars[numTyvars-n].kind);
  32. putchar('\n');
  33. #endif
  34.     }
  35.     return beta;
  36. }
  37.  
  38. static Int local newKindedVars(k)    /* allocate new variables with       */
  39. Kind k; {                /* specified kinds           */
  40.     Int beta = numTyvars;        /* if k = k0 -> k1 -> ... -> kn       */
  41.     for (; isAp(k); k=snd(k)) {        /* then allocate n vars with kinds */
  42.     if (numTyvars+1>NUM_TYVARS) {    /* k0, k1, ..., k(n-1)           */
  43.         ERROR(0) "Too many type variables in type checker"
  44.         EEND;
  45.     }
  46.     tyvars[numTyvars].offs  = UNUSED_GENERIC;
  47.     tyvars[numTyvars].bound = NIL;
  48.     tyvars[numTyvars].kind  = fst(k);
  49. #ifdef DEBUG_TYPES
  50. printf("new type variable: _%d ::: ",numTyvars);
  51. printKind(stdout,tyvars[numTyvars].kind);
  52. putchar('\n');
  53. #endif
  54.     numTyvars++;
  55.     }
  56.     return beta;
  57. }
  58.  
  59. #define freeTypeVars(beta) numTyvars=beta
  60.  
  61. #define deRef(tyv,t,o)  while ((tyv=getTypeVar(t,o)) && tyv->bound) { \
  62.                             t = tyv->bound;                           \
  63.                             o = tyv->offs;                            \
  64.                         }
  65.  
  66. static Tyvar *local getTypeVar(t,o)    /* get number of type variable       */
  67. Type t;                 /* represented by (t,o) [if any].  */
  68. Int  o; {
  69.     switch (whatIs(t)) {
  70.     case INTCELL : return tyvar(intOf(t));
  71.     case OFFSET  : return tyvar(o+offsetOf(t));
  72.     }
  73.     return ((Tyvar *)0);
  74. }
  75.  
  76. static Void local tyvarType(vn)           /* load type held in type variable */
  77. Int vn; {                       /* vn into (typeIs,typeOff)       */
  78.     Tyvar *tyv;
  79.  
  80.     while ((tyv=tyvar(vn))->bound)
  81.     switch(whatIs(tyv->bound)) {
  82.         case INTCELL : vn = intOf(tyv->bound);
  83.                break;
  84.  
  85.         case OFFSET  : vn = offsetOf(tyv->bound)+(tyv->offs);
  86.                break;
  87.  
  88.         default     : typeIs  = tyv->bound;
  89.                typeOff = tyv->offs;
  90.                return;
  91.     }
  92.     typeIs  = var;
  93.     typeOff = vn;
  94. }
  95.  
  96. static Void local bindTv(vn,t,o)           /* set type variable vn to (t,o)   */
  97. Int  vn;
  98. Type t;
  99. Int  o; {
  100.     Tyvar *tyv = tyvar(vn);
  101.     tyv->bound = t;
  102.     tyv->offs  = o;
  103. #ifdef DEBUG_TYPES
  104. printf("binding type variable: _%d to ",vn);
  105. printType(stdout,debugType(t,o));
  106. putchar('\n');
  107. #endif
  108. }
  109.  
  110. static Void local expandSynonym(h,at,ao)/* Expand type synonym with head h */
  111. Tycon h;                 /* original expression (*at,*ao)   */
  112. Type  *at;                    /* expansion returned in (*at,*ao) */
  113. Int   *ao; {
  114.     Int   n = tycon(h).arity;
  115.     Type  t = *at;
  116.     Int   o = *ao;
  117.     Tyvar *tyv;
  118.  
  119.     *at = tycon(h).defn;
  120.     *ao = newKindedVars(tycon(h).kind);
  121.     for (; 0<n--; t=fun(t)) {
  122.     deRef(tyv,t,o);
  123.     if (tyv || !isAp(t))
  124.         internal("expandSynonym");
  125.     bindTv(*ao+n,arg(t),o);
  126.     }
  127. }
  128.  
  129. static Cell local getDerefHead(t,o)    /* get value at head of type exp.  */
  130. Type t;
  131. Int  o; {
  132.     Tyvar *tyv;
  133.     argCount = 0;
  134.     for (;;) {
  135.     while (isAp(t)) {
  136.         argCount++;
  137.         t = fun(t);
  138.     }
  139.     tyv = getTypeVar(t,o);
  140.     if (tyv && tyv->bound) {
  141.         t = tyv->bound;
  142.         o = tyv->offs;
  143.     }
  144.     else
  145.         break;
  146.     }
  147.     return t;
  148. }
  149.  
  150. /* --------------------------------------------------------------------------
  151.  * Mark type expression, so that all variables are marked as unused generics
  152.  * ------------------------------------------------------------------------*/
  153.  
  154. static Void local clearMarks() {           /* set all unbound type vars to       */
  155.     Int i;                       /* unused generic variables       */
  156.     for (i=0; i<numTyvars; ++i)
  157.     if (isNull(tyvars[i].bound))
  158.         tyvars[i].offs = UNUSED_GENERIC;
  159.     nextGeneric = 0;
  160.     genericVars = NIL;
  161. }
  162.  
  163. static Void local resetGenericsFrom(n)    /* reset all generic vars to unused*/
  164. Int n; {                /* for generics >= n           */
  165.     Int i;
  166.  
  167.     if (n==0)                /* reset generic variables list       */
  168.     genericVars = NIL;        /* most common case: reset to zero */
  169.     else
  170.     for (i=length(genericVars); i>n; i--)
  171.         genericVars = tl(genericVars);
  172.  
  173.     for (i=0; i<numTyvars; ++i)
  174.     if (isNull(tyvars[i].bound) && tyvars[i].offs>=GENERIC+n)
  175.         tyvars[i].offs = UNUSED_GENERIC;
  176.     nextGeneric = n;
  177. }
  178.  
  179. static Void local markTyvar(vn)            /* mark fixed vars in type bound to*/
  180. Int vn; {                       /* given type variable           */
  181.     Tyvar *tyv = tyvar(vn);
  182.  
  183.     if (tyv->bound)
  184.     markType(tyv->bound, tyv->offs);
  185.     else
  186.     (tyv->offs) = FIXED_TYVAR;
  187. }
  188.  
  189. static Void local markType(t,o)            /* mark fixed vars in type (t,o)   */
  190. Type t;
  191. Int  o; {
  192.     switch (whatIs(t)) {
  193.     case TYCON   :
  194.     case TUPLE   :
  195.     case UNIT    :
  196.     case ARROW   :
  197.     case LIST    : return;
  198.  
  199.     case AP      : markType(fst(t),o);
  200.                markType(snd(t),o);
  201.                return;
  202.  
  203.     case OFFSET  : markTyvar(o+offsetOf(t));
  204.                return;
  205.  
  206.     case INTCELL : markTyvar(intOf(t));
  207.                return;
  208.  
  209.     default      : internal("markType");
  210.     }
  211. }
  212.  
  213. /* --------------------------------------------------------------------------
  214.  * Copy type expression from substitution to make a single type expression:
  215.  * ------------------------------------------------------------------------*/
  216.  
  217. static Type local copyTyvar(vn)            /* calculate most general form of  */
  218. Int vn; {                       /* type bound to given type var       */
  219.     Tyvar *tyv = tyvar(vn);
  220.  
  221.     if (tyv->bound)
  222.     return copyType(tyv->bound,tyv->offs);
  223.  
  224.     switch (tyv->offs) {
  225.     case FIXED_TYVAR    : return mkInt(vn);
  226.  
  227.     case UNUSED_GENERIC : (tyv->offs) = GENERIC + nextGeneric++;
  228.                   if (nextGeneric>=NUM_OFFSETS) {
  229.                   ERROR(0)
  230.                       "Too many polymorphic type variables"
  231.                   EEND;
  232.                   }
  233.                   genericVars = cons(mkInt(vn),genericVars);
  234.  
  235.     default         : return mkOffset(tyv->offs - GENERIC);
  236.     }
  237. }
  238.  
  239. static Type local copyType(t,o)            /* calculate most general form of  */
  240. Type t;                        /* type expression (t,o)        */
  241. Int  o; {
  242.     switch (whatIs(t)) {
  243.     case AP      : {   Type l = copyType(fst(t),o);  /* ensure correct */
  244.                Type r = copyType(snd(t),o);  /* eval. order    */
  245.                return ap(l,r);
  246.                }
  247.     case OFFSET  : return copyTyvar(o+offsetOf(t));
  248.     case INTCELL : return copyTyvar(intOf(t));
  249.     }
  250.  
  251.     return t;
  252. }
  253.  
  254. #ifdef DEBUG_TYPES
  255. static Type local debugTyvar(vn)    /* expand type structure in full   */
  256. Int vn; {                /* detail               */
  257.     Tyvar *tyv = tyvar(vn);
  258.  
  259.     if (tyv->bound)
  260.     return debugType(tyv->bound,tyv->offs);
  261.     return mkInt(vn);
  262. }
  263.  
  264. static Type local debugType(t,o)
  265. Type t;
  266. Int  o; {
  267.     switch (whatIs(t)) {
  268.     case AP      : {   Type l = debugType(fst(t),o);
  269.                Type r = debugType(snd(t),o);
  270.                return ap(l,r);
  271.                }
  272.     case OFFSET  : return debugTyvar(o+offsetOf(t));
  273.     case INTCELL : return debugTyvar(intOf(t));
  274.     }
  275.  
  276.     return t;
  277. }
  278. #endif /*DEBUG_TYPES*/
  279.  
  280. /* --------------------------------------------------------------------------
  281.  * Occurs check:
  282.  * ------------------------------------------------------------------------*/
  283.  
  284. static Tyvar *lookingFor;               /* var to look for in occurs check */
  285.  
  286. static Bool local doesntOccurIn(t,o)       /* Return TRUE if var lookingFor   */
  287. Type t;                        /* isn't referenced in (t,o)       */
  288. Int o; {
  289.     Tyvar *tyv;
  290.  
  291.     for (;;) {
  292.     deRef(tyv,t,o);
  293.     if (tyv)            /* type variable           */
  294.         return tyv!=lookingFor;
  295.         else if (isAp(t)) {        /* application               */
  296.         if (doesntOccurIn(snd(t),o))
  297.         t = fst(t);
  298.         else
  299.         return FALSE;
  300.     }
  301.     else                            /* no variable found           */
  302.         break;
  303.     }
  304.     return TRUE;
  305. }
  306.  
  307. /* --------------------------------------------------------------------------
  308.  * Unification algorithm:
  309.  * ------------------------------------------------------------------------*/
  310.  
  311. static char *unifyFails = 0;        /* unification error message       */
  312. static Bool matchMode    = FALSE;    /* set to TRUE to prevent binding  */
  313.                            /* during matching process       */
  314.  
  315. static Bool local varToVarBind(tyv1,tyv2)/* Make binding tyv1 := tyv2       */
  316. Tyvar *tyv1, *tyv2; {
  317.     if (tyv1!=tyv2)
  318.     if (matchMode)
  319.         return FALSE;
  320.     else {
  321.         if (!eqKind(tyv1->kind,tyv2->kind)) {
  322.         unifyFails = "constructor variable kinds do not match";
  323.         return FALSE;
  324.         }
  325.         tyv1->bound = var;
  326.         tyv1->offs    = tyvNum(tyv2);
  327. #ifdef DEBUG_TYPES
  328. printf("vv binding type variable: _%d to _%d\n",tyvNum(tyv1),tyvNum(tyv2));
  329. #endif
  330.     }
  331.     return TRUE;
  332. }
  333.  
  334. static Bool local varToTypeBind(tyv,t,o)/* Make binding tyv := (t,o)       */
  335. Tyvar *tyv;
  336. Type  t;                /* guaranteed not to be a v'ble or */
  337. Int   o; {                /* have synonym as outermost constr*/
  338.     if (!matchMode) {
  339.     lookingFor = tyv;
  340.     if (doesntOccurIn(t,o)) {
  341.         if (!eqKind(tyv->kind,getKind(t,o))) {
  342.         unifyFails = "constructor variable kinds do not match";
  343.         return FALSE;
  344.         }
  345.         tyv->bound = t;
  346.         tyv->offs  = o;
  347. #ifdef DEBUG_TYPES
  348. printf("vt binding type variable: _%d to ",tyvNum(tyv));
  349. printType(stdout,debugType(t,o));
  350. putchar('\n');
  351. #endif
  352.         return TRUE;
  353.     }
  354.     }
  355.     unifyFails = "unification would give infinite type";
  356.     return FALSE;    /* INFINITE TYPE (or failed match in matchMode)    */
  357. }
  358.  
  359. static Bool local kvarToVarBind(tyv1,tyv2)/* Make binding tyv1 := tyv2       */
  360. Tyvar *tyv1, *tyv2; {              /* for kind variable bindings       */
  361.     if (tyv1!=tyv2) {
  362.     tyv1->bound = var;
  363.     tyv1->offs  = tyvNum(tyv2);
  364.     }
  365.     return TRUE;
  366. }
  367.  
  368. static Bool local kvarToTypeBind(tyv,t,o)/* Make binding tyv := (t,o)       */
  369. Tyvar *tyv;                /* for kind variable bindings       */
  370. Type  t;                /* guaranteed not to be a v'ble or */
  371. Int   o; {                /* have synonym as outermost constr*/
  372.     lookingFor = tyv;
  373.     if (doesntOccurIn(t,o)) {
  374.     tyv->bound = t;
  375.     tyv->offs  = o;
  376.     return TRUE;
  377.     }
  378.     unifyFails = "unification would give infinite kind";
  379.     return FALSE;
  380. }
  381.  
  382. static Bool local unify(t1,o1,t2,o2)    /* Main unification routine       */
  383. Type t1,t2;                /* unify (t1,o1) with (t2,o2)       */
  384. Int  o1,o2; {
  385.     Tyvar *tyv1, *tyv2;
  386.  
  387.     deRef(tyv1,t1,o1);
  388.     deRef(tyv2,t2,o2);
  389.  
  390. un: if (tyv1)
  391.         if (tyv2)
  392.         return varToVarBind(tyv1,tyv2);        /* t1, t2 variables    */
  393.         else {
  394.         Cell h2 = getDerefHead(t2,o2);        /* t1 variable, t2 not */
  395.         if (isSynonym(h2) && argCount==tycon(h2).arity) {
  396.         expandSynonym(h2,&t2,&o2);
  397.         deRef(tyv2,t2,o2);
  398.         goto un;
  399.         }
  400.         return varToTypeBind(tyv1,t2,o2);
  401.         }
  402.     else
  403.         if (tyv2) {
  404.         Cell h1 = getDerefHead(t1,o1);        /* t2 variable, t1 not */
  405.         if (isSynonym(h1) && argCount==tycon(h1).arity) {
  406.         expandSynonym(h1,&t1,&o1);
  407.         deRef(tyv1,t1,o1);
  408.         goto un;
  409.         }
  410.         return varToTypeBind(tyv2,t1,o1);
  411.         }
  412.     else {                        /* t1, t2 not vars       */
  413.         Type h1 = getDerefHead(t1,o1);
  414.         Int  a1 = argCount;
  415.         Type h2 = getDerefHead(t2,o2);
  416.         Int  a2 = argCount;
  417.  
  418.         if (isOffset(h1) || isInt(h1)) h1=NIL;  /* represent var by NIL*/
  419.         if (isOffset(h2) || isInt(h2)) h2=NIL;
  420.  
  421.         if (nonNull(h1) && h1==h2) {/* Assuming well-formed types, both*/
  422.         if (a1!=a2)        /* t1, t2 must have same no of args*/
  423.             internal("unify");
  424.         while (isAp(t1)) {
  425.             if (!unify(arg(t1),o1,arg(t2),o2))
  426.             return FALSE;
  427.             t1 = fun(t1);
  428.             deRef(tyv1,t1,o1);
  429.             t2 = fun(t2);
  430.             deRef(tyv2,t2,o2);
  431.         }
  432.         return TRUE;
  433.         }
  434.  
  435.         /* Types do not match -- look for type synonyms to expand */
  436.  
  437.         if (isSynonym(h1) && a1==tycon(h1).arity) {
  438.         expandSynonym(h1,&t1,&o1);
  439.         deRef(tyv1,t1,o1);
  440.         goto un;
  441.         }
  442.         if (isSynonym(h2) && a2==tycon(h2).arity) {
  443.         expandSynonym(h2,&t2,&o2);
  444.                 deRef(tyv2,t2,o2);
  445.         goto un;
  446.         }
  447.  
  448.         if ((isNull(h1) && a1<=a2) ||       /* last attempt -- maybe   */
  449.         (isNull(h2) && a2<=a1))    {    /* one head is a variable? */
  450.         for (;;) {
  451.             deRef(tyv1,t1,o1);
  452.             deRef(tyv2,t2,o2);
  453.  
  454.             if (tyv1)                /* unify heads!       */
  455.             if (tyv2)
  456.                 return varToVarBind(tyv1,tyv2);
  457.             else
  458.                 return varToTypeBind(tyv1,t2,o2);
  459.             else if (tyv2)
  460.             return varToTypeBind(tyv2,t1,o1);
  461.  
  462.             /* at this point, neither t1 nor t2 is a variable. In  */
  463.             /* addition, they must both be APs unless one of the   */
  464.             /* head variables has been bound during unification of */
  465.             /* the arguments.                       */
  466.  
  467.             if (!isAp(t1) || !isAp(t2)) {    /* might not be APs*/
  468.             unifyFails = 0;
  469.             return t1==t2;
  470.             }
  471.             if (!unify(arg(t1),o1,arg(t2),o2))    /* o/w must be APs */
  472.             return FALSE;
  473.             t1 = fun(t1);
  474.             t2 = fun(t2);
  475.         }
  476.         }
  477.     }
  478.     unifyFails = 0;
  479.     return FALSE;
  480. }
  481.  
  482. static Bool local sameType(t1,o1,t2,o2)/* Compare types without binding    */
  483. Type t1,t2;
  484. Int  o1,o2; {
  485.     Bool result;
  486.     matchMode = TRUE;
  487.     result    = unify(t1,o1,t2,o2);
  488.     matchMode = FALSE;
  489.     return result;
  490. }
  491.  
  492. Bool typeMatches(type,mt)        /* test if type matches monotype mt*/
  493. Type type, mt; {
  494.     Bool result;
  495.     if (isPolyType(type) || whatIs(type)==QUAL)
  496.     return FALSE;
  497.     typeChecker(RESET);
  498.     matchMode = TRUE;
  499.     result    = unify(mt,0,type,0);
  500.     matchMode = FALSE;
  501.     typeChecker(RESET);
  502.     return result;
  503. }
  504.  
  505. /* --------------------------------------------------------------------------
  506.  * Unify kind expressions:
  507.  * ------------------------------------------------------------------------*/
  508.  
  509. static Bool local kunify(k1,o1,k2,o2)    /* Unify kind expr (k1,o1) with       */
  510. Kind k1,k2;                /* (k2,o2)               */
  511. Int  o1,o2; {
  512.     Tyvar *kyv1, *kyv2;
  513.  
  514.     deRef(kyv1,k1,o1);
  515.     deRef(kyv2,k2,o2);
  516.  
  517.     if (kyv1)
  518.         if (kyv2)
  519.         return kvarToVarBind(kyv1,kyv2);        /* k1, k2 variables    */
  520.         else
  521.         return kvarToTypeBind(kyv1,k2,o2);        /* k1 variable, k2 not */
  522.     else
  523.         if (kyv2)
  524.         return kvarToTypeBind(kyv2,k1,o1);        /* k2 variable, k1 not */
  525.     else
  526.         if (k1==STAR && k2==STAR)            /* k1, k2 not vars       */
  527.         return TRUE;
  528.         else if (isAp(k1) && isAp(k2))
  529.         return kunify(fst(k1),o1,fst(k2),o2) &&
  530.                kunify(snd(k1),o1,snd(k2),o2);
  531.     unifyFails = 0;
  532.     return FALSE;
  533. }
  534.  
  535. /*-------------------------------------------------------------------------*/
  536.