Overview of the mltaylor implementation

taylor.ml

is the most interesting part: it contains the implementation of the function diff_of_term, an adaptation of the KAM that extract, from the normalization sequence of a lambda-term, the associated simple term;

mltaylor.ml

puts all the pieces together to build the program mltaylor.

lambda.ml

contains the definition of the type lambda_term, the lambda-term parser lambda_of_string, the lambda-term printer string_of_lambda and a function normalize that... normalizes lambda-terms, using the Krivine Abstract Machine;

diff.ml

contains the definition of the type diff_term of simple terms, a number of utilities functions on simple terms, the parser diff_of_string and the printer string_of_diff;

term_lexer.ml

contains a simple lexer used by the parsers, plus some utilities functions;