package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

Generic discrimination net implementation over recursive types. This module implements a association data structure similar to tries but working on any types (not just lists). It is a term indexing datastructure, a generalization of the discrimination nets described for example in W.W.McCune, 1992, related also to generalized tries Hinze, 2000.

You can add pairs of (term,identifier) into a dnet, where the identifier is *unique*, and search terms in a dnet filtering a given pattern (retrievial of instances). It returns all identifiers associated with terms matching the pattern. It also works the other way around : You provide a set of patterns and a term, and it returns all patterns which the term matches (retrievial of generalizations). That's why you provide *patterns* everywhere.

Warning 1: Full unification doesn't work as for now. Make sure the set of metavariables in the structure and in the queries are distincts, or you'll get unexpected behaviours.

Warning 2: This structure is perfect, i.e. the set of candidates returned is equal to the set of solutions. Beware of de Bruijn shifts and sorts subtyping though (which makes the comparison not symmetric, see term_dnet.ml).

The complexity of the search is (almost) the depth of the term.

To use it, you have to provide a module (Datatype) with the datatype parametrized on the recursive argument. example:

type btree = type 'a btree0 = | Leaf ===> | Leaf | Node of btree * btree | Node of 'a * 'a

module type Datatype = sig ... end

datatype you want to build a dnet on

module type S = sig ... end
module Make (T : Datatype) (Ident : Stdlib.Set.OrderedType) (Meta : Stdlib.Set.OrderedType) : S with type ident = Ident.t and type meta = Meta.t and type 'a structure = 'a T.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct