/* Unify.c *******************************************************************************

                                    The Anubis Compiler. 
                                   Unification of types. 

*****************************************************************************************/

#include "compil.h"

/* Environments are just A-lists ((v1 . T1) ...) where v_i are type unknowns and where T_i
   are  types.  The environment  just  tells  which type  unknowns  are  already bound  to
   types. */ 
   
/* We use an auxiliary function */ 
static int unify_aux(Expr x,               // first expression
                     Expr y ,              // second expression 
                     Expr *env);           // environment


/* 'depends_on' is used for circularity testing.  It returns 1 if 'y' contains a reference
   to 'x'. */ 
static int depends_on(Expr x,             // x is an unknown
                      Expr y,             // y is an expression 
                      Expr env)
{
  assert(is_unknown(x));           // only meaningful if 'x' is an unknown. 
  /* It is also assumed that 'x' is not a key of env. It is actually the case: check below
   all calls to 'depends_on'. */ 
   
 begin: 
  /* find if y  contains the unknown x. This is  relative to env: i.e. if  y is an unknown
     and y is bound in env, we must first replace y by its value.  */ 
  if (y == x) return 1;     
   
  if (is_unknown(y))
    {
      Expr yval = assoc(y,env);
      if (yval != key_not_found)
        { /* replace y by its value */ 
          y = yval; 
          goto begin;    // and restart
        }
    }

  if (!consp(y))  // y is a 'constant'
    return 0; 
  else
    {
      if (depends_on(x,car(y),env))
 return 1; 
      y = cdr(y); 
      goto begin; 
    }
}


/* Join two environments. */ 
Expr join_envs(Expr e1, Expr e2)
{
  Expr key, val, entry, val2; 

  while (consp(e1))
    {
      entry = car(e1); 
      key = car(entry);
      val = cdr(entry); 
      e1 = cdr(e1); 

      /* if 'key' is not  a key of e2, just add the entry to  e2. Otherwise, if the values
     of  'key'  in  e1   and  e2  do  not  unify  (with  envs   nil  and  e2),  return
     'not_unifiable'. If they unify, replace e2 by the result of this unification. */ 
      val2 = assoc(key,e2); 

      if (val2 == key_not_found)
 e2 = cons(entry,e2); 

      else 
 {
   e2 = unify(val,nil,val2,e2); 
   if (e2 == not_unifiable)
     {
       return e2; 
     }
 }
    }
  return e2; 
}



/* interface to unification */ 
Expr                /* returns a new environment */ 
_unify(Expr x,       /* first expression to unify */
       Expr ex,      /* environment for first expression */ 
       Expr y,       /* second expression to unify */ 
       Expr ey)      /* environment for second expression */ 
{
  Expr env, result; 
  int old_next_pair = next_pair; 

  /* the two environments must join together */ 
  if ((env = join_envs(ex,ey)) == not_unifiable) 
    return env; 

  if (unify_aux(x,y,&env))    /* unify and record instanciations in env */ 
    result = env; 
  else
    {
      next_pair = old_next_pair; 
      result = not_unifiable; 
    }
  return result;

}


/* the unification itself */ 
static int unify_aux(Expr x, 
       Expr y, 
       Expr *env)
{
  Expr aux; 
 begin:

  if (x == y)
    return 1; 

  if (is_unknown(x))
    {
      Expr v = assoc(x,*env); 
      if (v == key_not_found)  
 {
   /* x not instanciated */ 
   /* pairs ($x . $y) in env must always satisfy $x > $y */ 
   if (is_unknown(y) && x <= y)
     {
       /* exchange x and y, and try again */ 
       aux = x; 
       x = y; 
       y = aux; 
       goto begin; 
     }
   else
     {
       if (depends_on(x,y,*env)) 
  return 0; 
       else
  {
    *env = cons(cons(x,y),*env); 
    return 1; 
  }
     }
 }
      else
 {
   x = v; 
   goto begin; 
 }
    }

  if (is_unknown(y))
    {
      Expr v = assoc(y,*env); 
      if (v == key_not_found)
 {
   /* y not instanciated */ 
   {
     if (depends_on(y,x,*env))
       return 0; 
     else
       {
  *env = cons(cons(y,x),*env); 
  return 1; 
       }
   }
 }
      else
 {
   y = v; 
   goto begin; 
 }
    }

  if (!(consp(x) && consp(y)))
    return 0; 

  /* now x and y are pairs */ 
  if (!unify_aux(car(x),car(y),env))
    return 0; 

  /* the two heads have unified */ 
  x = cdr(x); 
  y = cdr(y);
  goto begin; 
}