Commit | Line | Data |
---|---|---|
7f918cf1 CE |
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 |