diff options
Diffstat (limited to 'types.c')
| -rw-r--r-- | types.c | 1674 |
1 files changed, 1674 insertions, 0 deletions
@@ -0,0 +1,1674 @@ +/* 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. * + * * + * Revised to C11 standard and made 64bit compatible, January 2020 * + *------------------------------------------------------------------------*/ + +#include "data.h" +#include "lex.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 */ + +static void abstr_check(word); +static void abstr_mcheck(word); +static void addsubst(word,word); +static word ap_subst(word,word); +static void checkfbs(void); +static int clear_SUBST(void); +static void comp_deps(word); +static word conforms(word,word,word,word); +static word cyclic_abstr(word); +static word etype(word,word,word); +static word fix_type(word); +static void fixshows(void); +static void genbnft(void); +static void infer_type(word); +static word linst(word,word); +static void locate_inc(void); +static void mcheckfbs(void); +static word meta_tcheck(word); +static int non_generic(word); +static int occurs(word,word); +static void out_formal(FILE*,word); +static void out_formal1(FILE*,word); +static void out_type1(word); +static void out_type2(word); +static void out_typel(word); +static void printelement(word); +static void redtfr(word); +static word rembvars(word,word); +static word remove1(word,word*); +static word rep_t(word,word); +static void sterilise(word); +static word subst(word); +static word subsu1(word,word,word); +static word tail(word); +static void txchange(word,word); +static void type_error(char*,char*,word,word); +static void type_error1(word); +static void type_error2(word); +static void type_error3(word); +static void type_error4(word); +static void type_error5(word); +static void type_error6(word,word,word); +static void type_error7(word,word); +static void type_error8(word,word); +static word ult(word); +static int unify(word,word); +static int unify1(word,word); + +void 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? */ + +void 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); +} + +word 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)); +} + +word 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; + +word 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 %ld)\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 */ + +void 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) + +void 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; + +void 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 */ + +void 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]]); +} + +void 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; +} + +word fix_type(t) /* substitute out any indirected typenames in t */ +word t; +{ switch(tag[t]) + { case AP: + case CONS: tl[t]=fix_type(tl[t]); + hd[t]=fix_type(hd[t]); + default: return(t); + case STRCONS: while(tag[pn_val(t)]!=CONS)t=pn_val(t);/*at most twice*/ + return(t); + } +} + +void locate_inc() +{ if(lasthereinc==hereinc)return; + printf("incorrect %%include directive "); + sayhere(lasthereinc=hereinc,1); +} + +void 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]; + } +} + +void 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; +} + +word 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); +} + +void 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]; } +} + +void report_type(x) +word x; +{ printf("%s",get_id(x)); + if(id_type(x)==type_t) + if(t_arity(x)>5)printf("(arity %ld)",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)); +} + +void report_types(header,x) +char *header; +word x; +{ printf("%s",header); + while(x!=NIL) + report_type(hd[x]),putchar(';'),x=tl[x]; + putchar('\n'); +} + +word 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)); +} + +word 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); +} + +word rep_t(T,L) /* see above */ +word T,L; +{ word t=rep_t1(T,L); + return(t==T?t:redtvars(t)); +} + +word 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); +} + +word 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; + +void 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 */ + +word genlstat_t() /* type of %lex state */ +{ return(pair_t(num_t,num_t)); } + +void 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; + +void 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 */ + +word 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); + } +} + +word 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 */ + +word 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); +}} + +void 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 */ + +void 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 %3ld 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; } +} + +void 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'); +} + +void type_error1(x) /* typename in expression */ +word x; +{ locate("type error"); + printf("typename used as identifier (%s)\n",get_id(x)); +} + +void 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)); +} + +void 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)); +} + +void 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"); +} + +void 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); +} + +void 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'); +} + +void type_error7(a,b) +word a,b; +{ locate("type error"); + printf("\nrhs of lex rule :: "); + out_type(redtvars(subst(b))); + printf("\n type expected :: "); + out_type(redtvars(subst(a))); + putchar('\n'); +} + +/* void type_error7(t,args) +word t,args; +{ int 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"); +} */ + +void 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'); +} + +int 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); +} + +int 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); +} + +word 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)); } + +word 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); +} + +word 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); +} + +int 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); +} + +int 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 */ + +int 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 */ + +void fixshows() +{ while(showchain!=NIL) + { tl[hd[showchain]]=subst(tl[hd[showchain]]); + showchain=tl[showchain]; } +} + +word 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 */ +} + +void addsubst(tv,t) /* add new substitution to SUBST */ +word tv,t; +{ word h=hashval(tv); + SUBST[h]=cons(cons(tv,t),SUBST[h]); +} + +word ult(tv) /* fully substituted out value of a type var */ +word tv; +{ word s=lookup(tv); + return(s==tv?tv:subst(s)); +} + +word subst(t) /* returns fully substituted out value of type expression */ +word t; +{ return(walktype(t,ult)); +} + +word localtvmap=NIL; +word NGT=0; + +word 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); +} + +word linst(t,ngt) /* local instantiate */ +word t,ngt; /* relevant tvars are those not in ngt */ +{ localtvmap=NIL; NGT=ngt; + return(walktype(t,lmap)); +} + +int 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; + +word 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]); +} + +word 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)); +} + +word 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); +} + + +word 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)); +} + +word 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)); +} + + +word 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); +} + +word 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); +} + +word 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 */ + +word 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); +} + +word 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); +} + +word 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)); +} + +word 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); +}} + +word 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); +}} + +word member(s,x) +word s,x; +{ while(s!=NIL&&x!=hd[s])s=tl[s]; + return(s!=NIL); +} + +void 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]; } +} + +void 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(')'); +} + +void 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"); +} + +word printob(title,x) /* for debugging */ +char *title; +word x; +{ printf("%s",title); out(stdout,x); putchar('\n'); + return(x); } + +void 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 */ + +void 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 */ +} + +void 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); +} + +void 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]); } +} + +word tail(x) +word x; +{ allchars=1; + while(tag[x]==CONS)allchars&=(is_char(hd[x])),x=tl[x]; + return(x); +} + +void 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); +} + +void 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); +} + +void 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("%ld",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,%ld,%ld>",tag[t],hd[t],tl[t]); + } +} + +void 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 */ + |