package elpi

  1. Overview
  2. Docs
package elpi
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Elpi_runtime.Discrimination_treeSource

Sourcetype cell
Sourcemodule Path : sig ... end
Sourceval mkConstant : safe:bool -> data:int -> arity:int -> cell
Sourceval mkPrimitive : Elpi_util.Util.CData.t -> cell
Sourceval mkVariable : cell

This is for: unification variables, discard

Sourceval mkAny : cell

This is for:

  • lambda-abstractions: DT does not perform HO unification, nor βη-redex unif
  • too big terms: if the path of the goal is bigger then the max path in the rules, each term is replaced with this constructor. Note that we do not use mkVariable, since in input mode a variable cannot be unified with non-flex terms. In DT, mkAny is unified with anything
Sourceval mkInputMode : cell
Sourceval mkOutputMode : cell
Sourceval mkListTailVariable : cell

This is for the last term of opened lists.

If the list ends is 1,2|X == Cons (CData'1',Cons(CData'2',Arg (_, _)))

The corresponding path will be: ListHead, Primitive, Primitive, ListTailVariable

ListTailVariable is considered as a variable, and if it appears in a goal in input position, it cannot be unified with non-flex terms

Sourceval mkListTailVariableUnif : cell

This is used for capped lists.

If the length of the maximal list in the rules of a predicate is N, then any (sub-)list in the goal longer then N encodes the first N elements in the path and the last are replaced with ListTailVariableUnif.

The main difference with ListTailVariable is that DT will unify this symbol to both flex and non-flex terms in the path of rules

Sourceval mkListHead : cell
Sourceval mkListEnd : cell
Sourceval mkPathEnd : cell

This is padding used to fill the array in paths and indicate the retrieve function to stop making unification.

Note that the array for the path has a length which is doubled each time the terms in it are larger then the forseen length. Each time the array is doubled, the new cells are filled with PathEnd.

Sourcetype 'a t
Sourceval index : 'a t -> max_list_length:int -> Path.t -> 'a -> 'a t

index dt ~max_list_length path value returns a new discrimination tree starting from dt where value is added wrt its path.

max_list_length is provided and used to update (if needed) the length of the longest list in the received path.

Sourceval max_path : 'a t -> int
Sourceval max_list_length : 'a t -> int
Sourceval max_depths : 'a t -> int array
Sourceval empty_dt : 'b list -> 'a t
Sourceval retrieve : ('a -> 'a -> int) -> Path.t -> 'a t -> 'a Bl.scan

retrive cmp path dt Retrives all values in a discrimination tree dt from a given path p.

The retrival algorithm performs a light unification between p and the nodes in the discrimination tree. This light unification takes care of unification variables that can be either in the path or in the nodes of dt

The returned list is sorted wrt cmp so that rules are given in the expected order

Sourceval replace : ('a -> bool) -> 'a -> 'a t -> 'a t
Sourceval remove : ('a -> bool) -> 'a t -> 'a t
Sourceval pp_cell : Format.formatter -> cell -> unit
Sourceval show_cell : cell -> string
Sourceval pp : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
Sourceval show : (Format.formatter -> 'a -> unit) -> 'a t -> string
Sourcemodule Internal : sig ... end
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