diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-09-11 18:32:41 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-09-11 18:32:41 -0400 |
| commit | 42944f71120301ea2dff0e93f3a0f2e7df4a44b0 (patch) | |
| tree | 527e676197eaa7c1c4377678e5e6d9731fb11a98 /src/elab_ops.sml | |
| parent | 48b9d4dae3d1ca6ff39e71571a6db3a43497c9f9 (diff) | |
Crud list works
Diffstat (limited to 'src/elab_ops.sml')
| -rw-r--r-- | src/elab_ops.sml | 60 |
1 files changed, 32 insertions, 28 deletions
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 |