Overview of directories and files
doc/
: documentation in ReStructured Text formatdoc/README.md
: introduction to the user manual and guidelines
editors/
: editor plugins for handling Lambdapi filesemacs/
: code for Emacsvim/
: code for Vimvscode/
: code for VSCode.vscode/*.json
: config for launching and debugging the extensionlp.configuration.json
: specific charactersmedia/styles.css
: stylespackage.json
: manifest of the plugin (activation events, scripts, dependencies, …)snippets/unicode.json
: short-cuts for entering unicode characterssrc/*.ts
: source code of the extensionsyntaxes/lp.tmLanguage.json
: grammar of Lambdapitsconfig.json
: TypeScript configuration (directories, …)
libraries/
: libraries of Dedukti files (seeMakefile
)src/cli/
: command line interfaceconfig.ml
: main program configurationinit.ml
: lambdapi init commandinstall.ml
: lambdapi install commandlambdapi.ml
: main program
src/common/
: miscellaneous modules and librariesconsole.ml
: flag managementdebug.ml
: debugging toolserror.ml
: warning and error managementescape.ml
: basic functions on escaped identifierslibrary.ml
: Lambdapi library managementlogger.ml
: logging toolspath.ml
: module paths in the Lambdapi librarypos.ml
: source file position management
src/core/
: core of Lambdapiterms:
term.ml
: internal representation of termslibTerm.ml
: basic operations on termslibMeta.ml
: basic operations on metavariablesprint.ml
: pretty printing of termsenv.ml
: maps identifier -> variable and type
signatures:
builtin.ml
: managing builtinssign.ml
: compiled module signature (symbols and rules in a module)sig_state.ml
: signature under construction
rewriting:
tree_type.ml
: types and basic functions for decision treestree.ml
: compilation of rewriting rules to decision treeseval.ml
: rewriting engine
type inference/checking:
ctxt.ml
: typing contexts (maps variable -> type)infer.ml
: constraints generating type inference and checking
unification:
unif_rule.ml
: ghost signature for unification rulesunif.ml
: unification algorithminverse.ml
: inverse of injective functions
src/handle
: signature buildingcommand.ml
: command handlingcompile.ml
: file parsing and compiling (.lpo files)inductive.ml
: generation of induction principlesquery.ml
: handling of queries (commands that do not change the signature or the proof state)tactics:
proof.ml
: proof staterewrite.ml
: rewrite tactic (similar to Ssreflect)tactic.ml
: tactic handlingwhy3_tactic.ml
: why3 tactic
src/lplib/
: extension of the Ocaml standard libraryrange_intf.ml
: module type of abstract intervalsrangeMap_intf.ml
: module type of abstract maps on intervalsrangeMap.ml
: instance ofrangeMap_intf
usingrange
range.ml
: instance ofrange_intf
with integer intervalsrealpath.c
: C implementation ofFilename.realpath
src/lsp/
: LSP serverlp_doc.ml
: document typelp_lsp.ml
: LSP serverlsp_base.ml
: basic functions for building messageslsp_io.ml
: basic functions for reading and sending messages
src/parsing/
: parsing Dedukti and Lambdapi filespkg file parsing;
package.ml
: parsing of package fileslambdapi.pkg
abstract syntax:
syntax.ml
: abstract syntax
dk file parsing:
dkBasic.ml
: basic definitions for dk parsingdkTokens.ml
: lexing tokens for dk syntaxdkLexer.mll
: lexer for dk syntaxdkRule.ml
: convert dk rules into lp rulesdkParser.mly
: parser for dk syntax
lp file parsing:
lpLexer.ml
: lexer for Lambdapi syntaxlpParser.mly
: parser for Lambdapi syntaxparser.ml
: interfaces for parserspretty.ml
: pretty print the abstract syntax (used to convert Dedukti files into Lambdapi files)
scoping:
pratt.ml
: parsing of applications wrt symbol notationsscope.ml
: convert the abstract syntax into terms
src/pure/
: pure interface (mainly used by the LSP server)pure.ml
: provide utilities to roll back the state
src/tool/
: toolsexternal.ml
: call of external toolshrs.ml
: export to the .hrs format of the confluence competitionsr.ml
: algorithm for checking subject reductiontree_graphviz.ml
: representation of trees as graphviz filesxtc.ml
: export to the .xtc format of the termination competition
tests/
: unit testsOK/
: tests that should succeedKO/
: tests that should fail
misc/
:gen_version.ml
: script used by dune to generate_build/default/src/core/version.ml
used inlambdapi.ml
sanity_check.sh
: script checking some style guidelines below (called bymake sanity_check
)generate_tests.ml
: creates test files intests/OK
that can be parametrisedlistings.tex
: setup of the LaTeX package listings for including Lambdapi code into a LaTeX documentdeps.ml
: gives the#REQUIRE
commands that should be added at the beginning of a Dedukti file