Mercurial > urweb

comparison src/corify.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 aa54250f58ac
children 8a70e2919e86
comparison
equal deleted inserted replaced
191:aa54250f58ac 192:9bbf4d383381
60 60
61 val debug : t -> unit 61 val debug : t -> unit
62 62
63 val enter : t -> t 63 val enter : t -> t
64 val leave : t -> {outer : t, inner : t} 64 val leave : t -> {outer : t, inner : t}
65 val ffi : string -> L'.con SM.map -> (string * L'.con option * L'.datatype_kind) SM.map -> t 65 val ffi : string -> L'.con SM.map -> (string * string list * L'.con option * L'.datatype_kind) SM.map -> t
66 66
67 datatype core_con = 67 datatype core_con =
68 CNormal of int 68 CNormal of int
69 | CFfi of string 69 | CFfi of string
70 val bindCon : t -> string -> int -> t * int 70 val bindCon : t -> string -> int -> t * int
99 vals : int SM.map, 99 vals : int SM.map,
100 strs : flattening SM.map, 100 strs : flattening SM.map,
101 funs : (string * int * L.str) SM.map} 101 funs : (string * int * L.str) SM.map}
102 | FFfi of {mod : string, 102 | FFfi of {mod : string,
103 vals : L'.con SM.map, 103 vals : L'.con SM.map,
104 constructors : (string * L'.con option * L'.datatype_kind) SM.map} 104 constructors : (string * string list * L'.con option * L'.datatype_kind) SM.map}
105 105
106 type t = { 106 type t = {
107 cons : int IM.map, 107 cons : int IM.map,
108 constructors : L'.patCon IM.map, 108 constructors : L'.patCon IM.map,
109 vals : int IM.map, 109 vals : int IM.map,
261 fun lookupConstructorByNameOpt ({current, ...} : t) x = 261 fun lookupConstructorByNameOpt ({current, ...} : t) x =
262 case current of 262 case current of
263 FFfi {mod = m, constructors, ...} => 263 FFfi {mod = m, constructors, ...} =>
264 (case SM.find (constructors, x) of 264 (case SM.find (constructors, x) of
265 NONE => NONE 265 NONE => NONE
266 | SOME (n, to, dk) => SOME (L'.PConFfi {mod = m, datatyp = n, con = x, arg = to, kind = dk})) 266 | SOME (n, xs, to, dk) => SOME (L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk}))
267 | FNormal {constructors, ...} => 267 | FNormal {constructors, ...} =>
268 case SM.find (constructors, x) of 268 case SM.find (constructors, x) of
269 NONE => NONE 269 NONE => NONE
270 | SOME n => SOME n 270 | SOME n => SOME n
271 271
272 fun lookupConstructorByName ({current, ...} : t) x = 272 fun lookupConstructorByName ({current, ...} : t) x =
273 case current of 273 case current of
274 FFfi {mod = m, constructors, ...} => 274 FFfi {mod = m, constructors, ...} =>
275 (case SM.find (constructors, x) of 275 (case SM.find (constructors, x) of
276 NONE => raise Fail "Corify.St.lookupConstructorByName [1]" 276 NONE => raise Fail "Corify.St.lookupConstructorByName [1]"
277 | SOME (n, to, dk) => L'.PConFfi {mod = m, datatyp = n, con = x, arg = to, kind = dk}) 277 | SOME (n, xs, to, dk) => L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk})
278 | FNormal {constructors, ...} => 278 | FNormal {constructors, ...} =>
279 case SM.find (constructors, x) of 279 case SM.find (constructors, x) of
280 NONE => raise Fail "Corify.St.lookupConstructorByName [2]" 280 NONE => raise Fail "Corify.St.lookupConstructorByName [2]"
281 | SOME n => n 281 | SOME n => n
282 282
427 fun corifyPat st (p, loc) = 427 fun corifyPat st (p, loc) =
428 case p of 428 case p of
429 L.PWild => (L'.PWild, loc) 429 L.PWild => (L'.PWild, loc)
430 | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc) 430 | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc)
431 | L.PPrim p => (L'.PPrim p, loc) 431 | L.PPrim p => (L'.PPrim p, loc)
432 | L.PCon (dk, pc, ts, po) => raise Fail "Corify PCon" (*(L'.PCon (dk, corifyPatCon st pc, Option.map (corifyPat st) po), loc)*) 432 | L.PCon (dk, pc, ts, po) => (L'.PCon (dk, corifyPatCon st pc, map (corifyCon st) ts,
433 Option.map (corifyPat st) po), loc)
433 | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc) 434 | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc)
434 435
435 fun corifyExp st (e, loc) = 436 fun corifyExp st (e, loc) =
436 case e of 437 case e of
437 L.EPrim p => (L'.EPrim p, loc) 438 L.EPrim p => (L'.EPrim p, loc)
444 let 445 let
445 val st = St.lookupStrById st m 446 val st = St.lookupStrById st m
446 val st = foldl St.lookupStrByName st ms 447 val st = foldl St.lookupStrByName st ms
447 in 448 in
448 case St.lookupConstructorByNameOpt st x of 449 case St.lookupConstructorByNameOpt st x of
449 SOME (pc as L'.PConFfi {mod = m, datatyp, arg, kind, ...}) => 450 SOME (pc as L'.PConFfi {mod = m, datatyp, params, arg, kind, ...}) =>
450 (case arg of 451 let
451 NONE => (L'.ECon (kind, pc, NONE), loc) 452 val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) params
452 | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc), 453 val e = case arg of
453 (L'.ECon (kind, pc, SOME (L'.ERel 0, loc)), loc)), loc)) 454 NONE => (L'.ECon (kind, pc, args, NONE), loc)
455 | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc),
456 (L'.ECon (kind, pc, args, SOME (L'.ERel 0, loc)), loc)), loc)
457
458 val k = (L'.KType, loc)
459 in
460 foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e params
461 end
454 | _ => 462 | _ =>
455 case St.lookupValByName st x of 463 case St.lookupValByName st x of
456 St.ENormal n => (L'.ENamed n, loc) 464 St.ENormal n => (L'.ENamed n, loc)
457 | St.EFfi (m, t) => 465 | St.EFfi (m, t) =>
458 case t of 466 case t of
510 let 518 let
511 val (st, n) = St.bindCon st x n 519 val (st, n) = St.bindCon st x n
512 in 520 in
513 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) 521 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
514 end 522 end
515 | L.DDatatype (x, n, xs, xncs) => raise Fail "Corify DDatatype" 523 | L.DDatatype (x, n, xs, xncs) =>
516 (*let 524 let
517 val (st, n) = St.bindCon st x n 525 val (st, n) = St.bindCon st x n
518 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => 526 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
519 let 527 let
520 val st = St.bindConstructor st x n (L'.PConVar n) 528 val st = St.bindConstructor st x n (L'.PConVar n)
521 val st = St.bindConstructorVal st x n 529 val st = St.bindConstructorVal st x n
524 ((x, n, co), st) 532 ((x, n, co), st)
525 end) st xncs 533 end) st xncs
526 534
527 val dk = CoreUtil.classifyDatatype xncs 535 val dk = CoreUtil.classifyDatatype xncs
528 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
538 val k = (L'.KType, loc)
529 val dcons = map (fn (x, n, to) => 539 val dcons = map (fn (x, n, to) =>
530 let 540 let
541 val args = ListUtil.mapi (fn (i, _) => (L'.CRel n, loc)) xs
531 val (e, t) = 542 val (e, t) =
532 case to of 543 case to of
533 NONE => ((L'.ECon (dk, L'.PConVar n, NONE), loc), t) 544 NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE), loc), t)
534 | SOME t' => ((L'.EAbs ("x", t', t, 545 | SOME t' => ((L'.EAbs ("x", t', t,
535 (L'.ECon (dk, L'.PConVar n, SOME (L'.ERel 0, loc)), 546 (L'.ECon (dk, L'.PConVar n, args,
547 SOME (L'.ERel 0, loc)),
536 loc)), 548 loc)),
537 loc), 549 loc),
538 (L'.TFun (t', t), loc)) 550 (L'.TFun (t', t), loc))
551
552 val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
553 val e = foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
539 in 554 in
540 (L'.DVal (x, n, t, e, ""), loc) 555 (L'.DVal (x, n, t, e, ""), loc)
541 end) xncs 556 end) xncs
542 in 557 in
543 ((L'.DDatatype (x, n, xncs), loc) :: dcons, st) 558 ((L'.DDatatype (x, n, xs, xncs), loc) :: dcons, st)
544 end*) 559 end
545 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => raise Fail "Corify DDatatypeImp" 560 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
546 (*let 561 let
547 val (st, n) = St.bindCon st x n 562 val (st, n) = St.bindCon st x n
548 val c = corifyCon st (L.CModProj (m1, ms, s), loc) 563 val c = corifyCon st (L.CModProj (m1, ms, s), loc)
549 564
550 val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms 565 val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms
551 val (_, {inner, ...}) = corifyStr (m, st) 566 val (_, {inner, ...}) = corifyStr (m, st)
558 val co = Option.map (corifyCon st) co 573 val co = Option.map (corifyCon st) co
559 in 574 in
560 ((x, n, co), st) 575 ((x, n, co), st)
561 end) st xncs 576 end) st xncs
562 577
578 val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel i, loc)), loc)) c xs
579 val k = (L'.KType, loc)
580 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
581
563 val cds = map (fn (x, n, co) => 582 val cds = map (fn (x, n, co) =>
564 let 583 let
565 val t = case co of 584 val t = case co of
566 NONE => c 585 NONE => c
567 | SOME t' => (L'.TFun (t', c), loc) 586 | SOME t' => (L'.TFun (t', c), loc)
568 val e = corifyExp st (L.EModProj (m1, ms, x), loc) 587 val e = corifyExp st (L.EModProj (m1, ms, x), loc)
588
589 val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
569 in 590 in
570 (L'.DVal (x, n, t, e, x), loc) 591 (L'.DVal (x, n, t, e, x), loc)
571 end) xncs 592 end) xncs
572 in 593 in
573 ((L'.DCon (x, n, (L'.KType, loc), c), loc) :: cds, st) 594 ((L'.DCon (x, n, k', c), loc) :: cds, st)
574 end*) 595 end
575 | L.DVal (x, n, t, e) => 596 | L.DVal (x, n, t, e) =>
576 let 597 let
577 val (st, n) = St.bindVal st x n 598 val (st, n) = St.bindVal st x n
578 val s = 599 val s =
579 if String.isPrefix "wrap_" x then 600 if String.isPrefix "wrap_" x then
646 cmap, 667 cmap,
647 conmap, 668 conmap,
648 st) 669 st)
649 end 670 end
650 671
651 | L.SgiDatatype (x, n, xs, xnts) => raise Fail "Corify FFI SgiDatatype" 672 | L.SgiDatatype (x, n, xs, xnts) =>
652 (*let 673 let
674 val k = (L'.KType, loc)
653 val dk = ExplUtil.classifyDatatype xnts 675 val dk = ExplUtil.classifyDatatype xnts
654 val (st, n') = St.bindCon st x n 676 val (st, n') = St.bindCon st x n
655 val (xnts, (ds', st, cmap, conmap)) = 677 val (xnts, (ds', st, cmap, conmap)) =
656 ListUtil.foldlMap 678 ListUtil.foldlMap
657 (fn ((x', n, to), (ds', st, cmap, conmap)) => 679 (fn ((x', n, to), (ds', st, cmap, conmap)) =>
658 let 680 let
659 val dt = (L'.CNamed n', loc) 681 val dt = (L'.CNamed n', loc)
682 val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs
660 683
661 val to = Option.map (corifyCon st) to 684 val to = Option.map (corifyCon st) to
662 685
663 val pc = L'.PConFfi {mod = m, 686 val pc = L'.PConFfi {mod = m,
664 datatyp = x, 687 datatyp = x,
688 params = xs,
665 con = x', 689 con = x',
666 arg = to, 690 arg = to,
667 kind = dk} 691 kind = dk}
668 692
693 fun wrapT t =
694 foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
695 fun wrapE e =
696 foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
697
669 val (cmap, d) = 698 val (cmap, d) =
670 case to of 699 case to of
671 NONE => (SM.insert (cmap, x', dt), 700 NONE => (SM.insert (cmap, x', wrapT dt),
672 (L'.DVal (x', n, dt, 701 (L'.DVal (x', n, wrapT dt,
673 (L'.ECon (dk, pc, NONE), loc), 702 wrapE
703 (L'.ECon (dk, pc, args, NONE),
704 loc),
674 ""), loc)) 705 ""), loc))
675 | SOME t => 706 | SOME t =>
676 let 707 let
677 val tf = (L'.TFun (t, dt), loc) 708 val tf = (L'.TFun (t, dt), loc)
678 val d = (L'.DVal (x', n, tf, 709 val e = wrapE (L'.EAbs ("x", t, tf,
679 (L'.EAbs ("x", t, tf, 710 (L'.ECon (dk, pc, args,
680 (L'.ECon (dk, pc, 711 SOME (L'.ERel 0,
681 SOME (L'.ERel 0, 712 loc)),
682 loc)), 713 loc)), loc)
683 loc)), loc), ""), loc) 714 val d = (L'.DVal (x', n, wrapT tf,
715 e, ""), loc)
684 in 716 in
685 (SM.insert (cmap, x', tf), d) 717 (SM.insert (cmap, x', wrapT tf), d)
686 end 718 end
687 719
688 val st = St.bindConstructor st x' n pc 720 val st = St.bindConstructor st x' n pc
689 (*val st = St.bindConstructorVal st x' n*) 721
690 722 val conmap = SM.insert (conmap, x', (x, xs, to, dk))
691 val conmap = SM.insert (conmap, x', (x, to, dk))
692 in 723 in
693 ((x', n, to), 724 ((x', n, to),
694 (d :: ds', st, cmap, conmap)) 725 (d :: ds', st, cmap, conmap))
695 end) ([], st, cmap, conmap) xnts 726 end) ([], st, cmap, conmap) xnts
696 in 727 in
697 (ds' @ (L'.DDatatype (x, n', xnts), loc) :: ds, 728 (ds' @ (L'.DDatatype (x, n', xs, xnts), loc) :: ds,
698 cmap, 729 cmap,
699 conmap, 730 conmap,
700 st) 731 st)
701 end*) 732 end
702 733
703 | L.SgiVal (x, _, c) => 734 | L.SgiVal (x, _, c) =>
704 (ds, 735 (ds,
705 SM.insert (cmap, x, corifyCon st c), 736 SM.insert (cmap, x, corifyCon st c),
706 conmap, 737 conmap,