From 0563578b434dd3fcbb1cf3ce3e8fef76bc751e5f Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Wed, 13 Jun 2018 13:13:28 -0700 Subject: [PATCH] Propgraph: relax types Reviewed By: jeremydubreil Differential Revision: D8397714 fbshipit-source-id: 3f32838 --- infer/src/biabduction/Propgraph.ml | 12 ++++++------ infer/src/biabduction/Propgraph.mli | 13 ++++++------- 2 files changed, 12 insertions(+), 13 deletions(-) diff --git a/infer/src/biabduction/Propgraph.ml b/infer/src/biabduction/Propgraph.ml index fcb8aee4b..718e2b29c 100644 --- a/infer/src/biabduction/Propgraph.ml +++ b/infer/src/biabduction/Propgraph.ml @@ -13,7 +13,7 @@ open! IStd module F = Format module L = Logging -type t = Prop.normal Prop.t +type 'a t = 'a Prop.t type sub_entry = Ident.t * Exp.t @@ -88,13 +88,13 @@ let edge_equal e1 e2 = (** [contains_edge footprint_part g e] returns true if the graph [g] contains edge [e], searching the footprint part if [footprint_part] is true. *) -let contains_edge (footprint_part: bool) (g: t) (e: edge) = +let contains_edge (footprint_part: bool) (g: _ t) (e: edge) = List.exists ~f:(fun e' -> edge_equal e e') (get_edges footprint_part g) (** Graph annotated with the differences w.r.t. a previous graph *) -type diff = - { diff_newgraph: t (** the new graph *) +type 'a diff = + { diff_newgraph: 'a t (** the new graph *) ; diff_changed_norm: Obj.t list (** objects changed in the normal part *) ; diff_cmap_norm: Pp.colormap (** colormap for the normal part *) ; diff_changed_foot: Obj.t list (** objects changed in the footprint part *) @@ -169,7 +169,7 @@ let compute_edge_diff (oldedge: edge) (newedge: edge) : Obj.t list = (** [compute_diff oldgraph newgraph] returns the list of edges which are only in [newgraph] *) -let compute_diff default_color oldgraph newgraph : diff = +let compute_diff default_color oldgraph newgraph : _ diff = let compute_changed footprint_part = let newedges = get_edges footprint_part newgraph in let changed = ref [] in @@ -224,7 +224,7 @@ let pp_proplist pe0 s (base_prop, extract_stack) f plist = let add_base_stack prop = if extract_stack then Prop.set prop ~sigma:(base_stack @ prop.Prop.sigma) else Prop.expose prop in - let update_pe_diff (prop: Prop.normal Prop.t) : Pp.env = + let update_pe_diff (prop: _ Prop.t) : Pp.env = if Config.print_using_diff then let diff = compute_diff Blue (from_prop base_prop) (from_prop prop) in let cmap_norm = diff_get_colormap false diff in diff --git a/infer/src/biabduction/Propgraph.mli b/infer/src/biabduction/Propgraph.mli index c33d7bf1d..a27b0394f 100644 --- a/infer/src/biabduction/Propgraph.mli +++ b/infer/src/biabduction/Propgraph.mli @@ -11,25 +11,24 @@ open! IStd (** Propositions seen as graphs *) (** prop considered as a graph *) -type t +type 'a t -val from_prop : Prop.normal Prop.t -> t +val from_prop : 'a Prop.t -> 'a t (** create a graph from a prop *) (** Graph annotated with the differences w.r.t. a previous graph *) -type diff +type 'a diff -val compute_diff : Pp.color -> t -> t -> diff +val compute_diff : Pp.color -> 'a t -> 'a t -> 'a diff (** [compute_diff default_color oldgraph newgraph] returns the list of edges which are only in [newgraph] *) -val diff_get_colormap : bool -> diff -> Pp.colormap +val diff_get_colormap : bool -> 'a diff -> Pp.colormap (** [diff_get_colormap footprint_part diff] returns the colormap of a computed diff, selecting the footprint colormap if [footprint_part] is true. *) val pp_proplist : - Pp.env -> string -> Prop.normal Prop.t * bool -> Format.formatter -> Prop.normal Prop.t list - -> unit + Pp.env -> string -> 'a Prop.t * bool -> Format.formatter -> 'b Prop.t list -> unit (** Print a list of propositions, prepending each one with the given string, If !Config.pring_using_diff is true, print the diff w.r.t. the given prop, extracting its local stack vars if the boolean is true. *)