Mercurial > urweb

comparison src/elaborate.sml @ 1264:79b2bcac6200

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix bug in module path generation with module roots; push wildification through substructures
author Adam Chlipala <adamc@hcoop.net>
date Thu, 27 May 2010 10:56:52 -0400
parents 950d1e540df6
children 9f4b9315810d
comparison
equal deleted inserted replaced
1263:be2ef50780ed 1264:79b2bcac6200
1650 | L.ECApp (e, _) => findHead e 1650 | L.ECApp (e, _) => findHead e
1651 | L.EDisjointApp e => findHead e 1651 | L.EDisjointApp e => findHead e
1652 | _ => NONE 1652 | _ => NONE
1653 in 1653 in
1654 findHead e 1654 findHead e
1655 end
1656
1657 datatype needed = Needed of {Cons : (L'.kind * L'.con option) SM.map,
1658 Constraints : (E.env * (L'.con * L'.con) * ErrorMsg.span) list,
1659 Vals : SS.set,
1660 Mods : needed SM.map}
1661
1662 fun ncons (Needed r) = #Cons r
1663 fun nconstraints (Needed r) = #Constraints r
1664 fun nvals (Needed r) = #Vals r
1665 fun nmods (Needed r) = #Mods r
1666
1667 val nempty = Needed {Cons = SM.empty,
1668 Constraints = nil,
1669 Vals = SS.empty,
1670 Mods = SM.empty}
1671
1672 fun naddCon (r : needed, k, v) =
1673 let
1674 val Needed r = r
1675 in
1676 Needed {Cons = SM.insert (#Cons r, k, v),
1677 Constraints = #Constraints r,
1678 Vals = #Vals r,
1679 Mods = #Mods r}
1680 end
1681
1682 fun naddConstraint (r : needed, v) =
1683 let
1684 val Needed r = r
1685 in
1686 Needed {Cons = #Cons r,
1687 Constraints = v :: #Constraints r,
1688 Vals = #Vals r,
1689 Mods = #Mods r}
1690 end
1691
1692 fun naddVal (r : needed, k) =
1693 let
1694 val Needed r = r
1695 in
1696 Needed {Cons = #Cons r,
1697 Constraints = #Constraints r,
1698 Vals = SS.add (#Vals r, k),
1699 Mods = #Mods r}
1700 end
1701
1702 fun naddMod (r : needed, k, v) =
1703 let
1704 val Needed r = r
1705 in
1706 Needed {Cons = #Cons r,
1707 Constraints = #Constraints r,
1708 Vals = #Vals r,
1709 Mods = SM.insert (#Mods r, k, v)}
1710 end
1711
1712 fun ndelCon (r : needed, k) =
1713 let
1714 val Needed r = r
1715 in
1716 Needed {Cons = #1 (SM.remove (#Cons r, k)) handle NotFound => #Cons r,
1717 Constraints = #Constraints r,
1718 Vals = #Vals r,
1719 Mods = #Mods r}
1720 end
1721
1722 fun ndelVal (r : needed, k) =
1723 let
1724 val Needed r = r
1725 in
1726 Needed {Cons = #Cons r,
1727 Constraints = #Constraints r,
1728 Vals = SS.delete (#Vals r, k) handle NotFound => #Vals r,
1729 Mods = #Mods r}
1655 end 1730 end
1656 1731
1657 fun elabExp (env, denv) (eAll as (e, loc)) = 1732 fun elabExp (env, denv) (eAll as (e, loc)) =
1658 let 1733 let
1659 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*) 1734 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*)
3180 | L'.CUnit => SOME (L.CUnit, loc) 3255 | L'.CUnit => SOME (L.CUnit, loc)
3181 | L'.CUnif (_, _, _, ref (SOME c)) => decompileCon env c 3256 | L'.CUnif (_, _, _, ref (SOME c)) => decompileCon env c
3182 3257
3183 | _ => NONE 3258 | _ => NONE
3184 3259
3185 val (neededC, constraints, neededV, _) = 3260 fun buildNeeded env sgis =
3186 foldl (fn ((sgi, loc), (neededC, constraints, neededV, env')) => 3261 #1 (foldl (fn ((sgi, loc), (nd, env')) =>
3187 let 3262 (case sgi of
3188 val (needed, constraints, neededV) = 3263 L'.SgiCon (x, _, k, c) => naddCon (nd, x, (k, SOME c))
3189 case sgi of 3264 | L'.SgiConAbs (x, _, k) => naddCon (nd, x, (k, NONE))
3190 L'.SgiCon (x, _, k, c) => (SM.insert (neededC, x, (k, SOME c)), 3265 | L'.SgiConstraint cs => naddConstraint (nd, (env', cs, loc))
3191 constraints, neededV) 3266 | L'.SgiVal (x, _, t) =>
3192 | L'.SgiConAbs (x, _, k) => (SM.insert (neededC, x, (k, NONE)), constraints, neededV) 3267 let
3193 | L'.SgiConstraint cs => (neededC, (env', cs, loc) :: constraints, neededV) 3268 val t = normClassConstraint env' t
3194 3269 in
3195 | L'.SgiVal (x, _, t) => 3270 case #1 t of
3196 let 3271 L'.CApp (f, _) =>
3197 fun default () = (neededC, constraints, neededV) 3272 if isClassOrFolder env' f then
3198 3273 naddVal (nd, x)
3199 val t = normClassConstraint env' t 3274 else
3200 in 3275 nd
3201 case #1 t of 3276 | _ => nd
3202 L'.CApp (f, _) => 3277 end
3203 if isClassOrFolder env' f then 3278 | L'.SgiStr (x, _, s) =>
3204 (neededC, constraints, SS.add (neededV, x)) 3279 (case #1 (hnormSgn env s) of
3205 else 3280 L'.SgnConst sgis' => naddMod (nd, x, buildNeeded env sgis')
3206 default () 3281 | _ => nd)
3207 | _ => default () 3282 | _ => nd,
3208 end 3283 E.sgiBinds env' (sgi, loc)))
3209 3284 (nempty, env) sgis)
3210 | _ => (neededC, constraints, neededV) 3285
3211 in 3286 val nd = buildNeeded env sgis
3212 (needed, constraints, neededV, E.sgiBinds env' (sgi, loc)) 3287
3213 end) 3288 fun removeUsed (nd, ds) =
3214 (SM.empty, [], SS.empty, env) sgis 3289 foldl (fn ((d, _), nd) =>
3215
3216 val (neededC, neededV) =
3217 foldl (fn ((d, _), needed as (neededC, neededV)) =>
3218 case d of 3290 case d of
3219 L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV) 3291 L.DCon (x, _, _) => ndelCon (nd, x)
3220 handle NotFound => 3292 | L.DClass (x, _, _) => ndelCon (nd, x)
3221 needed) 3293 | L.DVal (x, _, _) => ndelVal (nd, x)
3222 | L.DClass (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV) 3294 | L.DOpen _ => nempty
3223 handle NotFound => needed) 3295 | L.DStr (x, _, (L.StrConst ds', _)) =>
3224 | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x)) 3296 (case SM.find (nmods nd, x) of
3225 handle NotFound => needed) 3297 NONE => nd
3226 | L.DOpen _ => (SM.empty, SS.empty) 3298 | SOME nd' => naddMod (nd, x, removeUsed (nd', ds')))
3227 | _ => needed) 3299 | _ => nd)
3228 (neededC, neededV) ds 3300 nd ds
3229 3301
3230 val ds' = List.mapPartial (fn (env', (c1, c2), loc) => 3302 val nd = removeUsed (nd, ds)
3231 case (decompileCon env' c1, decompileCon env' c2) of 3303
3232 (SOME c1, SOME c2) => 3304 fun extend (nd, ds) =
3233 SOME (L.DConstraint (c1, c2), loc) 3305 let
3234 | _ => NONE) constraints 3306 val ds' = List.mapPartial (fn (env', (c1, c2), loc) =>
3235 3307 case (decompileCon env' c1, decompileCon env' c2) of
3236 val ds' = 3308 (SOME c1, SOME c2) =>
3237 case SS.listItems neededV of 3309 SOME (L.DConstraint (c1, c2), loc)
3238 [] => ds' 3310 | _ => NONE) (nconstraints nd)
3239 | xs => 3311
3240 let 3312 val ds' =
3241 val ewild = (L.EWild, #2 str) 3313 case SS.listItems (nvals nd) of
3242 val ds'' = map (fn x => (L.DVal (x, NONE, ewild), #2 str)) xs 3314 [] => ds'
3243 in 3315 | xs =>
3244 ds'' @ ds' 3316 let
3245 end 3317 val ewild = (L.EWild, #2 str)
3246 3318 val ds'' = map (fn x => (L.DVal (x, NONE, ewild), #2 str)) xs
3247 val ds' = 3319 in
3248 case SM.listItemsi neededC of 3320 ds'' @ ds'
3249 [] => ds' 3321 end
3250 | xs => 3322
3251 let 3323 val ds' =
3252 val ds'' = map (fn (x, (k, co)) => 3324 case SM.listItemsi (ncons nd) of
3253 let 3325 [] => ds'
3254 val k = 3326 | xs =>
3255 case decompileKind k of 3327 let
3256 NONE => (L.KWild, #2 str) 3328 val ds'' = map (fn (x, (k, co)) =>
3257 | SOME k => k 3329 let
3258 3330 val k =
3259 val cwild = (L.CWild k, #2 str) 3331 case decompileKind k of
3260 val c = 3332 NONE => (L.KWild, #2 str)
3261 case co of 3333 | SOME k => k
3262 NONE => cwild 3334
3263 | SOME c => 3335 val cwild = (L.CWild k, #2 str)
3264 case decompileCon env c of 3336 val c =
3265 NONE => cwild 3337 case co of
3266 | SOME c' => c' 3338 NONE => cwild
3267 in 3339 | SOME c =>
3268 (L.DCon (x, NONE, c), #2 str) 3340 case decompileCon env c of
3269 end) xs 3341 NONE => cwild
3270 in 3342 | SOME c' => c'
3271 ds'' @ ds' 3343 in
3272 end 3344 (L.DCon (x, NONE, c), #2 str)
3345 end) xs
3346 in
3347 ds'' @ ds'
3348 end
3349
3350 val ds = map (fn d as (L.DStr (x, s, (L.StrConst ds', loc')), loc) =>
3351 (case SM.find (nmods nd, x) of
3352 NONE => d
3353 | SOME nd' => (L.DStr (x, s, (L.StrConst (extend (nd', ds')), loc')), loc))
3354 | d => d) ds
3355 in
3356 ds @ ds'
3357 end
3273 in 3358 in
3274 (L.StrConst (ds @ ds'), #2 str) 3359 (L.StrConst (extend (nd, ds)), #2 str)
3275 end 3360 end
3276 | _ => str) 3361 | _ => str)
3277 | _ => str 3362 | _ => str
3278 3363
3279 and elabDecl (dAll as (d, loc), (env, denv, gs)) = 3364 and elabDecl (dAll as (d, loc), (env, denv, gs)) =