Module Biabduction__BiabductionSummary.Jprop
Module for joined props: the result of joining together propositions repeatedly
type 'a t=|Prop of int * 'a Biabduction.Prop.t|Joined of int * 'a Biabduction.Prop.t * 'a t * 'a tRemember when a prop is obtained as the join of two other props; the first parameter is an id
val d_shallow : Biabduction.Prop.normal t -> unitDump the toplevel prop
val d_list : shallow:bool -> Biabduction.Prop.normal t list -> unitdump a joined prop list, the boolean indicates whether to print toplevel props only
val free_vars : Biabduction.Prop.normal t -> IR.Ident.t IStdlib.IStd.Sequence.tval filter : ('a t -> 'b option) -> 'a t list -> 'b listjprop_filter filter joinedpropsappliesfilterto the elements ofjoindepropsand applies it to the subparts if the result isNone. Returns the most absract results which passfilter.
val jprop_sub : Biabduction.Predicates.subst -> Biabduction.Prop.normal t -> Biabduction.Prop.exposed tapply a substitution to a jprop
val map : ('a Biabduction.Prop.t -> 'b Biabduction.Prop.t) -> 'a t -> 'b tmap the function to each prop in the jprop, pointwise
val shallow_map : f:('a Biabduction.Prop.t -> 'a Biabduction.Prop.t) -> 'a t -> 'a tmap f over the top-level prop
val to_prop : 'a t -> 'a Biabduction.Prop.tExtract the toplevel jprop of a prop