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.4.1.tbz
sha256=221dff97ab245c49b7e6480fa2a3a331ab70eb86dd5d521e2c73151029bbb787
sha512=a39961bb7f04f739660a98a52981d4793709619cd21310ca6982ba78af81ef09e01c7517ee3b8b2687b09f7d2614d878c1d69494ca6ab8ef8205d240c216ce8a

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.