Module BiabductionSummary.Jprop

Module for joined props: the result of joining together propositions repeatedly

type 'a t =
  1. | Prop of int * 'a Prop.t
  2. | Joined of int * 'a Prop.t * 'a t * 'a t

Remember when a prop is obtained as the join of two other props; the first parameter is an id

val compare : 'a t -> 'a t -> int

Comparison for joined_prop

val equal : 'a t -> 'a t -> bool

Return true if the two join_prop's are equal

val d_shallow : Prop.normal t -> unit

Dump the toplevel prop

val d_list : shallow:bool -> Prop.normal t list -> unit

dump a joined prop list, the boolean indicates whether to print toplevel props only

val free_vars : Prop.normal t -> IR.Ident.t IStdlib.IStd.Sequence.t
val filter : ('a t -> 'b option) -> 'a t list -> 'b list

jprop_filter filter joinedprops applies filter to the elements of joindeprops and applies it to the subparts if the result is None. Returns the most absract results which pass filter.

apply a substitution to a jprop

val map : ('a Prop.t -> 'b Prop.t) -> 'a t -> 'b t

map the function to each prop in the jprop, pointwise

val shallow_map : f:('a Prop.t -> 'a Prop.t) -> 'a t -> 'a t

map f over the top-level prop

val to_prop : 'a t -> 'a Prop.t

Extract the toplevel jprop of a prop