Mercurial > urweb

comparison src/elab_ops.sml @ 621:8998114760c1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
"Hello world" compiles, after replacing type-level fold with map
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 15:33:20 -0500
parents 11fc77fb8257
children 588b9d16b00a
comparison
equal deleted inserted replaced
620:d828b143e147 621:8998114760c1
112 ("cb", ElabPrint.p_con env' cb), 112 ("cb", ElabPrint.p_con env' cb),
113 ("c2", ElabPrint.p_con env c2), 113 ("c2", ElabPrint.p_con env c2),
114 ("sc", ElabPrint.p_con env sc)];*) 114 ("sc", ElabPrint.p_con env sc)];*)
115 sc 115 sc
116 end 116 end
117 | c1' as CApp (c', i) => 117 | c1' as CApp (c', f) =>
118 let 118 let
119 fun default () = (CApp ((c1', loc), hnormCon env c2), loc) 119 fun default () = (CApp ((c1', loc), hnormCon env c2), loc)
120 in 120 in
121 case #1 (hnormCon env c') of 121 case #1 (hnormCon env c') of
122 CApp (c', f) => 122 CMap (ks as (k1, k2)) =>
123 (case #1 (hnormCon env c') of 123 (case #1 (hnormCon env c2) of
124 CFold ks => 124 CRecord (_, []) => (CRecord (k2, []), loc)
125 (case #1 (hnormCon env c2) of 125 | CRecord (_, (x, c) :: rest) =>
126 CRecord (_, []) => hnormCon env i 126 hnormCon env
127 | CRecord (k, (x, c) :: rest) => 127 (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
128 hnormCon env 128 (CApp (c1, (CRecord (k2, rest), loc)), loc)), loc)
129 (CApp ((CApp ((CApp (f, x), loc), c), loc), 129 | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
130 (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), 130 let
131 (CRecord (k, rest), loc)), loc)), loc) 131 val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
132 | CConcat ((CRecord (k, (x, c) :: rest), _), rest') => 132 in
133 let 133 hnormCon env
134 val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc) 134 (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
135 135 (CApp (c1, rest''), loc)), loc)
136 (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc), 136 end
137 (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), 137 | _ =>
138 rest''), loc)), loc)*) 138 let
139 in 139 fun unconstraint c =
140 (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*) 140 case hnormCon env c of
141 hnormCon env 141 (CDisjoint (_, _, _, c), _) => unconstraint c
142 (CApp ((CApp ((CApp (f, x), loc), c), loc), 142 | c => c
143 (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), 143
144 rest''), loc)), loc) 144 fun tryDistributivity () =
145 end 145 case hnormCon env c2 of
146 | _ => 146 (CConcat (c1, c2'), _) =>
147 let 147 let
148 fun cunif () = 148 val c = (CMap ks, loc)
149 let 149 val c = (CApp (c, f), loc)
150 val r = ref NONE 150
151 in 151 val c1 = (CApp (c, c1), loc)
152 (r, (CUnif (loc, (KType, loc), "_", r), loc)) 152 val c2 = (CApp (c, c2'), loc)
153 end 153 val c = (CConcat (c1, c2), loc)
154 154 in
155 val (nmR, nm) = cunif () 155 hnormCon env c
156 val (vR, v) = cunif () 156 end
157 val (rR, r) = cunif () 157 | _ => default ()
158 158
159 val c = f 159 fun tryFusion () =
160 val c = (CApp (c, nm), loc) 160 case #1 (hnormCon env c2) of
161 val c = (CApp (c, v), loc) 161 CApp (f', r') =>
162 val c = (CApp (c, r), loc) 162 (case #1 (hnormCon env f') of
163 fun unconstraint c = 163 CApp (f', inner_f) =>
164 case hnormCon env c of 164 (case #1 (hnormCon env f') of
165 (CDisjoint (_, _, _, c), _) => unconstraint c 165 CMap (dom, _) =>
166 | c => c 166 let
167 val c = unconstraint c 167 val f' = (CApp (inner_f, (CRel 0, loc)), loc)
168 168 val f' = (CApp (f, f'), loc)
169 fun tryDistributivity () = 169 val f' = (CAbs ("v", dom, f'), loc)
170 let 170
171 fun distribute (c1, c2) = 171 val c = (CMap (dom, k2), loc)
172 let 172 val c = (CApp (c, f'), loc)
173 val c = (CFold ks, loc) 173 val c = (CApp (c, r'), loc)
174 val c = (CApp (c, f), loc) 174 in
175 val c = (CApp (c, i), loc) 175 hnormCon env c
176 176 end
177 val c1 = (CApp (c, c1), loc) 177 | _ => tryDistributivity ())
178 val c2 = (CApp (c, c2), loc) 178 | _ => tryDistributivity ())
179 val c = (CConcat (c1, c2), loc) 179 | _ => tryDistributivity ()
180 in 180
181 hnormCon env c 181 fun tryIdentity () =
182 end 182 let
183 in 183 fun cunif () =
184 case (hnormCon env i, hnormCon env c2, hnormCon env c) of 184 let
185 ((CRecord (_, []), _), 185 val r = ref NONE
186 (CConcat (arg1, arg2), _), 186 in
187 (CConcat (c1, c2'), _)) => 187 (r, (CUnif (loc, (KType, loc), "_", r), loc))
188 (case (hnormCon env c1, hnormCon env c2') of 188 end
189 ((CRecord (_, [(nm', v')]), _), 189
190 (CUnif (_, _, _, rR'), _)) => 190 val (vR, v) = cunif ()
191 (case hnormCon env nm' of 191
192 (CUnif (_, _, _, nmR'), _) => 192 val c = (CApp (f, v), loc)
193 if nmR' = nmR andalso rR' = rR then 193 in
194 distribute (arg1, arg2) 194 case unconstraint c of
195 else 195 (CUnif (_, _, _, vR'), _) =>
196 default () 196 if vR' = vR then
197 | _ => default ()) 197 hnormCon env c2
198 | _ => default ()) 198 else
199 | _ => default () 199 tryFusion ()
200 end 200 | _ => tryFusion ()
201 201 end
202 fun tryFusion () = 202 in
203 let 203 tryIdentity ()
204 fun fuse (dom, new_v, r') = 204 end)
205 let
206 val ran = #2 ks
207
208 val f = (CApp (f, (CRel 2, loc)), loc)
209 val f = (CApp (f, new_v), loc)
210 val f = (CApp (f, (CRel 0, loc)), loc)
211 val f = (CAbs ("acc", ran, f), loc)
212 val f = (CAbs ("v", dom, f), loc)
213 val f = (CAbs ("nm", (KName, loc), f), loc)
214
215 val c = (CFold (dom, ran), loc)
216 val c = (CApp (c, f), loc)
217 val c = (CApp (c, i), loc)
218 val c = (CApp (c, r'), loc)
219 in
220 hnormCon env c
221 end
222 in
223 case #1 (hnormCon env c2) of
224 CApp (f, r') =>
225 (case #1 (hnormCon env f) of
226 CApp (f, inner_i) =>
227 (case (#1 (hnormCon env f), #1 (hnormCon env inner_i)) of
228 (CApp (f, inner_f), CRecord (_, [])) =>
229 (case #1 (hnormCon env f) of
230 CFold (dom, _) =>
231 let
232 val c = inner_f
233 val c = (CApp (c, nm), loc)
234 val c = (CApp (c, v), loc)
235 val c = (CApp (c, r), loc)
236 val c = unconstraint c
237
238 (*val () = Print.prefaces "Onto something!"
239 [("c", ElabPrint.p_con env cAll),
240 ("c'", ElabPrint.p_con env c)]*)
241
242 in
243 case #1 (hnormCon env c) of
244 CConcat (first, rest) =>
245 (case (#1 (hnormCon env first),
246 #1 (hnormCon env rest)) of
247 (CRecord (_, [(nm', v')]),
248 CUnif (_, _, _, rR')) =>
249 (case #1 (hnormCon env nm') of
250 CUnif (_, _, _, nmR') =>
251 if rR' = rR andalso nmR' = nmR then
252 (nmR := SOME (CRel 2, loc);
253 vR := SOME (CRel 1, loc);
254 rR := SOME (CError, loc);
255 fuse (dom, v', r'))
256 else
257 tryDistributivity ()
258 | _ => tryDistributivity ())
259 | _ => tryDistributivity ())
260 | _ => tryDistributivity ()
261 end
262 | _ => tryDistributivity ())
263 | _ => tryDistributivity ())
264 | _ => tryDistributivity ())
265 | _ => tryDistributivity ()
266 end
267
268 in
269 (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*)
270 case (hnormCon env i, unconstraint c) of
271 ((CRecord (_, []), _),
272 (CConcat (c1, c2'), _)) =>
273 (case (hnormCon env c1, hnormCon env c2') of
274 ((CRecord (_, [(nm', v')]), _),
275 (CUnif (_, _, _, rR'), _)) =>
276 (case (hnormCon env nm', hnormCon env v') of
277 ((CUnif (_, _, _, nmR'), _),
278 (CUnif (_, _, _, vR'), _)) =>
279 if nmR' = nmR andalso vR' = vR andalso rR' = rR then
280 hnormCon env c2
281 else
282 tryFusion ()
283 | _ => tryFusion ())
284 | _ => tryFusion ())
285 | _ => tryFusion ()
286 end)
287 | _ => default ())
288 | _ => default () 205 | _ => default ()
289 end 206 end
290 | c1' => (CApp ((c1', loc), hnormCon env c2), loc)) 207 | c1' => (CApp ((c1', loc), hnormCon env c2), loc))
291 208
292 | CConcat (c1, c2) => 209 | CConcat (c1, c2) =>
293 (case (hnormCon env c1, hnormCon env c2) of 210 (case (hnormCon env c1, hnormCon env c2) of
294 ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => 211 ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) =>
295 (CRecord (k, xcs1 @ xcs2), loc) 212 (CRecord (k, xcs1 @ xcs2), loc)
296 | ((CRecord (_, []), _), c2') => c2' 213 | ((CRecord (_, []), _), c2') => c2'