/*
 * Primordial .hP file for the type checker.  It'll be upgraded as appropriate
 * with the rewrite.  For now, it contains signatures for private functions, so
 * these need not crud up type.h, nor, thereby, cause massive remakes, given
 * that many include type.h.
 */

#ifndef typechkPIncluded
#define typechkPIncluded

#include "std-macros.h"

bool chkModule1_5(
    nodep t,
    int Offset);

bool chkModule2(
    nodep t,
    int Offset);
void chkSpecBody2(
    nodep t,
    int Offset);

void exportAllFromMain();

void chkImports1(
    nodep t);

void chkImportItem(nodep item, nodep import);
void chkImportName(SymtabEntry* sym, nodep error_nodep);

bool initModule(nodep t);
void initSpecBody(nodep t);
void initVal(nodep t, SymtabEntry* sym);

TypeStruct chkExprSeq(nodep t, bool f);
TypeStruct chkPlusOp(nodep t, bool f);
TypeStruct AddToAnonUnionBasetype(TypeStruct base, TypeStruct elem);
TypeStruct chkMinusOp(nodep t, bool f);
TypeStruct chkMultOp(nodep t, bool f);

TypeStruct chkProcDesig(nodep t, SymtabEntry** sym);
TypeStruct chkBindingsNameCall(SymtabEntry* p, nodep desig, nodep t,
    TypeStruct tt, bool out);
TypeStruct chkBindingsDesigCall(SymtabEntry* p, nodep desig, nodep t, bool out);
bool chkBindings(SymtabEntry* p, nodep desig, nodep t, bool out);
bool chkBindingsSingleListArity(SymtabEntry* p, nodep desig, nodep t, bool out);
bool isSingleListArity(SymtabEntry* p, nodep desig);
void FreeTypeIfNecessary(TypeStruct t);
void chkOverloadedSigs(SymtabEntry* p);
TypeStruct LowestSignature(List* l, TypeStruct tt);

TypeStruct chkLambda(nodep t, bool f);

bool chkPrePostcondDecl(
    nodep t,
    char* errstr);

TypeStruct BuildEmptyLeftField(
    nodep t,
    int *n,
    struct Symt** st);

bool isModuleIdent(SymtabEntry* sym);

TypeStruct ResolveIdentType(
    TypeStruct t,	/* Any type struct */
    nodep errlocnode,	/* Node for error message location */
    bool doerror);	/* True if error message should be issued */

TypeStruct ResolveToBaseIdentType(
    TypeStruct t,	/* Any type struct */
    nodep errlocnode,	/* Node for error message location */
    bool doerror);	/* True if error message should be issued */

TypeStruct ResolveIdentTypeAsOneTuple(
    TypeStruct t,	/* Any type struct */
    nodep errlocnode,	/* Node for error message location */
    bool doerror);	/* True if error message should be issued */

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. */

TypeStruct ChkForImportedType(char* name);

TypeStruct NewDerivedIdentType(TypeStruct t, char* origname, char* rname);

TypeStruct chkModuleRef(nodep t);

TypeStruct chkModuleRefs(nodep t);

TypeStruct chkRecordOrUnionRef(
    nodep t,
    bool f,
    TypeStruct l,
    TypeStruct desig,	/* Result of recursive type chk of left operand. */
    char* errmsg1,
    char* errmsg2);

TypeStruct chkUnionRef(
    nodep t,
    bool f);

TypeStruct chkDotDotOp(nodep t, bool f);
TypeStruct chkListConstructor(nodep t, bool f);
void addToInferredBase(List* ibase, TypeStruct t);
TypeStruct chkTupleConstructor(nodep t, bool f);
TypeStruct BuildFullTupleType(List* l);

TypeStruct chkArraySliceRef(TypeStruct t, bool f);

bool equiv(
    TypeStruct t1, TypeStruct t2);

TypeStruct chkQuant(
    nodep t,
    bool f);

bool chkQuantInClause(nodep var, nodep inexpr, bool f);
bool chkQuantSuchthatClause(nodep vars, nodep suchthatexpr, bool f);

