/****
 *
 * Type check RSL parse trees.  This file was derived from a type checker for
 * the Modula-2 programming language.  As such, it contains references to the
 * way types are represented and checked in Modula-2, which is not necessarily
 * the best way to type check RSL.  A full rewrite of the type checker would be
 * nice, but there are other more pressing matters at the moment.
 *
 */

#include <stdlib.h>
#include "std-macros.h"
#include "parse-tree.h"
#include "parser.h"
#include "tokens.h"
#include "sym.h"
#include "sym-aux.h"
#include "type.h"
#include "interp.h"
#include "type-preds.h"
#include "parser-aux.h"
#include "list.h"
#include "typechk.hP"
#include "where.h"
#include "options.h"
#include "validate.h"
#include "token-mapping.h"


/*
 * Top-level spec check is a recursive descent of the parse tree for each
 * module.  Per the strategy outlined in translator.c, all spec modules have
 * been parsed, including initial symtab construction, before any type checking
 * happens.  This facilitates forward and recursive reference to named
 * entities.
 */
bool chkSpec()
{
    SymtabEntry *e;
    Symtab *Tab;
    int i;
    bool chk = true;
    bool chk1 = false;
    void chkSpecModule(Symtab *tab);


    /*
     * Pass 1.5.  See comments for chkModule1_5 function and in body of
     * chkModule2 regarding when chkExports needs to be called.  Note that
     * check of Main module, in MainSymtab, does not start until pass 2.
     */
    MoveToSymtab(Level0Symtab);
    for (Tab = (Symtab *) EnumCppList(ModuleList); Tab;
				Tab = (Symtab *) EnumCppList(ModuleList)) {
	MoveToSymtab(Tab);
	chkModule1_5(CurSymtab->Tree, Level0Symtab->Offset);
	Level0Symtab->Offset = CurStaticOffset;
    }

    /*
     * Pass 2.  See "interesting note" re. passes in comment above
     * chkObjParents.
     */
    MoveToSymtab(MainSymtab);
    exportAllFromMain();
    chkModule2(CurSymtab->Tree, Level0Symtab->Offset);
    MoveToSymtab(Level0Symtab);
    for (Tab = (Symtab *) EnumCppList(ModuleList); Tab;
				Tab = (Symtab *) EnumCppList(ModuleList)) {
	MoveToSymtab(Tab);
	chkModule2(CurSymtab->Tree, Level0Symtab->Offset);
	Level0Symtab->Offset = CurStaticOffset;
    }

    /*
     * Pass 3.  See comment above chkModule function for details of processing
     * performed in this pass.
     */
    MoveToSymtab(MainSymtab);
    chk = chk and chkModule(CurSymtab->Tree, Level0Symtab->Offset);
    MoveToSymtab(Level0Symtab);
    for (Tab = (Symtab *) EnumCppList(ModuleList); Tab;
				Tab = (Symtab *) EnumCppList(ModuleList)) {
	MoveToSymtab(Tab);
	chk1 = chkModule(CurSymtab->Tree, Level0Symtab->Offset);
	chk &= chk1;
	Level0Symtab->Offset = CurStaticOffset;
    }

    /*
     *
     * IMPORTANT UPDATE, 22apr09: This should not be done in a pre-execution
     * pass, because it leads to the counter-intuitive behavior that all values
     * happen before any executable expressions.  So instead, the interp should
     * treat a val decl as an executable expr, the action of which is what now
     * happens initModule.
     *
     * OLD COMMENT FOLLOWS.
     * Pass 4.  Having successfully resolved all type issues, make a final pass
     * to evaluate the exprs for values and initialized variables.  This is
     * done strictly in lexical order, so any dependencies are resolved in that
     * way.  Also, this pass is performed only for modules with an error count
     * of zero.
     */
    InitInterp(null);
    MoveToSymtab(MainSymtab);
    if (CurSymtab->Errors == 0) {
	chk = chk and initModule(CurSymtab->Tree);
    }
    MoveToSymtab(Level0Symtab);
    for (Tab = (Symtab *) EnumCppList(ModuleList); Tab;
				Tab = (Symtab *) EnumCppList(ModuleList)) {
	MoveToSymtab(Tab);
	if (CurSymtab->Errors == 0) {
	    chk1 = initModule(CurSymtab->Tree);
	}
	chk &= chk1;
    }

    return chk;
}

/*
 * Check the contents of a spec module body of the form:
 *
 *	entity spec list ;
 *	formal part ;
 *
 * either one or both of which may be empty.  Since nested modules are not
 * allowed, no recursing will happen.
 *
 */
void chkSpecBody(
    nodep t,
    int Offset)
{ 
    nodep n;
    void chkObj(nodep t);
    void chkOp(nodep t);

    /*
     * Cruise the parse tree entities list.
     */
    for (n=t->components.spec.entities;
		 n; n=n->components.decl.next) {

	/*
	 * As in chkSpecBody2, we must check here for a nested module, which we
	 * ignore at this point.  Since all modules, including nested ones, are
	 * entered on the global check list, they will be checked at a higher
	 * level than this, and so we can ignore them here.  This is rather
	 * kludgy, and should be fixed in the rewrite.
	 */
	if (n->header.kind != MODULE_NODE) {
	    switch (n->header.name) {
		case YOBJ:
		    if (PrintProgressOn()) {
			fprintf(stderr, "  Checking object %s\n",
			    n->components.decl.kind.obj.name->
				    components.atom.val.text);
		    }
		    chkObj(n);
		    break;
		case YOP:
		    if (PrintProgressOn()) {
			fprintf(stderr, "  Checking operation %s\n",
			    n->components.decl.kind.op.name->
				    components.atom.val.text);
		    }
		    chkOp(n);
		    break;
		case YAX:
		    if (PrintProgressOn()) {
			fprintf(stderr, "  Checking axiom, line %d\n",
			    n->header.loc.line);
		    }
		    chkAxOrThm(n, "axiom");
		    break;
		case YTHM:
		    if (PrintProgressOn()) {
			fprintf(stderr, "  Checking theorem, line %d\n",
			    n->header.loc.line);
		    }
		    chkAxOrThm(n, "theorem");
		    break;
		case YVAR:
		    if (PrintProgressOn()) {
			fprintf(stderr, "  Checking var decl, line %d\n",
			    n->header.loc.line);
		    }
		    chkFormalVarDecl(n);
		    break;
		case '>':
		    if (PrintProgressOn()) {
			fprintf(stderr, "  Checking top-level expr, line %d\n",
			    n->header.loc.line);
		    }
		    chkExpr(n->components.decl.kind.expr, true, null);
		    break;
	    }
	}
    }
}


/*
 * Type check a module, Pass 1.5.  This entails:
 *
 *     * initializing the module error counter
 *     * export checking 
 *
 * This pass is called "1.5" instead of 2, since it's only performed at the
 * module level, not on any of the definitions within the modules.  The other
 * full passes do descend into the modules.
 *
 * The timing requirement for export checking is rather subtle.  In order to
 * have imports be exportable, we need to check exports first, at least insofar
 * as marking them as such.  But we can't do this as early as Pass 1 in
 * sym-aux.ExitModule, since this leads to "Export not found" errors where
 * there should not be.
 *
 * So, Pass 1 is too early for export checking, but Pass 2 is too late.  This
 * is because we need to complete export checking across all modules before we
 * can begin import checking.  Therefore, we do export checking in one full
 * pass accross all modules first, then do import checking in pass 2.
 *
 */
bool chkModule1_5(
    nodep t,
    int Offset)
{
    /*
     * Hmm.  The following was originally in pass 2, but I figured it should be
     * moved here, and not repeated in pass 2.  Hope this is OK.  If it is,
     * maybe I'll come back here and take out this comment.  If it's OK and I
     * don't take out this comment, consider it an intresting read.
     *
     * Set the module error counter for level 1 modules.  In this way, we sum
     * errors at the global module (compilation level), not individually at the
     * local module level.
     */
    if (CurSymtab->Level == 1)
	SetErrorCounter(&(CurSymtab->Errors));

    chkExports(t);
}


/*
 * Type check a module, Pass 2.  At present, this checking entails:
 *
 *	* import checking
 *	* inheritance resolution.
 *
 */
bool chkModule2(
    nodep t,
    int Offset)
{
    /*
     * NOTE: It's too late to call chkExports here, even if it's done before
     * chkImports, because in the case of multiple modules in multiple files,
     * in makes the import/export dependencies order-dependent on the files,
     * i.e., dependent on the order of the files in the compilation line.  To
     * avoid this problem, we now have export checking done in pass 1.5
     */
    chkImports(t->components.module.imports);

    /*
     * Type check the body parts.
     */ 
    if (t->header.name == YOBJ) {
	chkSpecBody2(t->components.module.body, Offset);
    }

    return not CurSymtab->Errors;
}


/*
 * Type check a module body, Pass 2.  See chkSpecModule2 for description of
 * what checks are performed in this pass.
 */
void chkSpecBody2(
    nodep t,
    int Offset)
{ 
    nodep n;
    SymtabEntry* sym;
    void chkObj(nodep t);
    void chkOp(nodep t);

    /*
     * Cruise the parse tree entities list.
     */
    for (n=t->components.spec.entities;
		 n; n=n->components.decl.next) {

	/*
	 * Since modules can be nested, we can arrive here with a MODULE_NODE,
	 * which has no inheritance to resolve.
	 */
	if (n->header.kind != MODULE_NODE) {
	    switch (n->header.name) {
		case YOBJ:
		    sym = n->components.decl.kind.obj.sym;

		    /*
		     * Sym will be null for rules, which we'll deal with at
		     * some later date.
		     */
		    if (not sym)
			break;

		    if (isRecord(sym->Type)) {
			sym->Type->components.type.size = 
			    sym->Type->components.type.kind.record.numfields;
		    }
		    ResolveObjInheritance(n, sym);
		    ProcessObjWhereClause(n, sym);
		    break;
		case YOP:
		    sym = n->components.decl.kind.op.sym;
		    ResolveOpInheritance(n, sym);
		    ProcessOpWhereClause(n, sym);
		    break;
	    }
	}
    }
}


/*
 * Peform the last past of module type checking.  This entails storage offset
 * computation and the complete checking of all expressions.  There is also
 * some secondary processing to help out the browser tool, by entering names in
 * a browser-friendly symbol table.
 */
bool chkModule(
    nodep t,
    int Offset)
{
    SymtabEntry *e;
    bool err = false;

    /*
     * Grab the symtab entry for the module.
     */
    e = CurSymtab->ParentEntry;

    /*
     * Help the browser out.
     */
    BrowserModuleEnter(e);

    /*
     * Init the modules's storage offset to the current static offset, which
     * was passed in as a parm.  In this way, all module vars, at any level,
     * will be alloc'd in a single static pool.  The reason we transfer
     * CurStaticOffset into the module's symtab is so offset alloc can be done
     * in a uniform manner for both modules and procs.  Viz., offset alloc will
     * always use CurSymtab->Offset in the computation, without having to check
     * whether a symbol is static or local.
     */
    CurSymtab->Offset = Offset;

    /*
     * Set the module error counter for level 1 modules.  In this way, we sum
     * errors at the global module (compilation level), not individually at the
     * local module level.
     *
     * NOTE: Now done in Pass 2.
     *
    if (CurSymtab->Level == 1)
	SetErrorCounter(&(CurSymtab->Errors));
     *
     */

    /*
     * If the command -v option was specified, print the name of each module as
     * it's checked.
     */
    if (PrintProgressOn()) {
	fprintf(stderr, "Checking module %s\n",
	    t->components.module.name->components.atom.val.text);
    }

    /*
     * NOTE: chkImports must be called in the 2nd pass, so they'll be ready for
     * inheritance resolution.
     *
    chkImports(t->components.module.imports);
     *
     */

    /*
     * NOTE: chkExports must be called in first pass, so they'll be ready for
     * importing in the type checking pass.
     *
    chkExports(t->components.module.exports);
     *
     */

    /*
     * Type check the body parts.
     */ 
    chkSpecBody(t->components.module.body, Offset);

    /*
     * 11nov00: Two problems here.  (1) There's only one message output for all
     * modules, which means for multiple modules, the module name is at best
     * misleading.  (2) I'm not sure this info is all that useful anyway.
     *
     * I don't know if problem (1) is a recent phenominon or I've just recently
     * noticed it.  At any rate, the problems warrant disabling this entire
     * message for now, if not forever.  We'll see how it goes.  Original
     * comment follows.
     *
     * Output a summary error count if any errors occurred.  Note that error
     * counters for local modules will always stay 0 due to code above.
     *
   if (CurSymtab->Errors) {
       	error("ERROR TOTAL IN MODULE %s IS %d\n\n",
	    e->Symbol, CurSymtab->Errors);
	err = true;
    }
     *
     */

    /*
     * Update global static offset counter.
     */
    CurStaticOffset = CurSymtab->Offset;

    return ((not err) and (CurSymtab->Errors == 0));
}

/*
 * Just pass the buck to initSpecBody.
 */
bool initModule(nodep t) {
    initSpecBody(t->components.module.body);
    return CurSymtab->Errors == 0;
}

/*
 * Execute all value and variable initialization exprs, and bind the values to
 * the names.  The traversal structure is the same chkSpecBody{,2}, but here we
 * only consider YVAR and YVAL decls.  See the comments in and around those
 * functions for descriptions of what's going on here.
 */
void initSpecBody(nodep t) {
    nodep n;
    SymtabEntry* sym;

    for (n=t->components.spec.entities;
	    n; n=n->components.decl.next) {

	if (n->header.kind != MODULE_NODE) {
	    switch (n->header.name) {
		case YOBJ:
		    /*
		     * Sym will be null for rules, which we'll deal with at
		     * some later date.
		     */
		    if (not sym)
			break;

		    sym = n->components.decl.kind.obj.sym;
		    if ChkSymFlag(sym, isDef) {
		        initVal(n->components.decl.kind.obj.parts, sym);
		    }
		    break;
		case YVAR:
		    /* TODO */
		    break;
	    }
	}
    }
}


/*
 * Initialize a value to its declared expr.  Pass 3 will have done the type
 * checking, and set sym->Type to a non-null TypeStruct if checking succeeds.
 */
void initVal(nodep t, SymtabEntry* sym) {
    ValueStruct v;

    /*
     * Start things off with a negative outcome.
     */
    sym->Info.Obj.val = null;

    /*
     * If the type checked, interp the value and put it in the symtab.  Also,
     * and the value to the universe of the value type, if the type as
     * explicitly declared, or inferred as a ident type during type checking.
     */
    if (sym->Type) {
      if (not setjmp(RuntimeError)) {
	if (v = interpExpr(t, false, null)) {
	    sym->Info.Obj.val = v;

	    if (isIdentType(sym->Type)) {
		UniverseAddValue1(sym->Type->
		    components.type.kind.ident.type->
			components.atom.val.text, v);
	    }
	}
      }
    }
}

/*
 * Check a decl list.
 */
bool chkDecls(
    nodep t)
{
    nodep d;
    int StartErrors = CurSymtab->Errors;

    for (d = t; d; d = d->components.decl.next) {
	switch (d->header.name) {
	    case 0:
		break;
	    case YCONST:
		chkConstDecl(d);
		break;
	    case YVAR:
		chkVarDecl(d);
		break;
	    case YMODULE:
		chkModuleDecl(d);
		break;
	}
    }

    return (StartErrors == CurSymtab->Errors);
}


/*
 * Check a stmt seq.
 */
bool chkStmts(
    nodep t)
{
    nodep s;
    int StartErrors = CurSymtab->Errors;

    for (s = t; s; s = s->components.stmt.next) {
	switch (s->header.name) {
	    case 0:
		break;
	    case YIF:
		chkIf(s);
		break;
	}
    }

    return (StartErrors == CurSymtab->Errors);
}

/*
 * Check the zero or more import decls.  Bail if there as any parse error to
 * this point.
 */
void chkImports(nodep t)
{ 
    if (PARSE_ERROR)
	return;

    /*
     * Stick the imports tree in the symtab for future pp purposes.
     */
    CurSymtab->Imports = t;

    /*
     * Cruise the imports list
     */
    for (; t; t = t->components.decl.next)
	chkImports1(t);
}

/*
 * Check an import decl of the form
 *
 *     IMPORT import-item-1 [, ..., import-item-n]
 *
 * where import-item-1 has one the following two forms
 *
 *     M1[. ... .Mn].X
 *     M1[. ... .Mn].* [except X1, ..., Xn]
 *
 * and items 2 through n can be present only with the first of these forms.
 * I.e., there can be multiple non-starred items, but only one starred item.
 *
 * In the items, Mi must be module names, X is the name of an export of the
 * rightmost module in the leading qualification chain, * specifies all
 * exports, and the optional except clause is a list of export names not to
 * import.  The except clause is valid only when the * is present, which
 * constraint is enforced syntactically.
 *
 * In all cases, the name X is entered in the importing symtab, but none of the
 * module names is entered, i.e., none of the Mi in the leading qualification
 * chain.  The local entry of X is only an idirect reference to the full
 * definition of X in the defining scope.  The local entry has the name "X", is
 * marked as an import, and the Chain field points to the original entry in the
 * defining scope.  All other symbol info is stored in the original entry.
 *
 * In the non-star case, if any of the Xi are overloaded names, the all of the
 * overloaded defs are exported.
 *
 * Whenever an imported name already exists in the importing scope, an "already
 * defined" error message is output.  From the user's perspective, such
 * messages can be avoided by: (1) adding the already-defined names to the
 * except list; (2) by individually importing only undefined names; or (3) by
 * having no import at all, and referencing all of a module's exports in
 * qualified form.
 */
void chkImports1(
    nodep t)
{
    nodep n;
    nodep found_node;	/* Found node returned from LookupQid */

    /*
     * If no imports, we're outta here.
     */
    if (not t)
	return;

    /*
     * Traverse the list of import items, processing each per the header
     * comment.
     */
    for (n=t->components.decl.kind.import.items;
	     n; n=n->components.atom.next2) {
	chkImportItem(n, t);
    }
}

/*
 * Check one import item, of the form
 *
 *     quaalident[.*]
 *
 * by checking the validity of the qualident, and if OK, entering the
 * appropriate names in current (importing) scope.  The full import decl is
 * sent in with the item, in order to access the isall and except fields.
 */
void chkImportItem(nodep item, nodep import) {
    SymtabEntry* sym, * e;
    Symtab* FromTab;
    int i;
    nodep qid = item;
    bool isall = import->components.decl.kind.import.isall;
    char* lead_name;
    nodep found_node;	/* Found node returned from LookupQid */
    nodep n;		/* Nodes in except list */

    /*
     * Require that the item has at least two components.  Note that we do this
     * first, before calling LookupQid.  In this way, we'll output what is
     * hopefully a more meaningful error message.
     */
    if ((qid->components.atom.next == null) and (not isall)) {
	lerror(item, "Imports must be of the form \"module.name\" or \"module.*\"\n");
	return;
    }

    /*
     * Get the lefmost name in the qualident.
     */
    lead_name = qid->components.atom.val.text;

    /*
     * Disallow self import, i.e., import M.X from inside module M.
     */
    if (streq(lead_name, CurSymtab->ParentEntry->Symbol)) {
	lerror(item, "Module %s cannot import from itself.\n", lead_name);
	return;
    }

    /*
     * In the isall case, confirm that the leftmost name is a module.  For the
     * non-isall case, this is done by LookupQid, which is called after this.
     */
    if (isall) {
	sym = Lookup(lead_name);
	if ((not sym) or (not (sym->Class == C_Module))) {
	    lerror(item,
		"%s is not defined as a module in the current scope.\n",
		lead_name);
	    return;
	}
    }

    /*
     * Call LookupQid to validate the qid.  This is possible courtesy of Pass
     * 1.5, wherein all module exports were marked as such.  Note that
     * LookupQid handles the case of a parent module name being shadowed by a
     * local object or operation.  
     */
    if (not (sym = LookupQid(qid, &found_node))) {
	return;
    }

    /* OLD CODE:
    if (f = t->components.decl.kind.import.from) {
	if (not (s = LookupIn(f->components.atom.val.text, FromTab))) {
	    lerror(f, "Module in from clause not found.\n");
	    return;
	}
        FromTab = s->Info.Module.Symtab;
	noFrom = false;
    }
     */

    /*
     * Bifurcate on whether the import is a '*' or single indent.
     */
    if (isall) {

	/*
	 * Grab the symtab of the exporting module.
	 */
	FromTab = sym->Info.Module.Symtab;

	/*
	 * Check that each name on the except list is in fact an export.
	 */
	for (n = import->components.decl.kind.import.except; n;
	        n = n->components.atom.next) {
	    if (not LookupInThisScope(n->components.atom.val.text, FromTab)) {
		lerror(n, "%s is not an export %s.\n",
		   n->components.atom.val.text, FromTab->ParentEntry->Symbol);
	    }
	}

	/*
	 * Traverse through all entries of exporting symtab, in decl order,
	 * checking the importability of each exported name.
	 */
	for (e = FromTab->DeclThread; e; e = e->DeclNext) {
	    if (ChkSymFlag(e, isExport)) {

		/*
		 * Check for addition unless on except list.
		 */
		if (not InIdentList(e->Symbol, 
			import->components.decl.kind.import.except)) {
		    chkImportName(e, item);
		}
	    }
	}
    }
    else {
	chkImportName(sym, found_node);

	/* OLD CODE:
	for (im = t->components.decl.kind.import.names; im;
		 im = im->components.atom.next) {
	    chkImportListItem(
		im->components.atom.val.text, noFrom, FromTab, im);
	}
	 */
    }
}
	
/*
 * Enter an imported name in the current (importing) symtab if the name is not
 * already there.  The entry is an indirect reference to the imported symbol's
 * entry in its defining module.
 */
void chkImportName(SymtabEntry* sym, nodep error_nodep) {
    char* name;
    SymtabEntry *sl;

    /*
     * Outta here if the sym is null for any reason.
     */
    if (sym == null) {
	return;
    }

    /*
     * Grab the import name.
     */
    name = sym->Symbol;

    /* OLD CODE:
     * Lookup the import name in the from scope.
    if (not (s = LookupIn(name, FromTab))) {
	lerror(error_nodep, "Import %s not found.\n", name);
	return;
    }
     */

    /* OLD CODE:
     * If an explicit from is given, confirm that the imported symbol was
     * exported and enter the symbol in the importing scope.
    if (not noFrom) {
	if (not ChkSymFlag(s, isExport)) {
	    lerror(error_nodep, "Import %s is not an export from %s.\n",
		s->Symbol, FromTab->ParentEntry->Symbol);
	    return;
	}
    }
     */

    /*
     * Lookup import in importing scope to confirm it's not already there.
     */
    if (LookupThisScope(name)) {
	lerror (error_nodep,
	    "Imported name %s is already defined in this scope.\n",
	       name);
	return;
    }

    /*
     * Enter from'd name into importing scope, marking it as an import.
     * The only thing that is entered is the name; all other symbol
     * info remains in the defining (from) scope.  Hence, the entry in
     * the importing scope is an indirect reference to the entry in the
     * defining scope.  See how sym-aux.c:Lookup handles this.
     */
    Enter(sl = AllocSymtabEntry(name, null, null, null));
    SetSymFlag(sl, isImport);
    sl->Chain = sym;

    /*
     * TODO: handle the case of exporting overloaded name.  Each name is
     * exported.
     */


}

/*
 * Check if the given ident is in the given ident list.  This would seeminly
 * be defined elsewhere as a general search function, but I don't see it
 * anywhere, so I guess I'll just define it here.  Whatever.
 */
bool InIdentList(char* ident, nodep list) {
    nodep i;

    for (i = list; i; i= i->components.atom.next) {
	if (streq(ident, i->components.atom.val.text)) {
	    return true;
	}
    }
    return false;
}

/*
 * As a special case, mark all global symbols, i.e., symbols in the Main
 * symtab, as exports.  This allows global symbols to be imported from main
 * into other top-level modules.  It's a convenience for specs that are not
 * fully modularized.
 */
void exportAllFromMain() {
    int i;
    SymtabEntry* e;
    for (i=0; i<CurSymtab->Size; i++) {
	for (e=CurSymtab->Entries[i]; e; e=e->Next) {
	    SetSymFlag(e, isExport);
	}
    }
}    


/*
 * Check exports.
 */
void chkExports(
    nodep t)		/* Full module decl tree. */
{
    nodep exs, ex, en;
    SymtabEntry *s, *sl, *e;
    bool q;
    char *n;
    int i;
    List* already_exported;

    if (PARSE_ERROR or (not t))
	return;

    /*
     * If we've got at least some exports, print out a message that the
     * checking is happening.  This message is a user-level nicety, since if
     * any error messages follow in the checking loop below, they'll come
     * before the main message loop.
     */
    if (PrintProgressOn()) {
       fprintf(stderr, "Checking module %s's exports (in advance of other checks).\n",
	   t->components.module.name->components.atom.val.text);
    }

    /*
     * Now do the actual checking
     */
    for (exs = t->components.module.exports; exs;
	    exs = exs->components.decl.next) {

	/*
	 * If we've got a '*', mark all syms as exports, except for the ones in
	 * the except list.
	 */
	if (exs->components.decl.kind.export_.isall) {
	    /*
	     * Check that each name on the except list is in fact an export.
	     */
	    for (en = exs->components.decl.kind.export_.except; en;
		    en = en->components.atom.next) {
		if (not LookupThisScope(en->components.atom.val.text)) {
		    lerror(en, "%s is not an export %s.\n",
		       en->components.atom.val.text,
		       CurSymtab->ParentEntry->Symbol);
		}
	    }

	    /*
	     * Do the export marking of all non-excepted names.  Note the
	     * subtlety of building the list of already exported names, then
	     * sorting it before error message output.  Without this sorting,
	     * error messages would come out in hash table order, which is not
	     * going to be repeatable for regression testing, not to mention
	     * looking stupid to the user.
	     *
	     * TODO: Implement SortList to finish things here.  In the
	     * meantime, the output of the "already exported" message is
	     * disabled for the '*' form of export.  This is not a semantic
	     * problem, since over-export is inert, however the error
	     * message(s) would be nice.
	     */
	    already_exported = NewList();
	    for (i=0; i<CurSymtab->Size; i++) {
		for (e=CurSymtab->Entries[i]; e; e=e->Next) {
		    if (not InIdentList(e->Symbol, 
			    exs->components.decl.kind.export_.except)) {
			if (ChkSymFlag(e, isExport)) {
			    PutList(already_exported, stralloc(e->Symbol));
			}
			else {
		            SetSymFlag(e, isExport);
			}
		    }
		}
	    }
	    /* As noted above, message output is disabled pending
	     * implementation of SortList */
	    DelList(already_exported);
	}
	else {
	    /*
	     * For each export, look it up in this scope only, and mark as
	     * export if found.  This means that a module can only export
	     * things it defines itself, not things in parent scopes, and not
	     * things it imports.  The use of includes is what makes exporting
	     * sub-modules tractable.  See the reference manual for details.
	     */
	    for (ex = exs->components.decl.kind.export_.names;
		     ex; ex = ex->components.atom.next) {
		/*
		 * Do the lookup.
		 */
		s = LookupThisScope(n = ex->components.atom.val.text);

		/*
		 * Error if not defined.
		 */
		if (not s) {
		    lerror(ex, "Export %s not defined in module %s.\n", n,
			CurSymtab->ParentEntry->Symbol);
		}
		else {
		    /*
		     * Mark symbol as an export, if it hasn't been already.
		     */
		    if (ChkSymFlag(s, isExport)) {
			lerror(exs, "%s has already been exported.\n",
			    s->Symbol);
		    }
		    else {
		        SetSymFlag(s, isExport);
		    }
		}
	    }
	}	
    }
}


/*
 * Check a block;
 */
void chkBlock(
    nodep t)
{
    chkDecls(t->components.block.decls);
    chkStmts(t->components.block.stmts);
}


/*
 * Check that an imple module is consistent with the corresponding def module.
 * This consistency entails checking that all definintions appearing in the def
 * module are identically declared in the imple module and have implmentations
 * in the imple module.
 *
 * If things all check out OK, then we need to link the vars and procs in the
 * two modules, so that things are all hunky dory.
 * 
 */
void chkImpleModule(
    nodep t)
{
    /* LATER */
}


/*
 * Check an expr.  Second arg = true of we're checking a non-constant expr,
 * false if constant expr.  Third arg is the target type we're looking for, as
 * the generalized (top-down) means to resolve co-arity overloads.
 */
