Skip to content
Snippets Groups Projects
Commit 2f673a64 authored by Maxime Jacquemin's avatar Maxime Jacquemin
Browse files

[Kernel] State and List monads

parent b20b212c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/libraries/monads/list.ml 0 → 100644
+ 33
− 0
View file @ 2f673a64
(**************************************************************************)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
include Stdlib.List
module Minimal = struct
type 'a t = 'a list
let return x = [ x ]
let map f xs = map f xs
let flatten xs = flatten xs
let product ls rs = combine ls rs
end
include Monad.Extend_Categoric_with_product (Minimal)
src/libraries/monads/list.mli 0 → 100644
+ 24
− 0
View file @ 2f673a64
(**************************************************************************)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
include module type of Stdlib.List
include Monad.S_with_product with type 'a t = 'a list
src/libraries/monads/state_monad.ml 0 → 100644
+ 51
− 0
View file @ 2f673a64
(**************************************************************************)
(* *)
(* 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 Make (Env : Datatype.S_with_collections) = struct
module Cache = Env.Hashtbl
type 'a cache = 'a Cache.t
type env = Env.t
module Minimal = struct
type 'a t = ('a * env) cache option * (env -> 'a * env)
let return (x : 'a) : 'a t = (None, fun env -> x, env)
let compute ((cache, make) : 'a t) (env : env) : 'a * env =
match cache with
| None -> make env
| Some cache when Cache.mem cache env -> Cache.find cache env
| Some cache -> let r = make env in Cache.add cache env r ; r
let bind (f : 'a -> 'b t) (m : 'a t) : 'b t =
let make env = let a, env = compute m env in compute (f a) env in
(Some (Cache.create 13), make)
end
include Monad.Extend_Kleisli (Minimal)
let get_environment : env t = None, fun env -> env, env
let set_environment (env : env) : unit t = None, fun _ -> (), env
let resolve (m : 'a t) (env : env) : 'a * env = Minimal.compute m env
end
src/libraries/monads/state_monad.mli 0 → 100644
+ 29
− 0
View file @ 2f673a64
(**************************************************************************)
(* *)
(* 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 Make (Env : Datatype.S_with_collections) : sig
include Monad.S
type env = Env.t
val get_environment : env t
val set_environment : env -> unit t
val resolve : 'a t -> env -> 'a * env
end
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment