Mercurial > urweb

comparison src/elab_ops.sml @ 326:950320f33232

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Crud list works
author Adam Chlipala <adamc@hcoop.net>
date Thu, 11 Sep 2008 18:32:41 -0400
parents 1487c712eb12
children 58f1260f293f
comparison
equal deleted inserted replaced
325:e457d8972ff1 326:950320f33232
96 ("cb", p_con env' cb), 96 ("cb", p_con env' cb),
97 ("c2", p_con env c2), 97 ("c2", p_con env c2),
98 ("sc", p_con env sc)];*) 98 ("sc", p_con env sc)];*)
99 sc 99 sc
100 end 100 end
101 | CApp (c', i) => 101 | c1' as CApp (c', i) =>
102 (case #1 (hnormCon env c') of 102 let
103 CApp (c', f) => 103 fun default () = (CApp ((c1', loc), hnormCon env c2), loc)
104 (case #1 (hnormCon env c') of 104 in
105 CFold ks => 105 case #1 (hnormCon env c') of
106 (case #1 (hnormCon env c2) of 106 CApp (c', f) =>
107 CRecord (_, []) => hnormCon env i 107 (case #1 (hnormCon env c') of
108 | CRecord (k, (x, c) :: rest) => 108 CFold ks =>
109 hnormCon env 109 (case #1 (hnormCon env c2) of
110 (CApp ((CApp ((CApp (f, x), loc), c), loc), 110 CRecord (_, []) => hnormCon env i
111 | CRecord (k, (x, c) :: rest) =>
112 hnormCon env
113 (CApp ((CApp ((CApp (f, x), loc), c), loc),
111 (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), 114 (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
112 (CRecord (k, rest), loc)), loc)), loc) 115 (CRecord (k, rest), loc)), loc)), loc)
113 | CConcat ((CRecord (k, (x, c) :: rest), _), rest') => 116 | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
114 let 117 let
115 val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc) 118 val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
116 119
117 (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc), 120 (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc),
121 (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
122 rest''), loc)), loc)*)
123 in
124 (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*)
125 hnormCon env
126 (CApp ((CApp ((CApp (f, x), loc), c), loc),
118 (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), 127 (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
119 rest''), loc)), loc)*) 128 rest''), loc)), loc)
120 in 129 end
121 (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*) 130 | _ => default ())
122 hnormCon env 131 | _ => default ())
123 (CApp ((CApp ((CApp (f, x), loc), c), loc), 132 | _ => default ()
124 (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), 133 end
125 rest''), loc)), loc) 134 | c1' => (CApp ((c1', loc), hnormCon env c2), loc))
126 end
127 | _ => cAll)
128 | _ => cAll)
129 | _ => cAll)
130 | _ => cAll)
131 135
132 | CConcat (c1, c2) => 136 | CConcat (c1, c2) =>
133 (case (hnormCon env c1, hnormCon env c2) of 137 (case (hnormCon env c1, hnormCon env c2) of
134 ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => 138 ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) =>
135 (CRecord (k, xcs1 @ xcs2), loc) 139 (CRecord (k, xcs1 @ xcs2), loc)