/*********************************************************************************
 *
 *  Typechecking OQL algebraic forms (monoid comprehensions)
 *  (It's basically a type inference algorithm with a restricted form
 *  of bounded polymorphism to handle the monoid hierarchy)
 *
 *  Copyright (c) 1999-2003 by Leonidas Fegaras, the University of Texas at
 *     Arlington. All rights reserved.
 *  Programmer: Leonidas Fegaras
 *  Date: 10/10/98
 *
 ********************************************************************************/

#include "odl.h"
#include "constant.h"


/* set it to true to trace the typechecker */
const bool TRACE_TYPECHECK = false;


extern bool interpreterp;

/* return the variables of a pattern */
list<Expr>* pattern_variables ( Expr pattern );

/* defined in translate.gen */
Expr translate ( Expr e );

/* if e is a path, return the beginning of the path */
Expr project_variable ( Expr e );

typedef binding<Expr>* Schema;

Schema global_lvars = new binding<Expr>;

/* catching type exceptions */
#define DEBUG(exp) catch (odmg_error_class(m))		\
 { eout << "*** Found in " << exp << '\n';	\
   throw odmg_error_class(eout.str()); }

/* a type error is a fatal error: it causes the program to abort */
void fatal_type_error ( string msg, list<Expr>* errors ) {
  eout << "*** Type Error: " << msg << "  " << errors << "\n";
  throw odmg_error_class(eout.str());
};

void type_error ( string msg, Expr e ) {
  fatal_type_error(msg,Cons(e,Nil));
};

void type_error ( string msg, Expr e1, Expr e2 ) {
  fatal_type_error(msg,Cons(e1,Cons(e2,Nil)));
};

void type_error ( string msg, Expr e1, Expr e2, Expr e3 ) {
  fatal_type_error(msg,Cons(e1,Cons(e2,Cons(e3,Nil))));
};


/* returns a new type variable that hasn't been used before; it starts as
 * commutative-idempotent (equivalent to a set) but later (during unification) may be refined */
Expr fresh_type_variable () {
  return #<ALPHA(`(new_variable()),set)>;
};


/* this is a stack of environments to store transient variable
 * assignments in OQL of the form v := e			*/
static list<binding<pair<int,Expr>*>*>* scoped_variables = (new list<binding<pair<int,Expr>*>*>)->cons(new binding<pair<int,Expr>*>);

static int scoped_variable_number = -1;


int last_scoped_var () {
  return scoped_variable_number;
};


int set_scope ( int n ) {
  scoped_variable_number = n;
  return n;
};


Expr find_scoped_variable ( String s ) {
  for(list<binding<pair<int,Expr>*>*>* r = scoped_variables; r->consp(); r=r->tl)
     if (r->hd->in(s))
	return r->hd->find(s)->second;
  return #<none>;
};


void put_in_current_scope ( String name, Expr type ) {
  if (scoped_variables->hd->in(name))
     type_error("variable already defined in current scope",variable(name));
  scoped_variable_number++;
  scoped_variables->hd = scoped_variables->hd->extend(name,Pair(scoped_variable_number,type));
};


void new_scope () {
  scoped_variables = Cons(new binding<pair<int,Expr>*>,scoped_variables);
};


