lambdapi

Proof assistant for the λΠ-calculus modulo rewriting
Library lambdapi.common
Module Common . Pos
type pos = {
fname : string option;(*

File name for the position.

*)
start_line : int;(*

Line number of the starting point.

*)
start_col : int;(*

Column number (utf8) of the starting point.

*)
end_line : int;(*

Line number of the ending point.

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

type popt = pos option

Convenient short name for an optional position.

val equal : popt -> popt -> bool

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

type 'a loc = {
elt : 'a;(*

The element that is being localised.

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

type strloc = string loc

Localised string type (widely used).

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

make pos elt associates the position pos to elt.

val none : 'a -> 'a loc

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

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

in_pos pos elt associates the position pos to elt.

val end_pos : popt -> popt

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

val cat : popt -> popt -> popt
val shift : int -> popt -> popt

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

val after : popt -> popt
val before : popt -> popt
val 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.

val short : popt Lplib.Base.pp

short ppf pos prints the optional position pos on ppf.

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

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

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

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