package elpi

  1. Overview
  2. Docs
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
val mkLam : cell
val mkInputMode : cell
val mkOutputMode : cell
val mkListTailVariable : cell
val mkListHead : cell
val mkListEnd : cell
val mkPathEnd : cell
type 'a data
type 'a t
val index : 'a t -> Path.t -> 'a -> time:int -> 'a t

index 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 -> int
val max_depths : 'a t -> int array
val empty_dt : 'b list -> 'a t
val retrieve : Path.t -> 'a t -> 'a list

retrive 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 : Stdlib.Format.formatter -> cell -> unit
val show_cell : cell -> string
val pp : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a t -> unit
val show : (Stdlib.Format.formatter -> 'a -> unit) -> 'a t -> string
module Internal : sig ... end
OCaml

Innovation. Community. Security.