lambdapi 2.2.0

Libraries

This package provides the following libraries (via dune):

lambdapi.common

Documentation:

• Common.Console Verbose level and loggers management.
• Common.Debug Helper functions for debugging. *
• Common.Error Warnings and errors.
• Common.Escape Escaped identifiers "{|...|}".
• Common.Library Lambdapi library management.
• Common.Logger Functions for creating loggers. *
• Common.Path Module paths in the Lambdapi library.
• Common.Pos Positions in Lambdapi files.

Dependencies: timed, lambdapi.lplib

lambdapi.core

Documentation:

• Core.Builtin Registering and checking builtin symbols.
• Core.Ctxt Typing context.
• Core.Env Scoping environment for variables.
• Core.Eval Evaluation and conversion.
• Core.Infer Type inference and checking
• Core.Inverse Compute the inverse image of a term wrt an injective function.
• Core.LibMeta Functions to manipulate metavariables.
• Core.LibTerm Basic operations on terms.
• Core.Print Pretty-printing for the core AST.
• Core.Sig_state Signature state.
• Core.Sign Signature for symbols.
• Core.Term Internal representation of terms.
• Core.Tree Compilation of rewriting rules to decision trees.
• Core.Tree_type Miscellaneous types and utilities for decision trees.
• Core.Unif Solving unification constraints.
• Core.Unif_rule Symbols and signature for unification rules.
• Core.Version Version informations.

Dependencies: lambdapi.common, lambdapi.lplib, pratter, bindlib, why3

lambdapi.export

Documentation:

• Export.Dk Export a Lambdapi signature to Dedukti.
• Export.Hrs This module provides a function to translate a signature to the HRS format used in the confluence competition.
• Export.Xtc This module provides a function to translate a signature to the XTC format used in the termination competition.

Dependencies: lambdapi.core, lambdapi.parsing, lambdapi.lplib

lambdapi.handle

Documentation:

• Handle.Command Handling of commands.
• Handle.Compile High-level compilation functions.
• Handle.Inductive Generation of induction principles.
• Handle.Proof Proofs and tactics.
• Handle.Query Handling of queries.
• Handle.Rewrite Implementation of the rewrite tactic.
• Handle.Tactic Handling of tactics.
• Handle.Why3_tactic Calling a prover using Why3.

Dependencies: lambdapi.core, lambdapi.parsing, lambdapi.tool

lambdapi.lplib

Documentation:

• Lplib.Array
• Lplib.Base Standard library extension (mostly).
• Lplib.Color
• Lplib.Extra
• Lplib.Filename
• Lplib.List
• Lplib.Option
• Lplib.Range
• Lplib.RangeMap
• Lplib.RangeMap_intf
• Lplib.Range_intf
• Lplib.String

Dependencies: stdlib-shims, str, unix

lambdapi.lsp

Documentation:

• Lsp.Lp_doc
• Lsp.Lp_lsp
• Lsp.Lsp_base
• Lsp.Lsp_io

Dependencies: yojson, lambdapi.pure

lambdapi.parsing

Documentation:

• Parsing.DkBasic
• Parsing.DkLexer
• Parsing.DkParser
• Parsing.DkRule
• Parsing.DkTokens
• Parsing.LpLexer
• Parsing.LpParser
• Parsing.Package
• Parsing.Parser
• Parsing.Pratt
• Parsing.Pretty
• Parsing.Scope
• Parsing.Syntax

Dependencies: lambdapi.core, menhirLib, pratter, sedlex, sedlex.ppx, lambdapi.common

lambdapi.pure

Documentation: Pure

Dependencies: lambdapi.handle, lambdapi.core

lambdapi.tool

Documentation:

• Tool.External Provides a function for calling external checkers using a Unix command.
• Tool.Lcr Incremental verification of local confluence
• Tool.Sr Checking that a rule preserves typing (subject reduction property).
• Tool.Tree_graphviz Representation of trees as graphviz files.

Dependencies: lambdapi.parsing, lambdapi.core