[Eva] Structure: separates keys and shapes in two distinct modules.

Keys for abstract values, locations and states are created in structure.ml.
Shapes are created in the respective modules Value, Location and Domain
in abstract.ml.

src/plugins/value/domains/numerors/numerors_domain.ok.ml

@@ -88,7 +88,7 @@ module Numerors_Value = struct
 end
 
 let add_numerors_value (module Value: Abstract.Value.Internal) =
-  let module External_Value = Structure.Open (Structure.Key_Value) (Value) in
+  let module External_Value = Structure.Open (Abstract.Value) (Value) in
   let module V = struct
     include Value_product.Make (Value) (Numerors_value)
 

src/plugins/value/engine/abstractions.ml

@@ -114,7 +114,7 @@ end
 
 module CVal = struct
   include Internal_CVal
-  include Structure.Open (Structure.Key_Value) (Internal_CVal)
+  include Structure.Open (Abstract.Value) (Internal_CVal)
 end
 
 module Internal_PLoc = struct
@@ -153,7 +153,7 @@ let open_value_abstraction value =
   let module Value = (val value : Abstract.Value.Internal) in
   (module struct
     include Value
-    include Structure.Open (Structure.Key_Value) (Value)
+    include Structure.Open (Abstract.Value) (Value)
   end : V)
 
 let build_value config =
@@ -321,7 +321,7 @@ let add_generic_equalities (module Acc : Abstract) =
 
 let add_equalities (type v) (module Acc : Abstract with type Val.t = v) =
   match Acc.Val.structure with
-  | Structure.Key_Value.Leaf key ->
+  | Abstract.Value.Leaf key ->
     begin
       match Structure.Key_Value.eq_type key Main_values.CVal.key with
       | None -> add_generic_equalities (module Acc)
@@ -493,7 +493,7 @@ let build_abstractions config =
   let module V = (val value : V) in
   let abstractions =
     match V.structure with
-    | Structure.Key_Value.Leaf key
+    | Abstract.Value.Leaf key
       when Structure.Key_Value.equal key Main_values.CVal.key ->
       default_root_abstraction config
     | _ -> build_root_abstraction config value
@@ -617,17 +617,17 @@ module Reduce (Value : Abstract.Value.External) = struct
 end
 
 let open_abstractions abstraction =
-  let module Abstract = (val abstraction : Abstract) in
-  let module Val = Reduce (Abstract.Val) in
+  let module Acc = (val abstraction : Abstract) in
+  let module Val = Reduce (Acc.Val) in
   let module Loc = struct
-    include Abstract.Loc
+    include Acc.Loc
     include Structure.Open
-        (Structure.Key_Location)
-        (struct include Abstract.Loc type t = location end)
+        (Abstract.Location)
+        (struct include Acc.Loc type t = location end)
   end in
   let module Domain = struct
-    include Abstract.Dom
-    include Structure.Open (Structure.Key_Domain) (Abstract.Dom)
+    include Acc.Dom
+    include Structure.Open (Abstract.Domain) (Acc.Dom)
   end in
   (module struct
     module Val = Val

src/plugins/value/register.ml

@@ -176,7 +176,7 @@ end
 
 module Val = struct
   include CVal
-  include Structure.Open (Structure.Key_Value) (CVal)
+  include Structure.Open (Abstract.Value) (CVal)
   let reduce t = t
 end
 

src/plugins/value/utils/abstract.ml

@@ -30,7 +30,7 @@ module type Interface = sig
 end
 
 module Value = struct
-  include Structure.Key_Value
+  include Structure.Shape (Structure.Key_Value)
 
   module type Internal = sig
     include Abstract_value.S
@@ -45,7 +45,7 @@ module Value = struct
 end
 
 module Location = struct
-  include Structure.Key_Location
+  include Structure.Shape (Structure.Key_Location)
 
   module type Internal = sig
     include Abstract_location.S
@@ -60,7 +60,7 @@ module Location = struct
 end
 
 module Domain = struct
-  include Structure.Key_Domain
+  include Structure.Shape (Structure.Key_Domain)
 
   module type Internal = sig
     include Abstract_domain.Internal

src/plugins/value/utils/abstract.mli

@@ -60,7 +60,6 @@ end
 module Value : sig
   include Structure.Shape
     with type 'a key = 'a Structure.Key_Value.key
-     and type 'a structure = 'a Structure.Key_Value.structure
 
   module type Internal = sig
     include Abstract_value.S
@@ -79,7 +78,6 @@ end
 module Location : sig
   include Structure.Shape
     with type 'a key = 'a Structure.Key_Location.key
-     and type 'a structure = 'a Structure.Key_Location.structure
 
   module type Internal = sig
     include Abstract_location.S
@@ -98,7 +96,6 @@ end
 module Domain : sig
   include Structure.Shape
     with type 'a key = 'a Structure.Key_Domain.key
-     and type 'a structure = 'a Structure.Key_Domain.structure
 
   module type Internal = sig
     include Abstract_domain.Internal

src/plugins/value/utils/structure.ml

@@ -36,16 +36,6 @@ module type Key = sig
   val tag: 'a key -> int
 end
 
-module type Shape = sig
-  include Key
-
-  type 'a structure =
-    | Void : 'a structure
-    | Leaf : 'a key -> 'a structure
-    | Node : 'a structure * 'b structure -> ('a * 'b) structure
-end
-
-
 module Make (X : sig end) = struct
 
   type 'a key = { tag: int;
@@ -67,17 +57,43 @@ module Make (X : sig end) = struct
   let tag x = x.tag
 
   let print fmt x = Format.pp_print_string fmt x.name
+end
+
+module Key_Value = Make (struct end)
+module Key_Location = Make (struct end)
+module Key_Domain = Make (struct end)
+
+module type Shape = sig
+  include Key
 
   type 'a structure =
     | Void : 'a structure
     | Leaf : 'a key -> 'a structure
     | Node : 'a structure * 'b structure -> ('a * 'b) structure
+
+  val eq_structure: 'a structure -> 'b structure -> ('a, 'b) eq option
 end
 
-module Key_Value = Make (struct end)
-module Key_Location = Make (struct end)
-module Key_Domain = Make (struct end)
+module Shape (Key: Key) = struct
+  include Key
 
+  type 'a structure =
+    | Void : 'a structure
+    | Leaf : 'a Key.key -> 'a structure
+    | Node : 'a structure * 'b structure -> ('a * 'b) structure
+
+  let rec eq_structure : type a b. a structure -> b structure -> (a, b) eq option
+    = fun a b ->
+      match a, b with
+      | Leaf key1, Leaf key2 -> Key.eq_type key1 key2
+      | Node (l1, r1), Node (l2, r2) ->
+        begin
+          match eq_structure l1 l2, eq_structure r1 r2 with
+          | Some Eq, Some Eq -> Some Eq
+          | _, _ -> None
+        end
+      | _, _ -> None
+end
 
 module type Internal = sig
   type t
@@ -93,7 +109,6 @@ module type External = sig
   val set : 'a key -> 'a -> t -> t
 end
 
-
 module Open
     (Shape : Shape)
     (M : sig type t val structure : t Shape.structure end)

src/plugins/value/utils/structure.mli

@@ -41,6 +41,17 @@ module type Key = sig
   val tag: 'a key -> int
 end
 
+module Make (X : sig end) : Key
+
+(** Keys module for the abstract values of Eva. *)
+module Key_Value : Key
+
+(** Keys module for the abstract locations of Eva. *)
+module Key_Location : Key
+
+(** Keys module for the abstract domains of Eva. *)
+module Key_Domain : Key
+
 (** A Key module with its structure type. *)
 module type Shape = sig
   include Key
@@ -52,20 +63,11 @@ module type Shape = sig
     | Void : 'a structure
     | Leaf : 'a key -> 'a structure
     | Node : 'a structure * 'b structure -> ('a * 'b) structure
-end
 
-module Make (X : sig end) : Shape
-
-
-(** Keys module for the abstract values of Eva. *)
-module Key_Value : Shape
-
-(** Keys module for the abstract locations of Eva. *)
-module Key_Location : Shape
-
-(** Keys module for the abstract domains of Eva. *)
-module Key_Domain : Shape
+  val eq_structure: 'a structure -> 'b structure -> ('a, 'b) eq option
+end
 
+module Shape (Key : Key) : Shape with type 'a key = 'a Key.key
 
 (** Internal view of the tree, with the structure. *)
 module type Internal = sig