Module Elpi_runtime.Discrimination_tree

type cell
module Path : sig ... end
val mkConstant : safe:bool -> data:int -> arity:int -> cell
val mkPrimitive : Elpi_util.Util.CData.t -> cell
val mkVariable : cell

This is for: unification variables, discard

val 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
val mkInputMode : cell
val mkOutputMode : cell
val 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

val mkUvarConstant : cell

unique identifier for uvar constructor

val 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

val mkListHead : cell
val mkListNil : cell
val mkListEnd : cell
val 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.

type 'a t
val 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.

val max_path : 'a t -> int
val max_list_length : 'a t -> int
val max_depths : 'a t -> int array
val user_upper_bound_depth : 'a t -> int list
val empty_dt : int list -> 'a t
val 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

val replace : ('a -> bool) -> 'a -> 'a t -> 'a t
val remove : ('a -> bool) -> 'a t -> 'a t
val pp_cell : Format.formatter -> cell -> unit
val show_cell : cell -> string
val pp : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
val show : (Format.formatter -> 'a -> unit) -> 'a t -> string
module Internal : sig ... end