package elpi

  1. Overview
  2. Docs
ELPI - Embeddable λProlog Interpreter

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (16)

Authors

  1. C
    Claudio Sacerdoti Coen
  2. E
    Enrico Tassi

Maintainers

  1. E
    Enrico Tassi <enrico.tassi@inria.fr>

Sources

elpi-3.3.1.tbz
sha256=3186ebbf97d702e3cd5ebfa2aca50d9e93dd939a86c3db827dbde111656e3d5f
sha512=2ffafd7dbcaad4802fc2f076f90df36a1ce33dae1f0fa9226d45654a932a70e0a9f0627bbc703870561ad2d36a86039ad04c74393ccaf369c283eddb488525cf

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

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 mkUvarConstant : 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 : 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