# HG changeset patch # User Pawel Wieczorek # Date 1352235453 -3600 # Node ID 7240391878ec1fb707b64d66ef5ba028b88b3cb4 # Parent 70844288a8ef95c2f09e0a18dce62d18f91fe4ce better structure in Algebra_Monoid diff --git a/src/Lib/Algebra/Algebra_Monoid.ml b/src/Lib/Algebra/Algebra_Monoid.ml --- a/src/Lib/Algebra/Algebra_Monoid.ml +++ b/src/Lib/Algebra/Algebra_Monoid.ml @@ -49,27 +49,26 @@ * Tuple2 monoid ************************************************************************************************) -module MakeTuple2Monoid (M1 : Monoid) (M2 : Monoid) = struct - - type t = M1.t * M2.t - - let equal (a1,b1) (a2,b2) = - M1.equal a1 a2 && M2.equal b1 b2 - - let neutral = (M1.neutral, M2.neutral) - - let oper (a1,b1) (a2,b2) = (M1.oper a1 a2, M2.oper b1 b2) - - let combine f g a = (f a, g a) - -end module Tuple2Monoid (M1 : Monoid) (M2 : Monoid) = struct - module MM = MakeTuple2Monoid(M1)(M2) + module Raw = struct - include MM - include MonoidUtils(MM) + type t = M1.t * M2.t + + let equal (a1,b1) (a2,b2) = + M1.equal a1 a2 && M2.equal b1 b2 + + let neutral = (M1.neutral, M2.neutral) + + let oper (a1,b1) (a2,b2) = (M1.oper a1 a2, M2.oper b1 b2) + + let combine f g a = (f a, g a) + + end + + include Raw + include MonoidUtils(Raw) end @@ -78,31 +77,29 @@ * The option (lifted) lattice ************************************************************************************************) -module MakeOptionMonoid (M : Monoid) = struct - - type t = M.t option - - let oper a b = match (a,b) with - | None, None -> None - | Some a as t, None -> t - | None, (Some a as t) -> t - | Some a, Some b -> Some (M.oper a b) - - let neutral = None - - let equal a b = match a,b with - | None, None -> true - | Some a, Some b -> M.equal a b - | _ -> false - -end - module OptionMonoid (M : Monoid) = struct - module MM = MakeOptionMonoid(M) + module Raw = struct - include MM - include MonoidUtils(MM) + type t = M.t option + + let oper a b = match (a,b) with + | None, None -> None + | Some a as t, None -> t + | None, (Some a as t) -> t + | Some a, Some b -> Some (M.oper a b) + + let neutral = None + + let equal a b = match a,b with + | None, None -> true + | Some a, Some b -> M.equal a b + | _ -> false + + end + + include Raw + include MonoidUtils(Raw) end @@ -110,47 +107,46 @@ * The Set lattice ************************************************************************************************) -module MakeSetMonoid (V : Set.OrderedType) = struct - - module SV = Set.Make(V) - - type t - = BotSet of SV.t - - let neutral = BotSet SV.empty - - let embed_botset x = BotSet x - - let oper a b = match (a,b) with - | BotSet a, BotSet b -> - SV.union a b - |> embed_botset - - let equal a b = match a,b with - | BotSet a, BotSet b -> - SV.equal a b - - let from_list xs = - List.fold_right SV.add xs SV.empty - |> embed_botset - - let from_singleton = function - | BotSet m when SV.cardinal m > 1 -> - failwith "MakeSetMonoid.from_singleton" - - | BotSet m -> - m - |> SV.enum - |> Enum.get - -end module SetMonoid (V : Set.OrderedType) = struct - module M = MakeSetMonoid(V) + module Raw = struct - include M - include MonoidUtils(M) + module SV = Set.Make(V) + + type t + = BotSet of SV.t + + let neutral = BotSet SV.empty + + let embed_botset x = BotSet x + + let oper a b = match (a,b) with + | BotSet a, BotSet b -> + SV.union a b + |> embed_botset + + let equal a b = match a,b with + | BotSet a, BotSet b -> + SV.equal a b + + let from_list xs = + List.fold_right SV.add xs SV.empty + |> embed_botset + + let from_singleton = function + | BotSet m when SV.cardinal m > 1 -> + failwith "MakeSetMonoid.from_singleton" + + | BotSet m -> + m + |> SV.enum + |> Enum.get + + end + + include Raw + include MonoidUtils(Raw) end @@ -158,39 +154,38 @@ * The Map lattice ************************************************************************************************) -module MakeMapMonoid (K : Map.OrderedType) (V : Monoid) = struct - - module MK = Map.Make(K) - module OV = OptionMonoid(V) - - type t - = Map of V.t MK.t - - let neutral = Map MK.empty - - let embed_map x = Map x - - let oper ma mb = match (ma, mb) with - | Map ma, Map mb -> - MK.merge (fun _ -> OV.oper) ma mb - |> embed_map - - let singleton k v = - MK.singleton k v - |> embed_map - - let equal a b = match a,b with - | Map a, Map b -> - MK.equal V.equal a b - -end module MapMonoid (K : Map.OrderedType) (V : Monoid) = struct - module L = MakeMapMonoid(K)(V) + module Raw = struct - include L - include MonoidUtils(L) + module MK = Map.Make(K) + module OV = OptionMonoid(V) + + type t + = Map of V.t MK.t + + let neutral = Map MK.empty + + let embed_map x = Map x + + let oper ma mb = match (ma, mb) with + | Map ma, Map mb -> + MK.merge (fun _ -> OV.oper) ma mb + |> embed_map + + let singleton k v = + MK.singleton k v + |> embed_map + + let equal a b = match a,b with + | Map a, Map b -> + MK.equal V.equal a b + + end + + include Raw + include MonoidUtils(Raw) end @@ -198,63 +193,63 @@ * Finite Partial Functions ************************************************************************************************) -module MakeFunMonoid (K : Map.OrderedType) (V : Monoid) = struct - - module MK = Map.Make(K) - - module OV = OptionMonoid(V) - - module VH = MonoidUtils(V) - - type t - = BotDescr of V.t MK.t - - let neutral = BotDescr MK.empty - - let embed_botdescr x = BotDescr (MK.filter VH.not_is_neutral x) - - - let oper ma mb = match (ma, mb) with - | BotDescr ma, BotDescr mb -> - MK.merge (fun _ -> OV.oper) ma mb - |> embed_botdescr - - let equal ma mb = match (ma, mb) with - | BotDescr ma, BotDescr mb -> - MK.equal V.equal ma mb - - let call f x = - let find k def m = try MK.find k m with Not_found -> def in - match f with - | BotDescr m -> find x V.neutral m - - let update f x y = - match f with - | BotDescr m -> - MK.add x y m - |> embed_botdescr - - let singleton x y = - update neutral x y - - let from_list xs = - List.fold_right (uncurry MK.add) xs MK.empty - |> embed_botdescr - - let from_arg_list_with_val vl xs = - xs - |> List.map (fun a -> (a, vl)) - |> from_list - - let unhask (BotDescr m) = m - -end module FunMonoid (K : Map.OrderedType) (V : Monoid) = struct - module M = MakeFunMonoid(K)(V) + module Raw = struct - include M + module MK = Map.Make(K) + + module OV = OptionMonoid(V) + + module VH = MonoidUtils(V) + + type t + = BotDescr of V.t MK.t + + let neutral = BotDescr MK.empty + + let embed_botdescr x = BotDescr (MK.filter VH.not_is_neutral x) + + + let oper ma mb = match (ma, mb) with + | BotDescr ma, BotDescr mb -> + MK.merge (fun _ -> OV.oper) ma mb + |> embed_botdescr + + let equal ma mb = match (ma, mb) with + | BotDescr ma, BotDescr mb -> + MK.equal V.equal ma mb + + let call f x = + let find k def m = try MK.find k m with Not_found -> def in + match f with + | BotDescr m -> find x V.neutral m + + let update f x y = + match f with + | BotDescr m -> + MK.add x y m + |> embed_botdescr + + let singleton x y = + update neutral x y + + let from_list xs = + List.fold_right (uncurry MK.add) xs MK.empty + |> embed_botdescr + + let from_arg_list_with_val vl xs = + xs + |> List.map (fun a -> (a, vl)) + |> from_list + + let unhask (BotDescr m) = m + + end + + include Raw + include MonoidUtils(Raw) end @@ -262,24 +257,22 @@ * Monoid from Lattice ************************************************************************************************) -module MakeMonoidFromLattice (L : Algebra_Lattice.Lattice) = struct - - type t = L.t - - let oper = L.join - - let neutral = L.bot - - let equal = L.equal - -end - module MonoidFromLattice (L : Algebra_Lattice.Lattice) = struct - module MM = MakeMonoidFromLattice(L) + module Raw = struct - include MM - include MonoidUtils(MM) + type t = L.t + + let oper = L.join + + let neutral = L.bot + + let equal = L.equal + + end + + include Raw + include MonoidUtils(Raw) end