15.4.629  src/lib/compiler/front/typer/basics/debruijn-index.pkg

## debruijn-index.pkg 
#
# See overview comments in
#
#     src/lib/compiler/front/typer/basics/debruijn-index.api

# Compiled by:
#     src/lib/compiler/front/typer/typer.sublib

# This file implements the abstraction of de Bruijn indices
# used by the highcode type and term language.
#
# The notion of depth refers to the type-naming depth
# relative to the top level of the current compilation unit.



# I moved this into the typechecker library.  It may be moved
# back to highcode if the typechecker gets "cleaned up", i.e., if
# it is made to be unaware of such backend internals.
# (08/2001 Blume)

stipulate
    package err =  error_message;       # error_message         is from   src/lib/compiler/front/basics/errormsg/error-message.pkg
herein

    package   debruijn_index
    : (weak)  Debruijn_Index            # Debruijn_Index        is from   src/lib/compiler/front/typer/basics/debruijn-index.api
    {

        fun bug s = err::impossible ("debruijn_index: " + s);

        Debruijn_Depth =  Int;
        Debruijn_Index =  Int;

        top = 0;

        fun next i
            =
            i + 1;

        fun prev i
            =
            if (i > 0)      i - 1; 
            else            bug "negative depth in prev";
            fi;

        fun eq (i: Int, j)
            =
            i == j;

        fun dp_key (i:  Debruijn_Depth)
            =
            i;

        fun dp_print i
            =
            int::to_string i;

        fun dp_toint   (i:  Debruijn_Depth)   =   i;
        fun dp_fromint (i:  Int           )   =   i;

        fun subtract (cur: Int, def)
            = 
            if  (cur >= def)   cur - def;
            else               bug "the definition is deeper than the use";
            fi;

        cmp = int::compare;

        fun di_key i
            =
            i;

        fun di_print i
            =
            int::to_string i;

        fun di_toint   (i:  Debruijn_Index)   =   i;
        fun di_fromint (i:  Int           )   =   i;

        innermost = 1;
        innersnd  = 2;

        fun di_inner i
            =
            i+1;


    };                                                  #  package debruijn_index 
end;                                                    # stipulate