From 143c43a09febf823c7f8b2ddd3ed9886242282a0 Mon Sep 17 00:00:00 2001 From: Maxime Jacquemin <maxime.jacquemin@cea.fr> Date: Fri, 17 Jan 2025 13:24:05 +0100 Subject: [PATCH] [Kernel] Generic monads composition Based on distributives laws --- src/libraries/monads/composition.ml | 48 ++++++++++++++++++++++++++++ src/libraries/monads/composition.mli | 38 ++++++++++++++++++++++ 2 files changed, 86 insertions(+) create mode 100644 src/libraries/monads/composition.ml create mode 100644 src/libraries/monads/composition.mli diff --git a/src/libraries/monads/composition.ml b/src/libraries/monads/composition.ml new file mode 100644 index 0000000000..0364320faf --- /dev/null +++ b/src/libraries/monads/composition.ml @@ -0,0 +1,48 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2024 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +module type Axiom = sig + type 'a interior and 'a exterior + val swap : 'a exterior interior -> 'a interior exterior +end + +module Make + (Int : Monad.S) + (Ext : Monad.S) + (X : Axiom with type 'a interior = 'a Int.t and type 'a exterior = 'a Ext.t) += Monad.Make_based_on_map (struct + type 'a t = 'a Int.t Ext.t + let return x = Ext.return (Int.return x) + let map f m = Ext.map (Int.map f) m + let flatten m = Ext.map X.swap m |> Ext.flatten |> Ext.map Int.flatten +end) + +module Make_with_product + (Int : Monad.S_with_product) (Ext : Monad.S_with_product) + (X : Axiom with type 'a interior = 'a Int.t and type 'a exterior = 'a Ext.t) += Monad.Make_based_on_map_with_product (struct + type 'a t = 'a Int.t Ext.t + let return x = Ext.return (Int.return x) + let map f m = Ext.map (Int.map f) m + let flatten m = Ext.map X.swap m |> Ext.flatten |> Ext.map Int.flatten + let product l r = Ext.product l r |> Ext.map (fun (l, r) -> Int.product l r) +end) diff --git a/src/libraries/monads/composition.mli b/src/libraries/monads/composition.mli new file mode 100644 index 0000000000..33afc243e6 --- /dev/null +++ b/src/libraries/monads/composition.mli @@ -0,0 +1,38 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2024 *) +(* CEA (Commissariat à l'énergie atomique et aux énergies *) +(* alternatives) *) +(* *) +(* you can redistribute it and/or modify it under the terms of the GNU *) +(* Lesser General Public License as published by the Free Software *) +(* Foundation, version 2.1. *) +(* *) +(* It is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU Lesser General Public License for more details. *) +(* *) +(* See the GNU Lesser General Public License version 2.1 *) +(* for more details (enclosed in the file licenses/LGPLv2.1). *) +(* *) +(**************************************************************************) + +module type Axiom = sig + type 'a interior and 'a exterior + val swap : 'a exterior interior -> 'a interior exterior +end + +module Make + (Int : Monad.S) + (Ext : Monad.S) + (_ : Axiom with type 'a interior = 'a Int.t and type 'a exterior = 'a Ext.t) +: Monad.S with type 'a t = 'a Int.t Ext.t + +module Make_with_product + (Int : Monad.S_with_product) + (Ext : Monad.S_with_product) + (_ : Axiom with type 'a interior = 'a Int.t and type 'a exterior = 'a Ext.t) +: Monad.S_with_product with type 'a t = 'a Int.t Ext.t -- GitLab