package dedukti

  1. Overview
  2. Docs
An implementation of The Lambda-Pi Modulo Theory

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (2)

Authors

  1. D
    dedukti-dev@inria.fr

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

v2.7.tar.gz
sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c
sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c

doc/dedukti.api/Api/Dep/index.html

Module Api.DepSource

Debugging

Module which handle dependencies between Dedukti files

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

Type declaration

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

A map from an identifiers to its up and down dependencies

Sourcetype 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.

    *)
}

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

Dependencies function

Sourceval deps : t

deps contains the dependencies computed by the function handle

Sourceval ignore : bool ref

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

Sourceval compute_all_deps : bool ref

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

Sourceval 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.

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

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

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

Sourceval topological_sort : t -> string list

topological_sort f returns a list of files sorted by their dependencies

Sourceval transitive_closure : Kernel.Basic.name -> unit

transitive_closure n compute the transitive closure for n