*** empty log message ***

* empty log message *
Alain Prouté
1 parent a832582f
Showing 4 changed files with 460 additions and 94 deletions Show diff stats
anubis_dev/compiler2/src/common.anubis
anubis_dev/compiler2/src/dictionary_1.anubis
anubis_dev/compiler2/src/memory_1.anubis
anubis_dev/compiler2/src/shift_replace_2.anubis
@@ -38,7 +38,8 @@
    interpretations are computed.
 public type WeakExpr:...
-   
+public type StrongType:...
+public type StrongTerm:...   
@@ -57,6 +58,7 @@ public type WeakExpr:...
 public type Position:
+   predefined, 
    position(String    absolute_path,
             Nat       line_number, 
             Nat       column_number). 
@@ -203,8 +205,12 @@ public type WeakExpr:
    local_def      (Position          position, 
                    WeakExpr          symbol, 
                    WeakExpr          value, 
-                   WeakExpr          body). 
+                   WeakExpr          body),
+   
+   strong_type    (StrongType), 
+   strong_term    (StrongTerm). 
+   The alternatives 'strong_type' and 'strong_term' are needed by predefinitions. 
    The list of valid signs may be found in the file 'lexer_1.anubis'.
@@ -29,13 +29,22 @@
    Dictionaries  are  the  places  where  the  compiler  stores  its  'knowledge'.   These
    dictionaries are  saved to files,  so as to  be used at  the next compilation.   When a
    dictionary is retrieved  at the next compilation, obsolete  entries are discarded. This
-   is decided according  to dependancies between modules and  dates of last modifications.
-   Hence, unchanged modules are not recompiled.
+   is decided according to dependancies between modules and dates of last modifications.
+   
+   Hence, unmodified modules are not recompiled.
    ----------------------------------- Table of Contents ---------------------------------
+   *** (1) Creating dictionaries.
+   *** (2) Getting the size of a dictionary (number of non empty entries).
+   *** (3) Updating all non empty entries in a dictionary according to a method. 
+   *** (4) Adding entries to a dictionary.
+   *** (5) Getting entries from a dictionary. 
+   *** (6) Saving a dictionary. 
+   *** (7) Renumberings. 
+   *** (8) Retrieving a dictionary. 
    ---------------------------------------------------------------------------------------
@@ -64,7 +73,8 @@ public define Dictionary1($Entry,$Key1)
      (
        Int32                     bits_of_hash, 
        String                    dictionary_name, 
-       $Entry -> $Key1           compute_key1
+       $Entry -> $Key1           compute_key1,
+       $Entry                    empty_entry
      ). 
    The integer 'bits_of_hash' is the number of bits used for hashing keys. A value between
@@ -80,13 +90,14 @@ public define Dictionary2($Entry,$Key1,$Key2)
        Int32                     bits_of_hash, 
        String                    dictionary_name, 
        $Entry -> $Key1           compute_key1,
-       $Entry -> $Key2           compute_key2
+       $Entry -> $Key2           compute_key2,
+       $Entry                    empty_entry
      ). 
-   *** (2) Getting the size of a dictionary (number of non empty entries):
+   *** (2) Getting the size of a dictionary (number of non empty entries).
    Dictionaries are always filled  up from slot 0. Free slots are  above the most recently
    filled up one. The next functions return the number of filled up (non empty) entries. 
@@ -128,10 +139,11 @@ public define One
+
    *** (4) Adding entries to a dictionary.
-   One may add a new entry to a dictionary, using the following tools:
+   We can add a new entry to a dictionary, using the following tools:
 public define One    
    add_entry
@@ -154,18 +166,18 @@ public define One
    *** (5) Getting entries from a dictionary. 
-   Entries may be got by id or by key.  If  an entry is got by id, it is unique or does'nt
-   exist, hence  a result of  type 'Maybe($Entry)'.  If  it is got  by key, the  number of
-   entries is arbitrary (including 0), hence a result of type 'List($Entry)'.
+   Entries may be got by  id or by key.  If an entry is got by  id, it is unique (and must
+   exist), hence a result of type '$Entry'.  If it is got by key, the number of entries is
+   arbitrary (including 0), hence a result of type 'List($Entry)'.
-public define Maybe($Entry)
+public define $Entry
    get_entry
      (
        Dictionary1($Entry,$Key1)          dictionary, 
        Int32                              id   
      ).
