From 8d6ea0f475b6a47a2f1072897b226d51648eb3f7 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 11 Nov 2008 19:58:25 -0500 Subject: Map distributivity rule in hnormCon --- src/elab_ops.sml | 50 ++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 42 insertions(+), 8 deletions(-) (limited to 'src/elab_ops.sml') diff --git a/src/elab_ops.sml b/src/elab_ops.sml index 95ad971f..5102d0ab 100644 --- a/src/elab_ops.sml +++ b/src/elab_ops.sml @@ -150,6 +150,39 @@ fun hnormCon env (cAll as (c, loc)) = | 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 @@ fun hnormCon env (cAll as (c, loc)) = 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 -- cgit v1.2.3