Predicates.Env
record the occurrences of predicates as parameters of (doubly -)linked lists and Epara. Provides unique numbering for predicates and an iterator.
type t
predicate environment
val mk_empty : unit -> t
create an empty predicate environment
val is_empty : t -> bool
return true if the environment is empty
val iter : t -> (int -> hpara -> unit) -> (int -> hpara_dll -> unit) -> unit
iter env f f_dll iterates f and f_dll on all the hpara and hpara_dll, passing the unique id to the functions. The iterator can only be used once.
iter env f f_dll
f
f_dll
val process_hpred : t -> hpred -> unit
Process one hpred, updating the predicate environment