Mercurial > urweb

comparison src/expl_util.sml @ 64:d609820c5834

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proper hiding of shadowed bindings in principal signatures
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Jun 2008 08:54:49 -0400
parents 3c1ce1b4eb3d
children c1e21ab42896
comparison
equal deleted inserted replaced
63:c5a503ad0d8c 64:d609820c5834
292 292
293 datatype binder = 293 datatype binder =
294 RelC of string * Expl.kind 294 RelC of string * Expl.kind
295 | NamedC of string * Expl.kind 295 | NamedC of string * Expl.kind
296 | Str of string * Expl.sgn 296 | Str of string * Expl.sgn
297 | Sgn of string * Expl.sgn
297 298
298 fun mapfoldB {kind, con, sgn_item, sgn, bind} = 299 fun mapfoldB {kind, con, sgn_item, sgn, bind} =
299 let 300 let
300 fun bind' (ctx, b) = 301 fun bind' (ctx, b) =
301 let 302 let
330 (SgiVal (x, n, c'), loc)) 331 (SgiVal (x, n, c'), loc))
331 | SgiStr (x, n, s) => 332 | SgiStr (x, n, s) =>
332 S.map2 (sg ctx s, 333 S.map2 (sg ctx s,
333 fn s' => 334 fn s' =>
334 (SgiStr (x, n, s'), loc)) 335 (SgiStr (x, n, s'), loc))
336 | SgiSgn (x, n, s) =>
337 S.map2 (sg ctx s,
338 fn s' =>
339 (SgiSgn (x, n, s'), loc))
335 340
336 and sg ctx s acc = 341 and sg ctx s acc =
337 S.bindP (sg' ctx s acc, sgn ctx) 342 S.bindP (sg' ctx s acc, sgn ctx)
338 343
339 and sg' ctx (sAll as (s, loc)) = 344 and sg' ctx (sAll as (s, loc)) =
345 bind (ctx, NamedC (x, k)) 350 bind (ctx, NamedC (x, k))
346 | SgiCon (x, _, k, _) => 351 | SgiCon (x, _, k, _) =>
347 bind (ctx, NamedC (x, k)) 352 bind (ctx, NamedC (x, k))
348 | SgiVal _ => ctx 353 | SgiVal _ => ctx
349 | SgiStr (x, _, sgn) => 354 | SgiStr (x, _, sgn) =>
350 bind (ctx, Str (x, sgn)), 355 bind (ctx, Str (x, sgn))
356 | SgiSgn (x, _, sgn) =>
357 bind (ctx, Sgn (x, sgn)),
351 sgi ctx si)) ctx sgis, 358 sgi ctx si)) ctx sgis,
352 fn sgis' => 359 fn sgis' =>
353 (SgnConst sgis', loc)) 360 (SgnConst sgis', loc))
354 361
355 | SgnVar _ => S.return2 sAll 362 | SgnVar _ => S.return2 sAll
364 S.bind2 (sg ctx sgn, 371 S.bind2 (sg ctx sgn,
365 fn sgn' => 372 fn sgn' =>
366 S.map2 (con ctx c, 373 S.map2 (con ctx c,
367 fn c' => 374 fn c' =>
368 (SgnWhere (sgn', x, c'), loc))) 375 (SgnWhere (sgn', x, c'), loc)))
376 | SgnProj _ => S.return2 sAll
369 in 377 in
370 sg 378 sg
371 end 379 end
372 380
373 fun mapfold {kind, con, sgn_item, sgn} = 381 fun mapfold {kind, con, sgn_item, sgn} =