Module Indexed.ExtendFinite

Functor that creates an abstract function graph for (T * X) => Y) given a type with finite elements T and an abstract function graph for X => Y.

Parameters

module M : sig ... end
module X : sig ... end
module Y : sig ... end
module MFG : sig ... end

Signature

include Sigs.MFG with type t = MFG.t M.t and type dom = M.key * MFG.dom and type codom = MFG.codom and type strategy = MFG.strategy
type dom = M.key * MFG.dom
type codom = MFG.codom
type t = MFG.t M.t
type strategy = MFG.strategy
val bot : t
val is_bot : t -> bool
val init : dom -> t
val leq : t -> t -> bool
val map : (dom -> codom) -> t -> t
val apply : t -> dom -> codom
val join : t -> t -> t
val widen_gen : strategy array -> int -> t -> t -> t
val default_strategy : strategy array
val widen : int -> t -> t -> t
val pp : Stdlib.Format.formatter -> t -> unit
val meet : t -> t -> t
val iter : (dom -> codom -> unit) -> t -> unit
val apply0 : t -> M.key -> MFG.t
val dom0 : t -> M.key list