TypeStruct chkExpr(
    nodep t,
    bool f,
    TypeStruct tt)
{
    TypeStruct rtn;

    if (not t)
	return null;

    /*
     * NOTE: The following check is too fine-grain for detecting circularity in
     * value declarartions.  It may be useful in some future circumstances, but
     * it does not work for value decls.
     *
     * Check for circular def, which only happens for values defined in terms
     * of other values.
     *
    if ((InTreeStack(t) and (IsValDecl(t)) {
	lerror(t, "Circularity detected in value declaration.");
	ClearTreeStack();
	return null;
    }
    PushTree(t);
     *
     */

    switch (t->header.kind) {
	case UNOP_NODE:
	case BINOP_NODE:
	case EXPR_NODE:
	    switch (t->header.name) {
		case '=':
		    rtn = chkEqOp(t, f);
		    break;
		case '#':
		    rtn = chkLenOp(t, f);
		    break;
		case '<':
		case '>':
		case YLEQ:
		case YGEQ:
		case YNEQ:
		    rtn = chkRelOp(t, f);
		    break;
		case '+':
		    rtn = chkPlusOp(t, f);
		    break;
		case '-':
		    rtn = chkMinusOp(t, f);
		    break;
		case '^':
		case '*':
		case '/':
		    rtn = chkMultOp(t, f);
		    break;
		case YDIV:
		case YMOD:
		    rtn = chkArithIntOp(t, f);
		    break;
/*		case '/':
		    rtn = chkArithRealOp(t, f);
		    break;
 */
		case YUNYPLUS:
		case YUNYMINUS:
		    rtn = chkUnaryArithOp(t, f);
		    break;
		case YOR:
		case YXOR:
		case YAND:
		case YIMPLIES:
		case YIFF:
		    rtn = chkBoolOp(t, f);
		    break;
		case YNOT:
		    rtn = chkNotOp(t, f);
		    break;
		case YIN:
		    rtn = chkInOp(t, f);
		    break;
		case '[':
		    rtn = chkArrayRef(t, f);
		    break;
		case '.':
		    rtn = chkRecordRef(t, f);
		    break;
		/*
		 * Spec lang only.
		 */
		case YISA:
		    rtn = chkUnionRef(t, f);
		    break;
		case YDOTDOT:
		    rtn = chkDotDotOp(t, f);
		    break;
		case ']':
		    rtn = chkListConstructor(t, f);
		    break;
		case '}':
		    rtn = chkTupleConstructor(t, f);
		    break;
		case YLET:
		    rtn = chkLet(t, f);
		    break;
		case YGETINSTANCE:
		    rtn = chkGetInstance(t, f);
		    break;
		case YCHKINSTANCE:
		    rtn = chkChkInstance(t, f);
		    break;
		case YATTRSELECT:
		    rtn = chkAttrSelect(t, f);
		    break;
		case YASSMNT:
		    rtn = chkAssmnt(t);
		    break;
	    }
	    break;

	/*
	 * Spec lang only.
	 */
	case TRINOP_NODE:
	    switch (t->header.name) {
		case YIF:
		    rtn = chkIfExpr(t, f);
		    break;
		case '[':
		    rtn = chkArraySliceRef(t, f);
		    break;
		case YLAMBDA:
		    rtn = chkLambda(t, f);
		    break;
		case YAEQ:
		    rtn = chkAlmostEqOp(t, f);
		    break;
	    }
	    break;

	/*
	 * Spec lang only.
	 */
	case DECL_NODE:
	    switch (t->header.name) {
		case YFORALL:
		case YEXISTS:
		    rtn = chkQuant(t, f);
		    break;
		case YLET:
		    rtn = chkLet(t, f);
		    break;
	    }
	    break;

	case PROC_CALL_NODE:
	    if (f) {
		if (t->header.name == null) {
		    rtn = chkProcCall(t, tt);
		    break;
	        }
		else {
		    rtn = chkValidationCall(t, tt);
		    break;
		}
	    }
	    else {
		/*
		 * 31mar09 glf: Eliminated this error message, thereby allowing
		 * function calls in const exprs.
		 *
		lerror(t, "Function calls not allowed in const expr.\n");
		return null;
		 */
	    }
	    break;

	case ATOM_NODE:
	    switch (t->header.name) {
		case Yident:
		    rtn = chkIdent(t, f);
		    break;
		case Yreal:
 		    rtn = BuildLiteralType(t);
//		    rtn = RealType;
		    break;
		case Yinteger:
		    rtn = BuildLiteralType(t);
//		    rtn = IntLitType;
		    break;
		case Ystring:
		    rtn = BuildLiteralType(t);
//		    rtn =
//			strlen(t->components.atom.val.string) == 1
//			    ? StringCharType : StringType;
		    break;
		case Ynil:
		    rtn = NilType;
		    break;
	    }
	    break;

	case EXPR_LIST_NODE:
	    rtn = chkExprSeq(t, f);
	    break;
    }

    /*
     * Matches disabled PushTree at top of function.
     *
    PopTree();
     *
     */

    return rtn;
}


/*
 * Check an expr sequence of the form
 *
 *    ( e1; e2; ...; en )
 *
 * by entering an anon scope for it, and type checking each ei.  Leave the
 * scope when done, returning the type of en.
 */
TypeStruct chkExprSeq(nodep t, bool f) {
    nodep el;
    TypeStruct t1;

    NewLevel(HashAllocSymtabEntry("An Expr Seq", C_ExprSeq, null,
	CurSymtab->Level + 1), 64, null, '(');


    /*
     * Check each expr in the list.
     */
    for (el=t; el; el=el->components.exprlist.next)
	t1 = chkExpr(el->components.exprlist.expr, f, null);

    /*
     * Store the symtab in the tree, so the interp can use it.
     */
    t->components.exprlist.symtab = CurSymtab;

    /*
     * Increment act rec size by 1 for Display save pointer.  See chkProcCall
     * comments for further discussion.
     */
    CurSymtab->Offset++;

    /*
     * Move back to parent scope.
     */
    LeaveLevel();


    /*
     * Return type of last expr in the list.
     */
    return t1;
}


/*
 * Check a const expr.  Just call chkExpr with 2nd arg = false.
 */
TypeStruct chkConstExpr(
    nodep t)
{
    return chkExpr(t, false, null);
}


/*
 * Check a type.
 */
TypeStruct chkType(
    nodep t)
{
    switch (t->header.name) {
	case 0:
	    return null;
	case Yident:
	    return chkIdentType(t);
	case '(':	/* enum */
	    return chkEnumType(t);
	case '[':	/* subrange */
	    return chkSubrangeType(t);
	case YARRAY:
	    return chkArrayType(t);
	case YRECORD:
	    return chkRecordType(t);
    }
}


/**
 ** Check the decls.
 **/

/*
 * Check a constant decl of the form:
 *
 *	CONST n1 = c1;
 *	       ...
 *	      nk = ck;
 *
 * by recursively type checking each of the constant exprs c1 through ck.
 * Also, evaluate each constant expr for later use.
 */
void chkConstDecl(
    nodep t)
{
    nodep cd, expr;
    SymtabEntry *ce;
    TypeStruct ct;

    /*
     * Loop through each decl.
     */
    for (cd = t; cd; cd = cd->components.decl.kind.consta.next) {
	/*
	 * Type check the const expr and store result as its type.
	 */
	(ce = Lookup(cd->components.decl.kind.consta.name->
		components.atom.val.text))->Type =
	    (ct = chkConstExpr(expr = cd->components.decl.kind.consta.expr));

	/*
	 * Eval const expr and store result as its value.
	 */
	if (ct)
	    ce->Info.Consta.val = interpExpr(expr);
    }
}


/*
 * Check a type decl of the form:
 *
 *	type namelist1 = t1;
 *	       ...
 *	     namelistk = tk;
 *
 * by recursively type checking t1 through tk.
 */
void chkTypeDecl(
    nodep t)
{
    nodep td;

    for (td = t; td; td = td->components.decl.kind.type.next)
	chkType(td->components.decl.kind.type.type);
}


/*
 * For Modula-2 -- deprecated.  See chkFormalVarDecl.
 */
void chkVarDecl(
    nodep t)
{
    nodep vd, v;
    TypeStruct vt, ct;
    SymtabEntry *s;

    /*
     * As noted in sym-aux.c:EnterVar, if the declared type is a type ident,
     * then it's already been checked with LookupType, so we dont need to check
     * it again here.
     */
    for (vd = t; vd; vd = vd->components.decl.kind.var.next) {
	if ((vt = vd->components.decl.kind.var.type) and
		(not ChkNodeFlag(vt, TypeChecked))) {
	    chkType(vt);
	}
	for (v = vd->components.decl.kind.var.vars; v;
		v = v->components.atom.next) {
	    s = Lookup(v->components.atom.val.text);
	    s->Info.Var.Offset = CurSymtab->Offset;
	    CurSymtab->Offset += TypeSize(s->Type);
	}
    }
}


/*
 * Check a proc decl of the form:
 *
 *	proc n(p1a,...,p1k: t1,..., pka,...,pkk: tk): tr;
 *	    <block>
 *
 * by entering the proc's scope and recursively type checking its block.
 *
 * Note that we dont need to do any checking of the formal parm types or the
 * return type.  Since formals and return type must be qualidents, they have no
 * structure to check, so the call to LookupType in the parser has already done
 * all the checking that's necessary.  We do need to call chkParmDecls in order
 * to compute parm offsets.
 */
void chkProcDecl(
    nodep t)
{
    SymtabEntry *p;

    /*
     * Type check the block recursively.  As with a module, we descend into the
     * proc's symtab.
     */    
    PushSymtab();
    MoveToSymtab(Lookup(t->components.decl.kind.proc.name->
			components.atom.val.text)->
			    Info.Proc.Symtab);
    /*
     * Note that we dont set error counter here to the proc's symtab.  This
     * might be OK, since in the interp, a proc amounts to separate compilation
     * unit.  However, counting of errors will be done at the module level for
     * now.  This could change if we like.
     */
    chkParmDecls(t->components.decl.kind.proc.formals);
    chkBlock(t->components.decl.kind.proc.body);


    /*
     * If this is a function procedure, check that at least one return stmt has
     * been seen in the body.  The chkReturn routine will've set the flag.
     * Also reserve a pointer's worth of space in the act rec.
     */
    if ((p = CurSymtab->ParentEntry)->Type and
	    (not ChkSymFlag(p, returnSeen))) {
	lerror(t, "Value-returning procedure %s must contain a return stmt.\n",
	    p->Symbol);
    }

    /*
     * Add storage for return val and display save in act rec.  Note that all
     * return vals are the same size, namely a pointer to a value struct.  We
     * only need a pointer's worth because in the interp we'll use the return
     * val slot to hold a jmp_buf ptr (see interp.c) and the code generator
     * will always return structured vals as pointers (see codegen.c).
     *
     * Note further that we put this space in the act rec whether or not
     * there's a return value, i.e., whether or not we have a function
     * procedure.  This is because we need space for a jmp_buf for returning
     * from any proc, with or without a return value.  See doReturn and
     * doProcCall in interp.c for further details.
     */
    CurSymtab->ParentEntry->Info.Proc.Offset = CurSymtab->Offset;
    CurSymtab->Offset += sizeof(ValueStruct)	/* return val slot */
			+ sizeof(char *);	/* display save slot */

    /*
     * Restore entering scope.
     */
    PopSymtab();
}


/*
 * Check a list of formal parm decls of the form:
 *
 *	[var] name1, ..., namek: [array of] t
 *	    ...
 *
 * by entering offsets.  Since t must be a qualident, it was checked in the
 * first pass, in sym-aux.c:EnterParms.  The optional "array of" part was also
 * handled there.
 */
void chkParmDecls(
    nodep t)
{
    nodep ps, p;
    SymtabEntry *s;

    for (ps = t; ps; ps = ps->components.decl.next) {
	for (p = ps->components.decl.kind.parm.vars; p;
		p = p->components.atom.next) {
	    s = Lookup(p->components.atom.val.text);
	    s->Info.Parm.Offset = CurSymtab->Offset;
	    /*
	     * For var parms and open array parms, reserve only a pointer's
	     * worth of storage, otherwise reserve TypeSize(s->Type).
	     */
	    if (ChkSymFlag(s, varParm) or ChkSymFlag(s, arrayParm))
		CurSymtab->Offset += sizeof(char *);
	    else
		CurSymtab->Offset += TypeSize(s->Type);
	}
    }

}


/*
 * Type check a local module decl.
 */
void chkModuleDecl(
    nodep t)
{
    /*
     * Check the local module, passing it offset of the current symtab as its
     * starting point.  chkModule will bump the global offset counter by the
     * size of the local module's storage.
     */
    chkModule(t->components.decl.kind.module, CurSymtab->Offset);

    /*
     * Update the current symtab's offset counter to where the local module's
     * counter left off.  This includes all the storage consumed by the local
     * module that was just checked, plus any further nested modules.
     */
    CurSymtab->Offset = CurStaticOffset;
}


/**
 ** Check the stmts.
 **/

/*
 * Type check a proc call.  Type of each actual must be compatible with type of
 * each corresonding formal.  This routine also checks that there are the same
 * number of actuals and formals.
 *
 * New on 6jun00 is 2nd arg for coarity overload.  See comments on this in
 * chkExpr and elsewhere.
 */
TypeStruct chkProcCall(
    nodep t,		/* Parse tree proc call */
    TypeStruct tt)	/* Target type for resolving coarity overloads */ 
{
    TypeStruct t1;	/* Typical temp */
    TypeStruct desig=0;	/* Type of proc designator, if present */
    SymtabEntry *p=0;	/* Entry for proc name, if present */

    /*
     * First, check if proc designator is a simple qident, and if so, look it
     * up, else type check the desig expr.
     */
    desig = chkProcDesig(t, &p);

    /*
     * Call the appro binding function, based on the expressionness of the
     * proc desig.
     */
    if (p) {
       /*
        * Qualident case.
        */
	return chkBindingsNameCall(p, desig, t, tt, false);
    }
    else if (desig) {
        /*
	 * Proc expression case.
         */
	return chkBindingsDesigCall(p, desig, t, false);
    }
    else {
	/*
	 * Case where chkProcCallDesig found a problem.
	 */
	return null;
    }
}


/*
 * Check if the given proc call has a plain qual ident as the proc name, or a
 * proc-valued expr.  If the former, return a null return value, and non-null
 * symtab entry in the sym parameter.  If the latter, return the type struct
 * obtained by type checking the desig expr, and a null value in the sym
 * parameter.
 *
 * This somewhat obtuse returning structure comes from the fact that the code
 * for this function was originally in-line at the beginning of chkProcCall.
 * It was subsequently extracted into this function, for use in type checking
 * the outputs of a validation call, in validate.c:chkValidationCall.
 */
TypeStruct chkProcDesig(nodep t, SymtabEntry** sym) {

    SymtabEntry* p=0;	/* Local working variable */
    TypeStruct desig = (TypeStruct) t->components.proccall.desig;
    nodep found_node;	/* Found node returned from LookupQid */

    /*
     * Bifurcate based on whether or not the proc call desig is a qual ident.
     */
    if (isQid(desig)) {
	p = LookupQid(desig, &found_node);
	/*
	 * If lookup fails, we're done.
	 */
	if (not p) {
	    /* Skip this extra error message for now:
	     *
	    lerror(t, "Undeclared identifier %s in proc call.\n",
		    t->components.proccall.desig->components.atom.val.text);
	     *
	     */
	    return null;
	}

	/*
	 * Check if proc name is a var or parm, in which case type check it as
	 * a normal designator expression.
	 */
	if ((p->Class == C_Var) or (p->Class == C_Parm)) {
	    desig = chkExpr(desig, true, null);
	    p = null;
	}

	/*
	 * Disable this for RSL with overloading.
	 *
	else if (not ((p->Class == C_Proc) or (p->Class == C_Op))) {
	    lerror(desig,
		"Identifier %s is not an operation.\n", p->Symbol);
	    return null;
	}
	 *
	 */

    } /* Proc designator is not a single qualident, so type check it. */
    else
	desig = chkExpr(desig, true, null);

    /*
     * Protect ourselves if something goes wrong.
     */
    if (not desig)
	return null;

    /*
     * If proc desig is not a proc name and failed to type check, we're done.
     */
    if (desig->header.kind == TYPE_NODE)
	desig = ResolveIdentType(desig, null, false);
    if (not (p or (desig and isOp(desig)))) {
	lerror(t, "Expression in operation call is not an operation type.\n");
	return null;
    }

    /*
     * OK, we've got a legit proc call (finally) -- return appropriately.
     */
    if (p) {
	*sym = p;
	return null;
    }
    else {
        *sym = null;
	return desig;
    }
}


/*
 * Check actual/formal bindings for a call with a plain ident.  Here we must
 * handle overloaded proc names, which we do by looping through the hash
 * bucket.  Otherwise, binding is the same as in chkBindingsDesigCall. which
 * sameness is reflected in their call to the common chkBindings routine.
 *
 * The 5th parm is used for validation calls.  For such calls, its value is
 * true, otherwise false.  A true value means that checking is done with the
 * formal output parms, instead of the inputs for the binding check.  This parm
 * is not used directly here, but sent through to chkBindings.
 */
TypeStruct chkBindingsNameCall(SymtabEntry* p, nodep desig, nodep t,
	TypeStruct tt, bool out) {
    bool match = false;
    SymtabEntry* entry;
    List* l = NewList();

    /*
     * If it's not been done already, check that there are no dup signatures in
     * the bucket.  See notes in sym-aux.c:EnterOpName and 31oct94 entry in
     * TODO for dicussion about why this is done here.
     */
    if (not ChkSymFlag(p, sigsChecked)) {
	chkOverloadedSigs(p);
	SetSymFlag(p, sigsChecked);
    }

    /*
     * Cruise the hash bucket.  Clearly, this should be done with an
     * info-hiding generator function.  We'll do so in the rewrite.  Note that
     * the logic of sym-aux.c:EnterOpName, q.v., DOES NOT guarantee that only
     * same-name entries of class C_Op are in the bucket.
     */
    for (entry = p; entry; entry = entry->Next) {

	/*
	 * Check if proc name is one of the special (e.g., polymorphic)
	 * built-ins, and if so handle as a special case.  Note that we
	 * disallow special procs from being stored as proc values, so this is
	 * the only place we have to check for this.  Also, special procs
         * cannot be invoked with a validation call, since they are not
         * user-defined, and therefore have no spec to validate.
         */
	if (ChkSymFlag(p, specialProc)) {
	    if (! out) {
	        return chkSpecialProc(p, t->components.proccall.actuals);
	    }
	    else {
		lerror(t, "Built-in operation %s cannot be executed with a validation call.\n",
		p->Symbol);
	    }
	}

	/*
	 * Check if proc name is a type, in which case this is a type cast.
	 *
	 * DISABLE THIS FOR NOW
	 *
	if (p->Class == C_Type) {
	    t1 = chkExpr(t->components.proccall.actuals->
				components.exprlist.expr, true, null);
	    if (t->components.proccall.actuals->components.exprlist.next) {
		lerror(desig, "Type transfer with more than one argument.\n");
		return null;
	    }
	    return p->Type;	\* Force type to be that cast to. *\
	}
	 *
	 */

	/*
	 * Just skip over genuine hashing collisions (i.e., bucket entries that
         * have a different symbol than the possibly-overloaded op), or old
	 * entries on non-proc/op class.
	 */
	if ((entry->Symbol != p->Symbol) or
		((entry->Class != C_Proc) and (entry->Class != C_Op)))
	    continue;

	/*
	 * Check each signature match.  There can be more than one given
	 * subtyping.  
	 */
	if (chkBindings(entry, null, t, out)) {
	    PutList(l, (void*) entry);
	}
    }

    /*
     * If no match found, complain and return null.
     */
    if (ListLen(l) == 0) {
	if (not out) {
	    lerror(t,
	        "Actual parameter list does not match inputs for any definition of\n\t    operation %s\n",
		p->Symbol);
	}
	else {
	    lerror(t,
	        "Actual parameter list does not match outputs for any definition of\n\t    operation %s\n",
		p->Symbol);
	}
	DelListNodesOnly(l);
	return null;
    }

    /*
     * Return the "lowest" of the matches found.  (LowestSignature deletes l.)
     */
    return LowestSignature(l, tt);
}


TypeStruct chkBindingsDesigCall(SymtabEntry* p, nodep desig, nodep t, bool out) {
    if (chkBindings(
	    ((SymtabEntry*)desig->components.type.kind.op.entry),
	    null, t, out))
	return ((SymtabEntry*)desig->components.type.kind.op.entry)->Type;
    else {
	lerror(t,
         "Actual parameter list does not match inputs for operation value.\n");
	return null;
    }
}


/*
 * Common work doer called from both chkBindingsNameCall and
 * chkBindingsDesigCall.  It could be a bit cleaner, but hey.
 */
bool chkBindings(SymtabEntry* p, nodep desig, nodep t, bool out) {
    TypeStruct t1;	/* Return value for type check for each actual */
    nodep ap;		/* Pointer to expr tree for each actual */
    SymtabEntry *fp;	/* Pointer to TypeStruct for each formal, from symtab,
			 * proc type tree, or outputs parm */
    int i;		/* Formal/actual counter */
    bool clash = false;	/* Set if one or more actual/formal type clashes */

    /*
     * Check if the outputs parm is non-null.  If so, we're dealing with a
     * validation call, which means we use the formal outputs instead of the
     * inputs.
     */
    if (out) {
	fp = p ? p->Info.Op.OutParms
	       : desig->components.type.kind.proc.formalchain;
    }
    else {
	fp = p ? p->Info.Op.InParms
	       : desig->components.type.kind.proc.formalchain;
    }

    /*
     * Check for single top-level list parm, in which case we can bundle.
     */
    if (isSingleListArity(p, desig))
	return chkBindingsSingleListArity(p, desig, t, out);

    for (ap = out ? t->components.proccall.returns
		  : t->components.proccall.actuals,
	 i=1;
           ap && fp;
	     ap = ap->components.exprlist.next,
	     fp = fp->Info.Parm.Link,
	     i++) {
	/*
	 * Check first if var parm and if so, require actual to be an l-value.
	 */
	if (ChkSymFlag(fp, varParm)) {
	    if (not isLVal(ap->components.exprlist.expr, false)) {
		clash = true;
		continue;	/* Skip to next parm, so no extra error msg. */
	    }
	}

	/*
	 * Type check the actual and ensure that it's compat with formal.  This
	 * is the bottom of the line (or is it top of the line?, anyway) for
	 * the coarity overload resolution computation.  Viz., this is the
	 * place where we have the value of the target type (the formal type)
	 * that's to be passed on down until it gets used in LowestSig, q.v.
         * Note that this isn't really *THE* bottom of the line, since there
	 * ops (including assmnt) aren't all treated like calls, so there are
         * really a whole bunch of other places that will be other bottoms of
	 * the line.  Basically, these are places where we know from the
	 * context of what we're checking what type to expect.  In the current
	 * implementation there are in fact numerous such places, in each
	 * concrete imple of a type checking rule.
	 */
	t1 = chkExpr(ap->components.exprlist.expr, true, fp->Type);
	if (not parmCompat(fp, t1)) {
	    /*
	     *
	    lerror(ap,
		"Type of actual no. %d not compatible with type of corresponding formal.\n",
			i);
	     */
	    clash = true;	/* Set clash flag, but check the rest */
	}
	FreeTypeIfNecessary(t1);
    }

    /* Return null if one or more type clashes occrrued */
    if (clash)
	return null;

    /* Check for agreement in number of actuals and formals */
    if (ap) {
	/*
	 *
	lerror(t, "Too many actuals in procedure call.\n");
	 */
	return null;
    }
    if (fp) {
	/*
	 *
	lerror(t, "Too few actuals in procedure call\n");
	 */
	return null;
    }

    return true;
}


/*
 * Check a call to a proc with a single top-level list arg as input.  Each
 * actual must be parm compat with the base type of the list.  OR, there may be
 * a single actual of the same list type as the formal.
 */
bool chkBindingsSingleListArity(SymtabEntry* p, nodep desig, nodep t, bool out) {
    TypeStruct t1;	/* Return value for type check for each actual */
    nodep ap;		/* Pointer to expr tree for each actual */
    SymtabEntry* fsym;
    nodep fp;		/* Pointer to TypeStruct for each formal,
			 * either from symtab or proc type tree */
    int i;		/* Formal/actual counter */
    bool clash = false;	/* Set if one or more actual/formal type clashes */

    /*
     * Grab the formal and actual pointers.
     */
    if (out) {
	ap = t->components.proccall.returns;
	fsym = p ? p->Info.Op.OutParms :
	    desig->components.type.kind.proc.formalchain;
    }
    else {
	ap = t->components.proccall.actuals;
	fsym = p ? p->Info.Op.InParms :
	    desig->components.type.kind.proc.formalchain;
    }

    /*
     * This should be unified.  In the rewrite.  It's even worse than it used
     * to be, since it's obviously nugatory.
     */
    if (not ChkSymFlag(fsym, listParm)) {
	fp = fsym->Type->components.type.kind.arraytype.basetype;
    }
    else {
	fp = fsym->Type->components.type.kind.arraytype.basetype;
    }

    /*
     * Check for a single actual of a list type, which is the unbundling case
     * (at runtime, anyway).
     */
    t1 = ResolveIdentType(
	chkExpr(ap->components.exprlist.expr, true, null), null, false);
    if (isListType(t1) and (not ap->components.exprlist.next)) {
	return assmntCompat(fp, t1->components.type.kind.arraytype.basetype);
    }

    /*
     * Cruise the actuals list.
     */
    for (i=1;
           ap && fp;
	     ap = ap->components.exprlist.next,
	     i++) {

	/*
	 * Type check the actual and ensure that it's compat with formal.
	 */
	t1 = chkExpr(ap->components.exprlist.expr, true, null);
	if (not assmntCompat(fp, t1)) {
	    /*
	     *
	    lerror(ap,
		"Type of actual no. %d not compatible with type of corresponding formal.\n",
			i);
	     */
	    clash = true;	/* Set clash flag, but check the rest */
	}
	FreeTypeIfNecessary(t1);
    }

    return (not clash);
}


/*
 * Return true if this is an op with a single top-level list as input.  At
 * present, we grub around a bit to do this check.  It would be more efficient
 * if we set a flag at some earlier point, so all we'd do here is a check of
 * that flag.  LATER, if ever.
 */
bool isSingleListArity(SymtabEntry* p, nodep desig) {
    SymtabEntry* ip;

    if (p) {
	ip = p->Info.Op.InParms;
    }
    else {
	ip = desig->components.type.kind.proc.formalchain;
    }

    return (ip and (ChkSymFlag(ip, listParm) or isListType(ip->Type)) and
	(ip->Info.Parm.Link == null));
}


void FreeTypeIfNecessary(TypeStruct t) {
    if (t and t->components.type.isDerivedIdentType) {
	free(t->components.type.origname);
	free(t);
    }
}

void chkOverloadedSigs(SymtabEntry* p) {
}


/*
 * Find the lowest signature in a list of op-class symtab entries, and return
 * its coarity.  Lowest means the signature with the lowest subtype in each
 * position.
 *
 * A VERY INTERESTING OBSERVATION: It appears that this routine requires name
 * type equiv, at least in declared op sigs.  TODO: THINK CAREFULLY ABOUT THIS.
 *
 * New 6jun00 is the 2nd parm, which is used as is the last parm in chkExpr --
 * to resolve coarity-only overloads.  Hope this does the trick.
 */
TypeStruct LowestSignature(
    List* l,
    TypeStruct tt)	    /* Target type for resolving coarity overloads */ 
{
    TypeStruct rtn;
    int mins[100];	    /* Minimum type at each arity position */
    int lowscore = 0;	    /* Lowest overall arity score */
    int indexoflowest = 1;  /* Index in l of lowest scoring arity */
    SymtabEntry* sym = (SymtabEntry*) GetListNth(l,1);
    SymtabEntry* p;
    int i;

    /*
     * If there's only one sig, return its type.
     */
    if (ListLen(l) == 1) {
	rtn = sym->Type;
	DelListNodesOnly(l);
	return rtn;
    }

    /*
     * Coarity overloading is officially dead.
     *
     * Resolove coarity overloading.  Do this by cruising the sig list and
     * returning the first sig that matches the target input parm tt.  A bit of
     * an open question is exactly what "matches" means (currently it's compat)
     * and if the first should always be returned (but this will most likely be
     * resolved when the issue noted in the next paragraph is resolved).
     *
     * This coarity overload computation is being done before the rest of the
     * lowest sig resolution TODO item (below) has been completed.  This
     * coarity res will in all likelihood need to be integerated with the TODO
     * lowest computation in some way.  We'll have to figure this out when we
     * do it.
     *
    for (sym = (SymtabEntry *) EnumList(l); sym;
	    sym = (SymtabEntry *) EnumList(l)) {
	if (compat(sym->Type, tt))
	    return sym->Type;
    }
     */

    /*
     * Fall-back position if co-arity overload res doesn't pan out, for
     * whatever reason.
     */
    return ((SymtabEntry*) GetListNth(l, 1))->Type;

    /*
     * Cruise the first sig, init'ing the min array to its types.  TODO.
     */
    for (p = sym->Info.Op.InParms, i=0; sym; sym = sym->Info.Parm.Link, i++) {
	/*mins[i] = p->Type;*/
    }

    /*
     * Criuse the rest of the sigs, recomputing mins[i] for each.
     */
}


/*
 * OLD from Mod-2.
 *
 * Type check the std procs with polymorhic signatures.  What we do here is as
 * much compile-time type checking as possible.  In some cases, further runtime
 * type checks will be necesary.  See built-ins.c.
 *
 * To avoid a humungously inefficient if-then-elseif here, the trick is to
 * preload the special-purpose type checking function for each special proc in
 * the symtab.  Given, we just look the proc up and call its type checker.  By
 * convention, all special-purpose type chking funcs take the same two args
 * passed in here -- viz., the symtab entry for the called proc, and the raw
 * actuals tree pointer.
 */
TypeStruct chkSpecialProc(
    SymtabEntry *p,
    nodep t)
{
    return p->Info.Proc.ChkFunc(p, t);
}


/*
 * Type check an assmnt stmt/expr.  LHS and RHS must be assmnt compatible.
 * Also as subtle special case, disallow mutation of array element of a parent
 * type.  See the ref man for its discussion of covariance and contravariance
 * rules.
 */
TypeStruct chkAssmnt(
    nodep t)
{
    TypeStruct t1,t2;	/* Typical subtree pointers */
    TypeStruct it;	/* Array basetype ident type, if any */
    nodep v;
 
    /*
     * Confirm that the LHS is a visble l-value, i.e., a variable or parm.
     * If so, type check it.
     */
    if (isLVal(v = t->components.stmt.kind.assmnt.var, true)) {
	t1 = chkExpr(v, true, null);
    }
    else {
	t1 = null;
    }

    /*
     * If LHS desig is anything other than a plain ident, and its type is a
     * list, disaallow the mutation.  This is overkill, since there may be no
     * mutation involved, but tough luck.  See the discussion of a covariance
     * and contravariance in the ref man.
     */
    if (t and (not isIdentAtomNode(v)) and isListType(t1)) {
	it = t1->components.type.kind.arraytype.basetype;
	if (it and isIdentType(it)
	        /* and ChkSymFlag(Lookup(it->components.type.kind.ident */) {
	    printf("File %s, Line %d, char %d, %s\n",
		t->header.loc.file, t->header.loc.line, t->header.loc.col,
	        it->components.type.kind.ident.type->components.atom.val.text);
	}
    }

    /*
     * Type check the RHS, even if error in LHS.
     */
    t2 = chkExpr(t->components.stmt.kind.assmnt.expr, true, null);

    /*
     * Don't bother with further error message if error in LHS and/or RHS.
     */
    if ((t1 == null) or (t2 == null))
	return null;

    /*
     * Check for assignment compatility between LHS and RHS.
     */
    if (assmntCompat(t1,t2))
	return t1;
    else {
	lerror(t, "Incompatible types in set expression.\n");
	return null;
    }
}


