Mercurial > urweb
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) |