[Eva] Structure: adds a Void constructor for undescribed values of any type.

src/plugins/value/engine/abstractions.ml

@@ -221,6 +221,10 @@ module Internal_Value = struct
         let structure = Node (Value.structure, Leaf (key, v))
       end)
 
+  let void_value () =
+    Value_parameters.fatal
+      "Cannot register a value module from a Void structure."
+
   let add_value_structure value internal =
     let rec aux: type v. (module Internal) -> v structure -> (module Internal) =
       fun value -> function
@@ -228,6 +232,7 @@ module Internal_Value = struct
         | Leaf (key, v) -> add_value_leaf value (V (key, v))
         | Node (s1, s2) -> aux (aux value s1) s2
         | Unit -> value
+        | Void -> void_value ()
     in
     aux value internal
 
@@ -261,6 +266,7 @@ module Internal_Value = struct
           fun (v1, v2) value -> set1 v1 (set2 v2 value)
         | Option (s, default) -> fun v -> set s (Extlib.opt_conv default v)
         | Unit -> fun () value -> value
+        | Void -> void_value ()
       in
       set structure
 
@@ -274,6 +280,7 @@ module Internal_Value = struct
           fun v -> get1 v, get2 v
         | Option (s, _) -> fun v -> Some (get s v)
         | Unit -> fun _ -> ()
+        | Void -> void_value ()
       in
       get structure
 

src/plugins/value/engine/abstractions.mli

@@ -31,7 +31,8 @@
 *)
 
 (** Module types of value abstractions: either a single leaf module, or
-    a compound of several modules described by a structure. *)
+    a compound of several modules described by a structure. In this last case,
+    the structure must not contain the Void constructor. *)
 type 'v value =
   | Single of (module Abstract_value.Leaf with type t = 'v)
   | Struct of 'v Abstract.Value.structure

src/plugins/value/utils/structure.ml

@@ -69,6 +69,7 @@ module type Shape = sig
 
   type 'a structure =
     | Unit : unit structure
+    | Void : 'a structure
     | Leaf : 'a key * 'a data -> 'a structure
     | Node : 'a structure * 'b structure -> ('a * 'b) structure
     | Option : 'a structure * 'a -> 'a option structure
@@ -82,6 +83,7 @@ module Shape (Key: Key) (Data: sig type 'a t end) = struct
 
   type 'a structure =
     | Unit : unit structure
+    | Void : 'a structure
     | Leaf : 'a key * 'a data -> 'a structure
     | Node : 'a structure * 'b structure -> ('a * 'b) structure
     | Option : 'a structure * 'a -> 'a option structure
@@ -137,7 +139,7 @@ module Open
   open Shape
 
   let rec mem : type a. 'v Shape.key -> a structure -> bool = fun key -> function
-    | Unit -> false
+    | Unit | Void -> false
     | Leaf (k, _) -> Shape.equal key k
     | Node (left, right) -> mem key left || mem key right
     | Option (s, _) -> mem key s
@@ -152,7 +154,7 @@ module Open
   let lift_get f (Get (key, get)) = Get (key, fun t -> get (f t))
 
   let rec compute_getters : type a. a structure -> (a getter) KMap.t = function
-    | Unit -> KMap.empty
+    | Unit | Void -> KMap.empty
     | Leaf (key, _) ->  KMap.singleton key (Get (key, fun (t : a) -> t))
     | Node (left, right) ->
       let l = compute_getters left and r = compute_getters right in
@@ -178,7 +180,7 @@ module Open
   let lift_set f (Set (key, set)) = Set (key, fun v b -> f (fun a -> set v a) b)
 
   let rec compute_setters : type a. a structure -> (a setter) KMap.t = function
-    | Unit -> KMap.empty
+    | Unit | Void -> KMap.empty
     | Leaf (key, _) -> KMap.singleton key (Set (key, fun v _t -> v))
     | Node (left, right) ->
       let l = compute_setters left and r = compute_setters right in

src/plugins/value/utils/structure.mli

@@ -62,6 +62,7 @@ module type Shape = sig
       Used internally to automatically generate efficient accessors of its nodes. *)
   type 'a structure =
     | Unit : unit structure
+    | Void : 'a structure
     | Leaf : 'a key * 'a data -> 'a structure
     | Node : 'a structure * 'b structure -> ('a * 'b) structure
     | Option : 'a structure * 'a -> 'a option structure