interp.c 169 KB

Edit Raw Blame History

/* interp.c *******************************************************

                       The Anubis Compiler.
                        Interpreting terms. 

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

#include <string.h>   
#include "compil.h"

#define dummy     nil
int show_errors = 1;

/* prototypes */


Expr symbol_interpretations         (Expr lc,
                                     Expr ttype,
                                     Expr name,
                                     Expr ctxt,
                                     Expr env);

Expr of_type_interpretations        (Expr lc,
                                     Expr ttype,
                                     Expr type,
                                     Expr term,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr lambda_interpretations         (Expr lc,
                                     Expr ttype,
                                     Expr fname,   /* name of function (nil if non recursive) */
                                     Expr args,
                                     Expr body,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr app_interpretations            (Expr lc,
                                     Expr ttype,
                                     Expr op,
                                     Expr args,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs,
                                     int allow_mvar_access);

Expr app_interpretations_1          (Expr lc,
                                     Expr op_int_head,
                                     Expr op_int_env,
                                     Expr args_ints,
                                     int allow_mvar_access);

Expr with_interpretations           (Expr keyword,
                                     Expr lc,
                                     Expr ttype,
                                     Expr symbol,
                                     Expr value,
                                     Expr body,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr cond_interpretations           (Expr lc,
                                     Expr ttype,
                                     Expr test,
                                     Expr clauses,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr select_cond_interpretations    (Expr lc,
                                     Expr test,
                                     Expr constructor_name,
                                     Expr typed_resurg,
                                     Expr case_body,
                                     Expr else_term,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr read_interpretations           (Expr lc,
                                     Expr ttype,
                                     Expr conn,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr write_interpretations          (Expr lc,
                                     Expr ttype,
                                     Expr conn,
                                     Expr value,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr exchange_interpretations       (Expr lc,
                                     Expr ttype,
                                     Expr conn,
                                     Expr value,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr wait_for_interpretations       (Expr lc,
                                     Expr ttype,
                                     Expr condition,
                                     Expr milliseconds,
                                     Expr after,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr delegate_interpretations       (Expr lc,
                                     Expr ttype,
                                     Expr delegated,
                                     Expr body,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr delegatep_interpretations      (Expr lc,
                                     Expr ttype,
                                     Expr priority,
                                     Expr delegated,
                                     Expr body,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr serialize_interpretations      (Expr lc,
                                     int allow_serialize_Opaque,
                                     Expr ttype,
                                     Expr datum,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr unserialize_interpretations    (Expr lc,
                                     int allow_serialize_Opaque,
                                     Expr ttype,
                                     Expr bytes,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr protect_interpretations        (Expr lc,
                                     Expr target_type,
                                     Expr term,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr lock_interpretations           (Expr lc,
                                     Expr target_type,
                                     Expr lockedfile,
                                     Expr term,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr alt_number_interpretations     (Expr lc,
                                     Expr target_type,
                                     Expr term,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr vcopy_interpretations          (Expr lc,
                                     Expr n,
                                     Expr init,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr bit_width_interpretations      (Expr lc,
                                     Expr type,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr load_adm_interpretations       (Expr lc,
                                     Expr name,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs);

Expr type_desc_interpretations       (Expr lc,
                                      Expr type,
                                      Expr ctxt,
                                      Expr env,
                                      Expr tvs);

Expr definition_of_type_interpretations   (Expr   lc,
                                           Expr   type_name,        /* term of type String */
                                           Expr   ctxt,
                                           Expr   env,
                                           Expr   tvs);

Expr definition_of_term_interpretations   (Expr   lc,
                                           Expr   type_term,      /* term of type AnubisType */
                                           Expr   term_name,      /* term of type String */
                                           Expr   ctxt,
                                           Expr   env,
                                           Expr   tvs);


/*
   *** How to expand conditionals with subcases. ***
   
   Conditionals needs to be expanded into a tree of conditionals without subcases. 
   
   The first  thing to do is to  gather cases/subcases belonging to  the same alternative.
   All cases/subcases from the same alternative form a 'case group'. A case group may have
   an  arbitrary number  of elements.   Case groups  are easily  established because  in a
   defined type,  not two alternatives may  have the same  name and same arity  (number of
   components).  This  is the job  of 'separate_case_groups'.  After this  separation each
   group must correspond to an alternative of the type of the test, and in the same order.

   A case group is represented by the list:
   
                                (<subcase 1> ... <subcase k>)
   
   where '<subcase i>' has the form:
   
                                     (<head> <lc> . <body>)
   
   as produced by the parser, where '<lc>' is the position of the keyword 'then'.

   Now, consider as an example, the following  case group, where the alternative is of the
   form 'a(U,Bool,Maybe(V))':
   
     a(x,false,failure)    then A
     a(x,false,success(y)) then B
     a(x,true ,z)          then C 
   
   Remark that the third component sometimes has 'heads' ('failure' and 'success(y)'), and
   sometimes has  'symbols' ('z'), while the  first component has only  symbols ('x'), and
   the second one has only heads ('false', 'true'). When symbols are used, always the same
   symbol must be used for the same component ('x' above appears three times).

   We have to  gather consecutive elements which may  be replaced by a single  one. In the
   case of the example, the first two elements may be gathered:
   
     a(x,false,z)         then if z is 
                               {
                                 failure    then A,
                                 success(y) then B
                               },
     a(x,true ,z)         then C

   Of course, we  use 'z' as the resurgent  symbol, since it is already used  in the third
   element of the case group.
   
   At that state, the last (third) component  has no more instances in the form of 'heads'
   (we have 'z'  everywhere). So, we consider the previous  (second) component and proceed
   the same way:
   
     a(x,\A31,z)            then if \A31 is 
                               {
                                 false    then if z is 
                                               {
                                                 failure    then A,
                                                 success(y) then B
                                               },
                                 true     then C
                               }
   
   and now there  are no more subcases  anywhere. Of course, if the  component (the second
   one in our example) is always an head, we have to introduce a new symbol (here '\A31'). 

   When we find  an head, the elements to  be gathered are not necessarily as  many as the
   number of alternatives the type of the component, because these heads may themselves be
   divided into subsubcases. Here is an example of this situation:
   
     [h . []]                   then A,
     [h . [i . []]]             then B,
     [h . [i . [j . t]]]        then C
   
   In this  case, the  second component has  three successive  'heads', the last  two ones
   corresponding to the second alternative of 'List(...)'. Hence the transformation gives:
   
     [h . \A31]  then if \A31 is 
                      {
                        [ ]             then A,
                        [i . []]        then B,
                        [i . [j . t]]   then C
                      }
   
   and the conditional just created also needs to be expanded (recursively). 
   
   Below is another example where the test is of type (Bool,Bool):
   
     (false, false)      then A,
     (false, true )      then B, 
     (true , false)      then C,
     (true,  true )      then D
   
   It is expanded in 3 steps:

   
   Step 1:
     (false, \A31)    then if \A31 is 
                           {
                             false then A,
                             true  then B
                           },
     (true , false)      then C,
     (true,  true )      then D
     
   Step 2:
     (false, \A31)    then if \A31 is 
                           {
                             false then A,
                             true  then B
                           },
     (true , \A31)    then if \A31 is 
                           {
                             false then C,
                             true  then D
                           }
   
   Step 3:
     (\A30, \A31)       then if \A30 is 
                        {
                          false then if \A31 is 
                                      {
                                        false then A,
                                        true  then B
                                      },
                          true  then if \A31 is 
                                      {
                                        false then C,
                                        true  then D
                                      }
                        }

   Notice that  in the case of a  single alternative in the  type of a component,  it is a
   little more difficult to find the last element to be gathered. For example:
   
     a(false, unique)   then A
     a(true,  unique)   then B
   
   must be expanded as follows:
   
   Step 1:
     a(false, \A31) then if \A31 is unique then A,
     a(true,  \A31) then if \A31 is unique then B
   
   Step 2:
     a(\A30 , \A31) then if \A30 is 
                    {
                      false then if \A31 is unique then A,
                      true  then if \A31 is unique then B
                    }
   
   Actually,  when we  are  gathering elements  considering  the k-th  component, all  the
   instances  (symbols  or  heads) in  these  elements  for  previous components  must  be
   identical. For example the following would generate an error:
   
     (false, false)     then A, 
     (true,  false)     then B, 
     (false, true)      then C, 
     (true,  true)      then D
   
   because of the first two elements whose first components are non identical. 
   
   
   So, the method for expanding a case group is the following:
   
   
   Preliminaries:
   
     1. Establish the list of resurgent symbols for  this case group. This is a mixture of
        symbols alreay present in the case group and new symbols '\A30', '\A31', ...
   
     2. Set a  column index 'ci'  to the  number of columns  (number of components  in the
        alternative corresponding  to the case  group).  The meaning  of this index  is as
        follow: all  columns starting  at number 'ci'  contain only resurgent  symbols (no
        heads).
   
   Main loop:
   
     1. If 'ci == 0' the job is finished (all heads in the case group have been expanded).
   
     2. Otherwise,  consider the column  'C' number  'ci -  1'. In  this column,  find the
        topmost case head.
   
        2.a. If there is no such case head, decrement 'ci' and restart the main loop. 
   
        2.b. Otherwise, get the alternatives of  the type of the component, and gather the
          elements of the  group, starting at the topmost head  found, checking that heads
          correspond  (name/arity) to the  alternatives, with  maybe several  elements per
          alternative, and that the instances of  components to the left of column 'C' are
          all identical. When these elements are gathered replace them by a single element
          whose body is a new conditional. Of  course, use the resurgent symbol got in the
          preliminaries.  Don't  expand this  new  conditional  (not  necessary for  depth
          recursion which will be handled by 'cond_interpretations').
       
        2.c Restart the main loop. 
   
   
   Now, we  have to  do this for  each case group.  When it's  done, we have  our expanded
   conditional.
   
 */


/* 
    Testing if a symbol  is the name of a singleton in a  defined type.  For example, this
    will answer '1' for 'true' of type 'Bool' and '0' for 'x' of type 'Bool'. This is used
    to decide if a  symbol found in a head of case in a  conditional is a resurgent symbol
    or a nested case head (corresponding to a singleton). 
 */
int is_singleton_name(Expr   lc,           // position of the conditional case
                      Expr   the_symbol,   // a Lisp string (actually a symbol from a head of case)
                      Expr   type,         // type of the symbol
                      Expr   env)          // environment for this type
{
  Expr alts;

  //printf("Entering is_singleton_name.\n"); fflush(stdout);
  assert(is_string(the_symbol));

  soft_dereference_type(type,env);
  if (!is_sum_type(type,env))
    {
      //printf("Leaving is_singleton_name (0).\n"); fflush(stdout);
      return 0;
    }

  alts = get_alts(type,env,lc);

  while(consp(alts))
    {
      Expr alt = car(alts);   /* (("name" ...) (<type> . <symbol>) ...) */
      if (cdr(alt) == nil && car(car(alt)) == the_symbol)
        {
          //printf("Leaving is_singleton_name (1).\n"); fflush(stdout);
          return 1;
        }

      alts = cdr(alts);
    }
  //printf("Leaving is_singleton_name (2).\n"); fflush(stdout);    
  return 0;
}


/* 
    Discriminate  between resurgent  symbols and  nested case  heads.  When  we  analyse a
    case/subcase head  we have  to decide  if an instance  of a  component is  a resurgent
    symbol or a nested case head.
 */
int is_nested_head (Expr    lc,      // position of case/subcase
                    Expr    x,       // either a resurgent symbol or a case head
                    Expr    type,    // the type of x
                    Expr    env)     // environment for this type
{
  /* x is either:
   
       - <string>                                singleton head or untyped resurgent symbol
       - (non_singleton_nested_head . <head>)    a non singleton nested head
       - (<type> . <string>)                     typed resurgent symbol
   */

  if (is_string(x))
    return is_singleton_name(lc,x,type,env);

  assert(consp(x));
  if (car(x) == non_singleton_nested_head)
    return 1;
  else
    return 0;
}


/* Check if a case/subcase is modeled on an alternative (same name, same arity) */
int modeled_on(Expr alt,                // alternative        ((<name> ...) . <components>)
               Expr the_head_of_case)   // head of case: one of:
                                        //      <string>
                                        //      (<string> . <operands>)
                                        //      (non_singleton_nested_head <string> . <operands>)
{
  Expr alt_name = car(car(alt));
  Expr case_name;

  /* a head of  case may be a  singleton. In that case it  is a string 'a',  but should be
     '(a)' instead. */
  if (is_string(the_head_of_case))
    the_head_of_case = list1(the_head_of_case);

  /* if needed, remove the tag 'non_singleton_nested_head' in front of the case head */
  if (consp(the_head_of_case) && car(the_head_of_case) == non_singleton_nested_head)
    the_head_of_case = cdr(the_head_of_case);

  case_name = car(the_head_of_case);

  if (alt_name != case_name)                    return 0;
  if (length(alt) != length(the_head_of_case))  return 0;
  return 1;
}


/* 
   The function  'make_case_groups' gets a list  of cases/subcases, and  separates it into
   the  corresponding  list  of case  groups.   This  operation  does  not need  any  type
   definition. It  is base only on the  names and arities of  cases/subcases. For example,
   the list of cases/subcases:
   
   (
     (("a" "g")                 <lc> . <body 1>)
     (("a" ("f" "u" "v" "w"))   <lc> . <body 2>)
     (("a" "x" "y")             <lc> . <body 3>)
     (("b" ("c" "z"))           <lc> . <body 4>)
   )
   
   corresponding to the conditional:
   
     if t is 
       {
         a(g)          then <body 1>,
         a(f(u,v,w))   then <body 2>,
         a(x,y)        then <body 2>,
         b(c(z))       then <body 3>
       }
   
   will be separated into:
   
   (
     ( // arity 1
        (("a" "g")                 <lc> . <body 1>)
        (("a" ("f" "u" "v" "w"))   <lc> . <body 2>)
     )
     ( // arity 2
        (("a" "x" "y")             <lc> . <body 3>)
     )
     (
        (("b" ("c" "z"))           <lc> . <body 4>)
     )
   )
    
   However, it is good for error generation to compare the list to the alternatives of the
   type of the test of the conditional.
   
 */
Expr make_case_groups(Expr     lc,       // position of whole conditional
                      Expr     alts,     // list of alternatives of type of test
                      Expr     cases)    // list of cases/subcases
{
  Expr result = nil;          // current state of result (reversed list of groups) 
  Expr group = nil;           // current state of current group (reversed list of cases)
  Expr last_used_alt = nil;   // last used alternative ('nil' when starting 
                              //      or corresponding to previous case)
  while(consp(cases))  // do for each case/subcase
    {
      Expr the_case = car(cases);   // the current case
      cases = cdr(cases);           // remaining cases
      if (last_used_alt != nil)
        { /* the current case is not the first case */
          if (modeled_on(last_used_alt,car(the_case)))
            { /* continue an already started case group */
              group = cons(the_case,group);   // construct the group (in reverse order)
            }
          else
            { /* start a new case group */
              if (alts == nil)
                {
                  if (show_errors)
                    {
                      err_line_col(lc,"E100",
                                   str_format(msgtext_too_many_subcases[0]));
                    }
                  return nil;
                }
              else
                {
                  /* record the group just constructed */
                  last_used_alt = car(alts);
                  alts = cdr(alts);
                  result = cons(reverse(group),result);   // record a whole group 
                  group = nil;

                  if (modeled_on(last_used_alt,car(the_case)))
                    {
                      group = cons(the_case,group);
                    }
                  else
                    {
                      if (show_errors)
                        {
                          err_line_col(second(the_case),"E101a",
                                       str_format(msgtext_invalid_subcase[0]));
                        }
                      return nil;
                    }
                }
            }
        }
      else
        { /* the current case is the first case */
          if (alts == nil)
            {
              if (show_errors)
                {
                  err_line_col(lc,"E101b",
                               str_format(msgtext_invalid_subcase[0]));
                }
              return nil;
            }
          else
            {
              last_used_alt = car(alts);   // record the current alternative
              alts = cdr(alts);            // other alternatives
              if (modeled_on(last_used_alt,car(the_case)))
                { /* begin the first group */
                  group = cons(the_case,group);
                }
              else
                { /* first case not modeled on first alternative */
                  if (show_errors)
                    {
                      err_line_col(lc,"E101c",
                                   str_format(msgtext_invalid_subcase[0]));
                    }
                  return nil;
                }
            }
        }
    }

  /* if there a group under construction, record it */
  if (consp(group))
    {
      result = cons(reverse(group),result);
    }

  if (alts != nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E099",
                       str_format(msgtext_not_enough_subcases[0]));
        }
      return nil;
    }

  return reverse(result);
}


/*  Making the list of resurgent symbols for  a an element in a case group.  This function
    takes a case/subcase, for example:
   
        a(b,y,c(z))  then <body>
   
   and tries to  determine the resurgent symbol used for each  component. In this example,
   assuming that 'b' is a singleton nested head, the result will be:
   
        (nil y nil)
   
   i.e. 'nil' is used when the symbol cannot be determined from this case. 
 */
Expr list_symbols_for_one_case(Expr alt,       // the alternative on which the case is modeled
                               Expr the_case,
                               Expr env)
{
  Expr lc, ops, result;

  /* the case is either      ((name op1 ...) <lc> . <body>) 
                     or      (name           <lc> . <body>)
   */

  lc = second(the_case);

  if (is_string(car(the_case)))
    ops = nil;
  else
    ops = cdr(car(the_case));   /* (op1 ...) */

  result = nil; // returns a list of the form (x nil ...)
                // i.e. with 'nil' when the component is not a resurgent symbol
  alt = cdr(alt);    // ((<type> . <sym or nil>) ...)
  /* construct the result in reverse */
  while(consp(ops))
    {
      Expr op1   = car(ops);
      Expr type1 = car(car(alt));

      if (!is_nested_head(lc,op1,type1,env))
        {
          if (is_string(op1))
            result = cons(op1,result);
          else
            result = cons(cdr(op1),result);   // op1 is (<type> . <sym>)
        }
      else
        {
          result = cons(nil,result);
        }
      alt = cdr(alt);
      ops = cdr(ops);
    }
  return reverse(result);
}


/* Merging two lists of resurgent symbols for  elements of the same group. For example, it
   gives:
   
      merge( (x nil z   nil),
             (x y   nil nil)) 
         =   (x y   z   nil)
   
   At the  same type we  may check that  the same symbol appears  at the same  places. For
   example,
   
      merge((x, ...),(y, ...))
   
   will produce an error (actually the tag 'invalid') if x != y.
 */
Expr merge_case_symbols(Expr lc,    // position of second element of case group
                        Expr l1,    // the two lists are assumed of the same length
                        Expr l2)
{
  Expr result = nil;

  while(consp(l1))
    {
      assert(consp(l2));
      if (car(l1) == nil)    // (nil,y) |-> y   (nil,nil) |-> nil
        {
          result = cons(car(l2),result);
        }
      else   //  (x,x) |-> x    (x,y) |-> error (actually 'invalid')
        {
          if (car(l2) == nil)    // the second one may be 'nil'
            result = cons(car(l1),result);
          else if (car(l1) == car(l2))
            result = cons(car(l1),result);   // both are symbols
          else
            {
              if (show_errors)
                {
                  err_line_col(lc,"E102",
                               str_format(msgtext_non_equal_resurgents[0],
                                          string_content(car(l1)),
                                          string_content(car(l2))));
                }
              return invalid;
            }
        }
      l1 = cdr(l1);
      l2 = cdr(l2);
    }
  assert(!consp(l2));

  return reverse(result);
}


/* Generating a fresh resurgent symbol. */
U32 resurgent_symbols_counter = 0;
char frsbuf[20];
Expr fresh_resurgent_symbol(void)
{
  resurgent_symbols_counter++;
  sprintf(frsbuf,"+++fresh%d",(int)resurgent_symbols_counter);
  return new_string(frsbuf);
}


/* 
    Making the list of  resurgent symbols for a case group. May  return 'invalid'. Here we
    construct  the  complete list  of  resurgent symbols  for  a  group of  cases/subcases
    corresponding to a given alternative of the type of the test.
   
    In a first step we collect the symbols  for each case in the group, and merge them. At
    the end some symbols may be not determined (there are still occurences of 'nil' in the
    result). We replace these 'nil' by fresh resurgent symbols. 
 */
Expr list_case_group_resurgents(Expr alt,
                                Expr group,
                                Expr env)
{
  Expr result, aux;

  /* do for the first element */
  assert(consp(group));  // a group is always non empty
  result = list_symbols_for_one_case(alt,
                                     car(group),  // resurgents or heads 
                                     env);

  group = cdr(group);

  /* do for other elements */
  while(consp(group))
    {

      result = merge_case_symbols(second(car(group)),   // lc
                                  result,
                                  list_symbols_for_one_case(alt,
                                                            car(group),
                                                            env));

      if (result == invalid) return invalid;
      group = cdr(group);
    }

  /* replace all occurences of nil by fresh resurgent symbols */
  aux = result;
  result = nil;

  while(consp(aux)) // this will reverse the result
    {
      if (car(aux) == nil)
        result = cons(fresh_resurgent_symbol(),result);
      else
        result = cons(car(aux),result);
      aux = cdr(aux);
    }


  return reverse(result);
}


/*  
    Expand a subgroup into a single element.  We have a subgroup at hand, i.e. consecutive
    elements in a group,  with the same components in the first  k columns and nested case
    heads in the k-th column. For example:
   
     [h . []]                   then A,
     [h . [i . []]]             then B,
     [h . [i . [j . t]]]        then C

   where the common components are just 'h', and the nested heads are:
   
          []
          [i . []]
          [i . [j . k]]
   
   We also got the resurgent symbol (say \A31)  of the k-th column. We have to tranform this
   subgroup into a single case like this one:
   
     [h . \A31] then if \A31 is 
                  {
                    []              then A,
                    [i . []]        then B,
                    [i . [j . k]]   then C
                  }
   
   
 */
Expr expand_to_single(Expr    lc,         // position of the first element in the subgroup
                      Expr    subgroup,   // the subgroup itself  
                      Expr    resurg,     // the resurgent symbol
                      int     column)     // the column concerned by this operation
{
  Expr new_cases = nil;    // list of cases/subcases in the newly generated conditional
  Expr aux = subgroup;
  Expr alt_name = car(car(car(subgroup)));       // name of alternative
  Expr first_comps = cdr(car(car(subgroup)));    // components in the first case
  Expr new_head = nil;
  int i;

     /* Make the cases of the new conditional */
  while(consp(aux))
    {
      Expr the_case = car(aux);   // ((name op1 ...) <lc> . <body>)
      Expr nested_head = nth(new_integer(column-1),cdr(car(the_case)));

      /* if needed, remove 'non_singleton_nested_head' before unnesting the head */
      if (consp(nested_head) && car(nested_head) == non_singleton_nested_head)
        nested_head = cdr(nested_head);

      /* if the head is a string "a", replace it by ("a") */

      if (is_string(nested_head))
        nested_head = list1(nested_head);

      new_cases = cons(cons(nested_head,
                            cdr(the_case)),           // keep the same position and body
                       new_cases);
      aux = cdr(aux);
    }

  /* Make a  copy of the  head of the  first case, with the  resurgent symbol in  the k-th
   column. */
  aux = first_comps;   // (op1 ...)
  i = 0;
  while(consp(aux))
    {
      if (i != column-1)
        new_head = cons(car(aux),new_head);
      else
        new_head = cons(resurg,new_head);
      aux = cdr(aux);
      i++;
    }
  new_head = cons(alt_name,reverse(new_head));   // this is (for example) '[h . \A31]'
  /* construct the conditional and the new main case. */

  return mcons3(new_head,       // for example [h . \A31]
                lc,             // position of first case in the subgroup
                mcons4(cond,                      // the new (nested) conditional 
                       lc,                        // always the same position
                       mcons3(symbol,lc,resurg),  // the resurgent symbol as a term
                       reverse(new_cases)));
}


/*  Performing the expansion of a case group in a given column. 
 */
Expr expand_case_group_one_column(Expr group,
                                  Expr type,        // type of this column
                                  Expr type_alts,   // alternatives for this type
                                  Expr rsym,        // resurgent symbol for this column
                                  int column,       // column number 
                                  Expr env)
{
  Expr past_elements = nil;    // elements already seen (in reverse order)
  Expr the_case = nil;
  Expr components, components_to_the_left;
  Expr to_be_expanded;
  Expr aux, last_alt_seen;

  assert(consp(group));

 begin:

  /* skip elements with a resurgent symbol in the given column */
  while(consp(group))
    {
      the_case = car(group);

      if (is_nested_head(second(the_case),                 // position of this case/subcase
                         nth(new_integer(column-1),cdr(car(the_case))), // resurgent symbol or nested head
                         type,                             // type of this column
                         env))
        {
          break; // found the first nested head
        }
      else
        {
          past_elements = cons(the_case,past_elements);
          group = cdr(group);
        }
    }

  if (!consp(group)) // no nested head found in this column
    {
      return reverse(past_elements);
    }

  /* The first nested head  has been found.  We record the instances  of components on the
     left of our  column. They must be the  same for all following elements  until we have
     finished with the alternatives of the type of the column. */
  components = cdr(car(the_case));
  components_to_the_left = first_elements(new_integer(column-1),components);   // defined in 'expr.cpp'
  /* Extract the elements to be expanded (maybe we should say 'reduced' ?) into a single case */
  to_be_expanded = list1(the_case);
  group = cdr(group);
  aux = type_alts;
  last_alt_seen = car(aux);
  aux = cdr(aux);
  while(consp(group))
    {
      Expr element = car(group);       /* ((name comp1 ...) <lc> . <body>) */
      Expr comps = cdr(car(element));  /* (comp1 ...) */

      /* stop collecting elements if components on the right are changing */
      if (!equal(components_to_the_left,
                 first_elements(new_integer(column-1),comps)))
        {
          /* The  components  to the  left  have  changed: check  that  we  have used  all
             alternatives from the type of the column */
          if (!(aux == nil  ||
                (cdr(aux) == nil && !equal(car(aux),last_alt_seen))
               ))
            {
              if (show_errors)
                {
                  err_line_col(second(element),"E103",
                               str_format(msgtext_not_enough_subcases[0]));
                }
              return nil;
            }
          else
            { /* the subgroup is complete (without the current element) */
              break;
            }
        }
      else
        { /* components to the left are equal to the previous ones */
          if (modeled_on(last_alt_seen,nth(new_integer(column-1),comps)))
            { /* the component matches the current alternative */
              to_be_expanded = cons(element,to_be_expanded);
              group = cdr(group);
            }
          else
            { /* the component does'nt match the current alternative */
              if (aux == nil)
                {
                  if (show_errors)
                    {
                      err_line_col(second(element),"E104",
                                   str_format(msgtext_too_many_subcases[0]));
                    }
                  return nil;
                }
              else
                {
                  last_alt_seen = car(aux);
                  aux = cdr(aux);
                  if (modeled_on(last_alt_seen,nth(new_integer(column-1),comps)))
                    {
                      to_be_expanded = cons(element,to_be_expanded);
                      group = cdr(group);
                    }
                  else
                    { /* the element  does neither match the new  current alternative, nor
                         the previous one. */
                      if (show_errors)
                        {
                          err_line_col(second(element),"E105",
                                       str_format(msgtext_nested_head_doesnt_match_next_alt[0],column));
                        }
                      return nil;
                    }
                }
            }
        }
    }

  /* expand the selected elements into a single element */
  to_be_expanded = reverse(to_be_expanded);
  past_elements = cons(expand_to_single(second(car(to_be_expanded)),   // lc
                                        to_be_expanded,                // the subgroup 
                                        rsym,       // resurgent symbol for this column
                                        column),
                       past_elements);

  /* if there are still elements continue from the beginning. */
  if (consp(group)) goto begin;
  /* otherwise return the result in the right order */
  return reverse(past_elements);
}


/* Expanding a case group completely */
Expr expand_case_group(Expr    group,      // the case group
                       Expr    alt_tail,   // the corresponding alternative tail (components)
                       Expr    rsym_list,  // list of resurgent symbols
                       Expr    env)
{
  int column = length(alt_tail);    // column counter
  assert(group != nil);

  while(column > 0)
    {
      Expr type = car(nth(new_integer(column-1),alt_tail));  // type for this column
      group = expand_case_group_one_column(group,
                                           type,
                                           get_alts(type,env,second(car(group))),
                                           nth(new_integer(column-1),rsym_list),
                                           column,
                                           env);
      column--;
      if (group == nil) return nil; // an error was detected
    }
  return group;
}


/* 
    Expanding (at first level only) a  conditional with subcases (i.e.  with strictly more
    cases than the number of alternatives in the type of its test).
  
    There is no need to expand more than the first level, because after the expansion, the
    expanded conditional  is passed  to the normal  circuit of conditional  checking. This
    will call  'expand_conditional' again if  needed. Notice that  'expand_conditional' is
    called only  when the number of  cases in a  conditional is strictly greater  than the
    number of alternatives in the type of the test.
   
  */
Expr expand_conditional(Expr     lc,            // position of conditional
                        Expr     alts_of_test,  // alternatives of the type of the test
                        Expr     the_test,      // the test itself (a term)
                        Expr     cases,         // list of case/subcases
                        Expr     env)
{
  Expr groups = make_case_groups(lc,alts_of_test,cases);
  Expr new_cases = nil;

  if (groups == nil) return nil;   // an error was detected
  /* handle each case group */
  while(consp(groups))
    {
      Expr group = car(groups);
      Expr new_cases1;
      Expr alt = car(alts_of_test);
      Expr resurgents = list_case_group_resurgents(alt,group,env);

      if (resurgents == invalid) return nil;

      new_cases1 = expand_case_group(group,
                                     cdr(alt),
                                     resurgents,
                                     env);

      //if (length(group) > 1) anb_exit(1);
      if (new_cases1 == nil) return nil;
      new_cases = append(new_cases1,new_cases);
      groups = cdr(groups);
      alts_of_test = cdr(alts_of_test);
    }

  /* make the new conditional */
  return mcons4(cond,
                lc,
                the_test,
                reverse(new_cases));
}


/* 
    We   have  not  finished   with  subcases   since  we   must  also   handle  selective
    conditionals. For example, if we have:
   
      if t is [h . [u . [ ]]] then A else B
   
   we would at first glance expand it into:
   
      if t is [h . \A31] then 
        if \A31 is [u . \A32] then 
          if \A32 is [ ] then A
          else B 
        else B
      else B
   
   Of  course,  the problem  comes  from  the fact  that  B  is  duplicated maybe  several
   times. This is a problem if the code for B is big.
   
   The solution is to expand as follows:
   
   if (if t is [h . \A31] then 
         if \A31 is [u . \A32] then 
           if \A32 is [ ] then success(A)
           else failure
         else failure
       else failure) is
     {
       failure    then B, 
       success(a) then a
     }
     
   In order to  do this, what do we need ?  First of all, we have to  detect the fact that
   the head contains nested heads. To that end we need the type of the test. 
   
   In order to avoid generating a new surrounding 'if':
   
   if ... is 
     {
       failure    then B,
       success(a) then a
     }
   
   at each depth level, we actually expand in the form of:
   
       if t is [h . \A31] then 
         if \A31 is [u . \A32] then 
           if \A32 is [ ] then success(A)
           else failure
         else failure
       else failure   
   
   and  only at  the  end of  this  process we  envelop the  result  into the  surrounding
   conditional. Notice that if we proceed only one depth level on our example, we get:
   
      if t is [h . \A31] then 
        if \A31 is [u . []] then success(A) 
        else failure
      else failure
   
   So, in order to avoid  repeating the 'success(A)' (generating a 'success(success(A))'),
   we use a (fresh) marker for A: \A3A
   
      if t is [h . \A31] then 
        if \A31 is [u . []] then \A3A
        else failure
      else failure
   
   so that the second expansion gives:
   
      if t is [h . \A31] then 
        if \A31 is [u . \A32] then 
          if \A32 is [] then \A3A
          else failure
        else failure
      else failure
   
   At the end, we just have to replace the marker by 'success(A)', and put the envelop. 
   
   As an exempla, here is how
   
      if t is (true,false) then A else B 
   
   will be expanded:
   
   Step 1:
      if t is (true,\A31) then
        if \A31 is false then \A3A
        else failure
      else failure
   
   Step 2:
      if t is (\A30,\A31) then
        if \A30 is true then 
          if \A31 is false then \A3A
          else failure
        else failure
      else failure
   
   Step 3:
    if (if t is (\A30,\A31) then
          if \A30 is true then 
            if \A31 is false then success(A)
            else failure
          else failure
        else failure) is 
      {
        failure then B,
        success(_) then _
      }
   
 */


/* Testing for variable hiding (when strong preemption is forbidden) */
static Expr    /* Returns the list of entries of the context which are hidden by 'name'. */
get_hidden_entries (Expr name,
                    Expr ctxt)
{
  Expr result = nil;

  if (name == pdstr__) return nil;   /* allow hidding for '_' */

   /* ctxt = ((<symbol> . <type>) ...)   or 
      ctxt = ((f_micro_ctxt <fname> <ftype> (<symbol> . <type>) ...) ...) */

  while(consp(ctxt))
    {
      Expr entry = car(ctxt);

      if (car(entry) == f_micro_ctxt)
        {
          ctxt = cdr3(entry);
          continue;
        }

      assert(is_string(car(entry)));
      if (car(entry) == name)
        {
          result = cons(entry,result);
        }

      ctxt = cdr(ctxt);
    }

  return reverse(result);
}


/* An index (hash-table) for quickly interpreting symbols. */

SymbolIndexArray symbol_index[256];

void init_symbol_index(void)
{
  int i;
  for (i = 0; i < 256; i++)
    {
      symbol_index[i].max = 100;
      symbol_index[i].next = 0;
      symbol_index[i].array = (SymbolIndexEntry *)mallocz(100*sizeof(SymbolIndexEntry));
    }
}


U8 u8_symbol_hash(Expr x)
{
  int i = 0;
  U8 *s;
  U8 result = 0;

  assert(is_string(x));
  s = (U8 *)string_content(x);
  while (s[i] != 0)
   {
     result += s[i];
     i++;
   }
  return result;
}


/* Adding an entry */
void _add_symbol_index_entry(Expr symbol, SymbolSort sort, int index)
{
  U8 hash;
  U32 next;
  SymbolIndexEntry *array;

  hash = u8_symbol_hash(symbol);
  next = symbol_index[hash].next;
  array = symbol_index[hash].array;
  if (symbol_index[hash].next >= symbol_index[hash].max)
    {
      //printf("Enlarging array for hash %d in symbol index.\n",hash); 
      symbol_index[hash].max += 100;
      symbol_index[hash].array = reallocz(array,(symbol_index[hash].max)*sizeof(SymbolIndexEntry));
      array = symbol_index[hash].array;
    }
  array[next].symbol = symbol;
  array[next].sort = sort;
  array[next].index = index;
  (symbol_index[hash].next)++;
}


static Expr signature_from_type(Expr type, Expr env)
{

  /* dereference type */
  while (is_unknown(type))
    {
      type = assoc(type,env);
      assert(type != key_not_found);
    }

  if (consp(type))
    switch(car(type))
      {
      case functype:
 return second(type);
      }

  return nil;  /* because T is the same as () -> T */
}


/* The  next function  receives a  list  of interpretations,  and selects  among them  the
   interpretation whose type is  given by the pair (type,env). If it  does not exist or if
   there are several of them, an error  message is sent, and 'nil' is returned. Otherwise,
   the unique interpretation found is returned in the form (head,env).
*/

Expr select_unique_interpretation(Expr lc,
                                  Expr interps,
                                  Expr type,
                                  Expr env)
{
  Expr typed_interps = nil;
  Expr aux;

  aux = interps;
  while (consp(aux))
    {
      Expr interp = car(aux);
      if (same_type(type_from_interpretation(car(interp),cdr(interp)),cdr(interp),type,env))
        typed_interps = cons(interp,typed_interps);
      aux = cdr(aux);
    }

  if (typed_interps == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E012",
                       msgtext_no_interp_of_type[0]);
          show_type(errfile,type,env);
          fprintf(errfile,"%s",
                  msgtext_no_interp_of_type2[0]);
          show_interpretations_types(errfile,interps);
        }
      return nil;
    }

  if (length(typed_interps) >= 2)
    {
      if (show_errors)
        {
          err_line_col(lc,"E013",
                       msgtext_several_interps_of_type[0]);
          show_interpretations_types(errfile,typed_interps);
        }
      return nil;
    }

  return car(typed_interps);
}


const char *special_type_scheme_name(Expr type_ind)
{
  switch(type_ind)
    {
    default:
      assert(0);
      return NULL;
    }
}


Expr select_special_interpretation(Expr lc,
                                   Expr interps,
                                   Expr type_ind)
{
  Expr typed_interps = nil;
  Expr aux;

  aux = interps;
  while (consp(aux))
    {
      Expr interp = car(aux);
      Expr type = type_from_interpretation(car(interp),cdr(interp));
      if (consp(type) && car(type) == type_ind)
        typed_interps = cons(interp,typed_interps);
      aux = cdr(aux);
    }

  if (typed_interps == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E014",
                       msgtext_no_interp_of_type[0]);
          fprintf(errfile,"%s",special_type_scheme_name(type_ind));
          show_interpretations_types(errfile,interps);
        }
      return nil;
    }

  if (length(typed_interps) >= 2)
    {
      if (show_errors)
        {
          err_line_col(lc,"E015",
                       msgtext_several_interps_of_type[0]);
          show_interpretations_types(errfile,typed_interps);
        }
      return nil;
    }

  return car(typed_interps);
}


/********************* Interpreting terms ************************************/


/* Interpreting operations (and variable names) */

static Expr                              /* <operation interpretations> */
operation_interpretations(Expr lc,       /* <lc> */
                          Expr type,     /* required type for operation */
                          Expr name,     /* <operation name> */
                          Expr env)
{
  int i, h;
  Expr op_ints_result = nil;
  Expr already_refreshed, signature, opttype, parms;
  U8 hash = u8_symbol_hash(name);
  SymbolIndexEntry *hash_array = symbol_index[hash].array;
  U32 max_hash = symbol_index[hash].next;

  assert(consp(lc));
  assert(is_string(name));

  /* explore array of operations for the given hash */
  for (h = 0; h < (int)max_hash; h++)
    //for (i = 0; i < next_operation; i++)
    {
      if (hash_array[h].sort != syms_operation) continue;
      i = hash_array[h].index;
      /* consider only operations with the right name and not private to another file */
      if ( !((operations[i].global)&op_public) &&
            strcmp(current_file_abs_path,string_content(operations[i].abs_file_path)))
        continue;

      /* if the operation is the last one and is either macro or inline, ignore it 
         (this forbids recursive macro/inline). */
#if 0         
      if (   (i+1 == next_operation)
          && (((operations[i].global)&inline_mask) || ((operations[i].global)&macro_mask))
         ) continue; 
#endif
      /* in case of option '-read1' avoid invisible file names */
      if ( read1 && !(is_visible(string_content(operations[i].abs_file_path))))
        continue;

      if (member(name,operations[i].names))
        {
          /* get a refreshed signature of operation */
          already_refreshed = nil;
          signature = refresh(operations[i].signature,&already_refreshed);

          /* get a refreshed target type of operation */
          opttype = refresh(operations[i].target_type,&already_refreshed);

          /* get a refreshed list of parameters */
          parms = refresh(operations[i].parms,&already_refreshed);

          /* TODO: the type found for the operation must match the
             required type, otherwise, it is not recorded. */

          /* record this interpretation */
          op_ints_result = cons(cons(mcons7(operation,
                                            lc,
                                            new_integer(i),
                                            name,
                                            parms,
                                            opttype,
                                            signature),
                                     env),
                                op_ints_result);
        }
    }


  /* get also interpretations as global variable */
  for (h = 0; h < (int)max_hash; h++)
  //for (i = 0; i < next_variable; i++)
    {
      if (hash_array[h].sort != syms_variable) continue;
      i = hash_array[h].index;
         /* consider only variables with the right name and not private to another file */
      if ( !((variables[i].global)&op_public) &&
            strcmp(current_file_abs_path,string_content(variables[i].abs_file_path)))
        continue;

      /* in case of option '-read1' avoid invisible file names */
      if ( read1 && !(is_visible(string_content(variables[i].abs_file_path))))
        continue;

      if (name == variables[i].name)
 op_ints_result = cons(cons(mcons3(global_variable,lc,new_integer(i)),
       nil),
         op_ints_result);
    }

  /* if no match found, the operation is unknown */
  if (op_ints_result == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E016", str_format(
                                             msgtext_unknown_symbol[0],
                                             string_content(name)));
        }
    }

  /* in any case, return the list of interpretations */
  return op_ints_result;
}


/* interpreting a tuple of terms */
static
Expr /* returns a list of tuple interpretations */
tuple_interpretations(Expr ttypes,    /* required types */
                      Expr terms,     /* terms to be interpreted */
                      Expr ctxts,     /* list of contexts */
                      Expr env,       /* environment */
                      Expr tvs,       /* user type variable list */
                      int same_types) /* if 1 keep only those interpretations where the
                                         elements of the tuple may have the same type. */
{
  Expr result = nil;
  Expr first, aux;
  Expr first_int, first_env;
  Expr others_int, others_env;
  Expr others;

  assert(length(terms) == length(ctxts));

  if (terms == nil)
    {
      /* no term to  interpret, return ((() .  env)) (there is  only one interpretation of
         the empty tuple) */

      result = list1(cons(nil,env));
    }
  else
    {
      /* get all interpretations of first term */
      first =
        term_interpretations(dummy,car(terms),car(ctxts),env,tvs,0);
      if (first == nil) return nil;


      /* get all interpretations of other terms */
      others = tuple_interpretations(dummy,
                                     cdr(terms),
                                     cdr(ctxts),
                                     env,
                                     tvs,
                                     same_types);

      if (others == nil) return nil;


      /* construct interpretations of original tuple:  for each interpretation (I1 . e) of
         first, and each interpretation ((I2 ... Ik) . e') of others, construct:

         ((I1 I2 ... Ik) . e'')

         where e'' is obtained by merging e and e' */
      while (consp(first))
        {
          first_int = car(car(first));
          first_env = cdr(car(first));

          aux = others;

          while (consp(aux))
            {
              Expr new_env;

              others_int = car(car(aux));
              others_env = cdr(car(aux));

              new_env = join_envs(first_env,others_env);

              /* others_int may be 'nil'. */

              if (new_env != not_unifiable)
                {
                  if (same_types && consp(others_int))
                    {
                      Expr e = unify(type_from_interpretation(first_int,first_env),
                                     new_env,
                                     type_from_interpretation(car(others_int),others_env),
                                     nil);
                      if (e != not_unifiable)
                        {
                          result = cons(cons(cons(first_int,
                                                  others_int),
                                             e),
                                        result);
                        }
                    }
                  else
                    {
                      result = cons(cons(cons(first_int,
                                              others_int),
                                         new_env),
                                    result);
                    }
                }
              aux = cdr(aux);
            }
          first = cdr(first);
        }
    }

  return result;
}


int word32_value(Expr bigits) /* transform a sequence of bigits in basis 256 into a word32 */
{
  /* the result must fits into 32 bits */
  int result = 0;
  while(consp(bigits))
    {
      result = result << 8;
      result += integer_value(car(bigits));
      bigits = cdr(bigits);
    }
  return result;
}


/* interpreting a term */
Expr                /* returns a list of interpretations */
term_interpretations(Expr ttype,      /* required type for that term (may contain unknowns) */
                     Expr term,       /* <term> */
                     Expr ctxt,       /* <context> */
                     Expr env,        /* <environment> */
                     Expr tvs,        /* user type variable list */
                     int allow_mvar_access)   /* if non zero, allow pseudo-terms mv(i) */
{
  Expr result = nil;


 begin:


  switch (car(term))
    {

    case alt_number: /* (alt_number <lc> . <term>) */
      {
        result = alt_number_interpretations(second(term),
                                            dummy,
                                            cdr2(term),
                                            ctxt,
                                            env,
                                            tvs);
      }
      break;

    case protect: /* (protect <lc> . <term>) */
      {
        result = protect_interpretations(second(term),
                                         dummy,
                                         cdr2(term),
                                         ctxt,
                                         env,
                                         tvs);
      }
      break;

    case lock: /* (lock <lc> <term> . <term>) */
      {
        result = lock_interpretations(second(term),
                                      dummy,
                                      third(term),
                                      cdr3(term),
                                      ctxt,
                                      env,
                                      tvs);
      }
      break;

    case alert: /* (alert <lc> . <file name>) */
      {
        /* equivalent to the term: alert_handler(file_name,line,column), 
           with unknown type. */
        Expr lc = second(term);

        term = list6(app,
                     lc,
                     mcons3(symbol,lc,pdstr_alert_handler),
                     mcons3(string,lc,cdr2(term)),
                     list3(integer_10,lc,new_integer(line_in(lc))),
                     list3(integer_10,lc,new_integer(col_in(lc))));

        goto begin;
      }
      break;

    case todo:  /* (todo <lc> <file name> . <text>) */
      {
        Expr lc = second(term);
        Expr fn = third(term);
        Expr tx = cdr3(term);

        term = list7(app,
                     lc,
                     mcons3(symbol,lc,pdstr_todo_handler),
                     mcons3(string,lc,fn),
                     list3(integer_10,lc,new_integer(line_in(lc))),
                     list3(integer_10,lc,new_integer(col_in(lc))),
                     mcons3(string,lc,tx));
        goto begin;
      }
      break;

    case debug_avm: /* (debug_avm <lc> . <term>) */
      {
        Expr interps = term_interpretations(ttype,cdr2(term),ctxt,env,tvs,0);
        result = nil;
        while (consp(interps))
          {
            result = cons(cons(mcons3(debug_avm,
                                      second(term),
                                      car(car(interps))),
                               cdr(car(interps))),
                          result);
            interps = cdr(interps);
          }
      }
      break;

    case terminal: /* (terminal <lc> . <term>) */
      {
        Expr interps = term_interpretations(ttype,cdr2(term),ctxt,env,tvs,0);
        result = nil;
        while (consp(interps))
          {
            result = cons(cons(mcons3(terminal,
                                      second(term),
                                      car(car(interps))),
                               cdr(car(interps))),
                          result);
            interps = cdr(interps);
          }
      }
      break;


    case integer_10:
    case integer_16:
      {
        /* (integer_10 <lc> bigit ... bigit) */
        /* (integer_16 <lc> bigit ... bigit) */
        /* in both cases, the bigits are in basis 256 */

        Expr bigits = cdr2(term); /* (bigit ... bigit) */
        result = nil;

#if 0 
   Int32 is obsolete
        if ((length(bigits) < 4)
            || ((length(bigits) <= 4) && integer_value(car(bigits)) < 128))
          {
            /* (positive) number less than 2^31: add an interpretation as 'Int32' */
            result = cons(cons(mcons3(anb_int32,second(term),int32_value(bigits)),env),
                          result);
          }
#endif
        /* add an interpretation as 'Int' */
        result = cons(cons(cons(car(term) == integer_10 ? anb_int_10 : anb_int_16, cdr(term)),env),
                      result);

        /* add an interpretation as Float */
        result = cons(cons(mcons4(fpnum,second(term),new_integer(word32_value(bigits)),new_integer(0)),
                           env),
                      result);

        /* Interpretations  as words:  First compute  the interpretation  as  Word128, and
           reduce it modulo the other sizes. */
        {
          Expr bgts = bigits;
          U32 word3, word2, word1, word0;   /* 32 bits words of 128 bits word (most significant first) */

          /* Keep only the 16 least significant (basis 256) bigits */
          while (length(bgts) > 16) { bgts = cdr(bgts); }
          /* Add leading zeros if needed */
          while (length(bgts) < 16) { bgts = cons(new_integer(0),bgts); }
          /* At this point 'bgts' has 16 bigits. */
          assert(length(bgts) == 16);

          /* compute the 4 32 bits words */
          word3 = word32_value(first_elements(new_integer(4),bgts));
          bgts = cdr4(bgts);
          word2 = word32_value(first_elements(new_integer(4),bgts));
          bgts = cdr4(bgts);
          word1 = word32_value(first_elements(new_integer(4),bgts));
          bgts = cdr4(bgts);
          word0 = word32_value(first_elements(new_integer(4),bgts));

          /* make the Word128 interpretation */
          result = cons(cons(mcons5(word_128,word0,word1,word2,word3),env),result);
          /* make the Word64 interpretation */
          result = cons(cons(mcons3(word_64,word0,word1),env),result);
          /* make the Word32 interpretation */
          result = cons(cons(mcons3(small_datum,pdstr_Word32,(word0&0xFFFFFFFF)),env),result);
          /* make the Word16 interpretation */
          result = cons(cons(mcons3(small_datum,pdstr_Word16,(word0&0xFFFF)),env),result);
          /* make the Word8 interpretation */
          result = cons(cons(mcons3(small_datum,pdstr_Word8,(word0&0xFF)),env),result);
          /* make the Word4 interpretation */
          result = cons(cons(mcons3(small_datum,pdstr_Word4,(word0&0xF)),env),result);
        }
      }
      break;


    case fpnum:
      /* (fp <lc> . <word32 mantissa> . <word32 exponent>) */
      result = list1(cons(term,env));
      break;

    case symbol:
      /* (symbol <lc> . <string>) */
      term = cdr(term);
      result = symbol_interpretations(car(term),   /* <lc> */
                                      dummy,
                                      cdr(term),   /* <string> */
                                      ctxt,
                                      env);
      break;

#if 0
    case local: 
      /* (local <string> <depth> . <type>) */ 
      result = term; 
      break; 
#endif
    case of_type:
      /* (of_type <lc> <type> . <term>) */
      term = cdr(term);
      result = of_type_interpretations(car(term),       /* <lc> */
                                       dummy,
                                       car(cdr(term)),  /* <type> */
                                       cdr(cdr(term)),  /* <term> */
                                       ctxt,
                                       env,
                                       tvs);
      break;

    case constructor:
      result = list1(cons(term,env));
      break;


    case lambda:
      /* (lambda <lc> ((<type> . <sym>) ... ) . <term>) */
      term = cdr(term);
      result = lambda_interpretations(car(term),     /* <lc> */
                                      dummy,
                                      nil,           /* anonymous function */
                                      second(term),  /* args */
                                      cdr2(term),    /* body */
                                      ctxt,
                                      env,
                                      tvs);
      break;

    case rec_lambda:
      /* (rec_lambda <lc> <func_name> ((<type> . <sym>) ... ) . <term>) */
      term = cdr(term);
      result = lambda_interpretations(car(term),       /* lc */
                                      dummy,
                                      second(term),    /* name of function */
                                      third(term),     /* args */
                                      cdr3(term),      /* body */
                                      ctxt,
                                      env,
                                      tvs);
      break;

    case app:
      /* (app <lc> <term> . <terms>) */
    {
  /* we need to transform: 
  
         ((X x ...) |-f-> body)(args)
            
     into: 
           
         with #f = (X x ...) |-f-> body, 
           #f(args)
               
     where #f is an internal symbol. In pseudo-Lisp: 

         (app <lc1> (rec_lambda <lc2> "f" ((<type> . <sym>) ... ) . <term>) . <args>)

     becomes: 
     
         (with <lc2> "#f"  (rec_lambda <lc2> "f" ((<type> . <sym>) ... ) . <term>) . 
             (app <lc1> (symbol <lc2> . "#f") . <args>))
  
  */

      Expr func = third(term);
      Expr args = cdr3(term);

        if (consp(func) && car(func) == rec_lambda)
        {
            char buf[1000];
            snprintf(buf,995,"#%s",string_content(third(func)));
            term = mcons5(with,
                          second(func),       // <lc2>
                          new_string(buf),    // "#f"
                          func,
                          mcons4(app,
                                 second(term),    // <lc1>
                                 mcons3(symbol,
                                        second(func),
                                        new_string(buf)),
                                 args)
                          );

           result = term_interpretations(ttype,term,ctxt,env,tvs,allow_mvar_access);
        }
        else
        {
        term = cdr(term);
        result = app_interpretations(car(term),        /* <lc> */
                                     dummy,
                                     func,           //car(cdr(term)),   /* operation */
                                     args,           //cdr(cdr(term)),   /* operands */ 
                                     ctxt,
                                     env,
                                     tvs,
                                     allow_mvar_access);
        }
      }
      break;

    case cond:
      /* (cond <lc> <test> . <clauses 1>) */
      term = cdr(term);
      result = cond_interpretations(car(term),      /* <lc> */
                                    dummy,
                                    car(cdr(term)), /* test */
                                    cdr(cdr(term)), /* clauses */
                                    ctxt,
                                    env,
                                    tvs);
      break;

    case select_cond:
      /* (select_cond <lc> <test> ((<sym> <typed resurg> ...) <lc> . <term>) . <else term>) */
      term = cdr(term);
      {
        Expr clause = third(term);
        result = select_cond_interpretations(car(term),         /* lc */
                                             second(term),      /* test */
                                             car(car(clause)),  /* constructor name */
                                             cdr(car(clause)),  /* typed resurgent symbols */
                                             cdr2(clause),      /* body of case term */
                                             cdr3(term),        /* else term */
                                             ctxt,
                                             env,
                                             tvs);
      }
      break;

    case with:
      /* (with <lc> <symbol> <term> . <term>) */
      result = with_interpretations(car(term),
                                    second(term),       /* lc */
                                    dummy,
                                    third(term),        /* symbol */
                                    forth(term),        /* defined term */
                                    cdr4(term),         /* body term */
                                    ctxt,
                                    env,
                                    tvs);
      break;

    case string:
      /* (string <lc> . <string>) */

      /* TODO: The required type must match String */

      result = list1(cons(term,env));
      break;

    case anb_read:
      /* (anb_read <lc> . <conn>) */
      term = cdr(term);
      result = read_interpretations(car(term),          /* lc */
                                    dummy,
                                    cdr(term),          /* conn */
                                    ctxt,
                                    env,
                                    tvs);
      break;

    case anb_write:
      /* (anb_write <lc> <conn> . <term>) */
      term = cdr(term);
      result = write_interpretations(car(term),          /* lc */
                                     dummy,
                                     second(term),       /* conn (<term>) */
                                     cdr2(term),         /* value (<term>) */
                                     ctxt,
                                     env,
                                     tvs);
      break;

    case anb_exchange:
      /* (anb_exchange <lc> <conn> . <term>) */
      term = cdr(term);
      result = exchange_interpretations(car(term),          /* lc */
                                        dummy,
                                        second(term),       /* conn (<term>) */
                                        cdr2(term),         /* value (<term>) */
                                        ctxt,
                                        env,
                                        tvs);
      break;

    case wait_for:
      {
        /* (wait_for <lc> <term> <term> . <term>) */
        term = cdr(term);
        result = wait_for_interpretations(car(term),    /* lc */
                                          dummy,
                                          second(term), /* condition */
                                          third(term), /* milliseconds */
                                          cdr3(term),   /* term after condition realized */
                                          ctxt,
                                          env,
                                          tvs);
      }
      break;

    case delegate:
      {
        /* (delegate <lc> <term> . <term>) */
        term = cdr(term);
        result = delegate_interpretations(car(term),    /* lc */
                                          dummy,
                                          second(term), /* delegated */
                                          cdr2(term),   /* body */
                                          ctxt,
                                          env,
                                          tvs);
      }
       break;


    case delegatep:
      {
        /* (delegatep <lc> <term> <term> . <term>) */
        term = cdr(term);
        result = delegatep_interpretations(car(term),    /* lc */
                                           dummy,
                                           second(term), /* priority */
                                           third(term),  /* delegated */
                                           cdr3(term),   /* body */
                                           ctxt,
                                           env,
                                           tvs);
      }
      break;


    case omega_true:
    case omega_false:
      result = list1(cons(term,env));
      break;

    case serialize:
      /* (serialize <lc> . <term>) */
      //assert(reading_predef); 
      term = cdr(term);
      result = serialize_interpretations(car(term),
                                         0,    /* don't allow serialize Opaque */
                                         dummy,
                                         cdr(term),
                                         ctxt,
                                         env,
                                         tvs);
      break;

    case tempserialize:
      /* (tempserialize <lc> . <term>) */
      //assert(reading_predef); 
      term = cdr(term);
      result = serialize_interpretations(car(term),
                                         1,    /* allow serialize Opaque */
                                         dummy,
                                         cdr(term),
                                         ctxt,
                                         env,
                                         tvs);
      break;

    case unserialize:
      /* (unserialize <lc> . <term>) */
      //assert(reading_predef); 
      term = cdr(term);
      result = unserialize_interpretations(car(term),
                                           0,  /* don't allow serialize Opaque */
                                           dummy,
                                           cdr(term),
                                           ctxt,
                                           env,
                                           tvs);
      break;

    case tempunserialize:
      /* (tempunserialize <lc> . <term>) */
      //assert(reading_predef); 
      term = cdr(term);
      result = unserialize_interpretations(car(term),
                                           1,  /* allow serialize Opaque */
                                           dummy,
                                           cdr(term),
                                           ctxt,
                                           env,
                                           tvs);
      break;

    case vcopy:
      /* (vcopy <lc> <Word32 n> . <init>) */
      term = cdr(term);
      result = vcopy_interpretations(car(term),     // lc
                                     second(term),  // n 
                                     cdr2(term),    // init
                                     ctxt,
                                     env,
                                     tvs);
      break;


    case bit_width:
      /* (bit_width <lc> . <type>) */
      term = cdr(term);
      result = bit_width_interpretations(car(term),  // lc
                                         cdr(term),  // type
                                         ctxt,
                                         env,
                                         tvs);
      break;


    case type_desc:
      /* (type_desc <lc> . type) */
      term = cdr(term);
      result = type_desc_interpretations(car(term),   // lc
                                         cdr(term),   // type
                                         ctxt,
                                         env,
                                         tvs);
      break;


    case byte_array:
      /* (byte_array <lc> . <byte array>) */

      result = list1(cons(term,env));
      break;


    case definition_of_type:
      /* (definition_of_type <lc> . <term>)    the term must be of type String */
      term = cdr(term);
      result = definition_of_type_interpretations(car(term),   // lc
                                                  cdr(term),   // name of type 
                                                  ctxt,
                                                  env,
                                                  tvs);
      break;

    case definition_of_term:
      /* (definition_of_type <lc> <term> . <term>)    
                    the first term must be of type AnubisType, the second one of type String */
      term = cdr(term);
      result = definition_of_term_interpretations(car(term),         // lc
                                                  second(term),      // type (of type AnubisType)
                                                  cdr2(term),        // name of term (of type String)
                                                  ctxt,
                                                  env,
                                                  tvs);
      break;

    case __line__:   /* (__line__ . <lisp integer>) */
    case __file__:   /* (__file__ . <lisp string>) */
    case __dir__:
    result = list1(cons(term,env));
    break;


    default:
      internal_error("Unknown term to interpret",term);
    }

  return result;
}


/*------------ Computing the interpretations of a symbol -----------------------*/
Expr symbol_micro_interpretations(Expr lc,
                                  Expr ttype,   /* required type for the symbol */
                                  Expr name,    /* name of symbol */
                                  Expr mctxt,    /* micro context */
                                  Expr micro_depth, /* depth of micro context within stack */
                                  Expr env)     /* environment for type unkowns */
{
  int i = 0;      /* used to compute depth of symbol in context */

assert(consp(lc));

  /* try to find the symbol in the micro context (apply strong preemption principle) */
  while (consp(mctxt))  /* context walk */
    {

      /* mctxt = ((<symbol> . <type>) ...) */
      if (name == car(car(mctxt)))
        {
          /* The symbol has been found in the context. It is micro-local. By
             strong preemption principle, its required type must match
             the type found in the context. This updates the
             environment. */

          /* TODO: match types here (this may produce an error message) */

          return list1(cons(mcons5(micro_local,       /* the symbol is micro_local */
                                   name,              /* name of local symbol */
                                   micro_depth,       /* depth of micro context */
                                   new_integer(i),    /* depth within micro context */
                                   cdr(car(mctxt))),  /* type found for the symbol */
                            env));        /* environment is unchanged */

        }
      i++;                    /* next depth */
      mctxt = cdr(mctxt);     /* sequel of micro-context */
    }

  /* otherwise, the symbol must be defined globally */
  return operation_interpretations(lc,
                                   dummy,   /* required type for the symbol */
                                   name,    /* name of global symbol */
                                   env);
}


Expr symbol_interpretations(Expr lc,
       Expr ttype,   /* required type for the symbol */
       Expr name,    /* name of symbol */
       Expr ctxt,    /* local context */
       Expr env)     /* environment for type unkowns */
{
  int i = 0;      /* used to compute depth of symbol in context */

  assert(consp(lc));

  if (name == pdstr__)
    {
      err_line_col(lc,"E115",
                   msgtext_symbol___not_usable[0]);
      return nil;
    }

  /* try to find the symbol in the context (apply strong preemption principle) */
  while (consp(ctxt))  /* context walk */
    {

      /* ctxt = ((<symbol> . <type>) ...)   or 
         ctxt = ((f_micro_ctxt <fname> <ftype> (<symbol> . <type>) ...) ...) */
      if (car(car(ctxt)) == f_micro_ctxt)
        {
          if (name == second(car(ctxt)))
            /* the name is that of the recursive closure created by: '|-name->' */
            {
              return list1(cons(mcons4(local,
                                       name,               /* fname */
                                       new_integer(i),
                                       third(car(ctxt))),  /* ftype */
                                env));
            }
          else
            {
              return symbol_micro_interpretations(lc,ttype,name,cdr3(car(ctxt)),new_integer(i),env);
            }
        }
      else if (name == car(car(ctxt)))
        {
          /* The symbol has been found in the context. It is local. By
             strong preemption principle, its required type must match
             the type found in the context. This updates the
             environment. */

          /* TODO: match types here (this may produce an error message) */

          return list1(cons(mcons4(local,             /* the symbol is local */
                                   name,              /* name of local symbol */
                                   new_integer(i),    /* depth in context */
                                   cdr(car(ctxt))),   /* type found for the symbol */
                            env));        /* environment is unchanged */

        }
      i++;                    /* next depth */
      ctxt = cdr(ctxt);       /* sequel of context */
    }

  /* otherwise, the symbol must be defined globally */
  return operation_interpretations(lc,
                                   dummy,   /* required type for the symbol */
                                   name,    /* name of global symbol */
                                   env);
}


/* checking if a type refers to Opaque(...) */
static int has_Opaque(Expr type)
{
 begin:
  if (consp(type))
    {
      if (is_struct_ptr_type(type))
        {
          if (consp(cdr(type)))
            {
              assert(car(cdr(type)) == new_integer(C_struct_id(pdstr_Opaque)));
              return 1;
            }
          else
            return 0;
        }
      else if (has_Opaque(car(type)))
        return 1;
      else
        type = cdr(type);
      goto begin;
    }
  else
    return 0;
}


/* Computing interpretations  of explicitly typed term  (T)t, where T  is a type, and  t a
   term:

   We verify first  that the given type is  known (up to unknows it may  contain). Then we
   verify that it matches the required type.

   Then we compute all  interpretations of t with that type. This  may still yield several
   interpretations.  If  no interpretation  is  compatible with  T,  an  error message  is
   sent. */
Expr of_type_interpretations(Expr lc,
                             Expr ttype,   /* required type */
                             Expr type,    /* T */
                             Expr term,    /* t */
                             Expr ctxt,
                             Expr env,
                             Expr tvs)
{
  Expr term_ints, term_ints_before, term_int_head, term_int_env, term_type, new_env, result;

  /* checking the type */
  if (!check_explicit_type(lc,type,tvs)) return nil;

  /* get interpretations of term for that type. */
  term_ints = term_ints_before = term_interpretations(dummy,term,ctxt,env,tvs,0);
  if (term_ints == nil) return nil;

  /* keep only those interpretations whose type match. */
  result = nil;
  while (consp(term_ints))
    {
      term_int_head = car(car(term_ints));
      term_int_env = cdr(car(term_ints));
      term_ints = cdr(term_ints);
      term_type = type_from_interpretation(term_int_head,term_int_env);

      /* unify given type with type of term */
      new_env = unify(type,
                      nil,
                      term_type,
                      term_int_env);

      if (new_env != not_unifiable)
        result = cons(cons(term_int_head,new_env),result);  // 10/08/2005 
      //result = cons(cons(mcons3(i_of_type,type,term_int_head),new_env),result);  
    }


  /* if no interpretation left, error message */
  if (result == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E017",
                       msgtext_incompatible_explicit_type[0]);
          show_type(errfile,type,env);
          fprintf(errfile,"%s",
                  msgtext_incompatible_explicit_type_2[0]);
          show_interpretations_types(errfile,term_ints_before);
          fprintf(errfile,"\n");
        }
      return nil;
    }

  /* maybe cannot unserialize Opaque */
    {
      Expr aux = result;
      while (consp(aux))
        {
          Expr term_int = car(aux);
          aux = cdr(aux);

          if (consp(car(term_int)) && car(car(term_int)) == unserialize)
            {
              if (has_Opaque(type_from_interpretation(car(term_int),cdr(term_int))))
                {
                  err_line_col(lc,"E117",
                               msgtext_Opaque_not_serializable[0]);
                  return nil;
                }
            }
        }
    }

  /* otherwise, return list of interpretations of term */
  return result;
}


#ifdef toto
Expr type_rep_interpretations(Expr lc,
         Expr type,
         Expr ctxt,
         Expr env,
         Expr tvs)
{
  /* check type */
  if (!check_explicit_type(lc,type,tvs)) return nil;

  /* there is only one interpretation */
  return list1(cons(mcons3(type_rep,lc,type),env));
}
#endif


/* Computing interpretations of the function of an applicative term */
Expr func_interpretations(Expr lc,
                          Expr ttype, /* required type */
                          Expr op,    /* <term> */
                          int arity,  /* required arity */
                          Expr ctxt,
                          Expr env,
                          Expr tvs)
{
  Expr ints = term_interpretations(dummy,op,ctxt,env,tvs,0);
  Expr result = nil;
  Expr type, aux;

  if (ints == nil) return nil;

  /* we  must  keep  only  those  interpretations  which are  functional  with  the  right
     arity. Note: multiple variables are function of arity 1 at that point.  */
  aux = ints;

  while (consp(aux))
    {
      type = type_from_interpretation(car(car(aux)),cdr(car(aux)));
      soft_dereference_type(type,cdr(car(aux)));
      if (consp(type) &&
            (
              ((car(type) == functype) && length(second(type)) == arity) ||
              ((car(type) == type_MVar) && arity == 1)
             )
          )
        {
          result = cons(car(aux),result);
        }
      /* else do nothing */

      aux = cdr(aux);
    }

  /* if no interpretation left, warn */
  if (result == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E018", str_format(
                                             msgtext_not_a_function_of_arity[0],
                                             arity));
          show_interpretations_types(errfile,ints);
        }
    }

  return result;
}


Expr get_lambda_type(Expr lc,
                     Expr body,
                     Expr mctxt)
{
  /* mctxt = ((<sym> . <type>)...) */
  Expr source_types = nil;
  while(consp(mctxt))
    {
      source_types = cons(cdr(car(mctxt)),source_types);
      mctxt = cdr(mctxt);
    }
  source_types = reverse(source_types);
  return mcons3(functype,source_types,fresh_unknown());
}


Expr lambda_interpretations         (Expr lc,
                                     Expr ttype,
                                     Expr fname,
                                     Expr args,
                                     Expr body,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs)
{
  Expr aux, bints, result, mctxt, lctxt, ftype;

  /* check that Ti's are correct types, and construct the context of |-> declared symbols */
  aux = args;
  lctxt = nil;
  while consp(aux)
    {
      if (!check_explicit_type(lc,car(car(aux)),tvs)) return nil;
      lctxt = cons(cons(cdr(car(aux)),car(car(aux))),lctxt);
      /* if preemption forbidden check argument's names against 'ctxt'. */
      if (no_preemption)
        {
          Expr hidden_entries = get_hidden_entries(cdr(car(aux)),ctxt);
          if (hidden_entries != nil)
            {
              if (show_errors)
                {
                  warn_line_col(lc,"W019",
                               msgtext_hidden_variables[0]);
                  show_context(errfile,hidden_entries,env);
                }
              //return nil; 
            }
        }

      aux = cdr(aux);
    }
  lctxt = reverse(lctxt);


  /* construct the micro_context */
  mctxt = get_micro_ctxt(lc,body,fname,args,ctxt);
  /* at that point: mctxt = ((<sym> . <type>)...) */

  /* construct type of function */
  ftype = get_lambda_type(lc,body,lctxt);
  /* ftype = (functype <types> . <type>) 
   Actually, the target type is an unknown at that point. */

  /* Lisp syntax: (f_micro_ctxt <fname> <ftype> (<sym> . <type>) ...) */
  mctxt = mcons4(f_micro_ctxt,fname,ftype,mctxt);
  /* at this point: mctxt = (f_micro_ctxt fname ftype (<sym> . <type>)...) */

  /* interpret body */
  bints = term_interpretations(dummy,
                               body,
                               append(lctxt,
                                      list1(mctxt)),
                               env,
                               tvs,
                               0);


  if (bints == nil) return nil;

  /* For each interpretation 'body_interpretation' of  the body we construct the following
     interpretation of the function:
   
       (closure <lc> mctxt args . body_interpretation)
   
   For each one we unify the target type of the function with the type of the body. 
  */

  result = nil;
  while (consp(bints))
    {
      Expr new_env;
      aux = car(bints);
      bints = cdr(bints);

      if (unused_fun_name && fname != nil && !member(fname,symbols_in_interp(car(aux))))
      {
        warn_line_col(lc,
                      "W012",
                      str_format(msgtext_warn_rec_lambda_f_not_used[0],string_content(fname))
                      );
      }

      new_env = unify(cdr2(ftype),env,
                      type_from_interpretation(car(aux),cdr(aux)),cdr(aux));

      if (new_env == not_unifiable)
        {
          if (show_errors)
            {
              err_line_col(lc,"E020",
                           msgtext_incompatible_lambda_type[0]);
              show_interpretations_types(errfile,bints);
            }
          return nil;
        }

      result = cons(cons(mcons5(closure,
                                lc,
                                mctxt,
                                lctxt,
                                car(aux)),
                         new_env),
                    result);
    }

  return result;
}


   /* The function below tests if the argument number 'arg_rank' has a type compatible with
      the corresponding place in the function whose interpretation is op_int. 
      'args_ints' is the list of all interpretations of the tuple of all arguments. */

int compatible_arg(Expr   op_int,     // interpretation of a function 
                   int    arg_rank,   // rank of an argument (starting at 0)
                   int    arity,
                   Expr   args_ints)  // interpretations of the tuple of arguments
{
  Expr rank = new_integer(arg_rank);
  Expr op_type = type_from_interpretation(car(op_int),cdr(op_int));
  Expr op_arg_type = nth(rank,car(cdr(op_type))); // type of argument of the function
  Expr op_env = cdr(op_int);
  Expr args_int;
  Expr arg_type;
  Expr arg_env;
  Expr u;
  while(consp(args_ints))
    {
      args_int = car(args_ints);    // first interpretation of all arguments
      // args_int = ((I1 ... In) . e) 
      arg_env = cdr(args_int);
      arg_type = type_from_interpretation(nth(rank,car(args_int)),arg_env);
      u = unify(op_arg_type,op_env,arg_type,arg_env);
      if (u == not_unifiable)
        {
          args_ints = cdr(args_ints);   // do the same for the other interpretation of the arguments
          continue;
        }
      else return 1;
    }
  return 0;
}

/* Computing the list of interpretations of an applicative term:

   We have a  required type for the applicative  term. This means that the  target part of
   the type of the function must match that required type.

   Since the arity k  of the function is known, we may  construct a type like: ($1,...,$k)
   -> T, where T  is the required type.  Then, we get all interpretations  of the function
   with that type.

   It must be non empty. If it is empty, an error message, has already been sent.

   Then for  each interpretation found for  the function, we call  the auxiliary procedure
   app_interpretations_1,  to get  all interpretations  of the  applicative term  for that
   particular interpretation of the function.

   Finally, we just have to concatenate these results. */

Expr app_interpretations(Expr lc,
                         Expr ttype, /* required type */
                         Expr op,    /* <term> */
                         Expr args,  /* <terms> */
                         Expr ctxt,
                         Expr env,
                         Expr tvs,
                         int allow_mvar_access)
{
  Expr op_ints, args_ints, ctxts, result, aux;
  int arity = length(args);
  int i;

  if (car(op) == rec_lambda)
  {
  debug(op);
  debug(args);
  }

  /* TODO: construct ($1,...,$k) -> ttype, to replace dummy
     below. Keep the list ($1,...,$k) which is the list of required
     types for the operands (in all interpretations of the function !!!) */

  /* get interpretations of function */
  op_ints = func_interpretations(lc,dummy,op,arity,ctxt,env,tvs);
  if (op_ints == nil) return nil;

  /* prepare a list of identical contexts */
  ctxts = nil;
  for (i = 0; i < arity; i++)
    ctxts = cons(ctxt,ctxts);

  /* get interpretation of arguments */
  /* TODO: suppress this. */
  args_ints = tuple_interpretations(dummy,args,ctxts,env,tvs,0);

  if (args_ints == nil) return nil;

  /* collect interpretations of applicative term */
  result = nil;
  aux = op_ints;
  while (consp(aux))
    {
      /* TODO: transmit ($1,...,$k), args, ctxts, env and tvs,
         instead. app_interpretations_1 has to be rewritten. */
      result = append(app_interpretations_1(lc,
                                            car(car(aux)),
                                            cdr(car(aux)),
                                            args_ints,
                                            allow_mvar_access),
                      result);
      aux = cdr(aux);
    }

  /* this may result in no interpretation at all */
  if (result == nil)
    {
      int n = 1;

      if (show_errors)
        {
          err_line_col(lc,"E021",
                       msgtext_incompatible_args[0]);
          show_interpretations_types(errfile,op_ints);
          fprintf(errfile,"%s",msgtext_args_interpretations[0]);
          while (consp(args))
            {
              fprintf(errfile,msgtext_argument_number[0],n++);
              show_interpretations_types(errfile,
                                         term_interpretations(dummy,car(args),ctxt,env,tvs,0));
              args = cdr(args);
            }
          fprintf(errfile,"\n");
          fprintf(errfile,"%s",msgtext_func_args_table[0]);
          {
            int i, j;
            Expr ops = op_ints;
            fprintf(errfile,"                      ");
            for (i=9; i<arity; i++) fprintf(errfile," %d", (i+1)/10);
            fprintf(errfile,"\n    ");
            for (i=0; i<arity; i++) fprintf(errfile," %d", (i+1)%10);
            //fprintf(errfile,"\n");
            i = 1;   // used to number functions
            while(consp(ops))
              {
                fprintf(errfile,"\n %3d", i);
                for(j=0;j<arity;j++)
                  {
                      if (compatible_arg(car(ops),j,arity,args_ints))
                        fprintf(errfile," .");
                      else
                        fprintf(errfile," ?");
                  }
                ops = cdr(ops); i++;
              }
            fprintf(errfile,"\n\n");
          }
        }
    }

  return result;
}


/* Computing the interpretations of an applicative term, for a given
   interpretation of the operation */
Expr app_interpretations_1(Expr lc,
                           Expr op_int_head,         /* head of interpretation of the function */
                           Expr op_int_env,          /* environment of interpretation of the function */
                           Expr args_ints,           /* interpertations of arguments */
                           int allow_mvar_access)
{
  Expr new_env, args_int_heads, args_int_env, args_types, aux, sign, func_type;
  Expr result = nil;

  /* we have only one interpretation for the function: 

     (op_int_head . op_int_env)

     and a list of tuple interpretations for the arguments:

     args_ints

     We  can  construct at  most  one  interpretation of  the  applicative  term for  each
     interpretation of the tuple of arguments.
   
     There is  also the  particular case in  which the  'function' is actually  a multiple
     dynamic variable.
  */

  /* we get the signature of the function */
  func_type = type_from_interpretation(op_int_head,
                                       op_int_env);
  dereference_type(func_type,op_int_env);

  switch(car(func_type))
    {

    case functype:
      sign = signature_from_type(func_type,op_int_env);
      while (consp(args_ints))
        {
          /* do the following for each interpretation of the tuple of arguments */
          args_int_heads = car(car(args_ints));   /* tuple of interpretations heads */
          args_int_env = cdr(car(args_ints));     /* environment for arguments */
          args_ints = cdr(args_ints);

          /* collect types of actual arguments from their interpretations */
          args_types = nil;
          aux = args_int_heads;
          while (consp(aux))
            {
              args_types = cons(type_from_interpretation(car(aux),args_int_env),
                                args_types);
              aux = cdr(aux);
            }
          args_types = hard_reverse(args_types);

          /* unify types of actual arguments with types of formal
             arguments. */

          new_env = unify(args_types,
                          args_int_env,
                          sign,
                          op_int_env);

          /* if unification succeeds, record the interpretation */
          if (new_env != not_unifiable)
            {
              if ((car(op_int_head) == operation) &&
                  ((operations[integer_value(third(op_int_head))].global) & macro_mask))
                { /* operation is macro: perform a delta-reduction. 
                     Note: at this point, 'inline functions' have already be replaced by macros.
                
                     We proceed as follows. At this point, op_int_head has the form: 
                     
                        (operation <lc> <opid> <name> <parms> <type> . <types>)
                        
                   */
               U32 opid = integer_value(third(op_int_head));

                   /* From <opid> we can get the body of the function and its target type. */
               Expr body = operations[opid].definition;
               Expr body_type = operations[opid].target_type;

                   /* We also need the list of types which are the values 
                      (found so far) of the parameters, and the list of original
                      parameters */
               Expr    parms_values = fifth(op_int_head);
               Expr  original_parms = operations[opid].parms;

                   /* The parameters ($T1 ... $Tk) in the body, must be replaced 
                      by their values (U1 ... Uk). We construct the list:
                     
                        already_refreshed = (($T1 . U1) ... ($Tk . Uk))
                        
                   */
                Expr already_refreshed = nil;

                /* A macro or inline function cannot be used before it is defined. */
                if (body == no_term)
                {
                  err_line_col(lc,"E119",
                               str_format(msgtext_undefined_macro[0],
                                          string_content(car(operations[opid].names)),
                                          integer_value(operations[opid].line),
                                          string_content(operations[opid].abs_file_path)));
                  return nil;
                }

                while (consp(original_parms))
                {
                  already_refreshed = cons(cons(car(original_parms),
                                                car(parms_values)),
                                           already_refreshed);
                  original_parms = cdr(original_parms);
                  parms_values   = cdr(parms_values);
                }
                assert(parms_values == nil);   /* the two lists must have the same length */

                   /* Refresh the body ('refresh' is defined in 'unknowns.c') */
                body      = refresh(body,&already_refreshed);
                body_type = refresh(body_type,&already_refreshed);

                   /* At this point we have a new body with type parameters replaced by correct
                      types (which may still contain unknowns). 
                     
                      The next step is to replace all occurrences of the formal parameters
                      of the function by the interpretations of the arguments within this new body. 
                      We must of course avoid any capture of variable, which may lead to rename
                      some bound variables. Furthermore, all formal parameters must be replaced 
                      in parallel. 
                     
                      We don't have to worry about transitivity of macroness. Indeed, if
                      the macro functions 'f' called here itself calls another macro function
                      'g', the calls to 'g' have already been expanded within the body of 
                      'f'. 
                      
                      Before calling 'interp_replace' (defined in replace.c), we construct the needed 
                      dictionary:
                   */
                   Expr     dict = nil;
                   Expr     ctxt = operations[opid].ctxt;    /* ((x_1 . T_1) ... (x_k . T_k)) */
                   Expr   values = args_int_heads;           /* (v_1 ... v_k) */

                   while (consp(ctxt))
                   {
                     dict = cons(cons(car(car(ctxt)),car(values)),dict);

                     ctxt = cdr(ctxt);
                     values = cdr(values);
                   }
                   assert(values == nil);

                   /*  Now, dict has the form ((x_k . v_k) ... (x_1 . v_1)) 
                       where x_i is a formal variable of the inline function, and v_i 
                       the value to be substituted to it. 
                   */

                   //debug(dict);
                  body = interp_replace(body,
                                        dict,
                                        op_int_head);

                   /* The resulting interpretation head is wrapped into
                   
                      (inline <lc (of call)> 
                              <fname (of source file of inline function)> 
                              <line (of inline function)>  
                              . <interpretation head>) 
                      
                      so that it is possible to generate comment lines within the .sc
                      file indicating where is precisely the code put inline. */
                  result = cons(cons(mcons5(macro,
                                            lc,                                /* of call to inline operation */
                                            operations[opid].abs_file_path,    /* of inline operation definition */
                                            operations[opid].line,             /* of inline operation definition */
                                            body),
                                     new_env),
                                result);

                  //debug(result);
                }
              else
                {
                  result = cons(cons(mcons4(app,
                                            lc,
                                            op_int_head,
                                            args_int_heads),
                                     new_env),
                                result);
                }
            }
        }
      break;

    case type_MVar:
      {
        Expr word32_arg_ints;

        if (!allow_mvar_access)
          {
            err_line_col(lc,"E0116",
                         msgtext_mvar_access[0]);
            return nil;
          }

        /* keep only those interpretations of arguments which have just one argument of type
           Word32. */
        aux = args_ints;
        word32_arg_ints = nil;
        while (consp(aux))
          {
            if (
                (length(car(car(aux))) == 1) &&
                (type_from_interpretation(car(car(car(aux))),cdr(car(aux))) == pdstr_Word32)
                )
              word32_arg_ints = cons(car(aux),word32_arg_ints);
            aux = cdr(aux);
          }

        /* check if there are still interpretations */
        if (word32_arg_ints == nil)
          {
            if (show_errors)
              {
                err_line_col(lc,"E022",
                             msgtext_mvar_args[0]);
                show_tuple_interpretations_types(errfile,args_ints);
              }
            return nil;
          }

        /* for  the  interpretation  (h  .  e)   of  the  multiple  variable  and  for  each
           interpretation (ha . ea) of the argument, construct the interpretation:
   
           ((mvar_access h . ha) . ea)
   
        */
        aux = word32_arg_ints;
        while (consp(aux))
          {
            Expr new_env = join_envs(op_int_env,cdr(car(aux)));
            if (new_env != not_unifiable)
              result = cons(cons(mcons3(mvar_access,op_int_head,car(car(car(aux)))),
                                 new_env),
                            result);
            aux = cdr(aux);
          }

        /* check that there are still interpretations */
        if (result == nil)
          {
            if (show_errors)
              {
                err_line_col(lc,"E023",
                             msgtext_mvar_incompatible_arg[0]);
                show_interpretations(errfile,word32_arg_ints);
              }
          }
      }
      break;

    default: internal_error("Cannot apply to arguments",func_type); break;

    }
  return result;
}


Expr with_interpretations(Expr keyword,  /* with */
     Expr lc,
     Expr ttype,
     Expr symbol,
     Expr value,
     Expr body,
     Expr ctxt,
     Expr env,
     Expr tvs)
{
  Expr value_ints, body_ints, result;

  if (no_preemption)
    {
      Expr hidden_entries = get_hidden_entries(symbol,ctxt);
      if (hidden_entries != nil)
        {
          if (show_errors)
            {
              warn_line_col(lc,"W024",
                           msgtext_hidden_variables[0]);
              show_context(errfile,hidden_entries,env);
            }
          //return nil; 
        }
    }

  /* we ask for one and only one interpretation for the value, with
     possibly unknown types */
  value_ints = term_interpretations(dummy,
                                    value,
                                    ctxt,
                                    env,
                                    tvs,
                                    0);
  if (value_ints == nil) return nil;

  if (length(value_ints) >= 2)
    {
      if (show_errors)
        {
          err_line_col(lc,"E025",
                       str_format(keyword == with ? msgtext_ambiguous_local_def[0]
                                  : msgtext_ambiguous_local_init[0],
                                  string_content(symbol)));
          show_simple_ambiguity(errfile,value_ints);
          //show_interpretations_types(errfile,value_ints); 
        }
      return nil;
    }

  /* expand the context for the interpretation of the body */
  ctxt =
    cons(cons(symbol,type_from_interpretation(car(car(value_ints)),cdr(car(value_ints)))),
         ctxt);

  /* interpret the body */
  body_ints = term_interpretations(dummy,
                                   body,
       ctxt,  /* new context */
       cdr(car(value_ints)),  /* new environment */
                                   tvs,0);
  if (body_ints == nil) return nil;

  /* construct the resulting interpretations list. Each interpretation
     head has the form: 

         (with <lc> <symbol> <int head> . <int head>) 

  */
  result = nil;
  while (consp(body_ints))
    {
      result =
 cons(cons(mcons5(keyword,
    lc,
    symbol,
    car(car(value_ints)),
    car(car(body_ints))),
    cdr(car(body_ints))),
      result);
      body_ints = cdr(body_ints);
    }

  return result;
}


/* test_interpertation returns either nil, or the unique interpretation
   of a term supposed to be the test of a conditional. */
static Expr test_interpretation(Expr lc,
                                Expr test,
                                Expr ctxt,
                                Expr env,
                                Expr tvs,
                                Expr *already_refreshed_addr)
{
  Expr test_ints, aux, aux2, aux3, test_int_head, test_type;
  struct Type_struct *tt;
  int i;

  /* interpret test */
  /* TODO: replace dummy by a fresh unknown below. */
  test_ints = term_interpretations(dummy,test,ctxt,env,tvs,0);
  if (test_ints == nil) return nil;

  /* drop all interpretations whose type is not a sum (alias 'defined') type */
  aux = test_ints;
  aux2 = nil;
  while (consp(aux))
    {
      aux3 = type_from_interpretation(car(car(aux)),cdr(car(aux)));
      if (is_sum_type(aux3,cdr(car(aux))))
        aux2 = cons(car(aux),aux2);
      aux = cdr(aux);
    }
  if (aux2 == nil)
    {
      /* test has only non sum interpretations */
      if (show_errors)
        {
          err_line_col(lc,"E026",
                       msgtext_test_is_not_a_sum[0]);
          show_interpretations_types(errfile,test_ints);
        }
      return nil;
    }

  /* test should not have several interpretations */
  if ((i = length(test_ints)) >= 2)
    {
      if (show_errors)
        {
          err_line_col(lc,"E027", str_format(
                                             msgtext_test_has_several_interpretations[0],
                                             i));
          show_simple_ambiguity(errfile,test_ints);
          fprintf(errfile,"\n");
        }
      return nil;
    }

  /* test now has one interpretation (which may be still ambiguous,
     because we did not check for unknowns; we don't need to) */
  test_int_head = car(car(test_ints));
  env = cdr(car(test_ints));

  /* get the type of test */
  test_type = type_from_interpretation(test_int_head,env);

  /* dereference test type */
  while (is_unknown(test_type))
    {
      aux = assoc(test_type,env);
      if (aux == key_not_found)
        break;
      else
        test_type = aux;
    }

  /* type of test cannot be unknown */
  if (is_unknown(test_type))
    {
      if (show_errors)
        {
          err_line_col(lc,"E028",
                       msgtext_test_type_unknown[0]);
        }
      return nil;
    }

  /* type of test cannot be a parameter: $T */
  if (is_user_type_variable(test_type))
    {
      if (show_errors)
        {
          err_line_col(lc,"E029", str_format(
                                             msgtext_test_type_is_parameter[0],
                                             utvar_name(test_type)));
        }
      return nil;
    }

  /* get test type description */
  tt = get_type_description(test_type,lc);
  if (tt == NULL) return nil;

  /* check that type is complete (all alternatives defined) */
  if (!(tt->completed))
    {
      if (show_errors)
        {
          err_line_col(lc,"E030",
                       msgtext_test_type_not_complete[0]);
        }
      return nil;
    }

  /* unify parms in tt, with operands of type of test */
  if (consp(test_type))
    {
      env = unify(refresh(tt->parms,already_refreshed_addr),
                  nil,
                  cdr(cdr(test_type)),
                  env);
      assert(env != not_unifiable);
    }

  /* return the unique interpretation */
  return cons(test_int_head,env);
}


/* Computing the interpretations of a conditional:

   First, we compute  the interpretations of the test with an  unknown required type. This
   must  lead to  one  and only  one  interpretation, whose  type  may eventually  contain
   unknowns.

   The type of the test must be such that its alternatives are known. In other words, this
   type cannot be  an unknown or a  user type variable. It must  be a type name  or a type
   scheme  name.  In  the case  of  a  type  scheme  name,  the operands  may  still  have
   unknowns. This  is not a problem,  since the alternatives of  the type of  the test are
   well defined.

   Next, all the cases must match one alternative and only one.

   We prepare contexts  for bodies interpretations of all the cases.  The required type is
   also the required type for all the bodies.

   We interpret the bodies as a tuple whose list of required types is (T,...,T) where T is
   the required type.

   Finally, we construct the list of interpretations of the conditional. */

Expr cond_interpretations(Expr lc,
                          Expr ttype,
                          Expr test,
                          Expr clauses,
                          Expr ctxt,
                          Expr env,
                          Expr tvs)
{
  Expr test_int_head, test_type, result, aux, alts;
  int nclauses, nalt, i, j, k;
  Expr clauses_heads, ctxts, bodies, bodies_ints, clauses_int, new_seg;
  Expr aux2, aux3;
  Expr already_refreshed = nil;

  /* get unique interpretation of test */
  aux = test_interpretation(lc,test,ctxt,env,tvs,&already_refreshed);
  if (aux == nil) return nil;

  /* extract informations */
  test_int_head = car(aux);
  env = cdr(aux);
  test_type = type_from_interpretation(test_int_head,env);

  /* get alternatives of type of test */
  alts = get_alts(test_type,env,lc);

  /* alts have been obtained  from the type description of the type  of the test. alts has
     the form:
   
     (
     ((<sym>...) (<type> . <sym name>) ...)
     ...
     )

     The types in alts should be unified with the types in test_type.

  */


  /* check number of clauses */
  nalt = length(alts);
  nclauses = length(clauses);
  if (nclauses < nalt)
    {
      if (show_errors)
        {
          err_line_col(lc,"E031", str_format(
                                             msgtext_wrong_number_of_cases[0],
                                             nclauses,
                                             nalt));
          //show_type(errfile,test_type,env); 
          fprintf(errfile,"\n");
          show_alts(errfile,alts,env);
          fprintf(errfile,"\n");
        }
      return nil;
    }

  if (nclauses > nalt)
    {
      Expr new_conditional;

      new_conditional = expand_conditional(lc,
                                           alts,
                                           test,
                                           clauses,
                                           env);

      if (!consp(new_conditional))
        return nil;

      return cond_interpretations(lc,
                                  ttype,
                                  test,
                                  cdr3(new_conditional),
                                  ctxt,
                                  env,
                                  tvs);
    }

  /* if required, check for named (i.e. not "_") unused resurgent symbols 
     This must be done only after the expansion of subcases (done just above). 
  */
  if (unused_resurg)
  {
    Expr cs = clauses;
    while (consp(cs))
    {
      Expr c = car(cs);                             /* c = ((<name> (<sym> . <type>) ...) <lc> . <head>) */
      Expr rsyms = cdr(car(c));                     /* rsyms = (<sym> ... (<type>. <sym>) ...) */
      Expr body_syms = _symbols_in_term(cdr2(c));   /* list of symbols free in body of case */
      while (consp(rsyms))
      {
        Expr sym =       consp(car(rsyms)) ? cdr(car(rsyms)) : car(rsyms);
        if (    is_string(sym)
            &&  sym != pdstr__
            &&  !member(sym, body_syms)
           )
        {
          warn_line_col(second(c),   /* <lc> in conditional case (position of 'then') */
                        "W011",
                        str_format(msgtext_unused_named_resurgent[0],
                                   string_content(sym)));
        }
        rsyms = cdr(rsyms);
      }
      cs = cdr(cs);
    }
  }

  /* check each head of clause against corresponding alternative */
  bodies = nil;
  ctxts = nil;
  clauses_heads = nil;
  i = 1; // number of the alternative

  while (consp(alts))
    {

      /* car(alts) = ((name ... name) (type . sym) ... (type . sym)) */

      /* check constructor name */
      if (!member(car(car(car(clauses))),
                  car(car(alts))  ))
        {
          assert(is_string(car(car(car(clauses)))));
          if (show_errors)
            {
              err_line_col(lc,"E032", str_format(
                                                 msgtext_bad_case_name[0],
                                                 i,
                                                 string_content(car(car(car(clauses)))),
                                                 string_content(car(car(car(alts))))));
            }
          return nil;
        }

      /* check constructor arity */
      if ((j = length(cdr(car(alts))) )
          != (k = length(cdr(car(car(clauses))))))
        {
          if (show_errors)
            {
              err_line_col(lc,"E033", str_format(
                                                 msgtext_wrong_number_of_resurgent_variables[0],
                                                 i,
                                                 k,
                                                 j));
              show_typed_resurgent_symbols(errfile,car(alts),env);
              fprintf(errfile,"\n");
            }
          return nil;
        }

      /* record clause head, adding resurgent variables types.
         Each clause head has the form: 

         (<name> <sym> ... <sym>)

         transform it into 

         (<name> (<sym> . <type>) ... (<sym> . <type>))

         For 'else' case, keep 'else_case'. 

      */
      if (car(car(clauses)) == else_case)
        {
          clauses_heads = cons(else_case,clauses_heads);
        }
      else
        {
          aux = cdr(car(alts));           /* ((<type> . <destructor name>) ... ) [components of alt] */
          aux2 = nil;                     /* ((<resur sym> . <type>) ... ) */
          aux3 = cdr(car(car(clauses)));  /* (<var name> ... <var name>) [resurgent symbols] */
          j = 1;
          while (consp(aux))
            {
              /* 
                 at this point, car(car(aux)) is the  type of the resurgent variable as it
                 is declared in the type definition.
              */

              /* if the resurgent symbol has a  type declared, this type must unify with
                 to the type declared in the type definition. */
              if (consp(car(aux3)))
                {
                  Expr drstype = car(car(aux3));   // declared type of resurgent symbol
                  Expr ctype = car(car(aux));
                  Expr new_env = unify(drstype,env,ctype,env);
                  Expr the_symbol = cdr(car(aux3));   // the resurgent symbol itself
                  if (!is_string(the_symbol))
                    {
                      if (show_errors)
                        {
                          err_line_col(lc,"E092",
                                       str_format(msgtext_unexpected_subcase[0]));
                        }
                      return nil;
                    }

                  if (is_singleton_name(lc,the_symbol,ctype,env))
                    {
                      if (show_errors)
                        {
                          err_line_col(lc,"E093",
                                       str_format(msgtext_unexpected_subcase2[0],
                                                  string_content(the_symbol)));
                        }
                      return nil;
                    }

                  if (new_env == not_unifiable)
                    {
                      if (show_errors)
                        {
                          err_line_col(lc,"E034", str_format(
                                msgtext_wrong_resurgent_symbol_type_declaration1[0],i,j));
                          show_type(errfile,drstype,env);
                          fprintf(errfile,"%s",
                                  msgtext_wrong_resurgent_symbol_type_declaration2[0]);
                          show_type(errfile,ctype,env);
                          fprintf(errfile,"\n\n");
                        }
                      return nil;
                    }
                  else
                    {
                      env = new_env;
                    }
                }
              else
                {
                  Expr the_symbol = car(aux3);
                  Expr ctype = car(car(aux));

                  if (!is_string(the_symbol))
                    {
                      if (show_errors)
                        {
                          err_line_col(lc,"E092",
                                       str_format(msgtext_unexpected_subcase[0]));
                        }
                      return nil;
                    }

                  if (is_singleton_name(lc,the_symbol,ctype,env))
                    {
                      if (show_errors)
                        {
                          err_line_col(lc,"E093",
                                       str_format(msgtext_unexpected_subcase2[0],
                                                  string_content(the_symbol)));
                        }
                      return nil;
                    }
                }


              aux2 = cons(cons(consp(car(aux3)) ?
                               cdr(car(aux3)) :
                               car(aux3),
                               car(car(aux))),

                          aux2);
              aux = cdr(aux);
              aux3 = cdr(aux3);
              j++;
            }
          aux2 = hard_reverse(aux2); /* ((<resur sym> . <type>) ... ) */


          clauses_heads = cons(cons(car(car(car(clauses))),  /* name of case */
                                    aux2),                   /* typed resurgent symbols */
                               clauses_heads);
        }


      /* construct context for body interpretations */
      new_seg = nil;
      j = 0;
      aux = cdr(car(car(clauses)));   /* (<var> ... <var>) */
      aux2 = cdr(car(alts));          /* ((<type> . <sym>) ... ) */
      while (consp(aux))

        {

          Expr sym = consp(car(aux)) ? cdr(car(aux)) : car(aux);

          new_seg = cons(cons(sym,
                              car(car(aux2))),
                         new_seg);

          if (no_preemption)
            {
              Expr hidden_entries = get_hidden_entries(sym,ctxt);
              if (hidden_entries != nil)
                {
                  if (show_errors)
                    {
                      warn_line_col(lc,"W035",
                                   msgtext_hidden_variables[0]);
                      show_context(errfile,hidden_entries,env);
                    }
                  //return nil; 
                }
            }

          aux = cdr(aux);
          aux2 = cdr(aux2);
          j++;
        }
      ctxts = cons(rappend(new_seg,ctxt),ctxts);

      /* record body of clause */
      bodies = cons(cdr(cdr(car(clauses))),bodies);

      /* do for next clause and next alternative */
      clauses = cdr(clauses);
      alts = cdr(alts);
      i++;
    }

  /* put things in the right order */
  bodies = hard_reverse(bodies);
  ctxts = hard_reverse(ctxts);
  clauses_heads = hard_reverse(clauses_heads);

  /* interpret the tuple of bodies */
  bodies_ints = tuple_interpretations(dummy,bodies,ctxts,env,tvs,1);
  if (bodies_ints == nil)
   {
     Expr interps;
     int i = 1;

     if (show_errors && !errors)
       {
         err_line_col(lc,"E112",
                      msgtext_incompatible_case_bodies_types[0]);
         while (consp(bodies))
           {
             show_errors = 0;
             interps = term_interpretations(dummy,car(bodies),car(ctxts),env,tvs,0);
             show_errors = 1;
             fprintf(errfile,"\nCase number %d:\n",i);
             show_interpretations_types(errfile,interps);
             ctxts = cdr(ctxts);
             bodies = cdr(bodies);
             i++;
           }
       }
     return nil;
   }

  /* keep only those tuple interpretations, where the types of the
     elements of the tuple unify together. 
   
  */

  //#define checkforsametypeagain
#ifdef checkforsametypeagain
  aux = aux2 = bodies_ints;
  bodies_ints = nil;
  while (consp(aux))
    {
      bodies_int_heads = car(car(aux));
      bodies_int_env = cdr(car(aux));
      aux = cdr(aux);

      if (consp(bodies_int_heads))
        {
          /* there is at least one case */
          first_type =
            type_from_interpretation(car(bodies_int_heads),bodies_int_env);
          other_heads = cdr(bodies_int_heads);

          /* unify other's types with type of first body. This makes
             bodies_int_env grow or vanish (if unification fails). */
          while (consp(other_heads))
            {
              bodies_int_env = unify(first_type,
                                     nil,
                                     type_from_interpretation(car(other_heads),bodies_int_env),
                                     bodies_int_env);
              if (bodies_int_env == not_unifiable) break;
              other_heads = cdr(other_heads);
            }

          /* if bodies_int_env did not vanish, keep that interpretation
             (with its new environment) */
          if (bodies_int_env != not_unifiable)
            {
              bodies_ints = cons(cons(bodies_int_heads,
                                      bodies_int_env),
                                 bodies_ints);
            }
        }
      else
        {
          /* conditional with zero case */
          bodies_ints = cons(cons(nil,bodies_int_env),bodies_ints);
        }
      /* continue with next interpretation of bodies */
    }
#endif

  /* If no interpretation left for the set of bodies, warn. */
  /* TODO: no need to keep that, because already warned by
     tuple_interpretations. */
  if (bodies_ints == nil)
    {
      if (show_errors)
        {
          int n = 1;
          err_line_col(lc,"E036",
                       msgtext_cannot_interpret_cond_bodies[0]);
          //      show_tuple_interpretations_types(errfile,aux2); 
          while (consp(bodies))
            {
              fprintf(errfile,msgtext_case[0],n++);
              show_interpretations_types(errfile,
                                         term_interpretations(dummy,car(bodies),car(ctxts),env,tvs,0));
              bodies = cdr(bodies);
              ctxts = cdr(ctxts);
            }
        }
      return nil;
    }

  /* Finally, construct interpretations of the conditional. There is
     one for each left interpretation of the tuple of bodies. */
  /* TODO: change that to handle 'else' case */
  result = nil;
  while (consp(bodies_ints))
    {
      /* prepare clauses interpretation */
      aux = car(car(bodies_ints));   /* interpretation heads of bodies */
      aux2 = clauses_heads;
      clauses_int = nil;
      while (consp(aux))
        {
          clauses_int = cons(mcons3(car(aux2),       /* head */
                                    new_integer(0),  /* lc */
                                    car(aux)),       /* body */
                             clauses_int);
          aux = cdr(aux);
          aux2 = cdr(aux2);
        }
      clauses_int = hard_reverse(clauses_int);

      /* store interpretation of conditional */
      if (consp(clauses_int))
        result = cons(cons(mcons4(cond,
                                  lc,
                                  test_int_head,
                                  clauses_int),
                           cdr(car(bodies_ints))),
                      result);
      else
        result = cons(cons(mcons4(i_no_case_cond,
                                  lc,
                                  fresh_unknown(),
                                  test_int_head),
                           cdr(car(bodies_ints))),
                      result);

      /* next interpretation */
      bodies_ints = cdr(bodies_ints);
    }
  //if (find(new_string("first_arg"),original_clauses)) 
  return result;
}


static Expr matched_alternative(Expr alt,
                                Expr constructor_name,
                                Expr typed_resurg,
                                Expr env)
{
  Expr case_types = nil;
  Expr alt_types = nil;
  Expr result;

  if (!member(constructor_name,car(alt)))
    return not_unifiable;

  while (consp(typed_resurg))
    {
      if (consp(car(typed_resurg)))
        case_types = cons(car(car(typed_resurg)),case_types);
      else
        case_types = cons(fresh_unknown(),case_types);
      typed_resurg = cdr(typed_resurg);
    }

  alt = cdr(alt);
  while (consp(alt))
    {
      alt_types = cons(car(car(alt)),alt_types);
      alt = cdr(alt);
    }

  result = unify(case_types,env,alt_types,nil);
  return result;
}


static int select_alternative(Expr lc,
                              Expr alts,                /* refreshed alts */
                              Expr constructor_name,
                              Expr typed_resurg,
                              Expr *env_addr)
{
  int i = 0;
  Expr first_alt = nil;
  Expr other_alts = nil;
  Expr new_env = nil;

  /* no alternative found yet */
  while (consp(alts) && first_alt == nil)
    {
      if ((new_env = matched_alternative(car(alts),constructor_name,typed_resurg,*env_addr))
          != not_unifiable)
        /* a first alternative has been found */
        first_alt = cons(new_integer(i),car(alts));
      alts = cdr(alts);
      i++;
    }

  if (first_alt == nil)
    {
      /* no alternative has been found */
      if (show_errors)
        {
          err_line_col(lc,"E037",
                       msgtext_no_alt_match[0]);
        }
      return -1;
    }
  else
    {
      /* a first alternative has been found. Try to find others */
      while (consp(alts))
        {
          if (matched_alternative(car(alts),constructor_name,typed_resurg,*env_addr) != not_unifiable)
            other_alts = cons(cons(new_integer(i),car(alts)),other_alts);
          alts = cdr(alts);
          i++;
        }

      if (other_alts == nil)
        {
          /* there is one and only one matching alternative: success */
          *env_addr = new_env;
          return integer_value(car(first_alt));
        }
      else
        {
          /* other_alts is ((i . alt) ...) */

          /* get all matching alternatives */
          other_alts = cons(first_alt,other_alts);
          if (show_errors)
            {
              err_line_col(lc,"E038",
                           msgtext_several_alt_matches[0]);
              show_alternatives(errfile,other_alts);
              fprintf(errfile,"%s",msgtext_several_alt_matches_2[0]);
              fprintf(errfile,"\n");
            }
          return -1;
        }
    }
}


Expr select_cond_interpretations    (Expr lc,
                                     Expr test,
                                     Expr constructor_name,
                                     Expr typed_resurg,
                                     Expr case_body,
                                     Expr else_term,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs)
{
  Expr already_refreshed = nil;
  Expr aux, test_int_head, test_type, alts, alt, new_ctxt;
  Expr terms_ints, new_seg, result, aux2, type_template;
//  Expr test_type_name; 
  int i;


  /* if required check for unused resurgent symbols */
  if (unused_resurg)
  {
    Expr rsyms = typed_resurg;
    Expr body_syms = _symbols_in_term(case_body);
    while (consp(rsyms))
    {
      Expr sym = consp(car(rsyms)) ? cdr(car(rsyms)) : car(rsyms);
      if ( is_string(sym)  &&  sym != pdstr__  &&  !member(sym, body_syms) )
        {
          warn_line_col(lc,   /* <lc> of conditional */
                        "W011",
                        str_format(msgtext_unused_named_resurgent[0],
                                   string_content(sym)));
        }
      rsyms = cdr(rsyms);
    }
  }

  /* get unique interpretation of test */
  aux = test_interpretation(lc, test, ctxt, env, tvs, &already_refreshed);
  if (aux == nil) return nil;

  /* extract information */
  test_int_head = car(aux);
  env = cdr(aux);
  test_type = type_from_interpretation(test_int_head,env);

  /* get name of type of test */
//  if (is_string(test_type))
//    test_type_name = test_type; 
//  else if (consp(test_type))
//    test_type_name = second(test_type);
  /* get refreshed alternatives of type of test */
  alts = get_alts(test_type,env,lc);
  aux = refresh(cons(test_type,alts),&already_refreshed);
  alts = cdr(aux);
  type_template = car(aux);

  /* must unify type of test with type template */
  env = unify(type_template,env,test_type,nil);

  /* we should have at least two alternatives (the user wrote 'else') */
  if (cdr(alts) == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E039",
                       msgtext_select_cond_with_one_alternative[0]);
        }
      return nil;
    }

  /* select the right alternative */
  i = select_alternative(lc,alts,constructor_name,typed_resurg,&env);   /* this may update 'env' */
  if (i == -1) return nil;    /* selection failed */

  /* get the alternative */
  alt = nth(new_integer(i),alts);

  /* alt = ((name ...) (type . name) ...) */

  /* prepare the context for body interpretation */
  new_seg = nil;
  aux = cdr(alt);          /* ((type . name) ...) */
  aux2 = typed_resurg;     /* (name (type . name) ...) */
  while(consp(aux))
    {
      Expr sym = consp(car(aux2)) ? cdr(car(aux2)) : car(aux2);
      new_seg = cons(cons(sym,
     car(car(aux))),  /* type of symbol */
       new_seg);


      if (no_preemption)
        {
          Expr hidden_entries = get_hidden_entries(sym,ctxt);
          if (hidden_entries != nil)
            {
              if (show_errors)
                {
                  warn_line_col(lc,"W040",
                               msgtext_hidden_variables[0]);
                  show_context(errfile,hidden_entries,env);
                }
              //return nil; 
            }
        }


      aux = cdr(aux);
      aux2 = cdr(aux2);
    }
  new_seg = hard_reverse(new_seg);
  new_ctxt = append(new_seg,ctxt);

  /* now 'i' is the index of the right alternative. Interpret body of case 
     and else term. */

  terms_ints = tuple_interpretations(list2(dummy,dummy),
                                     list2(case_body,else_term),
                                     list2(new_ctxt,ctxt),
                                     env,
                                     tvs,
                                     0/*1*/);      /* must have same type */
  if (terms_ints == nil) return nil;

  /* each interpretation found has the form ((<head1> <head2>) . <env>). 
     Keep only those with type(<head1>) = type(<head2>). */

  aux = aux2 = terms_ints;
  terms_ints = nil;
  while (consp(aux))
    {
      Expr env2 = unify(type_from_interpretation(car(car(car(aux))),cdr(car(aux))),
   cdr(car(aux)),
   type_from_interpretation(second(car(car(aux))),cdr(car(aux))),
   nil);
      if (env2 != not_unifiable)
 terms_ints = cons(cons(car(car(aux)),env2),terms_ints);
      aux = cdr(aux);
    }
  if (terms_ints == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E041",
                       msgtext_select_cond_incompatible_types[0]);
          // show_tuple_interpretations_types(errfile,aux2); 
          fprintf(errfile,"%s",msgtext_case_term[0]);
          show_interpretations_types(errfile,
                                     term_interpretations(dummy,case_body,new_ctxt,env,tvs,0));
          fprintf(errfile,"%s",msgtext_else_term[0]);
          show_interpretations_types(errfile,
                                     term_interpretations(dummy,else_term,ctxt,env,tvs,0));
        }
      return nil;
    }

     /* For each one, construct:

   ((select_cond_interp <lc> <test head> i <clause head> <head1> . <head2>) . <env>)

   where <clause head> is

    (<sym> (<type> . <resurgent sym>) ...)

  */
  result = nil;
  while (consp(terms_ints))
    {
      /* compute <clause head> */
      aux = cons(car(car(alt)),    /* name of alternative */
   new_seg);

      result = cons(cons(mcons7(select_cond_interp,
    lc,
    test_int_head,
    new_integer(i),
    aux,
    car(car(car(terms_ints))),
    second(car(car(terms_ints)))),
    cdr(car(terms_ints))),
      result);
      terms_ints = cdr(terms_ints);
    }

  return result;
}


