Mercurial > urweb

comparison src/core_util.sml @ 192:9bbf4d383381

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parametrized datatypes through corify
author Adam Chlipala <adamc@hcoop.net>
date Fri, 08 Aug 2008 10:59:06 -0400
parents 8e9f97508f0d
children 8a70e2919e86
comparison
equal deleted inserted replaced
191:aa54250f58ac 192:9bbf4d383381
231 and mfe' ctx (eAll as (e, loc)) = 231 and mfe' ctx (eAll as (e, loc)) =
232 case e of 232 case e of
233 EPrim _ => S.return2 eAll 233 EPrim _ => S.return2 eAll
234 | ERel _ => S.return2 eAll 234 | ERel _ => S.return2 eAll
235 | ENamed _ => S.return2 eAll 235 | ENamed _ => S.return2 eAll
236 | ECon (_, _, NONE) => S.return2 eAll 236 | ECon (dk, pc, cs, NONE) =>
237 | ECon (dk, n, SOME e) => 237 S.map2 (ListUtil.mapfold (mfc ctx) cs,
238 S.map2 (mfe ctx e, 238 fn cs' =>
239 fn e' => 239 (ECon (dk, pc, cs', NONE), loc))
240 (ECon (dk, n, SOME e'), loc)) 240 | ECon (dk, n, cs, SOME e) =>
241 S.bind2 (mfe ctx e,
242 fn e' =>
243 S.map2 (ListUtil.mapfold (mfc ctx) cs,
244 fn cs' =>
245 (ECon (dk, n, cs', SOME e'), loc)))
241 | EFfi _ => S.return2 eAll 246 | EFfi _ => S.return2 eAll
242 | EFfiApp (m, x, es) => 247 | EFfiApp (m, x, es) =>
243 S.map2 (ListUtil.mapfold (fn e => mfe ctx e) es, 248 S.map2 (ListUtil.mapfold (mfe ctx) es,
244 fn es' => 249 fn es' =>
245 (EFfiApp (m, x, es'), loc)) 250 (EFfiApp (m, x, es'), loc))
246 | EApp (e1, e2) => 251 | EApp (e1, e2) =>
247 S.bind2 (mfe ctx e1, 252 S.bind2 (mfe ctx e1,
248 fn e1' => 253 fn e1' =>
412 S.bind2 (mfk k, 417 S.bind2 (mfk k,
413 fn k' => 418 fn k' =>
414 S.map2 (mfc ctx c, 419 S.map2 (mfc ctx c,
415 fn c' => 420 fn c' =>
416 (DCon (x, n, k', c'), loc))) 421 (DCon (x, n, k', c'), loc)))
417 | DDatatype (x, n, xncs) => 422 | DDatatype (x, n, xs, xncs) =>
418 S.map2 (ListUtil.mapfold (fn (x, n, c) => 423 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
419 case c of 424 case c of
420 NONE => S.return2 (x, n, c) 425 NONE => S.return2 (x, n, c)
421 | SOME c => 426 | SOME c =>
422 S.map2 (mfc ctx c, 427 S.map2 (mfc ctx c,
423 fn c' => (x, n, SOME c'))) xncs, 428 fn c' => (x, n, SOME c'))) xncs,
424 fn xncs' => 429 fn xncs' =>
425 (DDatatype (x, n, xncs'), loc)) 430 (DDatatype (x, n, xs, xncs'), loc))
426 | DVal vi => 431 | DVal vi =>
427 S.map2 (mfvi ctx vi, 432 S.map2 (mfvi ctx vi,
428 fn vi' => 433 fn vi' =>
429 (DVal vi', loc)) 434 (DVal vi', loc))
430 | DValRec vis => 435 | DValRec vis =>
489 fn d' => 494 fn d' =>
490 let 495 let
491 val ctx' = 496 val ctx' =
492 case #1 d' of 497 case #1 d' of
493 DCon (x, n, k, c) => bind (ctx, NamedC (x, n, k, SOME c)) 498 DCon (x, n, k, c) => bind (ctx, NamedC (x, n, k, SOME c))
494 | DDatatype (x, n, xncs) => 499 | DDatatype (x, n, xs, xncs) =>
495 let 500 let
496 val ctx = bind (ctx, NamedC (x, n, (KType, #2 d'), NONE)) 501 val loc = #2 d'
502 val k = (KType, loc)
503 val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
504
505 val ctx = bind (ctx, NamedC (x, n, k', NONE))
497 val t = (CNamed n, #2 d') 506 val t = (CNamed n, #2 d')
507 val t = ListUtil.foldli (fn (i, _, t) => (CApp (t, (CRel i, loc)), loc))
508 t xs
498 in 509 in
499 foldl (fn ((x, n, to), ctx) => 510 foldl (fn ((x, n, to), ctx) =>
500 let 511 let
501 val t = case to of 512 val t = case to of
502 NONE => t 513 NONE => t
503 | SOME t' => (TFun (t', t), #2 d') 514 | SOME t' => (TFun (t', t), #2 d')
515 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc))
516 t xs
504 in 517 in
505 bind (ctx, NamedE (x, n, t, NONE, "")) 518 bind (ctx, NamedE (x, n, t, NONE, ""))
506 end) 519 end)
507 ctx xncs 520 ctx xncs
508 end 521 end
553 | S.Return _ => raise Fail "CoreUtil.File.foldMap: Impossible" 566 | S.Return _ => raise Fail "CoreUtil.File.foldMap: Impossible"
554 567
555 val maxName = foldl (fn ((d, _) : decl, count) => 568 val maxName = foldl (fn ((d, _) : decl, count) =>
556 case d of 569 case d of
557 DCon (_, n, _, _) => Int.max (n, count) 570 DCon (_, n, _, _) => Int.max (n, count)
558 | DDatatype (_, n, _) => Int.max (n, count) 571 | DDatatype (_, n, _, _) => Int.max (n, count)
559 | DVal (_, n, _, _, _) => Int.max (n, count) 572 | DVal (_, n, _, _, _) => Int.max (n, count)
560 | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis 573 | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis
561 | DExport _ => count) 0 574 | DExport _ => count) 0
562 575
563 end 576 end