This directory contains several versions of the normalization procedure which can be
copied to the file hnorm.c 


hnorm.original:  consistent with the Teyjus-b33 distribution.  Performs head normalization with
explicit suspensions (no implicit suspensions) and annotations.  Uses SL stack instead of explicit
recursion

hnorm.na:  same as above but without using annotations.


All other versions in this directory have the new recursive style procedures with some use of
implicit suspensions.

comb_hnorm.c:  head normalization that creates explicit suspension terms when necessary.  does
not use annotations.

comb_an_hnorm.c:   head normalization that creates explicit suspension terms when necessary.  
Uses annotations.

full_hnorm.c:  full normalization without annotations.  This is the "non-naive" version that
does not normalize the arguments of head normal forms under empty environments.  Will combine
substitutions when reducing a single term.

full_an_hnorm.c:  full normalization with annotations.  Also uses the "non-naive" strategy as above.

imp_hnorm.c:  head normalization using implicit suspensions only.  no annotations.
 
imp_an_hnorm.c: head normalization using implicit suspensions only. with annotations.

lam_norm.c: naive full normalization without annotations.
 
lam_an_norm.c: naive full normalization with annotations.

full_nomerge: non-naive full normalization without annotations and 
              merging reductions.


exp_hnorm.c + exp_hnormlocal.h: head normalization, explicit substitutions,
                                eager commitment, no annotation




----  Variation concerning De Bruijn representation  -------


comb_sc_hnorm.c:  same as comb_hnorm.c but counts total 
   number of substitutions, non-trivial renumbering substitutions,
   and number of beta redexes.

full_sc_hnorm.c:  same as full_hnorm.c but counts total 
   number of substitutions, non-trivial renumbering substitutions,
   and number of beta redexes.


comb_ea_hnorm.c:  same as comb_sc_hnorm.c but eagerly head normalizes
   skeleton of (implicit) suspension in case nl>0.

full_ea_hnorm.c:  same as full_sc_hnorm.c but eagerly head normalizes
   skeleton of (implicit) suspension in case nl>0.