Mercurial > urweb

comparison src/elab_ops.sml @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hooks for measuring how much interesting proving is going on in elaboration
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Nov 2009 12:44:14 -0500
parents 46803e668a89
children c7b9a33c26c8
comparison
equal deleted inserted replaced
1033:b734ff578ac7 1034:a779402841f6
141 case b of 141 case b of
142 U.Con.RelC _ => n + 1 142 U.Con.RelC _ => n + 1
143 | _ => n} 143 | _ => n}
144 0 144 0
145 145
146 val identity = ref 0
147 val distribute = ref 0
148 val fuse = ref 0
149
150 fun reset () = (identity := 0;
151 distribute := 0;
152 fuse := 0)
146 153
147 fun hnormCon env (cAll as (c, loc)) = 154 fun hnormCon env (cAll as (c, loc)) =
148 case c of 155 case c of
149 CUnif (_, _, _, ref (SOME c)) => hnormCon env c 156 CUnif (_, _, _, ref (SOME c)) => hnormCon env c
150 157
217 fun unconstraint c = 224 fun unconstraint c =
218 case hnormCon env c of 225 case hnormCon env c of
219 (TDisjoint (_, _, c), _) => unconstraint c 226 (TDisjoint (_, _, c), _) => unconstraint c
220 | c => c 227 | c => c
221 228
229 fun inc r = r := !r + 1
230
222 fun tryDistributivity () = 231 fun tryDistributivity () =
223 case hnormCon env c2 of 232 case hnormCon env c2 of
224 (CConcat (c1, c2'), _) => 233 (CConcat (c1, c2'), _) =>
225 let 234 let
226 val c = (CMap ks, loc) 235 val c = (CMap ks, loc)
228 237
229 val c1 = (CApp (c, c1), loc) 238 val c1 = (CApp (c, c1), loc)
230 val c2 = (CApp (c, c2'), loc) 239 val c2 = (CApp (c, c2'), loc)
231 val c = (CConcat (c1, c2), loc) 240 val c = (CConcat (c1, c2), loc)
232 in 241 in
242 inc distribute;
233 hnormCon env c 243 hnormCon env c
234 end 244 end
235 | _ => default () 245 | _ => default ()
236 246
237 fun tryFusion () = 247 fun tryFusion () =
251 261
252 val c = (CMap (dom, k2), loc) 262 val c = (CMap (dom, k2), loc)
253 val c = (CApp (c, f'), loc) 263 val c = (CApp (c, f'), loc)
254 val c = (CApp (c, r'), loc) 264 val c = (CApp (c, r'), loc)
255 in 265 in
266 inc fuse;
256 hnormCon env c 267 hnormCon env c
257 end 268 end
258 | _ => tryDistributivity ()) 269 | _ => tryDistributivity ())
259 | _ => tryDistributivity ()) 270 | _ => tryDistributivity ())
260 | _ => tryDistributivity () 271 | _ => tryDistributivity ()
273 val c = (CApp (f, v), loc) 284 val c = (CApp (f, v), loc)
274 in 285 in
275 case unconstraint c of 286 case unconstraint c of
276 (CUnif (_, _, _, vR'), _) => 287 (CUnif (_, _, _, vR'), _) =>
277 if vR' = vR then 288 if vR' = vR then
278 hnormCon env c2 289 (inc identity;
290 hnormCon env c2)
279 else 291 else
280 tryFusion () 292 tryFusion ()
281 | _ => tryFusion () 293 | _ => tryFusion ()
282 end 294 end
283 in 295 in