-public define Maybe($Entry)
+public define $Entry
    get_entry
      (
        Dictionary2($Entry,$Key1,$Key2)    dictionary, 
@@ -199,8 +211,8 @@ public define List($Entry)
    *** (6) Saving a dictionary. 
    The  dictionary is  saved in  the current  directory in  the sens  of the  host system,
-   i.e. in the directory from where the compiler has been started. The name of the file is
-   the name of the dictionary, with the extension ".dictionary" appended.
+   i.e. in the directory  the compiler has been started from. The name  of the file is the
+   name of the dictionary, with the extension ".dictionary" appended.
 public define One
    save
@@ -223,9 +235,9 @@ public define One
    When a  dictionary is retrieved at the  beginning of a new  compilation, source modules
    may have changed since the last  compilation. Hence, some entries in the dictionary may
-   be obsolete. For this  reason, we must provide a function for  dicarding or updating an
-   entry.  This has the effect of renumbering the entries.  The correspondance between old
-   ids and new ids is given by a datum of type 'Renumbering($Entry)'.
+   be  obsolete. For  this  reason, we  must  provide a  function  for dicarding  obsolete
+   entries.  This has  the effect of renumbering the  entries.  The correspondance between
+   old ids and new ids is given by a datum of type 'Renumbering($Entry)'.
 public type Renumbering($Entry):...
@@ -239,7 +251,8 @@ public define Renumbering($Entry)
        Int32       number_of_entries
      ). 
-   The next tool gives the size (number of old ids) in a renumbering. 
+   The  next tool  gives  the size  (number  of old  ids, including  those  which have  no
+   corresponding new id) in a renumbering.
 public define Int32
    size
@@ -250,17 +263,17 @@ public define Int32
    For getting a new id knowing the old  id, we use one of the following, depending on the
-   fact that we knwo that the new id exists or not.
+   fact that we know that the new id exists or not.
 public define Int32
-   new_id
+   new_id                   // if we know that the new id exists
      (
        Renumbering($Entry)   renumbering, 
        Int32                 old_id
      ). 
 public define Maybe(Int32)
-   maybe_new_id
+   maybe_new_id             // if we don't know if the new id exists
      (
        Renumbering($Entry)   renumbering, 
        Int32                 old_id
@@ -286,7 +299,8 @@ public define Maybe((Dictionary1($Entry,$Key),Renumbering($Entry)))
        Int32                       bits_of_hash, 
        String                      name,
        $Entry -> $Key              compute_key,
-       $Entry -> KeepOrDiscard     discard
+       $Entry -> KeepOrDiscard     discard,
+       $Entry                      empty_entry
      ). 
 public define Maybe((Dictionary2($Entry,$Key1,$Key2),Renumbering($Entry)))
@@ -296,12 +310,13 @@ public define Maybe((Dictionary2($Entry,$Key1,$Key2),Renumbering($Entry)))
        String                      name,
        $Entry -> $Key1             compute_key1,
        $Entry -> $Key2             compute_key2,
-       $Entry -> KeepOrDiscard     discard
+       $Entry -> KeepOrDiscard     discard,
+       $Entry                      empty_entry
      ). 
    A  result of  'failure' means  that some  problem has  been encountered,  and  that the
    dictionary must  be regenerated.  Otherwise, we get  the retrieved  dictionary together
-   with the correponding 'Renumbering($Entry)'. 
+   with the correponding 'Renumbering'. 
    Dictionaries usually depend  on each other. For example, an entry  in the dictionary of
    types contains  references by  id to entries  in the  dictionary of modules.   When all
@@ -321,6 +336,24 @@ read tools/basis.anubis
    ----------------------------------- Table of Contents ---------------------------------
