Mercurial > urweb

comparison src/disjoint.sml @ 251:326fb4686f60

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Monoize transaction identifiers; improve disjointness prover on irreducible folds; change 'query' type
author Adam Chlipala <adamc@hcoop.net>
date Sun, 31 Aug 2008 10:36:54 -0400
parents cc68da3801bc
children 950320f33232
comparison
equal deleted inserted replaced
250:98f551ddd54b 251:326fb4686f60
102 structure PS = BinarySetFn(PK) 102 structure PS = BinarySetFn(PK)
103 structure PM = BinaryMapFn(PK) 103 structure PM = BinaryMapFn(PK)
104 104
105 type env = PS.set PM.map 105 type env = PS.set PM.map
106 106
107 type goal = ErrorMsg.span * ElabEnv.env * env * Elab.con * Elab.con 107 structure E = ElabEnv
108
109 type goal = ErrorMsg.span * E.env * env * Elab.con * Elab.con
108 110
109 val empty = PM.empty 111 val empty = PM.empty
110 112
111 fun nameToRow (c, loc) = 113 fun nameToRow (c, loc) =
112 (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc) 114 (CRecord ((KUnit, loc), [((c, loc), (CUnit, loc))]), loc)
149 NONE => false 151 NONE => false
150 | SOME pset => PS.member (pset, p2) 152 | SOME pset => PS.member (pset, p2)
151 153
152 fun decomposeRow (env, denv) c = 154 fun decomposeRow (env, denv) c =
153 let 155 let
156 val loc = #2 c
157
154 fun decomposeProj c = 158 fun decomposeProj c =
155 let 159 let
156 val (c, gs) = hnormCon (env, denv) c 160 val (c, gs) = hnormCon (env, denv) c
157 in 161 in
158 case #1 c of 162 case #1 c of
177 | _ => Unknown cAll :: acc 181 | _ => Unknown cAll :: acc
178 in 182 in
179 (acc, gs' @ gs) 183 (acc, gs' @ gs)
180 end 184 end
181 185
182 fun decomposeRow (c, (acc, gs)) = 186 fun decomposeRow' (c, (acc, gs)) =
183 let 187 let
184 val (cAll as (c, _), ns, gs') = decomposeProj c 188 fun default () =
185 val gs = gs' @ gs 189 let
186 in 190 val (cAll as (c, _), ns, gs') = decomposeProj c
187 case c of 191 val gs = gs' @ gs
188 CRecord (_, xcs) => foldl (fn ((x, _), acc_gs) => decomposeName (x, acc_gs)) (acc, gs) xcs 192 in
189 | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, (acc, gs))) 193 case c of
190 | CRel n => (Piece (RowR n, ns) :: acc, gs) 194 CRecord (_, xcs) => foldl (fn ((x, _), acc_gs) => decomposeName (x, acc_gs)) (acc, gs) xcs
191 | CNamed n => (Piece (RowN n, ns) :: acc, gs) 195 | CConcat (c1, c2) => decomposeRow' (c1, decomposeRow' (c2, (acc, gs)))
192 | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x), ns) :: acc, gs) 196 | CRel n => (Piece (RowR n, ns) :: acc, gs)
193 | _ => (Unknown cAll :: acc, gs) 197 | CNamed n => (Piece (RowN n, ns) :: acc, gs)
198 | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x), ns) :: acc, gs)
199 | _ => (Unknown cAll :: acc, gs)
200 end
201 in
202 case #1 (#1 (hnormCon (env, denv) c)) of
203 CApp (
204 (CApp (
205 (CApp ((CFold (dom, ran), _), f), _),
206 i), _),
207 r) =>
208 let
209 val (env', nm) = E.pushCNamed env "nm" (KName, loc) NONE
210 val (env', v) = E.pushCNamed env' "v" dom NONE
211 val (env', st) = E.pushCNamed env' "st" ran NONE
212
213 val (denv', gs') = assert env' denv ((CRecord (dom, [((CNamed nm, loc),
214 (CUnit, loc))]), loc),
215 (CNamed st, loc))
216
217 val c' = (CApp (f, (CNamed nm, loc)), loc)
218 val c' = (CApp (c', (CNamed v, loc)), loc)
219 val c' = (CApp (c', (CNamed st, loc)), loc)
220 val (ps, gs'') = decomposeRow (env', denv') c'
221
222 fun covered p =
223 case p of
224 Unknown _ => false
225 | Piece p =>
226 case p of
227 (NameN n, []) => n = nm
228 | (RowN n, []) => n = st
229 | _ => false
230
231 val ps = List.filter (not o covered) ps
232 in
233 decomposeRow' (i, decomposeRow' (r, (ps @ acc, gs'' @ gs' @ gs)))
234 end
235 | _ => default ()
194 end 236 end
195 in 237 in
196 decomposeRow (c, ([], [])) 238 decomposeRow' (c, ([], []))
197 end 239 end
198 240
199 and assert env denv (c1, c2) = 241 and assert env denv (c1, c2) =
200 let 242 let
201 val (ps1, gs1) = decomposeRow (env, denv) c1 243 val (ps1, gs1) = decomposeRow (env, denv) c1