/* the following selects, amongh a list of interpretations, those
   which are acceptable as a readable connection (including local 
   variables) */
Expr select_readable_connection_interpretations(Expr lc,
                                                Expr conn_ints,
                                                Expr env)
{
  Expr result, aux;

  aux = conn_ints;
  result = nil;
  while (consp(aux))
    {
      if (
           (consp(car(car(aux))) && (car(car(car(aux))) == mvar_access)) ||
           (is_readable_address_type(type_from_interpretation(car(car(aux)),cdr(car(aux))), cdr(car(aux)) ))
         )
 result = cons(car(aux),result);
      aux = cdr(aux);
    }

  /* If no interpretation left, the 'conn' term may not be interpreted
     as a connection. */
  if (result == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E042",
                       msgtext_cannot_interpret_as_readable_connection[0]);
          show_interpretations_types(errfile,conn_ints);
        }
      return nil;
    }

  return result;
}


Expr select_writable_connection_interpretations(Expr lc,
                                                Expr conn_ints)
{
  Expr result, aux;

  aux = conn_ints;
  result = nil;
  while (consp(aux))
    {
      if (
          (consp(car(car(aux))) && (car(car(car(aux))) == mvar_access)) ||
          (is_writable_address_type(type_from_interpretation(car(car(aux)),cdr(car(aux))),cdr(car(aux))))
         )
        result = cons(car(aux),result);
      aux = cdr(aux);
    }

  /* If no interpretation left, the 'conn' term may not be interpreted
     as a connection. */
  if (result == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E043",
                       msgtext_cannot_interpret_as_writable_connection[0]);
          show_interpretations_types(errfile,conn_ints);
        }
      return nil;
    }

  return result;
}


