summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-11 19:58:25 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-11 19:58:25 -0500
commit8d6ea0f475b6a47a2f1072897b226d51648eb3f7 (patch)
treef9de1c5b3c0d3061abe8db877a35e1b1e93b102c
parent887af944c67e3395679a750a205ef114234c61a0 (diff)
Map distributivity rule in hnormCon
-rw-r--r--src/elab_ops.sml50
-rw-r--r--src/elab_print.sml2
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}) =>