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.5.0.tbz
sha256=9bc8ae3694dd51bd5742e7aba760bd2878c4b0e5ef9b3d4a7b06f3cd303b611d
sha512=c812c3129b3d85b0c4d7e741d11137dbb4fe2a0aaba3a5968409080b742924ecb506280c19ad83ef6bc910346db96d87780313fa7683c29345edae16ae79c704

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

Module Common.PosSource

Positions in Lambdapi files.

Sourcetype pos = {
  1. fname : string option;
    (*

    File name for the position.

    *)
  2. start_line : int;
    (*

    Line number of the starting point.

    *)
  3. start_col : int;
    (*

    Column number (utf8) of the starting point.

    *)
  4. end_line : int;
    (*

    Line number of the ending point.

    *)
  5. end_col : int;
    (*

    Column number (utf8) of the ending point.

    *)
}

Type of a position, corresponding to a continuous range of characters in a (utf8-encoded) source.

Total comparison function on pos.

Sourcetype popt = pos option

Convenient short name for an optional position.

Sourceval equal : popt -> popt -> bool

equal p1 p2 tells whether p1 and p2 denote the same position.

Sourcetype 'a loc = {
  1. elt : 'a;
    (*

    The element that is being localised.

    *)
  2. pos : popt;
    (*

    Position of the element in the source code.

    *)
}

Type constructor extending a type (e.g. a piece of abstract syntax) with a a source code position.

Sourcetype strloc = string loc

Localised string type (widely used).

Sourceval make : popt -> 'a -> 'a loc

make pos elt associates the position pos to elt.

Sourceval none : 'a -> 'a loc

none elt wraps elt in a 'a loc structure without any specific source code position.

Sourceval in_pos : pos -> 'a -> 'a loc

in_pos pos elt associates the position pos to elt.

Sourceval end_pos : popt -> popt

end_pos po creates a position from the end of position po.

Sourceval cat : popt -> popt -> popt
Sourceval shift : int -> popt -> popt

shift k p returns a position that is k characters after p.

Sourceval after : popt -> popt
Sourceval before : popt -> popt
Sourceval to_string : ?print_fname:bool -> pos -> string

to_string ?print_fname pos transforms pos into a readable string. If print_fname is true (the default), the filename contained in pos is printed.

pp ppf pos prints the optional position pos on ppf.

short ppf pos prints the optional position pos on ppf.

Sourceval map : ('a -> 'b) -> 'a loc -> 'b loc

map f loc applies function f on the value of loc and keeps the position unchanged.

Sourceval locate : ?fname:string -> (Lexing.position * Lexing.position) -> pos

locate ?fname loc converts the pair of position loc and filename fname of the Lexing library into a pos.

Sourceval make_pos : (Lexing.position * Lexing.position) -> 'a -> 'a loc

make_pos lps elt creates a located element from the lexing positions lps and the element elt.

Sourceval print_file_contents : escape:(string -> string) -> delimiters:(string * string) -> popt Lplib.Base.pp

print_file_contents escape sep delimiters pos prints the contents of the file at position pos. sep is the separator replacing each newline (e.g. "<br>\n"). delimiters is a pair of delimiters used to wrap the "unknown location" message returned when the position does not refer to a file. escape is used to escape the file contents.