Library
Module
Module type
Parameter
Class
Class type
module PSet : sig ... end
Functional sets of pairs of integers.
type t = {
variables : int Lplib.Extra.IntMap.t; | (* An association |
nl_conds : PSet.t; | (* Set of convertibility constraints |
fv_conds : int array Lplib.Extra.IntMap.t; | (* A mapping of |
}
A pool of (convertibility and free variable) conditions.
val empty : t
empty
is the condition pool holding no condition.
val is_empty : t -> bool
is_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 -> bool
constrained_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 -> bool
is_contained cond pool
tells whether the condition cond
is contained in the pool pool
.
val remove : Tree_type.tree_cond -> t -> t
remove cond pool
removes condition cond
from the pool pool
.
val choose : t list -> Tree_type.tree_cond option
choose pools
selects a condition to check in the pools of pools
. The heuristic is to first select convertibility constraints.