comparison src/elab_env.sml @ 186:88d46972de53

bool in Basis
author Adam Chlipala <adamc@hcoop.net>
date Sun, 03 Aug 2008 18:53:20 -0400
parents 7ee424760d2f
children 8e9f97508f0d
comparison
equal deleted inserted replaced
185:19ee24bffbc0 186:88d46972de53
646 case d of 646 case d of
647 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) 647 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
648 | DDatatype (x, n, xncs) => 648 | DDatatype (x, n, xncs) =>
649 let 649 let
650 val env = pushCNamedAs env x n (KType, loc) NONE 650 val env = pushCNamedAs env x n (KType, loc) NONE
651 val env = pushDatatype env n xncs
651 in 652 in
652 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc) 653 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc)
653 | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc)) 654 | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc))
654 env xncs 655 env xncs
655 end 656 end
656 | DDatatypeImp (x, n, m, ms, x', xncs) => 657 | DDatatypeImp (x, n, m, ms, x', xncs) =>
657 let 658 let
658 val t = (CModProj (m, ms, x'), loc) 659 val t = (CModProj (m, ms, x'), loc)
659 val env = pushCNamedAs env x n (KType, loc) (SOME t) 660 val env = pushCNamedAs env x n (KType, loc) (SOME t)
661 val env = pushDatatype env n xncs
660 662
661 val t = (CNamed n, loc) 663 val t = (CNamed n, loc)
662 in 664 in
663 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' t 665 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' t
664 | ((x', n', SOME t'), env) => pushENamedAs env x' n' (TFun (t', t), loc)) 666 | ((x', n', SOME t'), env) => pushENamedAs env x' n' (TFun (t', t), loc))