Mercurial > urweb
comparison src/termination.sml @ 623:588b9d16b00a
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 22 Feb 2009 16:10:25 -0500 |
parents | ae03d09043c1 |
children | 7f871c03e3a1 |
comparison
equal
deleted
inserted
replaced
622:d64533157f40 | 623:588b9d16b00a |
---|---|
188 | Subarg _ => Rabble | 188 | Subarg _ => Rabble |
189 | Func _ => Rabble | 189 | Func _ => Rabble |
190 in | 190 in |
191 (p, ps, calls) | 191 (p, ps, calls) |
192 end | 192 end |
193 | EKApp (e, _) => combiner calls e | |
193 | _ => | 194 | _ => |
194 let | 195 let |
195 val (p, calls) = exp parent (penv, calls) e | 196 val (p, calls) = exp parent (penv, calls) e |
196 in | 197 in |
197 (*Print.prefaces "Head" [("e", ElabPrint.p_exp env e)]; | 198 (*Print.prefaces "Head" [("e", ElabPrint.p_exp env e)]; |
237 let | 238 let |
238 val (_, calls) = exp parent (penv, calls) e | 239 val (_, calls) = exp parent (penv, calls) e |
239 in | 240 in |
240 (Rabble, calls) | 241 (Rabble, calls) |
241 end | 242 end |
243 | EKApp _ => apps () | |
244 | EKAbs (_, e) => | |
245 let | |
246 val (_, calls) = exp parent (penv, calls) e | |
247 in | |
248 (Rabble, calls) | |
249 end | |
242 | 250 |
243 | ERecord xets => | 251 | ERecord xets => |
244 let | 252 let |
245 val calls = foldl (fn ((_, e, _), calls) => #2 (exp parent (penv, calls) e)) calls xets | 253 val calls = foldl (fn ((_, e, _), calls) => #2 (exp parent (penv, calls) e)) calls xets |
246 in | 254 in |
276 val (_, calls) = exp parent (penv, calls) e1 | 284 val (_, calls) = exp parent (penv, calls) e1 |
277 val (_, calls) = exp parent (penv, calls) e2 | 285 val (_, calls) = exp parent (penv, calls) e2 |
278 in | 286 in |
279 (Rabble, calls) | 287 (Rabble, calls) |
280 end | 288 end |
281 | EFold _ => (Rabble, calls) | |
282 | 289 |
283 | ECase (e, pes, _) => | 290 | ECase (e, pes, _) => |
284 let | 291 let |
285 val (p, calls) = exp parent (penv, calls) e | 292 val (p, calls) = exp parent (penv, calls) e |
286 | 293 |