Mercurial > urweb

comparison src/elaborate.sml @ 161:a5ae7b3e37a4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Normalize datatype choice during SgiDatatypeImp elaboration
author Adam Chlipala <adamc@hcoop.net>
date Thu, 24 Jul 2008 16:51:24 -0400
parents 870e8abbe3b9
children 06a98129b23f
comparison
equal deleted inserted replaced
160:870e8abbe3b9 161:a5ae7b3e37a4
1335 NONE => (conError env (UnboundStrInCon (loc, m)); 1335 NONE => (conError env (UnboundStrInCon (loc, m));
1336 (strerror, sgnerror)) 1336 (strerror, sgnerror))
1337 | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) 1337 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
1338 ((L'.StrVar n, loc), sgn) ms 1338 ((L'.StrVar n, loc), sgn) ms
1339 in 1339 in
1340 case E.projectDatatype env {sgn = sgn, str = str, field = s} of 1340 case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
1341 NONE => (conError env (UnboundDatatype (loc, s)); 1341 ((L'.CModProj (n, ms, s), _), gs) =>
1342 ([], (env, denv, gs))) 1342 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
1343 | SOME xncs => 1343 NONE => (conError env (UnboundDatatype (loc, s));
1344 let 1344 ([], (env, denv, gs)))
1345 val k = (L'.KType, loc) 1345 | SOME xncs =>
1346 val t = (L'.CModProj (n, ms, s), loc) 1346 let
1347 val (env, n') = E.pushCNamed env x k (SOME t) 1347 val k = (L'.KType, loc)
1348 val env = E.pushDatatype env n' xncs 1348 val t = (L'.CModProj (n, ms, s), loc)
1349 1349 val (env, n') = E.pushCNamed env x k (SOME t)
1350 val t = (L'.CNamed n', loc) 1350 val env = E.pushDatatype env n' xncs
1351 val env = foldl (fn ((x, n, to), env) => 1351
1352 let 1352 val t = (L'.CNamed n', loc)
1353 val t = case to of 1353 val env = foldl (fn ((x, n, to), env) =>
1354 NONE => t 1354 let
1355 | SOME t' => (L'.TFun (t', t), loc) 1355 val t = case to of
1356 in 1356 NONE => t
1357 E.pushENamedAs env x n t 1357 | SOME t' => (L'.TFun (t', t), loc)
1358 end) env xncs 1358 in
1359 in 1359 E.pushENamedAs env x n t
1360 ([(L'.SgiDatatypeImp (x, n', n, ms, s), loc)], (env, denv, [])) 1360 end) env xncs
1361 end 1361 in
1362 ([(L'.SgiDatatypeImp (x, n', n, ms, s), loc)], (env, denv, gs))
1363 end)
1364 | _ => (strError env (NotDatatype loc);
1365 ([], (env, denv, [])))
1362 end) 1366 end)
1363 1367
1364 | L.SgiVal (x, c) => 1368 | L.SgiVal (x, c) =>
1365 let 1369 let
1366 val (c', ck, gs') = elabCon (env, denv) c 1370 val (c', ck, gs') = elabCon (env, denv) c