From 383229717e0d68e5cff4567cf35e19e48a7b1c19 Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Tue, 18 Jan 2022 15:10:29 +0100
Subject: [PATCH] [e-acsl] auxilliary functions for error management
---
src/plugins/e-acsl/src/analyses/interval.ml | 1 -
src/plugins/e-acsl/src/analyses/typing.ml | 3 +--
src/plugins/e-acsl/src/libraries/error.ml | 21 +++++++++++++++++++++
src/plugins/e-acsl/src/libraries/error.mli | 10 ++++++++--
4 files changed, 30 insertions(+), 5 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 86bcf2fb9a0..ac50f02b6a2 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -400,7 +400,6 @@ module Profile = struct
(struct
let module_name = "E_ACSL.Interval.Logic_function_env.Profile"
end)
- let is_included p1 p2 = List.for_all2 is_included p1 p2
end
(* Imperative environments *)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index d4022ccc0b1..6394220aca7 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -199,8 +199,7 @@ module Memo: sig
(term -> computed_info) ->
term ->
computed_info Error.result
- val get: lenv:Function_params_ty.t -> term ->
- computed_info Error.result
+ val get: lenv:Function_params_ty.t -> term -> computed_info Error.result
val clear: unit -> unit
end = struct
diff --git a/src/plugins/e-acsl/src/libraries/error.ml b/src/plugins/e-acsl/src/libraries/error.ml
index 1b32febdce7..4e23a570061 100644
--- a/src/plugins/e-acsl/src/libraries/error.ml
+++ b/src/plugins/e-acsl/src/libraries/error.ml
@@ -54,6 +54,9 @@ module type S = sig
Format.formatter ->
'a result ->
unit
+ val map: ('a -> 'b) -> 'a result -> 'b
+ val map2: ('a -> 'b -> 'c) -> 'a result -> 'b result -> 'c
+ val map3 : ('a -> 'b -> 'c -> 'd) -> 'a result -> 'b result -> 'c result -> 'd
end
module Make_with_opt(P: sig val phase:Options.category option end): S = struct
@@ -125,6 +128,24 @@ module Make_with_opt(P: sig val phase:Options.category option end): S = struct
match res with
| Result.Ok a -> Format.fprintf fmt "@[%a@]" pp a
| Result.Error err -> Format.fprintf fmt "@[%s@]" (Printexc.to_string err)
+
+ let map f = function
+ | Result.Ok a -> f a
+ | Result.Error e -> raise e
+
+ let map2 f a b =
+ match a,b with
+ | Result.Ok a, Result.Ok b -> f a b
+ | Result.Ok _, Result.Error e -> raise e
+ | Result.Error e, _ -> raise e
+
+ let map3 f a b c =
+ match a,b,c with
+ | Result.Ok a, Result.Ok b, Result.Ok c -> f a b c
+ | Result.Ok _, Result.Ok _, Result.Error e -> raise e
+ | Result.Ok _, Result.Error e, _ -> raise e
+ | Result.Error e, _, _ -> raise e
+
end
module Make(P: sig val phase:Options.category end): S =
diff --git a/src/plugins/e-acsl/src/libraries/error.mli b/src/plugins/e-acsl/src/libraries/error.mli
index 599ec5cd1bb..a4a690ab56a 100644
--- a/src/plugins/e-acsl/src/libraries/error.mli
+++ b/src/plugins/e-acsl/src/libraries/error.mli
@@ -81,8 +81,14 @@ module type S = sig
Format.formatter ->
'a result ->
unit
- (** [pp_result pp] where [pp] is a formatter for ['a] returns a formatter for
- ['a result]. *)
+ (** [pp_result pp] where [pp] is a formatter for ['a] returns a formatter for
+ ['a result]. *)
+
+ val map : ('a -> 'b) -> 'a result -> 'b
+ val map2 : ('a -> 'b -> 'c) -> 'a result -> 'b result -> 'c
+ val map3 : ('a -> 'b -> 'c -> 'd) -> 'a result -> 'b result -> 'c result -> 'd
+ (** Apply a function to one or several results and propagate the errors *)
+
end
(** Functor to build an [Error] module for a given [phase]. *)
--
GitLab