Expr select_exchangeable_connection_interpretations(Expr lc,
      Expr conn_ints)
{
  Expr result, aux;

  aux = conn_ints;
  result = nil;
  while (consp(aux))
    {
      Expr conn_type =
 type_from_interpretation(car(car(aux)),cdr(car(aux)));
      if (is_exchangeable_address_type(conn_type))
 result = cons(car(aux),result);
      aux = cdr(aux);
    }

  /* If no interpretation left, the 'conn' term may not be interpreted
     as a connection. */
  if (result == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E044",
                       msgtext_cannot_interpret_as_exchangeable_connection[0]);
          show_interpretations_types(errfile,conn_ints);
        }
      return nil;
    }

  return result;
}


/* Interpreting a 'read' term, i.e. of the form '*t', where t is a
   term which must represent a readable connection or a local variable. 
*/
Expr read_interpretations(Expr lc,
     Expr ttype,
     Expr conn,
     Expr ctxt,
     Expr env,
     Expr tvs)
{
  Expr aux, conn_ints, result;

  /* conn may arrives in the form of any term. We keep only its
     interpretations whose type is acceptable for a readable connection 
     (including local variables). */

  aux = term_interpretations(dummy,conn,ctxt,env,tvs,1);

  if ((conn_ints = select_readable_connection_interpretations(lc,aux,env)) == nil)
    return nil;

  /* for each interpretation 'Iconn' of 'conn' we have the
     interpretation '(anb_read lc . Iconn)' of the read term. */
  result = nil;
  while (consp(conn_ints))
    {
      result =
 cons(cons(mcons3(anb_read,lc,car(car(conn_ints))),cdr(car(conn_ints))),result);
      conn_ints = cdr(conn_ints);
    }

  return result;
}