+   *** [1] Dictionaries.
+   *** [2] Creating a dictionary.
+   *** [3] Updating all entries in a dictionary. 
+   *** [4] Adding an entry to the dictionary.
+   *** [5] Getting an entry from a dictionary. 
+      *** [5.1] Getting an entry by id. 
+      *** [5.2] Getting the list of ids associated to a key. 
+      *** [5.3] Getting an entry by key. 
+   *** [6] Saving a dictionary. 
+      *** [6.1] Writing bytes. 
+      *** [6.2] Saving all entries.
+      *** [6.3] Saving the whole dictionary. 
+   *** [7] Retrieving a dictionary. 
+      *** [7.1] Renumberings. 
+      *** [7.2] Reading a given number of bytes.
+      *** [7.3] Retrieving a single entry. 
+      *** [7.4] Retrieving a whole dictionary. 
+      *** [7.5] The two interfaces. 
    ---------------------------------------------------------------------------------------
@@ -341,17 +374,18 @@ public type Dictionary1($Entry,$Key1):
    The reason why 'main_table'  has a double level of 'Var' is that  we must first be able
    to add  an entry (this is  enabled by the 'MVar'),  and also to change  the whole table
-   when it needs to be enlarged (this is  enabled by the 'Var'). Of course, since an entry
-   may be 'empty', we use 'Maybe($Entry)' instead of '$Entry'.
-   
-   'next' is the  position of the next free  (empty) slot in the table. The  main table is
-   always filled up from the bottom, and an entry is never discarded.
+   when it needs to  be enlarged (this is enabled by the  'Var').  '*next' is the position
+   of the next free (empty) slot in the table. The main table is always filled up from the
+   bottom,  and an entry  is never  discarded.  All  slots starting  at index  '*next' are
+   'empty'. Actually they are filled up with a default 'empty entry'.
    'index1' is a 'hashtable'. The size of the table is '2^b' where 'b' is the given number
    of bits of hash.  In each slot, we have a (usually  small) association list, giving the
    correspondance between a key and the list of corresponding ids. 
+   The same one with 2 keys:
+   
 public type Dictionary2($Entry,$Key1,$Key2):
    dict
      (
@@ -438,23 +472,25 @@ public define Int32
-   *** [] Updating all entries in a dictionary. 
+   *** [3] Updating all entries in a dictionary. 
 define One
    update_all_entries    // auxiliary function
      (
        MVar(Maybe($Entry))        table,
        $Entry -> $Entry           method,
-       Int32                      i     // increasing index
+       Int32                      i,     // increasing index
+       Int32                      next   // number of non empty entries
      ) = 
-   if i >= length(table) then unique else   // end of the table
+   if i >= next then unique else  
    if *table(i) is 
      {
-       failure then unique,    // end of the table
+       failure then unique, 
        success(entry) then 
          table(i) <- success(method(entry)); 
-         update_all_entries(table,method,i+1)
+         update_all_entries(table,method,i+1,next)
      }.
+
 public define One
    update_all_entries
@@ -463,8 +499,9 @@ public define One
        $Entry -> $Entry           method
      ) = 
    if dictionary is dict(name,main_tab,next,idx,ckey,hkey) then
