Mercurial > urweb

comparison src/disjoint.sml @ 82:b4f2a258e52c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial disjointness prover
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 10:55:38 -0400
parents
children 0a1baddd8ab2
comparison
equal deleted inserted replaced
81:60d97de1bbe8 82:b4f2a258e52c
1 (* Copyright (c) 2008, Adam Chlipala
2 * All rights reserved.
3 *
4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met:
6 *
7 * - Redistributions of source code must retain the above copyright notice,
8 * this list of conditions and the following disclaimer.
9 * - Redistributions in binary form must reproduce the above copyright notice,
10 * this list of conditions and the following disclaimer in the documentation
11 * and/or other materials provided with the distribution.
12 * - The names of contributors may not be used to endorse or promote products
13 * derived from this software without specific prior written permission.
14 *
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25 * POSSIBILITY OF SUCH DAMAGE.
26 *)
27
28 structure Disjoint :> DISJOINT = struct
29
30 open Elab
31 open ElabOps
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 =
91 NameC of string
92 | NameR of int
93 | NameN of int
94 | RowR of int
95 | RowN of int
96 | Unknown
97
98 fun nameToRow (c, loc) =
99 (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc)
100
101 fun pieceToRow (p, loc) =
102 case p of
103 NameC s => nameToRow (CName s, loc)
104 | NameR n => nameToRow (CRel n, loc)
105 | NameN n => nameToRow (CNamed n, loc)
106 | RowR n => (CRel n, loc)
107 | RowN n => (CRel n, loc)
108 | Unknown => raise Fail "Unknown to row"
109
110 fun decomposeRow env c =
111 let
112 fun decomposeName (c, acc) =
113 case #1 (hnormCon env c) of
114 CName s => NameC s :: acc
115 | CRel n => NameR n :: acc
116 | CNamed n => NameN n :: acc
117 | _ => Unknown :: acc
118
119 fun decomposeRow (c, acc) =
120 case #1 (hnormCon env c) of
121 CRecord (_, xcs) => foldl (fn ((x, _), acc) => decomposeName (x, acc)) acc xcs
122 | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc))
123 | CRel n => RowR n :: acc
124 | CNamed n => RowN n :: acc
125 | _ => Unknown :: acc
126 in
127 decomposeRow (c, [])
128 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
215 fun assert env denv (c1, c2) =
216 let
217 val ps1 = decomposeRow env c1
218 val ps2 = decomposeRow env c2
219
220 val denv = foldl (assertPiece ps2) denv ps1
221 in
222 foldl (assertPiece ps1) denv ps2
223 end
224
225 fun nameEnter {namesC, namesR, namesN} =
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
245 Unknown => raise Fail "getIneqs: Unknown"
246 | NameC _ => raise Fail "getIneqs: NameC"
247 | NameR n => nameToRow_ineqs (Option.getOpt (IM.find (#namesR denv, n), name_default))
248 | NameN n => nameToRow_ineqs (Option.getOpt (IM.find (#namesN denv, n), name_default))
249 | RowR n => Option.getOpt (IM.find (#rowsR denv, n), row_default)
250 | RowN n => Option.getOpt (IM.find (#rowsN denv, n), row_default)
251
252 fun prove1' denv (p1, p2) =
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
265 fun prove1 denv (p1, p2) =
266 case (p1, p2) of
267 (NameC s1, NameC s2) => s1 <> s2
268 | (_, RowR _) => prove1' denv (p2, p1)
269 | (_, RowN _) => prove1' denv (p2, p1)
270 | _ => prove1' denv (p1, p2)
271
272 fun prove env denv (c1, c2, loc) =
273 let
274 val ps1 = decomposeRow env c1
275 val ps2 = decomposeRow env c2
276
277 val hasUnknown = List.exists (fn p => p = Unknown)
278 in
279 if hasUnknown ps1 orelse hasUnknown ps2 then
280 (ErrorMsg.errorAt loc "Structure of row is too complicated to prove disjointness";
281 Print.eprefaces' [("Row 1", ElabPrint.p_con env c1),
282 ("Row 2", ElabPrint.p_con env c2)];
283 [])
284 else
285 foldl (fn (p1, rem) =>
286 foldl (fn (p2, rem) =>
287 if prove1 denv (p1, p2) then
288 rem
289 else
290 (pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2)
291 [] ps1
292 end
293
294 end