Expr write_interpretations(Expr lc,
      Expr ttype,
      Expr conn,     /* connection (including local variables) */
      Expr value,
      Expr ctxt,
      Expr env,
      Expr tvs)
{
  Expr aux, conn_ints, val_ints, result, aux2;
  Expr conn_type, val_type, new_env;

  /* get all interpretations of 'conn' */
  aux = term_interpretations(dummy,conn,ctxt,env,tvs,1);

  /* keep only those which are acceptable for a writable connection. */
  if ((conn_ints = select_writable_connection_interpretations(lc,aux)) == nil)
    return nil;

  /* 'aux' is empty */

  /* get all interpretations of the value */
  if ((val_ints = term_interpretations(dummy,value,ctxt,env,tvs,0)) ==
      nil)
    return nil;

  /* for each interpretation of the connection, we construct the
     corresponding list of interpretations of the write term. */
  result = nil;
  aux = conn_ints;
  while (consp(aux))   /* for each interpretation of 'conn' */
    {
      aux2 = val_ints;
      while (consp(aux2))
 {
   conn_type =
     type_from_interpretation(car(car(aux)),cdr(car(aux)));
   val_type =
     type_from_interpretation(car(car(aux2)),cdr(car(aux2)));

   soft_dereference_type(conn_type,cdr(car(aux)));

   assert(is_address_type(conn_type,nil)); /* (type_?Addr . T) */

   new_env = unify(cdr(conn_type),
     cdr(car(aux)),
     val_type,
     cdr(car(aux2)));

   if (new_env != not_unifiable)
     {
       result =
  cons(cons(mcons4(anb_write,
     lc,
     car(car(aux)),
     car(car(aux2))),
     new_env),
       result);
     }

   aux2 = cdr(aux2); /* next interpretation of value */
 }
      aux = cdr(aux);  /* next interpretation of 'conn' */
    }

  if (result == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E045",
                       msgtext_incompatible_write_type[0]);
          show_interpretations_types(errfile,conn_ints);
          fprintf(errfile,"%s",
                  msgtext_incompatible_write_type2[0]);
          show_interpretations_types(errfile,val_ints);
        }
    }

  return result;
}


