Commits

Paweł Wieczorek committed 1bfdaca

Lib.Algebra -> Lib_Algebra

Comments (0)

Files changed (13)

source/Lang/CWCPS/Analysis/CallGraphOfKnownFunctions.ml

 open AST
 open AnalysisFramework
 open Batteries
-open Lib.Algebra.Monoid
+open Lib_Algebra.Monoid
 open DataModuleTypes
 
 (*********************************************************************************************************************

source/Lang/CWCPS/Analysis/ClosureNeediness.ml

  *)
 
 open Batteries
-open Lib.Algebra.Monoid
+open Lib_Algebra.Monoid
 open AST
 
 (*
     module VariableSetMonoid = SetMonoid(VariableOrderedType)
     module VariableSetMonoidUtils = MonoidUtils(VariableSetMonoid)
 
-    module WorklistAlgorithm = Lib.Algebra.WorklistAlgorithm.MonoidBased(VariableSetMonoid)
+    module WorklistAlgorithm = Lib_Algebra.WorklistAlgorithm.MonoidBased(VariableSetMonoid)
 
     let free_variables = VariableSetMonoid.embed -| free_variables_of_expression
 

source/Lang/CWCPS/Analysis/SizeSavingAnalysis.ml

 open AST
 open AnalysisFramework
 open Batteries
-open Lib.Algebra.Monoid
+open Lib_Algebra.Monoid
 open DataModuleTypes
 
 (**

source/Lang/CWCPS/Analysis/VariableUsageAnalysis.ml

 open AST
 open AnalysisFramework
 open Batteries
-open Lib.Algebra.Monoid
+open Lib_Algebra.Monoid
 open DataModuleTypes
 
 (*********************************************************************************************************************

source/Lang/CWCPS/AnalysisFramework.ml

  *)
 
 open AST
-open Lib.Algebra.Monoid
+open Lib_Algebra.Monoid
 open Batteries
 
 (*********************************************************************************************************************

source/Lang/CWCPS/TransformationFramework.ml

  *)
 
 open AST
-open Lib.Algebra.Monoid
+open Lib_Algebra.Monoid
 open Lang_Common
 open Batteries
 

source/Lib.mlpack

-Algebra
 Toolchain

source/Lib/Algebra/Lattice.ml

-(*
- * Opifex
- *
- * Copyrights(C) 2012,2013 by Pawel Wieczorek <wieczyk at gmail>
- *)
-
-open Batteries
-
-(*********************************************************************************************************************
- * The Lattice (order structure)
- ********************************************************************************************************************)
-
-module type Lattice = sig
-
-    type t
-
-    val join : t -> t -> t
-
-    val meet : t -> t -> t
-
-    val top  : t
-
-    val bot  : t
-
-    val equal : t -> t -> bool
-
-end
-
-module DualLattice (L:Lattice) = struct
-
-    type t    = L.t
-
-    let join  = L.meet
-
-    let meet  = L.join
-
-    let top   = L.bot
-
-    let bot   = L.top
-   
-    let equal = L.equal
-
-end
-
-(*********************************************************************************************************************
- * Lattice utilities
- ********************************************************************************************************************)
-
-module LatticeUtils (L:Lattice) = struct
-
-    let joins = List.fold_left L.join L.bot 
-
-    let meets = List.fold_left L.meet L.top 
-
-    let join_map f xs = List.map f xs |> joins
-
-    let meet_map f xs = List.map f xs |> meets
-
-    let is_top = L.equal L.top
-
-    let not_is_top x = is_top x |> not
-
-    let is_bot = L.equal L.bot
-
-    let not_is_bot x = is_bot x |> not
-
-    let join_fold f data xs =
-        let f' data elem = joins [data; f data elem] in
-        List.fold_left f' data xs 
-end
-
-(*********************************************************************************************************************
- * The option (lifted) lattice
- ********************************************************************************************************************)
-
-module OptionLattice (L : Lattice) = struct
-
-    module Raw = struct
-
-        type t = L.t option
-
-        let join 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 (L.join a b)
-
-        let meet a b = match (a,b) with
-            | None, _ -> None
-            | _, None -> None
-            | Some a, Some b -> Some (L.meet a b)
-
-        let top = Some L.top
-
-        let bot = None
-
-        let equal a b = match a,b with
-            | None, None -> true
-            | Some a, Some b -> L.equal a b
-            | _ -> false
-
-    end
-
-    include Raw
-    include LatticeUtils(Raw)
-
-end
-
-(*********************************************************************************************************************
- * The Set lattice
- ********************************************************************************************************************)
-
-module SetLattice (V : Interfaces.OrderedType) = struct
-
-    module Raw = struct
-
-        module SV = Util.ExtSet(Set.Make(V))
-
-        type t
-            = TopSet of SV.t
-            | BotSet of SV.t
-
-        let top = TopSet SV.empty
-
-        let bot = BotSet SV.empty
-
-        let embed_botset x = BotSet x
-
-        let embed_topset x = TopSet x
-
-        let join a b = match (a,b) with
-            | TopSet a, TopSet b -> 
-                SV.inter a b 
-                |> embed_topset
-
-            | BotSet a, BotSet b ->
-                SV.union a b
-                |> embed_botset
-
-            (*
-             * x `in` (TOP \ A) + (BOT + B)
-             * iff x `in` TOP /\ x `not-in` A \/ x `in` BOT \/ x `in` B
-             * iff x `not-in` A \/ x `in` B
-             * iff not (x `not-not-in` A /\ x `not-in` B)
-             * iff not (x `in` A /\ x `not-in` B)
-             * iff x `not-in` A \ B
-             * iff x `in` TOP /\ `not-in` A \ B
-             *)
-            | TopSet a, BotSet b | BotSet b, TopSet a ->
-                SV.diff a b
-                |> embed_topset
-
-        let meet a b = match (a,b) with
-            | TopSet a, TopSet b -> 
-                SV.union a b 
-                |> embed_topset
-
-            | BotSet a, BotSet b ->
-                SV.inter a b
-                |> embed_botset
-
-            (*
-             * x `in` (TOP \ A) `inter` (BOT + B)
-             * iff x `in` TOP /\ x `not-in` A /\ (x `in` BOT \/ x `in` B)
-             * iff x `not-in` A /\ x `in` B
-             * iff x `in` B /\ x `not-in` A
-             * iff x `in` B \ A
-             *)
-            | TopSet a, BotSet b | BotSet b, TopSet a ->
-                SV.diff b a
-                |> embed_botset
-
-
-        let equal a b = match a,b with
-            | TopSet a, TopSet b ->
-                SV.equal a b
-
-            | BotSet a, BotSet b ->
-                SV.equal a b 
-
-            | _ ->
-                false
-
-
-        let from_list xs =
-            List.fold_right SV.add xs SV.empty 
-            |> embed_botset
-
-    end
-
-    include Raw
-    include LatticeUtils(Raw)
-
-end
-
-(*********************************************************************************************************************
- * The Map lattice
- ********************************************************************************************************************)
-
-
-module MapLattice (K : Map.OrderedType) (V : Lattice) = struct
-
-    module Raw = struct
-
-        module MK = Map.Make(K)
-        module OV = OptionLattice(V)
-
-        type t
-            = Map of V.t MK.t
-            | Top
-
-        let top = Top
-
-        let bot = Map MK.empty
-
-        let embed_map x = Map x
-
-        let join ma mb = match (ma, mb) with
-            | Top, _ -> Top
-            | _, Top -> Top
-            | Map ma, Map mb -> 
-                MK.merge (fun _ -> OV.join) ma mb
-                |> embed_map
-
-        let meet ma mb = match (ma, mb) with
-            | Top, a -> a
-            | a, Top -> a
-            | Map ma, Map mb -> 
-                MK.merge (fun _ -> OV.meet) ma mb
-                |> embed_map
-
-        let singleton k v = 
-            MK.singleton k v
-            |> embed_map
-           
-        let equal a b = match a,b with
-            | Top, Top ->
-                true
-
-            | Map a, Map b ->
-                MK.equal V.equal a b
-
-            | _ ->
-                false
-
-    end
-
-    include Raw
-
-    include LatticeUtils(Raw)
-
-end
-
-(*********************************************************************************************************************
- * Finite Partial Functions
- ********************************************************************************************************************)
-
-
-module FunLattice (K : Map.OrderedType) (V : Lattice) = struct
-
-    module Raw = struct
-
-        module MK = Map.Make(K)
-
-        module OV = OptionLattice(V)
-        module ODV = OptionLattice(DualLattice(V))
-
-        module VH = LatticeUtils(V)
-
-
-        (* Function encoding via maps:
-         * (BotDescr f)(x) = f(x)    when f(x) is defined
-         *                 = _BOT_   otherwise     
-         *
-         * (TopDescr f)(x) = f(x)    when f(x) is defined
-         *                 = _TOP_   otherwise
-         *)
-        type t
-            = BotDescr of V.t MK.t
-            | TopDescr of V.t MK.t
-
-
-        let embed_botdescr x = BotDescr (MK.filterv VH.not_is_bot x)
-
-        let embed_topdescr x = TopDescr (MK.filterv VH.not_is_top x)
-
-        (*
-         * MK.merge : (key -> 'a option -> 'b option -> 'c option) -> 'a MK.t -> 'b MK.t -> 'c MK.t
-         * Instead of writing operators for merging we use computations from the OptionLattice module
-         *)
-
-        let join ma mb = match (ma, mb) with
-            (* Cases:
-             *
-             * BotDescr-ma(x) `join` BotDescr-mb(x)
-             * Some a `OV.join` Some b
-             * = Some (a `V.join` b)
-             *
-             * BotDescr-ma(x) `join` BotDescr-mb(x)
-             * = Some a `OV.join` None
-             * = Some a
-             * = Some (a `V.join` V.bot)
-             *)
-            | BotDescr ma, BotDescr mb -> 
-                MK.merge (fun _ -> OV.join) ma mb
-                |> embed_botdescr
-
-            (* Cases:
-             *
-             * TopDescr-ma(x) `join` TopDescr-mb(x)
-             * = Some a `ODV.meet` Some b
-             * = Some (a `DV.meet` b)
-             * = Some (a `V.join` b)
-             *
-             * TopDescr-ma(x) `join` TopDescr-mb(x)
-             * = Some a `ODV.meet` None 
-             * = None
-             *)
-            | TopDescr ma, TopDescr mb -> 
-                MK.merge (fun _ -> ODV.meet) ma mb
-                |> embed_topdescr
-
-            (* Cases:
-             *
-             * TopDescr-ma(x) `join` BotDescr-mb(x)
-             * = Some a `join` Some b
-             * = Some (a `join` b)
-             *
-             * TopDescr-ma(x) `join` BotDescr-mb(x)
-             * = None `join` Some b
-             * = TOP `join` Some b
-             * = TOP
-             * = None
-             *
-             * TopDescr-ma(x) `join` BotDescr-mb(x)
-             * = Some a `join` None
-             * = Some a `join` BOT
-             * = Some a
-             *)
-            | TopDescr ma, BotDescr mb | BotDescr mb, TopDescr ma ->
-                let f a b = match a,b with
-                    | None, _        -> None
-                    | Some a, None   -> None
-                    | Some a, Some b -> Some (V.join a b)
-                    in
-                MK.merge (fun _ -> f) ma mb
-                |> embed_topdescr
-
-        let meet ma mb = match (ma, mb) with
-            | BotDescr ma, BotDescr mb -> 
-                MK.merge (fun _ -> OV.meet) ma mb
-                |> embed_botdescr
-
-            | TopDescr ma, TopDescr mb -> 
-                MK.merge (fun _ -> ODV.join) ma mb
-                |> embed_topdescr
-
-            (* Cases:
-             *
-             * TopDescr-ma(x) `meet` BotDescr-mb(x)
-             * = Some a `meet` Some b
-             * = Some (a `meet` b)
-             *
-             * TopDescr-ma(x) `meet` BotDescr-mb(x)
-             * = None `meet` Some b
-             * = TOP `meet` Some b
-             * = Some b
-             *
-             * TopDescr-ma(x) `join` BotDescr-mb(x)
-             * = Some a `meet` None
-             * = Some a `meet` BOT
-             * = BOT
-             * = None
-             *)
-            | TopDescr ma, BotDescr mb | BotDescr mb, TopDescr ma ->
-                let f a b = match a,b with
-                    | _, None        -> None
-                    | None, Some b   -> None
-                    | Some a, Some b -> Some (V.meet a b)
-                    in
-                MK.merge (fun _ -> f) ma mb
-                |> embed_botdescr
-
-        let call f x =
-            let find k def m = try MK.find k m with Not_found -> def in
-            match f with
-                | TopDescr m -> find x V.top m
-                | BotDescr m -> find x V.bot m
-
-        let update f x y =
-            match f with
-                | TopDescr m ->
-                    MK.add x y m
-                    |> embed_topdescr
-
-                | BotDescr m ->
-                    MK.add x y m
-                    |> embed_topdescr
-
-    end
-
-    include Raw
-
-end
-
-(*********************************************************************************************************************
- * Prepared
- ********************************************************************************************************************)
-
-module PreparedLattice = struct
-
-    module RawPlainIntLattice = struct
-
-        type t = int
-
-        let join a b = max a b
-
-        let meet a b = min a b
-
-        let top = max_int
-
-        let bot = min_int
-
-        let equal a b = a = b
-
-    end
-
-    module PlainIntLattice = struct
-
-        include RawPlainIntLattice
-        include LatticeUtils(RawPlainIntLattice)
-
-    end
-
-end

source/Lib/Algebra/Monoid.ml

-(*
- * Opifex
- *
- * Copyrights(C) 2012,2013 by Pawel Wieczorek <wieczyk at gmail>
- *)
-
-open Batteries
-open DataModuleTypes
-
-(*********************************************************************************************************************
- * The Monoid 
- *
- * Silently assumed to be.. abelian monoid, maybe should I change the name?
- ********************************************************************************************************************)
-
-module type Monoid = sig
-
-    type t
-
-    val oper     : t -> t -> t
-
-    val neutral  : t
-
-    val equal    : t -> t -> bool
-
-end
-
-(*********************************************************************************************************************
- * Monoid utilitites
- ********************************************************************************************************************)
-
-module MonoidUtils (M : Monoid) = struct
-
-    let opers = List.fold_left M.oper M.neutral
-
-    let oper_map f xs = List.map f xs |> opers
-
-    let is_neutral = M.equal M.neutral
-
-    let not_is_neutral x = is_neutral x |> not
-
-    let oper_fold f data xs =
-        let f' data elem = opers [data; f data elem] in
-        List.fold_left f' data xs 
-
-end
-
-(*********************************************************************************************************************
- * Tuple2 monoid
- ********************************************************************************************************************)
-
-module Tuple2Monoid (M1 : Monoid) (M2 : Monoid) = struct
-
-    module Raw = 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
-
-    include Raw
-    include MonoidUtils(Raw)
-
-end
-
-(*********************************************************************************************************************
- * Tuple3 monoid
- ********************************************************************************************************************)
-
-module Tuple3Monoid (M1 : Monoid) (M2 : Monoid) (M3 : Monoid) = struct
-
-    module Raw = struct
-
-        type t = M1.t * M2.t * M3.t
-
-        let equal (a1,b1,c1) (a2,b2,c2) =
-            M1.equal a1 a2 && M2.equal b1 b2 && M3.equal c1 c2
-
-        let neutral = (M1.neutral, M2.neutral, M3.neutral)
-
-        let oper (a1,b1,c1) (a2,b2,c2) = (M1.oper a1 a2, M2.oper b1 b2, M3.oper c1 c2)
-
-        let combine f g h a = (f a, g a, h a)
-
-    end
-
-    include Raw
-    include MonoidUtils(Raw)
-
-end
-
-(*********************************************************************************************************************
- * The option (lifted) monoid
- ********************************************************************************************************************)
-
-module OptionMonoid (M : Monoid) = struct
-
-    module Raw = 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
-
-    include Raw
-    include MonoidUtils(Raw)
-
-end
-
-
-(*********************************************************************************************************************
- * The one-shot partial monoid
- ********************************************************************************************************************)
-
-module OneShotPartialMonoid (M : EqType) = struct
-
-    exception Invariant_violation
-
-    module Raw = 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 -> raise Invariant_violation
-
-        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
-
-(*********************************************************************************************************************
- * The Set lattice
- ********************************************************************************************************************)
-
-
-module SetMonoid (V : Set.OrderedType) = struct
-
-    module Raw = struct
-
-        module SV = Util.ExtSet(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
-
-        let embed x = BotSet x
-
-        let diff_set m1 s2 = match m1 with
-            | BotSet s1 ->
-                BotSet (SV.diff s1 s2)
-
-        let diff m1 m2 = match m2 with
-            | BotSet s2 ->
-                diff_set m1 s2
-    end
-
-    include Raw
-    include MonoidUtils(Raw)
-
-end
-
-(*********************************************************************************************************************
- * The Map lattice
- ********************************************************************************************************************)
-
-
-module MapMonoid (K : Map.OrderedType) (V : Monoid) = struct
-
-    module Raw = struct
-
-        module MK = Util.ExtMap(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
-
-(*********************************************************************************************************************
- * Finite Partial Functions
- ********************************************************************************************************************)
-
-
-module FunMonoid (K : Map.OrderedType) (V : Monoid) = struct
-
-    module Raw = 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.filterv 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
-
-(*********************************************************************************************************************
- * Monoid from Lattice
- ********************************************************************************************************************)
-
-module MonoidFromLattice (L : Lattice.Lattice) = struct
-
-    module Raw = struct
-
-        type t = L.t
-
-        let oper = L.join
-
-        let neutral = L.bot
-
-        let equal = L.equal
-
-    end
-
-    include Raw
-    include MonoidUtils(Raw)
-
-end
-
-
-(*********************************************************************************************************************
- * 
- ********************************************************************************************************************)
-
-module PreparedMonoids = struct
-
-    (*-------------------------------------------------------------------------------------------
-     * IntSum Monoid
-     *)
-
-    module RawIntSumMonoid = struct
-
-        type t = int
-
-        let oper a b = a+b
-
-        let neutral = 0
-
-        let equal a b = a = b
-
-    end
-
-    module IntSumMonoid = struct
-
-        include RawIntSumMonoid
-        include MonoidUtils(RawIntSumMonoid)
-
-    end
-
-    (*-------------------------------------------------------------------------------------------
-     * IntSum Fun Monoid
-     *)
-
-    module SumInt_FunMonoid (K : Map.OrderedType ) = struct
-
-        include FunMonoid(K)(IntSumMonoid)
-
-    end
-
-
-    (*-------------------------------------------------------------------------------------------
-     * BoolSum Monoid
-     *)
-
-    module RawBoolSumMonoid = struct
-
-        type t = bool
-
-        let oper a b = a || b
-
-        let neutral = false
-
-        let equal a b = a = b
-
-    end
-
-    module BoolSumMonoid = struct
-
-        include RawBoolSumMonoid
-        include MonoidUtils(RawBoolSumMonoid)
-
-    end
-
-    (*-------------------------------------------------------------------------------------------
-     * BoolSum Fun Monoid
-     *)
-
-    module SumBool_FunMonoid (K : Map.OrderedType ) = struct
-
-        include FunMonoid(K)(BoolSumMonoid)
-
-    end
-
-
-
-end

source/Lib/Algebra/WorklistAlgorithm.ml

-open Batteries
-
-type ('a, 'b) result = ('a,'b) Hashtbl.t
-
-
-module MonoidBased (M : Monoid.Monoid) = struct
-
-
-    module Core = struct
-        module Utils = Monoid.MonoidUtils(M)
-
-        let compute f graph first =
-            let queue         = Queue.create () in
-            let result        = Hashtbl.create 512 in
-            let set_empty node =
-                    Hashtbl.replace result node M.neutral
-                    in
-            Graph.iter graph set_empty ;
-            Queue.push first queue;
-            try 
-
-                let rec loop () = 
-                    let node      = Queue.take queue in
-                    let old_value = Hashtbl.find result node in
-                    let parents   = Graph.get_parents graph node in
-                    let input     = Utils.oper_map (Hashtbl.find result) parents in
-                    let new_value = f node old_value input in
-                    if not (M.equal old_value new_value)
-                    then begin
-                        let children = Graph.get_children graph node in
-                        List.iter (fun node -> Queue.push node queue) children;
-                        Hashtbl.replace result node new_value
-                    end;
-                    loop ()
-                    in
-
-                loop ()
-            with Queue.Empty ->
-                result
-
-    end
-
-    module Simple = struct
-
-        let compute f = Core.compute (fun _ _ -> f)
-
-    end
-
-
-    
-
-end

source/Lib_Algebra/Lattice.ml

+(*
+ * Opifex
+ *
+ * Copyrights(C) 2012,2013 by Pawel Wieczorek <wieczyk at gmail>
+ *)
+
+open Batteries
+
+(*********************************************************************************************************************
+ * The Lattice (order structure)
+ ********************************************************************************************************************)
+
+module type Lattice = sig
+
+    type t
+
+    val join : t -> t -> t
+
+    val meet : t -> t -> t
+
+    val top  : t
+
+    val bot  : t
+
+    val equal : t -> t -> bool
+
+end
+
+module DualLattice (L:Lattice) = struct
+
+    type t    = L.t
+
+    let join  = L.meet
+
+    let meet  = L.join
+
+    let top   = L.bot
+
+    let bot   = L.top
+   
+    let equal = L.equal
+
+end
+
+(*********************************************************************************************************************
+ * Lattice utilities
+ ********************************************************************************************************************)
+
+module LatticeUtils (L:Lattice) = struct
+
+    let joins = List.fold_left L.join L.bot 
+
+    let meets = List.fold_left L.meet L.top 
+
+    let join_map f xs = List.map f xs |> joins
+
+    let meet_map f xs = List.map f xs |> meets
+
+    let is_top = L.equal L.top
+
+    let not_is_top x = is_top x |> not
+
+    let is_bot = L.equal L.bot
+
+    let not_is_bot x = is_bot x |> not
+
+    let join_fold f data xs =
+        let f' data elem = joins [data; f data elem] in
+        List.fold_left f' data xs 
+end
+
+(*********************************************************************************************************************
+ * The option (lifted) lattice
+ ********************************************************************************************************************)
+
+module OptionLattice (L : Lattice) = struct
+
+    module Raw = struct
+
+        type t = L.t option
+
+        let join 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 (L.join a b)
+
+        let meet a b = match (a,b) with
+            | None, _ -> None
+            | _, None -> None
+            | Some a, Some b -> Some (L.meet a b)
+
+        let top = Some L.top
+
+        let bot = None
+
+        let equal a b = match a,b with
+            | None, None -> true
+            | Some a, Some b -> L.equal a b
+            | _ -> false
+
+    end
+
+    include Raw
+    include LatticeUtils(Raw)
+
+end
+
+(*********************************************************************************************************************
+ * The Set lattice
+ ********************************************************************************************************************)
+
+module SetLattice (V : Interfaces.OrderedType) = struct
+
+    module Raw = struct
+
+        module SV = Util.ExtSet(Set.Make(V))
+
+        type t
+            = TopSet of SV.t
+            | BotSet of SV.t
+
+        let top = TopSet SV.empty
+
+        let bot = BotSet SV.empty
+
+        let embed_botset x = BotSet x
+
+        let embed_topset x = TopSet x
+
+        let join a b = match (a,b) with
+            | TopSet a, TopSet b -> 
+                SV.inter a b 
+                |> embed_topset
+
+            | BotSet a, BotSet b ->
+                SV.union a b
+                |> embed_botset
+
+            (*
+             * x `in` (TOP \ A) + (BOT + B)
+             * iff x `in` TOP /\ x `not-in` A \/ x `in` BOT \/ x `in` B
+             * iff x `not-in` A \/ x `in` B
+             * iff not (x `not-not-in` A /\ x `not-in` B)
+             * iff not (x `in` A /\ x `not-in` B)
+             * iff x `not-in` A \ B
+             * iff x `in` TOP /\ `not-in` A \ B
+             *)
+            | TopSet a, BotSet b | BotSet b, TopSet a ->
+                SV.diff a b
+                |> embed_topset
+
+        let meet a b = match (a,b) with
+            | TopSet a, TopSet b -> 
+                SV.union a b 
+                |> embed_topset
+
+            | BotSet a, BotSet b ->
+                SV.inter a b
+                |> embed_botset
+
+            (*
+             * x `in` (TOP \ A) `inter` (BOT + B)
+             * iff x `in` TOP /\ x `not-in` A /\ (x `in` BOT \/ x `in` B)
+             * iff x `not-in` A /\ x `in` B
+             * iff x `in` B /\ x `not-in` A
+             * iff x `in` B \ A
+             *)
+            | TopSet a, BotSet b | BotSet b, TopSet a ->
+                SV.diff b a
+                |> embed_botset
+
+
+        let equal a b = match a,b with
+            | TopSet a, TopSet b ->
+                SV.equal a b
+
+            | BotSet a, BotSet b ->
+                SV.equal a b 
+
+            | _ ->
+                false
+
+
+        let from_list xs =
+            List.fold_right SV.add xs SV.empty 
+            |> embed_botset
+
+    end
+
+    include Raw
+    include LatticeUtils(Raw)
+
+end
+
+(*********************************************************************************************************************
+ * The Map lattice
+ ********************************************************************************************************************)
+
+
+module MapLattice (K : Map.OrderedType) (V : Lattice) = struct
+
+    module Raw = struct
+
+        module MK = Map.Make(K)
+        module OV = OptionLattice(V)
+
+        type t
+            = Map of V.t MK.t
+            | Top
+
+        let top = Top
+
+        let bot = Map MK.empty
+
+        let embed_map x = Map x
+
+        let join ma mb = match (ma, mb) with
+            | Top, _ -> Top
+            | _, Top -> Top
+            | Map ma, Map mb -> 
+                MK.merge (fun _ -> OV.join) ma mb
+                |> embed_map
+
+        let meet ma mb = match (ma, mb) with
+            | Top, a -> a
+            | a, Top -> a
+            | Map ma, Map mb -> 
+                MK.merge (fun _ -> OV.meet) ma mb
+                |> embed_map
+
+        let singleton k v = 
+            MK.singleton k v
+            |> embed_map
+           
+        let equal a b = match a,b with
+            | Top, Top ->
+                true
+
+            | Map a, Map b ->
+                MK.equal V.equal a b
+
+            | _ ->
+                false
+
+    end
+
+    include Raw
+
+    include LatticeUtils(Raw)
+
+end
+
+(*********************************************************************************************************************
+ * Finite Partial Functions
+ ********************************************************************************************************************)
+
+
+module FunLattice (K : Map.OrderedType) (V : Lattice) = struct
+
+    module Raw = struct
+
+        module MK = Map.Make(K)
+
+        module OV = OptionLattice(V)
+        module ODV = OptionLattice(DualLattice(V))
+
+        module VH = LatticeUtils(V)
+
+
+        (* Function encoding via maps:
+         * (BotDescr f)(x) = f(x)    when f(x) is defined
+         *                 = _BOT_   otherwise     
+         *
+         * (TopDescr f)(x) = f(x)    when f(x) is defined
+         *                 = _TOP_   otherwise
+         *)
+        type t
+            = BotDescr of V.t MK.t
+            | TopDescr of V.t MK.t
+
+
+        let embed_botdescr x = BotDescr (MK.filterv VH.not_is_bot x)
+
+        let embed_topdescr x = TopDescr (MK.filterv VH.not_is_top x)
+
+        (*
+         * MK.merge : (key -> 'a option -> 'b option -> 'c option) -> 'a MK.t -> 'b MK.t -> 'c MK.t
+         * Instead of writing operators for merging we use computations from the OptionLattice module
+         *)
+
+        let join ma mb = match (ma, mb) with
+            (* Cases:
+             *
+             * BotDescr-ma(x) `join` BotDescr-mb(x)
+             * Some a `OV.join` Some b
+             * = Some (a `V.join` b)
+             *
+             * BotDescr-ma(x) `join` BotDescr-mb(x)
+             * = Some a `OV.join` None
+             * = Some a
+             * = Some (a `V.join` V.bot)
+             *)
+            | BotDescr ma, BotDescr mb -> 
+                MK.merge (fun _ -> OV.join) ma mb
+                |> embed_botdescr
+
+            (* Cases:
+             *
+             * TopDescr-ma(x) `join` TopDescr-mb(x)
+             * = Some a `ODV.meet` Some b
+             * = Some (a `DV.meet` b)
+             * = Some (a `V.join` b)
+             *
+             * TopDescr-ma(x) `join` TopDescr-mb(x)
+             * = Some a `ODV.meet` None 
+             * = None
+             *)
+            | TopDescr ma, TopDescr mb -> 
+                MK.merge (fun _ -> ODV.meet) ma mb
+                |> embed_topdescr
+
+            (* Cases:
+             *
+             * TopDescr-ma(x) `join` BotDescr-mb(x)
+             * = Some a `join` Some b
+             * = Some (a `join` b)
+             *
+             * TopDescr-ma(x) `join` BotDescr-mb(x)
+             * = None `join` Some b
+             * = TOP `join` Some b
+             * = TOP
+             * = None
+             *
+             * TopDescr-ma(x) `join` BotDescr-mb(x)
+             * = Some a `join` None
+             * = Some a `join` BOT
+             * = Some a
+             *)
+            | TopDescr ma, BotDescr mb | BotDescr mb, TopDescr ma ->
+                let f a b = match a,b with
+                    | None, _        -> None
+                    | Some a, None   -> None
+                    | Some a, Some b -> Some (V.join a b)
+                    in
+                MK.merge (fun _ -> f) ma mb
+                |> embed_topdescr
+
+        let meet ma mb = match (ma, mb) with
+            | BotDescr ma, BotDescr mb -> 
+                MK.merge (fun _ -> OV.meet) ma mb
+                |> embed_botdescr
+
+            | TopDescr ma, TopDescr mb -> 
+                MK.merge (fun _ -> ODV.join) ma mb
+                |> embed_topdescr
+
+            (* Cases:
+             *
+             * TopDescr-ma(x) `meet` BotDescr-mb(x)
+             * = Some a `meet` Some b
+             * = Some (a `meet` b)
+             *
+             * TopDescr-ma(x) `meet` BotDescr-mb(x)
+             * = None `meet` Some b
+             * = TOP `meet` Some b
+             * = Some b
+             *
+             * TopDescr-ma(x) `join` BotDescr-mb(x)
+             * = Some a `meet` None
+             * = Some a `meet` BOT
+             * = BOT
+             * = None
+             *)
+            | TopDescr ma, BotDescr mb | BotDescr mb, TopDescr ma ->
+                let f a b = match a,b with
+                    | _, None        -> None
+                    | None, Some b   -> None
+                    | Some a, Some b -> Some (V.meet a b)
+                    in
+                MK.merge (fun _ -> f) ma mb
+                |> embed_botdescr
+
+        let call f x =
+            let find k def m = try MK.find k m with Not_found -> def in
+            match f with
+                | TopDescr m -> find x V.top m
+                | BotDescr m -> find x V.bot m
+
+        let update f x y =
+            match f with
+                | TopDescr m ->
+                    MK.add x y m
+                    |> embed_topdescr
+
+                | BotDescr m ->
+                    MK.add x y m
+                    |> embed_topdescr
+
+    end
+
+    include Raw
+
+end
+
+(*********************************************************************************************************************
+ * Prepared
+ ********************************************************************************************************************)
+
+module PreparedLattice = struct
+
+    module RawPlainIntLattice = struct
+
+        type t = int
+
+        let join a b = max a b
+
+        let meet a b = min a b
+
+        let top = max_int
+
+        let bot = min_int
+
+        let equal a b = a = b
+
+    end
+
+    module PlainIntLattice = struct
+
+        include RawPlainIntLattice
+        include LatticeUtils(RawPlainIntLattice)
+
+    end
+
+end

source/Lib_Algebra/Monoid.ml

+(*
+ * Opifex
+ *
+ * Copyrights(C) 2012,2013 by Pawel Wieczorek <wieczyk at gmail>
+ *)
+
+open Batteries
+open DataModuleTypes
+
+(*********************************************************************************************************************
+ * The Monoid 
+ *
+ * Silently assumed to be.. abelian monoid, maybe should I change the name?
+ ********************************************************************************************************************)
+
+module type Monoid = sig
+
+    type t
+
+    val oper     : t -> t -> t
+
+    val neutral  : t
+
+    val equal    : t -> t -> bool
+
+end
+
+(*********************************************************************************************************************
+ * Monoid utilitites
+ ********************************************************************************************************************)
+
+module MonoidUtils (M : Monoid) = struct
+
+    let opers = List.fold_left M.oper M.neutral
+
+    let oper_map f xs = List.map f xs |> opers
+
+    let is_neutral = M.equal M.neutral
+
+    let not_is_neutral x = is_neutral x |> not
+
+    let oper_fold f data xs =
+        let f' data elem = opers [data; f data elem] in
+        List.fold_left f' data xs 
+
+end
+
+(*********************************************************************************************************************
+ * Tuple2 monoid
+ ********************************************************************************************************************)
+
+module Tuple2Monoid (M1 : Monoid) (M2 : Monoid) = struct
+
+    module Raw = 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
+
+    include Raw
+    include MonoidUtils(Raw)
+
+end
+
+(*********************************************************************************************************************
+ * Tuple3 monoid
+ ********************************************************************************************************************)
+
+module Tuple3Monoid (M1 : Monoid) (M2 : Monoid) (M3 : Monoid) = struct
+
+    module Raw = struct
+
+        type t = M1.t * M2.t * M3.t
+
+        let equal (a1,b1,c1) (a2,b2,c2) =
+            M1.equal a1 a2 && M2.equal b1 b2 && M3.equal c1 c2
+
+        let neutral = (M1.neutral, M2.neutral, M3.neutral)
+
+        let oper (a1,b1,c1) (a2,b2,c2) = (M1.oper a1 a2, M2.oper b1 b2, M3.oper c1 c2)
+
+        let combine f g h a = (f a, g a, h a)
+
+    end
+
+    include Raw
+    include MonoidUtils(Raw)
+
+end
+
+(*********************************************************************************************************************
+ * The option (lifted) monoid
+ ********************************************************************************************************************)
+
+module OptionMonoid (M : Monoid) = struct
+
+    module Raw = 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
+
+    include Raw
+    include MonoidUtils(Raw)
+
+end
+
+
+(*********************************************************************************************************************
+ * The one-shot partial monoid
+ ********************************************************************************************************************)
+
+module OneShotPartialMonoid (M : EqType) = struct
+
+    exception Invariant_violation
+
+    module Raw = 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 -> raise Invariant_violation
+
+        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
+
+(*********************************************************************************************************************
+ * The Set lattice
+ ********************************************************************************************************************)
+
+
+module SetMonoid (V : Set.OrderedType) = struct
+
+    module Raw = struct
+
+        module SV = Util.ExtSet(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
+
+        let embed x = BotSet x
+
+        let diff_set m1 s2 = match m1 with
+            | BotSet s1 ->
+                BotSet (SV.diff s1 s2)
+
+        let diff m1 m2 = match m2 with
+            | BotSet s2 ->
+                diff_set m1 s2
+    end
+
+    include Raw
+    include MonoidUtils(Raw)
+
+end
+
+(*********************************************************************************************************************
+ * The Map lattice
+ ********************************************************************************************************************)
+
+
+module MapMonoid (K : Map.OrderedType) (V : Monoid) = struct
+
+    module Raw = struct
+
+        module MK = Util.ExtMap(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
+
+(*********************************************************************************************************************
+ * Finite Partial Functions
+ ********************************************************************************************************************)
+
+
+module FunMonoid (K : Map.OrderedType) (V : Monoid) = struct
+
+    module Raw = 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.filterv 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
+
+(*********************************************************************************************************************
+ * Monoid from Lattice
+ ********************************************************************************************************************)
+
+module MonoidFromLattice (L : Lattice.Lattice) = struct
+
+    module Raw = struct
+
+        type t = L.t
+
+        let oper = L.join
+
+        let neutral = L.bot
+
+        let equal = L.equal
+
+    end
+
+    include Raw
+    include MonoidUtils(Raw)
+
+end
+
+
+(*********************************************************************************************************************
+ * 
+ ********************************************************************************************************************)
+
+module PreparedMonoids = struct
+
+    (*-------------------------------------------------------------------------------------------
+     * IntSum Monoid
+     *)
+
+    module RawIntSumMonoid = struct
+
+        type t = int
+
+        let oper a b = a+b
+
+        let neutral = 0
+
+        let equal a b = a = b
+
+    end
+
+    module IntSumMonoid = struct
+
+        include RawIntSumMonoid
+        include MonoidUtils(RawIntSumMonoid)
+
+    end
+
+    (*-------------------------------------------------------------------------------------------
+     * IntSum Fun Monoid
+     *)
+
+    module SumInt_FunMonoid (K : Map.OrderedType ) = struct
+
+        include FunMonoid(K)(IntSumMonoid)
+
+    end
+
+
+    (*-------------------------------------------------------------------------------------------
+     * BoolSum Monoid
+     *)
+
+    module RawBoolSumMonoid = struct
+
+        type t = bool
+
+        let oper a b = a || b
+
+        let neutral = false
+
+        let equal a b = a = b
+
+    end
+
+    module BoolSumMonoid = struct
+
+        include RawBoolSumMonoid
+        include MonoidUtils(RawBoolSumMonoid)
+
+    end
+
+    (*-------------------------------------------------------------------------------------------
+     * BoolSum Fun Monoid
+     *)
+
+    module SumBool_FunMonoid (K : Map.OrderedType ) = struct
+
+        include FunMonoid(K)(BoolSumMonoid)
+
+    end
+
+
+
+end

source/Lib_Algebra/WorklistAlgorithm.ml

+open Batteries
+
+type ('a, 'b) result = ('a,'b) Hashtbl.t
+
+
+module MonoidBased (M : Monoid.Monoid) = struct
+
+
+    module Core = struct
+        module Utils = Monoid.MonoidUtils(M)
+
+        let compute f graph first =
+            let queue         = Queue.create () in
+            let result        = Hashtbl.create 512 in
+            let set_empty node =
+                    Hashtbl.replace result node M.neutral
+                    in
+            Graph.iter graph set_empty ;
+            Queue.push first queue;
+            try 
+
+                let rec loop () = 
+                    let node      = Queue.take queue in
+                    let old_value = Hashtbl.find result node in
+                    let parents   = Graph.get_parents graph node in
+                    let input     = Utils.oper_map (Hashtbl.find result) parents in
+                    let new_value = f node old_value input in
+                    if not (M.equal old_value new_value)
+                    then begin
+                        let children = Graph.get_children graph node in
+                        List.iter (fun node -> Queue.push node queue) children;
+                        Hashtbl.replace result node new_value
+                    end;
+                    loop ()
+                    in
+
+                loop ()
+            with Queue.Empty ->
+                result
+
+    end
+
+    module Simple = struct
+
+        let compute f = Core.compute (fun _ _ -> f)
+
+    end
+
+
+    
+
+end