/*
 * Check that a designator is an l-value.  The fly in the ointment is that the
 * qualident part of a designator may be a sequenece of module names, which we
 * must traverse a la LookupQid, but without issuing an error when we don't
 * find a module.  Once we get through the modules, we lookup the ident on the
 * RHS of the '.' and check that its class is C_Var or C_Parm.
 *
 * Note that isLVal gets called from two places -- checking the LHS of an
 * assmnt stmt in chkAssmnt, and checking the actual corresponding to a formal
 * var parm in chkProcCall.  The significant diff in the handling of these two
 * cases has to do with the syntax.  In the case of an assmnt LHS, the syntax
 * restricts the expr to be a designator.  In the case of an actual parm, a
 * full expr is syntactically legal. Hence, for parms, we have to eliminate all
 * exprs that aren't designators, including literal constants and such like.
 * The other diff in the two cases is the text of the error message.
 */
bool isLVal(
    nodep t,
    bool assmnt)	/* True if called from chkAssmnt, false if called from
			 * chkProcCall (checking a var parm). */
{
    nodep ql, qr;
    SymtabEntry *syml, *symr;
    char *nl, *nr;

    /*
     * If t->header.name is a designator operator, we'll assume that it's a
     * legal var.  Further type checking after we leave here will be done to
     * confirm it.
     */
    if (assmnt and (t->header.name != Yident))
	return true;
    if ((not assmnt)) {
	switch (t->header.name) {

	    /*
	     * Continue with further checks below of actual is an ident.
	     */
	    case Yident:
		break;

	    /*
	     * Return OK, with further checking to be done, if actual is a
	     * designator expr.
	     */
	    case '.':	/* '.' actually cant happen here in current syntax */
	    case '[':
	    case '^':
		return true;

	    /*
	     * Error if actual is not an plain ident or designator expr.
	     */
	    default:	
		lerror(t, "Var parameter must designate a variable.\n");
		return false;
	}
    }

    /*
     * Lookup first (possible only) qid component and quit if not found.
     */
    if (not (syml = Lookup(nl = t->components.atom.val.text))) {
	lerror(t, "%s is not defined in this scope.\n", nl);
	return false;
    }

    /*
     * Prepare to move into new symtab(s) by saving CurSymtab.
     */
    PushSymtab();
    
    /* 
     * Move through each qid component that's a module name.
     */
    if (t->header.name == Yident) {
	for (ql = t, qr = t->components.atom.next;
		 qr; ql = qr, qr = qr->components.atom.next, syml = symr) {

	    /*
	     * Check if left operand is a module.
	     */
	    if (syml->Class != C_Module) {
		break;
	    }

	    /*
	     * Move into the scope of the left operand.
	     */
	    MoveToSymtab(syml->Info.Module.Symtab);

	    /*
	     * Lookup right oprnd and confirm that it's an export of the left
	     * oprnd.
	     */
	    symr = Lookup(nr = qr->components.atom.val.text);
	    if ((not symr) or (not ChkSymFlag(symr, isExport))) {
		lerror(qr, "%s is not an export of %s.\n", nr, nl);
		PopSymtab();
		return false;
	    }
	}
    }

    /*
     * OK, we're at the end of the module names prefix.  We have a legit var if
     * the class of the last (only) ident is C_Var or C_Parm.  No additional
     * checking of the remaining designator expr, if it exists, is done here --
     * it's done after we leave by further type checking in the caller.
     */
    PopSymtab();
    if ((syml->Class == C_Var) or (syml->Class == C_Parm)) {
	return true;
    }
    else {
	lerror(t,
	    "%s is not a global variable that can be set.\n",
		syml->Symbol);
	return false;
    }
}


/*
 * Type check an if stmt.  If expr must be bool.  Each of the then, elsif, and
 * else clauses is recursively type checked.
 */
void chkIf(
    nodep t)
{
    nodep ti;

    if (not isBool(chkExpr((ti = t->components.stmt.kind.ifstmt.expr),
	    true, null)))
	lerror(ti, "Type of if expr must be bool.\n");
    chkStmts(t->components.stmt.kind.ifstmt.thenpart);
    chkStmts(t->components.stmt.kind.ifstmt.elsifparts);
    chkStmts(t->components.stmt.kind.ifstmt.elsepart);
}


/*
 * Type check an elsif clause.  Elsif expr must be bool.  The then clause is
 * recursively type checked.
 */
void chkElseIf(
    nodep t)
{
    if (not isBool(chkExpr(t->components.stmt.kind.elsif.expr, true, null)))
	lerror(t, "Type of elsif expr must be bool.\n");
    chkStmts(t->components.stmt.kind.elsif.thenpart);
}


/**
 ** Check the ops.
 **/

/*
 * Check '+'.  Operand types must be numeric, string, list, or element of list.
 *
 * 5dec09 glf.  OK, this is a real mess at this point, given the piecemeal
 * testing that's gone on.  Among the issues are:
 *
 *     -- isIntOrIntLit has been hacked on 3dec09 to call compat2
 *     -- I'm not sure about the call to compat for the istListType(t1) case;
 *        viz., should it be compat2?
 *     -- the whole compat, compat2, assntCompat shit is very convoluted and
 *        should be reworked
 *     -- a formal semantics would not only be nice for advertising and
 *        publication purposes, it would probably help guide an improved, aka,
 *        correct implementation
 *
 */
TypeStruct chkPlusOp(
    nodep t,
    bool f)
{
    TypeStruct t1,t2;

    t1 = ResolveIdentType(chkExpr(t->components.binop.left_operand, f, null),
	t, true);
    t2 = ResolveIdentType(chkExpr(t->components.binop.right_operand, f, null),
	t, true);

    if ((t1 == null) or (t2 == null))
	return null;

    if (isIntOrIntLit(t1) and isIntOrIntLit(t2))
	return IntType;
    if (isIntOrIntLit(t1) and isReal(t2))
    	return RealType;
    if (isReal(t1) and isIntOrIntLit(t2))
    	return RealType;
    if (isReal(t1) and isReal(t2))
    	return RealType;
    if (isListType(t1) and isListType(t2) and compat(t1,t2))
	return t1;
    if (isListType(t1) and isElemOf(t2,t1))
	return t1;
    if (isListType(t2) and isElemOf(t1,t2))
	return t2;
    if (isStringOrStringLit(t1) and isStringOrStringLit(t2))
	return StringType;

    lerror(t, "Operands of '+' must be numeric, string, list, or list element.\n");
    return null;
}


/*
 * Check '-'.  Operand types must be numeric, list, or element of list.
 */
TypeStruct chkMinusOp(
    nodep t,
    bool f)
{
    TypeStruct t1,t2;

    t1 = ResolveIdentType(chkExpr(t->components.binop.left_operand, f, null),
	t, true);
    t2 = ResolveIdentType(chkExpr(t->components.binop.right_operand, f, null),
	t, true);

    if ((t1 == null) or (t2 == null))
	return null;

    if (isIntOrIntLit(t1) and isIntOrIntLit(t2))
	return IntType;
    if (isIntOrIntLit(t1) and isReal(t2))
    	return RealType;
    if (isReal(t1) and isIntOrIntLit(t2))
    	return RealType;
    if (isReal(t1) and isReal(t2))
    	return RealType;
    if (isList(t1) and isList(t2) and compat(t1,t2))
	return t1;
    if (isListType(t1) and isElemOf(t2,t1))
	return t1;
    if (isListType(t2) and isElemOf(t1,t2))
	return t2;

    lerror(t, "Operands of '-' must be numeric, list, or list element.\n");
    return null;
}


/*
 * Check '*'.  Operand types must be numeric.
 */
TypeStruct chkMultOp(
    nodep t,
    bool f)
{
    TypeStruct t1,t2;

    t1 = ResolveIdentType(chkExpr(t->components.binop.left_operand, f, null),
	t, true);
    t2 = ResolveIdentType(chkExpr(t->components.binop.right_operand, f, null),
	t, true);

    if ((t1 == null) or (t2 == null))
	return null;

    if (isIntOrIntLit(t1) and isIntOrIntLit(t2))
	return IntType;
    if (isIntOrIntLit(t1) and isReal(t2))
    	return RealType;
    if (isReal(t1) and isIntOrIntLit(t2))
    	return RealType;
    if (isReal(t1) and isReal(t2))
    	return RealType;

    lerror(t, "Operands of '*' of '/' must be numeric.\n");
    return null;
}


/*
 * Type check a non-real arithmetic op (i.e., div or mod).  Operand types must
 * be int or card, and compatible.
 */
TypeStruct chkArithIntOp(
    nodep t,
    bool f)
{
    TypeStruct t1,t2;

    t1 = ResolveIdentType(chkExpr(t->components.binop.left_operand, f, null),
	t, true);
    t2 = ResolveIdentType(chkExpr(t->components.binop.right_operand, f, null),
	t, true);

    if ((t1 == null) or (t2 == null))
	return null;

    if ((not isIntOrCardOrSubrangeOfEither(t1)) or
	    (not isIntOrCardOrSubrangeOfEither(t2))) {
	lerror(t, "Operands of %s must be int or card.\n",
	    (t->header.name == YDIV) ? "div" : "mod");
	return null;
    }
	
    if (compat(t1,t2))
	return t1;
    else {
	lerror(t, "Incompatible operand types in an arithmetic expr.\n");
	return null;
    }
}


/*
 * Type check '/'.  Operand types must real.
 */
TypeStruct chkArithRealOp(
    nodep t,
    bool f)
{
    TypeStruct t1,t2;

    t1 = ResolveIdentType(chkExpr(t->components.binop.left_operand, f, null),
	t, true);
    t2 = ResolveIdentType(chkExpr(t->components.binop.right_operand, f, null),
	t, true);

    if ((t1 == null) or (t2 == null))
	return null;

    if ((isReal(t1) and isReal(t2)) or
	    (isLongReal(t1) and isLongReal(t2))) {
	return t1;
    }
    else {
	lerror(t, "Operands of '/' must be real.\n");
	return null;
    }
}


/*
 * Type check a unary arithmetic op.  Operand type must be numeric.
 */
TypeStruct chkUnaryArithOp(
    nodep t,
    bool f)
{
    TypeStruct t1;

    t1 = ResolveIdentType(chkExpr(t->components.binop.left_operand, f, null),
	t, true);

    if (t1 == null)
	return null;

    if (not isNumeric(t1)) {
	lerror(t, "Operand in a unary arithmetic expr must be numeric.\n");
	return null;
    }

    return t1;
}


/*
 * Type check a boolean op.  Operand types must be bool.
 */
TypeStruct chkBoolOp(
    nodep t,
    bool f)
{
    TypeStruct t1,t2;

    t1 = ResolveIdentType(chkExpr(t->components.binop.left_operand, f, null),
	t, true);
    t2 = ResolveIdentType(chkExpr(t->components.binop.right_operand, f, null),
	t, true);

    if ((t1 == null) or (t2 == null))
	return null;

    if (isBool(t1) and isBool(t2))
	return BoolType;
    else {
	lerror(t, "Operands in a boolean expr must be bool.\n");
	return null;
    }
}


/*
 * Type check a unary not operator.  Operand type must be bool.
 */
TypeStruct chkNotOp(
    nodep t,
    bool f)
{
    TypeStruct t1;

    t1 = ResolveIdentType(chkExpr(t->components.binop.left_operand, f, null),
	t, true);

    if (t1 == null)
	return null;

    if (not isBool(t1)) {
	lerror(t, "Operand of a not operator must be bool.\n");
	return null;
    }

    return t1;
}


/*
 * Type check a rel op.  Operand types must be ordered and compat.  Return type
 * is bool
 */
TypeStruct chkRelOp(
    nodep t,
    bool f)
{
    TypeStruct t1,t2;

    t1 = ResolveIdentType(chkExpr(t->components.binop.left_operand, f, null),
	t, true);
    t2 = ResolveIdentType(chkExpr(t->components.binop.right_operand, f, null),
	t, true);

    if ((t1 == null) or (t2 == null))
	return null;

    if ((not compat(t1,t2)) and (not litBaseCompat2(t1,t2))) {
	lerror(t, "Incompatible operand types in a relational expr.\n");
	return null;
    }

    /*
     * Check that types are orderable.
     */
    if (not isOrdered(t1)) {
	lerror(t, "Operands in a relational expr must be\n\t\tnumeric, bool, char, enum, subrange, or set.\n");
	return null;
    }

    /*
     * Upon success, return bool.
     */
    return BoolType;
}

/*
 * Type check an equality op, or the RSL list size op.  For eq ops, operand
 * types must be compat and return type is bool.
 *
 * For list size op, see chkSizeOp below.
 */
TypeStruct chkEqOp(
    nodep t,
    bool f)
{
    TypeStruct t1,t2;

    /* I think the next two lines are remnant of mod-2 '#' op, and can be
     * purged. */
    if (t->header.kind == UNOP_NODE)
	return chkLenOp(t, f);

    t1 = ResolveIdentType(chkExpr(t->components.binop.left_operand, f, null),
	t, true);
    t2 = ResolveIdentType(chkExpr(t->components.binop.right_operand, f, t1),
	t, true);

    if ((t1 == null) or (t2 == null))
	return null;

    if ((not compat2(t1,t2)) and (not litCompat2(t1,t2)) and
	    (not litBaseCompat2(t1,t2))) {
	lerror(t, "Incompatible operand types in an equality expr.\n");
	return null;
    }

    /*
     * Check that types are equatable, which for now is any type.
     */
    if (not isEquatable(t1)) {
	lerror(t, "Operands in an equality expr must be\n\t\tnumeric, bool, char, enum, subrange, set, or pointer.\n");
	return null;
    }

    /*
     * Upon success, return bool.
     */
    return BoolType;
}


/*
 * Type check an almost-equal op of the form
 *
 *     name ~= expr EXCEPT exception [, ..., exception]
 *
 * where the following constraints apply:
 *
 *    (1) name and expr must be the same tuple type
 *    (2) the exceptions are tuple selector expressions with name leftmost var
 *        in the expression
 */
TypeStruct chkAlmostEqOp(
    nodep t,
    bool f)
{
    TypeStruct t1, t2;
    nodep name, expr, el, left_oprnd;
    char* namestr;
    bool inner_exception_error, any_exception_error = false;

    /*
     * Type check name and expr.
     */
    t1 = ResolveIdentType(
	chkExpr(name = t->components.trinop.left_operand, f, null), t, true);
    t2 = ResolveIdentType(
	chkExpr(expr = t->components.trinop.middle_operand, f, null), t, true);
    namestr = name->components.atom.val.text;


    /*
     * Confirm that t1 and t2 are the same tuple type.
     */
    if ((not isRecord(t1)) || (not isRecord(t2)) || (not compat(t1, t2))) {
	lerror(t,
	    "Operands in almost equality expr must be the same tuple type.\n");
	return null;
    }

    /*
     * Cruise the exception list and ensure that each element in the list
     * has compatible operands and that the left operand of each element is a
     * tuple selector expr with name as its leftmost var.
     */
    for (el=t->components.trinop.right_operand; el;
	    el=el->components.exprlist.next) {

	/*
	 * Next access is safe because each exception clause is guaranteed
         * syntactically to be a '=' binop.
	 */
	left_oprnd =
            el->components.exprlist.expr->components.binop.left_operand;

	/*
         * Confirm that left_oprnd is a tuple selection expression with its
         * leftmost operand equal to name.  Since tuple select exprs are left
         * heavy trees, we must descend all the way down to the left to get
         * where to need to go.  In this descent, we'll assume that we have
         * nothing but binops, and that we're looking for the case that the
         * left operand during the descent turns into an ident.  Anything that
         * doesn't match this descent pattern we'll treat it as an error.
         * Tough luck of this isn't general enough.
	 */
	for (expr = left_oprnd, inner_exception_error = false; true;
		expr = expr->components.binop.left_operand) {
	    
	    /*
             * A check for binopness needs to be true always at the top of the
             * loop.  As soon as it's not, we've either descended all the way
             * down to the left without finding name as the left operand, or
             * we've found something other than a binop.  Either way, we're
             * done, with an error as the result.  Since we keep going left in
             * the loop increment, we can't get stuck in an infinite loop,
             * since all binops will eventually end to the left.
	     */
	    if (expr->header.kind != BINOP_NODE) {
	        lerror(el,
		    "Left operand in almost equal exception must reference tuple variable.\n");
		inner_exception_error = any_exception_error = true;
		break;
	    }

	    /*
	     * If we have a binop and its left operand is an atom node, then
             * we're also done.  If the atom node's text val = name, then we're
             * done successfully, otherwise we have an error.
	     */
	    if ((expr->header.name == '.') &&
		    isIdentAtomNode(expr->components.binop.left_operand)) {
		if (streq(namestr, expr->components.binop.left_operand->
			components.atom.val.text)) {
		    break;
		}
		else {
	            lerror(el,
		        "Left operand in almost equal exception must reference tuple variable %s.\n", namestr);
		    inner_exception_error = any_exception_error = true;
		    break;
		}
	    }

	    /*
             * At this point, we've found a binop with a non-atom left operand,
             * in which case we continue to descend to the left.  This is done
             * by doing nothing but just continuing with the loop, since the
             * loop increment does the descent thing.
	     */
	}

	if (inner_exception_error) {
	    continue;
	}

	t1 = chkExpr(
	    el->components.exprlist.expr->components.binop.left_operand,
		f, null);
	t2 = chkExpr(
	    el->components.exprlist.expr->components.binop.right_operand,
		f, null);

	if (not compat(t1,t2)) {
	    lerror(el, "Incompatible operand types in an almost equality exception clause.\n");
	    any_exception_error = true;
	}
    }

    return any_exception_error ? null : BoolType;
}


/*
 * Type check a list size op.  Operand must be a list, and return type is int.
 */
TypeStruct chkLenOp(
    nodep t,
    bool f)
{
    TypeStruct t1;

    t1 = ResolveIdentType(chkExpr(t->components.unop.operand, f, null),
	t, true);

    if (t1 == null)
	return null;

    if ( (not isListType(t1)) and (not isStringOrStringLit(t1)) and (not isIntOrIntLit(t1)) ) {
	lerror(t, "Operand of '#' operator must be a list, string, or int type.\n");
	return null;
    }

    return IntType;
}
    

/*
 * Check the 'in' operator.  Type of right operand must be list and type of
 * left operand must be assmnt compat with the basetype of list, or both types
 * must be list.  In the list case, we use assmnt compat so we can check
 * without casting that a subtype is is a parent type list.  To be clear, here
 * is exactly what happens to distinguish the string and list cases:
 *
 *     left arg		right arg	return		remark
 *     ===================================================================
 *     string		string		bool		this is substring
 *     string		string*		bool		this is string in list
 *     T		T*		bool		this is elem in list
 *     other		other		error		this doesn't work
 *
 */
TypeStruct chkInOp(
    nodep t,
    bool f)
{
    TypeStruct t1,t2,t3;

    t1 = ResolveIdentType(chkExpr(t->components.binop.left_operand,
//	f, null), t, true);
	f, null), t->components.binop.left_operand, true);
    t2 = ResolveIdentType(chkExpr(t3 = t->components.binop.right_operand,
//	f, null), t, true);
	f, null), t->components.binop.right_operand, true);

    if ((t1 == null) or (t2 == null))
	return null;

    /*
     * If right operand is a one-tuple, descend on down.
     */
    if (isOneTuple(t2))
	t2 = ResolveIdentType(t2->components.type.kind.record.fields->
	    components.decl.kind.field.type, t, true);

    /*
     * Check the string case first.  If both are strings, fine.  If right is
     * string, but left is not, then signal an appropriate error.  Otherwise,
     * proceed to check the list case.
     */
    if (isStringOrStringLit(t1) and isStringOrStringLit(t2)) {
	return BoolType;
    }
    if (isStringOrStringLit(t2) and (not isStringOrStringLit(t1))) {
	lerror(t, "If right operand of 'in' is a string, left operand must be string.\n");
	return null;
    }

    /*
     * Check that the right op is a list first.  We do this, because it's
     * useless, and in fact erroneous, to check basetype if we don't have a
     * list.
     */
    if (not isArray(t2)) {
	lerror(t, "Right operand of 'in' must be a list or a string.\n");
	return null;
    }

    /*
     * Now check that left operand is assmnt compat with basetype of list.
     * Note position of t1 and t2 args in actuals list of assmntCompat.  Here
     * t2 must be considered the LHS, since we want to check that t1 is subtype
     * compat with t2.
     */
    if ( ResolveIdentType(t1, null, false) and
	    (not assmntCompat(
		t2->components.type.kind.arraytype.basetype, t1))) {
	lerror(t, "Left operand of 'in' must be compatible with base type of right operand\n");
	return null;
    }

    /*
     * Upon success, return bool
     */
    return BoolType;
}

/*
 * Check a list ref of the form
 *
 * 	desig [ index-expr ]
 *
 * where the desig is in the left operand and the index-exp is in the right
 * operand.  The desig must be a list or string type and the index-expr must
 * int compat.
 *
 */
TypeStruct chkArrayRef(
    nodep t,
    bool f)
{
    TypeStruct desig;	/* Pointer to designated list (aka, array) type. */
    TypeStruct t1,t2;	/* Typical subtree pointers */
    nodep ip;		/* Pointer to expr tree for each index expr. */
    int i;		/* Index counter */
    bool clash = false;	/* Set if one or more index expr/decl clashes */

    /*
     * Type check the left operand.
     */
    if (not (desig = ResolveIdentType(
	    chkExpr(t->components.binop.left_operand, f, null), t, true)))
	return null;	/* So we dont output extra error messages. */

    /*
     * If left operand is a one-tuple, descend on down.
     */
    if (isOneTuple(desig))
	desig = ResolveIdentType(desig->components.type.kind.record.fields->
	    components.decl.kind.field.type, t, true);

    /*
     * Check that the left operand is a list (aka, array) or string type,
     * including a one-tuple of one of these.
     */
    if (not (isArray(desig) or isStringOrStringLit(desig))) {
	lerror(t, "Left operand of [...] is not a list or string.\n");
	return null;  /* go no further, even though we might consider type
		       * checking the indices, we'll wait to do this until
		       * the user fixes the array ref itself */
    }

    /*
     * Check that the index expr is int compat.
     */
    t1 = chkExpr(ip = t->components.binop.right_operand, f, null);
    if (not compat(t1, IntType)) {
	lerror(ip,
	    "Type of list index expression must be integer.\n",
	    i);
	clash = true;	/* Set clash flag, but check the rest */
    }

    /*
     * Say goodbye if a type clash occurred.
     */
    if (clash)
	return null;

    /*
     * Return type is basetype of the list, or string if left operand is a
     * string. 
     */
    return (isArray(desig)) ?
        desig->components.type.kind.arraytype.basetype :
        StringType;
}

/*
 * Type check a list slice ref of the form
 *
 *	desig [ index-expr1 : index-expr2 ]
 *
 * where desig is the left operand, index-expr1 is the middle operand, and
 * index-expr2 is the right operand (of a trinop).  The desig must be a list
 * type, and the index-expr's must be int compat.
 */
TypeStruct chkArraySliceRef(TypeStruct t, bool f) {
    TypeStruct desig;	/* Pointer to designated list (aka, array) type. */
    TypeStruct desig1;	/* Unresolved version of desig. */
    TypeStruct t1,t2;	/* Typical subtree pointers */
    nodep ip1,ip2;	/* Pointer to expr tree for each index expr. */
    int i;		/* Index counter */
    bool clash = false;	/* Set if one or more index expr/decl clashes */

    /*
     * Type check the left operand.
     */
    if (not (desig = ResolveIdentType(
	    desig1 = chkExpr(t->components.trinop.left_operand, f, null),
		t, true)))
	return null;	/* So we dont output extra error messages. */

    /*
     * If left operand is a one-tuple, descend on down.
     */
    if (isOneTuple(desig))
	desig = ResolveIdentType(desig->components.type.kind.record.fields->
	    components.decl.kind.field.type, t, true);

    /*
     * Check that the left operand is a list (aka, array) type.
     */
    if (not (isArray(desig) or isStringOrStringLit(desig))) {
	lerror(t, "Left operand of [...] is not a list or string.\n");
	return null;  /* go no further, even though we might consider type
		       * checking the indices, we'll wait to do this until
		       * the user fixes the array ref itself */
    }

    /*
     * Check that the index exprs are int compat.
     */
    t1 = chkExpr(ip1 = t->components.trinop.middle_operand, f, null);
    t2 = chkExpr(ip2 = t->components.trinop.right_operand, f, null);
    if (not compat(t1, IntType)) {
	lerror(ip1,
	    "Type of list index expression must be integer.\n",
	    i);
	clash = true;	/* Set clash flag, but check the rest */
    }
    if (not compat(t2, IntType)) {
	lerror(ip2,
	    "Type of list index expression must be integer.\n",
	    i);
	clash = true;	/* Set clash flag, but check the rest */
    }

    /*
     * Say goodbye if a type clash occurred.
     */
    if (clash)
	return null;

    /*
     * Return type is same as incoming list or string type.
     */
    return desig1;
}


/*
 * TODO.
 */
TypeStruct chkLambda(nodep t, bool f) {
    return null;
}

/*
 * Check the dot operator used as a module, tuple, or union field selector.
 * The left operand is a module, tuple (aka, record), or union, and the right
 * operand must be an export or field thereof.
 *
 * Since modules are not themselves objects, they cannot be tuple components.
 * Therefore, the stucture of a chain of dot operators must look like this
 *
 *     M1.M2. ... .Mn.T1.T2. ... .Tn.ident
 *
 * where the Mi are module names and the Ti are tuple or union types.  Given
 * this structure, this function will cruise all the way down any leading
 * prefix of module refs to the first non-module.  Doing this cruise of an
 * initial leading module prefix avoids having to return some fake TypeStruct
 * for a module, which is not a type.
 */
TypeStruct chkRecordRef(
    nodep t,
    bool f)
{
    TypeStruct t1;
    TypeStruct l, desig;

    /*
     * Check first if we have a leading prefix of one or more module refs and
     * if so return what comes back, which will be the type of the first
     * non-module ident.  
     */
    if (t1 = chkModuleRefs(t))
	return t1;

    l = chkExpr(t->components.binop.left_operand, f, null);
    desig = ResolveIdentTypeAsOneTuple(l, t, false);
    return chkRecordOrUnionRef(t, f, l, desig,
	"Left operand of '.' is not a module, tuple, or union.\n",
	"is not a field of the tuple or union on the left of the '.'\n");
}


/*
 * Check if the left operand is a module.  If so, check if the right operand is
 * an export from that module.  If both those conditions are true, return the
 * type of the right operand, otherwise return null.
 */
TypeStruct chkModuleRefs(nodep t) {
    return null;
}


/*
 * Check the isa operator used as a field tag interrogator.  The left operand
 * is a union, and the right operand must be a field thereof.
 */
TypeStruct chkUnionRef(
    nodep t,
    bool f)
{

    TypeStruct l = chkExpr(t->components.binop.left_operand, f, null);
    TypeStruct desig = ResolveIdentTypeAsOneTuple(l, t, true);

    if ((not isUnion(desig)) and
	    (not (isRecord(desig) and (isOneTuple(desig) and
		isUnion(desig->components.type.kind.record.fields->
		    components.decl.kind.field.type))))) {
	lerror(t, "Left operand of isa is not a union.\n");
	return null;
    }

    return chkRecordOrUnionRef(t, f, l, desig,
	"Left operand of ?. is not a union.\n",
	"is not a tag of the union on the left of the ?.\n")
	    ? BoolType : null;
}


/*
 * Common function for chkRecordRef and chkUnionRef.
 */
TypeStruct chkRecordOrUnionRef(
    nodep t,
    bool f,
    TypeStruct l,
    TypeStruct desig,	/* Result of recursive type chk of left operand. */
    char* errmsg1,
    char* errmsg2)
{
    char *fname;	/* String name of field to be found. */
    int fnum;		/* Int find number of field to be found. */
    SymtabEntry *fsym;	/* Entry for field. */
    bool onetuple = false;
    int i;		/* Loop index for counting to numeric field position. */
    nodep fp;		/* Field node pointer, for counting loop. */

    /*
     * Loop to handle one-tuple go round's (not often > 1, presumably).
     */
    while (true) {

	/*
	 * Grab the right operand field name or number.
	 */
	if (t && t->components.binop.right_operand &&
		t->components.binop.right_operand->header.name == Yident) {
	    fname = t->components.binop.right_operand->components.atom.val.text;
	}
	else {
	    fname = null;
	    fnum = t->components.binop.right_operand->components.atom.val.integer; 
	}

	/*
	 * Recursively type check the left operand.  The somewhat complicated
	 * if-tests are to avoid outputting excessive error messages.  It's
	 * logic was determined empirically, by examining error message logs.
	 */
	if ((not (desig = ResolveIdentTypeAsOneTuple(l, t, false))) and
		(not onetuple)) {

	    /*
	     * A non-null value of l is taken as an indication that an adequte
	     * error message has already been output, in particular by
	     * chkIdent, which will have been called prior to this.
	     */
	    if (l) {
		lerror(t, errmsg1);
	    }
	    return null;
	}

	if (onetuple and ((not desig) or (not isTupleOrUnion(desig)))) {
	    if (fname) {
		lerror(t, "%s %s", fname, errmsg2);
	    }
	    else {
		lerror(t,
		    "%d is not a field position of the tuple or union on the left of the '.'",
		    fnum);
	    }
	    return null;
	}
	if ((not desig) or (not isTupleOrUnion(desig))) {
	    lerror(t, errmsg1);
	    return null;
	}

	/*
	 * Move into the records symtab scope.
	 */
	PushSymtab();
	MoveToSymtab(desig->components.type.kind.record.fieldstab);

	/*
	 * Find a field name via lookup, or use an integer field access as an
	 * index into the fields list.  For the integer case, check that the
	 * value is between 1 and the number of fields, inclusive.
	 */
	if (fsym = LookupThisScope(fname)) {
	    PopSymtab();

	    /*
	     * Note -- no ident type resolution here.
	     */
	    return fsym->Type;
	}

	
	/*
	 * If the left operand is a one-tuple, descend into it and try again.
	 */
	if (isOneTuple(desig)) {
	    l = desig->components.type.kind.record.fields->
		components.decl.kind.field.type;
	    PopSymtab();
	    onetuple = true;
	    desig = ResolveIdentTypeAsOneTuple(l, t, true);
	    continue;
	}
	else if (not fname) {
	    if (fnum < 1) {
		lerror(t,
		    "The numeric position of a record or union field must be > 0\n");
		PopSymtab();
		return null;
	    }
	    if (fnum > desig->components.type.kind.record.numfields) {
		lerror(t,
		    "There are fewer than %d fields in the record or union on the left of the '.'\n",
		    fnum);
		PopSymtab();
		return null;
	    }

	    /*
	     * OK, we've got a legit field number.  Return the type of field at
	     * that numeric position in the field list.
	     */
	    for (i = 1, fp = desig->components.type.kind.record.fields;
		i < fnum;
		    i++, fp = fp->components.decl.next) {
		;
	    }
	    PopSymtab();
	    return fp->components.decl.kind.field.type;
	}
	else {
	    lerror(t, "%s %s", fname, errmsg2);
	    PopSymtab();
	    return null;
	}
    }
}