Expr exchange_interpretations(Expr lc,
      Expr ttype,
      Expr conn,     /* connection (including local variables) */
      Expr value,
      Expr ctxt,
      Expr env,
      Expr tvs)
{
  Expr aux, conn_ints, val_ints, result, aux2;
  Expr conn_type, val_type, new_env;

  /* get all interpretations of 'conn' */
  aux = term_interpretations(dummy,conn,ctxt,env,tvs,1);

  /* keep only those which are acceptable for a exchangeable connection. */
  if ((conn_ints = select_exchangeable_connection_interpretations(lc,aux)) == nil)
    return nil;

  /* 'aux' is empty */

  /* get all interpretations of the value */
  if ((val_ints = term_interpretations(dummy,value,ctxt,env,tvs,0)) ==
      nil)
    return nil;

  /* for each interpretation of the connection, we construct the
     corresponding list of interpretations of the write term. */
  result = nil;
  aux = conn_ints;
  while (consp(aux))   /* for each interpretation of 'conn' */
    {
      aux2 = val_ints;
      while (consp(aux2))
 {
   conn_type =
     type_from_interpretation(car(car(aux)),cdr(car(aux)));
   val_type =
     type_from_interpretation(car(car(aux2)),cdr(car(aux2)));

   soft_dereference_type(conn_type,cdr(car(aux)));

   assert(is_address_type(conn_type,nil)); /* (type_?Addr . T) */

   new_env = unify(cdr(conn_type),
     cdr(car(aux)),
     val_type,
     cdr(car(aux2)));

   if (new_env != not_unifiable)
     {
       result =
  cons(cons(mcons4(anb_exchange,
     lc,
     car(car(aux)),
     car(car(aux2))),
     new_env),
       result);
     }

   aux2 = cdr(aux2); /* next interpretation of value */
 }
      aux = cdr(aux);  /* next interpretation of 'conn' */
    }

  if (result == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E046",
                       msgtext_incompatible_write_type[0]);
          show_interpretations_types(errfile,conn_ints);
          fprintf(errfile,"%s",
                  msgtext_incompatible_write_type2[0]);
          show_interpretations_types(errfile,val_ints);
        }
    }

  return result;
}


