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.0.0.tbz
sha256=66d7d29f7a0d10493b8178c4c3aeb247971e24fab3eba1c54887e1b9a82fe005
sha512=69ecf2406e4c7225ab7f8ebe11624db5d2ab989c8f30f5b6e5d426fd8ef9102f142a2840af16fb9103bb712ebcf7d314635f8b413a05df66e7b7a38548867032

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

Module Common.PosSource

Source code position management. This module may be used to map sequences of characters in a source file to an abstract syntax tree.

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.

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 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.

Sourceval pp_short : popt Lplib.Base.pp

pp_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.