packages feed

liquid-fixpoint-0.1.0.0: external/ocamlgraph/src/blocks.ml

(**************************************************************************)
(*                                                                        *)
(*  Ocamlgraph: a generic graph library for OCaml                         *)
(*  Copyright (C) 2004-2007                                               *)
(*  Sylvain Conchon, Jean-Christophe Filliatre and Julien Signoles        *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2, with the special exception on linking              *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software 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.                  *)
(*                                                                        *)
(**************************************************************************)

(* $Id: per_imp.ml,v 1.32 2006-02-03 09:27:29 filliatr Exp $ *)

(** Common implementation to persistent and imperative graphs. *)

open Sig
open Util

let cpt_vertex = ref min_int
  (* global counter for abstract vertex *)

(* ************************************************************************* *)
(** {2 Association table builder} *)
(* ************************************************************************* *)

(** Common signature to an imperative/persistent association table *)
module type HM = sig
  type 'a return
  type 'a t
  type key
  val create : int -> 'a t
  val create_from : 'a t -> 'a t
  val empty : 'a return
  val is_empty : 'a t -> bool
  val add : key -> 'a -> 'a t -> 'a t
  val remove : key -> 'a t -> 'a t
  val mem : key -> 'a t -> bool
  val find : key -> 'a t -> 'a
  val find_and_raise : key -> 'a t -> string -> 'a
    (** [find_and_raise k t s] is equivalent to [find k t] but
       raises [Invalid_argument s] when [find k t] raises [Not_found] *)

  val iter : (key -> 'a -> unit) -> 'a t -> unit
  val map : (key -> 'a -> key * 'a) -> 'a t -> 'a t
  val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
  val copy : 'a t -> 'a t
end

module type TBL_BUILDER = functor(X: COMPARABLE) -> HM with type key = X.t

(** [HM] implementation using hashtbl. *)
module Make_Hashtbl(X: COMPARABLE) = struct

  include Hashtbl.Make(X)

  type 'a return = unit
  let empty = ()
    (* never call and not visible for the user thank's to signature 
       constraints *)

  let create_from h = create (length h)

  let is_empty h = (length h = 0)

  let find_and_raise k h s = try find h k with Not_found -> invalid_arg s

  let map f h = 
    let h' = create_from h  in
    iter (fun k v -> let k, v = f k v in add h' k v) h;
    h'

  let add k v h = replace h k v; h
  let remove k h = remove h k; h
  let mem k h = mem h k
  let find k h = find h k

end

(** [HM] implementation using map *)
module Make_Map(X: COMPARABLE) = struct
  include Map.Make(X)
  type 'a return = 'a t
  let is_empty m = (m = empty)
  let create _ = assert false
    (* never call and not visible for the user thank's to 
       signature constraints *)
  let create_from _ = empty
  let copy m = m
  let map f m = fold (fun k v m -> let k, v = f k v in add k v m) m empty
  let find_and_raise k h s = try find k h with Not_found -> invalid_arg s
end

(* ************************************************************************* *)
(** {2 Blocks builder} *)
(* ************************************************************************* *)

(** Common implementation to all (directed) graph implementations. *)
module Minimal(S: Set.S)(HM: HM) = struct

  type vertex = HM.key

  let is_directed = true
  let empty = HM.empty
  let create = HM.create
  let is_empty = HM.is_empty

  let nb_vertex g = HM.fold (fun _ _ -> succ) g 0
  let nb_edges g = HM.fold (fun _ s n -> n + S.cardinal s) g 0
  let out_degree g v = 
    S.cardinal (try HM.find v g with Not_found -> invalid_arg "out_degree")

  let mem_vertex g v = HM.mem v g

  let unsafe_add_vertex g v = HM.add v S.empty g
  let unsafe_add_edge g v1 v2 = HM.add v1 (S.add v2 (HM.find v1 g)) g

  let add_vertex g v = if HM.mem v g then g else unsafe_add_vertex g v

  let iter_vertex f = HM.iter (fun v _ -> f v)
  let fold_vertex f = HM.fold (fun v _ -> f v)
    
end

(** All the predecessor operations from the iterators on the edges *)
module Pred(S: sig
	      module PV: COMPARABLE
	      module PE: EDGE with type vertex = PV.t
	      type t
	      val mem_vertex : PV.t -> t -> bool
	      val iter_edges : (PV.t -> PV.t -> unit) -> t -> unit
	      val fold_edges : (PV.t -> PV.t -> 'a -> 'a) -> t -> 'a -> 'a
	      val iter_edges_e : (PE.t -> unit) -> t -> unit
	      val fold_edges_e : (PE.t -> 'a -> 'a) -> t -> 'a -> 'a
	    end) =
struct

  open S

  let iter_pred f g v = 
    if not (mem_vertex v g) then invalid_arg "iter_pred";
    iter_edges (fun v1 v2 -> if PV.equal v v2 then f v1) g

  let fold_pred f g v = 
    if not (mem_vertex v g) then invalid_arg "fold_pred";
    fold_edges (fun v1 v2 a -> if PV.equal v v2 then f v1 a else a) g

  let pred g v = fold_pred (fun v l -> v :: l) g v []

  let in_degree g v = 
    if not (mem_vertex v g) then invalid_arg "in_degree";
    fold_pred (fun v n -> n + 1) g v 0

  let iter_pred_e f g v =
    if not (mem_vertex v g) then invalid_arg "iter_pred_e";
    iter_edges_e (fun e -> if PV.equal v (PE.dst e) then f e) g

  let fold_pred_e f g v =
    if not (mem_vertex v g) then invalid_arg "fold_pred_e";
    fold_edges_e (fun e a -> if PV.equal v (PE.dst e) then f e a else a) g
      
  let pred_e g v = fold_pred_e (fun v l -> v :: l) g v []

end

(** Common implementation to all the unlabeled (directed) graphs. *)
module Unlabeled(V: COMPARABLE)(HM: HM with type key = V.t) = struct
  
  module S = Set.Make(V)

  module E = struct
    type vertex = V.t
    include OTProduct(V)(V)
    let src = fst
    let dst = snd
    type label = unit
    let label _ = ()
    let create v1 () v2 = v1, v2
  end

  type edge = E.t

  let mem_edge g v1 v2 = 
    try
      S.mem v2 (HM.find v1 g)
    with Not_found ->
      false

  let mem_edge_e g (v1, v2) = mem_edge g v1 v2

  let find_edge g v1 v2 = if mem_edge g v1 v2 then v1, v2 else raise Not_found

  let unsafe_remove_edge g v1 v2 = HM.add v1 (S.remove v2 (HM.find v1 g)) g
  let unsafe_remove_edge_e g (v1, v2) = unsafe_remove_edge g v1 v2

  let remove_edge g v1 v2 = 
    if not (HM.mem v2 g) then invalid_arg "remove_edge";
    HM.add v1 (S.remove v2 (HM.find_and_raise v1 g "remove_edge")) g

  let remove_edge_e g (v1, v2) = remove_edge g v1 v2

  let iter_succ f g v = S.iter f (HM.find_and_raise v g "iter_succ")
  let fold_succ f g v = S.fold f (HM.find_and_raise v g "fold_succ")

  let iter_succ_e f g v = iter_succ (fun v2 -> f (v, v2)) g v
  let fold_succ_e f g v = fold_succ (fun v2 -> f (v, v2)) g v

  let succ g v = S.elements (HM.find_and_raise v g "succ")
  let succ_e g v = fold_succ_e (fun e l -> e :: l) g v []

  let map_vertex f = 
    HM.map (fun v s -> f v, S.fold (fun v s -> S.add (f v) s) s S.empty)

  module I = struct
    type t = S.t HM.t
    module PV = V
    module PE = E
    let iter_edges f = HM.iter (fun v -> S.iter (f v))
    let fold_edges f = HM.fold (fun v -> S.fold (f v))
    let iter_edges_e f = iter_edges (fun v1 v2 -> f (v1, v2))
    let fold_edges_e f = fold_edges (fun v1 v2 a -> f (v1, v2) a)
  end
  include I

  include Pred(struct include I let mem_vertex = HM.mem end)

end

(** Common implementation to all the labeled (directed) graphs. *)
module Labeled(V: COMPARABLE)(E: ORDERED_TYPE)(HM: HM with type key = V.t) = 
struct

  module VE = OTProduct(V)(E)

  module S = Set.Make(VE)

  module E = struct
    type vertex = V.t
    type label = E.t
    type t = vertex * label * vertex
    let src (v, _, _) = v
    let dst (_, _, v) = v
    let label (_, l, _) = l
    let create v1 l v2 = v1, l, v2
    module C = OTProduct(V)(VE)
    let compare (x1, x2, x3) (y1, y2, y3) = 
      C.compare (x1, (x3, x2)) (y1, (y3, y2))
  end

  type edge = E.t

  let mem_edge g v1 v2 = 
    try
      S.exists (fun (v2', _) -> V.equal v2 v2') (HM.find v1 g)
    with Not_found ->
      false

  let mem_edge_e g (v1, l, v2) =
    try
      let ve = v2, l in
      S.exists (fun ve' -> VE.compare ve ve' == 0) (HM.find v1 g)
    with Not_found ->
      false

  exception Found of edge
  let find_edge g v1 v2 =
    try
      S.iter 
	(fun (v2', l) -> if V.equal v2 v2' then raise (Found (v1, l, v2')))
	(HM.find v1 g);
      raise Not_found
    with Found e ->
      e

  let unsafe_remove_edge g v1 v2 = 
    HM.add v1 (S.filter 
		 (fun (v2', _) -> not (V.equal v2 v2')) (HM.find v1 g)) g

  let unsafe_remove_edge_e g (v1, l, v2) = 
    HM.add v1 (S.remove (v2, l) (HM.find v1 g)) g

  let remove_edge g v1 v2 =
    if not (HM.mem v2 g) then invalid_arg "remove_edge";
    HM.add v1 (S.filter 
		 (fun (v2', _) -> not (V.equal v2 v2'))
		 (HM.find_and_raise v1 g "remove_edge")) g

  let remove_edge_e g (v1, l, v2) = 
    if not (HM.mem v2 g) then invalid_arg "remove_edge_e";
    HM.add v1 (S.remove (v2, l) (HM.find_and_raise v1 g "remove_edge_e")) g

  let iter_succ f g v = 
    S.iter (fun (w, _) -> f w) (HM.find_and_raise v g "iter_succ")
  let fold_succ f g v = 
    S.fold (fun (w, _) -> f w) (HM.find_and_raise v g "fold_succ")

  let iter_succ_e f g v = 
    S.iter (fun (w, l) -> f (v, l, w)) (HM.find_and_raise v g "iter_succ_e")
  let fold_succ_e f g v = 
    S.fold (fun (w, l) -> f (v, l, w)) (HM.find_and_raise v g "fold_succ_e")

  let succ g v = fold_succ (fun w l -> w :: l) g v []
  let succ_e g v = fold_succ_e (fun e l -> e :: l) g v []

  let map_vertex f = 
    HM.map (fun v s -> 
	      f v, S.fold (fun (v, l) s -> S.add (f v, l) s) s S.empty)

  module I = struct
    type t = S.t HM.t
    module PV = V
    module PE = E

    let iter_edges f = HM.iter (fun v -> S.iter (fun (w, _) -> f v w))
    let fold_edges f = HM.fold (fun v -> S.fold (fun (w, _) -> f v w))
    let iter_edges_e f = 
      HM.iter (fun v -> S.iter (fun (w, l) -> f (v, l, w)))
    let fold_edges_e f = 
      HM.fold (fun v -> S.fold (fun (w, l) -> f (v, l, w)))
  end
  include I

  include Pred(struct include I let mem_vertex = HM.mem end)

end

(** The vertex module and the vertex table for the concrete graphs. *)
module ConcreteVertex(F : TBL_BUILDER)(V: COMPARABLE) = struct

  module V = struct
    include V
    type label = t
    let label v = v
    let create v = v
  end

  module HM = F(V)

end

(* Support for explicitly maintaining edge set of
   predecessors.  Crucial for algorithms that do a lot of backwards
   traversal. *)

module BidirectionalMinimal(S:Set.S)(HM:HM with type key = S.elt) = 
struct

  type vertex = HM.key

  let is_directed = true
  let empty = HM.empty
  let create = HM.create
  let is_empty = HM.is_empty

  let nb_vertex g = HM.fold (fun _ _ -> succ) g 0
  let nb_edges g = HM.fold (fun _ (_,s) n -> n + S.cardinal s) g 0
  let out_degree g v = 
    S.cardinal (snd (try HM.find v g with Not_found -> invalid_arg "out_degree"))

  let mem_vertex g v = HM.mem v g

  let unsafe_add_vertex g v = HM.add v (S.empty,S.empty) g
  let unsafe_add_edge g v1 v2 = 
    let (in_set,out_set) = HM.find v1 g
    in 
      ignore ( HM.add v1 (in_set,S.add v2 out_set) g ) ;
      let (in_set,out_set) = HM.find v2 g
      in
	HM.add v2 (S.add v1 in_set,out_set) g

  let iter_vertex f = HM.iter (fun v _ -> f v)
  let fold_vertex f = HM.fold (fun v _ -> f v)
end

module BidirectionalUnlabeled(V:COMPARABLE)(HM:HM with type key = V.t) =
struct

  module S = Set.Make(V)

  (* Edge definition *)

  module E = struct
    type vertex = V.t
    include OTProduct(V)(V)
    let src = fst
    let dst = snd
    type label = unit
    let label _ = ()
    let create v1 () v2 = v1, v2
  end

  type edge = E.t

  let mem_edge g v1 v2 =
    try S.mem v2 (snd (HM.find v1 g))
    with Not_found -> false

  let mem_edge_e g (v1,v2) = mem_edge g v1 v2

  let find_edge g v1 v2 = if mem_edge g v1 v2 then v1, v2 else raise Not_found

  let unsafe_remove_edge g v1 v2 =
    let (in_set,out_set) = HM.find v1 g in 
    ignore ( HM.add v1 (in_set,( S.remove v2 out_set )) g ) ;
    let (in_set,out_set) = HM.find v2 g in
    HM.add v2 (S.remove v1 in_set,out_set) g

  let unsafe_remove_edge_e g (v1,v2) = unsafe_remove_edge g v1 v2

  let remove_edge g v1 v2 = 
    if not (HM.mem v2 g) then invalid_arg "remove_edge";
    unsafe_remove_edge g v1 v2
    (* HM.add v1 (S.remove v2 (HM.find_and_raise v1 g "remove_edge")) g *)

  let remove_edge_e g (v1, v2) = remove_edge g v1 v2

  let iter_succ f g v = S.iter f (snd (HM.find_and_raise v g "iter_succ"))
  let fold_succ f g v = S.fold f (snd (HM.find_and_raise v g "fold_succ"))

  let iter_succ_e f g v = iter_succ (fun v2 -> f (v, v2)) g v
  let fold_succ_e f g v = fold_succ (fun v2 -> f (v, v2)) g v

  let succ g v = S.elements (snd (HM.find_and_raise v g "succ"))
  let succ_e g v = fold_succ_e (fun e l -> e :: l) g v []
 
  let map_vertex f = 
    HM.map (fun v (s1,s2) -> 
	      f v, 
	      ( S.fold (fun v s -> S.add (f v) s) s1 S.empty,
		S.fold (fun v s -> S.add (f v) s) s2 S.empty ) 
	   )

  module I = struct
    (* we keep sets for both incoming and outgoing edges *)
    type t = (S.t * S.t) HM.t  
    module PV = V
    module PE = E
    let iter_edges f = HM.iter (fun v (_,outset) -> S.iter (f v) outset )
    let fold_edges f = HM.fold (fun v (_,outset) -> S.fold (f v) outset )
    let iter_edges_e f = iter_edges (fun v1 v2 -> f (v1, v2))
    let fold_edges_e f = fold_edges (fun v1 v2 a -> f (v1, v2) a)
  end
  include I

  let iter_pred f g v = S.iter f (fst (HM.find_and_raise v g "iter_pred"))
  let fold_pred f g v = S.fold f (fst (HM.find_and_raise v g "fold_pred"))

  let pred g v = S.elements (fst (HM.find_and_raise v g "pred"))

  let in_degree g v = 
    S.cardinal 
      (fst (try HM.find v g with Not_found -> invalid_arg "in_degree"))

  let iter_pred_e f g v = iter_pred (fun v2 -> f (v2,v)) g v
  let fold_pred_e f g v = fold_pred (fun v2 -> f (v2,v)) g v

  let pred_e g v = fold_pred_e (fun e l -> e :: l) g v []   
end

module Make_Abstract
  (G: sig
     module HM: HM
     module S: Set.S
     include G with type t = S.t HM.t and type V.t = HM.key
     val remove_edge: t -> vertex -> vertex -> t
     val remove_edge_e: t -> edge -> t
     val unsafe_add_vertex: t -> vertex -> t
     val unsafe_add_edge: t -> vertex -> S.elt -> t
     val unsafe_remove_edge: t -> vertex -> vertex -> t
     val unsafe_remove_edge_e: t -> edge -> t
     val empty: S.t HM.return
     val create: int -> t
   end) = 
struct

  module I = struct
    type t = { edges : G.t; mutable size : int }
	(* BE CAREFUL: [size] is only mutable in the imperative version.
	   As there is no extensible records in current ocaml version,
	   and for genericity purpose, [size] is mutable in both the
	   imperative and persistent implementation.
	   Do not modify size in the persistent implementation! *)

    type vertex = G.vertex
    type edge = G.edge

    module PV = G.V
    module PE = G.E

    let iter_edges f g = G.iter_edges f g.edges
    let fold_edges f g = G.fold_edges f g.edges
    let iter_edges_e f g = G.iter_edges_e f g.edges
    let fold_edges_e f g = G.fold_edges_e f g.edges
    let mem_vertex v g = G.mem_vertex g.edges v
  end
  include I

  include Pred(I)

  (* optimisations *)

  let is_empty g = g.size = 0
  let nb_vertex g = g.size

  (* redefinitions *)
  module V = G.V
  module E = G.E
  module HM = G.HM
  module S = G.S

  let unsafe_add_edge = G.unsafe_add_edge
  let unsafe_remove_edge = G.unsafe_remove_edge
  let unsafe_remove_edge_e = G.unsafe_remove_edge_e
  let is_directed = G.is_directed

  let remove_edge g = G.remove_edge g.edges
  let remove_edge_e g = G.remove_edge_e g.edges

  let out_degree g = G.out_degree g.edges
  let in_degree g = G.in_degree g.edges

  let nb_edges g = G.nb_edges g.edges
  let succ g = G.succ g.edges
  let mem_vertex g = G.mem_vertex g.edges
  let mem_edge g = G.mem_edge g.edges
  let mem_edge_e g = G.mem_edge_e g.edges
  let find_edge g = G.find_edge g.edges

  let iter_vertex f g = G.iter_vertex f g.edges
  let fold_vertex f g = G.fold_vertex f g.edges
  let iter_succ f g = G.iter_succ f g.edges
  let fold_succ f g = G.fold_succ f g.edges
  let succ_e g = G.succ_e g.edges
  let iter_succ_e f g = G.iter_succ_e f g.edges
  let fold_succ_e f g = G.fold_succ_e f g.edges
  let map_vertex f g = { g with edges = G.map_vertex f g.edges }

end

(** Build persistent (resp. imperative) graphs from a persistent (resp. 
    imperative) association table *)
module Make(F : TBL_BUILDER) = struct

  module Digraph = struct

    module Concrete(V: COMPARABLE) = struct
      include ConcreteVertex(F)(V)
      include Unlabeled(V)(HM)
      include Minimal(S)(HM)

      let add_edge g v1 v2 = 
	let g = add_vertex g v1 in
	let g = add_vertex g v2 in
	unsafe_add_edge g v1 v2

      let add_edge_e g (v1, v2) = add_edge g v1 v2

      let remove_vertex g v =
	if HM.mem v g then
	  let g = HM.remove v g in
	  HM.fold 
	    (fun k s g -> HM.add k (S.remove v s) g) 
	    g 
	    (HM.create_from g)
	else
	  g

    end

    module ConcreteBidirectional(V: COMPARABLE) = struct
      include ConcreteVertex(F)(V)
      include BidirectionalUnlabeled(V)(HM)
      include BidirectionalMinimal(S)(HM)
    end

    module ConcreteLabeled(V: COMPARABLE)(E: ORDERED_TYPE_DFT) = struct
      include ConcreteVertex(F)(V)
      include Labeled(V)(E)(HM)
      include Minimal(S)(HM)
    end

    module Abstract(V: VERTEX) = struct
      module G = struct
	module V = V
	module HM = F(V)
	include Unlabeled(V)(HM) 
	include Minimal(S)(HM)
      end
      include Make_Abstract(G)
    end

    module AbstractLabeled(V: VERTEX)(E: ORDERED_TYPE_DFT) = struct
      module G = struct
	module V = V
	module HM = F(V)
	include Labeled(V)(E)(HM) 
	include Minimal(S)(HM)
      end
      include Make_Abstract(G)
    end

  end

end

(** Implementation of undirected graphs from implementation of directed
    graphs. *)
module Graph(G: Sig.G) = struct

  include G

  let is_directed = false

  (* Redefine iterators and [nb_edges]. *)

  let iter_edges f =
    iter_edges (fun v1 v2 -> if V.compare v1 v2 >= 0 then f v1 v2)

  let fold_edges f =
    fold_edges 
      (fun v1 v2 acc -> if V.compare v1 v2 >= 0 then f v1 v2 acc else acc)

  let iter_edges_e f =
    iter_edges_e
      (fun e -> if V.compare (E.src e) (E.dst e) >= 0 then f e)

  let fold_edges_e f =
    fold_edges_e
      (fun e acc -> 
	 if V.compare (E.src e) (E.dst e) >= 0 then f e acc else acc)

  let nb_edges g = fold_edges_e (fun _ -> (+) 1) g 0

  (* Redefine operations on predecessors:
     predecessors are successors in an undirected graph. *)

  let pred = succ
  let in_degree = out_degree
  let iter_pred = iter_succ
  let fold_pred = fold_succ
  let pred_e = succ_e
  let iter_pred_e = iter_succ_e
  let fold_pred_e = fold_succ_e

end