/*
 * Check a list range constructor of the form
 *
 *	'[' expr .. expr ']'
 *
 * where the type of each expr must be integer and the return type is list of
 * integer.
 */
TypeStruct chkDotDotOp(nodep t, bool f) {
    TypeStruct t1,t2,rtn;
    nodep l,r;
    bool err = false;

    /*
     * Check each expr and complain if both arent int.
     */
    t1 = ResolveIdentType(
	chkExpr(l = t->components.binop.left_operand, f, null), t, true);
    t2 = ResolveIdentType(
	chkExpr(r = t->components.binop.right_operand, f, null), t, true);

    if ((t1 == null) or (t2 == null))
	return null;

    if (not isIntOrIntLit(t1)) {
	lerror(l, "Type of list range lower bound must be integer.\n");
	err = true;
    }
    if (not isIntOrIntLit(t2)) {
	lerror(r, "Type of list range upper bound must be integer.\n");
	err = true;
    }

    /*
     * Return int list type if all is OK.
     */
    if (not err) {
	rtn = BuildOpenArrayType(IntType, null);
	t->header.attachment.n2 = rtn;
	return rtn;
    }
    else
	return null;
}


/*
 * Check an elementwise list constructor of the form
 *
 *	'[' expr, ..., expr ']'
 *
 * where the type of each expr must be the same and the return type is a list
 * of the FIRST expr type.  We say FIRST in case of subtypes.  TODO: FIX THIS.
 *
 * In the case where one or more elements is a literal type, then all of the
 * elements must have the same literal base type, and the base type of the 
 * returned list is the literal base type.  TODO: I believe this latter
 * paragraph at least partially addresses the immediately preceding TODO.  This
 * will all get ironed out soon enough.
 */
TypeStruct chkListConstructor(nodep t, bool f) {
    nodep oprnd, expr;
    TypeStruct t1,t2;
    int err = 0, size = 0;
    TypeStruct rtn;

    /*
     * Return NilType if the expr list is empty. 
     */
    if (not (oprnd = t->components.unop.operand))
	return NilType;

    /*
     * Check the first expr in the list to get started.
     */
    if (not (t1 = chkExpr(oprnd->components.exprlist.expr, f, null)))
	return null;

    /*
     * Check the rest of the exprs in the list, noting if each is the same type
     * as the first.  Note that we use assmntCompat here, so we can allow lists
     * with subtype objects.  Note new -- assmntCompat is not now used.
     */
    for (expr = oprnd->components.exprlist.next, size = 1;
	    expr; expr = expr->components.exprlist.next, size++) {
	t2 = chkExpr(expr->components.exprlist.expr, f, null);
	if (not /*assmnt*/compat(t1, t2))
	    err++;
    }

    /*
     * Return a list of the expr type if all is OK.  Per top-level comment, if
     * the expr type is a literal, then return its base type.
     */
    if (not err) {
        if (isLiteralType(t1)) {
	    t1 = t1->components.type.kind.lit.type;
	}
	rtn = BuildOpenArrayTypeSize(t1, size, null);
	t->header.attachment.n2 = rtn;
	return rtn;
    }
    else {
	lerror(t, "Type of each expression in list constructor must be the same.\n");
	return null;
    }
}

/*
 * Check a tuple constructor of the form
 *
 *     '{' expr, ..., expr '}'
 *
 * by type checking each expr.  If each expr is OK, then return the tuple type
 * comprised of them else return null.
 */
TypeStruct chkTupleConstructor(nodep t, bool f) {
    nodep oprnd, expr;
    List* l = NewList();
    TypeStruct t1;
    bool allok = true;
    TypeStruct tt;

    /*
     * Outta here if the expr list is empty.  I.e., th'ain't so such thing as a
     * 0-tuple.
     */
    if (not (oprnd = t->components.unop.operand))
	return null;

    /*
     * Cruise the tuple constructor args, type checking each and sticking each
     * (confirmed) type on the list.
     */
    for (expr=oprnd; expr; expr=expr->components.exprlist.next) {
	tt = chkExpr(expr->components.exprlist.expr, f, null);
	t1 = ResolveIdentType(tt, expr, true);
	if (t1) {
	    PutList(l, (void*) t1);
	}
	else {
	    allok = false;
	}
    }

    if (allok) {
	return (oprnd->components.exprlist.type = BuildFullTupleType(l));
    }
    else {
	return null;
    }
}

/*
 * Build a complete tuple type comprised of the types in the given list.
 */
TypeStruct BuildFullTupleType(List* l) {
    TypeStruct t;
    void* le = EnumList(l);
    Symtab* st;
    nodep* prevnode;

    /*
     * Init things by calling BuildNewTupleTypeSized with the first elem of the
     * list and a size that's 20% bigger than the number of types.
     */
    t = BuildNewTupleTypeSized((nodep) le, 1.2 * ListLen(l), true);
    st = t->components.type.kind.record.fieldstab;

    /*
     * Cruise the rest of the types, adding a new tuple field for each.
     */
    prevnode = &(t->components.type.kind.record.fields->components.decl.next);
    for (le = EnumList(l); le; le = EnumList(l)) {
	EnterTupleField(st, (TypeStruct) le, false, t, &prevnode);
    }

    /*
     * 25dec00: This is outta here now.
     *
    t->components.type.kind.record.fields = 
	FixDeclList(t->components.type.kind.record.fields);
     *
     */

    return t;
}

/*
 *
 * For RSL, the qualident business is really secondary.  What's more important
 * is the way that ident types need to be chased down to their ground types.
 * E.g., in a var, parm decl, or field decl of the form
 *
 *     name: ident-type
 *
 * the symtab entry for name contains a pointer to an ident type, not what the
 * ident type resoves to as in Modula-2.  As noted elsewhere, the reason for
 * this is RSL's lack of declare-before-use constraint.  Given this, we must
 * dynamically lookup ident types, and follow through transitive references
 * until we get to a ground type, or null.
 *
 * Check a qualident of the general form:
 *
 *	M1.M2. ... .Mn.R1.R2. ... .Rn.ident
 *
 * where the Mi are module names and the Ri are records.  Both the Mi and Ri
 * may be missing.  If Mi and/or Ri are present, we traverse through all of
 * them.  If at any point the left operand of the '.' is neither a module nor
 * record, then we have an error.  An error is also signaled if the right
 * operand of the '.' is not a module export or record field, as appropriate.
 *
 * Syntactically, qualidents are built as lists, in contrast to designators,
 * which are built as left recursive expression trees.  As a result, we check
 * qualidents iteratively whereas we check designators recursively (see
 * chkRecordRef below).  This seems to be the path of least resistance, for
 * reasons that I dont feel like elaborating more fully at the moment.  The
 * main point is, it's largely an issule of syntactic convenience, paid for
 * with semantic inconvenience.
 */
TypeStruct chkIdent(
    nodep t,
    bool f)
{
    nodep ql, qr, errlocnode;
    SymtabEntry *syml, *symr;
    TypeStruct t1, t2;
    char *nl, *nr;
    nodep found_node;	/* Found node returned from LookupQid */

    /*
     * Lookup first (possible only) qid component and quit if not found.
     */
    if (not (syml = Lookup(nl = t->components.atom.val.text))) {
	lchastise(t, "%s is not defined in this scope.\n", nl);
	return null;
    }

    /*
     * Prepare to move into new symtab(s) by saving CurSymtab.
     */
    PushSymtab();
    
    /*
     * Traverse through module parts, if any.  This is just like LookupQid in
     * sym-aux.c, q.v.  We could probably merge the two with a common
     * subfunction if we thought about it.
     */ 
    for (ql = t, qr = t->components.atom.next;
	     qr; ql = qr, qr = qr->components.atom.next, syml = symr) {

	/*
	 * Confirm that left operand is a module.
	 */
	if (syml->Class != C_Module) {
	    break;
	}

	/*
	 * Move into the scope of the left operand.
	 */
	MoveToSymtab(syml->Info.Module.Symtab);

	/*
	 * Lookup right oprnd and confirm that it's a visible export of the
	 * left oprnd.
	 */
	symr = Lookup(nr = qr->components.atom.val.text);
	if ((not symr) or (not ChkSymFlag(symr, isExport))) {
	    lerror(qr, "%s is not an export of %s.\n", nr, syml->Symbol);
	    PopSymtab();
	    return null;
	}
    }

    /*
     * If we're checking a const expr, then ident must be a declared const or
     * an op name.
     */
    if (not f) {
	if ((syml->Class != C_Const) and (syml->Class != C_Enum)
	        and (syml->Class != C_Op) and 
	        (not ((syml->Class == C_Obj) and ChkSymFlag(syml, isDef)))) {
	    lerror(ql, "Identifier %s in constant expr is not a constannt.\n",
	syml->Symbol);
	    PopSymtab();
	    return null;
	}
	if (ql->components.atom.next != null) {
	    lerror(qr, "Constant identifiers may not be qualified.\n");
	    PopSymtab();
	    return null;
	}

	/*
	 * If syml->Type is null, try an incremental forward check of the value
	 * decl for syml.  If it succeeds, the call to chkValExprDecl will
	 * assign the checked type to sym->Type.  Note that this is only done
	 * for values, due to the kind of mutual dependencies that they may
	 * entail.
         */
	if (isValSym(syml)) {
	    chkValExprDecl(syml->Info.Obj.theTree, syml);
	}

	PopSymtab();
	return syml->Type;
    }

    /*
     * Traverse through record parts, if any, checking that each left operand
     * is a record, and each right operand is a field thereof.
     */
    for (; qr; ql = qr, qr = qr->components.atom.next, syml = symr) {

	/*
	 * Do a quick hack to make a new node for the possible error message
	 * loc, so that the '.' is reported as the location in the error
	 * message, instead of the left operand of the '.'.  This will make
	 * error message reporting for qualident synatx of record refs
	 * consistent with binop syntax.
	 */
	errlocnode = NewNode(BINOP_NODE, '.', ql->header.loc);
	errlocnode->header.loc.col += strlen(ql->components.atom.val.text);

	/*
	 * If syml->Type is module-qualified type, then Do a ResolveIdentType
	 * on it, otherwise use it as is.
         */
	if (not (t2 = ResolveIdentTypeAsOneTuple(
		syml->Type, errlocnode, true))) {
	    PopSymtab();
	    return null;
	}

	/*
	 * Confirm that left operand is a record and a var.
	 */
	if ((not isRecord(t2)) and (not isUnion(t2))) {
	    lerror(errlocnode,
		"Left operand of '.' is not a module, tuple, or union.\n");
	    PopSymtab();
	    return null;
	}
	if (not ((syml->Class == C_Var) or (syml->Class == C_Parm))) {
	    lerror(errlocnode,
		"Left operand of '.' is not a tuple or union variable.\n");
	    PopSymtab();
	    return null;
	}

	/*
	 * Move into the scope of the left operand.
	 */
	MoveToSymtab(t2->components.type.kind.record.fieldstab);

	/*
	 * Lookup right oprnd and confirm that it's a visible field of the left
         * oprnd.
	 */
	if (not (symr = Lookup(nr = qr->components.atom.val.text))) {
	    lerror(errlocnode,
		"%s is not a field of the tuple or union on the left of the '.'\n",
		nr);
	    PopSymtab();
	    return null;
	}
    }

    /*
     * Having traversed through any modules and/or records, syml is the entry
     * of the final (only) ident.
     */
    PopSymtab();

    /*
     * For a var, let var, parm, const, enum ident, or concrete object return
     * its type.  NOTE: this is NOT where we resolve ident types.
     */
    if ((syml->Class == C_Var) or (syml->Class == C_Parm) or
	    (syml->Class == C_Let_Var) or
	    (syml->Class == C_Const) or (syml->Class == C_Enum) or
	    ((syml->Class == C_Obj) and (ChkSymFlag(syml, isDef))))
	return syml->Type;

    /*
     * Handle the case of a proc name as a designator for an unevaluated proc
     * body rather than an invocation.
     */
    if (syml->Class == C_Proc) {
	/*
	 * First, handle the restructions: no built-ins and no nesteds.
	 */
	if (syml->Level <= 1) {
	    lerror(ql, "Built-in procedures cannot be used as procedure values.\n");
	    return null;
	}
	if (syml->Level > 2) {
	    lerror(ql, "Locally nested procedures cannot be used as procedure values\n");
	    return null;
	}
	return syml->Info.Proc.FType;
    }

    /*
     * For RSL, handle the case where we have an declared op id.
     */
    if (syml->Class == C_Op) {
	return syml->Info.Op.OpType;
    }

    /*
     * Also for RSL, handle the case of a concrete obj, which is OK as a value
     * denotation.
     */
    /* Later. */
    /* Update -- this seems already to be handled above in the isDef chk. */

    /*
     * Check if ident is a module name, in which case just return NULL.  This
     * will mean that if the module name is used in any context other than
     * qualified ref, a banal but appropriate error message will appear.
     */
    if (isModuleIdent(syml))
	return null;

    /*
     * At this point, we have an ident that's not a var, parm, const, proc, 
     * concrete object, or module.  Since we're being called in an expression
     * context, we have an error.
     */
    lerror(ql, "Identifier %s erroneously used as a variable.\n",
	syml->Symbol);
    return null;
}

/*
 * Check if the given symtab entry is that of a module ident.  A module ident
 * is distinguished from a possible entity def of the same name by prefixing
 * the module name with "M$".  This is done in sym-aux.c:chkImports1, q.v.
 */
bool isModuleIdent(SymtabEntry* sym) {
    char* name = sym->Symbol;
    char* mname;

    mname = strcat(strcpy((char*)malloc(strlen(name) + 3), "M$"), name);
    return LookupString(mname) != null;
}

/*
 * If the given type is an ident type, resolve to its ground type, including
 * chasing through transitive defs.  If the given type is something else, just
 * return it as is.  Note that this resolution must be done for all ident types
 * during the type checking pass, since the first pass left all of them
 * unresolved.
 *
 * Here is (almost) precisely how the resolution is carried out:
 *
 *    (1) Let sym = Lookup(type)
 *    (2) If sym->Type is another ident type, goto step 1
 *    (3) At this point, there are three possibilitis:
 *	  (a) sym == null, in which case this type is undefined,
 *		so we issue an error message and return null
 *	  (b) sym->Type == null, in which case this is an opaque type,
 *		so we return type
 *	  (c) isBuiltIn is set in sym->Flags, in which case this is a built-in
 *		 type (e.g., integer), so we return sym.
 *
 * This processing is rather wasteful timewise and could be avoided with a
 * separate resolution pass.  However, it is unclear if such a pass would end
 * up providing a net time savings.  Further, it is unclear if this incremental
 * resolution really adds a measurable amount of processing time, from the
 * users perspective.  We'll need to see how things go.
 *
 * A noteworthy consideration in this regard is if we add coarity overloading,
 * then we'd need another pass for it, during which we could do ident type
 * resolution.  So, it seems, if we need another pass for something else in
 * future, then we can do type resolution then, but adding a separate pass for
 * type resolution only is probably not worth it.  Again, we'll see.
 *
 * One last bit of caca to do here -- resovle int lit type to int (int lit is a
 * remnant of Mod-2).
 */
TypeStruct ResolveIdentType(
    TypeStruct t,	/* Any type struct */
    nodep errlocnode,	/* Node for error message location */
    bool doerror)	/* True if error message should be issued */
{
    return ResolveIdentType1(t, errlocnode, doerror, false, false);
}


/*
 * Just one step short of ResolveIdentType.  Here we stop at the last ident
 * type in a possibly transitive chain.
 */
TypeStruct ResolveToBaseIdentType(
    TypeStruct t,	/* Any type struct */
    nodep errlocnode,	/* Node for error message location */
    bool doerror)	/* True if error message should be issued */
{
    return ResolveIdentType1(t, errlocnode, doerror, true, false);
}


/*
 * Version of ResovleIdentType called from chkRecordRef to leave ident type as
 * one tuple if it is one so we can select its one component, if that's what
 * the user wants.  The normal version of ResolveIdentType will descend all the
 * way through one-tuples, since no one but chkRecordRef ever cares about their
 * tupleness.  Clear enough?
 */
TypeStruct ResolveIdentTypeAsOneTuple(
    TypeStruct t,	/* Any type struct */
    nodep errlocnode,	/* Node for error message location */
    bool doerror)	/* True if error message should be issued */
{
    return ResolveIdentType1(t, errlocnode, doerror, false, true);
}


/*
 * Common workdoer for ResolveIdentType, ResovleToBaseIdenType, and
 * ResolveIdentTypeAsOneTuple.
 */
TypeStruct ResolveIdentType1(
    TypeStruct t,	/* Any type struct */
    nodep errlocnode,	/* Node for error message location */
    bool doerror,	/* True if error message should be issued */
    bool tobase,	/* True if reslution should go just to base ident type,
			 * not all the way to the base type struct. */
    bool rtnonetuple)	/* True if we should return one-tuples without
			 * descending into them. */
{
    SymtabEntry* sym;
    char* name, *origname, *nr;
    TypeStruct t1,ti,to,ti2;
    bool onetupling = false, moduled;
    nodep ql, qr;
    SymtabEntry *syml, *symr;

    /*
     * If one-tuple, descend on down if we should.
     */
    ti = null;
    if (isOneTuple(t) /*and (not rtnonetuple)*/) {
	ti = t;
	t = t->components.type.kind.record.fields->
	    components.decl.kind.field.type;
    }

    /*
     * If not ident type, outta here.
     */
    if (not isIdentType(t)) {
	return ti ? ti : t;
    }

    /*
     * Save starting name in possible transitive chain of names.
     */
    t->components.type.origname = t1 = t->components.type.kind.ident.type;
    name = origname = t1->components.atom.val.text;

    while (true) {
	if (not (sym = Lookup(name))) {

	    /*
	     * 23nov10 update: The following block of commented out code is
	     * evidently total doodoo, since  the regression tests run fine
	     * without it.  It may well be old Modula-2 code, or code that is
	     * no longer relied upon.  The bit about using a name that's an
	     * export of an imported module is definitely doodoo, since we no
	     * longer have whole-module imports in SpecL.
	     *
	     * Don't output an error if the original name is an import, but we
	     * can't find one of the types it equates with.  This prevents the
	     * annoyance of having to import both a type as well as its only
	     * component type if the original type is a one tuple.  Note well
	     * that a "feature" of Lookup is to return imports "resolved" to
	     * thier exporting symbol, which means that an imported symbol will
	     * have isExport true, not isImport.  Whatever.  It works if you
	     * get it.
             *
	    if (name and origname and (not streq(name, origname)) and
		    ChkSymFlag(Lookup(origname), isExport)) {
		if (sym = Lookup(origname))
		    return sym->Type;
		else
		    return null;
	    }
	     *
	     * Check if origname is an export of any imported module, and if so
	     * use it.
	     *
	    else if (ti2 = ChkForImportedType(name)) {
		return ti2;
	    }

	     *
	     * Otherwise report an error.
	     *
	    else {
	     */
		if (doerror)
		    lchastise(errlocnode, "Type %s is not defined.\n", origname);
		return null;
	    /*
	    }
	    */
	}
        
	/*
	 * Cruise through the module qualifying prefix, if any, up to the first
	 * non-module.  The code to do this was lifted from chkIdent, and
	 * should be functionized, but hey, I'm lazy.
	 */
        PushSymtab();
	for (ql = t1, qr = t1->components.atom.next, syml = sym, moduled = false;
		 qr; ql = qr, qr = qr->components.atom.next, syml = symr) {

	    /*
	     * Confirm that left operand is a module.
	     */
	    if (syml->Class != C_Module) {
		break;
	    }

	    /*
	     * Set flag to indicate that we've done a module descent.  This is
	     * for proper error messaging on origname.
 	     */
	    moduled = true;

	    /*
	     * Move into the scope of the left operand.
	     */
	    MoveToSymtab(syml->Info.Module.Symtab);

	    /*
	     * Lookup right oprnd and confirm that it's a visible export of
	     * the left oprnd.
	     */
	    symr = Lookup(nr = qr->components.atom.val.text);
	    if ((not symr) or (not ChkSymFlag(symr, isExport))) {
		if (doerror) {
		    lerror(errlocnode,
			"%s is not an export of %s.\n", nr, syml->Symbol);
		}
		PopSymtab();
		return null;
	    }
	}

	/*
	 * If we've done the module prefix thing, adjust t1, etc.
	 */
	if (moduled) {
	    t1 = ql;
	    name = origname = t1->components.atom.val.text;
	    sym = syml;
	}

	if (not ((sym->Class == C_Type) or (sym->Class == C_Obj))) {
	    if (doerror)
		lerror(errlocnode, "Identfier %s is not a type.\n", name);
	    PopSymtab();
	    return null;
	}

	if (ChkSymFlag(sym, isBuiltIn) or (not isIdentType(sym->Type))) {
	    if (isIntLit(sym->Type)) {
		PopSymtab();
		return IntType;
	    }
	    /*
	     * Check if we`ve got a one-tuple and should descend into it.
	     */
	    else if (isOneTuple(sym->Type) and (not rtnonetuple)) {
		to = sym->Type->components.type.kind.record.fields->
		    components.decl.kind.field.type;

		/*
		 * Check further if one-tuple field is an ident type.
		 */
		if (isIdentType(to)) {
		    /*
		     * If it is an ident type, then prepare to join continuing
		     * logic below.
		     */
		    onetupling = true;
		    t1 = to->components.type.kind.ident.type;
		}
		else {
		    /*
		     * If one-tuple field is not an ident type, then just
		     * return that type.  This is what would happen in the else
		     * immediately below if we hadn't done the one-tuple
		     * descent.
		     */
		    PopSymtab();
		    return to;
		}
	    }
	    else {
		//return sym->Type;
		//return NewDerivedIdentType(sym->Type, origname);
		PopSymtab();
		TypeStruct newdtype = NewDerivedIdentType(sym->Type, origname, name);
		return newdtype;
	    }
	}

	if (not onetupling)
	    t1 = sym->Type->components.type.kind.ident.type;
	else
	    onetupling = false;

	if (t1->header.kind == ATOM_NODE) {
	    name = t1->components.atom.val.text;
	}
	else {
	    if (tobase) {
		PopSymtab();
		return t1;
	    }
	    else {
		PopSymtab();
		return /*NewDerivedIdentType*/
		    sym->Type->components.type.kind.ident.type/*, origname)*/;
	    }
	}

	/*
	 * Check for unresolved recursion.
	 */
	if (name == origname) {
	    if (doerror)
		lerror(errlocnode,
		    "Unresolved recursive type definition of %s.\n", name);
	    PopSymtab();
	    return null;
	}

	PopSymtab();
    }
}

/*
 * Check if the given string name is the name of a type exported from an
 * imported module.
 */
TypeStruct ChkForImportedType(char* name) {
    Symtab* symt;
    nodep im, names;

    /*
     * Find the containing module symtab.
     */
    for (symt = CurSymtab; symt && symt->ParentEntry &&
	symt->ParentEntry->Class != C_Module;
	    symt = symt->ParentTab)
	;

    /*
     * Bail if we get no where (not quite sure if this can ever happen, but
     * defense, defense, defense.
     */
    if (not symt) return null;

    /*
     * Cruise the imports list of the module symtab, going into each imported
     * module to see if name is an exported type.  For now, don't check if
     * there's more than one possibility, just return the first one that's
     * found.   TODO -- fix this, in conjunction with the general makeover of
     * imports.
     */
    PushSymtab();
    for (im = symt->Imports; im; im = im->components.decl.next) {

	/*
	 * If the import decl has a from clause, then checking has already been
	 * done, however we need to do differently here.  This is where we
	 * invoke the rule that says that a module in from clause is itself
	 * imported, making all of its exports available for qualified
	 * referece.  Hence, we won't look in the names list that accompanies
	 * the from clause, but rather go straight to the module from clause.
	 * For that module, we check if name is an export, and if so check if
	 * name is defined in the module.  Got it?
	 */

/*
	if (im->components.decl.kind.import.from) {
	    printf("Import from: %s\n",
	        im->components.decl.kind.import.from->
		    components.atom.val.text);
	}
 */

/*
	if (im->components.decl.kind.import.names) {
	    for (names = im->components.decl.kind.import.names; names;
		     names = names->components.atom.next) {
		         printf("Name: %s\n",
			     names->components.atom.val.text);
	    }
	}
 */
    }

    PopSymtab();
    return null;
}

/*
 *
 * 18jan07: The hacking continues.  Didn't really figure out what the f is
 * going on, but added a parm to support the codegen.c:MakeJavaType.  The
 * problem was that ResolveToBaseIdentType was working as seemingily
 * advertised, in that it returns a non-ident type in the end.  So, what would
 * have been the "last" ident type in a transitive chain is sent in here as the
 * rname parm, and put in the (newly added today) resolvedname component of a
 * TYPE_NODE.
 *
 * 31may04: I don't know what the f is going on here.  The 6may02 comment seems
 * to indicate that this code should still be functional, but as of 31may04,
 * everthing below the "return t" is commented out.  The problem that has now
 * arisen is that with fixes to chkInOp, the origname component of the incoming
 * to needs to be set.  I still don't know if other parts of this code should
 * be happening or not, but fixing the origname thing is fixing the immediate
 * problem.
 *
 * 6may02 Update: It looks as if the assumption of this being able to go away
 * was incorrect, at least insofar as resolving list subtypes is concerned.
 * The particular problem that resurected this is the reassign function in the
 * example classes/530/examples/semantics/sil.rsl.attr. q.v.
 *
 * OLD (now incorrect comment: Hopefully, this has also gone the way of
 * isNonIdentIdentType below, of q.v.  the comment.
 */
TypeStruct NewDerivedIdentType(TypeStruct t, char* origname, char* rname) {
    TypeStruct rtn = NewNode(TYPE_NODE, Yident, EmptyLoc);
    TypeStruct t1;

    if (t and (not t->components.type.origname)) {
	t->components.type.origname = NewNode(ATOM_NODE, Yident, EmptyLoc);
	t->components.type.origname->components.atom.val.text = origname;
    }
    if (t) {
        t->components.type.resolvedname = stralloc(rname);
    }
    return t;

//    rtn->components.type.kind.ident.type = t;
//    rtn->components.type.origname = t1 = NewNode(ATOM_NODE, Yident, EmptyLoc);
//    t1->components.atom.val.text = origname;
//    rtn->components.type.isDerivedIdentType = true;
//    return rtn;
}


/*
 * Adding a the generic name field to type nodes eliminates the need for this
 * proc, for now anyway.
 * 
 * Hack city!  Here we're checking to see if we have an ident type that isn't
 * really an ident type because it's one of those funky non-tuple single-field
 * tuple types that's built as an ident type so that inheritance resolution can
 * know the name field of the would-be single-field tuple.  Hope you know what
 * the f is going on here.
 */
bool isNonIdentIdentType(TypeStruct t) {
    return (t and (t->header.name == Yident) and
	t->components.type.kind.ident.type and
	    (t->components.type.kind.ident.type->header.kind != ATOM_NODE));
}


/***
 ** Check the types.
 **/

/*
 * Check a type idetifier by looking it up.  Note that in contrast to Mod-2, we
 * do need to check that the type is defined, since we do not have the
 * declare-before-use policy.
 */
TypeStruct chkIdentType(
    nodep t)
{
    SymtabEntry *s;
    nodep found_node;	/* Found node returned from LookupQid */

    if (s = LookupQid(t->components.type.kind.ident.type, &found_node))
	return s->Type;
    else {
	lerror(t, "Object %s is undefined.\n",
	    t->components.type.kind.ident.type);
	return null;
    }
}


/*
 * Check an enumeration type.  Nothing to do here but set the type size and
 * tag.  All the rest of the work was done in sym-aux.c:EnterEnumIdents, q.v.
 */
TypeStruct chkEnumType(
    nodep t)
{
    t->header.attachment.count = sizeof(int);
    t->components.type.tag = IntTag;	/* Valuewise, an enum is an int. */
    return t;
}


/*
 * Check a subrange type.  The base type, if given, must be subrangeable and
 * the upper and lower bounds types must be compatible.  Also, if no base type
 * is explicitly declared, then it must be inferred from the bounds' type.
 *
 * Legal subrangeable types are card, int, longint, char, and enum.  Note that
 * we disallow subranges of subranges.  Even though these would make semantic
 * sense, a strict reading of Wirth seems to indicate that subrange types are
 * not themselves subrangeable.
 */
