package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (12)

Authors

  1. D
    Deducteam

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

lambdapi-2.2.0.tbz
sha256=920de48ec6c2c3223b6b93879bb65d07ea24aa27f7f7176b3de16e5e467b9939
sha512=135f132730825adeb084669222e68bc999de97b12378fae6abcd9f91ae13093eab29fa49c854adb28d064d52c9890c0f5c8ff9d47a9916f66fe5e0fba3479759

doc/lambdapi.common/Common/Library/index.html

Module Common.LibrarySource

Lambdapi library management.

Sourceval log_lib : 'a Lplib.Base.outfmt -> 'a
Sourcemodule LibMap : sig ... end

Representation of the mapping from module paths to files.

Sourceval lib_root : string option ref

lib_root stores the result of the "--lib-root" flag when given.

Sourceval lib_mappings : LibMap.t Timed.ref

lib_mappings stores the specified mappings of library paths.

Sourceval iter : (Path.t -> string -> unit) -> unit

iter f iterates f on current mappings.

Sourceval set_lib_root : string option -> unit

set_lib_root dir sets the library root to directory dir. The following directories are set sequentially, such that the active one is the last valid one

  • /usr/local/lib/lambdapi/lib_root/
  • $OPAM_SWITCH_PREFIX/lib/lambdapi/lib_root
  • $LAMBDAPI_LIB_ROOT/lib/lambdapi/lib_root
  • the directory given as parameter of the --lib-root command line argument. If the directory given on command line is not a valid existing directory, the program terminates with a graceful error message.
Sourceval add_mapping : (Path.t * string) -> unit

add_mapping (mn, fn) adds a new mapping from the module name mn to the file name fn if mn is not already mapped and fn is a valid directory. In case of failure the program terminates and a graceful error message is displayed.

Sourceval file_of_path : Path.t -> string

file_of_path mp converts module path mp into the corresponding "file path" (with no attached extension). It is assumed that lib_root has been set, possibly with set_lib_root.

Sourceval lp_src_extension : string

lp_src_extension is the expected extension for source files.

Sourceval dk_src_extension : string

dk_src_extension is the extension for dk source files.

Sourceval is_valid_src_extension : string -> bool

is_valid_src_extension s returns true iff s ends with lp_src_extension or dk_src_extension.

Sourceval obj_extension : string

obj_extension is the expected extension for binary (object) files.

Sourceval valid_extensions : string list

valids_extensions is the list of valid file extensions.

Sourceval path_of_file : (string -> string) -> string -> Path.t

path_of_file escape fname computes the module path that corresponds to the filename fname. escape converts irregular path elements into escaped identifiers if needed.

  • raises [Fatal]

    if fn doesn't have a valid extension.

Sourceval install_path : string -> string

install_path fname prefixes the filename fname by the path to the library root.