Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | (* Copyright (C) 1999-2007 Henry Cejtin, Matthew Fluet, Suresh |
2 | * Jagannathan, and Stephen Weeks. | |
3 | * Copyright (C) 1997-2000 NEC Research Institute. | |
4 | * | |
5 | * MLton is released under a BSD-style license. | |
6 | * See the file MLton-LICENSE for details. | |
7 | *) | |
8 | ||
9 | functor FlatLattice (S: FLAT_LATTICE_STRUCTS): FLAT_LATTICE = | |
10 | struct | |
11 | ||
12 | open S | |
13 | ||
14 | structure Elt = | |
15 | struct | |
16 | datatype t = | |
17 | Bottom | |
18 | | Point of Point.t | |
19 | | Top | |
20 | ||
21 | local | |
22 | open Layout | |
23 | in | |
24 | val layout = | |
25 | fn Bottom => str "Bottom" | |
26 | | Point p => Point.layout p | |
27 | | Top => str "Top" | |
28 | end | |
29 | end | |
30 | datatype z = datatype Elt.t | |
31 | ||
32 | datatype t = T of {lessThan: t list ref, | |
33 | upperBound: Point.t option ref, | |
34 | value: Elt.t ref} | |
35 | ||
36 | fun layout (T {value, ...}) = Elt.layout (!value) | |
37 | ||
38 | fun new () = T {lessThan = ref [], | |
39 | upperBound = ref NONE, | |
40 | value = ref Bottom} | |
41 | ||
42 | val isBottom = | |
43 | fn (T {value = ref Bottom, ...}) => true | |
44 | | _ => false | |
45 | val isPoint = | |
46 | fn (T {value = ref (Point _), ...}) => true | |
47 | | _ => false | |
48 | val isPointEq = | |
49 | fn (T {value = ref (Point p), ...}, p') => Point.equals (p, p') | |
50 | | _ => false | |
51 | val getPoint = | |
52 | fn (T {value = ref (Point p), ...}) => SOME p | |
53 | | _ => NONE | |
54 | val isTop = | |
55 | fn (T {value = ref Top, ...}) => true | |
56 | | _ => false | |
57 | ||
58 | fun forceTop (T {upperBound, value, ...}): bool = | |
59 | if isSome (!upperBound) | |
60 | then false | |
61 | else (value := Top; true) | |
62 | ||
63 | fun up (T {lessThan, upperBound, value, ...}, e: Elt.t): bool = | |
64 | let | |
65 | fun continue e = List.forall (!lessThan, fn z => up (z, e)) | |
66 | fun setTop () = | |
67 | not (isSome (!upperBound)) | |
68 | andalso (value := Top | |
69 | ; continue Top) | |
70 | in | |
71 | case (!value, e) of | |
72 | (_, Bottom) => true | |
73 | | (Top, _) => true | |
74 | | (_, Top) => setTop () | |
75 | | (Bottom, Point p) => | |
76 | (value := Point p | |
77 | ; (case !upperBound of | |
78 | NONE => continue (Point p) | |
79 | | SOME p' => | |
80 | Point.equals (p, p') andalso continue (Point p))) | |
81 | | (Point p, Point p') => Point.equals (p, p') orelse setTop () | |
82 | end | |
83 | ||
84 | val op <= : t * t -> bool = | |
85 | fn (T {lessThan, value, ...}, e) => | |
86 | (List.push (lessThan, e) | |
87 | ; up (e, !value)) | |
88 | ||
89 | val op <= = | |
90 | Trace.trace2 ("FlatLattice.<=", layout, layout, Bool.layout) | |
91 | (op <=) | |
92 | ||
93 | fun lowerBound (e, p): bool = up (e, Point p) | |
94 | ||
95 | val lowerBound = | |
96 | Trace.trace2 ("FlatLattice.lowerBound", layout, Point.layout, Bool.layout) | |
97 | lowerBound | |
98 | ||
99 | fun upperBound (T {upperBound = r, value, ...}, p): bool = | |
100 | case !r of | |
101 | NONE => (r := SOME p | |
102 | ; (case !value of | |
103 | Bottom => true | |
104 | | Point p' => Point.equals (p, p') | |
105 | | Top => false)) | |
106 | | SOME p' => Point.equals (p, p') | |
107 | ||
108 | val upperBound = | |
109 | Trace.trace2 ("FlatLattice.upperBound", layout, Point.layout, Bool.layout) | |
110 | upperBound | |
111 | ||
112 | fun forcePoint (e, p) = | |
113 | lowerBound (e, p) andalso upperBound (e, p) | |
114 | ||
115 | val forcePoint = | |
116 | Trace.trace2 ("FlatLattice.forcePoint", layout, Point.layout, Bool.layout) | |
117 | forcePoint | |
118 | ||
119 | fun point p = | |
120 | let | |
121 | val e = new () | |
122 | val _ = forcePoint (e, p) | |
123 | in | |
124 | e | |
125 | end | |
126 | ||
127 | val point = Trace.trace ("FlatLattice.point", Point.layout, layout) point | |
128 | ||
129 | end |