Update various utils

GillianCore/utils/ext_list.ml

@@ -33,6 +33,7 @@ let append x l =
       l.last <- cell
 
 let add = append
+let add_all xs t = List.iter (fun x -> add x t) xs
 let length t = t.length
 
 let to_list t =
@@ -210,6 +211,14 @@ let exists f l =
   in
   aux l.first
 
+let assoc_opt a l =
+  let rec aux = function
+    | Nil -> None
+    | Cons { contents = k, v; _ } when a = k -> Some v
+    | Cons { next; _ } -> aux next
+  in
+  aux l.first
+
 let nth n l =
   if n >= l.length || n < 0 then None
   else

GillianCore/utils/ext_list.mli

@@ -11,6 +11,7 @@ val clear : 'a t -> unit
 val prepend : 'a -> 'a t -> unit
 val append : 'a -> 'a t -> unit
 val add : 'a -> 'a t -> unit
+val add_all : 'a list -> 'a t -> unit
 val length : 'a t -> int
 val to_list : 'a t -> 'a list
 val of_list : 'a list -> 'a t
@@ -31,6 +32,7 @@ val iter : ('a -> unit) -> 'a t -> unit
 val for_all2 : ('a -> 'b -> bool) -> 'a t -> 'b t -> bool
 
 val exists : ('a -> bool) -> 'a t -> bool
+val assoc_opt : 'a -> ('a * 'b) t -> 'b option
 val remove_duplicates : ?equal:('a -> 'a -> bool) -> 'a t -> unit
 
 (** Filter-maps the list in place according to [f]

GillianCore/utils/list_utils.ml

@@ -175,6 +175,16 @@ let map_results f l =
   in
   aux [] l
 
+let iter_results f l =
+  let rec aux = function
+    | [] -> Ok ()
+    | x :: xs -> (
+        match f x with
+        | Ok () -> aux xs
+        | Error e -> Error e)
+  in
+  aux l
+
 let for_alli f l =
   let rec aux i = function
     | [] -> true

GillianCore/utils/result_utils.ml

@@ -2,3 +2,7 @@ let of_option ~none x =
   match x with
   | None -> Error none
   | Some x -> Ok x
+
+let or_else f = function
+  | Ok x -> x
+  | Error e -> f e

GillianCore/utils/syntaxes.ml

@@ -16,8 +16,43 @@ end
 
 (** @canonical Gillian.Utils.Syntaxes.Option *)
 module Option = struct
-  let ( let+ ) f o = Option.map o f
+  let ( let+ ) o f = Option.map f o
   let ( let* ) o f = Option.bind o f
+
+  let ( let- ) o f =
+    match o with
+    | None -> f ()
+    | Some o -> o
+
+  let ( let/ ) o f =
+    match o with
+    | None -> f ()
+    | o -> o
+end
+
+(** @canonical Gillian.Utils.Syntaxes.Result_of_option *)
+module Result_of_option = struct
+  let ( let=* ) o f =
+    match o with
+    | Ok (Some o) -> f o
+    | Ok None -> Ok None
+    | Error e -> Error e
+
+  let ( let=+ ) o f =
+    match o with
+    | Ok (Some o) -> Ok (Some (f o))
+    | Ok None -> Ok None
+    | Error e -> Error e
+
+  let ( let=/ ) o f =
+    match o with
+    | Ok None -> f ()
+    | o -> o
+
+  let ( let=- ) o f =
+    match o with
+    | Ok None -> Ok (Some (f ()))
+    | o -> o
 end
 
 (** @canonical Gillian.Utils.Syntaxes.List *)