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 (6)

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.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

doc/src/rocq-runtime.lib/loc.ml.html

Source file loc.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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

type source =
  (* OCaml won't allow using DirPath.t in InFile *)
  | InFile of { dirpath : string option; file : string }
  | ToplevelInput

type t = {
  fname : source;
  line_nb : int;
  bol_pos : int;
  line_nb_last : int;
  bol_pos_last : int;
  bp : int;
  ep : int;
}

let create fname line_nb bol_pos bp ep = {
  fname = fname; line_nb = line_nb; bol_pos = bol_pos;
  line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep;
}

let initial source = create source 1 0 0 0

let make_loc (bp, ep) = {
  fname = ToplevelInput; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
  bp = bp; ep = ep;
}

let mergeable loc1 loc2 =
  loc1.fname = loc2.fname

let merge loc1 loc2 =
  if not (mergeable loc1 loc2) then
    failwith "Trying to merge unmergeable locations.";
  if loc1.bp < loc2.bp then
    if loc1.ep < loc2.ep then {
      fname = loc1.fname;
      line_nb = loc1.line_nb;
      bol_pos = loc1.bol_pos;
      line_nb_last = loc2.line_nb_last;
      bol_pos_last = loc2.bol_pos_last;
      bp = loc1.bp; ep = loc2.ep;
    }
    else loc1
  else if loc2.ep < loc1.ep then {
    fname = loc2.fname;
    line_nb = loc2.line_nb;
    bol_pos = loc2.bol_pos;
    line_nb_last = loc1.line_nb_last;
    bol_pos_last = loc1.bol_pos_last;
    bp = loc2.bp; ep = loc1.ep;
  }
  else loc2

let merge_opt l1 l2 = match l1, l2 with
  | None, None    -> None
  | Some l , None -> Some l
  | None, Some l  -> Some l
  | Some l1, Some l2 -> Some (merge l1 l2)

let sub loc sh len = {loc with bp = loc.bp + sh; ep = loc.bp + sh + len}

let after loc sh len = {loc with bp = loc.ep + sh; ep = loc.ep + sh + len}

let finer l1 l2 = match l1, l2 with
  | None, _    -> false
  | Some l , None -> true
  | Some l1, Some l2 -> l1.fname = l2.fname && merge l1 l2 = l2

let unloc loc = (loc.bp, loc.ep)

let shift_loc kb kp loc = { loc with bp = loc.bp + kb ; ep = loc.ep + kp }

(** Located type *)

type 'a located = t option * 'a

let tag ?loc x = loc, x
let map f (l,x) = (l, f x)

(** Exceptions *)

let location : t Exninfo.t = Exninfo.make "location"

let add_loc e loc = Exninfo.add e location loc
let get_loc e = Exninfo.get e location

let raise ?loc e =
  match loc with
  | None     -> raise e
  | Some loc ->
    let info = Exninfo.add Exninfo.null location loc in
    Exninfo.iraise (e, info)

let pr loc =
  let open Pp in
  let fname = loc.fname in
  match fname with
  | ToplevelInput ->
    (str"Toplevel input, characters " ++ int loc.bp ++
     str"-" ++ int loc.ep)
  | InFile { file } ->
    (str"File " ++ str "\"" ++ str file ++ str "\"" ++
     str", line " ++ int loc.line_nb ++ str", characters " ++
     int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos))

let current_command_loc = ref None

let get_current_command_loc () = !current_command_loc

let set_current_command_loc v = current_command_loc := v

let pr_use_dp loc = let open Pp in
  match loc.fname with
  | ToplevelInput ->
    (* NB emacs mangles the message if it contains the capitalized "Toplevel input" of [Loc.pr] *)
    str "toplevel input, characters " ++ int loc.bp ++ str "-" ++ int loc.ep
  | InFile  { dirpath = None } -> pr loc
  | InFile { dirpath = Some dp } ->
    let f = str "library " ++ str dp in
    (f ++
     str", line " ++ int loc.line_nb ++ str", characters " ++
     int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos))