From 052cd89d7a6cc87a3a9627166257ebaf6849a712 Mon Sep 17 00:00:00 2001
From: Dara LY <dara.ly@cea.fr>
Date: Thu, 18 Apr 2019 16:19:25 +0200
Subject: [PATCH] implement structural comparison for logic_info
---
.../ast_queries/cil_datatype.ml | 48 +++++++++++++++++++
.../ast_queries/cil_datatype.mli | 1 +
2 files changed, 49 insertions(+)
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index f0b07d285ac..30ed9edaa84 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -1357,6 +1357,54 @@ let rec hash_logic_type config = function
| Larrow (_,t) -> 41 * hash_logic_type config t
+(* Logic_info with structural comparison
+ if functions / predicates have the same name (overloading), compare
+ their arguments types ; ignore polymorphism *)
+module Logic_info_structural = struct
+ let pretty_ref = ref (fun fmt f -> Logic_var.pretty fmt f.l_var_info)
+ include Make_with_collections
+ (struct
+ type t = logic_info
+ let name = "Logic_info_structural"
+ let reprs =
+ List.map
+ (fun v ->
+ { l_var_info = v;
+ l_labels = [];
+ l_tparams = [];
+ l_type = None;
+ l_profile = [];
+ l_body = LBnone })
+ Logic_var.reprs
+ let compare i1 i2 =
+ match String.compare i1.l_var_info.lv_name i2.l_var_info.lv_name with
+ | (-1 | 1) as res -> res
+ | _ ->
+ let rec profile_cmp p1 p2 = match p1, p2 with
+ | [], [] -> 0
+ | [], _ -> -1
+ | _, [] -> 1
+ | h1::t1, h2::t2 ->
+ let ty1 = h1.lv_type in
+ let ty2 = h2.lv_type in
+ let config = { by_name = true ;
+ logic_type = true ;
+ unroll = true } in
+ match compare_logic_type config ty1 ty2 with
+ | (-1 | 1) as res -> res
+ | _ -> profile_cmp t1 t2
+ in
+ profile_cmp i1.l_profile i2.l_profile
+
+ let equal i1 i2 = Logic_var.equal i1.l_var_info i2.l_var_info
+ let hash i = Logic_var.hash i.l_var_info
+ let copy = Datatype.undefined
+ let internal_pretty_code = Datatype.undefined
+ let pretty = !pretty_ref
+ let varname _ = "logic_varinfo"
+ end)
+end
+
(* Shared between the different modules for logic types *)
let pretty_logic_type_ref = ref (fun _ _ -> assert false)
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index 983c6ba3a37..9e98b281b8e 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -256,6 +256,7 @@ module Identified_term: S_with_collections_pretty with type t = identified_term
module Logic_ctor_info: S_with_collections_pretty with type t = logic_ctor_info
module Logic_info: S_with_collections_pretty with type t = logic_info
+module Logic_info_structural: S_with_collections_pretty with type t = logic_info
module Logic_constant: S_with_collections_pretty with type t = logic_constant
module Logic_label: S_with_collections_pretty with type t = logic_label
--
GitLab