Mercurial > urweb

comparison src/disjoint.sml @ 88:7bab29834cd6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Constraints in modules
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 15:58:02 -0400
parents e86370850c30
children 94ef20a31550
comparison
equal deleted inserted replaced
87:275aaeb73f1f 88:7bab29834cd6
28 structure Disjoint :> DISJOINT = struct 28 structure Disjoint :> DISJOINT = struct
29 29
30 open Elab 30 open Elab
31 open ElabOps 31 open ElabOps
32 32
33 structure SS = BinarySetFn(struct
34 type ord_key = string
35 val compare = String.compare
36 end)
37
38 structure IS = IntBinarySet
39 structure IM = IntBinaryMap
40
41 type name_ineqs = {
42 namesC : SS.set,
43 namesR : IS.set,
44 namesN : IS.set
45 }
46
47 val name_default = {
48 namesC = SS.empty,
49 namesR = IS.empty,
50 namesN = IS.empty
51 }
52
53 type row_ineqs = {
54 namesC : SS.set,
55 namesR : IS.set,
56 namesN : IS.set,
57 rowsR : IS.set,
58 rowsN : IS.set
59 }
60
61 val row_default = {
62 namesC = SS.empty,
63 namesR = IS.empty,
64 namesN = IS.empty,
65 rowsR = IS.empty,
66 rowsN = IS.empty
67 }
68
69 fun nameToRow_ineqs {namesC, namesR, namesN} =
70 {namesC = namesC,
71 namesR = namesR,
72 namesN = namesN,
73 rowsR = IS.empty,
74 rowsN = IS.empty}
75
76 type env = {
77 namesR : name_ineqs IM.map,
78 namesN : name_ineqs IM.map,
79 rowsR : row_ineqs IM.map,
80 rowsN : row_ineqs IM.map
81 }
82
83 val empty = {
84 namesR = IM.empty,
85 namesN = IM.empty,
86 rowsR = IM.empty,
87 rowsN = IM.empty
88 }
89
90 datatype piece = 33 datatype piece =
91 NameC of string 34 NameC of string
92 | NameR of int 35 | NameR of int
93 | NameN of int 36 | NameN of int
37 | NameM of int * string list * string
94 | RowR of int 38 | RowR of int
95 | RowN of int 39 | RowN of int
96 | Unknown 40 | RowM of int * string list * string
41
42 fun p2s p =
43 case p of
44 NameC s => "NameC(" ^ s ^ ")"
45 | NameR n => "NameR(" ^ Int.toString n ^ ")"
46 | NameN n => "NameN(" ^ Int.toString n ^ ")"
47 | NameM (n, _, s) => "NameR(" ^ Int.toString n ^ ", " ^ s ^ ")"
48 | RowR n => "RowR(" ^ Int.toString n ^ ")"
49 | RowN n => "RowN(" ^ Int.toString n ^ ")"
50 | RowM (n, _, s) => "RowR(" ^ Int.toString n ^ ", " ^ s ^ ")"
51
52 fun pp p = print (p2s p ^ "\n")
53
54 structure PK = struct
55
56 type ord_key = piece
57
58 fun join (o1, o2) =
59 case o1 of
60 EQUAL => o2 ()
61 | v => v
62
63 fun joinL f (os1, os2) =
64 case (os1, os2) of
65 (nil, nil) => EQUAL
66 | (nil, _) => LESS
67 | (h1 :: t1, h2 :: t2) =>
68 join (f (h1, h2), fn () => joinL f (t1, t2))
69 | (_ :: _, nil) => GREATER
70
71 fun compare (p1, p2) =
72 case (p1, p2) of
73 (NameC s1, NameC s2) => String.compare (s1, s2)
74 | (NameR n1, NameR n2) => Int.compare (n1, n2)
75 | (NameN n1, NameN n2) => Int.compare (n1, n2)
76 | (NameM (n1, ss1, s1), NameM (n2, ss2, s2)) =>
77 join (Int.compare (n1, n2),
78 fn () => join (String.compare (s1, s2), fn () =>
79 joinL String.compare (ss1, ss2)))
80 | (RowR n1, RowR n2) => Int.compare (n1, n2)
81 | (RowN n1, RowN n2) => Int.compare (n1, n2)
82 | (RowM (n1, ss1, s1), RowM (n2, ss2, s2)) =>
83 join (Int.compare (n1, n2),
84 fn () => join (String.compare (s1, s2), fn () =>
85 joinL String.compare (ss1, ss2)))
86
87 | (NameC _, _) => LESS
88 | (_, NameC _) => GREATER
89
90 | (NameR _, _) => LESS
91 | (_, NameR _) => GREATER
92
93 | (NameN _, _) => LESS
94 | (_, NameN _) => GREATER
95
96 | (NameM _, _) => LESS
97 | (_, NameM _) => GREATER
98
99 | (RowR _, _) => LESS
100 | (_, RowR _) => GREATER
101
102 | (RowN _, _) => LESS
103 | (_, RowN _) => GREATER
104
105 end
106
107 structure PS = BinarySetFn(PK)
108 structure PM = BinaryMapFn(PK)
109
110 type env = PS.set PM.map
111
112 val empty = PM.empty
97 113
98 fun nameToRow (c, loc) = 114 fun nameToRow (c, loc) =
99 (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc) 115 (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc)
100 116
101 fun pieceToRow (p, loc) = 117 fun pieceToRow (p, loc) =
102 case p of 118 case p of
103 NameC s => nameToRow (CName s, loc) 119 NameC s => nameToRow (CName s, loc)
104 | NameR n => nameToRow (CRel n, loc) 120 | NameR n => nameToRow (CRel n, loc)
105 | NameN n => nameToRow (CNamed n, loc) 121 | NameN n => nameToRow (CNamed n, loc)
122 | NameM (n, xs, x) => nameToRow (CModProj (n, xs, x), loc)
106 | RowR n => (CRel n, loc) 123 | RowR n => (CRel n, loc)
107 | RowN n => (CRel n, loc) 124 | RowN n => (CNamed n, loc)
108 | Unknown => raise Fail "Unknown to row" 125 | RowM (n, xs, x) => (CModProj (n, xs, x), loc)
126
127 datatype piece' =
128 Piece of piece
129 | Unknown of con
109 130
110 fun decomposeRow env c = 131 fun decomposeRow env c =
111 let 132 let
112 fun decomposeName (c, acc) = 133 fun decomposeName (c, acc) =
113 case #1 (hnormCon env c) of 134 case #1 (hnormCon env c) of
114 CName s => NameC s :: acc 135 CName s => Piece (NameC s) :: acc
115 | CRel n => NameR n :: acc 136 | CRel n => Piece (NameR n) :: acc
116 | CNamed n => NameN n :: acc 137 | CNamed n => Piece (NameN n) :: acc
117 | _ => (print "Unknown name\n"; Unknown :: acc) 138 | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x)) :: acc
118 139 | _ => Unknown c :: acc
140
119 fun decomposeRow (c, acc) = 141 fun decomposeRow (c, acc) =
120 case #1 (hnormCon env c) of 142 case #1 (hnormCon env c) of
121 CRecord (_, xcs) => foldl (fn ((x, _), acc) => decomposeName (x, acc)) acc xcs 143 CRecord (_, xcs) => foldl (fn ((x, _), acc) => decomposeName (x, acc)) acc xcs
122 | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc)) 144 | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc))
123 | CRel n => RowR n :: acc 145 | CRel n => Piece (RowR n) :: acc
124 | CNamed n => RowN n :: acc 146 | CNamed n => Piece (RowN n) :: acc
125 | _ => (print "Unknown row\n"; Unknown :: acc) 147 | CModProj (m1, ms, x) => Piece (RowM (m1, ms, x)) :: acc
148 | _ => Unknown c :: acc
126 in 149 in
127 decomposeRow (c, []) 150 decomposeRow (c, [])
128 end 151 end
129
130 fun assertPiece_name (ps, ineqs : name_ineqs) =
131 {namesC = foldl (fn (p', namesC) =>
132 case p' of
133 NameC s => SS.add (namesC, s)
134 | _ => namesC) (#namesC ineqs) ps,
135 namesR = foldl (fn (p', namesR) =>
136 case p' of
137 NameR n => IS.add (namesR, n)
138 | _ => namesR) (#namesR ineqs) ps,
139 namesN = foldl (fn (p', namesN) =>
140 case p' of
141 NameN n => IS.add (namesN, n)
142 | _ => namesN) (#namesN ineqs) ps}
143
144 fun assertPiece_row (ps, ineqs : row_ineqs) =
145 {namesC = foldl (fn (p', namesC) =>
146 case p' of
147 NameC s => SS.add (namesC, s)
148 | _ => namesC) (#namesC ineqs) ps,
149 namesR = foldl (fn (p', namesR) =>
150 case p' of
151 NameR n => IS.add (namesR, n)
152 | _ => namesR) (#namesR ineqs) ps,
153 namesN = foldl (fn (p', namesN) =>
154 case p' of
155 NameN n => IS.add (namesN, n)
156 | _ => namesN) (#namesN ineqs) ps,
157 rowsR = foldl (fn (p', rowsR) =>
158 case p' of
159 RowR n => IS.add (rowsR, n)
160 | _ => rowsR) (#rowsR ineqs) ps,
161 rowsN = foldl (fn (p', rowsN) =>
162 case p' of
163 RowN n => IS.add (rowsN, n)
164 | _ => rowsN) (#rowsN ineqs) ps}
165
166 fun assertPiece ps (p, denv) =
167 case p of
168 Unknown => denv
169 | NameC _ => denv
170
171 | NameR n =>
172 let
173 val ineqs = Option.getOpt (IM.find (#namesR denv, n), name_default)
174 val ineqs = assertPiece_name (ps, ineqs)
175 in
176 {namesR = IM.insert (#namesR denv, n, ineqs),
177 namesN = #namesN denv,
178 rowsR = #rowsR denv,
179 rowsN = #rowsN denv}
180 end
181
182 | NameN n =>
183 let
184 val ineqs = Option.getOpt (IM.find (#namesN denv, n), name_default)
185 val ineqs = assertPiece_name (ps, ineqs)
186 in
187 {namesR = #namesR denv,
188 namesN = IM.insert (#namesN denv, n, ineqs),
189 rowsR = #rowsR denv,
190 rowsN = #rowsN denv}
191 end
192
193 | RowR n =>
194 let
195 val ineqs = Option.getOpt (IM.find (#rowsR denv, n), row_default)
196 val ineqs = assertPiece_row (ps, ineqs)
197 in
198 {namesR = #namesR denv,
199 namesN = #namesN denv,
200 rowsR = IM.insert (#rowsR denv, n, ineqs),
201 rowsN = #rowsN denv}
202 end
203
204 | RowN n =>
205 let
206 val ineqs = Option.getOpt (IM.find (#rowsN denv, n), row_default)
207 val ineqs = assertPiece_row (ps, ineqs)
208 in
209 {namesR = #namesR denv,
210 namesN = #namesN denv,
211 rowsR = #rowsR denv,
212 rowsN = IM.insert (#rowsN denv, n, ineqs)}
213 end
214 152
215 fun assert env denv (c1, c2) = 153 fun assert env denv (c1, c2) =
216 let 154 let
217 val ps1 = decomposeRow env c1 155 val ps1 = decomposeRow env c1
218 val ps2 = decomposeRow env c2 156 val ps2 = decomposeRow env c2
219 157
158 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
159 val ps1 = unUnknown ps1
160 val ps2 = unUnknown ps2
161
162 (*val () = print "APieces1:\n"
163 val () = app pp ps1
164 val () = print "APieces2:\n"
165 val () = app pp ps2*)
166
167 fun assertPiece ps (p, denv) =
168 let
169 val pset = Option.getOpt (PM.find (denv, p), PS.empty)
170 val pset = PS.addList (pset, ps)
171 in
172 PM.insert (denv, p, pset)
173 end
174
220 val denv = foldl (assertPiece ps2) denv ps1 175 val denv = foldl (assertPiece ps2) denv ps1
221 in 176 in
222 foldl (assertPiece ps1) denv ps2 177 foldl (assertPiece ps1) denv ps2
223 end 178 end
224 179
225 fun nameEnter {namesC, namesR, namesN} = 180 fun pieceEnter p =
226 {namesC = namesC,
227 namesR = IS.map (fn n => n + 1) namesR,
228 namesN = namesN}
229
230 fun rowEnter {namesC, namesR, namesN, rowsR, rowsN} =
231 {namesC = namesC,
232 namesR = IS.map (fn n => n + 1) namesR,
233 namesN = namesN,
234 rowsR = IS.map (fn n => n + 1) rowsR,
235 rowsN = rowsN}
236
237 fun enter {namesR, namesN, rowsR, rowsN} =
238 {namesR = IM.foldli (fn (n, ineqs, namesR) => IM.insert (namesR, n+1, nameEnter ineqs)) IM.empty namesR,
239 namesN = IM.map nameEnter namesN,
240 rowsR = IM.foldli (fn (n, ineqs, rowsR) => IM.insert (rowsR, n+1, rowEnter ineqs)) IM.empty rowsR,
241 rowsN = IM.map rowEnter rowsN}
242
243 fun getIneqs (denv : env) p =
244 case p of 181 case p of
245 Unknown => raise Fail "getIneqs: Unknown" 182 NameR n => NameR (n + 1)
246 | NameC _ => raise Fail "getIneqs: NameC" 183 | RowR n => RowR (n + 1)
247 | NameR n => nameToRow_ineqs (Option.getOpt (IM.find (#namesR denv, n), name_default)) 184 | _ => p
248 | NameN n => nameToRow_ineqs (Option.getOpt (IM.find (#namesN denv, n), name_default)) 185
249 | RowR n => Option.getOpt (IM.find (#rowsR denv, n), row_default) 186 fun enter denv =
250 | RowN n => Option.getOpt (IM.find (#rowsN denv, n), row_default) 187 PM.foldli (fn (p, pset, denv') =>
251 188 PM.insert (denv', pieceEnter p, PS.map pieceEnter pset))
252 fun prove1' denv (p1, p2) = 189 PM.empty denv
253 let
254 val {namesC, namesR, namesN, rowsR, rowsN} = getIneqs denv p1
255 in
256 case p2 of
257 Unknown => raise Fail "prove1': Unknown"
258 | NameC s => SS.member (namesC, s)
259 | NameR n => IS.member (namesR, n)
260 | NameN n => IS.member (namesN, n)
261 | RowR n => IS.member (rowsR, n)
262 | RowN n => IS.member (rowsN, n)
263 end
264 190
265 fun prove1 denv (p1, p2) = 191 fun prove1 denv (p1, p2) =
266 case (p1, p2) of 192 case (p1, p2) of
267 (NameC s1, NameC s2) => s1 <> s2 193 (NameC s1, NameC s2) => s1 <> s2
268 | (NameC _, _) => prove1' denv (p2, p1) 194 | _ =>
269 | (_, RowR _) => prove1' denv (p2, p1) 195 case PM.find (denv, p1) of
270 | (_, RowN _) => prove1' denv (p2, p1) 196 NONE => false
271 | _ => prove1' denv (p1, p2) 197 | SOME pset => PS.member (pset, p2)
272 198
273 fun prove env denv (c1, c2, loc) = 199 fun prove env denv (c1, c2, loc) =
274 let 200 let
275 val ps1 = decomposeRow env c1 201 val ps1 = decomposeRow env c1
276 val ps2 = decomposeRow env c2 202 val ps2 = decomposeRow env c2
277 203
278 val hasUnknown = List.exists (fn p => p = Unknown) 204 val hasUnknown = List.exists (fn Unknown _ => true | _ => false)
205 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
279 in 206 in
280 if hasUnknown ps1 orelse hasUnknown ps2 then 207 if hasUnknown ps1 orelse hasUnknown ps2 then
281 [(c1, c2)] 208 [(c1, c2)]
282 else 209 else
283 foldl (fn (p1, rem) => 210 let
284 foldl (fn (p2, rem) => 211 val ps1 = unUnknown ps1
285 if prove1 denv (p1, p2) then 212 val ps2 = unUnknown ps2
286 rem 213
287 else 214 in
288 (pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2) 215 (*print "Pieces1:\n";
289 [] ps1 216 app pp ps1;
217 print "Pieces2:\n";
218 app pp ps2;*)
219
220 foldl (fn (p1, rem) =>
221 foldl (fn (p2, rem) =>
222 if prove1 denv (p1, p2) then
223 rem
224 else
225 (pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2)
226 [] ps1
227 end
290 end 228 end
291 229
292 end 230 end