Mercurial > urweb
comparison src/disjoint.sml @ 251:326fb4686f60
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 |