diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-11-11 19:58:25 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-11-11 19:58:25 -0500 |
| commit | 8d6ea0f475b6a47a2f1072897b226d51648eb3f7 (patch) | |
| tree | f9de1c5b3c0d3061abe8db877a35e1b1e93b102c | |
| parent | 887af944c67e3395679a750a205ef114234c61a0 (diff) | |
Map distributivity rule in hnormCon
| -rw-r--r-- | src/elab_ops.sml | 50 | ||||
| -rw-r--r-- | src/elab_print.sml | 2 |
2 files changed, 43 insertions, 9 deletions
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 diff --git a/src/elab_print.sml b/src/elab_print.sml index 62b1ea02..2f652737 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -335,7 +335,7 @@ fun p_exp' par env (e, _) = else box [p_exp' true env e1, space, - string "with", + string "++", space, p_exp' true env e2]) | ECut (e, c, {field, rest}) => |