dkparse (Dedukti) is a small implementation of a type
checker for the lambda-Pi modulo. It features
normalization by evaluation through compilation to Lua
code.


INSTALL

To install the dkparse program make sure you have
lua5.1 or luajit installed, install the bison grammar
compiler and a C99 compliant compiler. Make sure the
default settings in the Makefile file are valid on your
current system (they should be). Then, issue the
following command:
    $ make

If you want to compile the documentation, make sure you
have GNU makeinfo installed and run:
    $ make doc
This will create the files doc/dkparse.info.gz and
doc/dkparse.html, the info file will be installed in
the directory specified by the Makefile, the HTML file
can be viewed in any browser. Once installed, you can
view the user manual using 'info dkparse'.

To install dkparse, run:
    $ sudo make install

You can test if your compiled version of dkparse is not
rotten by issuing the following command (you will need
lua5.1):
    $ make test

All tests must pass.


CHANGES

07/01 The makefile was changed to support installation.

06/01 Lua code can be generated using dkparse, the
feature is still experimental but on simple examples it
works. The code is generated on the standard output and
is meant to be executed by a Lua interpreter, note that
the file lua/dedukti.lua must be loaded first, a
typical use case is shown below:
    dkparse f.dk | lua -l dedukti

05/27 Syntactic support for dot patterns was added,
basic scoping and linearity checks are performed by
dkparse.

05/14 Now it also checks that identifiers are well
scoped, note that it does not handle external modules
yet.


vi: tw=55: nolist