## debruijn-index.api
# Compiled by:
# src/lib/compiler/front/typer/typer.sublib# From http://www-cse.ucsd.edu/ilks/wi06/cse230/hw/hw3.pdf:
#
# "An alternative notation for the lambda-calculus is the
# de Bruijn notation which elegantly sidesteps the confusion
# arising from free and bound variables.
#
# "The de Bruijn index of a variable occurrence is the number
# of lambdas that separate the occurrence from its naming
# lambda in the abstract syntax tree.
#
# "In the de Bruijn notation, the names of variables are
# replaced at each occurrence with the corresponding de Bruijn
# index at that occurrence.
#
# "Terms that are equivalent after renaming bound variables have
# the same de Bruijn representation.
#
# lambda term | de Bruijn term
# ---------------------------------------------
# \x::x | \.0
# \x.\x::x | \.\.0
# \x.\y::y | \.\.0
# \x.((\x.\y::x)x) | \.((\.\.1)0)
#
#
#
# Tree notation may make this clearer.
# Stealing a leaf from
# http://www.cs.cornell.edu/Info/Projects/NuPrl/cs611/fall94notes/cn14/section3_4.html
#
# \f.\g.\x::fx (gx)
#
# has a syntax tree looking like
#
# (f lambda)
# |
# (g lambda)
# |
# (x lambda)
# |
# (apply)
# / \
# (apply) (apply)
# / \ / \
# f x g x
#
# which in de Bruijn index representation becomes:
#
# (lambda)
# |
# (lambda)
# |
# (lambda)
# |
# (apply)
# / \
# (apply) (apply)
# / \ / \
# 2 0 1 0
#
# Note that travelling up the tree by the number
# of lambdas given by any de Bruijn index brings
# you to the lambda naming that index.
# This api is implemented in:
#
# src/lib/compiler/front/typer/basics/debruijn-index.pkgapi Debruijn_Index {
#
eqtype Debruijn_Depth;
eqtype Debruijn_Index;
top: Debruijn_Depth;
next: Debruijn_Depth -> Debruijn_Depth;
prev: Debruijn_Depth -> Debruijn_Depth;
eq: (Debruijn_Depth, Debruijn_Depth) -> Bool;
subtract: (Debruijn_Depth, Debruijn_Depth) -> Debruijn_Index;
cmp: (Debruijn_Depth, Debruijn_Depth) -> Order;
dp_print: Debruijn_Depth -> String;
dp_key: Debruijn_Depth -> Int;
dp_toint: Debruijn_Depth -> Int;
dp_fromint: Int -> Debruijn_Depth;
di_print: Debruijn_Index -> String;
di_key: Debruijn_Index -> Int;
di_toint: Debruijn_Index -> Int;
di_fromint: Int -> Debruijn_Index;
innermost: Debruijn_Index;
innersnd: Debruijn_Index;
di_inner: Debruijn_Index -> Debruijn_Index;
};
## COPYRIGHT (c) 1997 YALE FLINT PROJECT
## Subsequent changes by Jeff Prothero Copyright (c) 2010-2015,
## released per terms of SMLNJ-COPYRIGHT.