Module `BiabductionSummary.Jprop`

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

type 'a t = | Prop of int * 'a Prop.t | 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.

val jprop_sub : Predicates.subst -> Prop.normal t -> Prop.exposed t: 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