comparison src/elaborate.sml @ 1277:1e6a4f9d3e4a

More generous wildification, covering map-records
author Adam Chlipala <adamc@hcoop.net>
date Sun, 13 Jun 2010 10:55:20 -0400
parents 74150edf1134
children b4480a56cab7
comparison
equal deleted inserted replaced
1276:5b5c0b552f59 1277:1e6a4f9d3e4a
3279 L'.SgiCon (x, _, k, c) => naddCon (nd, x, (k, SOME c)) 3279 L'.SgiCon (x, _, k, c) => naddCon (nd, x, (k, SOME c))
3280 | L'.SgiConAbs (x, _, k) => naddCon (nd, x, (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 fun should t =
3285 let
3286 val t = normClassConstraint env' t
3287 in
3288 case #1 t of
3289 L'.CApp (f, _) => isClassOrFolder env' f
3290 | L'.TRecord t =>
3291 (case hnormCon env' t of
3292 (L'.CApp (f, _), _) =>
3293 (case hnormCon env' f of
3294 (L'.CApp (f, cl), loc) =>
3295 (case hnormCon env' f of
3296 (L'.CMap _, _) => isClassOrFolder env' cl
3297 | _ => false)
3298 | _ => false)
3299 | _ => false)
3300 | _ => false
3301 end
3285 in 3302 in
3286 case #1 t of 3303 if should t then
3287 L'.CApp (f, _) => 3304 naddVal (nd, x)
3288 if isClassOrFolder env' f then 3305 else
3289 naddVal (nd, x) 3306 nd
3290 else
3291 nd
3292 | _ => nd
3293 end 3307 end
3294 | L'.SgiStr (x, _, s) => 3308 | L'.SgiStr (x, _, s) =>
3295 (case #1 (hnormSgn env' s) of 3309 (case #1 (hnormSgn env' s) of
3296 L'.SgnConst sgis' => naddMod (nd, x, (env', buildNeeded env' sgis')) 3310 L'.SgnConst sgis' => naddMod (nd, x, (env', buildNeeded env' sgis'))
3297 | _ => nd) 3311 | _ => nd)