-   update_all_entries(*main_tab,method,0). 
+   update_all_entries(*main_tab,method,0,*next). 
+   
  public define One
    update_all_entries
      (
@@ -476,7 +513,7 @@ public define One
-   *** [3] Adding an entry to the dictionary.
+   *** [4] Adding an entry to the dictionary.
    First we have auxiliary  functions for updating the index. The first  one adds an index
    entry into a A-list with the index.
@@ -557,13 +594,47 @@ public define One
-   *** [4] Getting an entry from a dictionary. 
+   *** [5] Getting an entry from a dictionary. 
+
+   
+   
+   
+      *** [5.1] Getting an entry by id. 
+   
+public define $Entry
+   get_entry
+     (
+       Dictionary1($Entry,$Key1)          dictionary, 
+       Int32                              id   
+     ) = 
+   if dictionary is dict(name,main_tab,next,idx,ckey,hkey) then 
+   if *(*main_tab)(id) is 
+     {
+       failure then alert, 
+       success(entry) then entry
+     }.
+   
+   
+public define $Entry
+   get_entry
+     (
+       Dictionary2($Entry,$Key1,$Key2)    dictionary, 
+       Int32                              id   
+     ) =
+   if dictionary is dict(name,main_tab,next,idx1,idx2,ckey1,ckey2,hkey1,hkey2) then 
+   if *(*main_tab)(id) is 
+     {
+       failure then alert, 
+       success(entry) then entry
+     }.
+   
+   
-      *** [4.1] Tools. 
+      *** [5.2] Getting the list of ids associated to a key. 
-   This tool ('get_ids_from_index') retrieves the list of ids associated with a key, using
-   an index.
+   The tool 'get_ids_from_index' retrieves the list of ids associated with a key, using an
+   index.
 define List($U)
    assoc
@@ -592,31 +663,7 @@ define List(Int32)
-   
-      *** [4.2] Getting an entry by id. 
-   
-public define Maybe($Entry)
-   get_entry
-     (
-       Dictionary1($Entry,$Key1)          dictionary, 
-       Int32                              id   
-     ) = 
-   if dictionary is dict(name,main_tab,next,idx,ckey,hkey) then 
-   *(*main_tab)(id).
-   
-   
-public define Maybe($Entry)
-   get_entry
-     (
-       Dictionary2($Entry,$Key1,$Key2)    dictionary, 
-       Int32                              id   
-     ) =
-   if dictionary is dict(name,main_tab,next,idx1,idx2,ckey1,ckey2,hkey1,hkey2) then 
-   *(*main_tab)(id).
-   
-   
-
-      *** [4.3] Getting an entry by key. 
+      *** [5.3] Getting an entry by key. 
    'map_select' is defined in 'tools/basis.anubis'. 
@@ -660,7 +707,7 @@ public define List($Entry)
-   *** [5] Saving a dictionary. 
+   *** [6] Saving a dictionary. 
    Dictionaries are saved as follows into  the file 'name.dictionary', where 'name' is the
    name of the dictionary:
@@ -673,10 +720,12 @@ public define List($Entry)
-      *** [5.1] Writing bytes. 
+      *** [6.1] Writing bytes. 
    The tool below  writes all bytes of  the given 'ByteArray' into the  given file (recall
-   that 'write' may not write all bytes; see predefined.anubis).
+   that 'write' may not write all  bytes; see predefined.anubis).  If some problem arises,
+   there is  just nothing to  do, because the  file will be  inconsistant and at  the next
+   compilation the dictionary will be regenerated.
 define One
    write_all_bytes
@@ -695,7 +744,7 @@ define One
-      *** [5.2] Saving all entries.
+      *** [6.2] Saving all entries.
    The next function saves all entries (the number of entries is already saved). 
@@ -719,7 +768,7 @@ define One
-     *** [5.3] Saving the whole dictionary. 
+      *** [6.3] Saving the whole dictionary. 
    The next function saves the whole dictionary. 
@@ -764,25 +813,27 @@ public define One
-   *** [6] Retrieving a dictionary. 
+   *** [7] Retrieving a dictionary. 
-      *** [6.1] Renumberings. 
+      *** [7.1] Renumberings. 
 public type Renumbering($Entry):
    renum(MVar(Int32)). 
    As one  may see, the parameter  $Entry is not  used.  However, it enhances  the safety,
-   because it becomes it links the  renumbering to a specific type. Since all dictionaries
-   have distinct  types, it becomes impossible  to use one renumbering  instead of another
-   one.
+   because  it links  the renumbering  to  a specific  type. Since  all dictionaries  have
+   distinct types, it becomes impossible to use one renumbering instead of another one.
    By convention, within  a 'Renumbering', 0 represents an invalid id,  and each valid id,
-   say 'n' is represented as 'n+1'.
+   say 'n'  is represented  as 'n+1'.  It  would have  been cleaner to  use 'Maybe(Int32)'
+   instead of 'Int32', not using this  trick. However, the trick is encapsulated into this
+   section,  and  needs not  be  known  from the  outside.  Using  'Int32'  is better  for
+   performances, because 'Maybe(Int32)' is implemented as a 'mixed' type.
 public define Int32