Expr wait_for_interpretations (Expr lc,
          Expr ttype,
          Expr condition,
                               Expr milliseconds,
          Expr after,
          Expr ctxt,
          Expr env,
          Expr tvs)
{
  Expr cond_ints, bool_cond_ints, after_ints, aux, result, ms_ints, word32_ms_ints;

  /* interpret condition (its type must be 'Bool') */
  cond_ints = term_interpretations(dummy,condition,ctxt,env,tvs,0);
  if (cond_ints == nil) return nil;

  /* select only those interpretations which are of type 'Bool' */
  aux = cond_ints;
  bool_cond_ints = nil;
  while (consp(aux))
    {
      if (same_type(type_from_interpretation(car(car(aux)),cdr(car(aux))),
                    cdr(car(aux)),
                    pdstr_Bool,
                    nil))
 bool_cond_ints = cons(car(aux),bool_cond_ints);
      aux = cdr(aux);
    }

  /* we should have at least one interpretation of type 'Bool' */
  if (bool_cond_ints == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E053",
                       msgtext_wait_condition_not_boolean[0]);
          show_interpretations_types(errfile,cond_ints);
        }
      return nil;
    }

  /* we should not have several interpretations of type 'Bool' */
  if (cdr(bool_cond_ints) != nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E054",
                       msgtext_wait_condition_ambiguous[0]);
          show_simple_ambiguity(errfile,bool_cond_ints);
        }
      return nil;
    }

  /* update 'env' with the environment of the unique interpretation of 
     the condition */
  env = cdr(car(bool_cond_ints));

  /* do the same for milliseconds */

  /* interpret condition (its type must be 'Word32') */
  ms_ints = term_interpretations(dummy,milliseconds,ctxt,env,tvs,0);
  if (ms_ints == nil) return nil;

  /* select only those interpretations which are of type 'Word32' */
  aux = ms_ints;
  word32_ms_ints = nil;
  while (consp(aux))
    {
      if (type_from_interpretation(car(car(aux)),cdr(car(aux))) == pdstr_Word32)
 word32_ms_ints = cons(car(aux),word32_ms_ints);
      aux = cdr(aux);
    }

  /* we should have at least one interpretation of type 'Word32' */
  if (word32_ms_ints == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E055",
                       msgtext_wait_milliseconds_not_integer[0]);
          show_interpretations_types(errfile,ms_ints);
        }
      return nil;
    }

  /* we should not have several interpretations of type 'Word32' */
  if (cdr(word32_ms_ints) != nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E056",
                       msgtext_wait_milliseconds_ambiguous[0]);
          show_simple_ambiguity(errfile,word32_ms_ints);
        }
      return nil;
    }

  /* update 'env' with the environment of the unique interpretation of 
     'milliseconds' */
  env = cdr(car(word32_ms_ints));

  /* now, we have to interpret the 'after condition' term (in the same context) */
  after_ints = term_interpretations(dummy,after,ctxt,env,tvs,0);
  if (after_ints == nil) return nil;

  /* finally, we have one interpretation for each interpretation of the
     after term */
  result = nil;
  while (consp(after_ints))
    {
      /* each interpretation head is (wait_for lc Icond Itime . Iafter) */
      result = cons(cons(mcons5(wait_for,
    lc,
    car(car(bool_cond_ints)),
                                car(car(word32_ms_ints)),
    car(car(after_ints))),
    cdr(car(after_ints))),
      result);
      after_ints = cdr(after_ints);
    }
  return result;
}


