Mercurial > urweb

comparison src/elab_util.sml @ 59:abb2b32c19fb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Subsignatures
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Jun 2008 19:10:38 -0400
parents b3fbbc6cb1e5
children 9f89f0b00b84
comparison
equal deleted inserted replaced
58:fd8a81ecd598 59:abb2b32c19fb
303 303
304 datatype binder = 304 datatype binder =
305 RelC of string * Elab.kind 305 RelC of string * Elab.kind
306 | NamedC of string * Elab.kind 306 | NamedC of string * Elab.kind
307 | Str of string * Elab.sgn 307 | Str of string * Elab.sgn
308 | Sgn of string * Elab.sgn
308 309
309 fun mapfoldB {kind, con, sgn_item, sgn, bind} = 310 fun mapfoldB {kind, con, sgn_item, sgn, bind} =
310 let 311 let
311 fun bind' (ctx, b) = 312 fun bind' (ctx, b) =
312 let 313 let
341 (SgiVal (x, n, c'), loc)) 342 (SgiVal (x, n, c'), loc))
342 | SgiStr (x, n, s) => 343 | SgiStr (x, n, s) =>
343 S.map2 (sg ctx s, 344 S.map2 (sg ctx s,
344 fn s' => 345 fn s' =>
345 (SgiStr (x, n, s'), loc)) 346 (SgiStr (x, n, s'), loc))
347 | SgiSgn (x, n, s) =>
348 S.map2 (sg ctx s,
349 fn s' =>
350 (SgiSgn (x, n, s'), loc))
346 351
347 and sg ctx s acc = 352 and sg ctx s acc =
348 S.bindP (sg' ctx s acc, sgn ctx) 353 S.bindP (sg' ctx s acc, sgn ctx)
349 354
350 and sg' ctx (sAll as (s, loc)) = 355 and sg' ctx (sAll as (s, loc)) =
356 bind (ctx, NamedC (x, k)) 361 bind (ctx, NamedC (x, k))
357 | SgiCon (x, _, k, _) => 362 | SgiCon (x, _, k, _) =>
358 bind (ctx, NamedC (x, k)) 363 bind (ctx, NamedC (x, k))
359 | SgiVal _ => ctx 364 | SgiVal _ => ctx
360 | SgiStr (x, _, sgn) => 365 | SgiStr (x, _, sgn) =>
361 bind (ctx, Str (x, sgn)), 366 bind (ctx, Str (x, sgn))
367 | SgiSgn (x, _, sgn) =>
368 bind (ctx, Sgn (x, sgn)),
362 sgi ctx si)) ctx sgis, 369 sgi ctx si)) ctx sgis,
363 fn sgis' => 370 fn sgis' =>
364 (SgnConst sgis', loc)) 371 (SgnConst sgis', loc))
365 372
366 | SgnVar _ => S.return2 sAll 373 | SgnVar _ => S.return2 sAll
368 S.bind2 (sg ctx s1, 375 S.bind2 (sg ctx s1,
369 fn s1' => 376 fn s1' =>
370 S.map2 (sg (bind (ctx, Str (m, s1'))) s2, 377 S.map2 (sg (bind (ctx, Str (m, s1'))) s2,
371 fn s2' => 378 fn s2' =>
372 (SgnFun (m, n, s1', s2'), loc))) 379 (SgnFun (m, n, s1', s2'), loc)))
380 | SgnProj _ => S.return2 sAll
373 | SgnWhere (sgn, x, c) => 381 | SgnWhere (sgn, x, c) =>
374 S.bind2 (sg ctx sgn, 382 S.bind2 (sg ctx sgn,
375 fn sgn' => 383 fn sgn' =>
376 S.map2 (con ctx c, 384 S.map2 (con ctx c,
377 fn c' => 385 fn c' =>