TypeStruct chkSubrangeType(
    nodep t)
{
    TypeStruct t1,t2,bt;	/* Typical subtree pointers */

    /*
     * Check that declared basetype, if given, is subranageable, i.e., it's a
     * card, int, longint, char, or enum.  Note that the subrange base type is
     * syntactically a qualident, so its checking was handled already by
     * LookupType in the SubrangeType action routine in parser.y, q.v.
     */
    if (t->components.type.kind.subrange.basetype) {
	if (not isSubrangeable(t->components.type.kind.subrange.basetype)) {
	    lerror(t,
	      "The base type of a subrange must be card, int, longint, char, or enum.\n");
	    return null;
	}
    }

    /*
     * Check that the upper and lower bounds are compatible types.
     */
    t1 = chkConstExpr(t->components.type.kind.subrange.lower);
    t2 = chkConstExpr(t->components.type.kind.subrange.upper);
    if (not compat(t1,t2)) {
	lerror(t, "Subrange upper and lower bounds are not compatible.\n");
	return null;
    }

    /*
     * Check that the range types are compatible with the decl'd base type, if
     * given.
     */
    if (t->components.type.kind.subrange.basetype) {
	if (not compat(t1, t->components.type.kind.subrange.basetype)) {
	    lerror(t, "Subrange upper and lower bounds are not compatible with declared base type\n");
	    t->components.type.kind.subrange.basetype = null; /* for later chks */
	    return null;
	}
    }
    else {
    /*
     * If no base type given explicitly in decl, derive it from the range
     * types.  Base type derivation rules are:
     *    (1) if lower bound is negative integer, then base type = integer
     *    (2) if lower bound is cardinal (including IntLit), then base type =
     *        cardinal
     *    (3) otherwise, base type = type of lower (and upper) bound.
     */
	if (isNegInt(t->components.type.kind.subrange.lower))
	    bt = t->components.type.kind.subrange.basetype = IntType;
	else if (isIntLit(t1) and isIntLit(t2))
	    bt = t->components.type.kind.subrange.basetype = CardType;
	else
	    bt = t->components.type.kind.subrange.basetype = t1;
    }

    /*
     * To facilitate subsequent sizing, compute the numeric values of the upper
     * and lower bounds.  While it's at it, it computes the type size.
     */
    t->header.attachment.count = ComputeSubrangeBounds(t);

    /*
     * Valuewise, a subrange value is a value of its basetype.
     */
    if (isCard(bt) or isInt(bt) or isEnum(bt))
	t->components.type.tag = IntTag;
    else if (isLongInt(bt))
	t->components.type.tag = LIntTag;
    else if (isChar(bt))
	t->components.type.tag = CharTag;
    else if (isBool(bt))
	t->components.type.tag = BoolTag;

    return t;
}


/*
 * Compute the numeric values of subrange bounds.
 */
int ComputeSubrangeBounds(
    nodep t)
{
    nodep bt;
    ValueStruct uv, lv;

    bt = t->components.type.kind.subrange.basetype;
    uv = interpExpr(t->components.type.kind.subrange.upper);
    lv = interpExpr(t->components.type.kind.subrange.lower);

    if (isNumeric(uv->type)) {
	t->components.type.kind.subrange.upperval = uv->val.IntVal;
	t->components.type.kind.subrange.lowerval = lv->val.IntVal;
	return sizeof(int);
    }
    else if (isChar(uv->type)) {
	t->components.type.kind.subrange.upperval = (int) uv->val.CharVal;
	t->components.type.kind.subrange.lowerval = (int) lv->val.CharVal;
	return sizeof(char);
    }
    else {
	t->components.type.kind.subrange.upperval = (int) uv->val.BoolVal;
	t->components.type.kind.subrange.lowerval = (int) lv->val.BoolVal;
	return sizeof(bool);
    }
}


/*
 * Type check an array type.  The declared bounds are recursively type checked
 * and checked for legality -- bounds must be one of the types char, bool,
 * enum, or subrange.
 *
 * To facilitate subsequent checking, a multi-dimensional array type decl of
 * the form:
 *
 *    array A[d1, d2, ..., dn] of t
 *
 * is converted to an explicit type struct corresponding to the form:
 *
 *    array A[d1] of array[d2] of ... array[dn] of t
 *
 * This will mean that only one-dimensional array type checking is necessary.
 * This will also make life easier at runtime.
 */
TypeStruct chkArrayType(
    nodep t)
{
    TypeStruct t1, base, at, b, n;
    bool clash = false;
    int size, size1;
    int lbval;

    /*
     * Check the base type and save it for the conversion to follow.
     */
    base = chkType(t->components.type.kind.arraytype.basetype);

    /*
     * Check each dimension recursively.
     */
    t = chkArrayType1(t, base, 1);

}

/*
 * This is the tail-recursive subfunction that does the multi-d conversion and
 * computes the size of each bound.  Return from here is the array type at the
 * appropriate dimension, including the size and integerized lower bound value.
 * For all but the top-level dimension, a new array type is constructed.
 *
 * We use tail recursion because we need to get all the way down to the
 * innermost bound to start computing sizes.  If we proceeded iteratively from
 * the outermost bound, we would not compute the sizes of the inner dimensions
 * correctly.
 */
TypeStruct chkArrayType1(
    TypeStruct t,
    TypeStruct base,
    int level)
{
    nodep nd;
    TypeStruct nt, bt, bndt;
    int size, lbval, nubval;

    /*
     * Compute the base array type for the next dimension down if there is one.
     */
    if (nd = t->components.type.kind.arraytype.bounds->components.decl.next) {
	nt = NewNode(TYPE_NODE, YARRAY, t->header.loc);
	nt->components.type.kind.arraytype.bounds = nd;
	bt = chkArrayType1(nt, base, level + 1);
    }
    else
	bt = base;

    /*
     * Type check the bound at this dim.  If it doesn't check, the bound type
     * at this dim will be null.  It doesnt really matter what we do with a bad
     * bounds type, since we'll not make it to runtime with it anyway.  In
     * future, we might so we'll keep things orderly.
     */
    bndt = chkType(t->components.type.kind.arraytype.bounds->
				components.decl.kind.type.type);

    /*
     * Check that bound type is one of the allowables:
     *	char, bool, enum, or subrange.
     */
    if (not isIndexWorthy(bndt)) {
	lerror(bndt,
	    "Type of array index must be char, bool, enum, or subrange.\n");
	bndt = null;
	lbval = 0;
	nubval = 0;
    }
    else {
	size = IndexSize(bndt, &lbval, &nubval);
    }

    /*
     * Install all the new information for this dimension:
     *    (a) the checked bound as the new single bound type,
     *    (b) the checked base as the new base type,
     *    (c) the cummulative size of the type at this dim,
     *	  (d) the integerized value of the lower bound,
     *	  (e) the normalized value of the lower bound,
     *    (f) StructTag as the value of the type tag.
     */
    t->components.type.kind.arraytype.bound = bndt;
    t->components.type.kind.arraytype.basetype = bt;
    t->header.attachment.count = size * TypeSize(bt);
    t->components.type.kind.arraytype.lowerboundval = lbval;
    t->components.type.kind.arraytype.normalizedubval = nubval;
    t->components.type.tag = ListTag;

    /*
     * Return the fixed up type at this dimension as the type to be used as the
     * base type at the next dimension up.
     */
    return t;
}


/*
 * Compute the number of elements specified by an array index type.  Also
 * compute the numeric value of the lower bound in the given array type struct.
 * Also compute the normalized upper bound value, that is the upper bound val
 * based on a lower bound of 0.  This is used at runtime to quicken bounds
 * and facilitate open array parm binding.
 */
int IndexSize(
    TypeStruct t,	/* Bounds type. */
    int *lbval,		/* Lower bound val to be computed. */
    int *nubval)	/* Normalized upper bound val to be computed. */
{
    if (isSubrange(t)) {
	*lbval = t->components.type.kind.subrange.lowerval;
	return (*nubval = t->components.type.kind.subrange.upperval - *lbval)
			+ 1;
    }
    *lbval = 0;
    if (isEnum(t)) {
	return (*nubval = t->components.type.kind.enumtype.size - 1) + 1;
    }
    if (isChar(t)) {
	return (*nubval = 255) + 1;
    }
    if (isBool(t)) {
	return (*nubval = 1) + 1;
    }
}


/*
 * Type check a record type by recursively checking each of its fields.
 * Syntactically, the record type is a field list sequence of the form:
 *
 *	fieldlist[1]; ...; fieldlist[k]
 *
 * where each fieldlist is either a plain field list or a variant part.  These
 * two forms are handled in the functions chkPlainField and chkVariantPart that
 * follow.
 *
 * To facilitate subsequent checking, a symtab structure is built from the type
 * struct tree for the record.  In this structure, a symtab is alloc'd for the
 * record, and a symtab entry is made for each element in each fieldlist in the
 * sequence.  The size of the symtab was determined in the first pass when the
 * total number of record fields was computed.
 *
 * Note that a record symtab is rooted in a type node in a parse tree, not in
 * the current scope's symtab.  And, since record types are anonymous, there's
 * no way to give them a named parent entry.  But, we do give them a generic "A
 * Record" parent entry name in case we want to dump the tables for debugging
 * purposes.
 */
TypeStruct chkRecordType(
    nodep t)
{
    Symtab *st;
    bool chk;    

    /*
     * Alloc the record symtab.
     */
    PushSymtab();
    t->components.type.kind.record.fieldstab = (st =
	AllocSymtab( (int) (1.2 * t->components.type.kind.record.numfields + 3)));
    st->ParentTab = CurSymtab;
    st->ParentEntry = ARecordEntry;
    st->Level = CurSymtab == (Symtab *)0 ? 0 : CurSymtab->Level + 1;
    st->Offset = 0;
    MoveToSymtab(st);

    /*
     * Recursively type check the fieldlist sequence.  The allocation of symtab
     * entries will happen in chkPlainFieldList and chkVariantPart, defined
     * below.
     */
    chk = chkFieldListSeq(t->components.type.kind.record.fields);

    /*
     * Store the type size and tag of the record in the tree.
     */
    if (chk) {
	t->header.attachment.count = CurSymtab->Offset;
	t->components.type.tag = StructTag;
	PopSymtab();
	return (TypeStruct) t;
    }
    else {
	PopSymtab();
	t->components.type.tag = StructTag;
	return (TypeStruct) t;
    }
}


/*
 * Type check a field list sequence.
 */
bool chkFieldListSeq(
    nodep t)
{
    int err;
    nodep fl;

    /*
     * Save current offset, which will be used as 
     */
    for (err = 0, fl = t; fl; fl = fl->components.decl.next) {
	switch (fl->header.name) {
	    case ':':
		if (not chkPlainFieldList(fl))
		    err++;
		break;
	    case 0:
		break;
	}
    }
    return (not err);
}


/*
 * Type check a plain field list decl of the form:
 *
 *	name[1], ..., name[k] : type;
 *
 */
bool chkPlainFieldList(
    nodep t)
{
    nodep id;
    TypeStruct ft;
    SymtabEntry *s;
    int err;

    /*
     * Check the field type.
     */
    ft = chkType(t->components.decl.kind.field.type);

    /*
     * Alloc a symtab entry for each name in the field list, even if field type
     * is null.  This is precisely the same as is done for a normal var decl.
     */
    for (err = 0, id = t->components.decl.kind.field.vars;
		id; id = id->components.atom.next) {
	if (not EnterVar(id, ft))
	    err++;
	s = Lookup(id->components.atom.val.text);
	s->Info.Var.Offset = CurSymtab->Offset;
	CurSymtab->Offset += TypeSize(ft);
    }

    return (ft and (not err));
}


/*
 * Type check a proc type of the form:
 *
 *	procedure n(t1,..., tk): tr;
 *
 * by constructing a symtab signature that parallels that built for a proc decl
 * in chkProcDecl above.  This will facilitate subsequent type checking of
 * calls to proc-type vars.
 */
TypeStruct chkProcType(
    nodep t)
{
    nodep tp;		/* Parse tree node for each formal parm type. */
    SymtabEntry *ap;	/* New symtab entry for each formal parm type. */
    SymtabEntry **prev;

    /*
     * Make a SymtabEntry signature out of the proc type tree.
     */
    t->components.type.kind.proc.formalchain = null;
    for (tp = t->components.type.kind.proc.formals,
	 prev = &(t->components.type.kind.proc.formalchain);
	   tp;
	     tp = tp->components.decl.next,
	     prev = &(ap->Info.Parm.Link)) {
	ap = AllocSymtabEntry(null, C_Parm,
		LookupType(tp->components.decl.kind.parm.type),
		CurSymtab->Level);
	if (tp->components.decl.kind.parm.isvar)
	    SetSymFlag(ap, varParm);
	*prev = ap;
	ap->Info.Parm.Link = null;
    }

    t->header.attachment.count = sizeof(char *);
    t->components.type.tag = ProcTag;
    return t;
}


/*
 * NOTE: This is still Mod-2 compat, which is overkill for RSL.  We'll fix,
 * along with everything else, in the rewrite.  The Mod-2 comment follows.
 *
 * Compatibility predicate.  Two types, t1 and t2, are compatible if:
 *    (1) they are eqivalent, or
 *    (2) one is a subrange of the other,
 *    (3) both are subranges with the same base type.
 *    (4) one is of type char and the other a string literal of length 1
 *    (5) one is of type pointer and the other the literal 'nil'
 * Also, the special case of integer literals must be handled.  Viz., an int
 * literal is compatible with int, card, or any subrange of either.
 */
bool compat(TypeStruct t1, TypeStruct t2) {
    /*
     * First check if either type is null, which means a type checking error
     * has occurred, and we just propagate it
     */
    if ((t1 == null) or (t2 == null))
	return null;

    /*
     * Next check if types are equivalent (i.e., the same type).  For RSL, we
     * must chase pointers to do name equiv, given forward refs and lack of
     * desire to go to three passes.
     *
     * Formerly, i.e., for Mod-2, this check was done by pointer comparison,
     * given decl-before use policy.  I.e., we simply did the following:

     *     if (t1 == t2)
     *         return true;
     *
     * We can still do this, but we must also resolve ident types if this
     * doesnt work.
     */
    if (t1 == t2)
	return true;

    /*
     * Return true if t1 and t2 are the same ident, or in a transitive chain of
     * equal idents.
     */
    else if (identCompat(t1, t2))
	return true;

    /*
     * Return true if t1 and t2 are literal compatible.  This is the general
     * case of lit compt, in which any combination of literal and base type are
     * considered compat.  This general case is "retracted" in assmntCompat,
     * q.v.
     */
    else if (litCompat2(t1, t2))
	return true;

    /*
     * Deprecated, and scheduled for removal
     *
    else if (symlitCompat(t1, t2))
	return true;
     */

    /*
     * OK, we bite the bullet at last and do structural equiv.
     */
    else if (structCompat(t1, t2))
	return true;

    /*
     * One-tuple compat, i.e., T = {T}
     */
    else if (onetupleCompat(t1, t2))
	return true;

    /*
     * If not compat so far, check if otherwise compatible.
     */
    else
	return
	    ((isNil(t1) or isNil(t2)) or
/*
 * The following are all remnants of Mod-2 and can be purged.  They're left
 * here for historical observation, for the time being.
 *
	     (isNumeric(t1) and isNumeric(t2)) or
	     (isIntLit(t1) and
		  (isIntOrCardOrSubrangeOfEither(t2))) or
	     (isIntLit(t2) and
		  (isIntOrCardOrSubrangeOfEither(t1))) or
	     (isIntLit(t1) and isIntLit(t2)) or
	     (isSubrange(t1) and
		  (t1->components.type.kind.subrange.basetype == t2)) or
	     (isSubrange(t2) and
		  (t2->components.type.kind.subrange.basetype == t1)) or
	     (isSubrange(t1) and isSubrange(t2) and
		  (t1->components.type.kind.subrange.basetype ==
			t1->components.type.kind.subrange.basetype)) or
	     (isString(t1) and isString(t2)) or
	     (isChar(t1) and isStringChar(t2)) or
	     (isStringChar(t1) and isChar(t2)) or
 */
	     (isNil(t2) and isNil(t1))
	    );
}

/*
 * Two-way compat, i.e., compat(t1,t2) or compat(t2,t1).
 */
bool compat2(TypeStruct t1, TypeStruct t2) {
    return compat(t1,t2) or compat(t2,t1);
}

/*
 * Return true if t2 < t1.
 */
bool subtypeCompat(TypeStruct t1, TypeStruct t2) {
    char* parentname;
    TypeStruct wp;
    bool rtn;

    if (not (isOrWasIdentType(t1) or isOrWasIdentType(t2)))
	return false;

    /*
     * Protect against origname being null, which will happen with list or
     * tuple literals as actual parameters.
     */
    if ((not t1->components.type.origname) or
	    (not t2->components.type.origname))
	return false;

    if (rtn = subtypeCompat1(
	t1->components.type.origname->components.atom.val.text,
	    t2->components.type.origname->components.atom.val.text))
	return rtn;

    /*
     * Check explicit instantiated type parent pointer, which was set in
     * where.c:InstantiateWhereDef, q.v.
     */
    if (wp = t2->components.type.whereparent)
	return subtypeCompat(t1, wp);

    return false;
}


/*
 * Work doer for subtypeCompat (t2<t1).  Also called elsewhere when convenient.
 */
bool subtypeCompat1(char* parentname, char* childname) {
    nodep nextparentnode;
    TypeStruct nextparenttype;
    char* nextparentname;
    SymtabEntry* childsym;

    /*
     * Lookup t2 and upchuck if not found.
     */
    if (not (childsym = Lookup(childname)))
	return false;

    /*
     * Cruise across and up parent chain of childsym, looking for parentname.
     */
    for (nextparentnode = childsym->Info.Obj.inheritsfrom;
	    nextparentnode;
		nextparentnode = nextparentnode->components.atom.next) {
	if (parentname ==
		nextparentnode->components.atom.val.text)
	    return true;
    }

    for (nextparentnode = childsym->Info.Obj.inheritsfrom;
	    nextparentnode;
		nextparentnode = nextparentnode->components.atom.next) {

	if (subtypeCompat1(parentname,
		nextparentnode->components.atom.val.text))
	    return true;
    }

    /*
     * If child type is a non-built-in ident type, then transitively check
     * through its def.
     */
    if (isIdentType(childsym->Type) and
	    (not ChkSymFlag(childsym, isBuiltIn))) {
	return subtypeCompat1(parentname,
	    childsym->Type->components.type.kind.ident.type->
		components.atom.val.text);
    }

    /*
     * Transitively, we could have come to t1 = t2.  It seems that this is a
     * bit inefficeient, but cant see the more efficient way at the moment.
     * Maybe in the (imaginary) rewrite.
     */
    if (streq(childname, parentname))
	return true;

    return false;
}


/*
 * More probably-superfluous ident-type-resolution-related stuff.  This MUST
 * ALL BE CLEANED UP.
 */
bool isOrWasIdentType(TypeStruct t) {
    return (isIdentType(t) or t->components.type.origname);
}


/*
 * Here we are at long last -- the structural equivalencer.
 */
bool structCompat(
    TypeStruct t1, TypeStruct t2)	/* Type structs to compare */
{
    nodep f1, f2;			/* Tuple fields to compare types of */

    t1 = ResolveIdentType(t1, null, false);
    t2 = ResolveIdentType(t2, null, false);

    if (t1 and t2) {

	switch (t1->header.name) {
	    case YRECORD:
		if (t1->components.type.kind.record.numfields !=
			t2->components.type.kind.record.numfields)
		    return null;
		for (f1 = t1->components.type.kind.record.fields,
		     f2 = t2->components.type.kind.record.fields;
			 f1;
			     f1 = f1->components.decl.next,
			     f2 = f2->components.decl.next) {
		    if (not compat(f1->components.decl.kind.field.type,
			    f2->components.decl.kind.field.type))
			return false;
		}
		return true;

	    case YLIST:
	    case YARRAY:
		if ((t2->header.name == YLIST) or (t2->header.name == YARRAY)) {
		    return compat(
			t1->components.type.kind.arraytype.basetype,
			t2->components.type.kind.arraytype.basetype);
		}
		else {
		    return false;
		}

	    case YREF:
		if (t2->header.name == YREF) {
		    return compat(
			t1->components.type.kind.ref.basetype,
			t2->components.type.kind.ref.basetype);
		}
		else {
		    return false;
		}

	    case '\'':
		/*
		 * If t1 and t2 are both lit types, then their base types need
		 * to be compat and their values need to be equal.
		 */
		if (t2->header.name == '\'') {
		    if (compat(
			    t1->components.type.kind.lit.type,
			    t2->components.type.kind.lit.type)) {
			return chkEqLitValues(t1, t2);
		    }
		}
		/*
		 * If t1 is a lit type, and t2 is anything else, then they
		 * cannot be compatible.
		 */
		else {
		    return false;
		}
	}

	/*
	 * Check or compat.  At present it's two-way, but most likely needs to
         * be changed to one-way.
	 */
	if (t1->header.name == YOR) {
	  return orCompat(t1, t2);
	}

	/*
	 * If t2 is a lit type, then only its base type need be compat with t1.
	 */
	if (isLiteralType(t2)) {
	    return compat(t1, t2->components.type.kind.lit.type);
	}

    }

    return false;	/* Who know's what this might mean? */
}

/*

 * Check that the values of two lit types are equal.  At entry, both type
 * structs have been determined to be lit types, i.e., name = '\''.  What
 * remains to be determined here is whether they have the same base type and
 * value.
 *
 * There are five possibilities for components.type.kind.lit.type: StringType,
 * IntType, RealType, Niltype, or an ident type.  The logic builds the
 * appropritely tagged Value based on what type of literal we have.
 *
 * An important piece of info here is that the base type of an ident lit type
 * must be a type desig.  I.e., for any literal type "the T V", T must be a
 * type desig, which is a plain ident, a starred ident, or a paremeterized
 * ident.
 *
 * Performing this check requires possible incremental forward type checking
 * and value computation for a declared value.  Cf. what goes on in chkIdent,
 * with the forward call to chkValExprDecl.
 */
bool chkEqLitValues(TypeStruct t1, TypeStruct t2) {
    TypeStruct t;
    ValueStruct v1, v2, rtn;


    if (not compat(t = t1->components.type.kind.lit.type,
	    t2->components.type.kind.lit.type)) {
	return false;
    }

    v1 = interpExpr(t1->components.type.kind.lit.value);
    v2 = interpExpr(t2->components.type.kind.lit.value);

    rtn = doEq(v1, v2);

    if (isNilValue(rtn))
	return false;

    return rtn->val.BoolVal;

}

/*
 * This is where we sort out all the possibilities for nice or compatibility.
 * Here're the rules:
 *
 *   (a) Before we ever get here, we've checked for the same two ident types.
 *   (b) If both sides are non-ident-compat or's, then we just run through the
 *       types of each and check that each is struct compat.
 *   (c) Next we check if either side is an or and the other one of the
 *       types that's in the or.
 *   (d) Well, maybe the "all the possibilities" in the introductory comment
 *       was too pessimistic.  I.e., all we need to do is check for each elem
 *       of the or if it's compat with the singleton type of the other.  Hmm.,
 *       can it really be this simple?  Hope so.
 */

bool orCompat(
    TypeStruct t1, TypeStruct t2)	/* Type structs to compare */
{
    nodep f1, f2;
    bool proceed;

    if ((t1->header.name == YOR) and (t2->header.name == YOR)) {
	/*
	 * Cruise the fields and call compat on each pair.  As with any form of
	 * list comp such as this, fail if either list is shorter than the
	 * other.  IMPORTANT: field lists can be in different orders!  This
	 * means that we must do things a bit more complicatedly. 
	 */
	if (t1->components.type.kind.record.numfields !=
		t2->components.type.kind.record.numfields) {
	    return false;
	}
	for (f1 = t1->components.type.kind.record.fields; f1;
		f1 = f1->components.decl.next) {
	    proceed = false;
	    for (f2 = t2->components.type.kind.record.fields; f2;
		    f2 = f2->components.decl.next) {
		if (compat(f1->components.decl.kind.field.type,
			f2->components.decl.kind.field.type)) {
		    proceed = true;
		    break;
		}
		else {
		    continue;
		}
	    }
	    if (not proceed) {
		return false;
	    }
	}
	return true;
    }

    if (t1->header.name == YOR) {
	return orCompat1(t1, t2);
    }
    else {
	return orCompat1(t2, t1);
    }
}


/*
 * Work doer when one type is an or and the other a non-or.  Which is which has
 * been sorted out by the caller, so t1 is the or type here.
 *
 * What we're dealing with here is the case of auto-injection.  The
 * compatibility rule in this case is that t2 is compat with exactly one of the
 * union elements.
 */
bool orCompat1(
    TypeStruct t1, TypeStruct t2)	/* Type structs to compare */
{
    TypeStruct t;

    /*
     * Cruise the fields of t1, succeeding if one is compat with t2, failing if
     * none is.
     */
    for (t=t1->components.type.kind.record.fields;
	    t; t=t->components.decl.next) {
	if (compat(t->components.decl.kind.field.type, t2)) {
	    return true;
	}
    }

    return false;
}

/*
 * This is the bitchin new rule that allows T = {T}, for any type T.  See
 * various discussions and examples bestolling the virtue of this rule.
 */
bool onetupleCompat(
    TypeStruct t1, TypeStruct t2)	/* Type structs to compare */
{
    t1 = ResolveIdentType(t1, null, false);
    t2 = ResolveIdentType(t2, null, false);

    if
	(isRecord(t1) and isRecord(t2) and
	    (t1->components.type.kind.record.numfields == 1) and
	    (t2->components.type.kind.record.numfields == 1) and
	    compat(
		ResolveIdentType(
		    t1->components.type.kind.record.fields->
			components.decl.kind.field.type, null, false),
		ResolveIdentType(
		    t2->components.type.kind.record.fields->
			components.decl.kind.field.type, null, false)))
	return true;

    else if
	(isRecord(t1) and 
	    (t1->components.type.kind.record.numfields == 1) and
	    compat(
		ResolveIdentType(
		    t1->components.type.kind.record.fields->
			components.decl.kind.field.type, null, false),
		t2))
	return true;

    else if
	(isRecord(t2) and 
	    (t2->components.type.kind.record.numfields == 1) and
	    compat(
		ResolveIdentType(
		    t2->components.type.kind.record.fields->
			components.decl.kind.field.type, null, false),
		t1))
	return true;

    else
	return false;

/* Efficient way after debugging:
    return
	(isRecord(t1) and isRecord(t2) and
	    (t1->components.type.kind.record.numfields == 1) and
	    (t2->components.type.kind.record.numfields == 1) and
	    compat(
		t1->components.type.kind.record.fields->
		    components.decl.kind.field.type,
		t2->components.type.kind.record.fields->
		    components.decl.kind.field.type))  or

	(isRecord(t1) and 
	    (t1->components.type.kind.record.numfields == 1) and
	    compat(
		t1->components.type.kind.record.fields->
		    components.decl.kind.field.type,
		t2))  or

	(isRecord(t2) and 
	    (t2->components.type.kind.record.numfields == 1) and
	    compat(
		t2->components.type.kind.record.fields->
		    components.decl.kind.field.type,
		t1));
 */
}


/*
 * RSL equivalence predicate.  As noted above, we must chase pointers through
 * chains of name-equivalent ident types.
 */
bool equiv(
    TypeStruct t1, TypeStruct t2)	/* Type structs to equivalence */
{
    TypeStruct eq1, eq2;

    for (eq1 = t1; eq1; eq1 = GetNextEquivIdentType(eq1)) {
	for (eq2 = t2; eq2; eq2 = GetNextEquivIdentType(eq2)) {
	    if (SameIdentType(eq1, eq2))
		return true;
	}
    }
}

/*
 * Assuming an ident type coming in, follow a pointer to an equivalent ident
 * type, if there is one.  Note that we don't report any undef'd type lookups
 * here, since we're just doing equivalencing.  Such reporting is presumably
 * done elsewhere.
 */
TypeStruct GetNextEquivIdentType(
    TypeStruct it)	/* An ident type struct */
{
    SymtabEntry* sym;

    sym = Lookup(it->components.type.kind.ident.type->
	components.atom.val.text);
    if (sym and isIdentType(sym->Type))
	return sym->Type;
    else
	return null;
}

/*
 * Do the low-level pointer grubbing for the equivalence of two ident types.
 */
bool SameIdentType(
    TypeStruct t1, TypeStruct t2)	/* Two ident types */
{
    return t1->components.type.kind.ident.type->components.atom.val.text ==
	t2->components.type.kind.ident.type->components.atom.val.text;
}


/*
 * Assigment compatibility predicate.  Two types are assignment compatible if:
 *   (1) they are compatible, EXCEPT LHS cannot be a literal restriction of RHS
 *   (2) RHS is a subtype (aka subclass) of LHS, or
 *   (3) RHS is a multi-valued function and LHS is a structurally equiv tuple.
 */
bool assmntCompat(
    TypeStruct lt,
    TypeStruct rt)
{
    bool compat_result;

    /*
     * First check if either type is null, which means a type checking error
     * has occurred, and we just propagate it.
     */
    if ((lt == null) or (rt == null))
	return null;

    /*
     * Next check if lt and rt are compat.
     */
    if (compat(lt, rt)) {
	compat_result = true;

	/*
	 * Since compat allows two-way literal compat, we need to retract that
	 * here, if necessary.  Specifically, if LHS is a literal type, and RHS
	 * is its base type, then compat says they're OK, but here in assmnt
	 * compat we have to say they're NOT OK.  Implementing this as a
	 * "retraction" is a bit hokey, but it's seen at this point as the
	 * easiest way to go, given how many other places compat is called.
	 */
	if (isLiteralType(lt) and (not isLiteralType(rt))) {
	    compat_result = false;
	}
	return compat_result;
    }

    /*
     * Next check if subtype compat, i.e., rt < lt.
     */
    if (subtypeCompat(lt, rt)) {
	return true;
    }

    /*
     * Deprecated, and scheduled for removal.  Literal compatibility is handled
     * in the "retract" above.
     *
     * Check if literal compat, i.e., rt one of the values that define lt's
     * value set.  This could be done in union compat, but for now it's done
     * explicitly here.
     * 
     *
    if (litCompat(lt, rt)) {
	return true;
    }
     */

    /*
     * If lt and rt are not compat, then check if otherwise assmnt compat.
     */
    return
	((isIntOrCardOrSubrangeOfEither(lt) and
	     isIntOrCardOrSubrangeOfEither(rt)) or
	 (isString(rt) and isStringArray(lt) and 
	     stringCompat(lt, rt)) or
	 (isMultValFcnType(rt) and
	     oneLevelStructRecEquiv(lt, rt))
	);
}


/*
 * Check that a literal string is compatible with an array of char.  Since we
 * know the bounds of the array and size of the literal, we can make sure that
 * there's enough room in the array to hold all of the literal chars.
 */
bool stringCompat(
    TypeStruct at,
    TypeStruct st)
{
    int size;

    return true;

   /* LATER
    size = interpExpr(at->components.type.kind.arraytype.bounds->
		    components.decl.type.type->
			components.type.kind.subrange.upper);
    if (size > strlen(st->components.atom.val.string))
	return true;
    else {
	lerror(st, "Size of string literal too large for destination.\n");
	return null;
    }
    */
}