Expr delegate_interpretations (Expr lc,
                               Expr ttype,
                               Expr delegated,
                               Expr body,
                               Expr ctxt,
                               Expr env,
                               Expr tvs)
{
  /* 'delegate u, v' is correct if 'u' has a unique interpretation of type
     'One', and if 'v' may be interpreted. */

  Expr deleg_ints, one_deleg_ints, body_ints, aux, result;

  /* interpret delegated (its type must be 'One') */
  deleg_ints = term_interpretations(dummy,delegated,ctxt,env,tvs,0);
  if (deleg_ints == nil) return nil;

  /* select only those interpretations which are of type 'One' */
  aux = deleg_ints;
  one_deleg_ints = nil;
  while (consp(aux))
    {
      if (type_from_interpretation(car(car(aux)),cdr(car(aux))) == pdstr_One)
        one_deleg_ints = cons(car(aux),one_deleg_ints);
      aux = cdr(aux);
    }

  /* we should have at least one interpretation of type 'One' */
  if (one_deleg_ints == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E057",
                       msgtext_delegated_not_one[0]);
          show_interpretations_types(errfile,deleg_ints);
        }
      return nil;
    }

  /* we should not have several interpretations of type 'One' */
  if (cdr(one_deleg_ints) != nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E058",
                       msgtext_delegated_ambiguous[0]);
          show_simple_ambiguity(errfile,one_deleg_ints);
        }
      return nil;
    }

  /* update 'env' with the environment of the unique interpretation of 
     the delegated term */
  env = cdr(car(one_deleg_ints));

  /* now, we have to interpret the 'body' term (in the same context) */
  body_ints = term_interpretations(dummy,body,ctxt,env,tvs,0);
  if (body_ints == nil) return nil;

  /* finally, we have one interpretation for each interpretation of the
     body term */
  result = nil;
  while (consp(body_ints))
    {
      /* each interpretation head is (delegate lc Ideleg . Ibody) */
      result = cons(cons(mcons4(delegate,
                                lc,
                                car(car(one_deleg_ints)),
                                car(car(body_ints))),
                         cdr(car(body_ints))),
                    result);
      body_ints = cdr(body_ints);
    }
  return result;
}


