Mercurial > urweb

comparison src/elaborate.sml @ 402:ebf27030ae3b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Recursive unurlify for Default datatypes
author Adam Chlipala <adamc@hcoop.net>
date Tue, 21 Oct 2008 15:11:42 -0400
parents 4d519baf357c
children 8084fa9216de
comparison
equal deleted inserted replaced
401:cc71fb7e5e54 402:ebf27030ae3b
1157 | Datatype _ => "Datatype" 1157 | Datatype _ => "Datatype"
1158 | Record _ => "Record" 1158 | Record _ => "Record"
1159 1159
1160 fun exhaustive (env, denv, t, ps) = 1160 fun exhaustive (env, denv, t, ps) =
1161 let 1161 let
1162 fun depth (p, _) =
1163 case p of
1164 L'.PWild => 0
1165 | L'.PVar _ => 0
1166 | L'.PPrim _ => 0
1167 | L'.PCon (_, _, _, NONE) => 1
1168 | L'.PCon (_, _, _, SOME p) => 1 + depth p
1169 | L'.PRecord xps => foldl (fn ((_, p, _), n) => Int.max (depth p, n)) 0 xps
1170
1171 val depth = 1 + foldl (fn (p, n) => Int.max (depth p, n)) 0 ps
1172
1162 fun pcCoverage pc = 1173 fun pcCoverage pc =
1163 case pc of 1174 case pc of
1164 L'.PConVar n => n 1175 L'.PConVar n => n
1165 | L'.PConProj (m1, ms, x) => 1176 | L'.PConProj (m1, ms, x) =>
1166 let 1177 let
1199 case ps of 1210 case ps of
1200 [] => raise Fail "Empty pattern list for coverage checking" 1211 [] => raise Fail "Empty pattern list for coverage checking"
1201 | [p] => coverage p 1212 | [p] => coverage p
1202 | p :: ps => merge (coverage p, combinedCoverage ps) 1213 | p :: ps => merge (coverage p, combinedCoverage ps)
1203 1214
1204 fun enumerateCases t = 1215 fun enumerateCases depth t =
1205 let 1216 if depth = 0 then
1206 fun dtype cons = 1217 [Wild]
1207 ListUtil.mapConcat (fn (_, n, to) => 1218 else
1208 case to of 1219 let
1209 NONE => [Datatype (IM.insert (IM.empty, n, Wild))] 1220 fun dtype cons =
1210 | SOME t => map (fn c => Datatype (IM.insert (IM.empty, n, c))) 1221 ListUtil.mapConcat (fn (_, n, to) =>
1211 (enumerateCases t)) cons 1222 case to of
1212 in 1223 NONE => [Datatype (IM.insert (IM.empty, n, Wild))]
1213 case #1 (#1 (hnormCon (env, denv) t)) of 1224 | SOME t => map (fn c => Datatype (IM.insert (IM.empty, n, c)))
1214 L'.CNamed n => 1225 (enumerateCases (depth-1) t)) cons
1215 (let 1226 in
1216 val dt = E.lookupDatatype env n 1227 case #1 (#1 (hnormCon (env, denv) t)) of
1217 val cons = E.constructors dt 1228 L'.CNamed n =>
1218 in 1229 (let
1219 dtype cons 1230 val dt = E.lookupDatatype env n
1220 end handle E.UnboundNamed _ => [Wild]) 1231 val cons = E.constructors dt
1221 | L'.TRecord c =>
1222 (case #1 (#1 (hnormCon (env, denv) c)) of
1223 L'.CRecord (_, xts) =>
1224 let
1225 val xts = map (fn (x, t) => (#1 (hnormCon (env, denv) x), t)) xts
1226
1227 fun exponentiate fs =
1228 case fs of
1229 [] => [SM.empty]
1230 | ((L'.CName x, _), t) :: rest =>
1231 let
1232 val this = enumerateCases t
1233 val rest = exponentiate rest
1234 in
1235 ListUtil.mapConcat (fn fmap =>
1236 map (fn c => SM.insert (fmap, x, c)) this) rest
1237 end
1238 | _ => raise Fail "exponentiate: Not CName"
1239 in 1232 in
1240 if List.exists (fn ((L'.CName _, _), _) => false 1233 dtype cons
1241 | (c, _) => true) xts then 1234 end handle E.UnboundNamed _ => [Wild])
1242 [Wild] 1235 | L'.TRecord c =>
1243 else 1236 (case #1 (#1 (hnormCon (env, denv) c)) of
1244 map (fn ls => Record [ls]) (exponentiate xts) 1237 L'.CRecord (_, xts) =>
1245 end 1238 let
1246 | _ => [Wild]) 1239 val xts = map (fn (x, t) => (#1 (hnormCon (env, denv) x), t)) xts
1247 | _ => [Wild] 1240
1248 end 1241 fun exponentiate fs =
1242 case fs of
1243 [] => [SM.empty]
1244 | ((L'.CName x, _), t) :: rest =>
1245 let
1246 val this = enumerateCases depth t
1247 val rest = exponentiate rest
1248 in
1249 ListUtil.mapConcat (fn fmap =>
1250 map (fn c => SM.insert (fmap, x, c)) this) rest
1251 end
1252 | _ => raise Fail "exponentiate: Not CName"
1253 in
1254 if List.exists (fn ((L'.CName _, _), _) => false
1255 | (c, _) => true) xts then
1256 [Wild]
1257 else
1258 map (fn ls => Record [ls]) (exponentiate xts)
1259 end
1260 | _ => [Wild])
1261 | _ => [Wild]
1262 end
1249 1263
1250 fun coverageImp (c1, c2) = 1264 fun coverageImp (c1, c2) =
1251 let 1265 let
1252 val r = 1266 val r =
1253 case (c1, c2) of 1267 case (c1, c2) of
1329 | L'.CError => (true, gs) 1343 | L'.CError => (true, gs)
1330 | c => 1344 | c =>
1331 (prefaces "Not a datatype" [("c", p_con env (c, ErrorMsg.dummySpan))]; 1345 (prefaces "Not a datatype" [("c", p_con env (c, ErrorMsg.dummySpan))];
1332 raise Fail "isTotal: Not a datatype") 1346 raise Fail "isTotal: Not a datatype")
1333 end 1347 end
1334 | Record _ => (List.all (fn c2 => coverageImp (c, c2)) (enumerateCases t), []) 1348 | Record _ => (List.all (fn c2 => coverageImp (c, c2)) (enumerateCases depth t), [])
1335 in 1349 in
1336 isTotal (combinedCoverage ps, t) 1350 isTotal (combinedCoverage ps, t)
1337 end 1351 end
1338 1352
1339 fun unmodCon env (c, loc) = 1353 fun unmodCon env (c, loc) =
1638 else 1652 else
1639 expError env (Inexhaustive loc); 1653 expError env (Inexhaustive loc);
1640 1654
1641 ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, enD gs' @ gs) 1655 ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, enD gs' @ gs)
1642 end 1656 end
1643
1644 (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 r)*)
1645 in 1657 in
1646 (*prefaces "elabExp" [("e", SourcePrint.p_exp eAll), 1658 (*prefaces "/elabExp" [("e", SourcePrint.p_exp eAll)];*)
1647 ("|tcs|", PD.string (Int.toString (length tcs)))];*)
1648 r 1659 r
1649 end 1660 end
1650 1661
1651 val hnormSgn = E.hnormSgn 1662 val hnormSgn = E.hnormSgn
1652 1663