Mercurial > urweb

comparison src/elab_util.sml @ 34:44b5405e74c7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating module projection
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Jun 2008 16:38:54 -0400
parents 537db4ee89f4
children 1405d8c26790
comparison
equal deleted inserted replaced
33:535c324f0b35 34:44b5405e74c7
107 fn c' => 107 fn c' =>
108 (TRecord c', loc)) 108 (TRecord c', loc))
109 109
110 | CRel _ => S.return2 cAll 110 | CRel _ => S.return2 cAll
111 | CNamed _ => S.return2 cAll 111 | CNamed _ => S.return2 cAll
112 | CModProj _ => S.return2 cAll
112 | CApp (c1, c2) => 113 | CApp (c1, c2) =>
113 S.bind2 (mfc ctx c1, 114 S.bind2 (mfc ctx c1,
114 fn c1' => 115 fn c1' =>
115 S.map2 (mfc ctx c2, 116 S.map2 (mfc ctx c2,
116 fn c2' => 117 fn c2' =>
158 fun mapB {kind, con, bind} ctx c = 159 fun mapB {kind, con, bind} ctx c =
159 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), 160 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
160 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), 161 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
161 bind = bind} ctx c () of 162 bind = bind} ctx c () of
162 S.Continue (c, ()) => c 163 S.Continue (c, ()) => c
163 | S.Return _ => raise Fail "Con.mapB: Impossible" 164 | S.Return _ => raise Fail "ElabUtil.Con.mapB: Impossible"
165
166 fun map {kind, con} s =
167 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
168 con = fn c => fn () => S.Continue (con c, ())} s () of
169 S.Return () => raise Fail "ElabUtil.Con.map: Impossible"
170 | S.Continue (s, ()) => s
164 171
165 fun exists {kind, con} k = 172 fun exists {kind, con} k =
166 case mapfold {kind = fn k => fn () => 173 case mapfold {kind = fn k => fn () =>
167 if kind k then 174 if kind k then
168 S.Return () 175 S.Return ()
206 and mfe' ctx (eAll as (e, loc)) = 213 and mfe' ctx (eAll as (e, loc)) =
207 case e of 214 case e of
208 EPrim _ => S.return2 eAll 215 EPrim _ => S.return2 eAll
209 | ERel _ => S.return2 eAll 216 | ERel _ => S.return2 eAll
210 | ENamed _ => S.return2 eAll 217 | ENamed _ => S.return2 eAll
218 | EModProj _ => S.return2 eAll
211 | EApp (e1, e2) => 219 | EApp (e1, e2) =>
212 S.bind2 (mfe ctx e1, 220 S.bind2 (mfe ctx e1,
213 fn e1' => 221 fn e1' =>
214 S.map2 (mfe ctx e2, 222 S.map2 (mfe ctx e2,
215 fn e2' => 223 fn e2' =>
289 S.Return _ => true 297 S.Return _ => true
290 | S.Continue _ => false 298 | S.Continue _ => false
291 299
292 end 300 end
293 301
294 end 302 structure Sgn = struct
303
304 datatype binder =
305 RelC of string * Elab.kind
306 | NamedC of string * Elab.kind
307 | Str of string * Elab.sgn
308
309 fun mapfoldB {kind, con, sgn_item, sgn, bind} =
310 let
311 fun bind' (ctx, b) =
312 let
313 val b' = case b of
314 Con.Rel x => RelC x
315 | Con.Named x => NamedC x
316 in
317 bind (ctx, b')
318 end
319 val con = Con.mapfoldB {kind = kind, con = con, bind = bind'}
320
321 val kind = Kind.mapfold kind
322
323 fun sgi ctx si acc =
324 S.bindP (sgi' ctx si acc, sgn_item ctx)
325
326 and sgi' ctx (si, loc) =
327 case si of
328 SgiConAbs (x, n, k) =>
329 S.map2 (kind k,
330 fn k' =>
331 (SgiConAbs (x, n, k'), loc))
332 | SgiCon (x, n, k, c) =>
333 S.bind2 (kind k,
334 fn k' =>
335 S.map2 (con ctx c,
336 fn c' =>
337 (SgiCon (x, n, k', c'), loc)))
338 | SgiVal (x, n, c) =>
339 S.map2 (con ctx c,
340 fn c' =>
341 (SgiVal (x, n, c'), loc))
342 | SgiStr (x, n, s) =>
343 S.map2 (sg ctx s,
344 fn s' =>
345 (SgiStr (x, n, s'), loc))
346
347 and sg ctx s acc =
348 S.bindP (sg' ctx s acc, sgn ctx)
349
350 and sg' ctx (sAll as (s, loc)) =
351 case s of
352 SgnConst sgis =>
353 S.map2 (ListUtil.mapfoldB (fn (ctx, si) =>
354 (case #1 si of
355 SgiConAbs (x, _, k) =>
356 bind (ctx, NamedC (x, k))
357 | SgiCon (x, _, k, _) =>
358 bind (ctx, NamedC (x, k))
359 | SgiVal _ => ctx
360 | SgiStr (x, _, sgn) =>
361 bind (ctx, Str (x, sgn)),
362 sgi ctx si)) ctx sgis,
363 fn sgis' =>
364 (SgnConst sgis', loc))
365
366 | SgnVar _ => S.return2 sAll
367 | SgnError => S.return2 sAll
368 in
369 sg
370 end
371
372 fun mapfold {kind, con, sgn_item, sgn} =
373 mapfoldB {kind = kind,
374 con = fn () => con,
375 sgn_item = fn () => sgn_item,
376 sgn = fn () => sgn,
377 bind = fn ((), _) => ()} ()
378
379 fun map {kind, con, sgn_item, sgn} s =
380 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
381 con = fn c => fn () => S.Continue (con c, ()),
382 sgn_item = fn si => fn () => S.Continue (sgn_item si, ()),
383 sgn = fn s => fn () => S.Continue (sgn s, ())} s () of
384 S.Return () => raise Fail "Elab_util.Sgn.map"
385 | S.Continue (s, ()) => s
386
387 end
388
389 end