package dedukti

  1. Overview
  2. Docs

Debugging

Module which handle dependencies between Dedukti files

type dep_error =
  1. | CircularDependencies of string * string list
  2. | NameNotFound of Kernel.Basic.name
exception Dep_error of dep_error

Type declaration

type data = {
  1. up : Kernel.Basic.NameSet.t;
  2. down : Kernel.Basic.NameSet.t;
}

up dependencies are the name that requires the current item. down dependencies are the name that are required by the current item.

type name_deps = (Kernel.Basic.ident, data) Stdlib.Hashtbl.t

A map from an identifiers to its up and down dependencies

type file_deps = {
  1. file : string;
    (*

    path associated to the module

    *)
  2. deps : Kernel.Basic.MidentSet.t;
    (*

    pairs of module and its associated path

    *)
  3. name_deps : name_deps;
    (*

    up/down item dependencies. Not computed by default.

    *)
}
type t = (Kernel.Basic.mident, file_deps) Stdlib.Hashtbl.t

Map to a module a file dependencies which contains all the dependencies

Dependencies function

val deps : t

deps contains the dependencies computed by the function handle

val ignore : bool Stdlib.ref

(default: false) If true, no exception is raised if a module is not in the path

val compute_all_deps : bool Stdlib.ref

Whether to compute the dependencies of constants. If set to false, only module dependencies are computed.

val get_data : Kernel.Basic.name -> data

get_data name returns the data associated to name name. Raise NameNotfound if the dependencies for name have not been computed.

val make : Kernel.Basic.mident -> Parsers.Entry.entry list -> unit

make md es computes dependencies for the entries es in module md

val handle : Kernel.Basic.mident -> ((Parsers.Entry.entry -> unit) -> unit) -> unit

handle md f computes dependencies on the fly for the entries in module md

val topological_sort : t -> string list

topological_sort f returns a list of files sorted by their dependencies

val transitive_closure : Kernel.Basic.name -> unit

transitive_closure n compute the transitive closure for n