-   new_id
+   new_id                  // when we are sure the new id exists
      (
        Renumbering($Entry)   renumbering, 
        Int32                 old_id
@@ -796,7 +847,7 @@ public define Int32
    else val - 1. 
 public define Maybe(Int32)
-   maybe_new_id
+   maybe_new_id           // when we are not sure the new id exists
      (
        Renumbering($Entry)   renumbering, 
        Int32                 old_id
@@ -844,7 +895,7 @@ public define Int32
-      *** [6.2] Reading a given number of bytes.
+      *** [7.2] Reading a given number of bytes.
    Reading exactly 'n' bytes from a file (this may fail of course). 
@@ -877,7 +928,7 @@ define Maybe(ByteArray)
-      *** [6.3] Retrieving a single entry. 
+      *** [7.3] Retrieving a single entry. 
    For retrieving an entry we must:
@@ -921,7 +972,7 @@ define Maybe($Entry)
-      *** [6.4] Retrieving a whole dictionary. 
+      *** [7.4] Retrieving a whole dictionary. 
    When calling this auxiliary function, the  number of entries has already been read, and
    the dictionary is already created and empty (partially filled up for recursive calls).
@@ -974,15 +1025,15 @@ define Maybe(($Dict,Renumbering($Entry)))
-   The two interfaces:
+      *** [7.5] The two interfaces. 
-define Maybe((Dictionary1($Entry,$Key),Renumbering($Entry)))
-   retrieve_dict
+public define Maybe((Dictionary1($Entry,$Key),Renumbering($Entry)))
+   retrieve_dictionary
      (
        Int32                       bits_of_hash, 
        String                      name,
        $Entry -> $Key              compute_key, 
-       $Entry -> KeepOrDiscard     discard   
+       $Entry -> KeepOrDiscard     discard
      ) =
    with file_name = name+".dictionary", 
    if file(file_name,read) is 
@@ -1009,14 +1060,14 @@ define Maybe((Dictionary1($Entry,$Key),Renumbering($Entry)))
      }.
-define Maybe((Dictionary2($Entry,$Key1,$Key2),Renumbering($Entry)))
-   retrieve_dict
+public define Maybe((Dictionary2($Entry,$Key1,$Key2),Renumbering($Entry)))
+   retrieve_dictionary
      (
        Int32                       bits_of_hash, 
        String                      name,
        $Entry -> $Key1             compute_key1, 
        $Entry -> $Key2             compute_key2, 
-       $Entry -> KeepOrDiscard     discard 
+       $Entry -> KeepOrDiscard     discard
      ) =
    with file_name = name+".dictionary", 
    if file(file_name,read) is 
@@ -1035,7 +1086,8 @@ define Maybe((Dictionary2($Entry,$Key1,$Key2),Renumbering($Entry)))
                                     0,   // initial old_id
                                     0,   // initial new_id
                                     discard,
-                                    create_dictionary(bits_of_hash,name,compute_key1,compute_key2),
+                                    create_dictionary(bits_of_hash,name,
+                                                      compute_key1,compute_key2),
                                     add_entry, 
                                     create_renumbering(number_of_entries))
                }
@@ -27,6 +27,7 @@ read tools/basis.anubis
 read tools/streams.anubis   
 read common.anubis
 read dictionary_1.anubis   
+read src_files_1.anubis   
    ----------------------------------- Table of Contents ---------------------------------
@@ -151,7 +152,8 @@ public type State:
      (
        List(Option)           options, 
        Dictionaries           dictionaries,
-       Var(List(OpenModule))  read_stack
+       Var(List(OpenModule))  read_stack,
+       List(List(String))     read_paths
      ). 
@@ -522,7 +524,7 @@ public define One
      (
        State  state
      ) = 
-   if state is cstate(options,dictionaries,read_stack) then 
+   if state is cstate(options,dictionaries,read_stack,read_paths) then 
    save(dictionaries). 
