Mercurial > urweb
diff src/elab_ops.sml @ 339:075b36dbb1a4
Crud supports INSERT
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 14 Sep 2008 15:10:04 -0400 |
parents | eec65c11d3e2 |
children | b85e6ba56618 |
line wrap: on
line diff
--- a/src/elab_ops.sml Sun Sep 14 11:02:18 2008 -0400 +++ b/src/elab_ops.sml Sun Sep 14 15:10:04 2008 -0400 @@ -149,6 +149,72 @@ (CDisjoint (_, _, c), _) => unconstraint c | c => c val c = unconstraint c + + 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 + default () + | _ => default ()) + | _ => default ()) + | _ => default () + end + | _ => default ()) + | _ => default ()) + | _ => default ()) + | _ => default () + end in (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*) case (hnormCon env i, unconstraint c) of @@ -163,10 +229,10 @@ if nmR' = nmR andalso vR' = vR andalso rR' = rR then hnormCon env c2 else - default () - | _ => default ()) - | _ => default ()) - | _ => default () + tryFusion () + | _ => tryFusion ()) + | _ => tryFusion ()) + | _ => tryFusion () end) | _ => default ()) | _ => default ()