glob.ml 1.45 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10
(********************************************************************)
11 12 13

open Ident

Andrei Paskevich's avatar
Andrei Paskevich committed
14 15
let flag = Debug.register_flag "track_symbol_use"
  ~desc:"Track@ symbol@ occurrences@ in@ source@ files.@ Used@ by@ why3doc."
16

17
let () = Debug.unset_flag flag (* make sure it is unset by default *)
18

19 20
type def_use = Def | Use

21 22
let glob = Hashtbl.create 5003
  (* could be improved with nested hash tables *)
23

24 25 26 27 28 29
let key loc = let f, l, c, _ = Loc.get loc in f, l, c

let add loc idk =
  let k = key loc in
  if not (Hashtbl.mem glob k) then Hashtbl.add glob k idk

30 31
let def ~kind id =
  Opt.iter (fun loc -> add loc (id, Def, kind)) id.id_loc
32

33 34
let use ~kind loc id =
  add loc (id, Use, kind)
35 36 37

let find loc =
  Hashtbl.find glob (key loc)
38

39 40
(* FIXME allow several entries for the same loc, find returns all of them,
         and why3doc inserts several anchors *)