package lambdapi
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
Proof assistant for the λΠ-calculus modulo rewriting
Install
dune-project
Dependency
Authors
Maintainers
Sources
lambdapi-2.0.0.tbz
sha256=66d7d29f7a0d10493b8178c4c3aeb247971e24fab3eba1c54887e1b9a82fe005
sha512=69ecf2406e4c7225ab7f8ebe11624db5d2ab989c8f30f5b6e5d426fd8ef9102f142a2840af16fb9103bb712ebcf7d314635f8b413a05df66e7b7a38548867032
doc/src/lambdapi.common/pos.ml.html
Source file pos.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114(** Source code position management. This module may be used to map sequences of characters in a source file to an abstract syntax tree. *) (** Type of a position, corresponding to a continuous range of characters in a (utf8-encoded) source. *) 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. *) } (** Convenient short name for an optional position. *) type popt = pos option (** [equal p1 p2] tells whether [p1] and [p2] denote the same position. *) let equal : popt -> popt -> bool = fun p1 p2 -> match (p1, p2) with | (Some(p1), Some(p2)) -> p1 = p2 | (None , None ) -> true | (_ , _ ) -> false (** Type constructor extending a type (e.g. a piece of abstract syntax) with a a source code position. *) type 'a loc = { elt : 'a (** The element that is being localised. *) ; pos : popt (** Position of the element in the source code. *) } (** Localised string type (widely used). *) type strloc = string loc (** [make pos elt] associates the position [pos] to [elt]. *) let make : popt -> 'a -> 'a loc = fun pos elt -> { elt ; pos } (** [none elt] wraps [elt] in a ['a loc] structure without any specific source code position. *) let none : 'a -> 'a loc = fun elt -> make None elt (** [in_pos pos elt] associates the position [pos] to [elt]. *) let in_pos : pos -> 'a -> 'a loc = fun p elt -> make (Some p) elt (** [end_pos po] creates a position from the end of position [po]. *) let end_pos : popt -> popt = fun po -> match po with | None -> None | Some p -> Some {p with start_line = p.end_line; start_col = p.end_col} (** [cat p1 p2] returns a position starting from [p1] start and ending with [p2] end. [p1] and [p2] must have the same filename. *) let cat : pos -> pos -> pos = fun p1 p2 -> { fname = if p1.fname <> p2.fname then invalid_arg __LOC__ else p1.fname ; start_line = p1.start_line ; start_col = p1.start_col ; end_line = p2.end_line ; end_col = p2.end_col } let cat : popt -> popt -> popt = fun p1 p2 -> match p1, p2 with | Some p1, Some p2 -> Some (cat p1 p2) | Some p, None | None, Some p -> Some p | None, None -> None (** [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. *) let to_string : ?print_fname:bool -> pos -> string = fun ?(print_fname=true) {fname; start_line; start_col; end_line; end_col} -> let fname = if not print_fname then "" else match fname with | None -> "" | Some(n) -> n ^ ":" in if start_line <> end_line then Printf.sprintf "%s%d:%d-%d:%d" fname start_line start_col end_line end_col else if start_col = end_col then Printf.sprintf "%s%d:%d" fname start_line start_col else Printf.sprintf "%s%d:%d-%d" fname start_line start_col end_col (** [pp ppf pos] prints the optional position [pos] on [ppf]. *) let pp : popt Lplib.Base.pp = fun ppf p -> match p with | None -> Format.pp_print_string ppf "unknown location" | Some(p) -> Format.pp_print_string ppf (to_string p) (** [pp_short ppf pos] prints the optional position [pos] on [ppf]. *) let pp_short : popt Lplib.Base.pp = fun ppf p -> match p with | None -> Format.pp_print_string ppf "unknown location" | Some(p) -> let print_fname=false in Format.pp_print_string ppf (to_string ~print_fname p) (** [map f loc] applies function [f] on the value of [loc] and keeps the position unchanged. *) let map : ('a -> 'b) -> 'a loc -> 'b loc = fun f loc -> {loc with elt = f loc.elt} (** [locate ?fname loc] converts the pair of position [loc] and filename [fname] of the Lexing library into a {!type:pos}. *) let locate : ?fname:string -> Lexing.position * Lexing.position -> pos = fun ?fname (p1, p2) -> let fname = if p1.pos_fname = "" then fname else Some(p1.pos_fname) in let start_line = p1.pos_lnum in let start_col = p1.pos_cnum - p1.pos_bol in let end_line = p2.pos_lnum in let end_col = p2.pos_cnum - p2.pos_bol in {fname; start_line; start_col; end_line; end_col} (** [make_pos lps elt] creates a located element from the lexing positions [lps] and the element [elt]. *) let make_pos : Lexing.position * Lexing.position -> 'a -> 'a loc = fun lps elt -> in_pos (locate lps) elt
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>