@@ -557,6 +559,16 @@ define List(Int32)
    Create an 'empty' state:
+define List(List(String))
+   get_read_paths
+     =
+   [
+      split_path(get_current_directory),
+      split_path(my_anubis_directory),
+      split_path(anubis_directory)
+   ]. 
+   
+   
 define State
    new_state
      (
@@ -570,7 +582,9 @@ define State
               create_dictionary(12, dat_dict_name,name),
               create_dictionary(12, thm_dict_name,pattern)
             ),
-          var([])). 
+          var([]),
+          get_read_paths
+         ). 
@@ -837,7 +851,8 @@ public define State
          update_thm_dictionary(thm_dict,mod_renum,typ_renum,dat_renum);
          cstate(options,
                 dictionaries(mod_dict,typ_dict,dat_dict,thm_dict),
-                var([]))
+                var([]),
+                get_read_paths)
      }. 
+   
+   
+                     _____              ___.   .__         ________  
+                    /  _  \   ____  __ _\_ |__ |__| ______ \_____  \ 
+                   /  /_\  \ /    \|  |  \ __ \|  |/  ___/  /  ____/ 
+                  /    |    \   |  \  |  / \_\ \  |\___ \  /       \ 
+                  \____|__  /___|  /____/|___  /__/____  > \_______ \
+                          \/ The \/  Anubis  \/    2   \/  Project \/
+   
+   
+   Name of this file:           shift_replace_2.anubis
+   
+   Purpose of this file:        Tools for shifting strong items and replacing de Bruijn 
+                                  symbols in strong items. 
+   
+   
+
+   Authors (Name [initials]):   Alain Proute'   [AP]
+   
+   Updates ([initials] (date) comment): 
+      [AP] (2007 jul 04) Creation of this file.
+   
+   ---------------------------------------------------------------------------------------   
+   
+read common.anubis
+   
+   
+   There two  fundamental operations we  must be able  to perform on strong  items (strong
+   terms and strong types). They are named 'shifting' and 'replacing'. 
+   
+   
+   
+   *** (1) Shifting. 
+   
+   A  strong item contains  occurrences of  'de Bruijn  symbols'. These  symbols represent
+   depths into the  stack of the virtual  machine. It is sometimes necessary  to 'shift' a
+   strong item  by a certain  number, say  'n'. The result  is meaningful relative  to any
+   extention  of  the  original  stack  obtained  by  pushing  'n'  data  on  top  of  the
+   stack. Notice that the stack is heterogeneous,  which means that the slots in the stack
+   do not have  the same size. Their size depends  only of the type of  the content of the
+   slot.
+   
+   For example, if 'E' is statement  (strong term of type 'Omega'), meaningful relative to
+   some strong context 'G' (representing the stack),  the result of shifting 'E' by '1' is
+   meaningful relative to any strong context of the form '[T . G]', where 'T' is any type.
+   
+public define StrongType shift(Int32 n, StrongType t). 
+public define StrongTerm shift(Int32 n, StrongTerm t). 
+   
+   Actually,  the operation  of shifting  by 'n'  just amounts  to add  'n' to  all depths
+   encountered in the strong item.
+   
+   
+   
+   
+   *** (2) Replacing.
+   
+   Given a  strong item 'E', we  may need to replace  all occurences of a  given de Bruijn
+   symbol by a given strong term. The result of replacing all occurrences of the de Bruijn
+   symbol 'x' by the strong term 'a' in a strong item 'E' is generally denoted 'E[a/x]' by
+   logicians  (read: 'E'  within which  'a'  replaces 'x').  The strong  item 'E[a/x]'  is
+   represented in this compiler by 'replace(E,a,x)'. 
+   
+public define StrongType replace(StrongType t, StrongTerm a, Int32 i).    
+public define StrongTerm replace(StrongTerm t, StrongTerm a, Int32 i).    
+   
+   Notice hat 'E[a/x]' is meaningful relative to the same strong context as 'E'. 
+   
+   
+   
+   --- That's all for the public part ! --------------------------------------------------
+   
+   
+   
+   Shifting a strong type. 
+   
+public define StrongType 
+   shift
+     (
+       Int32       n, 
+       StrongType  t
+     ) =
+   if t is 
+     {
+       _Parameter(String name) then
+          t, 
+   
+       _Defined(Int32 type_id,List(StrongType) operands) then
+         _Defined(type_id,
+                  map((StrongType st) |-> shift(n,st),
+                      operands)),
+   
+       _Product(List(StrongType) l) then
+         _Product(map((StrongType st) |-> shift(n,st),
+                      l)), 
+   
+       _Functional(StrongType source,StrongType target) then
+         _Functional(shift(n,source),shift(n,target)), 
+   
+       _Omega then
+         _Omega, 
+   
+       _Witness(StrongTerm statement) then
+         _Witness(shift(n,statement)), 
+   
+       _Quantified(String parameter,StrongType _T) then
+         _Quantified(parameter,shift(n,_T))
+     }. 
+   
+   
+   
+   Shifting a strong  term. 'n' is added to  a depth at the unique place  where depths are
+   found, i.e.  in  the alternative 'symbol'. Furthermore, shifting  the declarative terms
+   'lambda(...)' and  'forall(...)' requires a replacement because  the symbol 'symbol(0)'
+   must not be shifted (the replacement 'undoes' the shifting for this symbol).
+   
+public define StrongTerm 
+   shift
+     (
+       Int32         n, 
+       StrongTerm    t
+     ) =
+   if t is 
+     {
+       global(Int32 id) then
+         global(id),
+   
+       symbol(Int32 depth) then
+         symbol(depth + n), 
+   
+       tuple(List(StrongTerm) l) then
+         tuple(map((StrongTerm st) |-> shift(n,st),l)),
+   
+       proj(Int32 i,StrongTerm st) then
+         proj(i,shift(n,st)),
+   
+       incl(StrongType _T,Int32 i,StrongTerm st) then
+         incl(shift(n,_T),i,shift(n,st)), 
+   
+       cond(StrongType _T,StrongTerm test,List(StrongTerm) cases) then
+         cond(shift(n,_T),shift(n,test),
+              map((StrongTerm st) |-> shift(n,st),cases)),
+   
+       lambda(StrongType _T,StrongTerm st) then
+         lambda(shift(n,_T),replace(shift(n,st),symbol(0),n)),
+   
+       app(StrongTerm f,StrongTerm a) then
+         app(shift(n,f),shift(n,a)), 
+   
+       forall(StrongType _T,StrongTerm _E) then
+         forall(shift(n,_T),replace(shift(n,_E),symbol(0),n)),
+   
+       description(StrongTerm p) then
+         description(shift(n,p)), 
+   
+       property(StrongTerm p) then
+         property(shift(n,p)),
+   
+       choice(StrongTerm p) then
+         choice(shift(n,p)),
+   
+       parametric(String parameter,StrongTerm st) then
+         parametric(parameter,shift(n,st)), 
+   
+       parametric_app(StrongTerm st,StrongType _T) then
+         parametric_app(shift(n,st),shift(n,_T))
+     }. 
+   
+
+   
+   *** [] Replacement in strong types. 
+
+   _Parameter(N)[a/i]                  is  _Parameter(N)
+   _Defined(N,T_1,...,T_k)[a/i]        is  _Defined(N,T_1[a/i],...,T_k[a/i])
+   _Product(T_1,...,T_k)[a/i]          is  _Product(T_1[a/i],...,T_k[a/i])
+   _Functional(T,U)[a/i]               is  _Functional(T[a/i],U[a/i+1])
+   _Omega[a/i]                         is  _Omega
+   _Witness(E)[a/i]                    is  _Witness(E[a/i])
+   _Quantified($X T)[a/i]              is  _Quantified($X T[a/i])
+   
+   
+public define StrongType 
+   replace                       // computes 't[a/s(i)]'
+     (
+       StrongType         t, 
+       StrongTerm         a, 
+       Int32              i
+     ) = 
+   if t is 
+     {
+       _Parameter(String name) then
+         t, 
+   
+       _Defined(Int32 type_id,List(StrongType) operands) then
+         _Defined(type_id,
+                  map((StrongType st) |-> replace(st,a,i),
+                      operands)),
+   
+       _Product(List(StrongType) l) then
+         _Product(map((StrongType st) |-> replace(st,a,i),l)),
+   
+       _Functional(StrongType source,StrongType target) then
+         _Functional(replace(source,a,i),replace(target,a,i+1)),
+   
+       _Omega then
+         _Omega,
+   
+       _Witness(StrongTerm statement) then
+         _Witness(replace(statement,a,i)), 
+   
+       _Quantified(String parameter,StrongType _T) then
+         _Quantified(parameter,replace(_T,a,i))
+     }. 
+   
+   
+   
+   
+   *** [] Replacement in strong terms. 
+   
+   global(n)[a/i]                     is  global(n)
+   symbol(i)[a/i]                     is  a
+   symbol(i)[a/j]                     is  symbol(i)         (if i != j)
+   tuple(t_1,...,t_k)[a/i]            is  tuple(t_1[a/i],...,t_k[a/i])
+   proj(n,t)[a/i]                     is  proj(n,t[a/i])
+   incl(U,n,t)[a/i]                   is  incl(U[a/i],n,t[a/i])
+   cond(T,t,c_1,...,c_k)[a/i]         is  cond(T[a/i],t[a/i],c_1[a/i],...,c_k[a/i])
+   lambda(T,E)[a/i]                   is  lambda(T[a/i],E[a/i+1])
+   app(f,b)[a/i]                      is  app(f[a/i],b[a/i])
+   forall(T,E)[a/i]                   is  forall(T[a/i],E[a/i+1])
+   description(p)[a/i]                is  description(p[a/i])
+   property(p)[a/i]                   is  property(p[a/i])
+   choice(p)[a/i]                     is  choice(p[a/i])
+   parametric($X,t)[a/i]              is  parametric($X,t[a/i])
+   parametric_app(t,T)[a/i]           is  parametric_app(t[a/i],T[a/i])
+   
+   
+public define StrongTerm 
+   replace                     // computes 't[a/i]'
+     (
+       StrongTerm        t, 
+       StrongTerm        a, 
+       Int32             i
+     ) =
+   if t is 
+     {
+       global(Int32 id) then
+         t,
+   
+       symbol(Int32 depth) then
+         if depth = i then a else t,
+   
+       tuple(List(StrongTerm) l) then
+         tuple(map((StrongTerm st) |-> replace(st,a,i),l)),
+   
+       proj(Int32 i,StrongTerm st) then
+         proj(i,replace(st,a,i)),
+   
+       incl(StrongType _T,Int32 j,StrongTerm st) then
+         incl(replace(_T,a,i),j,replace(st,a,i)), 
+   
+       cond(StrongType _T,StrongTerm test,List(StrongTerm) cases) then
+         cond(replace(_T,a,i),replace(test,a,i),
+              map((StrongTerm c) |-> replace(c,a,i),cases)),
+   
+       lambda(StrongType _T,StrongTerm _E) then
+         lambda(replace(_T,a,i),replace(_E,a,i+1)), 
+   
+       app(StrongTerm f,StrongTerm b) then
+         app(replace(f,a,i),replace(b,a,i)),
+   
+       forall(StrongType _T,StrongTerm _E) then
+         forall(replace(_T,a,i),replace(_E,a,i+1)), 
+   
+       description(StrongTerm p) then
+         description(replace(p,a,i)), 
+   
+       property(StrongTerm p) then
+         property(replace(p,a,i)), 
+   
+       choice(StrongTerm p) then
+         choice(replace(p,a,i)), 
+   
+       parametric(String parameter,StrongTerm st) then
+         parametric(parameter,replace(st,a,i)),
+   
+       parametric_app(StrongTerm st,StrongType _T) then
+         parametric_app(replace(st,a,i),replace(_T,a,i))
+     }. 
+   
+
+   
+   
+   
 \ No newline at end of file