/*
 * Perform the structural equivalence required between an lvalue of a proc type
 * and a "dproc" type derived from a declared procedure name.
 */
bool procCompat(
    TypeStruct pt,	/* Proc type as defined in a proc type decl. */
    TypeStruct dpt)	/* Derived proc type, built at the end of chkIdent. */
{
    SymtabEntry *e1, *e2;
    TypeStruct ptt, dptt;

    /*
     * Check that the arities agree in type and number.
     */
    for (e1 = pt->components.type.kind.proc.formalchain,
	 e2 = dpt->components.type.kind.dproc.formalchain;
	    e1 and e2;
		e1 = e1->Info.Parm.Link, e2 = e2->Info.Parm.Link) {
	if (not compat(e1->Type, e2->Type))
	    return false;
    }
    if (e1 or e2) return false;

    /*
     * Check that the coarities agree, if they exist.
     */
    ptt = pt->components.type.kind.proc.type;
    dptt = dpt->components.type.kind.dproc.type;
    if (((not ptt) and dptt) or (ptt and (not dptt))) {
	return false;
    }
    else {
	if ((not ptt) and (not dptt))
	    return true;
	else
	    return compat(ptt, dptt);
    }
}


/*
 * Perform the structural equivalence required between an array index expr and
 * the corresponding index decl.  What's structural about it is that the index
 * decls do not have to be named types, but rather can be any simple type decl.
 */
bool arrayCompat(
    TypeStruct it,	/* The index expr type. */
    TypeStruct dt)	/* The declared index type. This is assumed to be a
			 * pointer to a simple-type type struct. */
{
    /*
     * Switch on the allowable types of array index:
     *     char, boolean, enum, or subrange
     */

    switch (dt->header.name) {
	case Yident:
	    return assmntCompat(it, dt);
	case '(':
	    return assmntCompat(it, dt);
	case '[':
	    return assmntCompat(it, dt->components.type.kind.subrange.basetype);
    }
}

/*
 * Perform the structural equivalence required between an lvalue of record type
 * and the return type of a multi-valued function.
 */
bool oneLevelStructRecEquiv()
{
    /* TODO */
    return false;
}

/*
 * Perform formal/actual parm type checking.  The diffs between this and
 * assmntCompat is that here we must check for formal var parms and open array
 * parms.  For var parms, we require strict equivalence.  For open array parms,
 * we do a bit of structural equivalence.  Otherwise, for val parms we just use
 * assmntCompat.
 */
bool parmCompat(
    SymtabEntry *fp,
    TypeStruct ap)
{
    TypeStruct fpt = fp->Type;

    /*
     * Check if formal is an open array, and if so let it be assmnt compat with
     * any 1-d array of the same base type.
     */
    if (ChkSymFlag(fp, arrayParm)) {
	return ((isArray(ap) or isString(ap)) and
	    assmntCompat(fpt->components.type.kind.arraytype.basetype,
		isString(ap) ? CharType :
		    ap->components.type.kind.arraytype.basetype));
    }

    /*
     * Check if formal is a var parm (but not open array), and if so require
     * strict equiv.  Note that we already checked that the var parm is an
     * l-value, so that chk is not done here.  We did the l-val check earlier
     * to avoid multiple error messages.
     */
    if (ChkSymFlag(fp, varParm))
	return (ap == fpt);
    else {
	return assmntCompat(fpt, ap);
		/* NOTE: order of parms to assmntCompat IS significant. */
    }
}


/*
 * Uniformly return the typesize of ANY type as 1, representing the increment
 * to be used when indexing into a memory segment declared as an array of
 * Value*.
 *
 * This computation of TypeSize is different than in the past, and could
 * possibly be amended in the future.  However at present, this computation
 * reflects a fully uniform memory model, wherein the type size of any bound
 * value is the size of a single Value pointer.
 */
int TypeSize(
    TypeStruct t)
{
    return 1;
}


/*
 * Return the computed typesize for the browser.  See the 6jan01 LOG entry for
 * a comment about unifying this with the above TypeSize.
 */
int BrowserTypeSize(
    TypeStruct t)
{
    TypeStruct t1;

    if (not t)
	return 0;

    t1 = ResolveIdentType(t, null, false);

    if (not t1) {
	if isIdentType(t)
	    return 1;
    }

    if (isOpaqueType(t1))
	return 0;

    if (t1->components.type.size == 0)
	return 1;

    return t1->components.type.size;
}


/*
 * Perform one-time-only type checker init.
 */
void InitTypechk()
{
    ARecordEntry = HashAllocSymtabEntry("A Record", null, null, null);
    SetErrorCounter(&(CurSymtab->Errors));
    CurStaticOffset = 0;
    ValidationTupleType = BuildValidationTupleType();
    treetos = TreeStack;
    TreeStackSize = STACKSIZE;
}


/*
 * Please tell me you're kidding, Klaus.
 */
bool isNegInt(
    nodep t)
{
    ValueStruct v;

    v = interpExpr(t);
    return (isInt(v->type) and (v->val.IntVal < 0));
}



/****
 * Begin spec-language-specfic type checking.
 */


/*
 * Build the type struct for a component composition expr.  In particular, the
 * following mapping is made between RSL types and Mod-2 types:
 *
 *	RSL Type		Mod-2 Type
 *	  and			  record
 *	  or			  union (clone of record; see BuildOr below)
 *	  list			  List
 *	  recursive		  ref to ident type
 *	  name:value pair	  ident type (see BuildNameTypePairType)
 *	  single name		  ident type
 *
 * To facilitate subsequent checking and exeuction, a symtab is built for 'and'
 * and 'or' comp exprs a la Mod-2's chkRecordType above.
 *
 * Note that this function is called at pass 1.5, after the tree is built but
 * before type checking commences.  It must be done this way, since RSL does
 * not have a declare-before-use policy, as in Mod-2.  In Mod-2, all the type
 * decls must appear before their use, so the record symtab construction and
 * array type handling can happen in the same pass as the type checking.  Here
 * in RSL, we must build record symtabs first, since during type checking, we
 * may refer to a type (i.e., object) before its def is lexically encountered.
 *
 * OLD and WRONG:
 * Except for top-level lists, all RSL comp exprs are represented with a
 * RECORD_TYPE as the top-most node, the components.type.kind.record.fields
 * field of which points to the components expression tree.  If there's only
 * one list field in the record, then the record type is stripped off, so that
 * the components can be ref'd directly with bracket notation.  E.g., this is
 * the way we want to be able to ref list-composed objects:
 *
 *	obj O is
 *	    components: O1*;
 *
 *	op Op is
 *	    inputs: In1: O;
 *	    pre: forall (n: integer) (In1[n] > = 0);
 *
 */
TypeStruct BuildCompType(
    nodep t)			/* Ptr to complete obj def */
{
    nodep p, rtn;

    /*
     * Some folks like to call us with a null, so we're accomdating.
     */
    if (not t)
	return null;

    /*
     * Check if it's list from a var decl, which, alas, we handle as a special
     * case, which we'll just forward on to BuildCompType1.
     */
    if (isList(t)) {
	return BuildCompType1(t);
    }

    /*
     * Check next for zero components, in which case we have an opaque type.
     */
    if (not (p = t->components.decl.kind.obj.parts))
	return BuildOpaqueType(t);

    /*
     * If there's at least something at the top-level, let the recursive buddy
     * handle it.
     */
    rtn = BuildCompType1(t->components.decl.kind.obj.parts);

    /*
     * Outta here.
     */
    return rtn;
}

TypeStruct BuildCompType1(
    nodep p)			/* Ptr to complete parts expr */
{
    int AutoNameIndex = 1, n;
    TypeStruct s;

    /*
     * Evidently we can get here with a null, so protect, protect!
     */
    if (not p)
	return null;

    /*
     * Build the appropriate type for a literal constant.
     */
    if (isConstAtom(p)) {
	return BuildLiteralType(p);
    }

    /*
     * Check for ident atom, which comes from a recursive call in building a
     * tuple field.
     */
    if (isIdentAtomNode(p)) {
	return BuildAtomType(p);
    }

    /*
     * Check for a sym lit, in which case we have to build the opaque type if
     * it's not already, and return it.
     *
     * 8may09: Deprecated in specl.
     *
    if (isSymLit(p)) {
	return BuildOrFetchSymLitType(p);
    }
     *
     */

    /*
     * Check for a single name/type pair, in which case we have an ident type,
     * a literal-value type, or a named parenthesized type.
     */
    if (isNameTypePair(p)) {
	return BuildNameTypePairType(p);
    }

    /*
     * Handle an init name/type pair the same as a plain name/type pair, just
     * skipping the init part.  We come across init name/type pairs here when
     * we're building the coarity type for an op, having been called from
     * sym-aux.c:EnterOperation, q.v.
     */
    if (isInitNameTypePair(p))
	return BuildNameTypePairType(p->components.decl.kind.initdecl.decl);

    /*
     * Next check for a list.
     */
    if (isList(p))
	return BuildList(p);

    /*
     * And then for a ref.
     */
    if (isRef(p))
	return BuildRef(p);

    /*
     * With an and or or, recurse on the composition operator.  Note
     * that we pass in a 0 to each of the recursive builders to start the
     * component counting.  The idea is that we want to count the number of
     * subcomponents of each and'd and or'd subexpr so that we can alloc the
     * right size symtab down at the bottom of the traverse.
     */
    switch (p->header.name) {
	case YAND:	/* And composition */
	    return BuildAnd(p);
	    return s;
	case YOR:	/* Or composition */
	    return BuildOr(p);
	case YRTARROW:
	    return BuildOp(p);
    }
}

TypeStruct BuildOpaqueType(nodep t) {
    return NewNode(TYPE_NODE, ';', t->header.loc);
}

/*
 * Build an ident type for an atom node.  This will only happen when we've
 * recursed into the fields of a tuple, i.e., via BuildAnd.
 */
TypeStruct BuildAtomType(nodep t) {
    TypeStruct type;

    if (t) {
	type = NewNode(TYPE_NODE, Yident, t->header.loc);
	type->components.type.kind.ident.type = t;
	type->components.type.origname = t;
	return type;
    }
    return null;
}

/*
 * Build the type appropriate for a literal constant atom.  This comes from a
 * literal-valued object component.  Note that we're protected here, because
 * the caller checks isConstAtom before calling.
 */
TypeStruct BuildLiteralType(nodep t) {
    TypeStruct type = NewNode(TYPE_NODE, '\'', t->header.loc);
    type->components.type.kind.lit.value = t;

    switch (t->header.name) {
	case Ystring:
	    type->components.type.kind.lit.type = StringType;
	    return type;
//	    return StringType;
	case Yinteger:
	    type->components.type.kind.lit.type = IntType;
	    return type;
//	    return IntType;
	case Yreal:
	    type->components.type.kind.lit.type = RealType;
//	    return type;
	    return RealType;
	case Ynil:
	    return NilType;
    }
}

TypeStruct BuildOrFetchSymLitType(nodep t) {
    /*
     * What needs to be done here is to lookup to see if the symlit string is
     * already defined as a type, and deal with it accrodingly.  I think
     * there's can of worms here, since we have to deal with the case that a
     * symlit is already defined as some other non-opaque type.  Whatever,
     * we'll deal with it as we must.  In the meantime, things at least wont
     * seg fault on the HPs (see LOG entry of 29oc98).
     */

    return BuildOpaqueType(t);
}

/*
 *
 * Any of the following discussion that says we cant have one tuples is WRONG.
 * The current implementation does in fact support one tuples.  See elsewhere
 * in the type checker to see where this happens, e.g., isOneTupleComapt.
 *
 * For any name/type pair, build an ident type, the type field of which points
 * to a type struct for the type part, even if a name is present.  This means
 * that we cannot build a one-element tuple, even with explicit parens.  This
 * is reasonably consistent with a formal def of tuple, but not so much with a
 * PL-style record.  We'll live with the current scheme for now, and see how
 * things go.
 *
 * An alternative would be to build a type struct for a comp expr consisting of
 * a single name/type pair as follows:
 *
 *    1. If it's a single value, with no name, then we build just an ident
 *       type.  E.g., we have a comp expr of the form
 *		obj x is y;
 *    2. If there is a name, then we build a one-element tuple (i.e., record)
 *       type struct.  E.g., we have a comp expr of the form
 *		obj x is n:y;
 *
 * The point here is that if the specifier takes the trouble to add a name,
 * then she has in mind accessing the field via that name.  The problem with
 * this is that we get two different types, even with the same type name, which
 * I don't much care for.  Hence, as noted above, we'll live with the current
 * scheme and see how things go.
 *
 * Note, after all of this, that we do in fact squirrel away the name, so that
 * it can be used to resolve inheritance.  The deal is that if a name/type pair
 * type has a name, then that name should be used as a field name in
 * subclasses.
 */
TypeStruct BuildNameTypePairType(nodep t) {
    TypeStruct type;
    nodep v;

    if (v = t->components.decl.kind.attr.value) {
	type = BuildCompType1(t->components.decl.kind.attr.value);
	type->components.type.name = t->components.decl.kind.attr.name;
	/*
	 * Next line doesnt work as hoped for -- maybe sometime later.
	type->components.type.isTopLevelNameTypePair = true;
	 *
	 */

	/*
	 * Since preceding line didnt work to help with id'ing top-level
	 * name/type pair types, we'll just byte the bullet and make such types
	 * 1-tuples.  This will allow them to be ref'd via name, a long-time
	 * thorn in the side.
	 */
	type = BuildNewTupleTypeSized(type, 5, false);
    }
    else {
	type = BuildCompType1(t->components.decl.kind.attr.name);
    }
    return type;
}

/*

 * Build the the type struct, including the record symtab, for an AND
 * composition op.  Here's the strategy: We recursively traverse through the
 * comp expr tree at one level of AND'ing until we're done.  As we do so, we
 * build up a linked list of record parse tree nodes as well as the count of
 * the nodes at this level.  The nodes are chained by the standard decl next
 * field.
 *
 * Due to the left associativity of AND defined in Yacc, the right operand of
 * an AND is always just built recursively and stuck as the type of the field.

 */
TypeStruct BuildAnd(
    nodep t)		/* Ptr to AND subtree */
{
    Symtab* st = null;	/* Upcoming symtab */
    int i = 0;		/* Down-going cout of and'd components */
    int n = 0;		/* Upcoming count of and'd components */
    TypeStruct rtn;

    rtn = NewNode(TYPE_NODE, YRECORD, t->header.loc);
    rtn->components.type.kind.record.fields =
	FixDeclList(BuildAndOrFields(t, i, &n, &st, YAND));
    rtn->components.type.kind.record.numfields = n;
    rtn->components.type.kind.record.fieldstab = st;
    PopSymtab();

    return rtn;
}

/*
 * Build the fields of the record or union type struct for an and.  Do so by
 * recursing on the left operand, and building the right.  On the way back out,
 * splice the right-operand field onto the end of the left-operatnd field list
 * and enter the right-operand field into the upcoming symtab.
 *
 * On the way down, we count fields.  At the bottom (left), we alloc the
 * symtab, based on the count coming down.  At each level, we alloc field
 * nodes.  */
TypeStruct BuildAndOrFields(
    nodep t,		/* Ptr to AND of OR subtree */
    int i,		/* Down-going count of and'd components */
    int *n,		/* Up-going count of and'd components */
    Symtab **st,	/* Up-going symtab */
    TokenType compop)	/* YAND or YOR */
{
    TypeStruct t1,t2;
    nodep f, r;

    /* 
     * Check for null left operand, which is syntactically allowed, and can
     * happen in a def such as
     *
     *     obj X is (* later *) and Y and Z;
     */
    if (not t->components.binop.left_operand) {
	/*
	 * Bump the field counters.  NOTE: Should we do this here?
	 */
	i++;
	(*n)++;

	/*
	 * Splice an empty upcoming left-recursive field list with the single
	 * right field.  We need to go into BuildEmptyLeftField, instead of
	 * just going right only, since we've not yet alloc'd a symtab.  This
	 * happens at the far left of the traversal, so we must do it even if
	 * the far left operand is null.
         */
	t1 = BuildEmptyLeftField(t->components.binop.left_operand, n, st);
	t2 = BuildRightField(t->components.binop.right_operand, st, i);
	return AddToDeclList(t1, t2);
    }

    /*
     * Check if left operand is another and.  If so, recurse on it, and splice
     * on the field for the right operand on the way back up.
     */
    if ((t->components.binop.left_operand->header.kind == BINOP_NODE) and
	    (t->components.binop.left_operand->header.name == compop)) {

	/*
	 * Bump the field counters.
	 */
	i++;
	(*n)++;

	/*
	 * Splice the upcoming left-recursive field list with the single right
	 * field.
         */
	t1 = BuildAndOrFields(
	    t->components.binop.left_operand, i, n, st, compop);
	t2 = BuildRightField(t->components.binop.right_operand, st, i);
	return AddToDeclList(t1, t2);
    }
    else {
	/*
	 * We've left-bottomed out on this level of AND or OR.  Recursively
	 * build the field type struct for the left operand, including alloc of
	 * the fields tab.  Do the same for the right operand and then start
	 * unwiding.
	 */
	*n = *n + 2;
	i++;

	/*
 	 * Note that either or both args to AddToDeclList could be null (rare,
         * but possible).  Fortunately, AddToDeclList does the right thing with
         * null args.  Thank you.
	 */
	t1 = BuildLeftField(t->components.binop.left_operand, n, st); 
	t2 = BuildRightField(t->components.binop.right_operand, st, i);
	return AddToDeclList(t1, t2);
    }
}

/*
 * Build a field out of an AND or OR right operand and enter it in the incoming
 * symtab.  Return the built field.
 */
nodep BuildRightField(
    nodep t,		/* Pointer to right operand of AND tree */
    Symtab** st,	/* Symtab to enter in */
    int i)		/* Ordinal position of this field. */
{
    nodep f;		/* New field node for right operand */

    /*
     * Need to check for null t.  This can happen with a null component, a
     * typical example of which is
     *
     *     obj O id A and B and (*...*) ;
     */
    if (not t)
	return null;

    /*
     * Alloc a new field node.
     */
    f = AllocFieldNode(t);

    /*
     * Enter the field into the fields symtab.
     */
    EnterAndField(f->components.decl.kind.field.vars,
	f->components.decl.kind.field.type, st, i);

    return f;
}

void EnterAndField(nodep var, TypeStruct type, Symtab** st, int i) {
    char *name;
    char defaultname[20];
    SymtabEntry* sym;

    /*
     * Complain if field of given name already declared.
     */
    name = var ? var->components.atom.val.text : null;
    if (name and LookupInThisScope(name, *st)) {
	lerror(var, "Redeclaration of tuple name %s\n", name);
	return;
   }

    /*
     * Compute the "[i]" default name for the field.
     */
    sprintf(defaultname, "[%d]\0", i);

    /*
     * Do the entering, both of given name, if non-null, and default name.
     */
    if (name) {
	Enter(sym = HashAllocSymtabEntry(name, C_Var, type, (*st)->Level));
	sym->Info.Var.Offset = CurSymtab->Offset;
    }
    Enter(sym = HashAllocSymtabEntry(defaultname, C_Var, type, (*st)->Level));
    if (name) {
	SetSymFlag(sym, hasName);
    }
    sym->Info.Var.Offset = CurSymtab->Offset;
    CurSymtab->Offset += TypeSize(type);
}


/*
 * Alloc a new field node.  If we have a full name/type pair, use the name as
 * the field name and the recursive build of the type as the field type.
 * Otherwise, make the field name null, and use the recursive build of the the
 * type as the field type.
 */
nodep AllocFieldNode(nodep t) {
    nodep f;

    f = NewNode(DECL_NODE, 'f', EmptyLoc);

    if (not t)
	return f;

    if (isInitNameTypePair(t))
	t = t->components.decl.kind.initdecl.decl;

    if (! isNameTypePair(t)) {
	f->components.decl.kind.field.type = BuildCompType1(t);
	return f;
    }

    if (isFullNameTypePair(t)) {
	f->components.decl.kind.field.vars = t->components.decl.kind.attr.name;
	f->components.decl.kind.field.type =
	    BuildCompType1(t->components.decl.kind.attr.value);
    }
    else {
	f->components.decl.kind.field.type = BuildCompType1(
	    t->components.decl.kind.attr.name);
    }

    return f;
}


/*
 * A la AllocFieldNode, but takes unbundled name and type values.  This is
 * because we're calling from a context like inheritance resolution, where we
 * don't have an intact field tree node anymore.
 */
nodep AllocFieldNodeFromType(char* fname, TypeStruct type) {
    nodep f,n;

    f = NewNode(DECL_NODE, 'f', EmptyLoc);
    n = f->components.decl.kind.field.vars = 
	NewNode(ATOM_NODE, Yident, EmptyLoc);
    n->components.atom.val.text = fname;
    f->components.decl.kind.field.type = type;

    return f;
}


/*
 * Build a field out of an AND or OR left operand.  The situation at this point
 * is that we've bottomed out on the left-heavy AND or OR tree, and we're ready
 * to alloc the first field, as well as the symtab that we'll send back up.
 */
TypeStruct BuildLeftField(
    nodep t,		/* Pointer to left operand of AND tree */
    int *n,		/* Incoming field count */
    Symtab** st)	/* Symtab to build and pass back up */
{
    nodep f;

    /*
     * Need to check for null t.  This is rare, but evidently possible given
     * the null alternative for parts_spec in parser.y, q.v.
     *
     * NOTE: Dont think this is needed anymore, given check above for empty
     * left operand, and new BuildEmptyLeftField call.  THINK ABOUT IT.
     */
    if (not t)
	return null;

    /*
     * Alloc a new field node, including init of the field list so
     * AddToDeclList can be used during the unwinding.
     */
    f = InitDeclList(AllocFieldNode(t));

    /*
     * Alloc record symtab.
     */
    PushSymtab();
    /* NOTE: Not clear why t->...fieldstab was ever being set here */
    /* t->components.type.kind.record.fieldstab = */ (*st =
	AllocSymtab((int)(1.2 * *n + 3)));
    (*st)->ParentTab = CurSymtab;
    (*st)->ParentEntry = ARecordEntry;
    (*st)->Level = CurSymtab == (Symtab *)0 ? 0 : CurSymtab->Level + 1;
    (*st)->Offset = 0;
    MoveToSymtab(*st);

    /*
     * Apparently, some mean little syntax error can give us a null f here, so
     * we muse exit gracefully if so.
     */
    if (not f)
	return null;

    /*
     * Enter the field into the fields symtab.
     */
    EnterAndField(f->components.decl.kind.field.vars,
	f->components.decl.kind.field.type, st, *n);

    return f;
}


/*
 * A la BuildLeftField, but here for an empty operand.  Hence, we build a
 * symtab (for sending up to others), but don't make any entry in it.
 */
TypeStruct BuildEmptyLeftField(
    nodep t,		/* Pointer to left operand of AND tree */
    int *n,		/* Incoming field count */
    Symtab** st)	/* Symtab to build and pass back up */
{
    nodep f;

    /*
     * Alloc a new field node, including init of the field list so
     * AddToDeclList can be used during the unwinding.
     */
    f = InitDeclList(AllocFieldNode(t));
    /*
     * Alloc record symtab.
     */
    PushSymtab();
    /* NOTE: Not clear why t->...fieldstab was ever being set here */
    /* t->components.type.kind.record.fieldstab = */ (*st =
	AllocSymtab((int)(1.2 * *n + 3)));
    (*st)->ParentTab = CurSymtab;
    (*st)->ParentEntry = ARecordEntry;
    (*st)->Level = CurSymtab == (Symtab *)0 ? 0 : CurSymtab->Level + 1;
    (*st)->Offset = 0;
    MoveToSymtab(*st);

    /*
     * Apparently, some mean little syntax error can give us a null f here, so
     * we muse exit gracefully if so.
     */
    if (not f)
	return null;

    /*
     * DONT enter the field into the fields symtab.
     */

    return f;
}


/*
 * Build a union type as a virtual clone of a tuple.  Maybe we'll go for
 * efficiency later, maybe not.  As of now, the *only* diff between a record
 * type vs union is the name field -- YRECORD vs YOR.
 */
TypeStruct BuildOr(
    nodep t)
{
    Symtab* st = null;	/* Upcoming symtab */
    int i = 0;		/* Down-going cout of and'd components */
    int n = 0;		/* Upcoming count of and'd components */
    TypeStruct rtn;

    rtn = NewNode(TYPE_NODE, YOR, t->header.loc);
    rtn->components.type.kind.record.fields =
	FixDeclList(BuildAndOrFields(t, i, &n, &st, YOR));
    rtn->components.type.kind.record.numfields = n;
    rtn->components.type.kind.record.fieldstab = st;
    PopSymtab();

    return rtn;
}


/*
 * Build an op type.
 */
TypeStruct BuildOp(nodep p) {
    nodep n;
    n = NewNode(TYPE_NODE, YOP, EmptyLoc);
    n->components.type.kind.op.entry =
	(SymtabEntry*) p->components.trinop.right_operand;
    n->components.type.kind.op.ins = p->components.trinop.left_operand;
    n->components.type.kind.op.outs = p->components.trinop.middle_operand;
    return n;
}


/*
 * Build a list directly as an open array.
 */
TypeStruct BuildList(
    nodep t)
{
    if (t->header.kind  == BINOP_NODE)
	return BuildOpenArrayType(BuildCompType1(
	    t->components.binop.left_operand), null);
    else
	return BuildOpenArrayType(BuildCompType1(
	    t->components.unop.operand), null);
}

/*
 * Ditto, but from basetype instead of array type.
 */
TypeStruct BuildListFromBasetype(
    nodep t)
{
    return BuildOpenArrayType(t, null);
}

/*
 * Build a ref as a simple little trincket, that's just got its base type.
 */
TypeStruct BuildRef(
    nodep t)
{
    TypeStruct t1;

    t1 = NewNode(TYPE_NODE, YREF, t->header.loc);
    t1->components.type.kind.ref.basetype = BuildCompType1(
	t->components.unop.operand);
}


/*
 * Build a type struct for a parenthesized component.  If what's inside isn't
 * already a record, then make it one, and ... .
 *
 *    obj o is parts: x:(a and b and c) or y:(d or e);
 *
 * Here, both parenthsized exprs are records already, so 
 *   FIX -- comment dropped off here.
 *
 */
TypeStruct BuildSubPart(
    nodep t,
    int *n)
{
    

}

bool isIdentAtomNode(nodep t) {
    return (t and (t->header.kind == ATOM_NODE) and
	(t->header.name == Yident));
}

bool isNameTypePair(nodep t) {
    if (t) {		/* Protection just in case */
	return (t->header.kind == DECL_NODE) and
	    ((t->header.name == ':') or (t->header.name == 'f'));
    }
    else
	return false;
}

/*
 * NOTE: The following two functions are not currently used, but may be at some
 * point.
 */
bool isConstNameTypePair(nodep t) {
    if (isNameTypePair(t)) {
        if (not t->components.decl.kind.attr.value) {
	    return isConstAtom(t->components.decl.kind.attr.name);
	}
	else {
	    return isConstAtom(t->components.decl.kind.attr.value);
	}
    }
    return false;
}

bool isConstInitNameTypePair(nodep t) {
    return isInitNameTypePair(t) and
	isConstNameTypePair(t->components.decl.kind.initdecl.decl);
}

bool isOpaqueType(TypeStruct t) {
    return (t and (t->header.kind == TYPE_NODE) and (t->header.name == ';'));
}

bool isFullNameTypePair(nodep t) {
    if (t) {		/* Protection just in case */
	return (t->header.kind == DECL_NODE) and
	  ((t->header.name == ':') or (t->header.name == 'f')) and
	    (t->components.decl.kind.attr.name) and
		(t->components.decl.kind.attr.value);
    }
    else
	return false;
}


bool isList(nodep t) {
    if (t) {
	return ((t->header.kind == UNOP_NODE) or
		    (t->header.kind == BINOP_NODE)) and
			(t->header.name == YLIST);
    }
    else {
	return false;
    }
}

bool isRef(nodep t) {
    if (t) {
	return ((t->header.kind == UNOP_NODE) or
		    (t->header.kind == BINOP_NODE)) and
			(t->header.name == YREF);
    }
    else {
	return false;
    }
}

bool isCoarityList(nodep t) {
    return (isInitNameTypePair(t) and
	t->components.decl.kind.initdecl.islist and
	t->components.decl.kind.initdecl.iscoarity);
}


/*
 * Check an object decl of the form:
 *
 *	{obj | val} name is
 *	    components;
 * 	    operations;
 *	    equations;
 *	    other attributes;
 *	end name;
 *
 * The current tree represntation of objects and values is structrually the
 * same, with the 'isDef' flag set to true to distinguish values from objects.
 * This representation is an historical remnant of the fact that values were at
 * one time declared using the 'object' keyword, with a different syntax to
 * distinguish between types and values.  This should have been changed with
 * the introduction of the 'value' keyword, but alas was not.  So we have yet
 * another item to clean up.
 */
void chkObj (
    nodep t)
{
    SymtabEntry* sym = t->components.decl.kind.obj.sym;

    /*
     * Sym will be null for rules, which we'll deal with at some later date.
     */
    if (not sym)
	return;

    chkObjParents(t->components.decl.kind.obj.name, sym);
    if (ChkSymFlag(sym, isDef)) {
	chkValExprDecl(t, sym);
    }
    else {
	chkObjPartsDecl(t->components.decl.kind.obj.parts, sym);
    }
    chkOpsDecl(t->components.decl.kind.obj.ops);
    chkEqnsDecl(t->components.decl.kind.obj.eqns);
    chkObjAttrDecls(t->components.decl.kind.obj.attrs);

    /*
     * Resolve inheritance and process the where clause, as necessary.  Note
     * that where clause processing comes *after* inheritance resolution, which
     * means that the where clause is applied to all inherited stuff.
     * 
     * NOTE: ResolveInheritance and ProcessWhereClause now done in pass 2.
     *
     *
    ResolveInheritance(t, sym);
     *
    ProcessWhereClause(t, sym);
     *
     */

    /*
     * Help out the browser.
     */
    EnterBrowserInfo(t, sym);
}


/*
 * Check an operation decl of the form:
 *
 *	op name is
 *	    components;
 * 	    inputs;
 * 	    outputs;
 *	    preconds;
 *	    postconds;
 *	    other attributes;
 *	end name;
 */
