From 11c319909094afb80d920fa90509d5863a447845 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 17 Feb 2020 14:52:34 +0100
Subject: [PATCH] [Eva] Structure: adds an Option constructor for optional
values.
---
src/plugins/value/engine/abstractions.ml | 3 +++
src/plugins/value/utils/structure.ml | 15 +++++++++++++++
src/plugins/value/utils/structure.mli | 1 +
3 files changed, 19 insertions(+)
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index d393a206140..1b68607c5f3 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/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
diff --git a/src/plugins/value/utils/structure.ml b/src/plugins/value/utils/structure.ml
index 1d221ef7590..b4594d86858 100644
--- a/src/plugins/value/utils/structure.ml
+++ b/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) =
diff --git a/src/plugins/value/utils/structure.mli b/src/plugins/value/utils/structure.mli
index 51a5d26d183..4e99e2232c4 100644
--- a/src/plugins/value/utils/structure.mli
+++ b/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
--
GitLab