diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml index 1b68607c5f33e37bb8411418788e90641dfeec7e..7c7e4524ac864fd00f7c1fe4af6d68daec1ed9ce 100644 --- a/src/plugins/value/engine/abstractions.ml +++ b/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 diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli index 0156b516d8ad4b0e39cdad5baaa1986a5547e08b..8d646a00775e99109545b6707303e0040260526e 100644 --- a/src/plugins/value/engine/abstractions.mli +++ b/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 diff --git a/src/plugins/value/utils/structure.ml b/src/plugins/value/utils/structure.ml index b4594d86858954a47f88bde73a354b19fb66e8c4..e1e1d9b84d2ffedf7fd2cd16ac0aca5674a1a2b9 100644 --- a/src/plugins/value/utils/structure.ml +++ b/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 diff --git a/src/plugins/value/utils/structure.mli b/src/plugins/value/utils/structure.mli index 4e99e2232c44a05e33a4c4c167bb8fea9c02f8e0..96555303c0f1139131ae32877f80e65806b3583c 100644 --- a/src/plugins/value/utils/structure.mli +++ b/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