Mercurial > urweb

comparison src/elaborate.sml @ 35:1dfbd9e3e790

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proper selfification
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Jun 2008 17:08:28 -0400
parents 44b5405e74c7
children e3d3c2791105
comparison
equal deleted inserted replaced
34:44b5405e74c7 35:1dfbd9e3e790
1103 L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc) 1103 L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc)
1104 | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc) 1104 | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc)
1105 | L'.DSgn _ => NONE 1105 | L'.DSgn _ => NONE
1106 | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc) 1106 | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc)
1107 1107
1108 fun subSgn env (all1 as (sgn1, _)) (all2 as (sgn2, loc2)) = 1108 fun hnormSgn env (all as (sgn, _)) =
1109 case (sgn1, sgn2) of 1109 case sgn of
1110 L'.SgnError => all
1111 | L'.SgnVar n => hnormSgn env (#2 (E.lookupSgnNamed env n))
1112 | L'.SgnConst _ => all
1113
1114 fun subSgn env sgn1 (sgn2 as (_, loc2)) =
1115 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
1110 (L'.SgnError, _) => () 1116 (L'.SgnError, _) => ()
1111 | (_, L'.SgnError) => () 1117 | (_, L'.SgnError) => ()
1112 1118
1113 | (L'.SgnVar n, _) => 1119 | (L'.SgnVar n, _) => raise Fail "subSgn: Variable remains"
1114 subSgn env (#2 (E.lookupSgnNamed env n)) all2 1120 | (_, L'.SgnVar n) => raise Fail "subSgn: Variable remains"
1115 | (_, L'.SgnVar n) =>
1116 subSgn env all1 (#2 (E.lookupSgnNamed env n))
1117 1121
1118 | (L'.SgnConst sgis1, L'.SgnConst sgis2) => 1122 | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
1119 let 1123 let
1120 fun folder (sgi2All as (sgi, _), env) = 1124 fun folder (sgi2All as (sgi, _), env) =
1121 let 1125 let
1193 end 1197 end
1194 in 1198 in
1195 ignore (foldl folder env sgis2) 1199 ignore (foldl folder env sgis2)
1196 end 1200 end
1197 1201
1202 fun selfify env {str, strs, sgn} =
1203 case #1 (hnormSgn env sgn) of
1204 L'.SgnError => sgn
1205 | L'.SgnVar _ => sgn
1206
1207 | L'.SgnConst sgis =>
1208 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
1209 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
1210 | (L'.SgiStr (x, n, sgn), loc) =>
1211 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
1212 | x => x) sgis), #2 sgn)
1213
1198 fun elabDecl ((d, loc), env) = 1214 fun elabDecl ((d, loc), env) =
1199 let 1215 let
1200 1216
1201 in 1217 in
1202 resetKunif (); 1218 resetKunif ();
1277 | L.DStr (x, sgno, str) => 1293 | L.DStr (x, sgno, str) =>
1278 let 1294 let
1279 val formal = Option.map (elabSgn env) sgno 1295 val formal = Option.map (elabSgn env) sgno
1280 val (str', actual) = elabStr env str 1296 val (str', actual) = elabStr env str
1281 1297
1298 fun self (str, _) =
1299 case str of
1300 L'.StrVar x => SOME (x, [])
1301 | L'.StrProj (str, x) =>
1302 (case self str of
1303 NONE => NONE
1304 | SOME (m, ms) => SOME (m, ms @ [x]))
1305 | _ => NONE
1306
1282 val sgn' = case formal of 1307 val sgn' = case formal of
1283 NONE => actual 1308 NONE =>
1309 (case self str' of
1310 NONE => actual
1311 | SOME (str, strs) => selfify env {sgn = actual, str = str, strs = strs})
1284 | SOME formal => 1312 | SOME formal =>
1285 (subSgn env actual formal; 1313 (subSgn env actual formal;
1286 formal) 1314 formal)
1287 1315
1288 val (env', n) = E.pushStrNamed env x sgn' 1316 val (env', n) = E.pushStrNamed env x sgn'