Mercurial > urweb
comparison src/elaborate.sml @ 46:44a1bc863f0f
Corifying functors
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 19 Jun 2008 17:55:36 -0400 |
parents | a9f3ce2d1b9b |
children | 0a5c312de09a |
comparison
equal
deleted
inserted
replaced
45:3c1ce1b4eb3d | 46:44a1bc863f0f |
---|---|
1013 ("Field", PD.string x)]) | 1013 ("Field", PD.string x)]) |
1014 | 1014 |
1015 datatype str_error = | 1015 datatype str_error = |
1016 UnboundStr of ErrorMsg.span * string | 1016 UnboundStr of ErrorMsg.span * string |
1017 | NotFunctor of L'.sgn | 1017 | NotFunctor of L'.sgn |
1018 | FunctorRebind of ErrorMsg.span | |
1018 | 1019 |
1019 fun strError env err = | 1020 fun strError env err = |
1020 case err of | 1021 case err of |
1021 UnboundStr (loc, s) => | 1022 UnboundStr (loc, s) => |
1022 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s) | 1023 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s) |
1023 | NotFunctor sgn => | 1024 | NotFunctor sgn => |
1024 (ErrorMsg.errorAt (#2 sgn) "Application of non-functor"; | 1025 (ErrorMsg.errorAt (#2 sgn) "Application of non-functor"; |
1025 eprefaces' [("Signature", p_sgn env sgn)]) | 1026 eprefaces' [("Signature", p_sgn env sgn)]) |
1027 | FunctorRebind loc => | |
1028 ErrorMsg.errorAt loc "Attempt to rebind functor" | |
1026 | 1029 |
1027 val hnormSgn = E.hnormSgn | 1030 val hnormSgn = E.hnormSgn |
1028 | 1031 |
1029 fun elabSgn_item ((sgi, loc), env) = | 1032 fun elabSgn_item ((sgi, loc), env) = |
1030 let | 1033 let |
1389 (subSgn env actual formal; | 1392 (subSgn env actual formal; |
1390 formal) | 1393 formal) |
1391 | 1394 |
1392 val (env', n) = E.pushStrNamed env x sgn' | 1395 val (env', n) = E.pushStrNamed env x sgn' |
1393 in | 1396 in |
1397 case #1 (hnormSgn env sgn') of | |
1398 L'.SgnFun _ => | |
1399 (case #1 str' of | |
1400 L'.StrFun _ => () | |
1401 | _ => strError env (FunctorRebind loc)) | |
1402 | _ => (); | |
1403 | |
1394 ((L'.DStr (x, n, sgn', str'), loc), env') | 1404 ((L'.DStr (x, n, sgn', str'), loc), env') |
1395 end | 1405 end |
1396 end | 1406 end |
1397 | 1407 |
1398 and elabStr env (str, loc) = | 1408 and elabStr env (str, loc) = |