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 t
Remember 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 -> unit
Dump the toplevel prop
val d_list : shallow:bool -> Biabduction.Prop.normal t list -> unit
dump 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.t
val filter : ('a t -> 'b option) -> 'a t list -> 'b list
jprop_filter filter joinedprops
appliesfilter
to the elements ofjoindeprops
and 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 t
apply a substitution to a jprop
val map : ('a Biabduction.Prop.t -> 'b Biabduction.Prop.t) -> 'a t -> 'b t
map the function to each prop in the jprop, pointwise
val shallow_map : f:('a Biabduction.Prop.t -> 'a Biabduction.Prop.t) -> 'a t -> 'a t
map f over the top-level prop
val to_prop : 'a t -> 'a Biabduction.Prop.t
Extract the toplevel jprop of a prop