Mercurial > urweb

comparison src/corify.sml @ 194:df5fd8f6913a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A multi-parameter datatype all the way through
author Adam Chlipala <adamc@hcoop.net>
date Sat, 09 Aug 2008 08:47:36 -0400
parents 8a70e2919e86
children ab86aa858e6c
comparison
equal deleted inserted replaced
193:8a70e2919e86 194:df5fd8f6913a
532 ((x, n, co), st) 532 ((x, n, co), st)
533 end) st xncs 533 end) st xncs
534 534
535 val dk = CoreUtil.classifyDatatype xncs 535 val dk = CoreUtil.classifyDatatype xncs
536 val t = (L'.CNamed n, loc) 536 val t = (L'.CNamed n, loc)
537 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel i, loc)), loc)) t xs 537 val nxs = length xs - 1
538 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
538 val k = (L'.KType, loc) 539 val k = (L'.KType, loc)
539 val dcons = map (fn (x, n, to) => 540 val dcons = map (fn (x, n, to) =>
540 let 541 let
541 val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs 542 val args = ListUtil.mapi (fn (i, _) => (L'.CRel (nxs - i), loc)) xs
542 val (e, t) = 543 val (e, t) =
543 case to of 544 case to of
544 NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t) 545 NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t)
545 | SOME t' => ((L'.EAbs ("x", t', t, 546 | SOME t' => ((L'.EAbs ("x", t', t,
546 (L'.ECon (dk, L'.PConVar n, args, 547 (L'.ECon (dk, L'.PConVar n, args,
573 val co = Option.map (corifyCon st) co 574 val co = Option.map (corifyCon st) co
574 in 575 in
575 ((x, n, co), st) 576 ((x, n, co), st)
576 end) st xncs 577 end) st xncs
577 578
578 val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel i, loc)), loc)) c xs 579 val nxs = length xs - 1
580 val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel (nxs - i), loc)), loc)) c xs
579 val k = (L'.KType, loc) 581 val k = (L'.KType, loc)
580 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs 582 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
581 583
582 val cds = map (fn (x, n, co) => 584 val cds = map (fn (x, n, co) =>
583 let 585 let