Mercurial > urweb

comparison src/elab_ops.sml @ 1714:d6c45026240d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Do a lot more type simplification for error messages
author Adam Chlipala <adam@chlipala.net>
date Mon, 16 Apr 2012 09:46:42 -0400
parents 6c00d8af6239
children dd12d6d9e9a7
comparison
equal deleted inserted replaced
1713:1b3f82b09bb0 1714:d6c45026240d
322 (CTuple cs, _) => hnormCon env (List.nth (cs, n - 1)) 322 (CTuple cs, _) => hnormCon env (List.nth (cs, n - 1))
323 | _ => cAll) 323 | _ => cAll)
324 324
325 | _ => cAll 325 | _ => cAll
326 326
327 fun reduceCon env (cAll as (c, loc)) =
328 case c of
329 TFun (c1, c2) => (TFun (reduceCon env c1, reduceCon env c2), loc)
330 | TCFun (exp, x, k, c) => (TCFun (exp, x, k, reduceCon env c), loc)
331 | TRecord c => (TRecord (reduceCon env c), loc)
332 | TDisjoint (c1, c2, c3) => (TDisjoint (reduceCon env c1, reduceCon env c2, reduceCon env c3), loc)
333
334 | CRel _ => cAll
335 | CNamed xn =>
336 (case E.lookupCNamed env xn of
337 (_, _, SOME c') => reduceCon env c'
338 | _ => cAll)
339 | CModProj _ => cAll
340 | CApp (c1, c2) =>
341 let
342 val c1 = reduceCon env c1
343 val c2 = reduceCon env c2
344 fun default () = (CApp (c1, c2), loc)
345 in
346 case #1 c1 of
347 CAbs (x, k, cb) =>
348 ((reduceCon env (subConInCon (0, c2) cb))
349 handle SynUnif => default ())
350 | CApp (c', f) =>
351 let
352 val c' = reduceCon env c'
353 val f = reduceCon env f
354 in
355 case #1 c' of
356 CMap (ks as (k1, k2)) =>
357 (case #1 c2 of
358 CRecord (_, []) => (CRecord (k2, []), loc)
359 | CRecord (_, (x, c) :: rest) =>
360 reduceCon env
361 (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
362 (CApp (c1, (CRecord (k2, rest), loc)), loc)), loc)
363 | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
364 let
365 val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
366 in
367 reduceCon env
368 (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
369 (CApp (c1, rest''), loc)), loc)
370 end
371 | _ =>
372 let
373 fun unconstraint c =
374 case reduceCon env c of
375 (TDisjoint (_, _, c), _) => unconstraint c
376 | c => c
377
378 fun inc r = r := !r + 1
379
380 fun tryDistributivity () =
381 case reduceCon env c2 of
382 (CConcat (c1, c2), _) =>
383 let
384 val c = (CMap ks, loc)
385 val c = (CApp (c, f), loc)
386
387 val c1 = (CApp (c, c1), loc)
388 val c2 = (CApp (c, c2), loc)
389 val c = (CConcat (c1, c2), loc)
390 in
391 inc distribute;
392 reduceCon env c
393 end
394 | _ => default ()
395
396 fun tryFusion () =
397 case #1 (reduceCon env c2) of
398 CApp (f', r') =>
399 (case #1 (reduceCon env f') of
400 CApp (f', inner_f) =>
401 (case #1 (reduceCon env f') of
402 CMap (dom, _) =>
403 let
404 val inner_f = liftConInCon 0 inner_f
405 val f = liftConInCon 0 f
406
407 val f' = (CApp (inner_f, (CRel 0, loc)), loc)
408 val f' = (CApp (f, f'), loc)
409 val f' = (CAbs ("v", dom, f'), loc)
410
411 val c = (CMap (dom, k2), loc)
412 val c = (CApp (c, f'), loc)
413 val c = (CApp (c, r'), loc)
414 in
415 inc fuse;
416 reduceCon env c
417 end
418 | _ => tryDistributivity ())
419 | _ => tryDistributivity ())
420 | _ => tryDistributivity ()
421
422 fun tryIdentity () =
423 let
424 fun cunif () =
425 let
426 val r = ref (Unknown (fn _ => true))
427 in
428 (r, (CUnif (0, loc, (KType, loc), "_", r), loc))
429 end
430
431 val (vR, v) = cunif ()
432
433 val c = (CApp (f, v), loc)
434 in
435 case unconstraint c of
436 (CUnif (_, _, _, _, vR'), _) =>
437 if vR' = vR then
438 (inc identity;
439 reduceCon env c2)
440 else
441 tryFusion ()
442 | _ => tryFusion ()
443 end
444 in
445 tryIdentity ()
446 end)
447 | _ => default ()
448 end
449 | _ => default ()
450 end
451 | CAbs (x, k, b) =>
452 let
453 val b = reduceCon (E.pushCRel env x k) b
454 fun default () = (CAbs (x, k, b), loc)
455 in
456 case #1 b of
457 CApp (f, (CRel 0, _)) =>
458 if occurs f then
459 default ()
460 else
461 reduceCon env (subConInCon (0, (CUnit, loc)) f)
462 | _ => default ()
463 end
464
465 | CKAbs (x, b) => (CKAbs (x, reduceCon (E.pushKRel env x) b), loc)
466 | CKApp (c1, k) =>
467 (case reduceCon env c1 of
468 (CKAbs (_, body), _) => reduceCon env (subKindInCon (0, k) body)
469 | c1 => (CKApp (c1, k), loc))
470 | TKFun (x, c) => (TKFun (x, reduceCon env c), loc)
471
472 | CName _ => cAll
473
474 | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (reduceCon env x, reduceCon env c)) xcs), loc)
475 | CConcat (c1, c2) =>
476 let
477 val c1 = reduceCon env c1
478 val c2 = reduceCon env c2
479 in
480 case (c1, c2) of
481 ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => (CRecord (k, xcs1 @ xcs2), loc)
482 | ((CRecord (_, []), _), _) => c2
483 | ((CConcat (c11, c12), loc), _) => reduceCon env (CConcat (c11, (CConcat (c12, c2), loc)), loc)
484 | (_, (CRecord (_, []), _)) => c1
485 | _ => (CConcat (c1, c2), loc)
486 end
487 | CMap _ => cAll
488
489 | CUnit => cAll
490
491 | CTuple cs => (CTuple (map (reduceCon env) cs), loc)
492 | CProj (c, n) =>
493 (case reduceCon env c of
494 (CTuple cs, _) => reduceCon env (List.nth (cs, n - 1))
495 | c => (CProj (c, n), loc))
496
497 | CError => cAll
498
499 | CUnif (nl, _, _, _, ref (Known c)) => reduceCon env (E.mliftConInCon nl c)
500 | CUnif _ => cAll
501
327 end 502 end