void chkOp(
    nodep t)
{
    SymtabEntry* sym = t->components.decl.kind.op.sym;
    nodep p;
    TypeStruct t1;

    chkOpOverloading(sym);

    PushSymtab();
    MoveToSymtab(sym->Info.Op.Symtab);

    chkOpParms(sym->Info.Op.InParms);
    chkOpParms(sym->Info.Op.OutParms);

    /*
     * Note that the next call installs the op type if necessary.
     */
    chkOpPartsDecl(t->components.decl.kind.op.parts,
	sym, t->components.decl.kind.op.flags);

    /*
     * Next two superceded by chkOpParms calls.  However, the more specific
     * error messages in chk{Ins,Outs}Decl are appealing, and we should
     * consider how to get them back, if possible.  TODO.
     *
    chkInsDecl(t->components.decl.kind.op.ins, sym);
    chkOutsDecl(t->components.decl.kind.op.outs, sym);
     */

    /*
     * Check the pre/post decls, and if successful, store the exprs in the
     * symtab entry, for subsequent use by validate.c:doValidationCall, q.v.
     */
    if (chkPrePostcondDecl((p = t->components.decl.kind.op.precond), "pre")) {
	sym->Info.Op.precond = p->components.decl.kind.pre.expr;
    }
    if (chkPrePostcondDecl((p = t->components.decl.kind.op.postcond), "post")) {
	sym->Info.Op.postcond = p->components.decl.kind.pre.expr;
    }

    chkOpAttrDecls(t->components.decl.kind.op.attrs, sym);

    /*
     * Help out the browser.
     */
    EnterBrowserInfo(t, sym);

    /*
     * Increment act rec size by 2, for jmp_buf pointer and Display save
     * pointer.  This may increase further for trace-back info, as is done in
     * latest Modula-2 interpreter.
     */
    sym->Info.Op.Offset = CurSymtab->Offset;
    CurSymtab->Offset += 2;

    PopSymtab();
}


/*
 * Check an object's class parent, if any.  The restrictions are that the
 * parent must exist and multiple parents are not allowed in V3.
 *
 * An intresting note re. passes:  In this function we are in Pass 3.  What
 * should happen in a function like this is not to duplicate the checking logic
 * that was already performed in Pass 2, but to have Pass 2 generate, but not
 * output error message text, and then have this rule simply print out those
 * messages.  We should definitely do this as Pass 2 expands.
 */
chkObjParents(nodep t, SymtabEntry* sym)
{
    char* errmsg;

    for (errmsg = (char*) EnumCppList(sym->errors); errmsg;
	    errmsg = (char*) EnumCppList(sym->errors)) {
	/*
	 * Replace error with lerror if we want src loc's.  Also, change gen of
	 * these messages, as commented in ResolveInheritance, q.v.
	 */
	lchastise(t, "%s", errmsg);
    }
}


/*
 * Check an object components decl.  A type structure was built for the
 * components expr in pass 1.5.  What remains to be checked is that each of the
 * referenced types is defined.
 *
 * An archaic comment follows.  I'm not 100% certain that there's nothing to
 * it, but I'm 99% certain.  So the comment remains until I attain the last 1%
 * of certitude.
 *
 * Also in future, this is the place where we should detect all occurences of
 * recursive type refs, so that the appro pointer-based rep can be built.  This
 * does not have to happen until we want executability.
 */
void chkObjPartsDecl(
    nodep t,
    SymtabEntry* sym)
{
    nodep n, next_save;
    TypeStruct t1;
    SymtabEntry* partsym;
    char* qs;
    nodep found_node;	/* Found node returned from LookupQid */

    for (n=sym->Info.Obj.namelist; n; n=n->components.atom.next) {

	/*
	 * Temporarily swap .next2 with .next, just for this loop iteration.
	 * This will allow n to be procesed like a normal qid.  This is way
	 * funky, but it comes with the territory of using .next2 to allow qids
	 * to be elements of the parts list.
	 */
	next_save = n->components.atom.next;
        n->components.atom.next = n->components.atom.next2 ?
	    n->components.atom.next2 : null;

	partsym = LookupQidNoError(n, &found_node);
	if (not partsym) {
            if (not isConstAtom(n)) {
	      /* 
		 8may09: Sym lits are gone now, so this check is deprecated.

		 25oct07: don't complain about sym lits, but fix things for
	         them, obvimotherfuckingously.
	       */
/*	      if (n->header.name != Ysymlit) {	*/
		lchastise(n, "Component %s not defined.\n",
		    qs = qidToString(n));

		/*
		 * Make an entry for this undefined symbol so the browser can
		 * deal with it explicitly as such.
		 */
		BrowserEnterUndefined(qs);
/*	    }	*/
	    /* Think about what to do for the browser for const components. */
	  }
	}

	else {
	    if (partsym->Class != C_Obj) {
		lerror(n,
		    "Components of objects must be objects (%s is not).\n",
			partsym->Symbol);
	    }
	}

	n->components.atom.next = next_save;
    }
}

/*
 * Type check the name, type, and expr parts of a value decl.  I.e., check a
 * value decl of the form:
 *
 *     val name [: type] = expr ...
 *
 * If a type is explicitly specified, check that it's compat with the type of
 * the expr.  If both these checks succeed, store the type in the symtab entry.
 * The type stored is the declared type, if specified, otherwise it's the type
 * of checked expr.  The stored type is used subsequently in the Pass 4
 * evaluation.  Specifically, Pass 4 checks the type, and if non-null, proceeds
 * with the evaluation.
 *
 * As noted in the comment for chkObj, obj decls and val decls have the same
 * tree rep.  Therefore, any additional attributes in a value decl are checked
 * in common with object decls, in chkObj.  These additional attributes are the
 * in the "..." portion of the form abbreviation just above.
 *
 * Also very significant in this function is the check for circular value
 * declartions.  With untyped value decls, it may take an arbitrary number of
 * passes to resolve all forward references to value names.  (Recall the n-pass
 * requirement for resolving arbitrary references in attribute grammar
 * definitions.)  Given this, a check for circular value decls is required
 * here, since chkIdent will call this function recursively when it encounters
 * a value name with an as-yet undefined type.  The circularity check is
 * performed by pushing the entering type tree onto a tree-node stack, and
 * checking if the function is re-entered with same node before the stack is
 * cleared off.
 */
void chkValExprDecl(nodep t, SymtabEntry* sym) {
    TypeStruct t1, t2;
    nodep n = t->components.decl.kind.obj.name;
    nodep dtype;

    /*
     * Check for circularity.
     */
    if (InTreeStack(t)) {
	lerror(t, "Circularity detected in value declaration.\n");
/*	ClearTreeStack(); */
	return;
    }
    PushTree(t);

    /*
     * Initialize the type to null, for starters.
     */
    sym->Type = null;

    /*
     * Access the name component of the value decl.  In this case, the name is
     * actually a name/type pair, represented syntactically as attribute decl.
     * This makes things a it confusing nomenclaturally.  Whatever.
     */
    n = t->components.decl.kind.obj.name;

    /*
     * Type check the expr.
     */
    t1 = chkExpr(t->components.decl.kind.obj.parts, false, null);

    /*
     * Check if there's a declared type, and if so, that it's assmnt compat
     * with the expr type.  Assign the return type to the declared type if
     * present, or the expr type otherwise.
     */
    if ((t2 = t->components.decl.kind.obj.type) == null) {
        sym->Type = t1;
    }
    else {
        if (assmntCompat(t2, t1)) {
	    sym->Type = t2;
	}
	else {
	    lerror(t, "Declared value type and its expression type must be compatible.\n");
	    /*
	     * Go ahead and use the declared type, to avoid subsequent excess
	     * error messages.  This is a value judgement.
	     */
	    sym->Type = t2;
        }
    }

    PopTree();
}

/*
 * Return true if the given sym is a value decl, i.e., class = C_Obj and isDef
 * flag on.
 */
bool isValSym(SymtabEntry* sym) {
    return (sym and (sym->Class == C_Obj) and ChkSymFlag(sym, isDef));
}

/*
 * Return true if the give nodep is an ATOM_NODE, and constant value, i.e.,
 * string, integer, real, or nil.
 */
bool isConstAtom(nodep t) {
    return (t->header.kind == ATOM_NODE) &&
           ((t->header.name == Ystring) ||
            (t->header.name == Yinteger) ||
            (t->header.name == Yreal) ||
            (t->header.name == Ynil));
}

/*
 * This probably should go elsewhere, but whatever.
 */
char* qidToString(nodep qid) {
    char string[1000], *text;
    int i, j, l;
    nodep n;

/*    return qid->components.atom.val.text;    */

    for (n = qid, i = 0; n && i < 1000; n = n->components.atom.next) {
	for (j = 0, l = strlen(text = n->components.atom.val.text);
		j < l; j++, i++) {
	    string[i] = text[j];
	    if (n->components.atom.next) {
		string[++i] = '.';
	    }
	}
    }
    string[i] = '\0';

    return stralloc(string);
}
	    
/*
 * Check the ops part of an obj decl by confirming that each referenced op is
 * defined and that the signatures agree with the in/out decls in the
 * corresponding op defs.
 */
void chkOpsDecl(
    nodep t)
{
    /* TODO */
}


/*
 * Check the eqns part of an obj decl.  Var decl part is type checked as a
 * normal var decl.  LHS of each eqn must be a functional expr and RHS a
 * quantifier-free expr.  Other than that, both sides of each equn are simply
 * type checked normally.
 */
void chkEqnsDecl(
    nodep t)
{
    /* TODO */
}


/*
 * Check remaining obj attributes.  For comment-valued attributes, there's
 * nothing to do.  For entity-valued attributes, the entity must exist, and
 * then the relation defined (LATER on the relation defs).
 */
void chkObjAttrDecls(
    nodep t)
{
    /* TODO */
}


/*
 * Check that an op is a legal overload by confirming that its sig is not
 * identical to any extant op sig.  Also, check the special case that allows an
 * op to be the same name as an obj, as long as the op sig is identical to the
 * standard constructor sig for the extant obj.
 */
void chkOpOverloading(SymtabEntry* sym) {
    SymtabEntry* sym1;

    /*
     * Not sure when this could happen, but hey, it can't hurt to be safe.
     * Well, maybe it could hurt a little, but what's a little pain among
     * friends?
     */
    if (not sym)
	return;
     
    /*
     * Get a pointer to the beginning of the bucket, since sym may point
     * somewhere inside the bucket.
     */
    sym1 = Lookup(sym->Symbol);

    /*
     * Cruise the bucket, looking for (a) any op with an identical sig; (b) an
     * obj with a non-matching constructor sig.  Either case (a) or (b) is an
     * error.
     *
     * Evidently TODO.
     */
}


/*
 * Check an op parm list, either inputs or outputs, by checking that any
 * referenced ident types are now defined.
 */
void chkOpParms(
    SymtabEntry* parmlist)	/* An op parmlist thread */
{
    SymtabEntry* p;
    nodep n = NewNode(null,null,EmptyLoc); /* This is a little silly. Clearly,
					    * we could use an overloaded
					    * version of lerror that takes a
					    * src loc direclty instead of a
					    * node.  Oh well, C may have
					    * overloading some day. */

    for (p = parmlist; p ; p = p->Info.Parm.Link) {
	n->header.loc = p->Loc;
	ResolveIdentType(isListType(p->Type) ?
	    p->Type->components.type.kind.arraytype.basetype : p->Type,
	    n, true);
        p->Info.Parm.Offset = CurSymtab->Offset;
	CurSymtab->Offset += TypeSize(p->Type);
    }

    free(n);
}


/*
 * Check an operation components decl.  Despite some vague notion that there
 * should be some duality between obj and op components, it seems that
 * components of these two types of entities must be treated fundamentally
 * differently.  For now, what remains to be done here is to check that all
 * referenced ops are defined, or in the case of a def-type op (i.e., defined
 * with '=' expr), to type check the expr.
 *
 * In future, this is the place where we should attempt to build some
 * dataflow-style representation, using the and/or comp primitives in some
 * rigorous way to accomplish this.  Also, when we integrate formally with the
 * dataflow tool, this may be a place where some work is done, though most or
 * all of the datflow-related work may be done earlier, in EnterOp in
 * particular.
 */
void chkOpPartsDecl(
    nodep t,
    SymtabEntry* sym,
    unsigned int flags)
{
    TypeStruct t1;
    nodep n;
    SymtabEntry* partsym;

    if (ChkSubnodeFlag(flags, isDef)) {
	t1 = chkExpr(t, true, null);

	sym->Info.Op.Code.Tree = t;

	/*
	 * TODO: check that t1 agrees with output type, including multi-val
	 * output case.  Output error message as appro.
	 *
	if ((sym->Type != null) and (t1 != null) and
		not compat2(t1, sym->Type)) {
	    lerror(t, "Type of function expression not compatible with declared output type.\n");
	}
	 */

	/*
	 * Until the preceding TODO is completed, store the expr type as the
	 * return type, if the return type is null.
	 */
	if (sym->Type == null) {
	    sym->Type = t1;
	}
    }

    for (n= sym->Info.Op.namelist; n; n=n->components.atom.next) {
	if (not (partsym = Lookup(n->components.atom.val.text)))
	    lchastise(t, "Component %s not defined.\n",
		n->components.atom.val.text);
	else {
	    if (partsym->Class != C_Op) {
		lerror(t, "Components of operations must be operations (%s is not).\n",
		    partsym->Symbol);
	    }
	}
    }
}


/*
 * NOTE: Superceded by chkOpParms.
 *
 * Check the inputs part of an op decl by confirming that each of the
 * referenced types has been defined by now.
 */
void chkInsDecl(
    nodep t,
    SymtabEntry* sym)
{
    nodep n;
    SymtabEntry* insym;

    for (n= sym->Info.Op.ins; n; n=n->components.atom.next) {
	if (not (insym = Lookup(n->components.atom.val.text)))
	    lerror(n, "Input %s not defined.\n",
		n->components.atom.val.text);
	else {
	    if (insym->Class != C_Obj) {
		lerror(n, "Inputs must be objects (%s is not).\n",
		    insym->Symbol);
	    }
	}
    }
}


/*
 * NOTE: Superceded by chkOpParms.
 *
 * Check the outputs part of an op decl by confirming that each of the
 * referenced types has been defined by now.
 */
void chkOutsDecl(
    nodep t,
    SymtabEntry* sym)
{
    nodep n;
    SymtabEntry* outsym;

    for (n= sym->Info.Op.outs; n; n=n->components.atom.next) {
	if (not (outsym = Lookup(n->components.atom.val.text)))
	    lerror(n, "Output %s not defined.\n",
		n->components.atom.val.text);
	else {
	    if (outsym->Class != C_Obj) {
		lerror(n, "Outputs must be objects (%s is not).\n",
		    outsym->Symbol);
	    }
	}
    }
}


/*
 * Check the pre/postcond part of an op decl by type checking the expr and
 * confirming that it is of type bool.  Enter and exit the cond scope before
 * and after expr checking.
 */
bool chkPrePostcondDecl(
    nodep t,
    char* errstr)
{
    TypeStruct t1;
    nodep expr;

    if (t == null)
	return false;

    if ((expr = t->components.decl.kind.pre.expr) == null)
	return false;

    PushSymtab();
    MoveToSymtab(t->components.decl.kind.pre.symtab);

    if (not (t1 = ResolveIdentType(chkExpr(expr, true, null), expr, true))) {
	PopSymtab();
	return false;
    }

    if (not isBool(t1))
	lerror(expr, "Type of %scondition must be boolean.\n", errstr);

    PopSymtab();
    return true;
}


/*
 * Check a quantifier decl/expr of one of the forms:
 *
 *	[forall | exists] (varlist:identtype) expr
 *	[forall | exists] (var in expr) expr
 *	[forall | exists] (varlist:identtype | expr) expr
 *
 *
 * For all forms, the quantifier scope is first entered by descending into the
 * quantifier's local symtab.
 *
 * In forms 1 and 3, the varlist decls have already been entered into the
 * quantifier's symtab, but the ident types have not yet been resolved.  Hence,
 * this resolution must be performed, reporting any undef'd ident types that
 * are found.  After this, the suchthat expr (form 3) and body expr must
 * evaluate to a bool.
 *
 * In form 2, the var has not yet been entered, since its type depends on the
 * the of the 'in' expr.  Viz, the type of the var is the basetype of the 'in'
 * expr, which must be a list type.  After this checking is performed, the 'in'
 * var is entered into the symtab, for subsequent lookup as the body is
 * checked, which must evaluate to bool
 *
 * Note the slight bit of tree trickery used to distinguish forms 2 and 3.
 * Viz., the decl.kind.quant.in field points to unop node, the name of which is
 * either YIN (for form 2) or '|' (for form 3).
 *
 * The remaining two paragraphs are historical notes, regarding the on-again,
 * off-again scope issues of quantifiers.  Bottom line is that quantifier
 * expression DO in fact define a new local scope.
 *
 * 9nov01 Note: Ignore the 8nov01 note.  Quantifiers have their own scopes
 * again, to avoid global binding effects of them not having  scopes.  See LOG
 * entry of this date for further discussion.
 *
 * 8nov01 Note: As of now, quantifiers don't have their own scopes, but rather
 * exist in the parent scope.  So, in the comments that follow, ignore the
 * references to entering the quantifier scope and replace "quantifier scope"
 * with "parent scope".
 */
TypeStruct chkQuant(
    nodep t,
    bool f)
{
    TypeStruct t1, t2, rtn;
    nodep in;
    bool inok = true;

    PushSymtab();
    MoveToSymtab(t->components.decl.kind.quant.symtab, true);

    /*
     * Check which form we're dealing with and handle the particulars.
     */
    if (in = t->components.decl.kind.quant.in) {
	switch (in->header.name) {
	    case YIN:
		inok = chkQuantInClause(t->components.decl.kind.quant.vars,
		    in->components.unop.operand, f);
		break;
	    case '|': 
		inok = chkQuantSuchthatClause(
			t->components.decl.kind.quant.vars,
			    in->components.unop.operand, f);
		break;
	}
    }
    /*
     * It's likely we've got a quantifier of the format: {forall, exists} (var:type) (expr)
     *
     * That doesn't mean we shouldn't make space in the symtab for the variable(s) here,
     * so we'll make space in the symtab for the variable(s) here.
     */
    else {
	SymtabEntry* sym;
	nodep var;
	char* varname;
	for (var = t->components.decl.kind.quant.vars; var;
		var = var->components.atom.next) {
	    varname = var->components.decl.kind.var.vars->
		components.atom.val.text;
	    sym = Lookup(varname);

	    /*
	     * All of these var names should already have been entered via
	     * EnterVars, called from the name_obj_pair rule in the parser,
	     * which is in turn referenced from the quantifier RHS.  However,
	     * as a protective measure, we'll allocate a symtab entry if it's
	     * not already been.
	     */
	    if (!sym) {
		t1 = t->components.decl.kind.quant.vars->
		    components.decl.kind.attr.value;
		t2 = ResolveIdentType(BuildCompType1(t1), t1, true);
		Enter(sym = HashAllocSymtabEntry(
		    varname, C_Var, t2, CurSymtab->Level));
	    }

	    /*
	     * Assign a memory offest to the var.
	     */
	    sym->Info.Var.Offset = CurSymtab->Offset;
	    CurSymtab->Offset += TypeSize(sym->Type);
	} // end for
    }

    /*
     * Increment act rec size by 1 for Display save pointer.  See chkProcCall
     * comments for further discussion.  This incrementation is also do in
     * chkExprSeq, which is also scope-defining.
     */
    CurSymtab->Offset++;

    /*
     * Now check the body expr and complain if not bool.
     */
    if (not (t1 = ResolveIdentType(
	    chkExpr(t->components.decl.kind.quant.expr, f, null), t, true))) {
	PopSymtab();
	return null;
    }

    if (isBool(t1)) {
	rtn = BoolType;
    }
    else {
	lerror(t->components.decl.kind.quant.expr,
	    "Type of a quantifier body must be boolean.\n");
	rtn = null;
    }

    PopSymtab();
    return inok ? rtn : null;
}

bool chkQuantInClause(nodep vars, nodep inexpr, bool f) {
    TypeStruct t1, basetype;
    SymtabEntry* sym;
    bool rtn = true;
    nodep var;

    t1 = ResolveIdentType(chkExpr(inexpr, f, null), inexpr, true);

    if (t1 and (not isListType(t1))) {
	lerror(inexpr, "Type of quantifier 'in' expression must be list.\n");
	basetype = null;
	rtn = false;
    }
    else {
	basetype = t1 ? 
	    t1->components.type.kind.arraytype.basetype : null;
    }

    /*
     * Go ahead and make the entry(ies), even if t1 is in error.  In this way,
     * when we check the body back in chkQuant, we won't see any extra undecl
     * errors for the 'in' var, even though we might "officially" want to.
     */
    for (var = vars; var; var = var->components.atom.next) {
	Enter(sym = HashAllocSymtabEntry(var->components.atom.val.text, C_Var, basetype,
	    CurSymtab->Level));
        sym->Info.Var.Offset = CurSymtab->Offset;
        CurSymtab->Offset += TypeSize(sym->Type);
    }

    return rtn;
}

/*
 * Resolve var type decls and verify the suchthat expr is bool.
 */
bool chkQuantSuchthatClause(nodep vars, nodep suchthatexpr, bool f) {
    nodep vardecl, t;
    char* varname;
    SymtabEntry* sym;
    bool rtn = true;
    TypeStruct t1;

    /*
     * Cruise the var decl list, verifying (i.e., resolving) each type.  We're
     * in luck that types are syntactically restricted to ident types.  Thanks
     * for small favors, anyway.
     *
     * If we were lazy, we'd just scan the symtab, but that would put error
     * messsages out in hashed order.  This would be a very minor problem in
     * most cases, but it's not really right.  And we just *cant* do anything
     * that isnt really right, now can we!?
     */
    for (vardecl = vars; vardecl; vardecl = vardecl->components.decl.next) {
	t = vardecl->components.decl.kind.attr.value;
	if (not (t1 = ResolveIdentType(BuildCompType1(t), t, true))) {
	    rtn = false;
	}
	varname = vardecl->
	    components.decl.kind.var.vars->components.atom.val.text;
	sym = Lookup(varname);

	/*
	 * See comment in chkQuant regarding these syms already being entered,
	 * but guarding here protectively.
	 */
	if (!sym) {
	    Enter(sym = HashAllocSymtabEntry(
		varname, C_Var, t1, CurSymtab->Level));
	}

	/*
	 * Assign a memory offest to the var.
	 */
	sym->Info.Var.Offset = CurSymtab->Offset;
	CurSymtab->Offset += TypeSize(sym->Type);
    }

    /*
     * Now check the suchthat expr to be bool.
     */
    if (not (t1 = ResolveIdentType(chkExpr(suchthatexpr, f, null),
	    suchthatexpr, true)))
	return false;
    else if (isBool(t1)) {
	return rtn;
    }
    else {
	lerror(suchthatexpr, "Type of quantifier such that expression must be bool.\n"); 
	return false;
    }
}


/*
 * Type check a let expr of the following form
 *
 *	let namelist [ : type ] = expr;
 *
 * by entering each name in namelist in the current scope.  Figure out the
 * types of namelist names as follows:
 *
 *     (1) If the optional type decl is given, then it's that type, which must
 *         also be compat with the type of the expr.
 *     (2) Otherwise, it's the type of the expr.
 *	   
 */
TypeStruct chkLet(nodep t, bool f) {
    TypeStruct t1, rtn;
    SymtabEntry* sym;
    nodep n;

    /*
     * Disallow let outside of expr seq.  This could be done syntactially, but
     * it's much more painful that way.
     */
    if (not isAnonScope(CurSymtab)) {
	lerror(t, "Let expr only allowed in an expr sequence.\n");
	return null;
    }

    /*
     * Type check the expr first off.  We won't leave if there's an error, so
     * we can make entries for the let vars, a la chkQuantInClause.  This makes
     * the user-level type checking experience a tad less painful.  (OK, so it
     * really only is a *tad*.)
     *
     * Note carefully that the let expr is checked before the initial entry of
     * the let var in the current scope.  This means if the let var is already
     * bound in this or a parent scope, then the type of that existing binding
     * is used in the type checking.  This implements the proper semantics of
     * let, i.e., the RHS expr is evaluated in the pre-binding environment.
     */
    t1 = chkExpr(t->components.decl.kind.let.expr, f, null);

    /*
     * Check if there's a declared type, and if so, that it's assmnt compat
     * with the expr type.  Assign the return type to the declared type if
     * present, or the expr type otherwise.
     */
    if ((rtn = t->components.decl.kind.let.type) == null) {
        rtn = t1;
    }
    else {
        if (! assmntCompat(rtn, t1)) {
	    lerror(t, "Let type and value expression must be compatible.\n");
        }
    }

    /*
     * Traverse the list of names, entering or redeclaring each.  Entering
     * happens when the name has not yet been let-declared in the current
     * scope.  In this case, the a new symtabe entry is created, with storage
     * allocated.
     *
     * If the name has already been entered in the expr sequence scope, then
     * change the existing entry's type.  I.e., do not reenter and realloc
     * storage.
     *
     * Note well that this entry processing imposes lexical order dependence on
     * the type checking of lets, per the semantics current semantics.  In Lisp
     * terms, SpecL let is let*.
     */
    for (n = t->components.decl.kind.let.names; n != null;
	     n = n->components.atom.next) {

	sym = LookupThisScope(n->components.atom.val.text);
	if (sym == null) {
	    Enter(sym = AllocSymtabEntry(
		n->components.atom.val.text, C_Let_Var, rtn, CurSymtab->Level));
	    sym->Info.Var.Offset = CurSymtab->Offset;
	    CurSymtab->Offset += TypeSize(sym->Type);
	}
	else {
	    sym->Type = rtn;
	}
    }

    /*
     * Return the decided-upon return type.
     */
    return rtn;
}


/*
 * Type check an instance extraction expr of the form
 *
 *	desig '.<' name
 *
 * where desig must be a class type, and name must be the name of one of its
 * instances.  Return the instance type if successful, null oherwise.
 */
TypeStruct chkGetInstance(nodep t, bool f) {
    TypeStruct desig;
    nodep left;
    char* name;
    SymtabEntry* namesym;
    TypeStruct rtn;

    if (not (desig = chkExpr(t->components.binop.left_operand, f, null)))
	return null;
  
    /*
     * Complain if checked left operand is not an ident type.
     */
    if ((not isOrWasIdentType(desig)) or
	    (not desig->components.type.origname)) {
	lerror(t, "Left operand of .< is not of a subclassable type.\n");
	return null;
    }

    /*
     * Complain if right operand is not a type name at all.
     */
    if (not (namesym = Lookup(name =
	    t->components.binop.right_operand->components.atom.val.text))) {
	lerror(t, "Right operand of .< is not a subtype of the left operand.\n");
	return null;
    }

    if (not isTypeSym(namesym)) {
	lerror(t, "Right operand of .< is not a subtype of the left operand.\n");
	return null;
    }

    /*
     * SubtypeCompat1'll do the rest.
     */
    if (subtypeCompat1(
	    desig->components.type.origname->components.atom.val.text,
		t->components.binop.right_operand->components.atom.val.text)) {
	rtn = ResolveIdentType(namesym->Type, t, true);
	/*
	 * The following is a bit (maybe a lot) hokey, but it will allow .< ops
	 * to be chained in subexprs by forcing the return type here to have an
	 * origname.
	 */
	if (not rtn->components.type.origname) {
	    rtn->components.type.origname =
		NewNode(ATOM_NODE, Yident, EmptyLoc);
	    rtn->components.type.origname->
		components.atom.val.text = namesym->Symbol;
	}
	return rtn;
    }

    lerror(t, "Right operand of .< is not a subtype of the left operand.\n");
    return null;
}


/*
 * Type check an instance checking expr of the form
 *
 *	desig '?<' name
 *
 * where desig must be a class type, and name must be the name of one of its
 * instances.  Return BoolType if successful, null otherwise.
 */
TypeStruct chkChkInstance(nodep t, bool f) {
    TypeStruct desig;
    nodep left;
    char* name;
    SymtabEntry* namesym;

    if (not (desig = chkExpr(t->components.binop.left_operand, f, null)))
	return null;
  
    /*
     * Complain if checked left operand is not an ident type.
     */
    if ((not isOrWasIdentType(desig)) or
	    (not desig->components.type.origname)) {
	lerror(t, "Left operand of ?< is not of a subclassable type.\n");
	return null;
    }

    /*
     * Complain if right operand is not a type name at all.
     */
    if (not (namesym = Lookup(name =
	    t->components.binop.right_operand->components.atom.val.text))) {
	lerror(t, "Right operand of ?< is not defined in this scope.\n");
	return null;
    }

    if (not isTypeSym(namesym)) {
	lerror(t, "Right operand of ?< is not a type name.\n");
	return null;
    }

    /*
     * SubtypeCompat1'll do the rest.
     */
    if (subtypeCompat1(
	    desig->components.type.origname->components.atom.val.text,
		t->components.binop.right_operand->components.atom.val.text)) {
	return BoolType;
    }

    lerror(t, "Right operand of ?< is not a subtype of the left operand.\n");
    return null;
}


/*
 * Type check an attr selection expr of the form
 *
 *	o.-attr
 *
 * where o is an defined object, and attr is the name of one of its attributes.
 * Return type is the type of its attr, if it is a def'd ident type, string if
 * it is a comment, error otherwise.
 */
TypeStruct chkAttrSelect(nodep t, bool f) {
    TypeStruct t1,t2;
    nodep* attrsPtr;
    SymtabEntry* sym;
    char* name;
    nodep n, n1;

    if ((t1 = chkExpr(t->components.binop.left_operand, f, null)) == null)
	return null;

    if (not isIdentType(t1)) {
	lerror(t, "Left operand of '.-' is attribute selectable.\n");
	return null;
    }
	
    if (not (sym = Lookup(t1->components.type.kind.ident.type->
	    components.atom.val.text))) {
	lerror(t, "Left operand of '.-' is not defined.\n");
	return null;
    }

    if (sym->Class == C_Obj)
	attrsPtr = &(sym->Info.Obj.attrs);
    else if (sym->Class == C_Op)
	attrsPtr = &(sym->Info.Op.attrs);
    else {
	lerror(t, "Left operand of '.-' is not an object or operation.\n");
	return null;
    }

    /*
     * Cruise the attrs list, looking for the given name.
     */
    for (n = *attrsPtr,
	    name = t->components.binop.right_operand->components.atom.val.text;
		n; n = n->components.decl.next) {
	if ((n1 = n->components.decl.kind.attr.name) and
		streq(name, n1->components.atom.val.text))
	    return figureAttrType(n);
    }

    lerror(t, "%s is not an attribute of the entity on the lef of the '.-'\n",
	name);
    return null;
}


