Mercurial > urweb
changeset 494:1bbcc3345d12
Map distributivity rule in hnormCon
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 11 Nov 2008 19:58:25 -0500 |
| parents | ae03d09043c1 |
| children | 98f85c1bc867 |
| files | src/elab_ops.sml src/elab_print.sml |
| diffstat | 2 files changed, 43 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab_ops.sml Tue Nov 11 19:20:37 2008 -0500 +++ b/src/elab_ops.sml Tue Nov 11 19:58:25 2008 -0500 @@ -150,6 +150,39 @@ | c => c val c = unconstraint c + fun tryDistributivity () = + let + fun distribute (c1, c2) = + let + val c = (CFold ks, loc) + val c = (CApp (c, f), loc) + val c = (CApp (c, i), loc) + + val c1 = (CApp (c, c1), loc) + val c2 = (CApp (c, c2), loc) + val c = (CConcat (c1, c2), loc) + in + hnormCon env c + end + in + case (hnormCon env i, hnormCon env c2, hnormCon env c) of + ((CRecord (_, []), _), + (CConcat (arg1, arg2), _), + (CConcat (c1, c2'), _)) => + (case (hnormCon env c1, hnormCon env c2') of + ((CRecord (_, [(nm', v')]), _), + (CUnif (_, _, _, rR'), _)) => + (case hnormCon env nm' of + (CUnif (_, _, _, nmR'), _) => + if nmR' = nmR andalso rR' = rR then + distribute (arg1, arg2) + else + default () + | _ => default ()) + | _ => default ()) + | _ => default () + end + fun tryFusion () = let fun fuse (dom, new_v, r') = @@ -205,16 +238,17 @@ rR := SOME (CError, loc); fuse (dom, v', r')) else - default () - | _ => default ()) - | _ => default ()) - | _ => default () + tryDistributivity () + | _ => tryDistributivity ()) + | _ => tryDistributivity ()) + | _ => tryDistributivity () end - | _ => default ()) - | _ => default ()) - | _ => default ()) - | _ => default () + | _ => tryDistributivity ()) + | _ => tryDistributivity ()) + | _ => tryDistributivity ()) + | _ => tryDistributivity () end + in (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*) case (hnormCon env i, unconstraint c) of