void close_scope () {
  if (scoped_variables->nullp())
     type_error("trying to pop the last environment",#<none>);
  if (false)
     scoped_variable_number -= scoped_variables->hd->length();
  scoped_variables = scoped_variables->tl;
};


int scoped_variable_location ( String s ) {
  for(list<binding<pair<int,Expr>*>*>* r = scoped_variables; r->consp(); r=r->tl)
     for(Names nms = r->hd->names(); nms->consp(); nms=nms->tl)
	if (nms->hd->eq(s))
	   return r->hd->find(s)->first;
  return -1;
};


static list<Expr>* commutative_monoids
	= Nil->cons(#<set>)->cons(#<bag>)->cons(#<sum>)->cons(#<avg>)->cons(#<max>)->cons(#<min>)->cons(#<some>)->cons(#<all>);

static list<Expr>* idempotent_monoids
	= Nil->cons(#<set>)->cons(#<max>)->cons(#<min>)->cons(#<avg>)->cons(#<some>)->cons(#<all>);

static list<Expr>* collection_monoids
	= Nil->cons(#<set>)->cons(#<bag>)->cons(#<list>);

// is x a commutative monoid?
bool commutative ( Expr x ) { 
  return member(x,commutative_monoids);
};

// is x an idempotent monoid?
bool idempotent ( Expr x ) {
  return member(x,idempotent_monoids);
};

// is f a collection monoid?
bool collectionp ( Expr x ) {
  #case x
  | ordered(...r)
	=> return true;
  | _ => return member(x,collection_monoids);
  #end;
};


bool collection_typep ( Expr x ) {
  #case x
  | `f(...r) => return collectionp(f);
  | _ => return false;
  #end;
};


bool is_class ( Expr type ) {
  #case type
  | void(`tp) => return is_class(tp);
  | scope(`tp) => return is_class(tp);
  | _ => return type->variablep() && classp(type->name());
  #end;
};


/* type variable instantiations */
bool substitute ( Expr var, Expr y, Schema &lvars ) {
  Schema s = new binding<Expr>;
  for(Names ns = lvars->names(); ns->consp(); ns=ns->tl)
     s = s->extend(ns->hd,subst_expr(var,y,lvars->find(ns->hd)));
  lvars = s->extend(var->name(),y);					/* destructive */
  return true;
};


/* convert a structure into a binding from the structure attributes to their types */
Schema type_to_schema ( Expr tp ) {
  Schema res = new binding<Expr>;
  #case tp
  | struct(...args)
      => for(list<Expr>* r = args->reverse(); r->consp(); r=r->tl)
	    #case r->hd
	    | bind(`x,`t) => res = res->extend(x->name(),t);
	    #end;
  | _ => type_error("(in type_to_schema) Expected a record type",tp);
  #end;
  return res;
};


/* is the collection monoid x stronger than y? */
bool stronger_monoid ( Expr x, Expr y) {
  #case x
  | list => return true;
  | bag => return y->eq(#<list>);
  | _ => return false;
  #end;
};


/* type compatibility (weaker than type equality) */
bool compatible ( Expr x, Expr y ) {
  #case x
  | ALPHA(`v,`m)
	=> #case y
	   | `f(`tp) => if (f->eq(m))
			   return true;
			else if (stronger_monoid(f,m))
			{  x->arguments()->tl->hd = f;		/* destructive */
			   return true;
			} else return true;
	   | `f : (f->eq(#<list>) || f->eq(#<bag>) || f->eq(#<set>))
	       => if (f->eq(m))
		      return true;
		   else if (stronger_monoid(f,m))
			{  x->arguments()->tl->hd = f;		/* destructive */
			   return true;
			} else return true;
	   | _ => return true;
	   #end;
  | _ => return true;
  #end;
};


Expr equivalent_type ( Expr x ) {
  #case x
  | long => return #<integer>;
  | short => return #<integer>;
  | unsigned_long => return #<integer>;
  | unsigned_short => return #<integer>;
  | float => return #<float>;
  | double => return #<float>;
  | octet => return #<integer>;
  | char => return #<string>;
  | _ => return x;
  #end;
};


/* if type is an instantiated type variable, return its binding */
Expr instantiate_type ( Expr type, Schema lvars) {
  #case type
  |  ALPHA(`vx,_)
	=> if (lvars->in(vx->name()))
	      return instantiate_type(lvars->find(vx->name()),lvars);
	   else return type;
  | _ => return type;
  #end;
};


Expr get_scoped_type ( Expr type ) {
  #case type
  | scope(`w) : w->variablep()
	=> #case get_declaration_binding(w->name())
	   | none => type_error("Illegal type name",w);
	   | typedef(`tp,_) => return tp;
	   | union(...r)  => return #<union(...r)>;
	   | struct(...r)  => return #<struct(...r)>;
	   | _ => return w;
	   #end;
  | `w : w->variablep()
	=> #case get_declaration_binding(w->name())
	   | none => return w;
	   | typedef(`tp,_) => return tp;
	   | union(...r)  => return #<union(...r)>;
	   | struct(...r)  => return #<struct(...r)>;
	   | _ => return w;
	   #end;
  | _ => return type;
  #end;
};


/* if subtype=false, it is type unification; otherwise, it is both type unification and x subtype of y */
bool unify ( Expr e, Expr x, Expr y, Schema &lvars, bool subtype = false ) {
  if (x->eq(y) || x->eq(#<any>) || y->eq(#<any>))
     return true;
  #case x	/* if x is a bound type variable, retrieve its type */
  | ALPHA(`vx,_)
	=> if (lvars->in(vx->name()))
	      x = lvars->find(vx->name());
  | enum(`nm,...r) => return unify(e,nm,y,lvars,subtype);
  | scope(`w) : w->variablep()
	=> if (w->eq(y)) return true;
	   else x = get_scoped_type(x);
  | void(`tp) => return unify(e,tp,y,lvars,subtype);
  #end;
  #case y	/* if y is a bound type variable, retrieve its type */
  | ALPHA(`vy,_)
	=> if (lvars->in(vy->name()))
 	      y = lvars->find(vy->name());
  | enum(`nm,...r) => return unify(e,x,nm,lvars,subtype);
  | scope(`w) : w->variablep()
	=> if (x->eq(w)) return true;
	   else y = get_scoped_type(y);
  | void(`tp) => return unify(e,x,tp,lvars,subtype);
  #end;
  #case x
  |  ALPHA(`vx,`m)
	=> #case y
	   |  ALPHA(`vy,`n)
		=> if (compatible(y,x))
		      return substitute(vx,vy,lvars);
		   else return false;
	   |  _ => if (compatible(x,y))
		      return substitute(vx,y,lvars);
		   else return false;
	   #end;
  |  _ => #case y
	  |  ALPHA(`vy,`m)
		 => if (compatible(y,x))
		       return substitute(vy,x,lvars);
		    else return false;
          #end;
  #end;
  if (x->variablep() && y->variablep())
     if (subtype && subclass(x->name(),y->name()))
	return true;
  #case x
  |  struct(`name,...r) : name->variablep() => x = #<struct(...r)>;
  #end;
  #case y
  |  struct(`name,...r) : name->variablep() => y = #<struct(...r)>;
  #end;
  #case x
  |  struct(...r)
	=> #case y
	   |  struct(...s)
		 =>  {  bool b = subtype || (r->length() == s->length());
			Schema sch = type_to_schema(y);
		        for(; r->consp() && b; r=r->tl)
			   #case r->hd
			   |  bind(`v,`tp)
				=> if (sch->in(v->name()))
				      b = b && unify(e,tp,sch->find(v->name()),lvars,subtype);
				   else return false;
			   #end;
			return b;
		     };
	   #end;
  | ordered(`m)
	=> #case y
	   | ordered(`n) => return true;
	   | _ => return false;
	   #end;
  | `f(...r)
	=> #case y
	   |  `g(...s)
		  => {  bool b = unify(e,f,g,lvars,subtype);
		        for(; b && r->consp() && s->consp(); r=r->tl, s=s->tl)
			   b = b && unify(e,r->hd,s->hd,lvars,subtype);
			return b && s->nullp() && r->nullp();
		     };
	   #end;
  |  _  => if (y->variablep())
	      return equivalent_type(x)->eq(equivalent_type(y));
  #end;
  return false;
};


/* bind the variables of a pattern to a list of arguments */
Schema bind_pattern ( Expr pat, list<Expr>* args ) {
  Schema res = new binding<Expr>;
  list<Expr>* pvars = pattern_variables(pat);
  for(list<Expr>* r = args; r->consp(); r=r->tl)
     #case r->hd
     | bind(`v,`tp)
	=> if (pvars->consp() && (v->eq(pvars->hd) || v->eq(variable("_"))))
	   { res = res->extend(pvars->hd->name(),tp);
	     pvars=pvars->tl;
	   }
	   else res = res->extend(v->name(),tp);
	
     #end;
  return res;
};


/* find an internal method for method_name that matches the type signature
*  method_types (defined in constant.h) */
pair<Expr,int>* find_internal_method
	( String method_name, list<Expr>* method_types, Schema &lvars ) {
  for(list<pair<String,method_info*>*>* r = internal_methods->env; r->consp(); r=r->tl)
     if (r->hd->first->eq(method_name))
     {  list<Expr>* ts = method_types;
	list<Expr>* s = r->hd->second->parameters->tl;
	for(; s->consp() && ts->consp(); s=s->tl, ts=ts->tl)
	   if (!unify(ts->hd,ts->hd,s->hd,lvars))
	      break;
	if (s->consp() || ts->consp())
	   continue;
	return new pair<Expr,int>(r->hd->second->parameters->hd,r->hd->second->location);
     };
   return new pair<Expr,int>(#<none>,-1);
};


/* the types of the group-by expressions */
typedef list<pair<Expr,Expr>*>* GEnv;


/* defined below */
Expr typecheck ( Expr e, Schema &cvars, Schema &lvars, GEnv &gvars );
Expr eliminate_type_vars ( Expr x, Schema lvars, bool first_time, bool type_varsp );


list<Expr>* typecheck_nest_vars ( Expr e, Schema &cvars, Schema &lvars, GEnv &gvars ) {
  #case e
  | pair(`x,`y)
	=> return typecheck_nest_vars(x,cvars,lvars,gvars)->append(typecheck_nest_vars(y,cvars,lvars,gvars));
  | _ => {  Expr tp = typecheck(e,cvars,lvars,gvars);
	    gvars = gvars->cons(new pair<Expr,Expr>(e,tp));
	    if (e->variablep())
	       return Nil->cons(#<bind(`e,`tp)>);
	    else return Nil->cons(#<bind(`(new_variable()),`tp)>);
	 };
  #end;
};


Expr make_void_type ( Expr type ) {
  return #<void(`type)>;
};


int typecheck_counter = 1;


/* checks an expression for type errors */
Expr typecheck ( Expr e, Schema &cvars, Schema &lvars, GEnv &gvars ) {
try{
  if (TRACE_TYPECHECK)
     cout << typecheck_counter++ << ") ** " << e << "   " << cvars << endl;
  Expr retp;		/* the returned type */
  for(GEnv r = gvars; r->consp(); r=r->tl)
     if (r->hd->first->eq(e))	/* if e is a group-by expression */
	return r->hd->second;
  #case e
  | `op(`M,`tp)
	: op->eq(#<zero>) || op->eq(#<ZERO>)
	=> retp = #<`M(`tp)>;
  | `op(`M)
	: op->eq(#<zero>) || op->eq(#<ZERO>)
	=> { Expr lv = fresh_type_variable();
	     e->set_type(#<MODIFY(`op(`M,`lv))>);
	     if (collectionp(M) && interpreterp)
		retp = #<`M(`(make_void_type(lv)))>;
	     else retp = #<`M(`lv)>;
	   };
  | `op(`M,`e)
	: op->eq(#<unit>) || op->eq(#<UNIT>)
	=> { Expr tp = typecheck(e,cvars,lvars,gvars);
	     if (collectionp(M) && interpreterp)
		tp = make_void_type(tp);
	     retp = #<`M(`tp)>;
	   };
  | `op(`M,`x,`y)
	: op->eq(#<merge>) || op->eq(#<MERGE>)
	=> { Expr xtp = typecheck(x,cvars,lvars,gvars);
	     Expr ytp = typecheck(y,cvars,lvars,gvars);
	     if (unify(e,xtp,ytp,lvars,true))
		retp = ytp;
	     else if (unify(e,ytp,xtp,lvars,true))
		retp = xtp;
	     else type_error("Incompatible merge inputs",xtp,ytp);
	     #case retp
	     | `f(_) => e->set_type(#<MODIFY(`op(`f,`x,`y))>);
	     #end;
	   };
  | compr(`M,`head,...qualifiers)
	=> { Schema s = cvars;
	     for(list<Expr>* r = qualifiers; r->consp(); r=r->tl)
	        #case r->hd
	        | iterate(`v,`u)
		    => #case instantiate_type(typecheck(u,s,lvars,gvars),lvars)
		       | `N(void(`tp))
			     => s = s->extend(v->name(),tp);
		       | `N(`tp)
			     => s = s->extend(v->name(),tp);
		       | `tp => type_error("Expected a collection in the comprehension generator",u,tp);
		       #end;
	        | bind(`v,`u)
		    => s = s->extend(v->name(),typecheck(u,s,lvars,gvars));
	        | `u => { Expr tp = typecheck(u,s,lvars,gvars);
		          if (!(unify(e,tp,#<boolean>,lvars)))
			     type_error("Expected a boolean predicate",u,tp);
		        };
	        #end;
	     Expr tp = typecheck(head,s,lvars,gvars);
	     if (M->eq(#<all>) || M->eq(#<some>))
		if (unify(e,tp,#<boolean>,lvars))
		   retp = #<boolean>;
		else type_error("Expected a boolean predicate in quantification",e,tp);
	     else if (M->eq(#<sum>) || M->eq(#<prod>) || M->eq(#<max>) || M->eq(#<min>))
		if (unify(e,tp,#<integer>,lvars))
		   retp = #<integer>;
		else if (unify(e,tp,#<float>,lvars))
		   retp = #<float>;
		else type_error("Expected a numeric value in aggregation",e,tp);
	     else if (M->eq(#<concat>))
		if (unify(e,tp,#<string>,lvars))
		   retp = #<string>;
		else type_error("Expected a string value in aggregation",e,tp);
	     else #case M
		  | ordered(...r)
			=> {  for(; r->consp(); r=r->tl)
				 #case r->hd
				 | desc(`e) => typecheck(e,s,lvars,gvars);
				 | `e => typecheck(e,s,lvars,gvars);
				 #end;
			      retp = (interpreterp) ? #<list(`(make_void_type(tp)))> : #<list(`tp)>;
			   };
		  | _ => retp = (interpreterp) ? #<`M(`(make_void_type(tp)))> : #<`M(`tp)>;
		  #end;
	   };
  | project(`x,`a,`tp,...r)
	=> retp = tp;
  | project(`x,`a)
      => { Expr tp = get_scoped_type(typecheck(x,cvars,lvars,gvars));
	   #case tp
	   | void(`etp)
		=> tp = etp;
	   #end;
	   String cn;
	   #case tp
	   | XML_element
		: !a->eq(#<xml_element>) && !a->eq(#<tag>)
		=> {  Expr s = estring(a->name());
		      Expr ne;
		      if (a->eq(#<ANY>))
			 ne = #<call(any_projection,unit(list,`x))>;
		      else if (a->eq(#<STAR>))
			 ne = #<call(wildcard_projection,unit(list,`x))>;
		      else ne = #<call(tag_projection,unit(list,`x),`s)>;
		      typecheck(ne,cvars,lvars,gvars);
		      ne = eliminate_type_vars(ne,lvars,true,true);
		      e->set_type(#<MODIFY(`ne)>);
		      retp = #<list(`tp)>;
		   };
	   | list(XML_element)
		: !a->eq(#<xml_element>) && !a->eq(#<tag>)
		=> {  Expr s = estring(a->name());
		      Expr ne;
		      if (a->eq(#<ANY>))
			 ne = #<call(any_projection,`x)>;
		      else if (a->eq(#<STAR>))
			 ne = #<call(wildcard_projection,`x)>;
		      else ne = #<call(tag_projection,`x,`s)>;
		      typecheck(ne,cvars,lvars,gvars);
		      ne = eliminate_type_vars(ne,lvars,true,true);
		      e->set_type(#<MODIFY(`ne)>);
		      retp = tp;
		   };
	   | list(scope(XML_element))
		: !a->eq(#<xml_element>) && !a->eq(#<tag>)
		=> {  Expr s = estring(a->name());
		      Expr ne;
		      if (a->eq(#<ANY>))
			 ne = #<call(any_projection,`x)>;
		      else if (a->eq(#<STAR>))
			 ne = #<call(wildcard_projection,`x)>;
		      else ne = #<call(tag_projection,`x,`s)>;
		      typecheck(ne,cvars,lvars,gvars);
		      ne = eliminate_type_vars(ne,lvars,true,true);
		      e->set_type(#<MODIFY(`ne)>);
		      retp = tp;
		   };
	   | `v : (v->variablep() && classp(v->name()))
	      => { #case find_attribute_type(a->name(),v->name(),cn)
		   | none => type_error("Class does not have the attribute",v,a);
		   | scope(`w) : w->variablep()
			=> if (classp(w->name()))
			      retp = w;
			   else retp = get_scoped_type(#<scope(`w)>);
		   | `atp => retp = atp;
		   #end;
		   e->set_type(#<MODIFY(project(`x,`a,`retp))>);
	        };
	   | struct(...r)
		=> { bool found = false;
		     for(list<Expr>* s = r; !found && s->consp(); s=s->tl)
			#case s->hd
			|  bind(`v,scope(`ptp))
				: v->eq(a)
				=> { found = true; retp = ptp; };
			|  bind(`v,`ptp)
				: v->eq(a)
				=> { found = true; retp = ptp; };
			#end;
		     if (!found)
			type_error("Structure does not have the projection attribute",a,tp);
		     e->set_type(#<MODIFY(project(`x,`a,`retp))>);
		   };
	   | union(`nm,`etp,...cs)
		=> { bool found = false;
		     for(list<Expr>* r=cs; !found && r->consp(); r=r->tl)
			#case r->hd
			| case(`tp,`dcl,...cs)
				: dcl->eq(a)
				=> { found = true; retp = tp; };
			#end;
		     if (!found)
			type_error("Union type does not have the attribute",a,tp);
		     e->set_type(#<MODIFY(project(`x,`a,`retp))>);
		   };
	   | _ => type_error("Expected a structure in projection",tp);
	   #end;
	 };
  | struct(...r)
	=> { list<Expr>* s = Nil;
	     list<Expr>* attrs = Nil;
	     for(; r->consp(); r=r->tl)
	        #case r->hd
	        |  bind(`v,`u)
			=> {  s = s->cons(#<bind(`v,`(typecheck(u,cvars,lvars,gvars)))>);
			      if (member(v,attrs))
				 type_error("duplicate attribute name",v);
			      attrs = attrs->cons(v);
			    };
		#end;
	      s = s->reverse();
	      retp = #<struct(...s)>;
	    };
  | lambda(`otype,...binds,`value)
	=> { Schema new_vars = cvars;
	     for(list<Expr>* r = binds; r->consp(); r=r->tl)
		#case r->hd
		| bind(`v,`tp)
			=> new_vars = new_vars->extend(v->name(),tp);
		| _ => type_error("Ill-formed lambda abstraction",r->hd);
		#end;
		if (!unify(e,typecheck(value,new_vars,lvars,gvars),otype,lvars))
		   type_error("The body of the lambda abstraction does not have the expected type",otype);
		return otype;
	   };
  | method(`o,`name,...args)
	 => { Expr class_type = typecheck(o,cvars,lvars,gvars);
	      #case class_type
	      | void(`v) => class_type = v;
	      #end;
	      if (!is_class(class_type))
		 type_error("Methods can only apply to class instances",class_type);
	      #case get_declaration_binding(name->name(),class_type->name())
	      | none => type_error("There is no method with that name",name);
	      | method(`type,`tname,params(...r),`x,`y)
		=> {  for(; r->consp() && args->consp(); r=r->tl, args=args->tl)
			 #case r->hd
			 | `f(`tp,`m)
				=> if (!unify(args->hd,typecheck(args->hd,cvars,lvars,gvars),tp,lvars))
				      type_error("Method parameter does not have the expected type",
						 args->hd,tp);
			 #end;
		      if (r->consp() || args->consp())
			 type_error("Illegal number of arguments in method call",e);
		      retp = type;
		   };
	      | _ => type_error("This name is not a method in class",name,class_type);
	      #end;
	    };
  | coerce(`tp,`x)
	 => {  Expr etp = typecheck(x,cvars,lvars,gvars);
	       if (unify(e,variable(tp->name()),etp,lvars,true))
	          retp = variable(tp->name());
	       else type_error("Can't coerce types",tp,etp);
	    };
  | assign(bind(`v,`e),`u)
	=> { cvars = cvars->extend(v->name(),typecheck(e,cvars,lvars,gvars));
	     retp = typecheck(u,cvars,lvars,gvars);
	   };
  | `f(`dest,`source)
	: (f->eq(#<assign>) || f->eq(#<update>))
	=> {  retp = typecheck(source,cvars,lvars,gvars);
	      if (!unify(dest,typecheck(dest,cvars,lvars,gvars),retp,lvars))
		 type_error("Incompatible types",e);
	   };
  | `f(`dest,`source)
	: (f->eq(#<insert>) || f->eq(#<delete>))
	=> #case typecheck(dest,cvars,lvars,gvars)
	   | `f(`etp) : collectionp(f)
		=> if (!unify(source,typecheck(source,cvars,lvars,gvars),etp,lvars))
		      type_error("Incompatible types in insertion/deletion",e);
		   else return #<none>;
	   | _ => type_error("insertion/deletion can only be done on a collection",e);
	   #end;
  | vector_range(`x,`n,`m)
	=> type_error("Vector range v[n:m] has not been implemented yet",e);
  | vector_access(`x,`n)
	=> {  Expr tp = typecheck(x,cvars,lvars,gvars);
	      Expr ltp = fresh_type_variable();
	      if (unify(x,tp,#<list(`ltp)>,lvars))
		 if (unify(n,typecheck(n,cvars,lvars,gvars),#<integer>,lvars))
		    retp = ltp;
		 else type_error("Expected an integer index",n,typecheck(n,cvars,lvars,gvars));
	      else type_error("Vector access can only be applied to a list",x,tp);
	   };
  | if(`pred,`x,`y)
	 => { Expr tp = typecheck(pred,cvars,lvars,gvars);
	      if (!unify(pred,tp,#<boolean>,lvars))
		 type_error("Predicate in if-then-else is not a boolean",tp);
	      Expr tx = typecheck(x,cvars,lvars,gvars);
	      Expr ty = typecheck(y,cvars,lvars,gvars);
	      if (!unify(e,tx,ty,lvars))
		 type_error("Incompatible types in if-then-else",tx,ty);
	      retp = tx;
	    };
  | cases(`x,...cs)
	=> { list<Expr>* utags;
	     #case get_scoped_type(typecheck(x,cvars,lvars,gvars))
	     | union(_,`tp,...r) => utags = get_union_tags(tp);
	     | `tp => type_error("expected a union type for the case statement",e,tp);
	     #end;
	     list<Expr>* ts = Nil;
	     retp = fresh_type_variable();
	     for(list<Expr>* r = cs; r->consp(); r=r->tl)
		#case r->hd
		| case(`action,...tags)
		      => { Expr atp = typecheck(action,cvars,lvars,gvars);
			   if (!unify(action,retp,atp,lvars))
			      type_error("Incompatible types in the case statement",e);
			   retp = atp;
			   for(; tags->consp(); tags=tags->tl)
			   {  Expr tag = tags->hd;
			      #case tag
			      | scope(`v) => tag = v;
			      #end;
			      if (utags->nullp() && !tag->eq(#<default>) && !tag->integerp())
				 type_error("expected an integer case tag",tag);
			      else if (utags->consp() && !tag->eq(#<default>) && !member(tag,utags))
				 type_error("invalid case tag",tag);
			      else if (member(tag,ts))
				 type_error("duplicate union case tag",tag);
			      else ts = ts->cons(tag);
			   };
			 };
		#end;
	   };
  | xml_tag(`tag,attributes(...as),...cs)
	=> { if (interpreterp)
	        type_error("XML constructions during interpretation are not supported yet",e);
	     Expr ec = #<zero(list)>;
	     Expr nv = new_variable();
	     for(list<Expr>* r=cs; r->consp(); r=r->tl)
	     {  Expr tp = typecheck(r->hd,cvars,lvars,gvars);
		#case tp
		| string => ec = #<merge(list,`ec,unit(list,construct(XML_element,bind(xml_element,construct(element_type,bind(PCDATA,`(r->hd)))))))>;
		| list(string) => ec = #<merge(list,`ec,compr(list,construct(XML_element,bind(xml_element,construct(element_type,bind(PCDATA,`nv)))),
								   iterate(`nv,`(r->hd))))>;
		| XML_element => ec = #<merge(list,`ec,unit(list,`(r->hd)))>;
		| scope(XML_element) => ec = #<merge(list,`ec,unit(list,`(r->hd)))>;
		| list(XML_element) => ec = #<merge(list,`ec,`(r->hd))>;
		| list(scope(XML_element)) => ec = #<merge(list,`ec,`(r->hd))>;
		| _ => type_error("wrong element in an XML construction",r->hd,tp);
		#end;
	     };
	     Expr ne = #<construct(XML_element,bind(xml_element,construct(element_type,bind(TAG,struct(bind(name,`(estring(tag->name()))),
									  bind(attributes,zero(list)),bind(content,`ec))))))>;
	     typecheck(ne,cvars,lvars,gvars);
	     ne = eliminate_type_vars(ne,lvars,true,true);
	     e->set_type(#<MODIFY(`ne)>);
	     retp = #<scope(XML_element)>;
	   };
  | eq(`x,`y) => { Expr tx = typecheck(x,cvars,lvars,gvars);
		   Expr ty = typecheck(y,cvars,lvars,gvars);
		   if (!unify(e,tx,ty,lvars,true) && !unify(e,ty,tx,lvars,true))
		      type_error("Incompatible types in equality",tx,ty);
		   retp = #<boolean>;
		 };
  | neq(`x,`y) => { Expr tx = typecheck(x,cvars,lvars,gvars);
		    Expr ty = typecheck(y,cvars,lvars,gvars);
		    if (!unify(e,tx,ty,lvars,true) && !unify(e,ty,tx,lvars,true))
		       type_error("Incompatible types in inequality",tx,ty);
		   retp = #<boolean>;
		  };
  | and(...args) => { for(list<Expr>* r = args; r->consp(); r=r->tl)
		      {  Expr tp = typecheck(r->hd,cvars,lvars,gvars);
			 if (!unify(r->hd,tp,#<boolean>,lvars))
			    type_error("Expected a boolean",r->hd,tp);
		      };
		      retp = #<boolean>;
                    };
  | or(...args)  => { for(list<Expr>* r = args; r->consp(); r=r->tl)
		      {  Expr tp = typecheck(r->hd,cvars,lvars,gvars);
			 if (!unify(r->hd,tp,#<boolean>,lvars))
			    type_error("Expected a boolean",r->hd,tp);
		      };
		      retp = #<boolean>;
                    };
  | OID(`x) => retp = typecheck(x,cvars,lvars,gvars);
  | null => retp = fresh_type_variable();
  | plus(`x,`y)
	: collection_typep(typecheck(x,cvars,lvars,gvars))
	=> #case instantiate_type(typecheck(x,cvars,lvars,gvars),lvars)
	   | list(`tp)
		=> if (unify(e,#<list(`tp)>,typecheck(y,cvars,lvars,gvars),lvars))
		   {  e->set_type(#<MODIFY(merge(list,`x,`y))>);
		      retp = #<list(`tp)>;
		   }
		   else type_error("Incompatible types",#<list(`tp)>,typecheck(y,cvars,lvars,gvars));
	   | `tp => type_error("You can use '+' to merge lists only",e,tp);
	   #end;
  | simple_type_to_key(`x,`tp)
	=> retp = #<string>;
  | simple_type_to_cmp(`x,`y,`tp)
	=> retp = #<integer>;
  | merge_cmp(`x,`y)
	=> retp = #<integer>;
  | concat_keys(`x,`y)
	=> retp = #<string>;
  | `op(`x,`y)
	: ((op->eq(#<lt>) || op->eq(#<gt>) || op->eq(#<leq>) || op->eq(#<geq>))
	   && collection_typep(typecheck(x,cvars,lvars,gvars)))
	=> #case instantiate_type(typecheck(x,cvars,lvars,gvars),lvars)
	   | `f(`tp) : (f->eq(#<bag>) || f->eq(#<set>))
		=> if (unify(e,#<`f(`tp)>,typecheck(y,cvars,lvars,gvars),lvars))
		   {  Expr u;
		      #case op
		      | leq => u = #<compr(all,compr(some,eq(x,y),iterate(y,`y)),iterate(x,`x))>;
		      | geq => u = #<compr(all,compr(some,eq(y,x),iterate(x,`x)),iterate(y,`y))>;
		      | lt => u = #<and(compr(all,compr(some,eq(x,y),iterate(y,`y)),iterate(x,`x)),
					compr(some,compr(all,neq(y,x),iterate(x,`x)),iterate(y,`y)))>;
		      | gt => u = #<and(compr(all,compr(some,eq(y,x),iterate(x,`x)),iterate(y,`y)),
					compr(some,compr(all,neq(x,y),iterate(y,`y)),iterate(x,`x)))>;
		      #end;
		      e->set_type(#<MODIFY(`u)>);
		      retp = #<boolean>;
		   }
		   else type_error("Incompatible types",#<`f(`tp)>,typecheck(y,cvars,lvars,gvars));
	   | `tp => type_error("Comparison between these types is not permitted",
			       tp,typecheck(y,cvars,lvars,gvars));
	   #end;
  | `op(`x)
	: (op->eq(#<first>) || op->eq(#<last>))
	=> { Expr tp = typecheck(x,cvars,lvars,gvars);
	     Expr ltp = fresh_type_variable();
	     if (unify(x,tp,#<list(`ltp)>,lvars))
		retp = ltp;
	     else type_error("Expected a list collection",tp);
	   };
  | like(`x,`pat)
	=> if (unify(x,typecheck(x,cvars,lvars,gvars),#<string>,lvars))
	      retp = #<boolean>;
	   else type_error("pattern matching works only for strings",
			   typecheck(x,cvars,lvars,gvars),x);
  | element(`x)
	=> #case instantiate_type(typecheck(x,cvars,lvars,gvars),lvars)
	   | `f(void(`tp)) => retp = tp;
	   | `f(`tp) => retp = tp;
	   | `tp => type_error("Expected a list collection",tp);
	   #end;
  | union_construction(`f,`tag,_,`e,_,_)
	=> retp = typecheck(#<construct(`f,bind(`tag,`e))>,cvars,lvars,gvars);
  | union_construction(`f,_,`tag,_,`e,_,_)
	=> retp = typecheck(#<construct(`f,bind(`tag,`e))>,cvars,lvars,gvars);
  | scoped_variables(_,`tp)
	=> retp = tp;
  | LDBobject(`n)
	=> retp = LDBobject(n->info.Integer).gettype();
  | `c(`f,...args)	/* class constructor */
	  : c->eq(#<construct>) || c->eq(#<persistent_construct>)
	  => if (classp(f->name()))
	     {  Schema sm = type_to_schema(class_type(f->name()));
		for(; args->consp(); args=args->tl)
		   #case args->hd
		   | bind(`v,`e)
			=> if (sm->in(v->name()))
			   {  Expr tp = typecheck(e,cvars,lvars,gvars);
			      if (!unify(args->hd,tp,sm->find(v->name()),lvars,true))
				 type_error("Incompatible types in constructor",
					    args->hd,tp,sm->find(v->name()));
			   } else type_error("Wrong attribute in constructor",v);
		   #end;
		retp = f;
	     }
	     else #case get_declaration_binding(f->name())
		  | union(`nm,`etp,...cases)
			=> {  if (args->length() != 1)
				 type_error("union construction must have only one case",e);
			      list<Expr>* ncases = Nil;
			      Expr a = args->hd->arguments()->hd;
			      Expr v = args->hd->arguments()->tl->hd;
			      bool found = false;
			      for(list<Expr>* r=cases->reverse(); r->consp(); r=r->tl)
				 #case r->hd
				 | case(`tp,`dcl,...cs)
					: member(#<scope(`a)>,cs)
					=> { found = true;
					     Expr ntp = typecheck(v,cvars,lvars,gvars);
					     if (!unify(v,ntp,tp,lvars,true))
						type_error("Illegal union value",tp,ntp);
					     ncases = ncases->cons(#<case(`ntp,`dcl,...cs)>);
					     e->set_type(#<MODIFY(union_construction(`f,`a,`dcl,`v,`tp,
									union(`nm,`etp,...cases)))>);
					   };
				 | _ => ncases = ncases->cons(r->hd);
				 #end;
			      if (found)
				 retp = #<union(`nm,`etp,...ncases)>;
			      else type_error("Illegal tag in union construction",e);
			   };
		  | _ => type_error("invalid constructor name",f);
		  #end;
  | desc(`e)
	=> retp = typecheck(e,cvars,lvars,gvars);
  | call(reduce,`merge,`zero,`x)
	=> { if (!merge->variablep())
		type_error("The merge function of reduce must be the name of a function",merge);
	     #case instantiate_type(typecheck(x,cvars,lvars,gvars),lvars)
	     | list(`tp)
		       => #case get_declaration_binding(merge->name())
			  | function(`name,params(bind(_,`t1),bind(_,`t2)),`otype,_)
				: t2->eq(otype) && unify(merge,tp,t1,lvars)
				=> if (!unify(zero,typecheck(zero,cvars,lvars,gvars),otype,lvars))
				      type_error("The zero value of reduce has wrong type",zero);
				   else retp = otype;
			  | _ => type_error("Illegal merge function in reduce",merge);
			  #end;
	     | _ => type_error("Reduce can only be done on a list",e);
	     #end;
	   };
  | call(`f,...args)		/* class constructor */
	: classp(f->name())
	=> { list<Expr>* r = args;
	     list<Expr>* ar = Nil;
	     Schema sm = type_to_schema(class_type(f->name()));
	     Names s = sm->names();
	     for(; s->consp() && r->consp(); s=s->tl, r=r->tl)
	     {  Expr tp = typecheck(r->hd,cvars,lvars,gvars);
		ar = ar->cons(#<bind(`(variable(s->hd)),`(r->hd))>);
		if (!unify(r->hd,tp,sm->find(s->hd),lvars))
		   type_error("Incompatible types in constructor",
			      r->hd,tp,sm->find(s->hd));
	     };
	     if (r->consp() || s->consp())
		type_error("wrong number of arguments in constructor",e);
	     ar = ar->reverse();
	     e->set_type(#<MODIFY(construct(f,...ar))>);
	     retp = f;
	   };
  | call(`f,...args)		/* macro definition or function */
	: get_declarations(f->name())->consp()
	=> #case get_declaration_binding(f->name())
	   | define(`name,params(...ps),`body)
		=> { Expr new_exp = translate(body);
		     list<Expr>* r = args;
		     for(; r->consp() && ps->consp(); r=r->tl, ps=ps->tl)
			new_exp = subst_expr(ps->hd,r->hd,new_exp);
		     if (r->consp() || ps->consp())
			type_error("Wrong number of arguments in macro call",e);
		     e->set_type(#<MODIFY(`new_exp)>);
		     retp = typecheck(new_exp,cvars,lvars,gvars);
		   };
	   | function(`name,params(...ps),`otype,`body)
		=> { for(int i=1; args->consp() && ps->consp(); args=args->tl, ps=ps->tl, i++)
			#case ps->hd
			| bind(_,`tp)
				=> if (!unify(args->hd,typecheck(args->hd,cvars,lvars,gvars),tp,lvars))
				      type_error("function argument does not match the type",name,args->hd,tp);
			#end;
		     if (args->consp() || ps->consp())
			type_error("wrong number of arguments in constructor",e);
		     return otype;
		   };
	   | `dcl => type_error("Function call must be a constructor, a function, or a macro",e);
	   #end;
  | group_by(`m,`hd,...r)
	=> return typecheck(#<compr(`m,`hd)>,cvars,lvars,gvars);
  | `op( `M, `table, `v, `pred, ...r )
       : op->eq(#<get>) || op->eq(#<TABLE_SCAN>) || op->eq(#<INDEX_SCAN>)
       => #case instantiate_type(typecheck(table,cvars,lvars,gvars),lvars)
	  | `f(`tp) => retp = #<`M(struct(bind(`v,`tp)))>;
	  | `tp => type_error("Expected a collection",table,tp);
	  #end;
  | `op( `M, `e, `v, `hd, `pred, ...r )
       : op->eq(#<reduce>) || op->eq(#<REDUCE>)
       => #case instantiate_type(typecheck(e,cvars,lvars,gvars),lvars)
	  | `f(`tp) => { Schema s = type_to_schema(tp)->extend(cvars);
			 Expr tp = typecheck(hd,s,lvars,gvars);
			 if (!unify(pred,typecheck(pred,s,lvars,gvars),#<boolean>,lvars))
			    type_error("Expected a boolean",pred,typecheck(pred,s,lvars,gvars));
			 if (M->eq(#<all>) || M->eq(#<some>))
			    if (unify(e,tp,#<boolean>,lvars))
			       retp = #<boolean>;
			    else type_error("Expected a boolean predicate in quantification",e,tp);
			 else if (M->eq(#<sum>) || M->eq(#<prod>) || M->eq(#<max>) || M->eq(#<min>))
			    if (unify(e,tp,#<integer>,lvars))
			       retp = #<integer>;
			    else if (unify(e,tp,#<float>,lvars))
			       retp = #<float>;
			    else type_error("Expected a number in aggregation",e,tp);
			 else if (M->eq(#<concat>))
			    if (unify(e,tp,#<string>,lvars))
			       retp = #<string>;
			    else type_error("Expected a string value in aggregation",e,tp);
			 else retp = #<`M(`tp)>;
		       };
	  | `tp => type_error("Expected a collection of tuples",e,tp);
	  #end;
  | `op( `M, `e, `v, `hd, `vars, `bpred, `apred, ...r )
       : op->eq(#<nest>) || op->eq(#<NEST>)
       => #case instantiate_type(typecheck(e,cvars,lvars,gvars),lvars)
	  | `f(`tp) => { Schema s = type_to_schema(tp)->extend(cvars);
			 Expr tp = typecheck(hd,s,lvars,gvars);
			 if (M->eq(#<list>) || M->eq(#<bag>) || M->eq(#<set>))
			    tp = #<`M(`tp)>;
			 Schema ns = s->extend(v->name(),tp);
			 if (!unify(bpred,typecheck(bpred,ns,lvars,gvars),#<boolean>,lvars))
			    type_error("Expected a boolean",bpred,typecheck(bpred,s,lvars,gvars));
			 if (!unify(apred,typecheck(apred,ns,lvars,gvars),#<boolean>,lvars))
			    type_error("Expected a boolean",apred,typecheck(apred,s,lvars,gvars));
			 list<Expr>* t = typecheck_nest_vars(vars,s,lvars,gvars);
			 Expr ne = e;
			 bool stop = false;
			 for(; !stop;)
			 {  #case ne
			    | SORT(NEST( _, `me, `w, _, `vars2, ...k),_)
				: vars->eq(vars2)
				=> t = t->append(Cons(#<bind(`w,`(typecheck(w,s,lvars,gvars)))>,Nil));
				   ne = me;
			    | `op2( _, `me, `w, _, `vars2, ...k)
				: (op2->eq(#<nest>) || op2->eq(#<NEST>))
				  && vars->eq(vars2)
				=> t = t->append(Cons(#<bind(`w,`(typecheck(w,s,lvars,gvars)))>,Nil));
				   ne = me;
			    | _ => stop = true;
			    #end;
			 };
			 retp = #<`M(struct(...t,bind(`v,`tp)))>;
		       };
	  | `tp => type_error("Expected a collection of tuples",e,tp);
	  #end;
  | `op( `M, `e, `v, `path, `pred, ...r )
       : op->eq(#<unnest>) || op->eq(#<UNNEST>)
       => #case instantiate_type(typecheck(e,cvars,lvars,gvars),lvars)
	  | `f(struct(...args))
		=> { Schema s = type_to_schema(#<struct(...args)>)->extend(cvars);
		     #case instantiate_type(typecheck(path,s,lvars,gvars),lvars)
		     | `g(`tp) => { s = s->extend(v->name(),tp);
				    if (!unify(pred,typecheck(pred,s,lvars,gvars),#<boolean>,lvars))
				       type_error("Expected a boolean",pred,typecheck(pred,s,lvars,gvars));
				    retp = #<`M(struct(...args,bind(`v,`tp)))>;
				  };
		     | `tp => type_error("The unnesting path must return a collection",path,tp);
		     #end;
		  };
	  | `tp => type_error("Expected a collection of tuples",e,tp);
	  #end;
  | MAP( `M, `e, `v, `pred, _, `path )
       => #case instantiate_type(typecheck(e,cvars,lvars,gvars),lvars)
	  | `f(struct(...args))
		=> { Schema s = type_to_schema(#<struct(...args)>)->extend(cvars);
		     Expr tp = typecheck(path,s,lvars,gvars);
		     s = s->extend(v->name(),tp);
		     if (!unify(pred,typecheck(pred,s,lvars,gvars),#<boolean>,lvars))
			type_error("Expected a boolean",pred,typecheck(pred,s,lvars,gvars));
		     retp = #<`M(struct(...args,bind(`v,`tp)))>;
		  };
	  | `tp => type_error("Expected a collection of tuples",e,tp);
	  #end;
  | `op( `M, `x, `y, `pred, ...r )
       : op->eq(#<join>) || op->eq(#<NESTED_LOOP>) || op->eq(#<BLOCK_NESTED_LOOP>) || op->eq(#<MERGE_JOIN>) || op->eq(#<INDEXED_LOOP>)
       => #case instantiate_type(typecheck(x,cvars,lvars,gvars),lvars)
	  | `f(struct(...xargs))
		=> #case instantiate_type(typecheck(y,cvars,lvars,gvars),lvars)
		   | `g(struct(...yargs))
			=> { Schema s = type_to_schema(#<struct(...xargs)>)
						->extend(type_to_schema(#<struct(...yargs)>))
						->extend(cvars);
			     if (!unify(pred,typecheck(pred,s,lvars,gvars),#<boolean>,lvars))
				type_error("Expected a boolean",pred,typecheck(pred,s,lvars,gvars));
			     retp = #<`M(struct(...xargs,...yargs))>;
			   };
		   | `tp => type_error("Expected a collection of tuples",y,tp);
		   #end;
	  | `tp => type_error("Expected a collection of tuples",x,tp);
	  #end;
  | `op( `e, `order )
       : op->eq(#<sort>) || op->eq(#<SORT>)
       => #case instantiate_type(typecheck(e,cvars,lvars,gvars),lvars)
	  | `f(`etp)
		=> retp = #<`f(`etp)>;
	  | `tp => type_error("Expected a collection of tuples",e,tp);
	  #end;
  | `f(...args)		/* primitive operation, such as + */
	: internal_methods->in(f->name())
	=> { list<Expr>* types = Nil;
	     for(; args->consp(); args=args->tl)
		types = types->cons(typecheck(args->hd,cvars,lvars,gvars));
	     #case find_internal_method(f->name(),types->reverse(),lvars)->first
	     | none => type_error("Incompatible types for primitive operation",e,#<`f(...(types->reverse()))>);
	     | `tp => retp = tp;
	     #end;
	   };
  | `f(...args)		/* construction of a collection */
	: member(f,Nil->cons(#<set>)->cons(#<bag>)->cons(#<list>))
	=> { Expr tp = fresh_type_variable();
	     for(list<Expr>* r = args; r->consp(); r=r->tl)
		if (!unify(r->hd,tp,typecheck(r->hd,cvars,lvars,gvars),lvars))
		   type_error("incompatible types in collection construction",r->hd);
	     retp = #<`f(`tp)>;
	   };
  | `f(...args)
	=> type_error("no such function",e);
  | nil => retp = fresh_type_variable();
  | true => retp = #<boolean>;
  | false => retp = #<boolean>;
  | `e : e->stringp()
	=> retp = #<string>;
  | `e : e->integerp()
	=> retp = #<integer>;
  | `e : e->realp()
	=> retp = #<float>;
  | `v : v->variablep()
	=> if (cvars->in(v->name()))
	      retp = cvars->find(v->name());
	   else if (extentp(v))
	        {  Expr cn = extent_type(v->name());
		   // if v is the extent of a class with subclasses,
		   // merge the extents of these subclasses to the extent
		   Expr ee = variable(v->name());
		   for(list<String>* r = class_subclasses(cn->name()); r->consp(); r=r->tl)
		      if (!get_class_extent(variable(r->hd))->eq(#<none>))
			 ee = #<merge(set,`ee,`(get_class_extent(variable(r->hd))))>;
		   retp = (interpreterp) ? #<set(`(make_void_type(cn)))> : #<set(`cn)>;
		   if (!ee->eq(e))
		      e->set_type(#<MODIFY(`ee)>);
		}
	   else if (constantp(v))
		{  #case get_declaration_binding(v->name())
		   | constant(scope(`type),`cname,`value)
			=> {  //e->set_type(#<MODIFY(`value)>);
			      retp = type;
			   };
		   | constant(`type,`cname,`value)
			=> {  //e->set_type(#<MODIFY(`value)>);
			      retp = type;
			   };
		   #end; }
	   else {  // is v a scoped variable?
		   Expr tp = find_scoped_variable(v->name());
		   if (!tp->eq(#<none>))
		      retp = tp;
		   else {
		   // if v is an attribute name and there is no ambiguity, find the
		   // class name that has this attribute and make v a projection
		   bool found = false;
		   Expr cls;
		   for(Names ns = cvars->names(); ns->consp(); ns=ns->tl)
		   {  tp = cvars->find(ns->hd);
		      if (is_class(tp))
		      {  Schema env = type_to_schema(class_type(tp->name()));
			 if (env->in(v->name()))
			    if (found)
			       type_error("Ambiguous attribute name",v);
			    else {  found = true;
				    tp = env->find(v->name());
				    cls = #<project(`(variable(ns->hd)),`(variable(v->name())),`tp)>;
				 };
		      };
		  };
		  if (found)
		  {  e->set_type(#<MODIFY(`cls)>);
		     retp = tp;
		  }
		  else type_error("Undefined variable",e); };
	   };
  | _ => type_error("Unknown expression",e);
  #end;
  if (TRACE_TYPECHECK)
     cout << --typecheck_counter << ") -> " << retp << "\t" << lvars << endl;
  return retp;
} DEBUG(e);
};


Expr eliminate_type_vars ( Expr x, Schema lvars, bool first_time, bool type_varsp ) {
  if (x->type())
     #case x->type()
     | MODIFY(`e)
	: first_time
	=> return eliminate_type_vars(e,lvars,first_time,type_varsp);
     #end;
  #case x
  | ALPHA(`v,`m)
	=> if (lvars->in(v->name()))
	   {  Expr tp = eliminate_type_vars(lvars->find(v->name()),lvars,first_time,type_varsp);
	      x->arguments()->tl->hd = tp;
	      return tp;
	   } else if (false && !type_varsp)
		return eliminate_type_vars(m,lvars,first_time,true);
	   else return v;
  | `f(`z)
	: f->functionp()
	=> { Expr w = eliminate_type_vars(z,lvars,first_time,false);
	     #case f
	     | ALPHA(`v,`m)
		=> if (lvars->in(v->name()))
		   {  Expr tp = eliminate_type_vars(lvars->find(v->name()),lvars,first_time,type_varsp);
		      x->arguments()->tl->hd = tp;
		      return #<`tp(`w)>;
		   } else return #<`(eliminate_type_vars(m,lvars,first_time,true))(`w)>;
	     #end;
	   };
  | `f(...r) => { list<Expr>* args = Nil;
		  for(list<Expr>* s = r; s->consp(); s=s->tl)
		     args = args->cons(eliminate_type_vars(s->hd,lvars,first_time,false));
		  args = args->reverse();
		  Expr g = eliminate_type_vars(f,lvars,first_time,true);
		  return #<`g(...args)>;
		};
  | _ => return x;
  #end;
};


Expr type_of ( Expr &e, Schema vars, bool first_time = false, bool type_varsp = true ) {
  Schema cvars = vars;
  GEnv gvars = new list<pair<Expr,Expr>*>;
  Expr tp = typecheck(e,cvars,global_lvars,gvars);
  e = eliminate_type_vars(e,global_lvars,first_time,type_varsp);
  return eliminate_type_vars(tp,global_lvars,first_time,type_varsp);
};


Expr type_of ( Expr &e ) {
  Schema sch = new binding<Expr>;
  return type_of(e,sch);
};