Mercurial > urweb

comparison src/elaborate.sml @ 1275:74150edf1134

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Undo fancy wildification; instead, client code should include extra wildcard con declarations
author Adam Chlipala <adamc@hcoop.net>
date Thu, 03 Jun 2010 14:44:08 -0400
parents 9fd0cb0ef6e1
children 1e6a4f9d3e4a
comparison
equal deleted inserted replaced
1274:38eb0d0f39b9 1275:74150edf1134
1653 | _ => NONE 1653 | _ => NONE
1654 in 1654 in
1655 findHead e 1655 findHead e
1656 end 1656 end
1657 1657
1658 datatype needed = Needed of {Cons : (string option * L'.kind * L'.con option) SM.map, 1658 datatype needed = Needed of {Cons : (L'.kind * L'.con option) SM.map,
1659 Constraints : (E.env * (L'.con * L'.con) * ErrorMsg.span) list, 1659 Constraints : (E.env * (L'.con * L'.con) * ErrorMsg.span) list,
1660 Vals : SS.set, 1660 Vals : SS.set,
1661 Mods : (E.env * needed) SM.map} 1661 Mods : (E.env * needed) SM.map}
1662 1662
1663 fun ncons (Needed r) = #Cons r 1663 fun ncons (Needed r) = #Cons r
3272 | L'.CUnif (_, _, _, ref (SOME c)) => decompileCon env c 3272 | L'.CUnif (_, _, _, ref (SOME c)) => decompileCon env c
3273 3273
3274 | _ => NONE 3274 | _ => NONE
3275 3275
3276 fun buildNeeded env sgis = 3276 fun buildNeeded env sgis =
3277 #1 (foldl (fn ((sgi, loc), (nd, env', lastCon)) => 3277 #1 (foldl (fn ((sgi, loc), (nd, env')) =>
3278 (case sgi of 3278 (case sgi of
3279 L'.SgiCon (x, _, k, c) => naddCon (nd, x, (lastCon, k, SOME c)) 3279 L'.SgiCon (x, _, k, c) => naddCon (nd, x, (k, SOME c))
3280 | L'.SgiConAbs (x, _, k) => naddCon (nd, x, (lastCon, k, NONE)) 3280 | L'.SgiConAbs (x, _, k) => naddCon (nd, x, (k, NONE))
3281 | L'.SgiConstraint cs => naddConstraint (nd, (env', cs, loc)) 3281 | L'.SgiConstraint cs => naddConstraint (nd, (env', cs, loc))
3282 | L'.SgiVal (x, _, t) => 3282 | L'.SgiVal (x, _, t) =>
3283 let 3283 let
3284 val t = normClassConstraint env' t 3284 val t = normClassConstraint env' t
3285 in 3285 in
3294 | L'.SgiStr (x, _, s) => 3294 | L'.SgiStr (x, _, s) =>
3295 (case #1 (hnormSgn env' s) of 3295 (case #1 (hnormSgn env' s) of
3296 L'.SgnConst sgis' => naddMod (nd, x, (env', buildNeeded env' sgis')) 3296 L'.SgnConst sgis' => naddMod (nd, x, (env', buildNeeded env' sgis'))
3297 | _ => nd) 3297 | _ => nd)
3298 | _ => nd, 3298 | _ => nd,
3299 E.sgiBinds env' (sgi, loc), 3299 E.sgiBinds env' (sgi, loc)))
3300 case cname sgi of 3300 (nempty, env) sgis)
3301 NONE => lastCon
3302 | v => v))
3303 (nempty, env, NONE) sgis)
3304 3301
3305 val nd = buildNeeded env sgis 3302 val nd = buildNeeded env sgis
3306 3303
3307 fun removeUsed (nd, ds) = 3304 fun removeUsed (nd, ds) =
3308 foldl (fn ((d, _), nd) => 3305 foldl (fn ((d, _), nd) =>
3337 val ds'' = map (fn x => (L.DVal (x, NONE, ewild), #2 str)) xs 3334 val ds'' = map (fn x => (L.DVal (x, NONE, ewild), #2 str)) xs
3338 in 3335 in
3339 ds'' @ ds' 3336 ds'' @ ds'
3340 end 3337 end
3341 3338
3342 val ds = ds @ ds' 3339 val ds' =
3343
3344 val ds =
3345 case SM.listItemsi (ncons nd) of 3340 case SM.listItemsi (ncons nd) of
3346 [] => ds 3341 [] => ds'
3347 | xs => 3342 | xs =>
3348 let 3343 map (fn (x, (k, co)) =>
3349 fun findPlace ((x, (lastCon, k, co)), ds') =
3350 let 3344 let
3351 val k = 3345 val k =
3352 case decompileKind k of 3346 case decompileKind k of
3353 NONE => (L.KWild, #2 str) 3347 NONE => (L.KWild, #2 str)
3354 | SOME k => k 3348 | SOME k => k
3355 3349
3356 val cwild = (L.CWild k, #2 str) 3350 val cwild = (L.CWild k, #2 str)
3357 val c = 3351 val c =
3358 case co of 3352 case co of
3359 NONE => cwild 3353 NONE => cwild
3360 | SOME c => 3354 | SOME c =>
3361 case decompileCon env c of 3355 case decompileCon env c of
3362 NONE => cwild 3356 NONE => cwild
3363 | SOME c' => c' 3357 | SOME c' => c'
3364
3365 val d = (L.DCon (x, NONE, c), #2 str)
3366 in 3358 in
3367 case lastCon of 3359 (L.DCon (x, NONE, c), #2 str)
3368 NONE => d :: ds' 3360 end) xs @ ds'
3369 | _ => 3361
3370 let 3362 val ds = ds @ ds'
3371 fun seek (ds'', passed) =
3372 case ds'' of
3373 [] => d :: ds'
3374 | d1 :: ds'' =>
3375 if dname d1 = lastCon then
3376 List.revAppend (passed, d1 :: d :: ds'')
3377 else
3378 seek (ds'', d1 :: passed)
3379 in
3380 seek (ds', [])
3381 end
3382 end
3383 in
3384 foldl findPlace ds xs
3385 end
3386 in 3363 in
3387 map (fn d as (L.DStr (x, s, (L.StrConst ds', loc')), loc) => 3364 map (fn d as (L.DStr (x, s, (L.StrConst ds', loc')), loc) =>
3388 (case SM.find (nmods nd, x) of 3365 (case SM.find (nmods nd, x) of
3389 NONE => d 3366 NONE => d
3390 | SOME (env, nd') => 3367 | SOME (env, nd') =>
4037 let 4014 let
4038 val (str1', sgn1, gs1) = elabStr (env, denv) str1 4015 val (str1', sgn1, gs1) = elabStr (env, denv) str1
4039 val str2 = 4016 val str2 =
4040 case sgn1 of 4017 case sgn1 of
4041 (L'.SgnFun (_, _, dom, _), _) => 4018 (L'.SgnFun (_, _, dom, _), _) =>
4042 wildifyStr env (str2, dom) 4019 let
4020 val s = wildifyStr env (str2, dom)
4021 in
4022 (*Print.preface ("Wild", SourcePrint.p_str s);*)
4023 s
4024 end
4043 | _ => str2 4025 | _ => str2
4044 val (str2', sgn2, gs2) = elabStr (env, denv) str2 4026 val (str2', sgn2, gs2) = elabStr (env, denv) str2
4045 in 4027 in
4046 case #1 (hnormSgn env sgn1) of 4028 case #1 (hnormSgn env sgn1) of
4047 L'.SgnError => (strerror, sgnerror, []) 4029 L'.SgnError => (strerror, sgnerror, [])