searchdepend.mlg

(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
(*            This file is part of the DpdGraph tools.                        *)
(*   Copyright (C) 2009-2015 Anne Pacalet (Anne.Pacalet@free.fr)              *)
(*                       and Yves Bertot (Yves.Bertot@inria.fr)               *)
(*             ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~                                *)
(*        This file is distributed under the terms of the                     *)
(*         GNU Lesser General Public License Version 2.1                      *)
(*        (see the enclosed LICENSE file for mode details)                    *)
(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

DECLARE PLUGIN "coq-dpdgraph.plugin"

{

open Pp
open Stdarg

module Data = struct
  type t = int Names.GlobRef.Map.t

  let empty = Names.GlobRef.Map.empty

  let add gref d =
    let n = try  Names.GlobRef.Map.find gref d with Not_found -> 0 in
    Names.GlobRef.Map.add gref (n+1) d

      (* [f gref n acc] *)
  let fold f d acc = Names.GlobRef.Map.fold f d acc
end

let add_identifier (x:Names.Id.t)(d:Data.t) =
  failwith
    ("SearchDep does not expect to find plain identifiers :" ^
     Names.Id.to_string x)

let add_sort (s:Sorts.t)(d:Data.t) = d

let add_constant (cst:Names.Constant.t)(d:Data.t) =
  Data.add (Names.GlobRef.ConstRef cst) d

let add_inductive ((k,i):Names.inductive)(d:Data.t) =
  Data.add (Names.GlobRef.IndRef (k, i)) d

let add_constructor(((k,i),j):Names.constructor)(d:Data.t) =
  Data.add (Names.GlobRef.ConstructRef ((k,i),j)) d

let collect_long_names avoid (c:Constr.t) (acc:Data.t) =
  let rec add acc c =
    let open Constr in
    match kind c with
      | Var x -> add_identifier x acc
      | Sort s -> add_sort s acc
      | Const cst -> add_constant (UVars.out_punivs cst) acc
      | Ind (i,_) when not (List.exists (Names.MutInd.CanOrd.equal (fst i)) avoid) -> add_inductive i acc
      | Construct (cnst,_) when not (List.exists (Names.MutInd.CanOrd.equal (fst (fst cnst))) avoid) -> add_constructor cnst acc
      | Case({ci_ind=i},_,_,_,_,_,_) ->
          add_inductive i (Constr.fold add acc c)
      | _ -> Constr.fold add acc c
  in add acc c

exception NoDef of Names.GlobRef.t

let collect_dependance gref =
  (* This will change to Names.GlobRef in 8.10 *)
  let open Names in
  let open GlobRef in
  match gref with
  | VarRef _ -> assert false
  | ConstRef cst ->
      let cb = Environ.lookup_constant cst (Global.env()) in
      let cl = match Global.body_of_constant_body Library.indirect_accessor cb with
         Some (e,_,_) -> [e]
	| None -> [] in
      let cl = cb.Declarations.const_type :: cl in
      List.fold_right (collect_long_names []) cl Data.empty
  | IndRef i | ConstructRef (i,_) ->
      let _, indbody = Global.lookup_inductive i in
      let ca = indbody.Declarations.mind_user_lc in
        Array.fold_right (collect_long_names [fst i]) ca Data.empty

let display_dependance gref =
  let display d =
    let pp gr n s =
      Printer.pr_global gr ++ str "(" ++ int n ++ str ")" ++ spc() ++s
    in
      Feedback.msg_notice (str"[" ++ ((Data.fold pp) d (str "]")))
  in try let data = collect_dependance gref in display data
  with NoDef gref ->
    CErrors.user_err (Printer.pr_global gref ++ str " has no value")

}

VERNAC COMMAND EXTEND Searchdepend CLASSIFIED AS QUERY
| ["SearchDepend" global(ref) ] -> { display_dependance (Nametab.global ref) }
END