/********************************************************************************
*
* File: typecheck.gen
* Title: Type-checking for OQL
* Programmer: Leonidas Fegaras, UTA
* Date: 4/10/97
*
********************************************************************************/

#include "evaluation.h"
#include "typecheck.h"
#include "constant.h"


/* defined in constant.cc */
extern Internals internal_methods;


/* the database content and catalog */
extern database* DATABASE;


/* catching type exceptions */
#define DEBUG(exp) catch (type_exception)		\
 { cout << "*** Found in " << exp << endl;		\
   throw type_exception(); }


/* a type error is a fatal error: it causes the program to abort */
type_error ( string msg, Expr e ) {
  cout << "\n*** Type Error: " << msg << " (" << e << ")\n";
  throw type_exception();
};


/* 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 */
Type fresh_type_variable () {
  return #<ALPHA(`(new_variable()),set)>;
};


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

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

bool commutative ( Expr x ) { 
  return member(x,commutative_functions);
};

bool idempotent ( Expr x ) {
  return member(x,idempotent_functions);
};


Type expand ( String name ) {
  return #<bag(`(schema_to_type(find_extent(name)->schema)))>;
};


/* if a type name is an extent name, return the extent interface */
Type expand_type ( Type tp) {
  if (tp->variablep())
     if (extentp(tp))
	return expand(tp->name());
     else return schema_to_type(find_interface(tp->name())->schema);
  return tp;
};


