From e44434a592770472b58f4ba052404824442ace23 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 21 Feb 2009 15:33:20 -0500 Subject: "Hello world" compiles, after replacing type-level fold with map --- src/elab_ops.sml | 253 +++++++++++++++++++------------------------------------ 1 file changed, 85 insertions(+), 168 deletions(-) (limited to 'src/elab_ops.sml') diff --git a/src/elab_ops.sml b/src/elab_ops.sml index 0648d704..c3e9274c 100644 --- a/src/elab_ops.sml +++ b/src/elab_ops.sml @@ -114,181 +114,98 @@ fun hnormCon env (cAll as (c, loc)) = ("sc", ElabPrint.p_con env sc)];*) sc end - | c1' as CApp (c', i) => + | c1' as CApp (c', f) => let fun default () = (CApp ((c1', loc), hnormCon env c2), loc) in case #1 (hnormCon env c') of - CApp (c', f) => - (case #1 (hnormCon env c') of - CFold ks => - (case #1 (hnormCon env c2) of - CRecord (_, []) => hnormCon env i - | CRecord (k, (x, c) :: rest) => - hnormCon env - (CApp ((CApp ((CApp (f, x), loc), c), loc), - (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), - (CRecord (k, rest), loc)), loc)), loc) - | CConcat ((CRecord (k, (x, c) :: rest), _), rest') => - let - val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc) - - (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc), - (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), - rest''), loc)), loc)*) - in - (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*) - hnormCon env - (CApp ((CApp ((CApp (f, x), loc), c), loc), - (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), - rest''), loc)), loc) - end - | _ => - let - fun cunif () = - let - val r = ref NONE - in - (r, (CUnif (loc, (KType, loc), "_", r), loc)) - end - - val (nmR, nm) = cunif () - val (vR, v) = cunif () - val (rR, r) = cunif () - - val c = f - val c = (CApp (c, nm), loc) - val c = (CApp (c, v), loc) - val c = (CApp (c, r), loc) - fun unconstraint c = - case hnormCon env c of - (CDisjoint (_, _, _, c), _) => unconstraint c - | 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') = - let - val ran = #2 ks - - val f = (CApp (f, (CRel 2, loc)), loc) - val f = (CApp (f, new_v), loc) - val f = (CApp (f, (CRel 0, loc)), loc) - val f = (CAbs ("acc", ran, f), loc) - val f = (CAbs ("v", dom, f), loc) - val f = (CAbs ("nm", (KName, loc), f), loc) - - val c = (CFold (dom, ran), loc) - val c = (CApp (c, f), loc) - val c = (CApp (c, i), loc) - val c = (CApp (c, r'), loc) - in - hnormCon env c - end - in - case #1 (hnormCon env c2) of - CApp (f, r') => - (case #1 (hnormCon env f) of - CApp (f, inner_i) => - (case (#1 (hnormCon env f), #1 (hnormCon env inner_i)) of - (CApp (f, inner_f), CRecord (_, [])) => - (case #1 (hnormCon env f) of - CFold (dom, _) => - let - val c = inner_f - val c = (CApp (c, nm), loc) - val c = (CApp (c, v), loc) - val c = (CApp (c, r), loc) - val c = unconstraint c - - (*val () = Print.prefaces "Onto something!" - [("c", ElabPrint.p_con env cAll), - ("c'", ElabPrint.p_con env c)]*) - - in - case #1 (hnormCon env c) of - CConcat (first, rest) => - (case (#1 (hnormCon env first), - #1 (hnormCon env rest)) of - (CRecord (_, [(nm', v')]), - CUnif (_, _, _, rR')) => - (case #1 (hnormCon env nm') of - CUnif (_, _, _, nmR') => - if rR' = rR andalso nmR' = nmR then - (nmR := SOME (CRel 2, loc); - vR := SOME (CRel 1, loc); - rR := SOME (CError, loc); - fuse (dom, v', r')) - else - tryDistributivity () - | _ => tryDistributivity ()) - | _ => tryDistributivity ()) - | _ => tryDistributivity () - end - | _ => tryDistributivity ()) - | _ => tryDistributivity ()) - | _ => tryDistributivity ()) - | _ => tryDistributivity () - end - - in - (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*) - case (hnormCon env i, unconstraint c) of - ((CRecord (_, []), _), - (CConcat (c1, c2'), _)) => - (case (hnormCon env c1, hnormCon env c2') of - ((CRecord (_, [(nm', v')]), _), - (CUnif (_, _, _, rR'), _)) => - (case (hnormCon env nm', hnormCon env v') of - ((CUnif (_, _, _, nmR'), _), - (CUnif (_, _, _, vR'), _)) => - if nmR' = nmR andalso vR' = vR andalso rR' = rR then - hnormCon env c2 - else - tryFusion () - | _ => tryFusion ()) - | _ => tryFusion ()) - | _ => tryFusion () - end) - | _ => default ()) + CMap (ks as (k1, k2)) => + (case #1 (hnormCon env c2) of + CRecord (_, []) => (CRecord (k2, []), loc) + | CRecord (_, (x, c) :: rest) => + hnormCon env + (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc), + (CApp (c1, (CRecord (k2, rest), loc)), loc)), loc) + | CConcat ((CRecord (k, (x, c) :: rest), _), rest') => + let + val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc) + in + hnormCon env + (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc), + (CApp (c1, rest''), loc)), loc) + end + | _ => + let + fun unconstraint c = + case hnormCon env c of + (CDisjoint (_, _, _, c), _) => unconstraint c + | c => c + + fun tryDistributivity () = + case hnormCon env c2 of + (CConcat (c1, c2'), _) => + let + val c = (CMap ks, loc) + val c = (CApp (c, f), loc) + + val c1 = (CApp (c, c1), loc) + val c2 = (CApp (c, c2'), loc) + val c = (CConcat (c1, c2), loc) + in + hnormCon env c + end + | _ => default () + + fun tryFusion () = + case #1 (hnormCon env c2) of + CApp (f', r') => + (case #1 (hnormCon env f') of + CApp (f', inner_f) => + (case #1 (hnormCon env f') of + CMap (dom, _) => + let + val f' = (CApp (inner_f, (CRel 0, loc)), loc) + val f' = (CApp (f, f'), loc) + val f' = (CAbs ("v", dom, f'), loc) + + val c = (CMap (dom, k2), loc) + val c = (CApp (c, f'), loc) + val c = (CApp (c, r'), loc) + in + hnormCon env c + end + | _ => tryDistributivity ()) + | _ => tryDistributivity ()) + | _ => tryDistributivity () + + fun tryIdentity () = + let + fun cunif () = + let + val r = ref NONE + in + (r, (CUnif (loc, (KType, loc), "_", r), loc)) + end + + val (vR, v) = cunif () + + val c = (CApp (f, v), loc) + in + case unconstraint c of + (CUnif (_, _, _, vR'), _) => + if vR' = vR then + hnormCon env c2 + else + tryFusion () + | _ => tryFusion () + end + in + tryIdentity () + end) | _ => default () end | c1' => (CApp ((c1', loc), hnormCon env c2), loc)) - + | CConcat (c1, c2) => (case (hnormCon env c1, hnormCon env c2) of ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => -- cgit v1.2.3