libmojave/stdlib/lm_imp_dag.ml

   1 (*
   2  * Imperative DAGS.  We implement the DAG as a vector.
   3  * Each entry in the vector contains the value for a node,
   4  * and all the outgoing edges, represented by their destination
   5  * index.
   6  *
   7  * This is a space-saving dag.  Only the real edges
   8  * and the quiried edges are actually saved.
   9  *
  10  * ----------------------------------------------------------------
  11  *
  12  * This file is part of MetaPRL, a modular, higher order
  13  * logical framework that provides a logical programming
  14  * environment for OCaml and other languages.
  15  *
  16  * See the file doc/htmlman/default.html or visit http://metaprl.org/
  17  * for more information.
  18  *
  19  * Copyright (C) 1998-2005 PRL Group, Cornell University and Caltech
  20  *
  21  * This library is free software; you can redistribute it and/or
  22  * modify it under the terms of the GNU Lesser General Public
  23  * License as published by the Free Software Foundation,
  24  * version 2.1 of the License.
  25  *
  26  * This library is distributed in the hope that it will be useful,
  27  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  28  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  29  * Lesser General Public License for more details.
  30  *
  31  * You should have received a copy of the GNU Lesser General Public
  32  * License along with this library; if not, write to the Free Software
  33  * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
  34  *
  35  * Additional permission is given to link this library with the
  36  * OpenSSL project's "OpenSSL" library, and with the OCaml runtime,
  37  * and you may distribute the linked executables.  See the file
  38  * LICENSE.libmojave for more details.
  39  *
  40  * Author: Jason Hickey
  41  * jyh@cs.cornell.edu
  42  *)
  43
  44 open Lm_debug
  45 open Lm_dag_sig
  46
  47 (*
  48  * Show the file loading.
  49  *)
  50 let _ =
  51    show_loading "Loading Imp_dag%t"
  52
  53 module ImpDag =
  54 struct
  55    (************************************************************************
  56     * TYPES                                                                *
  57     ************************************************************************)
  58
  59    (*
  60     * An entry in the vector contains some value, and the edges
  61     * in the graph.  When a query is made.
  62     *    1. if the version number
  63     *       is up-to-date, and the edge is in unrelated, then
  64     *       NoRelation is returned.  If the edge is in entry_out_edges,
  65     *       the LessThan is returned.  Else, a search is made, and a new edge
  66     *       either added to out_edges or unrelated.
  67     *    2. If the version number is out of date, then the
  68     *       unrelated edges are cleared.
  69     *
  70     * Invariant: edge lists are sorted
  71     *
  72     *)
  73    type 'a entry =
  74       { mutable entry_value : 'a;
  75         mutable entry_in_edges : int list;
  76         mutable entry_out_edges : int list;
  77         mutable entry_no_relation : int list;
  78         mutable entry_version : int
  79       }
  80
  81    (*
  82     * A DAG is a vector of entries.
  83     * We add a level of indirection to allow for equating nodes.
  84     *)
  85    type 'a t =
  86       { mutable entries : ('a entry) array;
  87         mutable version : int
  88       }
  89
  90    type 'a node = int
  91
  92    (************************************************************************
  93     * IMPLEMENTATION                                                       *
  94     ************************************************************************)
  95
  96    (*
  97     * Raw equality.
  98     *)
  99    let eq (node1 : 'a node) (node2 : 'a node) =
 100       node1 == node2
 101
 102    (*
 103     * Insert a value into a sorted list.
 104     *)
 105    let rec list_insert i l =
 106       match l with
 107          h :: t ->
 108             if h < i then
 109                h :: (list_insert i t)
 110             else if h > i then
 111                i :: l
 112             else
 113                l
 114        | [] ->
 115             [i]
 116
 117    (*
 118     * Remove a particular entry from the list, and
 119     * decrement all larger indices.
 120     *)
 121    let rec list_delete i = function
 122       h :: t ->
 123          if h < i then
 124             h :: list_delete i t
 125          else if h = i then
 126             list_delete i t
 127          else
 128             h - 1 :: list_delete i t
 129     | [] ->
 130          []
 131
 132    (*
 133     * Construct a new DAG.
 134     *)
 135    let create () =
 136       { entries = [||]; version = 0 }
 137
 138    (*
 139     * Add a new node unrelated to the rest of the DAG.
 140     *)
 141    let insert dag v =
 142       let { entries = entries; version = version } = dag in
 143       let length = Array.length entries in
 144       let entry =
 145          { entry_value = v;
 146            entry_in_edges = [];
 147            entry_out_edges = [];
 148            entry_no_relation = [];
 149            entry_version = version;
 150          }
 151       in
 152       let newentries = Array.create (length + 1) entry in
 153          Array.blit entries 0 newentries 0 length;
 154          dag.entries <- newentries;
 155          length
 156
 157    (*
 158     * Delete a node by updating all indices.
 159     *)
 160    let delete dag node =
 161       let { entries = entries; version = version } = dag in
 162       let length = Array.length entries in
 163       let newentries = Array.create (length - 1) entries.(0) in
 164       let delete entry =
 165          entry.entry_in_edges <- list_delete node entry.entry_in_edges;
 166          entry.entry_out_edges <- list_delete node entry.entry_out_edges
 167       in
 168          Array.blit entries 0 newentries 0 node;
 169          Array.blit entries (node + 1) newentries node (length - node - 1);
 170          Array.iter delete entries;
 171          dag.version <- version + 1
 172
 173    (*
 174     * Add an edge from node1 to node2.
 175     *)
 176    let add_edge dag node1 node2 =
 177       let { entries = entries; version = version } = dag in
 178       let entry1 = entries.(node1) in
 179       let entry2 = entries.(node2) in
 180          entry1.entry_out_edges <- list_insert node2 entry1.entry_out_edges;
 181          entry2.entry_in_edges <- list_insert node1 entry2.entry_in_edges;
 182          dag.version <- version + 1
 183
 184    (*
 185     * Two nodes are made equal by creating a cycle.
 186     *)
 187    let equate dag node1 node2 =
 188       add_edge dag node1 node2;
 189       add_edge dag node2 node1
 190
 191    (*
 192     * Projections.
 193     *)
 194    let node_value { entries = entries } i =
 195       entries.(i).entry_value
 196
 197    let node_out_edges { entries = entries } i =
 198       entries.(i).entry_out_edges
 199
 200    let node_in_edges { entries = entries } i =
 201       entries.(i).entry_in_edges
 202
 203    (*
 204     * Sweep a function up the DAG, calling on the children first.
 205     * The function is called only once on each node, so we keep a vector
 206     * of cached values.  The oproj and iproj are the projection
 207     * functions for entry.entry_out_edges and entry.entry_in_edges, or
 208     * vice versa.
 209     *)
 210    let sweep_aux entries f oproj iproj =
 211       let len = Array.length entries in
 212       let values = Array.create len None in
 213       let rec expand i =
 214          match values.(i) with
 215             None ->
 216                let entry = entries.(i) in
 217                let children = List.map expand (oproj entry) in
 218                let result = f entry.entry_value children in
 219                   values.(i) <- Some result;
 220                   result
 221
 222           | Some result ->
 223                result
 224       in
 225       let rec aux i =
 226          if i < len then
 227             let entry = entries.(i) in
 228             let result = expand i in
 229                if (iproj entry) = [] then
 230                   result::(aux (i + 1))
 231                else
 232                   aux (i + 1)
 233          else
 234             []
 235       in
 236          aux 0
 237
 238    let out_edges_f { entry_out_edges = edges } = edges
 239
 240    let in_edges_f { entry_in_edges = edges } = edges
 241
 242    let some_edges_f { entry_in_edges = _ } = []
 243
 244    let sweep_up { entries = entries } f =
 245       sweep_aux entries f out_edges_f in_edges_f
 246
 247    let sweep_down { entries = entries } f =
 248       sweep_aux entries f in_edges_f out_edges_f
 249
 250    let sweep_up_all { entries = entries } f =
 251       sweep_aux entries f out_edges_f some_edges_f
 252
 253    let sweep_down_all { entries = entries } f =
 254       sweep_aux entries f in_edges_f some_edges_f
 255
 256    (*
 257     * Get the roots of the DAG.
 258     * These nodes have no in_edges.
 259     *)
 260    let roots { entries = entries } =
 261       let length = Array.length entries in
 262       let rec collect i =
 263          if i = length then
 264             []
 265          else
 266             let entry = entries.(i) in
 267                if entry.entry_in_edges = [] then
 268                   i :: collect (i + 1)
 269                else
 270                   collect (i + 1)
 271       in
 272          collect 0
 273
 274    (*
 275     * Sort the list from the roots.
 276     *)
 277    let sort info =
 278       let entries = info.entries in
 279       let length = Array.length entries in
 280       let found = Array.create length false in
 281       let roots = roots info in
 282       let rec collect l i =
 283          if found.(i) then
 284             l
 285          else
 286             let entry = entries.(i) in
 287             let next = entry.entry_out_edges in
 288                found.(i) <- true;
 289                List.fold_left collect (i :: l) next
 290       in
 291          List.fold_left collect [] roots
 292
 293    (*
 294     * Expand to all the reachable nodes.
 295     *)
 296    let search select entries node1 node2 =
 297       let rec loop searched front =
 298          match front with
 299             node :: t ->
 300                if node = node2 then
 301                   true
 302                else if List.mem node searched then
 303                   loop searched t
 304                else
 305                   let edges = select entries.(node) in
 306                      loop (node :: searched) (Sort.merge (<) edges t)
 307           | [] ->
 308                false
 309       in
 310          loop [] [node1]
 311
 312    (*
 313     * Find the relation and cache it.
 314     * If version is out-of-date, delete the no_relation.
 315     * If edge is found, then return it, else search.
 316     *)
 317    let node_rel dag node1 node2 =
 318       let { entries = entries; version = version } = dag in
 319       let entry1 = entries.(node1) in
 320       let { entry_in_edges = in_edges;
 321             entry_out_edges = out_edges;
 322             entry_no_relation = no_relation;
 323             entry_version = version'
 324           } = entry1
 325       in
 326       let no_relation =
 327          if version' = version then
 328             no_relation
 329          else
 330             begin
 331                entry1.entry_no_relation <- [];
 332                entry1.entry_version <- version;
 333                []
 334             end
 335       in
 336          (* First check for cached edges *)
 337          if List.mem node2 no_relation then
 338             NoRelation
 339          else if List.mem node2 out_edges then
 340             if List.mem node2 in_edges then
 341                Equal
 342             else
 343                LessThan
 344          else if List.mem node2 in_edges then
 345             GreaterThan
 346
 347          (* If not in cache, then do a search *)
 348          else if search out_edges_f entries node1 node2 then
 349             if search in_edges_f entries node1 node2 then
 350                begin
 351                   entry1.entry_out_edges <- list_insert node2 out_edges;
 352                   entry1.entry_in_edges <- list_insert node2 in_edges;
 353                   Equal
 354                end
 355             else
 356                begin
 357                   entry1.entry_out_edges <- list_insert node2 out_edges;
 358                   LessThan
 359                end
 360          else if search in_edges_f entries node1 node2 then
 361             begin
 362                entry1.entry_in_edges <- list_insert node2 in_edges;
 363                GreaterThan
 364             end
 365          else
 366             begin
 367                entry1.entry_no_relation <- list_insert node2 no_relation;
 368                NoRelation
 369             end
 370 end
 371
 372 (*
 373  * -*-
 374  * Local Variables:
 375  * Caml-master: "editor.top"
 376  * End:
 377  * -*-
 378  *)