Module `Elpi_runtime.Discrimination_tree`Source

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 mkUvarVariable : cell

unique identifier for uvar constructor

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 mkListNil : 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 user_upper_bound_depth : 'a t -> int list

Sourceval empty_dt : int 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 : Stdlib.Format.formatter -> cell -> unit

Sourceval show_cell : cell -> string

Source

val pp : 
  (Stdlib.Format.formatter -> 'a -> unit) ->
  Stdlib.Format.formatter ->
  'a t ->
  unit

Sourceval show : (Stdlib.Format.formatter -> 'a -> unit) -> 'a t -> string

Sourcemodule Internal : sig ... end

Install

Dune Dependency

Authors

Maintainers

Sources

doc/elpi.runtime/Elpi_runtime/Discrimination_tree/index.html

Module `Elpi_runtime.Discrimination_tree`Source

package elpi

Install

Dune Dependency

Authors

Maintainers

Sources

doc/elpi.runtime/Elpi_runtime/Discrimination_tree/index.html

Module Elpi_runtime.Discrimination_treeSource

Module `Elpi_runtime.Discrimination_tree`Source