package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=2c251021b6fac40c05282ca183902da5b1008e69d9179d7a9543905c2c21a28a
sha512=69535f92766e6fedc2675fc214f0fb699bde2a06aa91d338c93c99756235a293cf16776f6328973dda07cf2ad402e58fe3104a08f1a896990c1778b42f7f9fcf
doc/lambdapi.core/Core/Tree/CP/index.html
Module Tree.CP
Source
Module providing a representation for pools of conditions.
type t = {
variables : int Lplib.Extra.IntMap.t;
(*An association
*)(e, v)
maps the slot of a pattern variable (the first argument of aTerm.term.Patt
) to its slot in the arrayvars
of theEval.tree_walk
function. It is used to remember non linearity constraints.nl_conds : PSet.t;
(*Set of convertibility constraints
*)(i,j)
withi < j
. The constraint(i,j)
is satisfied if the terms stored at indicesi
andj
in thevars
array of theEval.tree_walk
function are convertible.fv_conds : int array Lplib.Extra.IntMap.t;
(*A mapping of
*)i
toxs
represents a free variable condition that can only be satisfied if only the free variables ofx
appear in the term stored at sloti
in thevars
array ofEval.tree_walk
.
}
A pool of (convertibility and free variable) conditions.
register_nl slot i pool
registers the fact that the slot slot
in the vars
array correspond to a term stored at index i
in the environment for the RHS. The first time that such a slot is associated to i
, it is registered to serve as a reference point for testing convertibility when (and if) another such slot is (ever) encountered. When that is the case, a convertibility constraint is registered between the term stored in the slot slot
and the term stored in the reference slot.
register_fv slot xs pool
registers a free variables constraint for the variables in xs
on the slot slot
of the vars
array in pool
.
constrained_nl i pool
tells whether index i
in the RHS's environment has already been associated to a variable of the vars
array.
is_contained cond pool
tells whether the condition cond
is contained in the pool pool
.
remove cond pool
removes condition cond
from the pool pool
.
choose pools
selects a condition to check in the pools of pools
. The heuristic is to first select convertibility constraints.