/*
 * Figure out what type of dodah to return for a successful attr select op.
 */
TypeStruct figureAttrType(nodep attr) {
    SymtabEntry* sym;
    nodep v;

    if ((v = attr->components.decl.kind.attr.value)->header.name == Ytext)
	return StringType;
    else
	if (not (sym = Lookup(v->components.atom.val.text))) {
	lerror(attr, "Right operand of '.-' is not defined.\n");
	return null;
    }

    return sym->Type;
}


/*
 * Type check an if expr by checking that the expr is bool, and that the then
 * and else parts are compat.  If all goes well, return the type of the then
 * (= else) part, else null.
 *
 * A couple special-case checks need to be made for int/real and lit type
 * compatibility of then and else clauses.  Specifically, if the types are
 * mixed int and real, then real is the return type.  If the types are
 * base-type compatible lit types, then the return type is the base type.
 */

TypeStruct chkIfExpr(
    nodep t,
    bool f)
{
    TypeStruct t1, t2, t3;
    nodep e;
    bool exprerr = false;

    if (not isBool(ResolveIdentType(
	    chkExpr((e = t->components.trinop.left_operand), f, null),
		t, true))) {
	lerror(e, "Type of if expression must be boolean\n");
	exprerr = true;
    }
    t2 = chkExpr(t->components.trinop.middle_operand, f, null);
    t3 = chkExpr(t->components.trinop.right_operand, f, null);

    /*
     * Handle special case of literal type then and else clauses.
     * Specifically, promote types to base types, and then let the subsequent
     * logic deal with them.
     */
    if (isLiteralType(t2) and isLiteralType(t3)) {
	t2 = t2->components.type.kind.lit.type;
	t3 = t3->components.type.kind.lit.type;
    }

    /* t2 and t3 have to be compatible OR t2 can be filled in, with t3 null */
    if ((not exprerr) and (compat2(t2, t3) || ((t2 != null) && (t3 == null)) )) {
	/*
	 * As special case, force return type to be real if there's a real/int
	 * mix.
	 */
	if (isReal(t2) or isReal(t3))
	    return RealType;

	return t2;
    }


    if ((not exprerr) && (t3 != null) && (t2 != null)) {
        lerror(t,
	    "Type of then expression not compatible with else expression.\n");
    }

    return null;
}

bool isSubType(
    TypeStruct t1,
    TypeStruct t2)
{
    /* TODO */
    return false;
}

bool isMultValFcnType(
    TypeStruct t)
{
    /* TODO */
    return false;
}

/*
 * This function is defeind ealier above -- figure out what's up (TODO).
 *
bool oneLevelStructRecEquiv()
{
    return false;
}
 */

void chkPartsDecl(
    nodep t)
{
    /* TODO */
}

void chkOpAttrDecls(
    nodep t,
    SymtabEntry* sym)
{
    /* TODO */
}


/*
 * Check for transitive chain of same-name type compatibility.  VERY IMPORTANT.
 * NOTE: must check for recursion, so as not to get in endless search, which is
 * done in ResolveToBaseIdentType, q.v.
 */
bool identCompat(TypeStruct t1, TypeStruct t2) {
    TypeStruct rt1, rt2;

    rt1 = ResolveToBaseIdentType(t1, null, false);
    rt2 = ResolveToBaseIdentType(t2, null, false);

    return ((rt1 == rt2) or
	(isInt(rt1) and isReal(rt2)) or (isInt(rt2) and isReal(rt1)));
}

/*
 *
 * Deprecated.  Will be removed when it's 100% clear that sym lits should no
 * longer exist.
 *
 * Check for symlit compatibility, with the symlit in t2, and the target type
 * in t1.  The target type must have the same name as the spelling of t2, and
 * the target type must be opaque.  Given that t1 has be resolved out, we'll
 * use the orignname component for comparison.  This needs to be put to the
 * test, of course.
 */
bool symlitCompat(TypeStruct t1, TypeStruct t2) {
    nodep on;
    char* name;

    if (not isSymlitType(t2)) return false;

    if (t1 == null) return false;

    if ((on = t1->components.type.origname) == null) return false;

    if ((name = on->components.atom.val.text) == null) return false;

    return streq(name, t2->components.type.kind.symlit);
}

/*
 * Check for the compatibility of a literal type and it's base type.  The rule
 * for literal compatibility is explained in the ref manual in terms of type
 * spellings.  A summary is the following:
 *
 *     * the type of a literal X of type T is "the T X" (not just T)
 *
 *     * like assignment compatibility, literal compatibility is an asymmetric
 *       relationship, specifically "the T X" is compatible with "T", but vice
 *       versa
 */
bool litCompat(TypeStruct base, TypeStruct lit) {
    if (isLiteralType(lit)) {
	return compat(base, lit->components.type.kind.lit.type);
    }
    return false;
}

bool litCompat2(TypeStruct t1, TypeStruct t2) {
    return litCompat(t1, t2) or litCompat(t2, t1);
}

bool litBaseCompat(TypeStruct t1, TypeStruct t2) {
    return isLiteralType(t1) and isLiteralType(t2) and 
	compat(t1->components.type.kind.lit.type,
	    t2->components.type.kind.lit.type);
}

bool litBaseCompat2(TypeStruct t1, TypeStruct t2) {
    return litBaseCompat(t1,t2) or litBaseCompat(t2,t1);
}

/*
 * Check an axiom or theorem of the form
 *
 *	AXIOM | THEROREM expr
 *
 * by checking the expr and confirming the it is of type bool.  The scope of
 * the formal def is entered and exited before and after checking, resp.
 */
void chkAxOrThm(nodep t, char* msgstr) {
    TypeStruct t1;
    nodep expr = t->components.decl.kind.formaldef.expr;

    PushSymtab();
    MoveToSymtab(t->components.decl.kind.formaldef.symtab, true);

    if (not (t1 = ResolveIdentType(chkExpr(expr, true, null), expr, true))) {
	PopSymtab();
	return;
    }

    if (not isBool(t1))
	lerror(expr, "Type of %s expression must be boolean\n", msgstr);

    PopSymtab();
}

/*
 * Check a formal var decl of the form
 *
 *	VAR vars: type;
 *
 * by type checking the type.  Allocate storage if the type is OK.
 */
void chkFormalVarDecl(nodep vardecl) {
    TypeStruct t, type;
    nodep v;
    SymtabEntry* s;

    type =  vardecl->components.decl.kind.var.type;
    if (not type) {
	lerror(vardecl, "Variables must be declared with a type.\n");
	return;
    }

    t = ResolveIdentType(BuildCompType(type), type, true);

    for (v = vardecl->components.decl.kind.var.vars; v != null;
	    v = v->components.atom.next) {
	s = Lookup(v->components.atom.val.text);

	/*
	 * Make the type right, for list types; it's funky coming from the
	 * parser.
	 *
	 * TODO: Fix this in the parser, so the special-case check for list
	 * type does not have to be done here.
	 */
	if (t->header.name == YARRAY) {
	    s->Type = t;
	}
	s->Info.Var.Offset = CurSymtab->Offset;
	CurSymtab->Offset += TypeSize(s->Type);
    }

    /*
     * TODO: check initialized and untyped forms, including error message for
     * if untyped form is not initialized.
     */
}

/*
 * Quicky string compare function to use in InList.
 */
bool StringEquals(void* s1, void* s2) {
    return streq((char*) s1, (char*) s2);
}

/*
 * Resolve inheritance for objects.  See the ref man for details of precisely
 * what this entails.  See individual comments below for further discussion.
 *
 * Note that since this resolution is being done in the 2nd pass, no error
 * messages are output.  Rather, errors are output in pass 3, specifically in
 * chkParents, called from chkObj.
 */
void ResolveObjInheritance(nodep t, SymtabEntry* sym) {
    char* name, *pname;
    nodep parent;
    SymtabEntry* psym;
    TypeStruct kidtype;
    Symtab* kidtab;
    char* errmsg;
    List* seenlist = NewList();
    nodep origname;
    TypeStruct t1, t2;

    /*
     * Lookup immediate parent and leave if none.
     */
    if (not (parent = sym->Info.Obj.inheritsfrom))
	return;

    /*
     * Disallow inheritance from a qualident.
     */
    if (parent->components.atom.next) {
	lerror(parent, "Inheritance using qualified identifiers is disallowed.\n");
        return;
    }

    /*
     * Grab a copy of this obj's name.
     */
    name = sym->Symbol;

    /*
     * If this object is not already a tuple, make it one, but record for
     * posterity that it once was an ident type, if it is now, posterity being,
     * in fact, subtypeCompat, q.v.
     */
    t1 = sym->Type;
    if (not isRecord(t1 )) {
	if (isIdentType(t1)) {
	    origname = t1->components.type.kind.ident.type;
	}
	sym->Type = BuildNewTupleType(sym->Type);
	sym->Type->components.type.origname = origname;
    }

    /*
     * Mark parent as seen, so circular inheritance can be detected.
     */
    PutList(seenlist, (void*)
	stralloc(pname = parent->components.atom.val.text));

    /*
     * Do error message construction for just this level, so that errors are
     * not reported repeatedly through transitive traversal up parent chains.
     */
    if (not (psym = Lookup(pname))) {
	if (not sym->errors)
	    sym->errors = NewCppList();

	/*
	 * Put the following back in if we want src loc info for this error
	 * message.  Right now we dont, since this message comes out with the
	 * other "Components ... not defined" msgs for an object, and these
	 * msgs have no src loc.
	 *
	PutList(sym->errors, errmsg = (ListElem) malloc(
	    strlen(pname) + strlen(name) +
		strlen("Parent class  not defined.\n") + 1));
	sprintf(errmsg, 
	    "Parent class %s of %s not defined.\n", pname, name);
	 *
	 */

	PutCppList(sym->errors, (void*) (errmsg = (char*) malloc(
	    strlen(pname) +
		strlen("Parent class %s not defined.\n") + 1)));
	sprintf(errmsg, "Parent class %s not defined.\n", pname);

	DelList(seenlist);
	return;
    }

    /*
     * Complain if multiple parents.  Note well that it's the next2 link that's
     * used to chain up multiple parents.
     */
    if (parent->components.atom.next2) {
	if (not sym->errors)
	    sym->errors = NewCppList();
	PutCppList(sym->errors, (void*) (errmsg = (char*) malloc(
	    strlen("Multiple inheritance not yet supported.\n"
		+ 1))));
	sprintf(errmsg,
	    "Multiple inheritance not yet supported.\n");
    }

    /*
     * Make convenience copies of this object's type and tuple symtab.
     */
    kidtype = sym->Type;
    kidtab = kidtype->components.type.kind.record.fieldstab;

    /*
     * Go through each parent, adding each distinct-name, uninherited symbol to
     * the symtab of this object.  In this way, we can resolve inheritance
     * piecewise, without a global inheritance map, nor concern of decl order.
     */
    while (psym) {

	/*
	 * Just quit outright if psym->Type == nil.  This can happen (at least)
	 * in the case of an undef'd import.
         */
	if (not psym->Type) {
	    break;
	}

	/*
	 * Mark the parent as being inherited from.  This once was used in the
	 * anti-covariance mutation check in chkAssmnt, but these checks are
         * gone now that list covariance is deprecated.  The isClass flag may
         * be used elsewhere in some future implementation.
	 */
       SetSymFlag(psym, isClass);

	/*
	 * Error if class of inherited-from symbol is not C_Obj.  The pass 2 vs
	 * 3 error msg ordering is a pain the ykw, and not working that well
	 * anyway, so the error just goes out right here.  The whole error msg
	 * ordering thing needs to be fixed.
	 */
	if (psym->Class != C_Obj) {
	    lerror(parent, "Objects can only inherit from other objects.\n");
	}

	/*
	 * Snatch appropriate parent fields.
	 */
	SnatchParentFields(psym, sym);

	/*
	 * Quit the loop when no more parents.
	 */
	if (not (parent = psym->Info.Obj.inheritsfrom))
	    break;

	/*
	 * Quit the entire function if circularity detected in inheritance
	 * chain.
	 */
	if (InListWithFunction(seenlist,
		pname = parent->components.atom.val.text, StringEquals)) {
	    if (not sym->errors)
		sym->errors = NewCppList();
	    PutCppList(sym->errors, (void*) hashsave(
		"Circularity detected in inheritance chain.\n"));
	    DelList(seenlist);
	    return;
	}

	/*
	 * Resolve operation inheritance.
	 */
	ResolveOpInObjInheritance(t, sym);

	/*
	 * Resolve equation inheritance.
	 */
	ResolveEqnInheritance(t, sym);

	/*
	 * Lookup next parent symbol and continue loop.
	 */
	psym = Lookup(pname);
    }

    /*
     * Fix up the fields list decl list.  This is where we could realloc a more
     * appropriately-sized record symtab (TODO).
     *
    sym->Type->components.type.kind.record.fields =
	FixDeclList(sym->Type->components.type.kind.record.fields);
     */

    /*
     * Clear out the temp list for detecting circularities.  Still not clear if
     * list is needed, but it works, so hey.
     */
    DelList(seenlist);
}

/*
 * NOTE: As of 20nov04, we I decided to disallow inheriting from a qualident,
 * given that allowing it was getting out of hand.  There may be a way to do it
 * cleanly, but I can't see it right now, given the current reliance on plain
 * names in the inheritance hierarchy.  A seemingly nasty snare is if we mangle
 * the qualident and enter it locally, as the following comment to this
 * would-be function indicates, then if it inherits from unmangled names in its
 * own scope, how to we deal with those in the local scope?  Hence, we've
 * decided as we have to disallow qualident inheritance.  This seems like a
 * pretty minor thing, in fact, since users can either do an unqualified import
 * of a type name or define one locally for inheritance purposes, based on the
 * qualified import nae.
 * 
 * The comment of the actual, but would-be method now follows.
 *
 * If an inherited-from name is a qualident, resolve it down to its rightmost
 * component and create a mangled-name ident type for it in the local symtab.
 * Do this only once for each distinct type that is inherited from as a
 * qualident.  The local mangled name is used to allow subtype compat checking
 * to use a flat string name consistently.
 *
 * It would appear that creating such a mangled name is more than just a
 * convenience issue for subtypeCompat.  The fundamental semantics of of
 * subtype compatibility relies on name-based inheritance.  So, when an
 * inherited-from name is a qualident, it needs to be considered "a name" in a
 * fundamental sense.  But since a qualident is really an expression, it needs
 * to be "flattened" into a name.  We use an actual "." char in the name to
 * avoid any possible conflict with a user-defined type name.
 */
char* ResolvedInheritedFromName(nodep parent) {

    /*
     * If parent is not a qualident it, then just return its text value.
     */
    if (not parent->components.atom.next) {
	return parent->components.atom.val.text;
    }

    /*
     * If parent is a qualident, mangle its name for starters.
     */

    /*
     * If this mangled name has already been entered locally as an ident type,
     * then return that type.
     */

    /*
     * At this point, we have a qualident with no local mangled name having yet
     * been created for it locally.  This means it's the first time we've been
     * here, so we need to check that the rightmost components of the qualident
     * is in fact an ident type.
     */

    /*
     * There would be more, but it's been aborted per the above NOTE in the
     * header comment.
     */
}

/*
 * Resolve inheritance for operations.  Details of this were yet to be added to
 * the ref man at the time of this writing, so here's the deal:
 *
 *     * When an op O2 inherits from op O1, formals from the arity and coherity
 *	 are anded onto the *beginning* of the O2 arity and coarity, resp.
 */
void ResolveOpInheritance(nodep t, SymtabEntry* sym) {
    nodep parent;

    /*
     * Lookup immediate parent and leave if none.
     */
    if (not (parent = sym->Info.Op.inheritsfrom))
	return;

    /* TODO */

}


/*
 * Make the inferred tuple type for an instance object, if the object is not
 * already a tuple.  Hmm, I guess we don't have a really good way of counting
 * the number of entries.  So, in contrast to how it's done elsewhere, let's
 * just guess 25.  That should be plenty.  Thanks for bucket hashing, too.  We
 * could of course rehash when we're done, but we'll leave that a TODOer.
 */
TypeStruct BuildNewTupleType(TypeStruct type) {
    return BuildNewTupleTypeSized(type, 25, false);
}

/*
 * Work doer BuildNewTupleType and also for starting from BuildFullTupletype.
 * In the former case, we don't want to make an entry for an opaque type,
 * whereas in the latter case we do.  This was discovered as a bug (hey, what
 * wasn't?).
 */
TypeStruct BuildNewTupleTypeSized(TypeStruct type, int size, bool full) {
    TypeStruct newtype;
    Symtab* st;
    nodep f;
    nodep* prevnode;

    /*
     * Build the record type.  Note that we might be tempted not to build a
     * field list, since the fields symtab will be used exclusively for any
     * subsequent access to the fields.  However, we need the fields list for
     * struct compat.
     */
    newtype = NewNode(TYPE_NODE, YRECORD, type->header.loc);

    /*
     * Build the tab.
     */
    newtype->components.type.kind.record.fieldstab = (st =
	AllocSymtab(size));
    st->ParentTab = CurSymtab;
    st->ParentEntry = ARecordEntry;
    st->Level = CurSymtab == (Symtab *)0 ? 0 : CurSymtab->Level + 1;
    st->Offset = 0;

    /*
     * Init the field count to 0, to be bumped to 1 subsequently by
     * EnterSingleTupleField, unless we have an opaque type, in which case the
     * field count stays 0.
     */
    newtype->components.type.kind.record.numfields = 0;

    /*
     * Make the lone entry, with inherited entries to follow, presumably.  Note
     * that we dont make any entry for an opaque type.  Later we'll check for
     * 0-tuple, and revert such back to an opaque type.
     */
    if ((not isOpaqueType(type)) or full) {
	prevnode = &(newtype->components.type.kind.record.fields);
	EnterSingleTupleField(st, type, newtype, &prevnode, full);
    }

    return newtype;
}


/*
 * Snatch each distinct-name, uniherited symbol from the parent, sticking each
 * in this obj's tuple symtab, and marking each as inherited.  Also, splice
 * each new file into the correct place in the field list, viz., starting at
 * the head of the extant field list.
 */
void SnatchParentFields(
    SymtabEntry* psym,		/* Symtab entry for parent class */
    SymtabEntry* kidsym)	/* Symtab entry for instance object */    
{
    Symtab* kidtab;		/* Symtab for instance object */
    char* fname = null;		/* Name of inherited field */
    TypeStruct kidtype;		/* Type for instance object */
    char* errmsg;
    nodep field;		/* Field pointer in field list traversal */
    nodep* prevnode;		/* Field list node after which new node is
				   spliced in */
    nodep vars;

    /*
     * Grab pointers to the type and record field tab for the instance object.
     */
    kidtype = kidsym->Type;
    kidtab = kidtype->components.type.kind.record.fieldstab;

    /*
     * Init the prev field list node pointer so that splicing-in will be done
     * right.  Despite what might be considerd better judgement, we're doing
     * the splice-in using the C pointer-to-pointer splicing hack.  Recall that
     * this allows the non-uniformity of the initial head pointer to be
     * ignored, since we point directly at the field of a struct, whether its
     * components.type.kind.record.fields or components.decl.next.  This
     * hackery is even nastier than usual, since we're passing the prevnode
     * pointer to the Enter*TupleField functions, which means that the pointer
     * is a node*** by the time it gets into those functions.  Geeze loueeze.
     */
    prevnode = &(kidtype->components.type.kind.record.fields);

    /*
     * If the parent is not a tuple, grab its top-level type as a new single
     * field.
     */
    if (not isRecord(psym->Type)) {
	EnterNonTupleInheritedField(kidtab, psym->Type, kidtype, kidsym,
	    &prevnode);
	return;
    }

    /*
     * 22dec00 Update: We do in fact now enter default-name fields.  If we
     * don't struct type equiv can't work.
     *
     * If the parent is a tuple, then cruise its record symtab, picking up each
     * of its fields, as long as each is not already in kid tab, not a default
     * name (of the form "[i]" (see EnterAndField)) and not inherited.  The
     * deal with the latter restriction is that we don't want to get in some
     * order-related tangle, since lexical order and inheritance order are
     * quite distinct.  To avoid the tangle, we always go direct to the source,
     * rather than grabbing alreay inherited symbols.  Get it?
     */
    for (field = psym->Type->components.type.kind.record.fields;
	    field; field = field->components.decl.next) {

	if (field->components.decl.kind.field.isinherited) {
	    continue;
	}

	if (vars = field->components.decl.kind.field.vars) {
	    fname = vars->components.atom.val.text;
	}
	else {
	    fname = hashsave("??");
	}

	if ((not streq(fname, "??")) and LookupIn(fname, kidtab)) {
	    if (not kidsym->errors)
		kidsym->errors = NewCppList();

	    PutCppList(kidsym->errors, (void*) (errmsg = (char*) malloc(
		strlen(fname) +
		    strlen("Inherited component named %s already defined.\n")
		        + 1)));
	    sprintf(errmsg, "Inherited component named %s already defined.\n", fname);

	    continue;
	}

	EnterInheritedField(kidtab, field->components.decl.kind.field.type,
	    fname, kidtype, kidsym, &prevnode);
    }

}


/*
 * The situation here is that we're inheriting from a parent the type of which
 * is not a tuple.  If the type is not opaque, we'll enter an inherited field
 * for it.
 *
 * NOTE: This seems to be the slickests place to resolve where clause
 * instantiation of components types.  It also happens in the companion.
 * EnterInheritedField). 
 *
 * The following comment is old and appears not to be true anymore.  I.e.,
 * we'll only skip opaque types, which seems to be what we want.
 *
 * OLD COMMENT: Iff the type is a name/type pair type, then we'll make an
 * inherited field for it.  Otherwise, we'll just skip it.  In this way, we do
 * NOT make default entires for inherited components (as we do for regular
 * components in EnterAndField, q.v.).
 */
void EnterNonTupleInheritedField(Symtab* kidtab, TypeStruct type,
	TypeStruct kidtype, SymtabEntry* kidsym, nodep** prevnode) {
    TypeStruct ptype;
    nodep where;

    /*
     * Reinstantiate parent type if there's a relevant where clause item.
     */
    if (where = GetWhereClause(kidsym))
	ptype = InstantiateWhereDef(type, where);
    else
	ptype = type;

    if (not isOpaqueType(type))
	EnterTupleField(kidtab, ptype, true, kidtype, prevnode);
}


/*
 * The situation here is that we're in the midst of an inheritance chain, and
 * we've come to an object that was not originally defined as a tuple.  We've
 * just alloc'd the new symtab, and here we install the original object type as
 * the (presumably) initial field.  As above, we skip entering if the type is
 * opaque.
 *
 * Well, there's another situation as well, namely that of building a full
 * tuple type, in which case we want to proceed even if entering type is
 * opaque.  This is a unfortunate complication, due to the way things have
 * evolved in the logic, but one I can live at this point to get things to
 * work.
 */
void EnterSingleTupleField(Symtab* kidtab, TypeStruct type,
	TypeStruct kidtype, nodep** prevnode, bool full) {
    if ((not isOpaqueType(type)) or full) {
/*	kidtype->components.type.kind.record.fields =
	    InitDeclList(type); */
	EnterTupleField(kidtab, type, false, kidtype, prevnode);
/*	kidtype->components.type.kind.record.fields =
	    FixDeclList(kidtype->components.type.kind.record.fields);*/
    }
}

/*
 * Common work doer for EnterNonTupleInheritedField and EnterSingleTupleField.
 */
void EnterTupleField(Symtab* kidtab, TypeStruct type, bool isinherited,
	TypeStruct kidtype, nodep** prevnode) {
    nodep fname;
    char* fnamestr;
    TypeStruct ftype;
    SymtabEntry* sym;
    nodep newnode;

    /*
     * Determine an appropriate field name.  Name/type pairs without a name get
     * the anonymous name "??".
     */
    if (fname = type->components.type.name)
	fnamestr = fname->components.atom.val.text;
    else
	fnamestr = hashsave("??");

    /*
     * Enter the field in the record fields tab.
     */
    EnterIn(sym = AllocSymtabEntry(fnamestr,
	C_Var, type, kidtab->Level), kidtab);
    sym->Info.Var.Offset = kidtab->Offset;
    kidtab->Offset += TypeSize(type);
    if (isinherited)
	SetSymFlag(sym, isInherited);

    /*
     * Add a field to the field list and bump the field list count.
     */
    /* WAS:
     *
    kidtype->components.type.kind.record.fields =
	AddToDeclList(kidtype->components.type.kind.record.fields,
	    AllocFieldNodeFromType(fnamestr, type));
     */
    newnode = AllocFieldNodeFromType(fnamestr, type);
    newnode->components.decl.kind.field.isinherited = isinherited;
    newnode->components.decl.next = **prevnode;
    **prevnode = newnode;
    *prevnode = &(newnode->components.decl.next);
    kidtype->components.type.kind.record.numfields++;
    kidtype->components.type.size++;
}


/*
 * Return true if the first char of a field name is a '[', indicating it is a
 * constructed default field name (see EnterAndField).
 */
bool IsDefaultName(char* name) {
    return name[0] == '[';
}


/*
 * Enter a field inherited from a parent in the "nice" way (cf.
 * EnterNonTupleInheritedField).
 *
 * NOTE: This seems to be the slickests place to resolve where clause
 * instantiation of components types.  It also happens in the companion.
 * EnterNonTupleInheritedField).
 */
void EnterInheritedField(Symtab* kidtab, nodep ptype, char* pname,
	TypeStruct kidtype, SymtabEntry* kidsym, nodep** prevnode) {
    SymtabEntry* sym;
    nodep where;
    nodep newnode;

    /*
     * Reinstantiate parent type if there's a relevant where clause item.
     */
    if (where = GetWhereClause(kidsym)) {
	ptype = InstantiateWhereDef(ptype, where);
    }

    /*
     * Enter the field in the record fields tab.
     */
    EnterIn(sym = AllocSymtabEntry(pname, C_Var, ptype,
	kidtab->Level+1), kidtab);
    sym->Info.Var.Offset = kidtab->Offset;
    kidtab->Offset += TypeSize(ptype);
    SetSymFlag(sym, isInherited);

    /*
     * Add a field to the field list and bump the field list count.
     *
     * Important 22dec00 update: The 21dec00 update is bogus!  See the
     * discussion in the 4jan01 CVS log entry for details.
     *
     * Important 21dec00 update: Don't add inherited field to the field list.
     * The fact that it's added to the symtab is the operationally important
     * thing for type checking.  We'll leave the field list alone, letting it
     * reflect in the directly-declared components.  This update is motivated
     * by needing an easy way to get at just the directly-declared components
     * in the browser.
     *
     * Also motivated by the browser, we leave in the bumping of the type size
     * counter, since it reflects total size, not just directly-declared size.
     */
    newnode = AllocFieldNodeFromType(pname, ptype);
    newnode->components.decl.kind.field.isinherited = true;
    newnode->components.decl.next = **prevnode;
    **prevnode = newnode;
    *prevnode = &(newnode->components.decl.next);
    kidtype->components.type.kind.record.numfields++;
    kidtype->components.type.size++;
}


/*
 * Do the nasty deed of where clause processing.  Again, see the ref man for
 * explantory details of what this processing entails.
 */
void ProcessObjWhereClause(nodep t, SymtabEntry* sym)
{
    nodep where;

    /*
     * Outta here if no where clause.
     */	
    if (not (where = FindAttr(t->components.decl.kind.obj.attrs, YWHERE)))
	return;

    /*
     * Disconnect parents to disable subtype polymorphism.
     *
     * NOT ANY MORE.
     *
    sym->Info.Obj.inheritsfrom = null;
     */

    /*
     * Real instantiation work is done incrementally for each where-clause
     * field, using InstantiateWhereDef.
     */
}

void ProcessOpWhereClause(nodep t, SymtabEntry* sym)
{
    /*
     * Disconnect parents to disable subtype polymorphism.
     */
/*    sym->Info.Op.inheritsfrom = null;	*/

    /* TODO */

}


/*
 *
 * IMPORTANT NOTE: We should probably nix the *anywhere* stuff below, because
 * it could lead to a multiple pass requirement, in that auto-gen'd ops would
 * need to be rechecked for more autogen'ing.  Need to think about this
 * seriously. 
 *
 * Resolve operation inheritance as follows (this level of detailed expl should
 * be in the ref man, but it's not currently):
 *
 *     (1) Chk ops attr.
 *     (2) If none, leave.
 *     (3) If one or more with no sigs (i.e., names only), then gen new
 *	   inherited ops for *all* non-imported ops with parent type
 *	   *anywhere* in the signature.
 *     (4) If one or more with explicit sigs, then gen new inherited ops for
 *	   each such op.
 */
ResolveOpInObjInheritance(nodep t, SymtabEntry* sym) {

    /* TODO */

}

ResolveEqnInheritance(nodep t, SymtabEntry* sym) {

    /* TODO */

}

/*
 * Return a sym lit type as the spelling of it's name.  This type is only
 * compatible with a declared opaque type of the same name.  While the sym lit
 * value can exist in a decl without its corresponding opaque type having been
 * created, a sym lit value cannot be bound to a variable without the opaque
 * type having been declared, since the variable could not have been declared
 * without the opaque type decl.
 */
TypeStruct BuildSymLitType(nodep t) {
    TypeStruct rtn = NewNode(TYPE_NODE, '\'', t->header.loc);
    rtn->components.type.kind.symlit = t->components.atom.val.symlit;
}

/*
 * Push/Pop functions used to push entering tree value, so circularity of value
 * checking can be detected.  Use the same stack size as sym.h uses.
 */
bool InTreeStack(nodep t) {
    nodep* sp;
    for (sp = treetos; sp > TreeStack; ) {
	if (*(--sp) == t) {
	    return true;
	}
    }
    return false;
}