package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.lib/Loc/index.html

Module LocSource

Basic types
Sourcetype source =
  1. | InFile of {
    1. dirpath : string option;
    2. file : string;
    }
  2. | ToplevelInput
Sourcetype t = {
  1. fname : source;
    (*

    filename or toplevel input

    *)
  2. line_nb : int;
    (*

    start line number

    *)
  3. bol_pos : int;
    (*

    position of the beginning of start line

    *)
  4. line_nb_last : int;
    (*

    end line number

    *)
  5. bol_pos_last : int;
    (*

    position of the beginning of end line

    *)
  6. bp : int;
    (*

    start position

    *)
  7. ep : int;
    (*

    end position

    *)
}
Location manipulation

This is inherited from CAMPL4/5.

Sourceval create : source -> int -> int -> int -> int -> t

Create a location from a filename, a line number, a position of the beginning of the line, a start and end position

Sourceval initial : source -> t

Create a location corresponding to the beginning of the given source

Sourceval unloc : t -> int * int

Return the start and end position of a location

Sourceval make_loc : (int * int) -> t

Make a location out of its start and end position

Sourceval merge : t -> t -> t
Sourceval merge_opt : t option -> t option -> t option

Merge locations, usually generating the largest possible span

Sourceval sub : t -> int -> int -> t

sub loc sh len is the location loc shifted with sh characters and with length len. The previous ending position of the location is lost.

Sourceval after : t -> int -> int -> t

after loc sh len is the location just after loc (starting at the end position of loc) shifted with sh characters and of length len.

Sourceval finer : t option -> t option -> bool

Answers true when the first location is more defined, or, when both defined, included in the second one

Sourceval shift_loc : int -> int -> t -> t

shift_loc loc n p shifts the beginning of location by n and the end by p; it is assumed that the shifts do not change the lines at which the location starts and ends

Located exceptions
Sourceval add_loc : Exninfo.info -> t -> Exninfo.info

Adding location to an exception

Sourceval get_loc : Exninfo.info -> t option

Retrieving the optional location of an exception

Sourceval raise : ?loc:t -> exn -> 'a

raise loc e is the same as Pervasives.raise (add_loc e loc).

Objects with location information
Sourcetype 'a located = t option * 'a
Sourceval tag : ?loc:t -> 'a -> 'a located

Embed a location in a type

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

Modify an object carrying a location

Sourceval pr : t -> Pp.t

Print for user consumption.

Location of the current command (if any)
Sourceval get_current_command_loc : unit -> t option
Sourceval set_current_command_loc : t option -> unit