Mercurial > urweb

comparison src/disjoint.sml @ 628:12b73f3c108e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Switch to TDisjoint from CDisjoint; still need to implement obligation generation at EDisjoint uses
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 12:01:24 -0500
parents 8998114760c1
children 0406e9cccb72
comparison
equal deleted inserted replaced
627:f4f2b09a533a 628:12b73f3c108e
159 | _ => 159 | _ =>
160 case PM.find (denv, p1) of 160 case PM.find (denv, p1) of
161 NONE => false 161 NONE => false
162 | SOME pset => PS.member (pset, p2) 162 | SOME pset => PS.member (pset, p2)
163 163
164 fun decomposeRow (env, denv) c = 164 fun decomposeRow env c =
165 let 165 let
166 val loc = #2 c 166 val loc = #2 c
167 167
168 fun decomposeProj c = 168 fun decomposeProj c =
169 let 169 let
170 val (c, gs) = hnormCon (env, denv) c 170 val c = hnormCon env c
171 in 171 in
172 case #1 c of 172 case #1 c of
173 CProj (c, n) => 173 CProj (c, n) =>
174 let 174 let
175 val (c', ns, gs') = decomposeProj c 175 val (c', ns) = decomposeProj c
176 in 176 in
177 (c', ns @ [n], gs @ gs') 177 (c', ns @ [n])
178 end 178 end
179 | _ => (c, [], gs) 179 | _ => (c, [])
180 end 180 end
181 181
182 fun decomposeName (c, (acc, gs)) = 182 fun decomposeName (c, acc) =
183 let 183 let
184 val (cAll as (c, _), ns, gs') = decomposeProj c 184 val (cAll as (c, _), ns) = decomposeProj c
185 185 in
186 val acc = case c of 186 case c of
187 CName s => Piece (NameC s, ns) :: acc 187 CName s => Piece (NameC s, ns) :: acc
188 | CRel n => Piece (NameR n, ns) :: acc 188 | CRel n => Piece (NameR n, ns) :: acc
189 | CNamed n => Piece (NameN n, ns) :: acc 189 | CNamed n => Piece (NameN n, ns) :: acc
190 | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x), ns) :: acc 190 | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x), ns) :: acc
191 | _ => Unknown cAll :: acc 191 | _ => Unknown cAll :: acc
192 in 192 end
193 (acc, gs' @ gs) 193
194 end 194 fun decomposeRow' (c, acc) =
195
196 fun decomposeRow' (c, (acc, gs)) =
197 let 195 let
198 fun default () = 196 fun default () =
199 let 197 let
200 val (cAll as (c, _), ns, gs') = decomposeProj c 198 val (cAll as (c, _), ns) = decomposeProj c
201 val gs = gs' @ gs
202 in 199 in
203 case c of 200 case c of
204 CRecord (_, xcs) => foldl (fn ((x, _), acc_gs) => decomposeName (x, acc_gs)) (acc, gs) xcs 201 CRecord (_, xcs) => foldl (fn ((x, _), acc) => decomposeName (x, acc)) acc xcs
205 | CConcat (c1, c2) => decomposeRow' (c1, decomposeRow' (c2, (acc, gs))) 202 | CConcat (c1, c2) => decomposeRow' (c1, decomposeRow' (c2, acc))
206 | CRel n => (Piece (RowR n, ns) :: acc, gs) 203 | CRel n => Piece (RowR n, ns) :: acc
207 | CNamed n => (Piece (RowN n, ns) :: acc, gs) 204 | CNamed n => Piece (RowN n, ns) :: acc
208 | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x), ns) :: acc, gs) 205 | CModProj (m1, ms, x) => Piece (RowM (m1, ms, x), ns) :: acc
209 | _ => (Unknown cAll :: acc, gs) 206 | _ => Unknown cAll :: acc
210 end 207 end
211 in 208 in
212 (*Print.prefaces "decomposeRow'" [("c", ElabPrint.p_con env c), 209 case #1 (hnormCon env c) of
213 ("c'", ElabPrint.p_con env (#1 (hnormCon (env, denv) c)))];*)
214 case #1 (#1 (hnormCon (env, denv) c)) of
215 CApp ( 210 CApp (
216 (CApp ((CMap _, _), _), _), 211 (CApp ((CMap _, _), _), _),
217 r) => decomposeRow' (r, (acc, gs)) 212 r) => decomposeRow' (r, acc)
218 | _ => default () 213 | _ => default ()
219 end 214 end
220 in 215 in
221 decomposeRow' (c, ([], [])) 216 decomposeRow' (c, [])
222 end 217 end
223 218
224 and assert env denv (c1, c2) = 219 and assert env denv (c1, c2) =
225 let 220 let
226 val (ps1, gs1) = decomposeRow (env, denv) c1 221 val ps1 = decomposeRow env c1
227 val (ps2, gs2) = decomposeRow (env, denv) c2 222 val ps2 = decomposeRow env c2
228 223
229 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p) 224 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
230 val ps1 = unUnknown ps1 225 val ps1 = unUnknown ps1
231 val ps2 = unUnknown ps2 226 val ps2 = unUnknown ps2
232 227
246 PM.insert (denv, p, pset) 241 PM.insert (denv, p, pset)
247 end 242 end
248 243
249 val denv = foldl (assertPiece ps2) denv ps1 244 val denv = foldl (assertPiece ps2) denv ps1
250 in 245 in
251 (foldl (assertPiece ps1) denv ps2, gs1 @ gs2) 246 foldl (assertPiece ps1) denv ps2
252 end 247 end
253 248
254 and prove env denv (c1, c2, loc) = 249 and prove env denv (c1, c2, loc) =
255 let 250 let
256 val (ps1, gs1) = decomposeRow (env, denv) c1 251 val ps1 = decomposeRow env c1
257 val (ps2, gs2) = decomposeRow (env, denv) c2 252 val ps2 = decomposeRow env c2
258 253
259 val hasUnknown = List.exists (fn Unknown _ => true | _ => false) 254 val hasUnknown = List.exists (fn Unknown _ => true | _ => false)
260 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p) 255 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p)
261 in 256 in
262 if hasUnknown ps1 orelse hasUnknown ps2 then 257 if hasUnknown ps1 orelse hasUnknown ps2 then
263 [(loc, env, denv, c1, c2)] 258 [(loc, env, denv, c1, c2)]
264 else 259 else
265 let 260 let
266 val ps1 = unUnknown ps1 261 val ps1 = unUnknown ps1
267 val ps2 = unUnknown ps2 262 val ps2 = unUnknown ps2
268
269 in 263 in
270 (*print "Pieces1:\n"; 264 (*print "Pieces1:\n";
271 app pp ps1; 265 app pp ps1;
272 print "Pieces2:\n"; 266 print "Pieces2:\n";
273 app pp ps2;*) 267 app pp ps2;*)
276 foldl (fn (p2, rem) => 270 foldl (fn (p2, rem) =>
277 if prove1 denv (p1, p2) then 271 if prove1 denv (p1, p2) then
278 rem 272 rem
279 else 273 else
280 (loc, env, denv, pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2) 274 (loc, env, denv, pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2)
281 (gs1 @ gs2) ps1 275 [] ps1
282 end 276 end
283 end 277 end
284 278
285 and hnormCon (env, denv) c =
286 let
287 val cAll as (c, loc) = ElabOps.hnormCon env c
288
289 fun doDisj (c1, c2, c) =
290 let
291 val (c, gs) = hnormCon (env, denv) c
292 in
293 (c, prove env denv (c1, c2, loc) @ gs)
294 end
295 in
296 case c of
297 CDisjoint (Instantiate, c1, c2, c) => doDisj (c1, c2, c)
298 | _ => (cAll, [])
299 end
300
301 end 279 end