lib/mlton/directed-graph/shortest-path-check.fun

   1 (* Copyright (C) 1999-2006 Henry Cejtin, Matthew Fluet, Suresh
   2  *    Jagannathan, and Stephen Weeks.
   3  *
   4  * MLton is released under a BSD-style license.
   5  * See the file MLton-LICENSE for details.
   6  *)
   7
   8 functor ShortestPathCheck (S: SHORTEST_PATH_CHECK_STRUCTS): SHORTEST_PATH_CHECK =
   9 struct
  10
  11 open S
  12
  13 structure Answer =
  14    struct
  15       datatype t =
  16          Shortest
  17        | SourceNonZero
  18        | PredecessorReachable of Node.t * Edge.t
  19        | Relaxable of Node.t * Edge.t
  20        | NoPath of Node.t
  21
  22       fun layout (a, layoutNode) =
  23          let open Layout
  24          in case a of
  25             Shortest =>
  26                str "The distances are correct shortest path distances."
  27           | SourceNonZero => str "The distance to the source must be zero."
  28           | PredecessorReachable (n, e) =>
  29                let val n = Node.layout n
  30                   val n' = Node.layout (Edge.to e)
  31                in align
  32                   [str "The distances are contradictory.",
  33                    seq [str "1. There is an edge from ", n, str " to ", n'],
  34                    seq [str "2. ", n, str " has a finite distancEdge."],
  35                    seq [str "3. ", n', str " has an infinite distancEdge."]]
  36                end
  37           | NoPath n =>
  38                seq [str "There is not a valid predecessor path from ",
  39                    layoutNode n, str " to the sourcEdge."]
  40           | Relaxable (n, e) =>
  41                let val n = layoutNode n
  42                   val n' = layoutNode (Edge.to e)
  43                in align
  44                   [str "The distances are not shortest path distances.",
  45                    seq [str "The edge from ", n, str " to ", n',
  46                        str " can be relaxed."]]
  47                end
  48          end
  49    end
  50
  51 structure Set = DisjointSet
  52
  53 fun check {graph, source, weight, distance} =
  54    case distance source of
  55       NONE => Answer.SourceNonZero
  56     | SOME d =>
  57           if not (Weight.equals (Weight.zero, d))
  58              then Answer.SourceNonZero
  59           else
  60              let
  61                 exception Answer of Answer.t
  62                 val {get = set, destroy, ...} =
  63                    Property.destGet (Node.plist,
  64                                      Property.initFun (fn _ => Set.singleton ()))
  65                 fun union (n, n') = Set.union (set n, set n')
  66                 fun checkRelax (n, e) =
  67                    let val n' = Edge.to e
  68                    in case distance n of
  69                       NONE => ()
  70                     | SOME d =>
  71                          case distance n' of
  72                             NONE =>
  73                                raise Answer (Answer.PredecessorReachable (n, e))
  74                           | SOME d' =>
  75                                let val d'' = Weight.+ (d, weight e)
  76                                in if Weight.< (d'', d')
  77                                      then raise Answer (Answer.Relaxable (n, e))
  78                                   else if Weight.equals (d', d'')
  79                                           then union (n, n')
  80                                        else ()
  81                                end
  82                    end
  83                 val _ = foreachEdge (graph, checkRelax)
  84                 val sourceSet = set source
  85                 fun canReachSource n =
  86                    let val equiv = Set.equals (set n, sourceSet)
  87                    in case distance n of
  88                       NONE => ()
  89                     | SOME _ => if equiv
  90                                    then ()
  91                                 else raise Answer (Answer.NoPath n)
  92                    end
  93              in (foreachNode (graph, canReachSource)
  94                  ; Answer.Shortest) handle Answer a => a
  95              end
  96
  97 end