package lambdapi
-
lambdapi.tool
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package lambdapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Module providing a representation for pools of conditions.
module PSet : sig ... endFunctional sets of pairs of integers.
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 arrayvarsof theEval.tree_walkfunction. 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 indicesiandjin thevarsarray of theEval.tree_walkfunction are convertible.fv_conds : int array Lplib.Extra.IntMap.t;(*A mapping of
*)itoxsrepresents a free variable condition that can only be satisfied if only the free variables ofxappear in the term stored at slotiin thevarsarray ofEval.tree_walk.
}A pool of (convertibility and free variable) conditions.
val empty : tempty is the condition pool holding no condition.
val is_empty : t -> boolis_empty pool tells whether the pool of constraints is empty.
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.
val constrained_nl : int -> t -> boolconstrained_nl i pool tells whether index i in the RHS's environment has already been associated to a variable of the vars array.
val is_contained : Tree_type.tree_cond -> t -> boolis_contained cond pool tells whether the condition cond is contained in the pool pool.
val remove : Tree_type.tree_cond -> t -> tremove cond pool removes condition cond from the pool pool.
val choose : t list -> Tree_type.tree_cond optionchoose pools selects a condition to check in the pools of pools. The heuristic is to first select convertibility constraints.