adamc@82
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@82
|
2 * All rights reserved.
|
adamc@82
|
3 *
|
adamc@82
|
4 * Redistribution and use in source and binary forms, with or without
|
adamc@82
|
5 * modification, are permitted provided that the following conditions are met:
|
adamc@82
|
6 *
|
adamc@82
|
7 * - Redistributions of source code must retain the above copyright notice,
|
adamc@82
|
8 * this list of conditions and the following disclaimer.
|
adamc@82
|
9 * - Redistributions in binary form must reproduce the above copyright notice,
|
adamc@82
|
10 * this list of conditions and the following disclaimer in the documentation
|
adamc@82
|
11 * and/or other materials provided with the distribution.
|
adamc@82
|
12 * - The names of contributors may not be used to endorse or promote products
|
adamc@82
|
13 * derived from this software without specific prior written permission.
|
adamc@82
|
14 *
|
adamc@82
|
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
adamc@82
|
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
adamc@82
|
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
|
adamc@82
|
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
|
adamc@82
|
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
|
adamc@82
|
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
|
adamc@82
|
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
|
adamc@82
|
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
|
adamc@82
|
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
|
adamc@82
|
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
adamc@82
|
25 * POSSIBILITY OF SUCH DAMAGE.
|
adamc@82
|
26 *)
|
adamc@82
|
27
|
adamc@82
|
28 structure Disjoint :> DISJOINT = struct
|
adamc@82
|
29
|
adamc@82
|
30 open Elab
|
adamc@82
|
31 open ElabOps
|
adamc@82
|
32
|
adamc@207
|
33 datatype piece_fst =
|
adamc@82
|
34 NameC of string
|
adamc@82
|
35 | NameR of int
|
adamc@82
|
36 | NameN of int
|
adamc@88
|
37 | NameM of int * string list * string
|
adamc@82
|
38 | RowR of int
|
adamc@82
|
39 | RowN of int
|
adamc@88
|
40 | RowM of int * string list * string
|
adamc@88
|
41
|
adamc@207
|
42 type piece = piece_fst * int list
|
adamc@207
|
43
|
adamc@88
|
44 fun p2s p =
|
adamc@88
|
45 case p of
|
adamc@88
|
46 NameC s => "NameC(" ^ s ^ ")"
|
adamc@88
|
47 | NameR n => "NameR(" ^ Int.toString n ^ ")"
|
adamc@88
|
48 | NameN n => "NameN(" ^ Int.toString n ^ ")"
|
adamc@88
|
49 | NameM (n, _, s) => "NameR(" ^ Int.toString n ^ ", " ^ s ^ ")"
|
adamc@88
|
50 | RowR n => "RowR(" ^ Int.toString n ^ ")"
|
adamc@88
|
51 | RowN n => "RowN(" ^ Int.toString n ^ ")"
|
adamc@88
|
52 | RowM (n, _, s) => "RowR(" ^ Int.toString n ^ ", " ^ s ^ ")"
|
adamc@88
|
53
|
adamc@88
|
54 fun pp p = print (p2s p ^ "\n")
|
adamc@88
|
55
|
adamc@478
|
56 fun rp2s (p, ns) = String.concatWith " " (p2s p :: map Int.toString ns)
|
adamc@478
|
57
|
adamc@88
|
58 structure PK = struct
|
adamc@88
|
59
|
adamc@88
|
60 type ord_key = piece
|
adamc@88
|
61
|
adamc@207
|
62 open Order
|
adamc@88
|
63
|
adamc@207
|
64 fun compare' (p1, p2) =
|
adamc@88
|
65 case (p1, p2) of
|
adamc@88
|
66 (NameC s1, NameC s2) => String.compare (s1, s2)
|
adamc@88
|
67 | (NameR n1, NameR n2) => Int.compare (n1, n2)
|
adamc@88
|
68 | (NameN n1, NameN n2) => Int.compare (n1, n2)
|
adamc@88
|
69 | (NameM (n1, ss1, s1), NameM (n2, ss2, s2)) =>
|
adamc@88
|
70 join (Int.compare (n1, n2),
|
adamc@88
|
71 fn () => join (String.compare (s1, s2), fn () =>
|
adamc@88
|
72 joinL String.compare (ss1, ss2)))
|
adamc@88
|
73 | (RowR n1, RowR n2) => Int.compare (n1, n2)
|
adamc@88
|
74 | (RowN n1, RowN n2) => Int.compare (n1, n2)
|
adamc@88
|
75 | (RowM (n1, ss1, s1), RowM (n2, ss2, s2)) =>
|
adamc@88
|
76 join (Int.compare (n1, n2),
|
adamc@88
|
77 fn () => join (String.compare (s1, s2), fn () =>
|
adamc@88
|
78 joinL String.compare (ss1, ss2)))
|
adamc@88
|
79
|
adamc@88
|
80 | (NameC _, _) => LESS
|
adamc@88
|
81 | (_, NameC _) => GREATER
|
adamc@88
|
82
|
adamc@88
|
83 | (NameR _, _) => LESS
|
adamc@88
|
84 | (_, NameR _) => GREATER
|
adamc@88
|
85
|
adamc@88
|
86 | (NameN _, _) => LESS
|
adamc@88
|
87 | (_, NameN _) => GREATER
|
adamc@88
|
88
|
adamc@88
|
89 | (NameM _, _) => LESS
|
adamc@88
|
90 | (_, NameM _) => GREATER
|
adamc@88
|
91
|
adamc@88
|
92 | (RowR _, _) => LESS
|
adamc@88
|
93 | (_, RowR _) => GREATER
|
adamc@88
|
94
|
adamc@88
|
95 | (RowN _, _) => LESS
|
adamc@88
|
96 | (_, RowN _) => GREATER
|
adamc@88
|
97
|
adamc@207
|
98 fun compare ((p1, ns1), (p2, ns2)) =
|
adamc@207
|
99 join (compare' (p1, p2),
|
adamc@207
|
100 fn () => joinL Int.compare (ns1, ns2))
|
adamc@207
|
101
|
adamc@88
|
102 end
|
adamc@88
|
103
|
adamc@88
|
104 structure PS = BinarySetFn(PK)
|
adamc@88
|
105 structure PM = BinaryMapFn(PK)
|
adamc@88
|
106
|
adamc@88
|
107 type env = PS.set PM.map
|
adamc@88
|
108
|
adamc@478
|
109 fun p_env x =
|
adamc@478
|
110 (print "\nDENV:\n";
|
adamc@478
|
111 PM.appi (fn (p1, ps) =>
|
adamc@478
|
112 PS.app (fn p2 =>
|
adamc@478
|
113 print (rp2s p1 ^ " ~ " ^ rp2s p2 ^ "\n")) ps) x)
|
adamc@478
|
114
|
adamc@251
|
115 structure E = ElabEnv
|
adamc@251
|
116
|
adamc@251
|
117 type goal = ErrorMsg.span * E.env * env * Elab.con * Elab.con
|
adamc@90
|
118
|
adamc@88
|
119 val empty = PM.empty
|
adamc@82
|
120
|
adamc@82
|
121 fun nameToRow (c, loc) =
|
adamc@82
|
122 (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc)
|
adamc@82
|
123
|
adamc@207
|
124 fun pieceToRow' (p, loc) =
|
adamc@82
|
125 case p of
|
adamc@82
|
126 NameC s => nameToRow (CName s, loc)
|
adamc@82
|
127 | NameR n => nameToRow (CRel n, loc)
|
adamc@82
|
128 | NameN n => nameToRow (CNamed n, loc)
|
adamc@88
|
129 | NameM (n, xs, x) => nameToRow (CModProj (n, xs, x), loc)
|
adamc@82
|
130 | RowR n => (CRel n, loc)
|
adamc@88
|
131 | RowN n => (CNamed n, loc)
|
adamc@88
|
132 | RowM (n, xs, x) => (CModProj (n, xs, x), loc)
|
adamc@88
|
133
|
adamc@207
|
134 fun pieceToRow ((p, ns), loc) =
|
adamc@207
|
135 foldl (fn (n, c) => (CProj (c, n), loc)) (pieceToRow' (p, loc)) ns
|
adamc@207
|
136
|
adamc@88
|
137 datatype piece' =
|
adamc@88
|
138 Piece of piece
|
adamc@88
|
139 | Unknown of con
|
adamc@82
|
140
|
adamc@207
|
141 fun pieceEnter' p =
|
adamc@88
|
142 case p of
|
adamc@88
|
143 NameR n => NameR (n + 1)
|
adamc@88
|
144 | RowR n => RowR (n + 1)
|
adamc@88
|
145 | _ => p
|
adamc@82
|
146
|
adamc@207
|
147 fun pieceEnter (p, n) = (pieceEnter' p, n)
|
adamc@207
|
148
|
adamc@88
|
149 fun enter denv =
|
adamc@88
|
150 PM.foldli (fn (p, pset, denv') =>
|
adamc@88
|
151 PM.insert (denv', pieceEnter p, PS.map pieceEnter pset))
|
adamc@88
|
152 PM.empty denv
|
adamc@82
|
153
|
adamc@335
|
154 val lowercase = CharVector.map Char.toLower
|
adamc@335
|
155
|
adamc@82
|
156 fun prove1 denv (p1, p2) =
|
adamc@82
|
157 case (p1, p2) of
|
adamc@335
|
158 ((NameC s1, _), (NameC s2, _)) => lowercase s1 <> lowercase s2
|
adamc@88
|
159 | _ =>
|
adamc@88
|
160 case PM.find (denv, p1) of
|
adamc@88
|
161 NONE => false
|
adamc@88
|
162 | SOME pset => PS.member (pset, p2)
|
adamc@82
|
163
|
adamc@90
|
164 fun decomposeRow (env, denv) c =
|
adamc@82
|
165 let
|
adamc@251
|
166 val loc = #2 c
|
adamc@251
|
167
|
adamc@207
|
168 fun decomposeProj c =
|
adamc@207
|
169 let
|
adamc@207
|
170 val (c, gs) = hnormCon (env, denv) c
|
adamc@207
|
171 in
|
adamc@207
|
172 case #1 c of
|
adamc@207
|
173 CProj (c, n) =>
|
adamc@207
|
174 let
|
adamc@207
|
175 val (c', ns, gs') = decomposeProj c
|
adamc@207
|
176 in
|
adamc@207
|
177 (c', ns @ [n], gs @ gs')
|
adamc@207
|
178 end
|
adamc@207
|
179 | _ => (c, [], gs)
|
adamc@207
|
180 end
|
adamc@207
|
181
|
adamc@90
|
182 fun decomposeName (c, (acc, gs)) =
|
adamc@90
|
183 let
|
adamc@207
|
184 val (cAll as (c, _), ns, gs') = decomposeProj c
|
adamc@90
|
185
|
adamc@90
|
186 val acc = case c of
|
adamc@207
|
187 CName s => Piece (NameC s, ns) :: acc
|
adamc@207
|
188 | CRel n => Piece (NameR n, ns) :: acc
|
adamc@207
|
189 | CNamed n => Piece (NameN n, ns) :: acc
|
adamc@207
|
190 | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x), ns) :: acc
|
adamc@90
|
191 | _ => Unknown cAll :: acc
|
adamc@90
|
192 in
|
adamc@90
|
193 (acc, gs' @ gs)
|
adamc@90
|
194 end
|
adamc@90
|
195
|
adamc@251
|
196 fun decomposeRow' (c, (acc, gs)) =
|
adamc@90
|
197 let
|
adamc@251
|
198 fun default () =
|
adamc@251
|
199 let
|
adamc@251
|
200 val (cAll as (c, _), ns, gs') = decomposeProj c
|
adamc@251
|
201 val gs = gs' @ gs
|
adamc@251
|
202 in
|
adamc@251
|
203 case c of
|
adamc@251
|
204 CRecord (_, xcs) => foldl (fn ((x, _), acc_gs) => decomposeName (x, acc_gs)) (acc, gs) xcs
|
adamc@251
|
205 | CConcat (c1, c2) => decomposeRow' (c1, decomposeRow' (c2, (acc, gs)))
|
adamc@251
|
206 | CRel n => (Piece (RowR n, ns) :: acc, gs)
|
adamc@251
|
207 | CNamed n => (Piece (RowN n, ns) :: acc, gs)
|
adamc@251
|
208 | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x), ns) :: acc, gs)
|
adamc@251
|
209 | _ => (Unknown cAll :: acc, gs)
|
adamc@251
|
210 end
|
adamc@90
|
211 in
|
adamc@326
|
212 (*Print.prefaces "decomposeRow'" [("c", ElabPrint.p_con env c),
|
adamc@326
|
213 ("c'", ElabPrint.p_con env (#1 (hnormCon (env, denv) c)))];*)
|
adamc@251
|
214 case #1 (#1 (hnormCon (env, denv) c)) of
|
adamc@251
|
215 CApp (
|
adamc@251
|
216 (CApp (
|
adamc@251
|
217 (CApp ((CFold (dom, ran), _), f), _),
|
adamc@251
|
218 i), _),
|
adamc@251
|
219 r) =>
|
adamc@251
|
220 let
|
adamc@251
|
221 val (env', nm) = E.pushCNamed env "nm" (KName, loc) NONE
|
adamc@251
|
222 val (env', v) = E.pushCNamed env' "v" dom NONE
|
adamc@251
|
223 val (env', st) = E.pushCNamed env' "st" ran NONE
|
adamc@251
|
224
|
adamc@251
|
225 val (denv', gs') = assert env' denv ((CRecord (dom, [((CNamed nm, loc),
|
adamc@251
|
226 (CUnit, loc))]), loc),
|
adamc@251
|
227 (CNamed st, loc))
|
adamc@251
|
228
|
adamc@251
|
229 val c' = (CApp (f, (CNamed nm, loc)), loc)
|
adamc@251
|
230 val c' = (CApp (c', (CNamed v, loc)), loc)
|
adamc@251
|
231 val c' = (CApp (c', (CNamed st, loc)), loc)
|
adamc@251
|
232 val (ps, gs'') = decomposeRow (env', denv') c'
|
adamc@251
|
233
|
adamc@251
|
234 fun covered p =
|
adamc@251
|
235 case p of
|
adamc@251
|
236 Unknown _ => false
|
adamc@251
|
237 | Piece p =>
|
adamc@251
|
238 case p of
|
adamc@251
|
239 (NameN n, []) => n = nm
|
adamc@251
|
240 | (RowN n, []) => n = st
|
adamc@251
|
241 | _ => false
|
adamc@251
|
242
|
adamc@251
|
243 val ps = List.filter (not o covered) ps
|
adamc@251
|
244 in
|
adamc@251
|
245 decomposeRow' (i, decomposeRow' (r, (ps @ acc, gs'' @ gs' @ gs)))
|
adamc@251
|
246 end
|
adamc@251
|
247 | _ => default ()
|
adamc@90
|
248 end
|
adamc@90
|
249 in
|
adamc@251
|
250 decomposeRow' (c, ([], []))
|
adamc@90
|
251 end
|
adamc@90
|
252
|
adamc@90
|
253 and assert env denv (c1, c2) =
|
adamc@90
|
254 let
|
adamc@90
|
255 val (ps1, gs1) = decomposeRow (env, denv) c1
|
adamc@90
|
256 val (ps2, gs2) = decomposeRow (env, denv) c2
|
adamc@90
|
257
|
adamc@90
|
258 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
|
adamc@90
|
259 val ps1 = unUnknown ps1
|
adamc@90
|
260 val ps2 = unUnknown ps2
|
adamc@90
|
261
|
adamc@90
|
262 (*val () = print "APieces1:\n"
|
adamc@90
|
263 val () = app pp ps1
|
adamc@90
|
264 val () = print "APieces2:\n"
|
adamc@90
|
265 val () = app pp ps2*)
|
adamc@90
|
266
|
adamc@90
|
267 fun assertPiece ps (p, denv) =
|
adamc@90
|
268 let
|
adamc@90
|
269 val pset = Option.getOpt (PM.find (denv, p), PS.empty)
|
adamc@90
|
270 val ps = case p of
|
adamc@207
|
271 (NameC _, _) => List.filter (fn (NameC _, _) => false | _ => true) ps
|
adamc@90
|
272 | _ => ps
|
adamc@90
|
273 val pset = PS.addList (pset, ps)
|
adamc@90
|
274 in
|
adamc@90
|
275 PM.insert (denv, p, pset)
|
adamc@90
|
276 end
|
adamc@90
|
277
|
adamc@90
|
278 val denv = foldl (assertPiece ps2) denv ps1
|
adamc@90
|
279 in
|
adamc@90
|
280 (foldl (assertPiece ps1) denv ps2, gs1 @ gs2)
|
adamc@90
|
281 end
|
adamc@90
|
282
|
adamc@90
|
283 and prove env denv (c1, c2, loc) =
|
adamc@90
|
284 let
|
adamc@90
|
285 val (ps1, gs1) = decomposeRow (env, denv) c1
|
adamc@90
|
286 val (ps2, gs2) = decomposeRow (env, denv) c2
|
adamc@82
|
287
|
adamc@88
|
288 val hasUnknown = List.exists (fn Unknown _ => true | _ => false)
|
adamc@88
|
289 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
|
adamc@82
|
290 in
|
adamc@82
|
291 if hasUnknown ps1 orelse hasUnknown ps2 then
|
adamc@90
|
292 [(loc, env, denv, c1, c2)]
|
adamc@82
|
293 else
|
adamc@88
|
294 let
|
adamc@88
|
295 val ps1 = unUnknown ps1
|
adamc@88
|
296 val ps2 = unUnknown ps2
|
adamc@88
|
297
|
adamc@88
|
298 in
|
adamc@88
|
299 (*print "Pieces1:\n";
|
adamc@88
|
300 app pp ps1;
|
adamc@88
|
301 print "Pieces2:\n";
|
adamc@88
|
302 app pp ps2;*)
|
adamc@88
|
303
|
adamc@88
|
304 foldl (fn (p1, rem) =>
|
adamc@88
|
305 foldl (fn (p2, rem) =>
|
adamc@88
|
306 if prove1 denv (p1, p2) then
|
adamc@88
|
307 rem
|
adamc@88
|
308 else
|
adamc@90
|
309 (loc, env, denv, pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2)
|
adamc@90
|
310 (gs1 @ gs2) ps1
|
adamc@88
|
311 end
|
adamc@82
|
312 end
|
adamc@82
|
313
|
adamc@90
|
314 and hnormCon (env, denv) c =
|
adamc@90
|
315 let
|
adamc@90
|
316 val cAll as (c, loc) = ElabOps.hnormCon env c
|
adamc@90
|
317
|
adamc@90
|
318 fun doDisj (c1, c2, c) =
|
adamc@90
|
319 let
|
adamc@90
|
320 val (c, gs) = hnormCon (env, denv) c
|
adamc@90
|
321 in
|
adamc@90
|
322 (c, prove env denv (c1, c2, loc) @ gs)
|
adamc@90
|
323 end
|
adamc@90
|
324 in
|
adamc@90
|
325 case c of
|
adamc@345
|
326 CDisjoint (Instantiate, c1, c2, c) => doDisj (c1, c2, c)
|
adamc@90
|
327 | _ => (cAll, [])
|
adamc@90
|
328 end
|
adamc@90
|
329
|
adamc@82
|
330 end
|