import Miranda 2.066 from upstream

1 files changed, 1613 insertions, 0 deletions

diff --git a/new/types.c b/new/types.c
new file mode 100644
index 0000000..f20627f
--- /dev/null
+++ b/new/types.c
@@ -0,0 +1,1613 @@
+/* MIRANDA TYPECHECKER  */
+
+/**************************************************************************
+ * Copyright (C) Research Software Limited 1985-90.  All rights reserved. *
+ * The Miranda system is distributed as free software under the terms in  *
+ * the file "COPYING" which is included in the distribution.              *
+ *------------------------------------------------------------------------*/
+
+#include "data.h"
+#include "big.h"
+word R=NIL;  /* direct-and-indirect dependency graph */
+word TABSTRS=NIL; /* list of abstype declarations */
+word ND;  /* undefined names used in script */
+word SBND; /* names specified but not defined (handled separately) */
+word FBS; /* list of bindings caused by parameterised %include's */
+word ATNAMES; /* global var set by abstr_check */
+word NT=NIL;  /* undefined typenames used in script */
+word TYPERRS;
+word bnf_t=0;
+word current_id=0,lastloc=0,lineptr=0;   /* used to locate type errors */
+word showchain=NIL; /* links together all occurrences of special forms (show)
+		      encountered during typecheck */
+extern word rfl;
+
+#include <setjmp.h>
+jmp_buf env1; /* for longjmp - see man (3) setjmp */
+
+checktypes() /* outcome indicated by setting of flags SYNERR, TYPERRS, ND */
+{ word s;
+  extern word freeids,SYNERR,fnts;
+  ATNAMES=TYPERRS=0;
+  NT=R=SBND=ND=NIL;  /* NT=R= added 4/6/88 */
+  if(setjmp(env1)==1)goto L;
+  if(rfl!=NIL)readoption();
+  for(s=reverse(fil_defs(hd[files]));s!=NIL;s=tl[s])
+     comp_deps(hd[s]);  /* for each identifier in current script, compute
+			      dependencies to form R */
+  R=tclos(sortrel(R));
+  if(FBS!=NIL)mcheckfbs();
+  abstr_mcheck(TABSTRS);
+L:if(TYPERRS)
+    { /* badly formed types, so give up */
+      TABSTRS=NT=R=NIL;
+      printf("typecheck cannot proceed - compilation abandoned\n");
+      SYNERR=1;
+      return; }
+  if(freeids!=NIL)redtfr(freeids);
+  /* printgraph("dependency analysis:",R); /* for debugging */
+  genshfns();
+  if(fnts!=NIL)genbnft();
+  R=msc(R);
+  /* printgraph("strong components:",R); /* for debugging */
+  s=tsort(R);
+  /* printlist("topological sort:",s); /* for debugging */
+  NT=R=NIL; /* must be invariant across the call */
+  while(s!=NIL)infer_type(hd[s]),s=tl[s];
+  checkfbs();
+  while(TABSTRS!=NIL)
+       abstr_check(hd[TABSTRS]),TABSTRS=tl[TABSTRS];
+  if(SBND!=NIL)
+    printlist("SPECIFIED BUT NOT DEFINED: ",alfasort(SBND)),SBND=NIL;
+  fixshows();
+  lastloc=0;
+  return;
+}
+
+/* NOTES
+   let element ::= id | list(id)
+   let graph1 ::= list(cons(id,list(id)))
+   let graph2 ::= list(cons(element,list(id)))
+   we define:
+   comp_deps(id)->builds R::graph1, direct dependencies
+   R=tclos(sortrel(R))::graph1, direct and indirect dependencies
+   msc(R)->collects maximal strong components in R, now R::graph2
+   tsort(graph2)->list(element), topologically sorted
+   infer_type(element)->fills in the id_type field(s) of element
+*/
+/* R occupies quadratic worst-case space - does anyone know a better way? */
+
+comp_deps(n) /* adds to R an entry of the form cons(n,RHS) where n is an
+		identifier and RHS is a list of all the identifiers in the
+                current script upon which n directly depends */
+/* it also meta-typechecks type specifications, and puts them in reduced
+   form, as it goes */
+word n;
+{ word rhs=NIL,r;
+  /* printf("comp_deps(%s)\n",get_id(n)); /* DEBUG */
+  if(id_type(n)==type_t)
+    { if(t_class(n)==algebraic_t)
+        { r=t_info(n);
+          while(r!=NIL) /* meta type check constructors */
+            { current_id=hd[r];
+              id_type(hd[r])=redtvars(meta_tcheck(id_type(hd[r])));
+              r=tl[r]; }
+        }
+      else if(t_class(n)==synonym_t)
+	     current_id=n,t_info(n)=meta_tcheck(t_info(n));
+      else if(t_class(n)==abstract_t)
+	   if(t_info(n)==undef_t)
+	     printf("error: script contains no binding for abstract typename\
+ \"%s\"\n",get_id(n)),sayhere(id_who(n),1),TYPERRS++;
+	   else current_id=n,t_info(n)=meta_tcheck(t_info(n));
+	   /* placeholder types - no action */
+      current_id=0;
+      return; }
+  if(tag[id_val(n)]==CONSTRUCTOR)return;
+    /* primitive constructors require no type analysis */
+  if(id_type(n)!=undef_t) /* meta typecheck spec, if present */
+    { current_id=n;
+      if(tag[id_type(n)]==CONS)
+	{ /* signature identifier */
+	  if(id_val(n)==UNDEF)SBND=add1(n,SBND);
+	  id_type(n)=redtvars(meta_tcheck(hd[id_type(n)]));
+	  current_id=0;
+	  return; }  /* typechecked separately, under TABSTRS */
+      id_type(n)=redtvars(meta_tcheck(id_type(n)));
+      current_id=0; }
+  if(id_val(n)==FREE)return; /* no further analysis required */
+  if(id_val(n)==UNDEF) /* name specified but not defined */
+    { SBND=add1(n,SBND); /* change of policy (as for undefined sigid, above) */
+      return; }  /* now not added to ND, so script can be %included */
+  r=deps(id_val(n));
+  while(r!=NIL)
+    { if(id_val(hd[r])!=UNDEF&&id_type(hd[r])==undef_t)
+        /* only defined names without explicitly assigned types
+	   cause dependency */
+        rhs=add1(hd[r],rhs);
+      r=tl[r]; }
+  R=cons(cons(n,rhs),R);
+}
+
+tsort(g) /* topological sort - returns a list of the elements in the domain
+  of relation g, in an order such that each element is preceded by everything
+  it depends on */
+word g;  /* the structure of g is "graph2" see NOTES above */
+{ word NP=NIL; /* NP is set of elements with no predecessor */
+  word g1=g, r=NIL; /* r is result */
+  g=NIL;
+  while(g1!=NIL)
+    { if(tl[hd[g1]]==NIL)NP=cons(hd[hd[g1]],NP);
+      else g=cons(hd[g1],g);
+      g1=tl[g1]; }
+  while(NP!=NIL)
+  { word D=NIL; /* ids to be removed from range of g */
+    while(NP!=NIL)
+    { r=cons(hd[NP],r);
+      if(tag[hd[NP]]==ID)D=add1(hd[NP],D);
+      else D=UNION(D,hd[NP]);
+      NP=tl[NP]; }
+    g1=g;g=NIL;
+    while(g1!=NIL)
+    { word rhs=setdiff(tl[hd[g1]],D);
+      if(rhs==NIL)NP=cons(hd[hd[g1]],NP);
+      else tl[hd[g1]]=rhs,g=cons(hd[g1],g);
+      g1=tl[g1]; }
+  }
+  if(g!=NIL)fprintf(stderr,"error: impossible event in tsort\n");
+  return(reverse(r));
+}
+
+msc(R) /* collects maximal strong components in R, converting it from "graph1"
+          to "graph2" form - destructive in R */
+word R;
+{ word R1=R;
+  while(R1!=NIL)
+  { word *r= &tl[hd[R1]],l=hd[hd[R1]];
+    if(remove1(l,r))
+      { hd[hd[R1]]=cons(l,NIL);
+	while(*r!=NIL)
+	{  word n=hd[*r],*R2= &tl[R1];
+           while(*R2!=NIL&&hd[hd[*R2]]!=n)R2= &tl[*R2]; /* find n-entry in R */
+	   if(*R2!=NIL&&member(tl[hd[*R2]],l))
+	     { *r=tl[*r]; /* remove n from r */
+               *R2=tl[*R2]; /* remove n's entry from R */
+	       hd[hd[R1]]=add1(n,hd[hd[R1]]);
+	     }
+	   else r= &tl[*r];
+	}
+      }
+    R1=tl[R1];
+  }
+  return(R);
+}
+
+word meta_pending=NIL;
+
+meta_tcheck(t) /* returns type t with synonyms substituted out and checks that
+                  the result is well formed */
+word t;
+{ word tn=t,i=0;
+  /* TO DO -- TIDY UP ERROR MESSAGES AND SET ERRLINE (ERRS) IF POSS */
+  while(iscompound_t(tn))
+     tl[tn]=meta_tcheck(tl[tn]),i++,tn=hd[tn];
+  if(tag[tn]==STRCONS)goto L; /* patch to handle free type bindings */
+  if(tag[tn]!=ID)
+    { if(i>0&&(isvar_t(tn)||tn==bool_t||tn==num_t||tn==char_t))
+        { TYPERRS++;
+	  if(tag[current_id]==DATAPAIR)
+	    locate_inc(),
+            printf("badly formed type \""),out_type(t),
+            printf("\" in binding for \"%s\"\n",(char *)hd[current_id]),
+            printf("("),out_type(tn),printf(" has zero arity)\n");
+	  else
+          printf("badly formed type \""),out_type(t),
+          printf("\" in %s for \"%s\"\n",
+            id_type(current_id)==type_t?"== binding":"specification",
+            get_id(current_id)),
+          printf("("),out_type(tn),printf(" has zero arity)\n"),
+	  sayhere(getspecloc(current_id),1); 
+	  sterilise(t); }
+        return(t); }
+  if(id_type(tn)==undef_t&&id_val(tn)==UNDEF)
+    { TYPERRS++;
+      if(!member(NT,tn))
+	{ if(tag[current_id]==DATAPAIR)locate_inc();
+	  printf("undeclared typename \"%s\" ",get_id(tn));
+	  if(tag[current_id]==DATAPAIR)
+	    printf("in binding for %s\n",(char *)hd[current_id]);
+	  else sayhere(getspecloc(current_id),1);
+          NT=add1(tn,NT); }
+      return(t); }else
+  if(id_type(tn)!=type_t||t_arity(tn)!=i)
+    { TYPERRS++;
+      if(tag[current_id]==DATAPAIR)
+	locate_inc(),
+        printf("badly formed type \""),out_type(t),
+        printf("\" in binding for \"%s\"\n",(char *)hd[current_id]);
+      else
+        printf("badly formed type \""),out_type(t),
+        printf("\" in %s for \"%s\"\n",
+          id_type(current_id)==type_t?"== binding":"specification",
+          get_id(current_id));
+      if(id_type(tn)!=type_t)
+        printf("(%s not defined as typename)\n",get_id(tn));
+      else printf("(typename %s has arity %d)\n",get_id(tn),t_arity(tn));
+      if(tag[current_id]!=DATAPAIR)
+        sayhere(getspecloc(current_id),1);
+      sterilise(t);
+      return(t); }
+L:if(t_class(tn)!=synonym_t)return(t);
+  if(member(meta_pending,tn))
+    { TYPERRS++;/* report cycle */
+      if(tag[current_id]==DATAPAIR)locate_inc();
+      printf("error: cycle in type \"==\" definition%s ",
+              meta_pending==NIL?"":"s");
+      printelement(meta_pending); putchar('\n');
+      if(tag[current_id]!=DATAPAIR)
+        sayhere(id_who(tn),1);
+      longjmp(env1,1); /* fatal error - give up */
+/*    t_class(tn)=algebraic_t;t_info(tn)=NIL;
+          /* to make sure we dont fall in here again! */
+      return(t); }
+  meta_pending=cons(tn,meta_pending);
+  tn=NIL;
+  while(iscompound_t(t))
+    tn=cons(tl[t],tn),t=hd[t];
+  t=meta_tcheck(ap_subst(t_info(t),tn));
+  meta_pending=tl[meta_pending];
+  return(t);
+}
+/* needless inefficiency - we recheck the rhs of a synonym every time we
+   use it */
+
+sterilise(t) /* to prevent multiple reporting of metatype errors from
+			namelist :: type	*/
+word t;
+{ if(tag[t]==AP)hd[t]=list_t,tl[t]=num_t;
+}
+
+word tvcount=1;
+#define NTV mktvar(tvcount++)
+  /* brand new type variable */
+#define reset_SUBST  (current_id=tvcount>=hashsize?clear_SUBST():0)
+
+infer_type(x) /* deduces the types of the identifiers in x - no result,
+                  works by filling in id_type fields */
+word x; /* x is an "element" */
+{ if(tag[x]==ID)
+    { word t,oldte=TYPERRS;
+      current_id=x;
+      t = subst(etype(id_val(x),NIL,NIL));
+      if(id_type(x)==undef_t)id_type(x)=redtvars(t);
+      else /* x already has assigned type */
+      if(!subsumes(t,instantiate(id_type(x))))
+	{ TYPERRS++;
+	  printf("incorrect declaration ");
+	  sayhere(getspecloc(x),1); /* or: id_who(x) to locate defn */
+          printf("specified, "); report_type(x); putchar('\n');
+	  printf("inferred,  %s :: ",get_id(x)); out_type(redtvars(t));
+	  putchar('\n'); }
+      if(TYPERRS>oldte)id_type(x)=wrong_t,
+		       id_val(x)=UNDEF,
+		       ND=add1(x,ND);
+      reset_SUBST; }
+  else{ /* recursive group of names */
+	word x1,oldte,ngt=NIL;
+	for(x1=x;x1!=NIL;x1=tl[x1])
+	   ngt=cons(NTV,ngt),
+	   id_type(hd[x1])=ap(bind_t,hd[ngt]);
+	for(x1=x;x1!=NIL;x1=tl[x1])
+	   { oldte=TYPERRS,
+             current_id=hd[x1],
+	     unify(tl[id_type(hd[x1])],etype(id_val(hd[x1]),NIL,ngt));
+	     if(TYPERRS>oldte)
+	       id_type(hd[x1])=wrong_t,
+		id_val(hd[x1])=UNDEF,ND=add1(hd[x1],ND); }
+	for(x1=x;x1!=NIL;x1=tl[x1])
+	   if(id_type(hd[x1])!=wrong_t)
+	     id_type(hd[x1])=redtvars(ult(tl[id_type(hd[x1])]));
+        reset_SUBST;
+      } 
+}
+
+word hereinc; /* location of currently-being-processed %include */
+word lasthereinc;
+
+mcheckfbs()
+{ word ff,formals,n;
+  lasthereinc=0;
+  for(ff=FBS;ff!=NIL;ff=tl[ff])
+     { hereinc=hd[hd[FBS]];
+       for(formals=tl[hd[ff]];formals!=NIL;formals=tl[formals])
+          { word t=tl[tl[hd[formals]]];
+            if(t!=type_t)continue;
+            current_id=hd[tl[hd[formals]]]; /* nb datapair(orig,0) not id */
+	    t_info(hd[hd[formals]])=meta_tcheck(t_info(hd[hd[formals]]));
+	    /*ATNAMES=cons(hd[hd[formals]],ATNAMES?ATNAMES:NIL); */
+            current_id=0;
+          }
+       if(TYPERRS)return; /* to avoid misleading error messages */
+       for(formals=tl[hd[ff]];formals!=NIL;formals=tl[formals])
+          { word t=tl[tl[hd[formals]]];
+            if(t==type_t)continue;
+            current_id=hd[tl[hd[formals]]]; /* nb datapair(orig,0) not id */
+            tl[tl[hd[formals]]]=redtvars(meta_tcheck(t));
+            current_id=0;
+          }
+     /* above double traverse is very inefficient way of doing types first
+	would be better to have bindings sorted in this order beforehand */
+     }
+  /* all imported names must now have their types reduced to
+     canonical form wrt the parameter bindings */
+  /* alternative method - put info in ATNAMES, see above and in abstr_check */
+  /* a problem with this is that types do not print in canonical form */
+  if(TYPERRS)return;
+  for(ff=tl[files];ff!=NIL;ff=tl[ff])
+  for(formals=fil_defs(hd[ff]);formals!=NIL;formals=tl[formals])
+  if(tag[n=hd[formals]]==ID)
+  if(id_type(n)==type_t)
+    { if(t_class(n)==synonym_t)t_info(n)=meta_tcheck(t_info(n)); }
+  else id_type(n)=redtvars(meta_tcheck(id_type(n)));
+} /* wasteful if many includes */
+
+redtfr(x) /* ensure types of freeids are in reduced form */
+word x;
+{ for(;x!=NIL;x=tl[x])
+     tl[tl[hd[x]]] = id_type(hd[hd[x]]);
+}
+
+checkfbs()
+/* FBS is list of entries of form cons(hereinfo,formals) where formals
+   has elements of form cons(id,cons(datapair(orig,0),type)) */
+{ word oldte=TYPERRS,formals;
+  lasthereinc=0;
+  for(;FBS!=NIL;FBS=tl[FBS])
+  for(hereinc=hd[hd[FBS]],formals=tl[hd[FBS]];
+      formals!=NIL;formals=tl[formals])
+  { word t,t1=fix_type(tl[tl[hd[formals]]]);
+    if(t1==type_t)continue;
+    current_id=hd[tl[hd[formals]]]; /* nb datapair(orig,0) not id */
+    t = subst(etype(the_val(hd[hd[formals]]),NIL,NIL));
+    if(!subsumes(t,instantiate(t1)))
+	{ TYPERRS++;
+	  locate_inc();
+	  printf("binding for parameter `%s' has wrong type\n",
+		 (char *)hd[current_id]);
+	  printf(  "required :: "); out_type(tl[tl[hd[formals]]]);
+	  printf("\n  actual :: "); out_type(redtvars(t));
+	  putchar('\n'); }
+    the_val(hd[hd[formals]])=codegen(the_val(hd[hd[formals]])); }
+  if(TYPERRS>oldte)
+    { /* badly typed parameter bindings, so give up */
+      extern word SYNERR;
+      TABSTRS=NT=R=NIL;
+      printf("compilation abandoned\n");
+      SYNERR=1; }
+  reset_SUBST;
+}
+
+fix_type(t,x)  /* substitute out any indirected typenames in t */
+word t,x;
+{ switch(tag[t])
+  { case AP: 
+    case CONS: tl[t]=fixtype(tl[t],x);
+               hd[t]=fixtype(hd[t],x);
+    default:   return(t);
+    case STRCONS: while(tag[pn_val(t)]!=CONS)t=pn_val(t);/*at most twice*/
+		  return(t);
+  }
+}
+
+locate_inc()
+{ if(lasthereinc==hereinc)return;
+  printf("incorrect %%include directive ");
+  sayhere(lasthereinc=hereinc,1);
+}
+
+abstr_mcheck(tabstrs) /* meta-typecheck abstract type declarations */
+word tabstrs;
+{ while(tabstrs!=NIL)
+     { word atnames=hd[hd[tabstrs]],sigids=tl[hd[tabstrs]],rtypes=NIL;
+       if(cyclic_abstr(atnames))return;
+       while(sigids!=NIL) /* compute representation types */
+          { word rt=rep_t(id_type(hd[sigids]),atnames);
+          /*if(rt==id_type(hd[sigids]))
+     	 printf("abstype declaration error: \"%s\" has a type unrelated to \
+the abstraction\n",get_id(hd[sigids])),
+	       sayhere(getspecloc(hd[sigids]),1),
+	       TYPERRS++; /* suppressed June 89, see karen.m, secret.m */
+            rtypes=cons(rt,rtypes);
+	    sigids=tl[sigids]; }
+       rtypes=reverse(rtypes);
+       hd[hd[tabstrs]]=cons(hd[hd[tabstrs]],rtypes);
+       tabstrs=tl[tabstrs];
+     }
+}
+
+abstr_check(x) /* typecheck the implementation equations of a type abstraction
+		  with the given signature */
+word x;
+{ word rtypes=tl[hd[x]],sigids=tl[x];
+/*int holdat=ATNAMES;
+  ATNAMES=shunt(hd[hd[x]],ATNAMES); */
+  ATNAMES=hd[hd[x]];
+  txchange(sigids,rtypes);  /* install representation types */
+  /* report_types("concrete signature:\n",sigids); /* DEBUG */
+  for(x=sigids;x!=NIL;x=tl[x])
+     { word t,oldte=TYPERRS;
+       current_id=hd[x];
+       t=subst(etype(id_val(hd[x]),NIL,NIL));
+       if(!subsumes(t,instantiate(id_type(hd[x]))))
+	 { TYPERRS++;
+	   printf("abstype implementation error\n");
+	   printf("\"%s\" is bound to value of type: ",get_id(hd[x]));
+	   out_type(redtvars(t));
+	   printf("\ntype expected: ");
+	   out_type(id_type(hd[x]));
+	   putchar('\n');
+	   sayhere(id_who(hd[x]),1); }
+       if(TYPERRS>oldte)
+	 id_type(hd[x])=wrong_t,id_val(hd[x])=UNDEF,ND=add1(hd[x],ND);
+       reset_SUBST; }
+  /* restore the abstract types - for "finger" */
+  for(x=sigids;x!=NIL;x=tl[x],rtypes=tl[rtypes])
+     if(id_type(hd[x])!=wrong_t)id_type(hd[x])=hd[rtypes];
+  ATNAMES= /* holdat */ 0;
+}
+
+cyclic_abstr(atnames) /* immediately-cyclic acts of dta are illegal */
+word atnames;
+{ word x,y=NIL;
+  for(x=atnames;x!=NIL;x=tl[x])y=ap(y,t_info(hd[x]));
+  for(x=atnames;x!=NIL;x=tl[x])
+  if(occurs(hd[x],y))
+    { printf("illegal type abstraction: cycle in \"==\" binding%s ",
+	     tl[atnames]==NIL?"":"s");
+      printelement(atnames); putchar('\n');
+      sayhere(id_who(hd[x]),1);
+      TYPERRS++; return(1); }
+  return(0);
+}
+
+txchange(ids,x)  /* swap the id_type of each id with the corresponding type 
+		    in the list x */
+word ids,x;
+{ while(ids!=NIL)
+       { word t=id_type(hd[ids]);
+	 id_type(hd[ids])=hd[x],hd[x]=t;
+	 ids=tl[ids],x=tl[x]; }
+}
+
+report_type(x)
+word x;
+{ printf("%s",get_id(x));
+  if(id_type(x)==type_t)
+  if(t_arity(x)>5)printf("(arity %d)",t_arity(x));
+  else { word i,j;
+	 for(i=1;i<=t_arity(x);i++)
+	    { putchar(' ');
+	      for(j=0;j<i;j++)putchar('*'); }
+       }
+  printf(" :: ");
+  out_type(id_type(x));
+}
+
+report_types(header,x)
+char *header;
+word x;
+{ printf("%s",header);
+  while(x!=NIL)
+       report_type(hd[x]),putchar(';'),x=tl[x];
+  putchar('\n');
+}
+
+typesfirst(x)  /* rearrange list of ids to put types first */
+word x;
+{ word *y= &x,z=NIL;
+  while(*y!=NIL)
+       if(id_type(hd[*y])==type_t)
+         z=cons(hd[*y],z),*y=tl[*y];
+       else y= &tl[*y];
+  return(shunt(z,x));
+}
+
+rep_t1(T,L) /* computes the representation type corresponding to T, wrt the
+              abstract typenames in L */
+	   /* will need to apply redtvars to result, see below */
+           /* if no substitutions found, result is identically T */
+word T,L;
+{ word args=NIL,t1,new=0;
+  for(t1=T;iscompound_t(t1);t1=hd[t1])
+     { word a=rep_t1(tl[t1],L);
+       if(a!=tl[t1])new=1;
+       args=cons(a,args); }
+  if(member(L,t1))return(ap_subst(t_info(t1),args));
+    	/* call to redtvars removed 26/11/85
+       	   leads to premature normalisation of subterms */
+  if(!new)return(T);
+  while(args!=NIL)
+       t1=ap(t1,hd[args]),args=tl[args];
+  return(t1);
+}
+
+rep_t(T,L) /* see above */
+word T,L;
+{ word t=rep_t1(T,L);
+  return(t==T?t:redtvars(t));
+}
+
+type_of(x)  /* returns the type of expression x, in reduced form */
+word x;
+{ word t;
+  TYPERRS=0;
+  t=redtvars(subst(etype(x,NIL,NIL)));
+  fixshows();
+  if(TYPERRS>0)t=wrong_t;
+  return(t);
+}
+
+checktype(x)  /* is expression x well-typed ? */
+           /* not currently used */
+word x;
+{ TYPERRS=0;
+  etype(x,NIL,NIL);
+  reset_SUBST;
+  return(!TYPERRS);
+}
+
+#define bound_t(t) (iscompound_t(t)&&hd[t]==bind_t)
+#define tf(a,b) ap2(arrow_t,a,b)
+#define tf2(a,b,c) tf(a,tf(b,c))
+#define tf3(a,b,c,d) tf(a,tf2(b,c,d))
+#define tf4(a,b,c,d,e) tf(a,tf3(b,c,d,e))
+#define lt(a) ap(list_t,a)
+#define pair_t(x,y) ap2(comma_t,x,ap2(comma_t,y,void_t))
+
+word tfnum,tfbool,tfbool2,tfnum2,tfstrstr,tfnumnum,ltchar,
+    tstep,tstepuntil;
+
+tsetup()
+{ tfnum=tf(num_t,num_t);
+  tfbool=tf(bool_t,bool_t);
+  tfnum2=tf(num_t,tfnum);
+  tfbool2=tf(bool_t,tfbool);
+  ltchar=lt(char_t);
+  tfstrstr=tf(ltchar,ltchar);
+  tfnumnum=tf(num_t,num_t);
+  tstep=tf2(num_t,num_t,lt(num_t));
+  tstepuntil=tf(num_t,tstep);
+}
+
+word exec_t=0,read_t=0,filestat_t=0; /* set lazily, when used */
+
+genlstat_t() /* type of %lex state */
+{ return(pair_t(num_t,num_t)); }
+
+genbnft()  /* if %bnf used, find out input type of parsing fns */
+{ word bnftokenstate=findid("bnftokenstate");
+  if(bnftokenstate!=NIL&&id_type(bnftokenstate)==type_t)
+  if(t_arity(bnftokenstate)==0)
+    bnf_t=t_class(bnftokenstate)==synonym_t?
+          t_info(bnftokenstate):bnftokenstate;
+  else printf("warning - bnftokenstate has arity>0 (ignored by parser)\n"),
+       bnf_t=void_t;
+  else bnf_t=void_t;  /* now bnf_t holds the state type */
+  bnf_t=ap2(comma_t,ltchar,ap2(comma_t,bnf_t,void_t));
+} /* the input type for parsers is lt(bnf_t)
+     note that tl[hd[tl[bnf_t]]] holds the state type */
+
+extern word col_fn;
+
+checkcolfn()  /* if offside rule used, check col_fn has right type */
+{ word t=id_type(col_fn),f=tf(tl[hd[tl[bnf_t]]],num_t);
+  if(t==undef_t||t==wrong_t 
+      /* will be already reported - do not generate further typerrs
+         in both cases col_fn will behave as undefined name */
+    ||subsumes(instantiate(t),f))
+    { col_fn=0; return; } /* no further action required */
+  printf("`bnftokenindentation' has wrong type for use in offside rule\n");
+  printf("type required :: "); out_type(f); putchar('\n');
+  printf("  actual type :: "); out_type(t); putchar('\n');
+  sayhere(getspecloc(col_fn),1);
+  TYPERRS++;
+  col_fn= -1; /* error flag */
+} /* note that all parsing fns get type wrong_t if offside rule used
+     anywhere and col_fn has wrong type - strictly this is overkill */
+
+etype(x,env,ngt) /* infer a type for an expression, by using unification */
+word x,env;   /* env is list of local bindings of variables to types */
+word ngt;     /* ngt is list of non-generic type variables */
+{ word a,b,c,d; /* initialise to 0 ? */
+  switch(tag[x])
+  { case AP: if(hd[x]==BADCASE||hd[x]==CONFERROR)return(NTV);
+	     /* don't type check insides of error messages */
+             { word ft=etype(hd[x],env,ngt),at=etype(tl[x],env,ngt),rt=NTV;
+               if(!unify1(ft,ap2(arrow_t,at,rt)))
+                 { ft=subst(ft);
+                   if(isarrow_t(ft))
+                     if(tag[hd[x]]==AP&&hd[hd[x]]==G_ERROR)
+                        type_error8(at,tl[hd[ft]]);
+                     else
+                     type_error("unify","with",at,tl[hd[ft]]);
+                   else type_error("apply","to",ft,at);
+		   return(NTV); }
+	       return(rt); }
+    case CONS: { word ht=etype(hd[x],env,ngt),rt=etype(tl[x],env,ngt);
+		 if(!unify1(ap(list_t,ht),rt))
+                   { type_error("cons","to",ht,rt);
+		     return(NTV); }
+		 return(rt); }
+    case LEXER: { word hold=lineptr;
+                  lineptr=hd[tl[tl[hd[x]]]];
+                  tl[tl[hd[x]]]=tl[tl[tl[hd[x]]]];/*discard label(hereinf,-)*/
+                  a=etype(tl[tl[hd[x]]],env,ngt);
+                  while((x=tl[x])!=NIL)
+                       { lineptr=hd[tl[tl[hd[x]]]];
+                         tl[tl[hd[x]]]=tl[tl[tl[hd[x]]]];/*discard label... */
+                         if(!unify1(a,b=etype(tl[tl[hd[x]]],env,ngt)))
+                           { type_error7(a,b);
+                             lineptr=hold;
+                             return(NTV); }
+                       }
+                  lineptr=hold;
+                  return(tf(ltchar,lt(a))); }
+    case TCONS: return(ap2(comma_t,etype(hd[x],env,ngt),
+		       etype(tl[x],env,ngt)));
+    case PAIR: return(ap2(comma_t,etype(hd[x],env,ngt),
+		      ap2(comma_t,etype(tl[x],env,ngt),void_t)));
+    case DOUBLE:
+    case INT: return(num_t);
+    case ID:  a=env;
+	      while(a!=NIL) /* take local binding, if present */
+		   if(hd[hd[a]]==x)
+		     return(linst(tl[hd[a]]=subst(tl[hd[a]]),ngt));
+		   else a=tl[a];
+	      a=id_type(x); /* otherwise pick up global binding */
+	      if(bound_t(a))return(tl[a]);
+              if(a==type_t)type_error1(x);
+	      if(a==undef_t)
+	        { extern word commandmode;
+		  if(commandmode)type_error2(x);
+		  else
+		  if(!member(ND,x))  /* report first occurrence only */
+		    { if(lineptr)sayhere(lineptr,0);
+                      else if(tag[current_id]==DATAPAIR) /* see checkfbs */
+			   locate_inc();
+		      printf("undefined name \"%s\"\n",get_id(x));
+                      ND=add1(x,ND); }
+		  return(NTV); }
+	      if(a==wrong_t)return(NTV);
+              return(instantiate(ATNAMES?rep_t(a,ATNAMES):a));
+    case LAMBDA: a=NTV; b=NTV;
+		 d=cons(a,ngt);
+		 c=conforms(hd[x],a,env,d);
+		 if(c==-1||!unify(b,etype(tl[x],c,d)))return(NTV);
+		 return(tf(a,b));
+    case LET: { word e,def=hd[x];
+		a=NTV,e=conforms(dlhs(def),a,env,cons(a,ngt));
+		current_id=cons(dlhs(def),current_id);
+	        c=lineptr; lineptr=dval(def);
+		b = unify(a,etype(dval(def),env,ngt));
+		lineptr=c;
+		current_id=tl[current_id];
+		if(e==-1||!b)return(NTV);
+		return(etype(tl[x],e,ngt)); }
+    case LETREC: { word e=env,s=NIL;
+		   a=NIL; c=ngt;
+		   for(d=hd[x];d!=NIL;d=tl[d])
+		      if(dtyp(hd[d])==undef_t)
+		         a=cons(hd[d],a), /* unspecified defs */
+			 dtyp(hd[d])=(b=NTV),
+		         c=cons(b,c),  /* collect non-generic tvars */
+		         e=conforms(dlhs(hd[d]),b,e,c);
+		      else dtyp(hd[d])=meta_tcheck(dtyp(hd[d])),
+		           /* should do earlier, and locate errs properly*/
+			   s=cons(hd[d],s), /* specified defs */
+			   e=cons(cons(dlhs(hd[d]),dtyp(hd[d])),e);
+		   if(e==-1)return(NTV);
+		   b=1;
+		   for(;a!=NIL;a=tl[a])
+		      { current_id=cons(dlhs(hd[a]),current_id);
+		        d=lineptr; lineptr=dval(hd[a]);
+		        b &= unify(dtyp(hd[a]),etype(dval(hd[a]),e,c));
+		        lineptr=d; current_id=tl[current_id]; }
+		   for(;s!=NIL;s=tl[s])
+		      { current_id=cons(dlhs(hd[s]),current_id);
+		        d=lineptr; lineptr=dval(hd[s]);
+		        if(!subsumes(a=etype(dval(hd[s]),e,ngt),
+				       linst(dtyp(hd[s]),ngt)))
+		       /* would be better to set lineptr to spec here */
+			  b=0,type_error6(dlhs(hd[s]),dtyp(hd[s]),a);
+		        lineptr=d; current_id=tl[current_id]; }
+		   if(!b)return(NTV);
+		   return(etype(tl[x],e,ngt)); }
+    case TRIES: { word hold=lineptr;
+		  a=NTV;
+		  x=tl[x];
+		  while(x!=NIL&&(lineptr=hd[hd[x]],
+		                 unify(a,etype(tl[hd[x]],env,ngt)))
+		       )x=tl[x];
+		  lineptr=hold;
+		  if(x!=NIL)return(NTV);
+		  return(a); }
+    case LABEL: { word hold=lineptr,t;
+		  lineptr=hd[x];
+		  t=etype(tl[x],env,ngt);
+		  lineptr=hold;
+		  return(t); }
+    case STARTREADVALS: if(tl[x]==0)
+			  hd[x]=lineptr, /* insert here-info */
+			  tl[x]=NTV,
+	                  showchain=cons(x,showchain);
+	                return(tf(ltchar,lt(tl[x])));
+    case SHOW: hd[x]=lineptr; /* insert here-info */
+	       showchain=cons(x,showchain);
+	       return(tf(tl[x]=NTV,ltchar));
+    case SHARE: if(tl[x]==undef_t)
+		  { word h=TYPERRS;
+		    tl[x]=subst(etype(hd[x],env,ngt));
+		    if(TYPERRS>h)hd[x]=UNDEF,tl[x]=wrong_t; }
+		if(tl[x]==wrong_t)
+		  { TYPERRS++; return(NTV); }
+		return(tl[x]);
+    case CONSTRUCTOR: a=id_type(tl[x]);
+                      return(instantiate(ATNAMES?rep_t(a,ATNAMES):a));
+    case UNICODE: return(char_t);
+    case ATOM: if(x<256)return(char_t);
+               switch(x)
+               { 
+               case S:a=NTV,b=NTV,c=NTV;
+                      d=tf3(tf2(a,b,c),tf(a,b),a,c);
+                      return(d);
+               case K:a=NTV,b=NTV;
+                      return(tf2(a,b,a));
+               case Y:a=NTV;
+                      return(tf(tf(a,a),a));
+               case C:a=NTV,b=NTV,c=NTV;
+                      return(tf3(tf2(a,b,c),b,a,c));
+               case B:a=NTV,b=NTV,c=NTV;
+		      return(tf3(tf(a,b),tf(c,a),c,b));
+	       case FORCE:
+	       case G_UNIT:
+	       case G_RULE:
+               case I:a=NTV;
+                      return(tf(a,a));
+               case G_ZERO:return(NTV);
+               case HD:a=NTV;
+                       return(tf(lt(a),a));
+               case TL:a=lt(NTV);
+                       return(tf(a,a));
+               case BODY:a=NTV,b=NTV;
+			 return(tf(ap(a,b),a));
+               case LAST:a=NTV,b=NTV;
+			 return(tf(ap(a,b),b));
+               case S_p:a=NTV,b=NTV;
+			c=lt(b);
+			return(tf3(tf(a,b),tf(a,c),a,c));
+               case U:
+               case U_: a=NTV,b=NTV;
+			c=lt(a);
+			return(tf2(tf2(a,c,b),c,b));
+               case Uf: a=NTV,b=NTV,c=NTV;
+                        return(tf2(tf2(tf(a,b),a,c),b,c));
+               case COND: a=NTV;
+			  return(tf3(bool_t,a,a,a));
+               case EQ:case GR:case GRE:
+               case NEQ: a=NTV;
+			 return(tf2(a,a,bool_t));
+	       case NEG: return(tfnum);
+               case AND:
+               case OR: return(tfbool2);
+               case NOT: return(tfbool);
+	       case MERGE:
+               case APPEND: a=lt(NTV);
+			    return(tf2(a,a,a));
+	       case STEP: return(tstep);
+	       case STEPUNTIL: return(tstepuntil);
+	       case MAP: a=NTV; b=NTV;
+			 return(tf2(tf(a,b),lt(a),lt(b)));
+	       case FLATMAP: a=NTV,b=lt(NTV);
+			     return(tf2(tf(a,b),lt(a),b));
+	       case FILTER: a=NTV; b=lt(a);
+			    return(tf2(tf(a,bool_t),b,b));
+  	       case ZIP: a=NTV; b=NTV;
+			 return(tf2(lt(a),lt(b),lt(pair_t(a,b))));
+	       case FOLDL: a=NTV; b=NTV;
+			   return(tf3(tf2(a,b,a),a,lt(b),a));
+	       case FOLDL1: a=NTV;
+			    return(tf2(tf2(a,a,a),lt(a),a));
+	       case LIST_LAST: a=NTV;
+			       return(tf(lt(a),a));
+	       case FOLDR: a=NTV; b=NTV;
+			   return(tf3(tf2(a,b,b),b,lt(a),b));
+	       case MATCHINT:
+               case MATCH: a=NTV,b=NTV;
+			   return(tf3(a,b,a,b));
+               case TRY: a=NTV;
+			 return(tf2(a,a,a));
+	       case DROP:
+               case TAKE: a=lt(NTV);
+			  return(tf2(num_t,a,a));
+               case SUBSCRIPT:a=NTV;
+			      return(tf2(num_t,lt(a),a));
+               case P: a=NTV;
+		       b=lt(a);
+		       return(tf2(a,b,b));
+               case B_p: a=NTV,b=NTV;
+			 c=lt(a);
+			 return(tf3(a,tf(b,c),b,c));
+               case C_p: a=NTV,b=NTV;
+			 c=lt(b);
+			 return(tf3(tf(a,b),c,a,c));
+               case S1: a=NTV,b=NTV,c=NTV,d=NTV;
+			return(tf4(tf2(a,b,c),tf(d,a),tf(d,b),d,c));
+               case B1: a=NTV,b=NTV,c=NTV,d=NTV;
+			return(tf4(tf(a,b),tf(c,a),tf(d,c),d,b));
+               case C1: a=NTV,b=NTV,c=NTV,d=NTV;
+			return(tf4(tf2(a,b,c),tf(d,a),b,d,c));
+	       case SEQ: a=NTV,b=NTV;
+			 return(tf2(a,b,b));
+	       case ITERATE1:
+	       case ITERATE: a=NTV;
+			     return(tf2(tf(a,a),a,lt(a)));
+               case EXEC: { if(!exec_t)
+                              a=ap2(comma_t,ltchar,ap2(comma_t,num_t,void_t)),
+                              exec_t=tf(ltchar,ap2(comma_t,ltchar,a));
+                            return(exec_t); }
+	       case READBIN:
+               case READ: { if(!read_t)
+                              read_t=tf(char_t,ltchar);
+                            /* $- is ap(READ,0) */
+                            return(read_t); }
+               case FILESTAT: { if(!filestat_t)
+                  filestat_t=tf(ltchar,pair_t(pair_t(num_t,num_t),num_t));
+                                return(filestat_t); }
+	       case FILEMODE:
+	       case GETENV:
+	       case NB_STARTREAD:
+	       case STARTREADBIN:
+	       case STARTREAD: return(tfstrstr);
+               case GETARGS: return(tf(char_t,lt(ltchar)));
+               case SHOWHEX:
+               case SHOWOCT:
+	       case SHOWNUM: return(tf(num_t,ltchar));
+	       case SHOWFLOAT:
+	       case SHOWSCALED: return(tf2(num_t,num_t,ltchar));
+	       case NUMVAL: return(tf(ltchar,num_t));
+	       case INTEGER: return(tf(num_t,bool_t));
+	       case CODE: return(tf(char_t,num_t));
+	       case DECODE: return(tf(num_t,char_t));
+	       case LENGTH: return(tf(lt(NTV),num_t));
+	       case ENTIER_FN: case ARCTAN_FN: case EXP_FN: case SIN_FN:
+	       case COS_FN: case SQRT_FN: case LOG_FN: case LOG10_FN:
+			    return(tfnumnum);
+               case MINUS:case PLUS:case TIMES:case INTDIV:case FDIV:
+               case MOD:case POWER: return(tfnum2);
+	       case True: case False: return(bool_t);
+	       case NIL: a=lt(NTV);
+                         return(a);
+	       case NILS: return(ltchar);
+               case MKSTRICT: a=NTV;
+			      return(tf(char_t,tf(a,a)));
+/* the following are not the true types of the G_fns, which have the action
+   	Ai->lt(bnf_t)->(B:lt(bnf_t))
+   here represented by the type Ai->B.  G_CLOSE interfaces the parser fns to
+   the outside world */
+	       case G_ALT: a=NTV;
+			   return(tf2(a,a,a));
+	       case G_ERROR: a=NTV;
+			     return(tf2(a,tf(lt(bnf_t),a),a));
+	       case G_OPT:
+	       case G_STAR: a=NTV;
+			    return(tf(a,lt(a)));
+	       case G_FBSTAR: a=NTV; b=tf(a,a);
+			      return(tf(b,b));
+	       case G_SYMB: return(tfstrstr);
+	       case G_ANY: return(ltchar);
+	       case G_SUCHTHAT: return(tf(tf(ltchar,bool_t),ltchar));
+	       case G_END: return(lt(bnf_t));
+	       case G_STATE: return(tl[hd[tl[bnf_t]]]);
+	       case G_SEQ: a=NTV; b=NTV;
+			   return(tf2(a,tf(a,b),b));
+	       /* G_RULE has same type as I */
+	       case G_CLOSE: a=NTV;
+			     if(col_fn) /* offside rule used */
+			     if(col_fn== -1) /* arbitrary flag */
+			       TYPERRS++; /*overkill, see note on checkcolfn*/
+			     else checkcolfn();
+			     return(tf3(ltchar,a,lt(bnf_t),a));
+	       case OFFSIDE: return(ltchar);
+			     /* pretend, used by indent, see prelude */
+	       case FAIL: /* compiled from last guard on rhs */
+	       case CONFERROR:
+	       case BADCASE:
+	       case UNDEF: return(NTV);
+	       case ERROR: return(tf(ltchar,NTV));
+               default: printf("do not know type of ");
+                        out(stdout,x);
+                        putchar('\n');
+                        return(wrong_t);
+               }
+    default: printf("unexpected tag in etype ");
+	     out(stdout,tag[x]);
+	     putchar('\n');
+	     return(wrong_t);
+  }
+}
+
+rhs_here(r)
+word r;
+{ if(tag[r]==LABEL)return(hd[r]);
+  if(tag[r]==TRIES)return(hd[hd[lastlink(tl[r])]]);
+  return(0); /* something wrong */
+} /* efficiency hack, sometimes we set lineptr to rhs, can extract here_info
+     as above when needed */
+
+conforms(p,t,e,ngt) /* returns new environment of local type bindings obtained
+		       by conforming pattern p to type t; -1 means failure */
+word p,t,e,ngt;
+{ if(e==-1)return(-1);
+  if(tag[p]==ID&&!isconstructor(p))return(cons(cons(p,t),e));
+  if(hd[p]==CONST)
+    { unify(etype(tl[p],e,ngt),t); return(e); }
+  if(tag[p]==CONS)
+    { word at=NTV;
+      if(!unify(lt(at),t))return(-1);
+      return(conforms(tl[p],t,conforms(hd[p],at,e,ngt),ngt)); }
+  if(tag[p]==TCONS)
+    { word at=NTV,bt=NTV;
+      if(!unify(ap2(comma_t,at,bt),t))return(-1);
+      return(conforms(tl[p],bt,conforms(hd[p],at,e,ngt),ngt)); }
+  if(tag[p]==PAIR)
+    { word at=NTV,bt=NTV;
+      if(!unify(ap2(comma_t,at,ap2(comma_t,bt,void_t)),t))return(-1);
+      return(conforms(tl[p],bt,conforms(hd[p],at,e,ngt),ngt)); }
+  if(tag[p]==AP&&tag[hd[p]]==AP&&hd[hd[p]]==PLUS) /* n+k pattern */
+    { if(!unify(num_t,t))return(1);
+      return(conforms(tl[p],num_t,e,ngt)); }
+{ word p_args=NIL,pt;
+  while(tag[p]==AP)p_args=cons(tl[p],p_args),p=hd[p];
+  if(!isconstructor(p))
+    { type_error4(p); return(-1); }
+  if(id_type(p)==undef_t)
+    { type_error5(p); return(-1); }
+  pt= /*instantiate(id_type(p)); */
+     instantiate(ATNAMES?rep_t(id_type(p),ATNAMES):id_type(p));
+  while(p_args!=NIL&&isarrow_t(pt))
+       { e=conforms(hd[p_args],tl[hd[pt]],e,ngt),pt=tl[pt],p_args=tl[p_args];
+	 if(e==-1)return(-1); }
+  if(p_args!=NIL||isarrow_t(pt)){ type_error3(p); return(-1); }
+  if(!unify(pt,t))return(-1);
+  return(e);
+}}
+
+locate(s) /* for locating type errors */
+char *s;
+{ TYPERRS++;
+  if(TYPERRS==1||lastloc!=current_id) /* avoid tedious repetition */
+    if(current_id)
+    if(tag[current_id]==DATAPAIR) /* see checkfbs */
+      { locate_inc();
+        printf("%s in binding for %s\n",s,(char *)hd[current_id]);
+	return; }
+    else
+      { extern word fnts;
+	word x=current_id;
+        printf("%s in definition of ",s);
+        while(tag[x]==CONS)
+	     if(tag[tl[x]]==ID&&member(fnts,tl[x]))
+	       printf("nonterminal "),x=hd[x]; else /*note1*/
+	     out_formal1(stdout,hd[x]),printf(", subdef of "),
+	     x=tl[x];
+        printf("%s",get_id(x));
+        putchar('\n'); }
+    else printf("%s in expression\n",s);
+  if(lineptr)sayhere(lineptr,0); else
+  if(current_id&&id_who(current_id)!=NIL)sayhere(id_who(current_id),0);
+  lastloc=current_id;
+}
+/* note1: this is hack to suppress extra `subdef of <fst start symb>' when
+   reporting error in defn of non-terminal in %bnf stuff */
+
+sayhere(h,nl) /* h is hereinfo - reports location (in parens, newline if nl)
+	         and sets errline/errs if not already set */
+word h,nl;
+{ extern word errs,errline;
+  extern char *current_script;
+  if(tag[h]!=FILEINFO)
+    { h=rhs_here(h); 
+      if(tag[h]!=FILEINFO)
+        { fprintf(stderr,"(impossible event in sayhere)\n"); return; }}
+  printf("(line %3d of %s\"%s\")",tl[h],
+          (char *)hd[h]==current_script?"":"%insert file ",(char *)hd[h]);
+  if(nl)putchar('\n'); else putchar(' ');
+  if((char *)hd[h]==current_script)
+    { if(!errline) /* tells editor where first error is */
+        errline=tl[h]; }
+  else { if(!errs)errs=h; }
+}
+
+type_error(a,b,t1,t2)
+char *a,*b;
+word t1,t2;
+{ t1=redtvars(ap(subst(t1),subst(t2)));
+  t2=tl[t1];t1=hd[t1];
+  locate("type error");
+  printf("cannot %s ",a);out_type(t1);
+  printf(" %s ",b);out_type(t2);putchar('\n');
+}
+
+type_error1(x)    /* typename in expression */
+word x;
+{ locate("type error");
+  printf("typename used as identifier (%s)\n",get_id(x));
+}
+
+type_error2(x)    /* undefined name in expression */
+word x;
+{ if(compiling)return; /* treat as type error only in $+ data */
+  TYPERRS++;
+  printf("undefined name - %s\n",get_id(x));
+}
+
+type_error3(x)    /* constructor used at wrong arity in formal */
+word x;
+{ locate("error");
+  printf("constructor \"%s\" used at wrong arity in formal\n", get_id(x));
+}
+
+type_error4(x) /* non-constructor as head of formal */
+word x;
+{ locate("error");
+  printf("illegal object \""); out_pattern(stdout,x);
+  printf("\" as head of formal\n");
+}
+
+type_error5(x) /* undeclared constructor in formal */
+word x;
+{ locate("error");
+  printf("undeclared constructor \""); out_pattern(stdout,x);
+  printf("\" in formal\n");
+  ND=add1(x,ND);
+}
+
+type_error6(x,f,a)
+word x,f,a;
+{ TYPERRS++;
+  printf("incorrect declaration "); sayhere(lineptr,1);
+  printf("specified, %s :: ",get_id(x)); out_type(f); putchar('\n');
+  printf("inferred,  %s :: ",get_id(x)); out_type(redtvars(subst(a)));
+  putchar('\n');
+}
+
+type_error7(t,args)
+word t,args;
+{ word i=1;
+  while((args=tl[args])!=NIL)i++;
+  locate("type error");
+  printf(i==1?"1st":i==2?"2nd":i==3?"3rd":"%dth",i);
+  printf(" arg of zip has type :: ");
+  out_type(redtvars(subst(t)));
+  printf("\n - should be list\n");
+}
+
+type_error8(t1,t2)
+word t1,t2;
+{ word big;
+  t1=subst(t1); t2=subst(t2);
+  if(same(hd[t1],hd[t2]))
+    t1=tl[t1],t2=tl[t2]; /* discard `[bnf_t]->' */
+  t1=redtvars(ap(t1,t2));
+  t2=tl[t1];t1=hd[t1];
+  big = size(t1)>=10 || size(t2)>=10;
+  locate("type error");
+  printf("cannot unify%s ",big?"\n ":"");out_type(t1);
+  printf(big?"\nwith\n  ":" with ");out_type(t2);putchar('\n');
+}
+
+unify(t1,t2) /* works by side-effecting SUBST, returns 1,0 as it succeeds
+		or fails */
+word t1,t2;
+{ t1=subst(t1),t2=subst(t2);
+  if(t1==t2)return(1);
+  if(isvar_t(t1)&&!occurs(t1,t2))
+  { addsubst(t1,t2); return(1); }
+  if(isvar_t(t2)&&!occurs(t2,t1))
+  { addsubst(t2,t1); return(1); }
+  if(iscompound_t(t1)&&iscompound_t(t2)&&
+      unify1(hd[t1],hd[t2])&&unify1(tl[t1],tl[t2]))return(1);
+  type_error("unify","with",t1,t2);
+  return(0);
+}
+
+unify1(t1,t2) /* inner call - exactly like unify, except error reporting is
+                 done only by top level, see above */
+         /* we do this to avoid printing inner parts of types */
+word t1,t2;
+{ t1=subst(t1),t2=subst(t2);
+  if(t1==t2)return(1);
+  if(isvar_t(t1)&&!occurs(t1,t2))
+  { addsubst(t1,t2); return(1); }
+  if(isvar_t(t2)&&!occurs(t2,t1))
+  { addsubst(t2,t1); return(1); }
+  if(iscompound_t(t1)&&iscompound_t(t2))
+  return(unify1(hd[t1],hd[t2])&&unify1(tl[t1],tl[t2]));
+  return(0);
+}
+
+subsumes(t1,t2) /* like unify but lop-sided; returns 1,0 as t2 falls, doesnt
+		   fall under t1 */
+word t1,t2;
+{ if(t2==wrong_t)return(1);
+  /* special case, shows up only when compiling prelude (changetype etc) */
+  return(subsu1(t1,t2,t2)); }
+
+subsu1(t1,t2,T2)
+word t1,t2,T2;
+{ t1=subst(t1);
+  if(t1==t2)return(1);
+  if(isvar_t(t1)&&!occurs(t1,T2))
+    { addsubst(t1,t2); return(1); }
+  if(iscompound_t(t1)&&iscompound_t(t2))
+    return(subsu1(hd[t1],hd[t2],T2)&&subsu1(tl[t1],tl[t2],T2));
+  return(0);
+}
+
+walktype(t,f)  /* make a copy of t with f applied to its variables */
+word t;
+word (*f)();
+{ if(isvar_t(t))return((*f)(t));
+  if(iscompound_t(t))
+  { word h1=walktype(hd[t],f);
+    word t1=walktype(tl[t],f);
+    return(h1==hd[t]&&t1==tl[t]?t:ap(h1,t1)); }
+  return(t);
+}
+
+occurs(tv,t)  /* does tv occur in type t? */
+word tv,t;
+{ while(iscompound_t(t))
+  { if(occurs(tv,tl[t]))return(1);
+    t=hd[t]; }
+  return(tv==t);
+}
+
+ispoly(t) /* does t contain tvars? (should call subst first) */
+word t;
+{ while(iscompound_t(t))
+  { if(ispoly(tl[t]))return(1);
+    t=hd[t]; }
+  return(isvar_t(t));
+}
+
+word SUBST[hashsize];  /* hash table of substitutions */
+
+clear_SUBST()
+/* To save time and space we call this after a type inference to clear  out
+   substitutions in extinct variables.  Calling this too often can slow you
+   down - whence #define reset_SUBST, see above */
+{ word i;
+  fixshows();
+  for(i=0;i<hashsize;i++)SUBST[i]=0;
+  /*printf("tvcount=%d\n",tvcount);  /* probe */
+  tvcount=1;
+  return(0);  /* see defn of reset_SUBST */
+}
+/* doubling hashsize from 512 to 1024  speeded  typecheck  by  only  3%  on
+   parser.m (=350 line block, used c. 5000 tvars) - may be worth increasing
+   for very large programs however.  Guesstimate -  further  increase  from 
+   512 would be worthwhile on blocks>2000 lines */
+
+fixshows()
+{ while(showchain!=NIL)
+       { tl[hd[showchain]]=subst(tl[hd[showchain]]);
+         showchain=tl[showchain]; }
+}
+
+lookup(tv)  /* find current substitution for type variable */
+word tv;
+{ word h=SUBST[hashval(tv)];
+  while(h)
+  { if(eqtvar(hd[hd[h]],tv))return(tl[hd[h]]);
+    h=tl[h]; }
+  return(tv);  /* no substitution found, so answer is self */
+}
+
+addsubst(tv,t) /* add new substitution to SUBST */
+word tv,t;
+{ word h=hashval(tv);
+  SUBST[h]=cons(cons(tv,t),SUBST[h]);
+}
+
+ult(tv)  /* fully substituted out value of a type var */
+word tv;
+{ word s=lookup(tv);
+  return(s==tv?tv:subst(s));
+}
+
+subst(t) /* returns fully substituted out value of type expression */
+word t;
+{ return(walktype(t,ult));
+}
+
+word localtvmap=NIL;
+word NGT=0;
+
+lmap(tv)
+word tv;
+{ word l;
+  if(non_generic(tv))return(tv);
+  for(l=localtvmap;l!=NIL;l=tl[l])
+     if(hd[hd[l]]==tv)return(tl[hd[l]]);
+  localtvmap=cons(cons(tv,l=NTV),localtvmap);
+  return(l);
+}
+
+linst(t,ngt) /* local instantiate */
+word t;   /* relevant tvars are those not in ngt */
+{ localtvmap=NIL; NGT=ngt;
+  return(walktype(t,lmap));
+}
+
+non_generic(tv)
+word tv;
+{ word x;
+  for(x=NGT;x!=NIL;x=tl[x])
+     if(occurs(tv,subst(hd[x])))return(1);
+  return(0);
+} /* note that when a non-generic tvar is unified against a texp, all tvars
+     in texp become non-generic; this is catered for by call to subst above
+     (obviating the need for unify to directly side-effect NGT) */
+
+word tvmap=NIL;
+
+mapup(tv)
+word tv;
+{ word *m= &tvmap;
+  tv=gettvar(tv);
+  while(--tv)m= &tl[*m];
+  if(*m==NIL)*m=cons(NTV,NIL);
+  return(hd[*m]);
+}
+
+instantiate(t) /* make a copy of t with a new set of type variables */
+word t;  /* t MUST be in reduced form - see redtvars */
+{ tvmap=NIL;
+  return(walktype(t,mapup));
+}
+
+ap_subst(t,args) /* similar, but with a list of substitions for the type
+               variables provided (args).  Again, t must be in reduced form */
+word t,args;
+{ word r;
+  tvmap=args;
+  r=walktype(t,mapup);
+  tvmap=NIL; /* ready for next use */
+  return(r);
+}
+
+
+mapdown(tv)
+word tv;
+{ word *m= &tvmap;
+  word i=1;
+  while(*m!=NIL&&!eqtvar(hd[*m],tv))m= &tl[*m],i++;
+  if(*m==NIL)*m=cons(tv,NIL);
+  return(mktvar(i));
+}
+
+redtvars(t) /* renames the variables in t, in order of appearance to walktype,
+	       using the numbers 1,2,3... */
+word t;
+{ tvmap=NIL;
+  return(walktype(t,mapdown));
+}
+
+
+remove1(e,ss) /* destructively remove e from set with address ss, returning
+                 1 if e was present, 0 otherwise */
+word e,*ss;
+{ while(*ss!=NIL&&hd[*ss]<e)ss= &tl[*ss]; /* we assume set in address order */
+  if(*ss==NIL||hd[*ss]!=e)return(0);
+  *ss=tl[*ss];
+  return(1);
+}
+
+setdiff(s1,s2) /* destructive on s1, returns set difference */
+word s1,s2; /* both are in ascending address order */
+{ word *ss1= &s1;
+  while(*ss1!=NIL&&s2!=NIL)
+       if(hd[*ss1]==hd[s2])*ss1=tl[*ss1]; else  /* removes element */
+       if(hd[*ss1]<hd[s2])ss1= &tl[*ss1];
+       else s2=tl[s2];
+  return(s1);
+}
+
+add1(e,s) /* inserts e destructively into set s, kept in ascending address
+             order */
+word e,s;
+{ word s1=s;
+  if(s==NIL||e<hd[s])return(cons(e,s));
+  if(e==hd[s])return(s); /* no duplicates! */
+  while(tl[s1]!=NIL&&e>hd[tl[s1]])s1=tl[s1];
+  if(tl[s1]==NIL)tl[s1]=cons(e,NIL);else
+  if(e!=hd[tl[s1]])tl[s1]=cons(e,tl[s1]);
+  return(s);
+}
+
+word NEW; /* nasty hack, see rules */
+
+newadd1(e,s)  /* as above, but with side-effect on NEW */
+word e,s;
+{ word s1=s;
+  NEW=1;
+  if(s==NIL||e<hd[s])return(cons(e,s));
+  if(e==hd[s]){ NEW=0; return(s); } /* no duplicates! */
+  while(tl[s1]!=NIL&&e>hd[tl[s1]])s1=tl[s1];
+  if(tl[s1]==NIL)tl[s1]=cons(e,NIL);else
+  if(e!=hd[tl[s1]])tl[s1]=cons(e,tl[s1]);
+  else NEW=0;
+  return(s);
+}
+
+UNION(s1,s2) /* destructive on s1; s1, s2 both in address order */
+word s1,s2;
+{ word *ss= &s1;
+  while(*ss!=NIL&&s2!=NIL)
+       if(hd[*ss]==hd[s2])ss= &tl[*ss],s2=tl[s2]; else
+       if(hd[*ss]<hd[s2])ss= &tl[*ss];
+       else *ss=cons(hd[s2],*ss),ss= &tl[*ss],s2=tl[s2];
+  if(*ss==NIL)
+    while(s2!=NIL)*ss=cons(hd[s2],*ss),ss= &tl[*ss],s2=tl[s2];
+    /* must copy tail of s2, in case of later destructive operations on s1 */
+  return(s1);
+}
+
+intersection(s1,s2)  /* s1, s2 and result all in address order */
+word s1,s2;
+{ word r=NIL;
+  while(s1!=NIL&&s2!=NIL)
+       if(hd[s1]==hd[s2])r=cons(hd[s1],r),s1=tl[s1],s2=tl[s2]; else
+       if(hd[s1]<hd[s2])s1=tl[s1];
+       else s2=tl[s2];
+  return(reverse(r));
+}
+
+deps(x) /* returns list of the free identifiers in expression x */
+word x;
+{ word d=NIL;
+L:switch(tag[x])
+{ case AP:
+  case TCONS:
+  case PAIR:
+  case CONS: d=UNION(d,deps(hd[x]));
+	     x=tl[x];
+	     goto L;
+  case ID: return(isconstructor(x)?d:add1(x,d));
+  case LAMBDA: /* d=UNION(d,patdeps(hd[x])); 
+	       /* should add this - see sahbug3.m */
+	       return(rembvars(UNION(d,deps(tl[x])),hd[x]));
+  case LET: d=rembvars(UNION(d,deps(tl[x])),dlhs(hd[x]));
+            return(UNION(d,deps(dval(hd[x]))));
+  case LETREC: { word y;
+		 d=UNION(d,deps(tl[x]));
+		 for(y=hd[x];y!=NIL;y=tl[y])
+		    d=UNION(d,deps(dval(hd[y])));
+		 for(y=hd[x];y!=NIL;y=tl[y])
+		    d=rembvars(d,dlhs(hd[y]));
+		 return(d); }
+  case LEXER: while(x!=NIL)
+                   d=UNION(d,deps(tl[tl[hd[x]]])),
+                   x=tl[x];
+              return(d);
+  case TRIES:
+  case LABEL: x=tl[x]; goto L;
+  case SHARE: x=hd[x]; goto L;  /* repeated analysis - fix later */
+  default: return(d);
+}}
+
+rembvars(x,p) /* x is list of ids in address order, remove bv's of pattern p
+                 (destructive on x) */
+word x,p;
+{ L:
+  switch(tag[p])
+  { case ID: return(remove1(p,&x),x);
+    case CONS: if(hd[p]==CONST)return(x);
+               x=rembvars(x,hd[p]);p=tl[p];goto L;
+    case AP: if(tag[hd[p]]==AP&&hd[hd[p]]==PLUS)
+               p=tl[p];  /* for n+k patterns */
+             else { x=rembvars(x,hd[p]);p=tl[p]; }
+	     goto L;
+    case PAIR:
+    case TCONS: x=rembvars(x,hd[p]);p=tl[p];goto L;
+    default: fprintf(stderr, "impossible event in rembvars\n");
+	     return(x);
+}}
+
+member(s,x)
+word s,x;
+{ while(s!=NIL&&x!=hd[s])s=tl[s];
+  return(s!=NIL);
+}
+
+printgraph(title,g) /* for debugging info */
+char *title;
+word g;
+{ printf("%s\n",title);
+  while(g!=NIL)
+  { printelement(hd[hd[g]]); putchar(':');
+    printelement(tl[hd[g]]); printf(";\n");
+    g=tl[g]; }
+}
+
+printelement(x)
+word x;
+{ if(tag[x]!=CONS){ out(stdout,x); return; }
+  putchar('(');
+  while(x!=NIL)
+    { out(stdout,hd[x]);
+      x=tl[x];
+      if(x!=NIL)putchar(' '); }
+  putchar(')');
+}
+
+printlist(title,l) /* for debugging */
+char *title;
+word l;
+{ printf("%s",title);
+  while(l!=NIL)
+  { printelement(hd[l]);
+    l=tl[l];
+    if(l!=NIL)putchar(','); }
+  printf(";\n");
+}
+
+printob(title,x) /* for debugging */
+char *title;
+word x;
+{ printf("%s",title); out(stdout,x); putchar('\n');
+  return(x); }
+
+print2obs(title,title2,x,y) /* for debugging */
+char *title,*title2;
+word x,y;
+{ printf("%s",title); out(stdout,x); printf("%s",title2); out(stdout,y); putchar('\n');
+}
+
+word allchars=0; /* flag used by tail */
+
+out_formal1(f,x)
+FILE *f;
+word x;
+{ extern word nill;
+  if(hd[x]==CONST)x=tl[x];
+  if(x==NIL)fprintf(f,"[]"); else
+  if(tag[x]==CONS&&tail(x)==NIL)
+    if(allchars)
+      { fprintf(f,"\"");while(x!=NIL)fprintf(f,"%s",charname(hd[x])),x=tl[x];
+	fprintf(f,"\""); } else
+    { fprintf(f,"[");
+      while(x!=nill&&x!=NIL)
+	   { out_pattern(f,hd[x]);
+	     x=tl[x];
+	     if(x!=nill&&x!=NIL)fprintf(f,","); }
+      fprintf(f,"]"); } else
+  if(tag[x]==AP||tag[x]==CONS)
+    { fprintf(f,"("); out_pattern(f,x);
+      fprintf(f,")"); } else
+  if(tag[x]==TCONS||tag[x]==PAIR)
+    { fprintf(f,"(");
+      while(tag[x]==TCONS)
+	   { out_pattern(f,hd[x]);
+	     x=tl[x]; fprintf(f,","); }
+      out_pattern(f,hd[x]); fprintf(f,","); out_pattern(f,tl[x]); 
+      fprintf(f,")"); } else
+  if(tag[x]==INT&&neg(x)||tag[x]==DOUBLE&&get_dbl(x)<0)
+    { fprintf(f,"("); out(f,x); fprintf(f,")"); } /* -ve numbers */
+  else
+  out(f,x);  /* all other cases */
+}
+
+out_pattern(f,x)
+FILE *f;
+word x;
+{ if(tag[x]==CONS)
+    if(hd[x]==CONST&&(tag[tl[x]]==INT||tag[tl[x]]==DOUBLE))out(f,tl[x]); else
+    if(hd[x]!=CONST&&tail(x)!=NIL)
+    { out_formal(f,hd[x]); fprintf(f,":"); out_pattern(f,tl[x]); }
+    else out_formal(f,x);
+  else out_formal(f,x);
+}
+
+out_formal(f,x)
+FILE *f;
+word x;
+{ if(tag[x]!=AP)
+    out_formal1(f,x); else
+  if(tag[hd[x]]==AP&&hd[hd[x]]==PLUS) /* n+k pattern */
+    { out_formal(f,tl[x]); fprintf(f,"+"); out(f,tl[hd[x]]); }
+  else
+    { out_formal(f,hd[x]); fprintf(f," "); out_formal1(f,tl[x]); }
+}
+
+tail(x)
+word x;
+{ allchars=1;
+  while(tag[x]==CONS)allchars&=(is_char(hd[x])),x=tl[x];
+  return(x);
+}
+
+out_type(t) /* for printing external representation of types */
+word t;
+{ while(isarrow_t(t))
+  { out_type1(tl[hd[t]]);
+    printf("->");
+    t=tl[t]; }
+  out_type1(t);
+}
+
+out_type1(t)
+word t;
+{ if(iscompound_t(t)&&!iscomma_t(t)&&!islist_t(t)&&!isarrow_t(t))
+    { out_type1(hd[t]);
+      putchar(' ');
+      t=tl[t]; }
+  out_type2(t);
+}
+
+out_type2(t)
+word t;
+{ if(islist_t(t))
+    { putchar('[');
+      out_type(tl[t]); /* could be out_typel, but absence of parentheses
+			   might be confusing */
+      putchar(']'); }else
+  if(iscompound_t(t))
+    { putchar('(');
+      out_typel(t);
+      if(iscomma_t(t)&&tl[t]==void_t)putchar(',');
+    /* type of a one-tuple -- an anomaly that should never occur */
+      putchar(')'); }else
+  switch(t)
+  {
+  case bool_t: printf("bool"); return;
+  case num_t: printf("num"); return;
+  case char_t: printf("char"); return;
+  case wrong_t: printf("WRONG"); return;
+  case undef_t: printf("UNKNOWN"); return;
+  case void_t: printf("()"); return;
+  case type_t: printf("type"); return;
+  default: if(tag[t]==ID)printf("%s",get_id(t));else
+	   if(isvar_t(t))
+	   { word n=gettvar(t);
+	   /*if(1)printf("t%d",n-1); else /* experiment, suppressed */
+	   /*if(n<=26)putchar('a'+n-1); else /* experiment */
+	     if(n>0&&n<7)while(n--)putchar('*'); /* 6 stars max */
+	     else printf("%d",n); }else
+           if(tag[t]==STRCONS)     /* pname - see hack in privatise */
+	     { extern char *current_script;
+	       if(tag[pn_val(t)]==ID)printf("%s",get_id(pn_val(t))); else
+	       /* ?? one level of indirection sometimes present */
+	       if(strcmp((char *)hd[tl[t_info(t)]],current_script)==0)
+		  printf("%s",(char *)hd[hd[t_info(t)]]); else /* elision */
+	       printf("`%s@%s'",
+		  (char *)hd[hd[t_info(t)]], /* original typename */
+		  (char *)hd[tl[t_info(t)]]); /* sourcefile */ }
+	   else printf("<BADLY FORMED TYPE:%d,%d,%d>",tag[t],hd[t],tl[t]);
+  }
+}
+
+out_typel(t)
+word t;
+{ while(iscomma_t(t))
+  { out_type(tl[hd[t]]);
+    t=tl[t];
+    if(iscomma_t(t))putchar(',');
+    else if(t!=void_t)printf("<>"); } /* "tuple-cons", shouldn't occur free */
+  if(t==void_t)return;
+  out_type(t);
+}
+
+/* end of MIRANDA TYPECHECKER  */
+