Expr delegatep_interpretations (Expr lc,
                                Expr ttype,
                                Expr priority,
                                Expr delegated,
                                Expr body,
                                Expr ctxt,
                                Expr env,
                                Expr tvs)
{
  /* 'delegate u, v' is correct if 'u' has a unique interpretation of type
     'One', and if 'v' may be interpreted. */

  Expr priority_ints, word8_priority_ints, deleg_ints, one_deleg_ints, body_ints, aux, result;

  /* interpert priority (its type must be Word8) */
  priority_ints = term_interpretations(dummy,priority,ctxt,env,tvs,0);
  if (priority_ints == nil) return nil;

  /* select only those interpretations which are of type 'Word8' */
  aux = priority_ints;
  word8_priority_ints = nil;
  while (consp(aux))
  {
    if (type_from_interpretation(car(car(aux)),cdr(car(aux))) == pdstr_Word8)
      word8_priority_ints = cons(car(aux),word8_priority_ints);
    aux = cdr(aux);
  }

  /* we should have at least one interpretation of type 'Word8' */
  if (word8_priority_ints == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E123",
                       msgtext_priority_not_word8[0]);
          show_interpretations_types(errfile,priority_ints);
        }
      return nil;
    }

  /* we should not have several interpretations of type 'Word8' */
  if (cdr(word8_priority_ints) != nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E124",
                       msgtext_priority_ambiguous[0]);
          show_simple_ambiguity(errfile,word8_priority_ints);
        }
      return nil;
    }

  /* update 'env' with the environment of the unique interpretation of 
     the delegated term */
  env = cdr(car(word8_priority_ints));

  /* interpret delegated (its type must be 'One') */
  deleg_ints = term_interpretations(dummy,delegated,ctxt,env,tvs,0);
  if (deleg_ints == nil) return nil;

  /* select only those interpretations which are of type 'One' */
  aux = deleg_ints;
  one_deleg_ints = nil;
  while (consp(aux))
    {
      if (type_from_interpretation(car(car(aux)),cdr(car(aux))) == pdstr_One)
        one_deleg_ints = cons(car(aux),one_deleg_ints);
      aux = cdr(aux);
    }

  /* we should have at least one interpretation of type 'One' */
  if (one_deleg_ints == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E057",
                       msgtext_delegated_not_one[0]);
          show_interpretations_types(errfile,deleg_ints);
        }
      return nil;
    }

  /* we should not have several interpretations of type 'One' */
  if (cdr(one_deleg_ints) != nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E058",
                       msgtext_delegated_ambiguous[0]);
          show_simple_ambiguity(errfile,one_deleg_ints);
        }
      return nil;
    }

  /* update 'env' with the environment of the unique interpretation of 
     the delegated term */
  env = cdr(car(one_deleg_ints));

  /* now, we have to interpret the 'body' term (in the same context) */
  body_ints = term_interpretations(dummy,body,ctxt,env,tvs,0);
  if (body_ints == nil) return nil;

  /* finally, we have one interpretation for each interpretation of the
     body term */
  result = nil;
  while (consp(body_ints))
    {
      /* each interpretation head is (delegatep lc Ipriority Ideleg . Ibody) */
      result = cons(cons(mcons5(delegatep,
                                lc,
                                car(car(word8_priority_ints)),
                                car(car(one_deleg_ints)),
                                car(car(body_ints))),
                         cdr(car(body_ints))),
                    result);
      body_ints = cdr(body_ints);
    }
  return result;
}


#ifdef toto
Expr set_interpretations            (Expr lc,
         Expr ttype,
         Expr x,
         Expr type,
         Expr body,
         Expr ctxt,
         Expr env,
         Expr tvs)
{
  Expr aux, body_ints, omega_body_ints, result;

  /* check the declared type */
  if (!check_explicit_type(lc,type,tvs)) return nil;

  /* interpret the body in the right context */
  body_ints = term_interpretations(dummy,body,cons(cons(x,type),ctxt),env,tvs,0);

  /* keep only those interpretations whose type is type_Omega */
  aux = body_ints;
  omega_body_ints = nil;
  while (consp(aux))
    {
      if (type_from_interpretation(car(car(aux)),cdr(car(aux))) == type_Omega)
 omega_body_ints = cons(car(aux),omega_body_ints);
      aux = cdr(aux);
    }

  /* check for ambiguities */
  if (omega_body_ints == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E059",
                       msgtext_no_omega_interpretation[0]);
          show_interpretations_types(errfile,body_ints);
        }
      return nil;
    }

  if (length(omega_body_ints) > 1)
    {
      if (show_errors)
        {
          err_line_col(lc,"E060",
                       msgtext_several_omega_interpretations[0]);
          show_interpretations_types(errfile,omega_body_ints);
        }
      return nil;
    }

  /* construct the list of interpretations */
  result = nil;
  while (consp(omega_body_ints))
    {
      result = cons(cons(mcons5(set,lc,x,type,car(car(omega_body_ints))),
    cdr(car(omega_body_ints))),
      result);
      omega_body_ints = cdr(omega_body_ints);
    }

  return result;
}
#endif


Expr serialize_interpretations      (Expr lc,
                                     int allow_serialize_Opaque,
                                     Expr ttype,
                                     Expr datum,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs)
{
  Expr datum_ints;

  /* interpret the datum to be serialized */
  datum_ints = term_interpretations(dummy,datum,ctxt,env,tvs,0);
  if (datum_ints == nil) return nil;

  /*
  if (has_Opaque(type_from_interpretation(car(car(datum_ints)),cdr(car(datum_ints)))))
    {
      if (!allow_serialize_Opaque)
        {
          err_line_col(lc,"E117",
                       msgtext_Opaque_not_serializable[0]);
          return nil; 
        }
    }
  */

  /* Here, there  is a problem, because  at that point it  is not possible to  know if the
     type is actually  serializable, because it may contain  parameters. Hence, we content
     ourself with types which may be serializable. If after instanciating unknowns (in the
     compilation phase) the type appear as  non serializable, a message will be sent. This
     is the reason why, we must keep lc in the interpretation.
  */

  if (cdr(datum_ints) != nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E061",
                       msgtext_serialize_ambiguous[0]);
          show_interpretations_types(errfile,datum_ints);
        }
      return nil;
    }

  /* now we may construct the interpretations list, which has the form:

        (((serialize lc . head) . env))

  */
  return list1(cons(mcons3(serialize, //allow_serialize_Opaque ? tempserialize : serialize,
      lc,
      car(car(datum_ints))),
      cdr(car(datum_ints))));
}


Expr unserialize_interpretations    (Expr lc,
                                     int allow_serialize_Opaque,
                                     Expr ttype,
                                     Expr bytes,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs)
{
  Expr bytes_ints, aux, byte_array_ints;

  /* interpret 'bytes'. */
  bytes_ints = term_interpretations(dummy,bytes,ctxt,env,tvs,0);
  if (bytes_ints == nil) return nil;

  /* keep only those interpretations whose type is 'ByteArray' or 'TempByteArray' */
  aux = bytes_ints;
  byte_array_ints = nil;
  while (consp(aux))
    {
      Expr new_env;
      Expr type = type_from_interpretation(car(car(aux)),cdr(car(aux)));

      new_env = unify(type,
                      cdr(car(aux)),
                      type_ByteArray, //allow_serialize_Opaque ? pdstr_TempByteArray : type_ByteArray,
                      nil);
      if (new_env != not_unifiable)
        byte_array_ints = cons(cons(car(car(aux)),new_env),
                               byte_array_ints);

      aux = cdr(aux);
    }


  /* 'bytes' must have one and only one interpretation of type 'ByteArray' or 'TempByteArray' */
  if (byte_array_ints == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E062",
                       //allow_serialize_Opaque ? 
                       //msgtext_no_TempByteArray_interpretation[0] :
                       msgtext_no_ByteArray_interpretation[0]);
          show_interpretations_types(errfile,bytes_ints);
        }
      return nil;
    }

  if (cdr(byte_array_ints) != nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E063",
                       //allow_serialize_Opaque ? 
                       //msgtext_several_TempByteArray_interpretations[0] :
                       msgtext_several_ByteArray_interpretations[0]);
          show_interpretations_types(errfile,byte_array_ints);
        }
      return nil;
    }

  /* now 'bytes'  has one  interpretation of  type 'ByteArray'. However,  the type  of the
     result is not known. Hence, we put a fresh unknown for it. This will be resolved (for
     example) if the 'unserialize' term is explicitly typed.

     The interpretation head has the form:

       (unserialize <lc> <type> . <head>)

     where <lc> is  needed to check the serializability of <type>  later, and where <head>
     is the interpretation head of 'bytes'.
  */

  return list1(cons(mcons4(unserialize, //allow_serialize_Opaque ? tempunserialize : unserialize,
      lc,
      fresh_unknown(),
      car(car(byte_array_ints))),
      cdr(car(byte_array_ints))));
}


Expr protect_interpretations        (Expr lc,
                                     Expr target_type,
                                     Expr term,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs)
{
  Expr ints, aux;

  ints = term_interpretations(dummy,term,ctxt,env,tvs,0);
  if (ints == nil) return nil;

  aux = ints;
  ints = nil;
  while (consp(aux))
    {
      ints = cons(cons(mcons3(protect,lc,car(car(aux))),cdr(car(aux))),ints);
      aux = cdr(aux);
    }
  return ints;
}


Expr lock_interpretations           (Expr lc,
                                     Expr target_type,
                                     Expr lockedfile,
                                     Expr term,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs)
{
  Expr fnints, sfnints, ints, aux, result;

  fnints = term_interpretations(dummy,lockedfile,ctxt,env,tvs,0);
  if (fnints == nil) return nil;

  /* should have only one interpretation of type String */
  aux = fnints;
  sfnints = nil;
  while (consp(aux))
    {
      if (type_from_interpretation(car(car(aux)),cdr(car(aux))) == type_String)
        sfnints = cons(car(aux),sfnints);
      aux = cdr(aux);
    }

  /* should have at least one String interpretation */
  if (sfnints == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E064",
                       msgtext_lock_no_string_interpretation[0]);
          show_interpretations(errfile,fnints);
        }
      return nil;
    }

  /* should not have several String interpretations */
  if (cdr(sfnints) != nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E065",
                       msgtext_lock_several_string_interpretations[0]);
          show_interpretations(errfile,sfnints);
        }
      return nil;
    }

  /* interpret body of 'lock filename, body' */
  ints = term_interpretations(dummy,term,ctxt,cdr(car(sfnints)),tvs,0);
  if (ints == nil) return nil;

  /* construct resulting interpretations */
  result = nil;
  while (consp(ints))
    {
      result = cons(cons(mcons4(lock,lc,car(car(sfnints)),car(car(ints))),
                         cdr(car(ints))),
                    result);
      ints = cdr(ints);
    }
  return result;
}


Expr alt_number_interpretations     (Expr lc,
                                     Expr target_type,
                                     Expr term,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs)
{
  Expr ints, aux, kints ;

  ints = term_interpretations(dummy,term,ctxt,env,tvs,0);
  if (ints == nil) return nil;

  aux = ints;
  kints = nil;
  while (consp(aux))
    {
      if (is_sum_type(type_from_interpretation(car(car(aux)),cdr(car(aux))),cdr(car(aux))))
        kints = cons(cons(mcons3(alt_number,lc,car(car(aux))),cdr(car(aux))),kints);
      aux = cdr(aux);
    }

  if (kints == nil)
    {
      if (show_errors)
        {
          err_line_col(lc,"E066",
                       msgtext_alt_number[0]);
          show_interpretations_types(errfile,ints);
        }
      return nil;
    }

  return kints;
}


Expr vcopy_interpretations(Expr lc,
                           Expr n,
                           Expr init,
                           Expr ctxt,
                           Expr env,
                           Expr tvs)
{
  Expr n_ints, n_int, init_ints, result;

  /* interpret n which must be an 'Word32' */
  n_ints = term_interpretations(dummy,n,ctxt,env,tvs,0);
  if (n_ints == nil) return nil;

  /* we must have only one interpretation of type Word32 */
  n_int = select_unique_interpretation(lc,n_ints,pdstr_Word32,env);
  if (n_int == nil) return nil;

  /* update env */
  env = cdr(n_int);

  /* interpret 'init' */
  init_ints = term_interpretations(dummy,init,ctxt,env,tvs,0);
  if (init_ints == nil) return nil;

  /* if  the interpretation of  n is  (hn .  env), for  each interpretation  (hi .  ei) of
     'init', construct the interpretation ((vcopy hn . hi) . ei) */
  result = nil;
  while (consp(init_ints))
    {
      result = cons(cons(mcons3(vcopy,car(n_int),car(car(init_ints))),cdr(car(init_ints))),result);
      init_ints = cdr(init_ints);
    }
  return result;
}


Expr bit_width_interpretations      (Expr lc,
                                     Expr type,
                                     Expr ctxt,
                                     Expr env,
                                     Expr tvs)
{
  /* check the type */
  if (!check_explicit_type(lc,type,tvs)) return nil;

  /* make the interpretation */
  return list1(cons(cons(bit_width,type),env));
}


/* Tool: checking if an Expr contains parameters or unknowns (aka type_variables (see compil.h) ) */
int has_parameters_or_unknowns(Expr e)
{
  if (consp(e))
  {
    return (has_parameters_or_unknowns(car(e)) || has_parameters_or_unknowns(cdr(e)));
  }
  else if is_type_variable(e) return 1;
  else return 0;
}


Expr type_desc_interpretations       (Expr lc,
                                      Expr type,
                                      Expr ctxt,
                                      Expr env,
                                      Expr tvs)
{
   /* It is not possible to compute the type description at that point, because 
      the type here is always '$T' (search for +++type_desc in 'predef.anubis') 
   
      Hence, despite the fact that the result is a string, the interpretation list is 
      just:  ((type_desc_interp <lc> . <type>) . env)
   */
  return list1(cons(mcons3(type_desc_interp,lc,type),env));
}


Expr definition_of_type_interpretations   (Expr   lc,
                                           Expr   type_name,        /* term of type String */
                                           Expr   ctxt,
                                           Expr   env,
                                           Expr   tvs)
{
  /* interpret type_name and keep only those interpretation which are of type String */

  assert(0);
  return nil;


}


Expr definition_of_term_interpretations   (Expr   lc,
                                           Expr   type_term,      /* term of type AnubisType */
                                           Expr   term_name,      /* term of type String */
                                           Expr   ctxt,
                                           Expr   env,
                                           Expr   tvs)
{
  assert(0);
  return nil;
}