Mercurial > urweb
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)) |