| 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 |