module Path : sig ... endval mkConstant : safe:bool -> data:int -> arity:int -> cellval mkPrimitive : Elpi_util.Util.CData.t -> cellval mkVariable : cellval mkLam : cellval mkInputMode : cellval mkOutputMode : cellval mkListTailVariable : cellval mkListHead : cellval mkListEnd : cellval mkPathEnd : cellindex dt path value ~time returns a new discrimination tree starting from dt where value is added wrt its path. ~time is used as a priority marker between two rules.
A rule with a given ~time has higher priority on other rules with lower ~time
@note: in the elpi runtime, there are no two rule having the same ~time
val max_path : 'a t -> intval max_depths : 'a t -> int arrayval empty_dt : 'b list -> 'a tretrive 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 of values are sorted wrt to the order in which values are added in the tree: given two rules r_1 and r_2 with same path, if r_1 has been added at time t and r_2 been added at time t+1 then r_2 will appear before r_1 in the final result
val pp_cell : Format.formatter -> cell -> unitval show_cell : cell -> stringval pp : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unitval show : (Format.formatter -> 'a -> unit) -> 'a t -> stringmodule Internal : sig ... end