TypeStruct chkLet(nodep t, bool f);
TypeStruct chkGetInstance(nodep t, bool f);
TypeStruct chkChkInstance(nodep t, bool f);
TypeStruct chkRetract(nodep t, bool f);
TypeStruct chkAttrSelect(nodep t, bool f);
TypeStruct chkBeginBlock(nodep t, bool f);
TypeStruct figureAttrType(nodep attr);

TypeStruct GetNextEquivIdentType(
    TypeStruct it);	/* An ident type struct */

bool SameIdentType(
    TypeStruct t1, TypeStruct t2);	/* Two ident types */

void chkAxOrThm(nodep expr, char* msgstr);

void chkFormalVarDecl(nodep vardecl);

void chkOpOverloading(SymtabEntry* sym);

void chkOpParms(
    SymtabEntry* parmlist);	/* An op parmlist thread */

TypeStruct chkLenOp(nodep t, bool f);
TypeStruct BuildOp(nodep p);

bool identCompat(TypeStruct t1, TypeStruct t2);
bool subtypeCompat(TypeStruct t1, TypeStruct t2);
bool subtypeCompat1(char* parentname, char* childname);
bool isOrWasIdentType(TypeStruct t);
bool structCompat(TypeStruct t1, TypeStruct t2);
bool chkEqLitValues(TypeStruct t1, TypeStruct t2);
bool orCompat(TypeStruct t1, TypeStruct t2);
bool orCompat1(TypeStruct t1, TypeStruct t2);
bool onetupleCompat(TypeStruct t1, TypeStruct t2);
void ResolveObjInheritance(nodep t, SymtabEntry* sym);
bool StringEquals(void* s1, void* s2);
void ResolveOpInheritance(nodep t, SymtabEntry* sym);
bool isNonIdentIdentType(TypeStruct t);
TypeStruct BuildNewTupleType(TypeStruct type);
TypeStruct BuildNewTupleTypeSized(TypeStruct type, int size, bool full);
void SnatchParentFields(SymtabEntry* psym, SymtabEntry* kidtype);
void EnterNonTupleInheritedField(Symtab* kidtab, TypeStruct type,
    TypeStruct kidtype, SymtabEntry* kidsym, nodep** prevnode);
void EnterSingleTupleField(Symtab* kidtab, TypeStruct type,
    TypeStruct kidtype, nodep** prevnode, bool full);
void EnterTupleField(Symtab* kidtab, TypeStruct type, bool isinherited,
    TypeStruct kidtype, nodep** prevnode);
bool IsDefaultName(char* name);
void EnterInheritedField(Symtab* kidtab, nodep ptype, char* pname,
    TypeStruct kidtype, SymtabEntry* kidsym, nodep** prevnode);
void ProcessObjWhereClause(nodep t, SymtabEntry* sym);
void ProcessOpWhereClause(nodep t, SymtabEntry* sym);
void chkValExprDecl(nodep t, SymtabEntry* sym);

bool isValSym(SymtabEntry* sym);

bool isConstAtom(nodep t);

#define isAnonScope(st) (st->Type == '(')

TypeStruct BuildSymLitType(nodep t);
bool symlitCompat(TypeStruct t1, TypeStruct t2);
bool litCompat(TypeStruct base, TypeStruct lit);
bool litCompat2(TypeStruct base, TypeStruct lit);
bool litBaseCompat(TypeStruct base, TypeStruct lit);
bool litBaseCompat2(TypeStruct t1, TypeStruct t2);

nodep TreeStack[STKINC];
nodep* treetos;
int TreeStackSize;

#define PushTree(t) \
	if (++TreeStackSize == STKINC) \
	    AllocTreeStack(); \
	*(treetos++) = t
#define PopTree() \
	if (treetos == TreeStack) error("Fatal type checking error.\n"); \
	treetos--; \
	TreeStackSize--
#define TopTree() \
	*(treetos-1)
#define ClearTreeStack() \
	treetos = TreeStack
#define AllocTreeStack() \
    error("Fatal type checking error.")

bool InTreeStack(nodep t);

TypeStruct BuildRef(nodep t);
bool isRef(nodep t);

#endif