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