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) =