From 42944f71120301ea2dff0e93f3a0f2e7df4a44b0 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 11 Sep 2008 18:32:41 -0400 Subject: Crud list works --- src/elab_ops.sml | 60 ++++++++++++++++++++++++++++++-------------------------- 1 file changed, 32 insertions(+), 28 deletions(-) (limited to 'src/elab_ops.sml') diff --git a/src/elab_ops.sml b/src/elab_ops.sml index 50c95ac7..6c75768b 100644 --- a/src/elab_ops.sml +++ b/src/elab_ops.sml @@ -98,36 +98,40 @@ fun hnormCon env (cAll as (c, loc)) = ("sc", p_con env sc)];*) sc end - | CApp (c', i) => - (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), + | c1' as CApp (c', i) => + 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), + (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)*) - 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 - | _ => cAll) - | _ => cAll) - | _ => cAll) - | _ => cAll) + rest''), loc)), loc) + end + | _ => default ()) + | _ => default ()) + | _ => default () + end + | c1' => (CApp ((c1', loc), hnormCon env c2), loc)) | CConcat (c1, c2) => (case (hnormCon env c1, hnormCon env c2) of -- cgit v1.2.3