unknowns.c 4.04 KB
/* unknowns.c *******************************************************

                        Anubis Web Server
                        Managing unknowns.

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

#include "compil.h"


/* testing if a term has unknowns */ 
int has_unknowns_aux(Expr term, Expr env)
{
  /* unknowns in term, which are keys of env are considered as
     implicitly replaced by their value (as found in env). */

 begin:
  if (is_unknown(term))
    {
      /* get its value */ 
      term = assoc(term,env); 
      if (term == key_not_found)
 /* unknown has no value */ 
 return 1; 
      else
 /* try again with the value */ 
 goto begin; 
    }

  else if (consp(term))
    {
      Expr car_term = car(term);
      if (car_term == anb_int32) return 0; 
      if (car_term == integer_10) return 0; 
      if (car_term == integer_16) return 0; 
      if (car_term == anb_int_10) return 0; 
      if (car_term == anb_int_16) return 0; 
      if (car_term == word_64) return 0; 
      if (car_term == word_128) return 0; 
      if (car_term == small_datum) return has_unknowns_aux(second(term),env); 
      if (has_unknowns_aux(car_term, env)) return 1; 
      return has_unknowns_aux(cdr(term),env);
    }
 
  else return 0; 
}


int has_unknowns(Expr term, Expr env)
{
  int result; 
   
  result = has_unknowns_aux(term,env);
   
  return result;  
}



/* testing if a term (given its list of interpretations) is non 
   ambiguous (error message if ambiguous) */ 
void must_be_non_ambiguous(Expr interps)
{
  /* interps is a list of interpretations. It must have length 1, and
     the unique interpretation must not contain uninstanciated
     internal type variables */ 

  int n = length(interps);      /* number of interpretations */ 

  if (n == 0)
    {
      /* No interpretation at all. Do not generate an error message,
  because there must be a subterm which has no interpretation,
  and which already generated an error message. */ 
      return;       
    }

  if (n >= 2)
    {
      err_line_col(car(cdr(car(car(interps)))),"E083", str_format(
       msgtext_ambiguous_term[0],
       length(interps))); 
      show_interpretations(errfile,interps); 
      return; 
    }

  /* now there is one and only one interpretation, but it may still be
     ambiguous, because it may contain an unknown */ 
  if (has_unknowns(car(car(interps)),
     cdr(car(interps))))
    {
      err_line_col(car(cdr(car(car(interps)))),"E084", 
       msgtext_term_with_unknowns[0]);
      show_interpretation(errfile,car(car(interps)),cdr(car(interps)));
      return; 
    }
}


/* refreshing an expression: replace all user type variables by fresh
   internal type variables */ 
Expr refresh(Expr expr,                 /* expression to refresh */ 
      Expr *already_refreshed)   /* (($T . $n) ...) */ 
{
  /* assert(!is_unknown(expr)); */ 

  /* type variables */ 
  if (is_user_type_variable(expr))
    {
      Expr replacement = assoc(expr,*already_refreshed); 
      if (replacement == key_not_found)
 {
   /* type variable not seen already */ 
   Expr result = fresh_unknown(); 
   *already_refreshed = cons(cons(expr,
      result),
        *already_refreshed); 
   return result; 
 }
      else
 {
   /* type variable already seen */ 
   return replacement; 
 }
    }

  if (consp(expr))
    {
      /* pairs */ 
      return cons(refresh(car(expr),already_refreshed),
    refresh(cdr(expr),already_refreshed)); 
    }
  else
    {
      /* other atoms */ 
      return expr; 
    } 
}

Expr merge_envs(Expr e1, Expr e2)
{
  /* verify that common keys in e1 and e2 have the same value, and put
     them only one time in result. Keep all other keys. */ 

  while (consp(e1))
    {
      if (is_key_of(e2,car(car(e1))))
        {  
 if (!equal(cdr(car(e1)),assoc(car(car(e1)),e2))) 
          {
            return not_unifiable;   /* cannot merge */ 
            debug(e1); 
            debug(e2); 
            internal_error("Should be equal",cons(cdr(car(e1)),assoc(car(car(e1)),e2))); 
          }
        }
      else
 e2 = cons(car(e1),e2); 
      e1 = cdr(e1); 
    }
  return e2; 
}