[Eva] Structure: adds an Option constructor for optional values.

src/plugins/value/engine/abstractions.ml

@@ -224,6 +224,7 @@ module Internal_Value = struct
   let add_value_structure value internal =
     let rec aux: type v. (module Internal) -> v structure -> (module Internal) =
       fun value -> function
+        | Option (s, _) -> aux value s
         | Leaf (key, v) -> add_value_leaf value (V (key, v))
         | Node (s1, s2) -> aux (aux value s1) s2
         | Unit -> value
@@ -258,6 +259,7 @@ module Internal_Value = struct
         | Node (s1, s2) ->
           let set1 = set s1 and set2 = set s2 in
           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
       in
       set structure
@@ -270,6 +272,7 @@ module Internal_Value = struct
         | Node (s1, s2) ->
           let get1 = get s1 and get2 = get s2 in
           fun v -> get1 v, get2 v
+        | Option (s, _) -> fun v -> Some (get s v)
         | Unit -> fun _ -> ()
       in
       get structure

src/plugins/value/utils/structure.ml

@@ -71,6 +71,7 @@ module type Shape = sig
     | Unit : unit structure
     | Leaf : 'a key * 'a data -> 'a structure
     | Node : 'a structure * 'b structure -> ('a * 'b) structure
+    | Option : 'a structure * 'a -> 'a option structure
 
   val eq_structure: 'a structure -> 'b structure -> ('a, 'b) eq option
 end
@@ -83,6 +84,7 @@ module Shape (Key: Key) (Data: sig type 'a t end) = struct
     | Unit : unit structure
     | Leaf : 'a key * 'a data -> 'a structure
     | Node : 'a structure * 'b structure -> ('a * 'b) structure
+    | Option : 'a structure * 'a -> 'a option structure
 
   let rec eq_structure : type a b. a structure -> b structure -> (a, b) eq option
     = fun a b ->
@@ -94,6 +96,12 @@ module Shape (Key: Key) (Data: sig type 'a t end) = struct
           | Some Eq, Some Eq -> Some Eq
           | _, _ -> None
         end
+      | Option (s1, _), Option (s2, _) ->
+        begin
+          match eq_structure s1 s2 with
+          | Some Eq -> Some Eq
+          | None -> None
+        end
       | Unit, Unit -> Some Eq
       | _, _ -> None
 end
@@ -132,6 +140,7 @@ module Open
     | Unit -> false
     | Leaf (k, _) -> Shape.equal key k
     | Node (left, right) -> mem key left || mem key right
+    | Option (s, _) -> mem key s
 
   let mem key = mem key M.structure
 
@@ -149,6 +158,9 @@ module Open
       let l = compute_getters left and r = compute_getters right in
       let l = KMap.map (lift_get fst) l and r = KMap.map (lift_get snd) r in
       KMap.union (fun _k a _b -> Some a) l r
+    | Option (s, default) ->
+      let l = compute_getters s in
+      KMap.map (lift_get (Extlib.opt_conv default)) l
 
   let getters = compute_getters M.structure
   let get (type a) (key: a Shape.key) : (M.t -> a) option =
@@ -173,6 +185,9 @@ module Open
       let l = KMap.map (lift_set (fun set (l, r) -> set l, r)) l
       and r = KMap.map (lift_set (fun set (l, r) -> l, set r)) r in
       KMap.union (fun _k a _b -> Some a) l r
+    | Option (s, _) ->
+      let l = compute_setters s in
+      KMap.map (lift_set Extlib.opt_map) l
 
   let setters = compute_setters M.structure
   let set (type a) (key: a Shape.key) : (a -> M.t -> M.t) =

src/plugins/value/utils/structure.mli

@@ -64,6 +64,7 @@ module type Shape = sig
     | Unit : unit structure
     | Leaf : 'a key * 'a data -> 'a structure
     | Node : 'a structure * 'b structure -> ('a * 'b) structure
+    | Option : 'a structure * 'a -> 'a option structure
 
   val eq_structure: 'a structure -> 'b structure -> ('a, 'b) eq option
 end