/* convert an OQL term to comprehension form */
Expr convert ( Expr e ) {
  Expr u;
  #case e
  | define(`tp,`x,`u)
      => return #<define(`tp,`x,`(convert(u)))>;
  | `f(...r) => { list<Expr>* nr = Nil;
		  for(list<Expr>* s = r; s->consp(); s=s->tl)
		     nr = nr->cons(convert(s->hd));
		  nr = nr->reverse();
		  u = #<`f(...nr)>;
		};
  | _ => u = e;
  #end;
  #case u
  | member(`x,`s)
      => { Expr nv = new_variable();
	   Type lv = fresh_type_variable();
	   return #<compr(`lv,eq(`x,`nv),iterate(`nv,`s))>;
	 };
  | intersect(`x,`y)
      => { Expr nx = new_variable();
	   Expr ny = new_variable();
	   Type lv = fresh_type_variable();
	   return #<compr(`lv,`nx,iterate(`nx,`x),compr(some,eq(`nx,`ny),iterate(`ny,`y)))>;
	 };
  | union(`x,`y) => Type lv = fresh_type_variable();
		    return #<merge(`lv,`x,`y)>;
  | exists(`x,`s,`e)
      => return #<compr(some,`e,iterate(`x,`s))>;
  | forall(`x,`s,`e)
      => return #<compr(all,`e,iterate(`x,`s))>;
  | group(`x,`s,NONE,...by)
           => { Expr nv = new_variable();
		list<Expr>* eqs = Nil;
		for(list<Expr>* r = by; r->consp(); r=r->tl)
		   #case r->hd
		   |  bind(_,`e) => eqs = eqs->cons(#<eq(`e,`(subst_expr(x,nv,e)))>);
		   #end;
		eqs = eqs->reverse();
		Type lv = fresh_type_variable();
		Type tv = fresh_type_variable();
	        return #<compr(`tv,struct(...by,bind(partition,compr(`lv,`nv,iterate(`nv,`s),...eqs))),
			       iterate(`x,`s))>;
	      };
  | group(`x,`s,struct(...with),...by)
           => { Expr nv = new_variable();
		list<Expr>* eqs = Nil;
		for(list<Expr>* r = by; r->consp(); r=r->tl)
		   #case r->hd
		   |  bind(_,`e) => eqs = eqs->cons(#<eq(`e,`(subst_expr(x,nv,e)))>);
		   #end;
		eqs = eqs->reverse();
		Type lv = fresh_type_variable();
		Type tv = fresh_type_variable();
		Type uv = fresh_type_variable();
	        return #<compr(`tv,struct(...by,...with),
			       iterate(`x,`s),iterate(partition,unit(`uv,compr(`lv,`nv,iterate(`nv,`s),...eqs))))>;
	      };
  | flatten(`e)
      => { Expr nx = new_variable();
	   Expr ns = new_variable();
	   Type lv = fresh_type_variable();
	   return #<compr(`lv,`nx,iterate(`ns,`e),iterate(`nx,`ns))>;
	 };
  | min(`e)
      => { Expr nx = new_variable();
	   return #<compr(min,`nx,iterate(`nx,`e))>;
	 };
  | max(`e)
      => { Expr nx = new_variable();
	   return #<compr(max,`nx,iterate(`nx,`e))>;
	 };
  | sum(`e)
      => { Expr nx = new_variable();
	   return #<compr(sum,`nx,iterate(`nx,`e))>;
	 };
  | count(`e)
      => { Expr nx = new_variable();
	   return #<compr(sum,1,iterate(`nx,`e))>;
	 };
  | `f(...r) => if (member(f,Nil->cons(#<set>)->cons(#<bag>)->cons(#<list>)))
		{  Expr res = #<zero(`f)>;
		   for(list<Expr>* s = r->reverse(); s->consp(); s=s->tl)
		      res = #<merge(`f,unit(`f,`(s->hd)),`res)>;
		   return res;
		};
  #end;
  return u;
};


/* type variable instantiations */
bool substitute ( Expr var, Type y, Schema &lvars ) {
  Schema s = new binding<Expr>;
  for(binding<Expr>* ns = lvars; ns->more(); ns=ns->next())
     s = s->extend(ns->current()->first,
		   subst_expr(var,y,ns->current()->second));
  lvars = s->extend(var->name(),y);					/* destructive */
  return true;
};


bool stronger_monoid ( Expr x, Expr y) {
  #case x
  | list => return y->eq(#<list>);
  | bag => return member(y,Nil->cons(#<bag>)->cons(#<list>));
  | _ => return true;
  #end;
};


bool compatible ( Type x, Type y ) {
  #case x
  | ALPHA(`v,`m) => #case y
		    | `f(`tp) => if (f->eq(m)) return true;
				 else if (stronger_monoid(m,f))
				 { x->arguments()->tl->hd = f;		/* destructive */
				   return true;
				 } else return false;
		    | Short => if (m->eq(#<bag>)) return true;
				 else if (stronger_monoid(m,#<bag>))
				 { x->arguments()->tl->hd = #<bag>;	/* destructive */
				   return true;
				 } else return false;
		    | bool => return m->eq(#<set>);
		    #end;
  #end;
  return true;
};


/* type unification */
bool unify ( Expr e, Type x, Type y, Schema &lvars ) {
  if (x->eq(y)) return true;
  #case x
  |  ALPHA(`vx,_) => if (lvars->in(vx->name()))
 			x = lvars->find(vx->name());
  #end;
  #case y
  |  ALPHA(`vy,_) => if (lvars->in(vy->name()))
 			y = lvars->find(vy->name());
  #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;
	  |  `f(...r) => #case x
			 |  `g(...s) => { bool b = unify(e,f,g,lvars);
					  for(; r->consp() && s->consp(); r=r->tl, s=s->tl)
					     b = b && unify(e,r->hd,s->hd,lvars);
					  return b;
					};
			 |  _ => if (x->variablep())
				    if (member(x,all_interfaces()))
				       return unify(e,schema_to_type(find_interface(x->name())->schema),y,lvars);
				    else return false;
				 else return false;
			 #end;
	  |  _  => if (y->variablep())
		      if (member(y,all_interfaces()))
			 return unify(e,x,schema_to_type(find_interface(y->name())->schema),lvars);
		      else return x->eq(y);
		   else return x->eq(y);
	  #end;
  #end;
  return true;
};


/* checks a comprehension for type errors */
Type typecheck ( Expr e, Schema &cvars, Schema &lvars ) {
try{
  #case e
  | zero(`M) => { Type lv = fresh_type_variable();
		  return #<`M(`lv)>;
	        };
  | unit(`M,`e) => { Type tp = typecheck(e,cvars,lvars);
		     return #<`M(`tp)>;
		   };
  | merge(`M,`x,`y)
      => { Type xtp = typecheck(x,cvars,lvars);
	   Type ytp = typecheck(y,cvars,lvars);
	   if (!(unify(e,xtp,ytp,lvars)))
	      type_error("Incompatible merge inputs",#<type_of(`e,`xtp,`ytp)>);
	   return xtp;
	 };
  | compr(`M,`head,...qualifiers)
      => { Schema s = cvars;
	   for(list<Expr>* r = qualifiers; r->consp(); r=r->tl)
	   #case r->hd
	   |  iterate(`v,`u)
		=> #case expand_type(typecheck(u,s,lvars))
		   | `M(`tp) => s = s->extend(v->name(),tp);
		   | _ => type_error("Value is not a collection",u);
		   #end;
	   |  `u => { Type tp = typecheck(u,s,lvars);
		      if (!(unify(e,tp,#<bool>,lvars)))
			 type_error("Expected a predicate",u);
		    };
	   #end;
	   Type tp = typecheck(head,s,lvars);
	   if (M->eq(#<all>) || M->eq(#<some>))
	      if (unify(e,tp,#<bool>,lvars)) return #<bool>;
		 else type_error("Expected a boolean predicate in quantification",e);
	   else if (M->eq(#<sum>) || M->eq(#<prod>) || M->eq(#<max>))
	      if (unify(e,tp,#<Short>,lvars)) return #<Short>;
		 else type_error("Expected a boolean predicate in quantification",e);
	   else return #<`M(`tp)>;
	 };
  | project(`x,`a)
      => { Type tp = typecheck(x,cvars,lvars);
	   if (tp->variablep())
	      tp = schema_to_type(find_interface(tp->name())->schema);
	   #case tp
	   |  struct(...r) => { for(list<Expr>* s = r; s->consp(); s=s->tl)
				   #case s->hd
				   |  bind(`v,`e) => if (v->eq(a)) return e;
				   #end;
				type_error("Structure does not have the projection attribute",e);
			      };
	   |  _ => type_error("Expected a structure in projection",#<type(`e,`tp)>);
	   #end;
	 };
  | struct(...r) => { list<Type>* s = Nil;
		      for(; r->consp(); r=r->tl)
		         #case r->hd
		         |  bind(`v,`u) => s = s->cons(#<bind(`v,`(typecheck(u,cvars,lvars)))>);
		         #end;
		      s = s->reverse();
		      return #<struct(...s)>;
		    };
  | method(`f,`o,...args)
	 => type_error("not implemented yet",e);
  | if(`pred,`x,`y)
	 => { Type tx = typecheck(x,cvars,lvars);
	      Type ty = typecheck(y,cvars,lvars);
	      if (!unify(pred,typecheck(pred,cvars,lvars),#<bool>,lvars))
		 type_error("Predicate in if-then-else is not boolean",e);
	      if (!unify(e,tx,ty,lvars))
		 type_error("Incompatible types in if-then-else",e);
	      return tx;
	    };
   | eq(`x,`y) => { Type tx = typecheck(x,cvars,lvars);
		   Type ty = typecheck(y,cvars,lvars);
		   if (!unify(e,tx,ty,lvars))
		      type_error("Incompatible types in equality",e);
		   return #<bool>;
		 };
  | neq(`x,`y) => { Type tx = typecheck(x,cvars,lvars);
		    Type ty = typecheck(y,cvars,lvars);
		    if (!unify(e,tx,ty,lvars))
		       type_error("Incompatible types in inequality",e);
		    return #<bool>;
		  };
  | and(...args) => { for(list<Expr>* r = args; r->consp(); r=r->tl)
			 if (!unify(r->hd,typecheck(r->hd,cvars,lvars),#<bool>,lvars))
			    type_error("Expected a boolean",r->hd);
		      return #<bool>;
                    };
  | or(...args)  => { for(list<Expr>* r = args; r->consp(); r=r->tl)
			 if (!unify(r->hd,typecheck(r->hd,cvars,lvars),#<bool>,lvars))
			    type_error("Expected a boolean",r->hd);
		      return #<bool>;
                    };
  | define(`tp,`x,`u)
	 => { if (!unify(u,typecheck(u,cvars,lvars),tp,lvars))
		 type_error(form("Type of %s is not",x->name()->value()),tp);
	      cvars = cvars->extend(x->name(),tp);
	      return #<unit>;
	    };
  | OID(`x) => return #<Short>;
  | null => return fresh_type_variable();
  | reduce(`M,`e,`v,`hd,`pred)
       => #case typecheck(e,cvars,lvars)
	  | `f(struct(...args))
		     => { Type tp = typecheck(hd,cvars,lvars);
			  cvars = cvars->extend(v->name(),tp);
			  if (!unify(pred,typecheck(pred,cvars,lvars),#<bool>,lvars))
			     type_error("Expected a boolean",pred);
			  return #<`M(struct(...args,bind(`v,`tp)))>;
			};
	  | _ => type_error("Expected a collection of tuples",e);
	  #end;
  | unnest( `M, `e, `v, `path, `pred, `keep )
       => #case typecheck(e,cvars,lvars)
	  | `f(struct(...args))
		     => { Type tp = typecheck(path,cvars,lvars);
			  cvars = cvars->extend(v->name(),tp);
			  if (!unify(pred,typecheck(pred,cvars,lvars),#<bool>,lvars))
			     type_error("Expected a boolean",pred);
			  return #<`M(struct(...args,bind(`v,`tp)))>;
			};
	  | _ => type_error("Expected a collection of tuples",e);
	  #end;
  | nest( `M, `e, `v, `hd, `gv, `vars, `pred )
       => #case typecheck(e,cvars,lvars)
	  | `f(struct(...args))
		     => { Type tp = typecheck(hd,cvars,lvars);
			  cvars = cvars->extend(v->name(),tp);
			  if (!unify(pred,typecheck(pred,cvars,lvars),#<bool>,lvars))
			     type_error("Expected a boolean",pred);
			  return #<`M(struct(...args,bind(`v,`tp)))>;
			};
	  | _ => type_error("Expected a collection of tuples",e);
	  #end;
  | get(`M,`table,`name,`pred)
       => #case typecheck(table,cvars,lvars)
	  | `f(`tp) => { cvars = cvars->extend(name->name(),tp);
			 return #<`M(struct(bind(`name,`tp)))>;
		       };
	  | _ => type_error("Expected a collection",table);
	  #end;
  | join( `M, `x, `y, `pred, `keep )
       => #case typecheck(x,cvars,lvars)
	  | `f(struct(...xargs))
		=> #case typecheck(y,cvars,lvars)
		   | `g(struct(...yargs))
			=> return #<`M(struct(...xargs,...yargs))>;
		   | _ => type_error("Expected a collection of tuples",y);
		   #end;
	  | _ => type_error("Expected a collection of tuples",x);
	  #end;
  | map( `M, `e, `v, `f )
       => #case typecheck(e,cvars,lvars)
	  | `f(struct(...args))
		     => { Type tp = typecheck(f,cvars,lvars);
			  cvars = cvars->extend(v->name(),tp);
			  return #<`M(struct(...args,bind(`v,`tp)))>;
			};
	  | _ => type_error("Expected a collection of tuples",e);
	  #end;
  | `f(...args) => { if (internal_methods->in(f->name()))
		     { list<Expr>* r = args;
		       pair<Signature,Function>* p = internal_methods->find(f->name());
		       Schema s;
		       for(s = p->first->first; r->consp() && s->more(); s=s->next(), r=r->tl)
			  if (!unify(r->hd,typecheck(r->hd,cvars,lvars),s->current()->second,lvars))
			    type_error("Incompatible types in primitive function",r->hd);
		       if (r->consp() || s->more())
			  type_error("wrong number of arguments in primitive function",e);
		       return p->first->second;
		     } else if (member(f,all_interfaces()))
		     { list<Expr>* r = args;
		       Schema s;
		       for(s = find_interface(f->name())->schema; s->more() && r->consp(); s=s->next(), r=r->tl)
			  if (!unify(r->hd,typecheck(r->hd,cvars,lvars),s->current()->second,lvars))
			    type_error("Incompatible types in constructor",r->hd);
		       if (r->consp() || s->more())
			  type_error("wrong number of arguments in constructor",e);
		       return f;
		     }
		     else if (member(f,Nil->cons(#<set>)->cons(#<bag>)->cons(#<list>)))
		     { Type tp = fresh_type_variable();
		       for(list<Expr>* r = args; r->consp(); r=r->tl)
			  if (!unify(r->hd,tp,typecheck(r->hd,cvars,lvars),lvars))
			     type_error("incompatible types in collection construction",r->hd);
		       return #<`f(`tp)>;
		     } else type_error("no such function",e);
		   };
  | `v => if (v->stringp())
	     return #<String>;
	  else if (v->integerp())
		  return #<Short>;
	  else if (v->variablep() && cvars->in(v->name()))
		  return cvars->find(v->name());
	  else if (v->variablep())
	          if (member(v,all_extents()))
	             return expand(v->name());
		  else type_error("Undefined variable",e);
	  else type_error("Unknown expression",e);
  #end;
} DEBUG(e);
};


Expr type_of ( Expr e, Schema vars ) {
  Schema lvars = new binding<Expr>;
  Schema cvars = vars;
  return typecheck(e,cvars,lvars);
};


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


bool extentp ( Expr x ) {
  if (x->variablep()) 
     return member(x,all_extents()) || DATABASE->extents->in(x->name());
 return false;
};


Expr get_extent ( Type tp ) {
  if (tp->variablep()) 
     if (member(tp,all_extents()))
	return variable(tp->name());
     else if (DATABASE->extents->in(tp->name()))
	return variable(DATABASE->extents->find(tp->name()));
  type_error("No such extent",tp);
};


Expr eliminate_type_vars ( Expr x ) {
  #case x
  |  ALPHA(`v,`m) => return m;
  | `f(...r) => { list<Expr>* args = Nil;
		  for(list<Expr>* s = r; s->consp(); s=s->tl)
		     args = args->cons(eliminate_type_vars(s->hd));
		  args = args->reverse();
		  Expr g = eliminate_type_vars(f);
		  return #<`g(...args)>;
		};
  | _ => return x;
  #end;
};