Mercurial > urweb

comparison src/elab_env.sml @ 191:aa54250f58ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parametrized datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Fri, 08 Aug 2008 10:28:32 -0400
parents 8e9f97508f0d
children dd82457fda82
comparison
equal deleted inserted replaced
190:3eb53c957d10 191:aa54250f58ac
71 datatype 'a var = 71 datatype 'a var =
72 NotBound 72 NotBound
73 | Rel of int * 'a 73 | Rel of int * 'a
74 | Named of int * 'a 74 | Named of int * 'a
75 75
76 type datatyp = (string * con option) IM.map 76 type datatyp = string list * (string * con option) IM.map
77 77
78 type env = { 78 type env = {
79 renameC : kind var' SM.map, 79 renameC : kind var' SM.map,
80 relC : (string * kind) list, 80 relC : (string * kind) list,
81 namedC : (string * kind * con option) IM.map, 81 namedC : (string * kind * con option) IM.map,
82 82
83 datatypes : datatyp IM.map, 83 datatypes : datatyp IM.map,
84 constructors : (datatype_kind * int * con option * int) SM.map, 84 constructors : (datatype_kind * int * string list * con option * int) SM.map,
85 85
86 renameE : con var' SM.map, 86 renameE : con var' SM.map,
87 relE : (string * con) list, 87 relE : (string * con) list,
88 namedE : (string * con) IM.map, 88 namedE : (string * con) IM.map,
89 89
186 case SM.find (#renameC env, x) of 186 case SM.find (#renameC env, x) of
187 NONE => NotBound 187 NONE => NotBound
188 | SOME (Rel' x) => Rel x 188 | SOME (Rel' x) => Rel x
189 | SOME (Named' x) => Named x 189 | SOME (Named' x) => Named x
190 190
191 fun pushDatatype (env : env) n xncs = 191 fun pushDatatype (env : env) n xs xncs =
192 let 192 let
193 val dk = U.classifyDatatype xncs 193 val dk = U.classifyDatatype xncs
194 in 194 in
195 {renameC = #renameC env, 195 {renameC = #renameC env,
196 relC = #relC env, 196 relC = #relC env,
197 namedC = #namedC env, 197 namedC = #namedC env,
198 198
199 datatypes = IM.insert (#datatypes env, n, 199 datatypes = IM.insert (#datatypes env, n,
200 foldl (fn ((x, n, to), cons) => 200 (xs, foldl (fn ((x, n, to), cons) =>
201 IM.insert (cons, n, (x, to))) IM.empty xncs), 201 IM.insert (cons, n, (x, to))) IM.empty xncs)),
202 constructors = foldl (fn ((x, n', to), cmap) => 202 constructors = foldl (fn ((x, n', to), cmap) =>
203 SM.insert (cmap, x, (dk, n', to, n))) 203 SM.insert (cmap, x, (dk, n', xs, to, n)))
204 (#constructors env) xncs, 204 (#constructors env) xncs,
205 205
206 renameE = #renameE env, 206 renameE = #renameE env,
207 relE = #relE env, 207 relE = #relE env,
208 namedE = #namedE env, 208 namedE = #namedE env,
217 fun lookupDatatype (env : env) n = 217 fun lookupDatatype (env : env) n =
218 case IM.find (#datatypes env, n) of 218 case IM.find (#datatypes env, n) of
219 NONE => raise UnboundNamed n 219 NONE => raise UnboundNamed n
220 | SOME x => x 220 | SOME x => x
221 221
222 fun lookupDatatypeConstructor dt n = 222 fun lookupDatatypeConstructor (_, dt) n =
223 case IM.find (dt, n) of 223 case IM.find (dt, n) of
224 NONE => raise UnboundNamed n 224 NONE => raise UnboundNamed n
225 | SOME x => x 225 | SOME x => x
226 226
227 fun lookupConstructor (env : env) s = SM.find (#constructors env, s) 227 fun lookupConstructor (env : env) s = SM.find (#constructors env, s)
228 228
229 fun constructors dt = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt 229 fun datatypeArgs (xs, _) = xs
230 fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt
230 231
231 fun pushERel (env : env) x t = 232 fun pushERel (env : env) x t =
232 let 233 let
233 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) 234 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
234 | x => x) (#renameE env) 235 | x => x) (#renameE env)
360 361
361 fun sgiBinds env (sgi, loc) = 362 fun sgiBinds env (sgi, loc) =
362 case sgi of 363 case sgi of
363 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE 364 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
364 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) 365 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
365 | SgiDatatype (x, n, xncs) => 366 | SgiDatatype (x, n, xs, xncs) =>
366 let 367 let
367 val env = pushCNamedAs env x n (KType, loc) NONE 368 val env = pushCNamedAs env x n (KType, loc) NONE
368 in 369 in
369 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc) 370 foldl (fn ((x', n', to), env) =>
370 | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc)) 371 let
372 val t =
373 case to of
374 NONE => (CNamed n, loc)
375 | SOME t => (TFun (t, (CNamed n, loc)), loc)
376
377 val k = (KType, loc)
378 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
379 in
380 pushENamedAs env x' n' t
381 end)
371 env xncs 382 env xncs
372 end 383 end
373 | SgiDatatypeImp (x, n, m1, ms, x', xncs) => 384 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
374 let 385 let
375 val env = pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc)) 386 val env = pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc))
376 in 387 in
377 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc) 388 foldl (fn ((x', n', to), env) =>
378 | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc)) 389 let
390 val t =
391 case to of
392 NONE => (CNamed n, loc)
393 | SOME t => (TFun (t, (CNamed n, loc)), loc)
394
395 val k = (KType, loc)
396 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
397 in
398 pushENamedAs env x' n' t
399 end)
379 env xncs 400 env xncs
380 end 401 end
381 | SgiVal (x, n, t) => pushENamedAs env x n t 402 | SgiVal (x, n, t) => pushENamedAs env x n t
382 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn 403 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
383 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn 404 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
392 case f sgi of 413 case f sgi of
393 SOME v => 414 SOME v =>
394 let 415 let
395 val cons = 416 val cons =
396 case sgi of 417 case sgi of
397 SgiDatatype (x, n, _) => IM.insert (cons, n, x) 418 SgiDatatype (x, n, _, _) => IM.insert (cons, n, x)
398 | SgiDatatypeImp (x, n, _, _, _, _) => IM.insert (cons, n, x) 419 | SgiDatatypeImp (x, n, _, _, _, _, _) => IM.insert (cons, n, x)
399 | _ => cons 420 | _ => cons
400 in 421 in
401 SOME (v, (sgns, strs, cons)) 422 SOME (v, (sgns, strs, cons))
402 end 423 end
403 | NONE => 424 | NONE =>
404 case sgi of 425 case sgi of
405 SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 426 SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
406 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 427 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
407 | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 428 | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
408 | SgiDatatypeImp (x, n, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) 429 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
409 | SgiVal _ => seek (sgis, sgns, strs, cons) 430 | SgiVal _ => seek (sgis, sgns, strs, cons)
410 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons) 431 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
411 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons) 432 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
412 | SgiConstraint _ => seek (sgis, sgns, strs, cons) 433 | SgiConstraint _ => seek (sgis, sgns, strs, cons)
413 in 434 in
550 fun projectCon env {sgn, str, field} = 571 fun projectCon env {sgn, str, field} =
551 case #1 (hnormSgn env sgn) of 572 case #1 (hnormSgn env sgn) of
552 SgnConst sgis => 573 SgnConst sgis =>
553 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE 574 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
554 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE 575 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
555 | SgiDatatype (x, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE 576 | SgiDatatype (x, _, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE
556 | SgiDatatypeImp (x, _, m1, ms, x', _) => 577 | SgiDatatypeImp (x, _, m1, ms, x', _, _) =>
557 if x = field then 578 if x = field then
558 SOME ((KType, #2 sgn), SOME (CModProj (m1, ms, x'), #2 sgn)) 579 SOME ((KType, #2 sgn), SOME (CModProj (m1, ms, x'), #2 sgn))
559 else 580 else
560 NONE 581 NONE
561 | _ => NONE) sgis of 582 | _ => NONE) sgis of
565 | _ => NONE 586 | _ => NONE
566 587
567 fun projectDatatype env {sgn, str, field} = 588 fun projectDatatype env {sgn, str, field} =
568 case #1 (hnormSgn env sgn) of 589 case #1 (hnormSgn env sgn) of
569 SgnConst sgis => 590 SgnConst sgis =>
570 (case sgnSeek (fn SgiDatatype (x, _, xncs) => if x = field then SOME xncs else NONE 591 (case sgnSeek (fn SgiDatatype (x, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE
571 | SgiDatatypeImp (x, _, _, _, _, xncs) => if x = field then SOME xncs else NONE 592 | SgiDatatypeImp (x, _, _, _, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE
572 | _ => NONE) sgis of 593 | _ => NONE) sgis of
573 NONE => NONE 594 NONE => NONE
574 | SOME (xncs, subs) => SOME (map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs)) 595 | SOME ((xs, xncs), subs) => SOME (xs,
596 map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs))
575 | _ => NONE 597 | _ => NONE
576 598
577 fun projectConstructor env {sgn, str, field} = 599 fun projectConstructor env {sgn, str, field} =
578 case #1 (hnormSgn env sgn) of 600 case #1 (hnormSgn env sgn) of
579 SgnConst sgis => 601 SgnConst sgis =>
580 let 602 let
581 fun consider (n, xncs) = 603 fun consider (n, xs, xncs) =
582 ListUtil.search (fn (x, n', to) => 604 ListUtil.search (fn (x, n', to) =>
583 if x <> field then 605 if x <> field then
584 NONE 606 NONE
585 else 607 else
586 SOME (U.classifyDatatype xncs, n', to, (CNamed n, #2 str))) xncs 608 SOME (U.classifyDatatype xncs, n', xs, to, (CNamed n, #2 str))) xncs
587 in 609 in
588 case sgnSeek (fn SgiDatatype (_, n, xncs) => consider (n, xncs) 610 case sgnSeek (fn SgiDatatype (_, n, xs, xncs) => consider (n, xs, xncs)
589 | SgiDatatypeImp (_, n, _, _, _, xncs) => consider (n, xncs) 611 | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => consider (n, xs, xncs)
590 | _ => NONE) sgis of 612 | _ => NONE) sgis of
591 NONE => NONE 613 NONE => NONE
592 | SOME ((dk, n, to, t), subs) => SOME (dk, n, Option.map (sgnSubCon (str, subs)) to, 614 | SOME ((dk, n, xs, to, t), subs) => SOME (dk, n, xs, Option.map (sgnSubCon (str, subs)) to,
593 sgnSubCon (str, subs) t) 615 sgnSubCon (str, subs) t)
594 end 616 end
595 | _ => NONE 617 | _ => NONE
596 618
597 fun projectVal env {sgn, str, field} = 619 fun projectVal env {sgn, str, field} =
598 case #1 (hnormSgn env sgn) of 620 case #1 (hnormSgn env sgn) of
599 SgnConst sgis => 621 SgnConst sgis =>
600 let 622 let
601 fun seek (n, xncs) = 623 fun seek (n, xs, xncs) =
602 ListUtil.search (fn (x, _, to) => 624 ListUtil.search (fn (x, _, to) =>
603 if x = field then 625 if x = field then
604 SOME (case to of 626 SOME (let
605 NONE => (CNamed n, #2 sgn) 627 val t =
606 | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn)) 628 case to of
629 NONE => (CNamed n, #2 sgn)
630 | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn)
631 val k = (KType, #2 sgn)
632 in
633 foldr (fn (x, t) => (TCFun (Explicit, x, k, t), #2 sgn))
634 t xs
635 end)
607 else 636 else
608 NONE) xncs 637 NONE) xncs
609 in 638 in
610 case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE 639 case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE
611 | SgiDatatype (_, n, xncs) => seek (n, xncs) 640 | SgiDatatype (_, n, xs, xncs) => seek (n, xs, xncs)
612 | SgiDatatypeImp (_, n, _, _, _, xncs) => seek (n, xncs) 641 | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => seek (n, xs, xncs)
613 | _ => NONE) sgis of 642 | _ => NONE) sgis of
614 NONE => NONE 643 NONE => NONE
615 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c) 644 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)
616 end 645 end
617 | SgnError => SOME (CError, ErrorMsg.dummySpan) 646 | SgnError => SOME (CError, ErrorMsg.dummySpan)
630 in 659 in
631 seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc) 660 seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc)
632 end 661 end
633 | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 662 | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
634 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 663 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
635 | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 664 | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
636 | SgiDatatypeImp (x, n, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 665 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
637 | SgiVal _ => seek (sgis, sgns, strs, cons, acc) 666 | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
638 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc) 667 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
639 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) 668 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
640 in 669 in
641 seek (sgis, IM.empty, IM.empty, IM.empty, []) 670 seek (sgis, IM.empty, IM.empty, IM.empty, [])
648 | _ => NONE 677 | _ => NONE
649 678
650 fun declBinds env (d, loc) = 679 fun declBinds env (d, loc) =
651 case d of 680 case d of
652 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) 681 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
653 | DDatatype (x, n, xncs) => 682 | DDatatype (x, n, xs, xncs) =>
654 let 683 let
655 val env = pushCNamedAs env x n (KType, loc) NONE 684 val env = pushCNamedAs env x n (KType, loc) NONE
656 val env = pushDatatype env n xncs 685 val env = pushDatatype env n xs xncs
657 in 686 in
658 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc) 687 foldl (fn ((x', n', to), env) =>
659 | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc)) 688 let
660 env xncs 689 val t =
690 case to of
691 NONE => (CNamed n, loc)
692 | SOME t => (TFun (t, (CNamed n, loc)), loc)
693 val k = (KType, loc)
694 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
695 in
696 pushENamedAs env x' n' t
697 end)
698 env xncs
661 end 699 end
662 | DDatatypeImp (x, n, m, ms, x', xncs) => 700 | DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
663 let 701 let
664 val t = (CModProj (m, ms, x'), loc) 702 val t = (CModProj (m, ms, x'), loc)
665 val env = pushCNamedAs env x n (KType, loc) (SOME t) 703 val env = pushCNamedAs env x n (KType, loc) (SOME t)
666 val env = pushDatatype env n xncs 704 val env = pushDatatype env n xs xncs
667 705
668 val t = (CNamed n, loc) 706 val t = (CNamed n, loc)
669 in 707 in
670 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' t 708 foldl (fn ((x', n', to), env) =>
671 | ((x', n', SOME t'), env) => pushENamedAs env x' n' (TFun (t', t), loc)) 709 let
672 env xncs 710 val t =
711 case to of
712 NONE => (CNamed n, loc)
713 | SOME t => (TFun (t, (CNamed n, loc)), loc)
714 val k = (KType, loc)
715 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
716 in
717 pushENamedAs env x' n' t
718 end)
719 env xncs
673 end 720 end
674 | DVal (x, n, t, _) => pushENamedAs env x n t 721 | DVal (x, n, t, _) => pushENamedAs env x n t
675 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis 722 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis
676 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn 723 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
677 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn 724 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn