Mercurial > urweb

annotate src/elab_util.sml @ 109:813e5a52063d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove closure conversion in favor of zany fun with modules, which also replaces 'page'
author Adam Chlipala <adamc@hcoop.net>
date Sun, 13 Jul 2008 10:17:06 -0400
parents f0f59e918cac
children e3041657d653
rev   line source
adamc@2 1 (* Copyright (c) 2008, Adam Chlipala
adamc@2 2 * All rights reserved.
adamc@2 3 *
adamc@2 4 * Redistribution and use in source and binary forms, with or without
adamc@2 5 * modification, are permitted provided that the following conditions are met:
adamc@2 6 *
adamc@2 7 * - Redistributions of source code must retain the above copyright notice,
adamc@2 8 * this list of conditions and the following disclaimer.
adamc@2 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@2 10 * this list of conditions and the following disclaimer in the documentation
adamc@2 11 * and/or other materials provided with the distribution.
adamc@2 12 * - The names of contributors may not be used to endorse or promote products
adamc@2 13 * derived from this software without specific prior written permission.
adamc@2 14 *
adamc@2 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@2 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@2 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@2 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@2 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@2 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@2 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@2 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@2 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@2 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@2 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@2 26 *)
adamc@2 27
adamc@2 28 structure ElabUtil :> ELAB_UTIL = struct
adamc@2 29
adamc@2 30 open Elab
adamc@2 31
adamc@2 32 structure S = Search
adamc@2 33
adamc@2 34 structure Kind = struct
adamc@2 35
adamc@6 36 fun mapfold f =
adamc@2 37 let
adamc@2 38 fun mfk k acc =
adamc@2 39 S.bindP (mfk' k acc, f)
adamc@2 40
adamc@2 41 and mfk' (kAll as (k, loc)) =
adamc@2 42 case k of
adamc@2 43 KType => S.return2 kAll
adamc@2 44
adamc@2 45 | KArrow (k1, k2) =>
adamc@2 46 S.bind2 (mfk k1,
adamc@2 47 fn k1' =>
adamc@2 48 S.map2 (mfk k2,
adamc@2 49 fn k2' =>
adamc@2 50 (KArrow (k1', k2'), loc)))
adamc@2 51
adamc@2 52 | KName => S.return2 kAll
adamc@2 53
adamc@2 54 | KRecord k =>
adamc@2 55 S.map2 (mfk k,
adamc@2 56 fn k' =>
adamc@2 57 (KRecord k', loc))
adamc@2 58
adamc@82 59 | KUnit => S.return2 kAll
adamc@82 60
adamc@2 61 | KError => S.return2 kAll
adamc@2 62
adamc@76 63 | KUnif (_, _, ref (SOME k)) => mfk' k
adamc@2 64 | KUnif _ => S.return2 kAll
adamc@2 65 in
adamc@2 66 mfk
adamc@2 67 end
adamc@2 68
adamc@2 69 fun exists f k =
adamc@6 70 case mapfold (fn k => fn () =>
adamc@6 71 if f k then
adamc@6 72 S.Return ()
adamc@6 73 else
adamc@6 74 S.Continue (k, ())) k () of
adamc@6 75 S.Return _ => true
adamc@6 76 | S.Continue _ => false
adamc@6 77
adamc@6 78 end
adamc@6 79
adamc@6 80 structure Con = struct
adamc@6 81
adamc@11 82 datatype binder =
adamc@11 83 Rel of string * Elab.kind
adamc@11 84 | Named of string * Elab.kind
adamc@11 85
adamc@11 86 fun mapfoldB {kind = fk, con = fc, bind} =
adamc@6 87 let
adamc@6 88 val mfk = Kind.mapfold fk
adamc@6 89
adamc@11 90 fun mfc ctx c acc =
adamc@11 91 S.bindP (mfc' ctx c acc, fc ctx)
adamc@6 92
adamc@11 93 and mfc' ctx (cAll as (c, loc)) =
adamc@6 94 case c of
adamc@6 95 TFun (c1, c2) =>
adamc@11 96 S.bind2 (mfc ctx c1,
adamc@6 97 fn c1' =>
adamc@11 98 S.map2 (mfc ctx c2,
adamc@6 99 fn c2' =>
adamc@6 100 (TFun (c1', c2'), loc)))
adamc@6 101 | TCFun (e, x, k, c) =>
adamc@6 102 S.bind2 (mfk k,
adamc@6 103 fn k' =>
adamc@11 104 S.map2 (mfc (bind (ctx, Rel (x, k))) c,
adamc@6 105 fn c' =>
adamc@6 106 (TCFun (e, x, k', c'), loc)))
adamc@85 107 | TDisjoint (c1, c2, c3) =>
adamc@85 108 S.bind2 (mfc ctx c1,
adamc@85 109 fn c1' =>
adamc@85 110 S.bind2 (mfc ctx c2,
adamc@85 111 fn c2' =>
adamc@85 112 S.map2 (mfc ctx c3,
adamc@85 113 fn c3' =>
adamc@85 114 (TDisjoint (c1', c2', c3'), loc))))
adamc@6 115 | TRecord c =>
adamc@11 116 S.map2 (mfc ctx c,
adamc@6 117 fn c' =>
adamc@6 118 (TRecord c', loc))
adamc@6 119
adamc@6 120 | CRel _ => S.return2 cAll
adamc@6 121 | CNamed _ => S.return2 cAll
adamc@34 122 | CModProj _ => S.return2 cAll
adamc@6 123 | CApp (c1, c2) =>
adamc@11 124 S.bind2 (mfc ctx c1,
adamc@6 125 fn c1' =>
adamc@11 126 S.map2 (mfc ctx c2,
adamc@6 127 fn c2' =>
adamc@6 128 (CApp (c1', c2'), loc)))
adamc@8 129 | CAbs (x, k, c) =>
adamc@6 130 S.bind2 (mfk k,
adamc@6 131 fn k' =>
adamc@11 132 S.map2 (mfc (bind (ctx, Rel (x, k))) c,
adamc@6 133 fn c' =>
adamc@8 134 (CAbs (x, k', c'), loc)))
adamc@84 135 | CDisjoint (c1, c2, c3) =>
adamc@84 136 S.bind2 (mfc ctx c1,
adamc@84 137 fn c1' =>
adamc@84 138 S.bind2 (mfc ctx c2,
adamc@84 139 fn c2' =>
adamc@84 140 S.map2 (mfc ctx c3,
adamc@84 141 fn c3' =>
adamc@84 142 (CDisjoint (c1', c2', c3'), loc))))
adamc@6 143
adamc@6 144 | CName _ => S.return2 cAll
adamc@6 145
adamc@6 146 | CRecord (k, xcs) =>
adamc@6 147 S.bind2 (mfk k,
adamc@6 148 fn k' =>
adamc@6 149 S.map2 (ListUtil.mapfold (fn (x, c) =>
adamc@11 150 S.bind2 (mfc ctx x,
adamc@6 151 fn x' =>
adamc@11 152 S.map2 (mfc ctx c,
adamc@6 153 fn c' =>
adamc@6 154 (x', c'))))
adamc@6 155 xcs,
adamc@6 156 fn xcs' =>
adamc@6 157 (CRecord (k', xcs'), loc)))
adamc@6 158 | CConcat (c1, c2) =>
adamc@11 159 S.bind2 (mfc ctx c1,
adamc@6 160 fn c1' =>
adamc@11 161 S.map2 (mfc ctx c2,
adamc@6 162 fn c2' =>
adamc@6 163 (CConcat (c1', c2'), loc)))
adamc@67 164 | CFold (k1, k2) =>
adamc@67 165 S.bind2 (mfk k1,
adamc@67 166 fn k1' =>
adamc@67 167 S.map2 (mfk k2,
adamc@67 168 fn k2' =>
adamc@67 169 (CFold (k1', k2'), loc)))
adamc@6 170
adamc@82 171 | CUnit => S.return2 cAll
adamc@82 172
adamc@6 173 | CError => S.return2 cAll
adamc@76 174 | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c
adamc@6 175 | CUnif _ => S.return2 cAll
adamc@6 176 in
adamc@6 177 mfc
adamc@6 178 end
adamc@6 179
adamc@11 180 fun mapfold {kind = fk, con = fc} =
adamc@11 181 mapfoldB {kind = fk,
adamc@11 182 con = fn () => fc,
adamc@11 183 bind = fn ((), _) => ()} ()
adamc@11 184
adamc@11 185 fun mapB {kind, con, bind} ctx c =
adamc@11 186 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@11 187 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@11 188 bind = bind} ctx c () of
adamc@11 189 S.Continue (c, ()) => c
adamc@34 190 | S.Return _ => raise Fail "ElabUtil.Con.mapB: Impossible"
adamc@34 191
adamc@34 192 fun map {kind, con} s =
adamc@34 193 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@34 194 con = fn c => fn () => S.Continue (con c, ())} s () of
adamc@34 195 S.Return () => raise Fail "ElabUtil.Con.map: Impossible"
adamc@34 196 | S.Continue (s, ()) => s
adamc@11 197
adamc@6 198 fun exists {kind, con} k =
adamc@6 199 case mapfold {kind = fn k => fn () =>
adamc@6 200 if kind k then
adamc@6 201 S.Return ()
adamc@6 202 else
adamc@6 203 S.Continue (k, ()),
adamc@6 204 con = fn c => fn () =>
adamc@6 205 if con c then
adamc@6 206 S.Return ()
adamc@6 207 else
adamc@6 208 S.Continue (c, ())} k () of
adamc@2 209 S.Return _ => true
adamc@2 210 | S.Continue _ => false
adamc@2 211
adamc@2 212 end
adamc@2 213
adamc@10 214 structure Exp = struct
adamc@10 215
adamc@11 216 datatype binder =
adamc@11 217 RelC of string * Elab.kind
adamc@11 218 | NamedC of string * Elab.kind
adamc@11 219 | RelE of string * Elab.con
adamc@11 220 | NamedE of string * Elab.con
adamc@11 221
adamc@11 222 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
adamc@10 223 let
adamc@10 224 val mfk = Kind.mapfold fk
adamc@10 225
adamc@11 226 fun bind' (ctx, b) =
adamc@11 227 let
adamc@11 228 val b' = case b of
adamc@11 229 Con.Rel x => RelC x
adamc@11 230 | Con.Named x => NamedC x
adamc@11 231 in
adamc@11 232 bind (ctx, b')
adamc@11 233 end
adamc@11 234 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@10 235
adamc@11 236 fun mfe ctx e acc =
adamc@11 237 S.bindP (mfe' ctx e acc, fe ctx)
adamc@11 238
adamc@11 239 and mfe' ctx (eAll as (e, loc)) =
adamc@10 240 case e of
adamc@14 241 EPrim _ => S.return2 eAll
adamc@14 242 | ERel _ => S.return2 eAll
adamc@10 243 | ENamed _ => S.return2 eAll
adamc@34 244 | EModProj _ => S.return2 eAll
adamc@10 245 | EApp (e1, e2) =>
adamc@11 246 S.bind2 (mfe ctx e1,
adamc@10 247 fn e1' =>
adamc@11 248 S.map2 (mfe ctx e2,
adamc@10 249 fn e2' =>
adamc@10 250 (EApp (e1', e2'), loc)))
adamc@26 251 | EAbs (x, dom, ran, e) =>
adamc@26 252 S.bind2 (mfc ctx dom,
adamc@26 253 fn dom' =>
adamc@26 254 S.bind2 (mfc ctx ran,
adamc@26 255 fn ran' =>
adamc@26 256 S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
adamc@26 257 fn e' =>
adamc@26 258 (EAbs (x, dom', ran', e'), loc))))
adamc@26 259
adamc@10 260 | ECApp (e, c) =>
adamc@11 261 S.bind2 (mfe ctx e,
adamc@10 262 fn e' =>
adamc@11 263 S.map2 (mfc ctx c,
adamc@10 264 fn c' =>
adamc@10 265 (ECApp (e', c'), loc)))
adamc@10 266 | ECAbs (expl, x, k, e) =>
adamc@10 267 S.bind2 (mfk k,
adamc@10 268 fn k' =>
adamc@11 269 S.map2 (mfe (bind (ctx, RelC (x, k))) e,
adamc@10 270 fn e' =>
adamc@10 271 (ECAbs (expl, x, k', e'), loc)))
adamc@10 272
adamc@12 273 | ERecord xes =>
adamc@29 274 S.map2 (ListUtil.mapfold (fn (x, e, t) =>
adamc@12 275 S.bind2 (mfc ctx x,
adamc@12 276 fn x' =>
adamc@29 277 S.bind2 (mfe ctx e,
adamc@12 278 fn e' =>
adamc@29 279 S.map2 (mfc ctx t,
adamc@29 280 fn t' =>
adamc@29 281 (x', e', t')))))
adamc@12 282 xes,
adamc@12 283 fn xes' =>
adamc@12 284 (ERecord xes', loc))
adamc@12 285 | EField (e, c, {field, rest}) =>
adamc@12 286 S.bind2 (mfe ctx e,
adamc@12 287 fn e' =>
adamc@12 288 S.bind2 (mfc ctx c,
adamc@12 289 fn c' =>
adamc@12 290 S.bind2 (mfc ctx field,
adamc@12 291 fn field' =>
adamc@12 292 S.map2 (mfc ctx rest,
adamc@12 293 fn rest' =>
adamc@12 294 (EField (e', c', {field = field', rest = rest'}), loc)))))
adamc@12 295
adamc@71 296 | EFold k =>
adamc@71 297 S.map2 (mfk k,
adamc@71 298 fn k' =>
adamc@71 299 (EFold k', loc))
adamc@71 300
adamc@10 301 | EError => S.return2 eAll
adamc@10 302 in
adamc@10 303 mfe
adamc@10 304 end
adamc@10 305
adamc@11 306 fun mapfold {kind = fk, con = fc, exp = fe} =
adamc@11 307 mapfoldB {kind = fk,
adamc@11 308 con = fn () => fc,
adamc@11 309 exp = fn () => fe,
adamc@11 310 bind = fn ((), _) => ()} ()
adamc@11 311
adamc@10 312 fun exists {kind, con, exp} k =
adamc@10 313 case mapfold {kind = fn k => fn () =>
adamc@10 314 if kind k then
adamc@10 315 S.Return ()
adamc@10 316 else
adamc@10 317 S.Continue (k, ()),
adamc@10 318 con = fn c => fn () =>
adamc@10 319 if con c then
adamc@10 320 S.Return ()
adamc@10 321 else
adamc@10 322 S.Continue (c, ()),
adamc@10 323 exp = fn e => fn () =>
adamc@10 324 if exp e then
adamc@10 325 S.Return ()
adamc@10 326 else
adamc@10 327 S.Continue (e, ())} k () of
adamc@10 328 S.Return _ => true
adamc@10 329 | S.Continue _ => false
adamc@10 330
adamc@10 331 end
adamc@10 332
adamc@34 333 structure Sgn = struct
adamc@34 334
adamc@34 335 datatype binder =
adamc@34 336 RelC of string * Elab.kind
adamc@34 337 | NamedC of string * Elab.kind
adamc@34 338 | Str of string * Elab.sgn
adamc@59 339 | Sgn of string * Elab.sgn
adamc@34 340
adamc@34 341 fun mapfoldB {kind, con, sgn_item, sgn, bind} =
adamc@34 342 let
adamc@34 343 fun bind' (ctx, b) =
adamc@34 344 let
adamc@34 345 val b' = case b of
adamc@34 346 Con.Rel x => RelC x
adamc@34 347 | Con.Named x => NamedC x
adamc@34 348 in
adamc@34 349 bind (ctx, b')
adamc@34 350 end
adamc@34 351 val con = Con.mapfoldB {kind = kind, con = con, bind = bind'}
adamc@34 352
adamc@34 353 val kind = Kind.mapfold kind
adamc@34 354
adamc@34 355 fun sgi ctx si acc =
adamc@34 356 S.bindP (sgi' ctx si acc, sgn_item ctx)
adamc@34 357
adamc@34 358 and sgi' ctx (si, loc) =
adamc@34 359 case si of
adamc@34 360 SgiConAbs (x, n, k) =>
adamc@34 361 S.map2 (kind k,
adamc@34 362 fn k' =>
adamc@34 363 (SgiConAbs (x, n, k'), loc))
adamc@34 364 | SgiCon (x, n, k, c) =>
adamc@34 365 S.bind2 (kind k,
adamc@34 366 fn k' =>
adamc@34 367 S.map2 (con ctx c,
adamc@34 368 fn c' =>
adamc@34 369 (SgiCon (x, n, k', c'), loc)))
adamc@34 370 | SgiVal (x, n, c) =>
adamc@34 371 S.map2 (con ctx c,
adamc@34 372 fn c' =>
adamc@34 373 (SgiVal (x, n, c'), loc))
adamc@34 374 | SgiStr (x, n, s) =>
adamc@34 375 S.map2 (sg ctx s,
adamc@34 376 fn s' =>
adamc@34 377 (SgiStr (x, n, s'), loc))
adamc@59 378 | SgiSgn (x, n, s) =>
adamc@59 379 S.map2 (sg ctx s,
adamc@59 380 fn s' =>
adamc@59 381 (SgiSgn (x, n, s'), loc))
adamc@88 382 | SgiConstraint (c1, c2) =>
adamc@88 383 S.bind2 (con ctx c1,
adamc@88 384 fn c1' =>
adamc@88 385 S.map2 (con ctx c2,
adamc@88 386 fn c2' =>
adamc@88 387 (SgiConstraint (c1', c2'), loc)))
adamc@34 388
adamc@34 389 and sg ctx s acc =
adamc@34 390 S.bindP (sg' ctx s acc, sgn ctx)
adamc@34 391
adamc@34 392 and sg' ctx (sAll as (s, loc)) =
adamc@34 393 case s of
adamc@34 394 SgnConst sgis =>
adamc@34 395 S.map2 (ListUtil.mapfoldB (fn (ctx, si) =>
adamc@34 396 (case #1 si of
adamc@34 397 SgiConAbs (x, _, k) =>
adamc@34 398 bind (ctx, NamedC (x, k))
adamc@34 399 | SgiCon (x, _, k, _) =>
adamc@34 400 bind (ctx, NamedC (x, k))
adamc@34 401 | SgiVal _ => ctx
adamc@34 402 | SgiStr (x, _, sgn) =>
adamc@59 403 bind (ctx, Str (x, sgn))
adamc@59 404 | SgiSgn (x, _, sgn) =>
adamc@88 405 bind (ctx, Sgn (x, sgn))
adamc@88 406 | SgiConstraint _ => ctx,
adamc@34 407 sgi ctx si)) ctx sgis,
adamc@34 408 fn sgis' =>
adamc@34 409 (SgnConst sgis', loc))
adamc@34 410
adamc@34 411 | SgnVar _ => S.return2 sAll
adamc@41 412 | SgnFun (m, n, s1, s2) =>
adamc@41 413 S.bind2 (sg ctx s1,
adamc@41 414 fn s1' =>
adamc@41 415 S.map2 (sg (bind (ctx, Str (m, s1'))) s2,
adamc@41 416 fn s2' =>
adamc@41 417 (SgnFun (m, n, s1', s2'), loc)))
adamc@59 418 | SgnProj _ => S.return2 sAll
adamc@42 419 | SgnWhere (sgn, x, c) =>
adamc@42 420 S.bind2 (sg ctx sgn,
adamc@42 421 fn sgn' =>
adamc@42 422 S.map2 (con ctx c,
adamc@42 423 fn c' =>
adamc@42 424 (SgnWhere (sgn', x, c'), loc)))
adamc@34 425 | SgnError => S.return2 sAll
adamc@34 426 in
adamc@34 427 sg
adamc@34 428 end
adamc@34 429
adamc@34 430 fun mapfold {kind, con, sgn_item, sgn} =
adamc@34 431 mapfoldB {kind = kind,
adamc@34 432 con = fn () => con,
adamc@34 433 sgn_item = fn () => sgn_item,
adamc@34 434 sgn = fn () => sgn,
adamc@34 435 bind = fn ((), _) => ()} ()
adamc@34 436
adamc@34 437 fun map {kind, con, sgn_item, sgn} s =
adamc@34 438 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@34 439 con = fn c => fn () => S.Continue (con c, ()),
adamc@34 440 sgn_item = fn si => fn () => S.Continue (sgn_item si, ()),
adamc@34 441 sgn = fn s => fn () => S.Continue (sgn s, ())} s () of
adamc@34 442 S.Return () => raise Fail "Elab_util.Sgn.map"
adamc@34 443 | S.Continue (s, ()) => s
adamc@34 444
adamc@2 445 end
adamc@34 446
adamc@76 447 structure Decl = struct
adamc@76 448
adamc@76 449 datatype binder =
adamc@76 450 RelC of string * Elab.kind
adamc@76 451 | NamedC of string * Elab.kind
adamc@76 452 | RelE of string * Elab.con
adamc@76 453 | NamedE of string * Elab.con
adamc@76 454 | Str of string * Elab.sgn
adamc@76 455 | Sgn of string * Elab.sgn
adamc@76 456
adamc@76 457 fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} =
adamc@76 458 let
adamc@76 459 val mfk = Kind.mapfold fk
adamc@76 460
adamc@76 461 fun bind' (ctx, b) =
adamc@76 462 let
adamc@76 463 val b' = case b of
adamc@76 464 Con.Rel x => RelC x
adamc@76 465 | Con.Named x => NamedC x
adamc@76 466 in
adamc@76 467 bind (ctx, b')
adamc@76 468 end
adamc@76 469 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@76 470
adamc@76 471 fun bind' (ctx, b) =
adamc@76 472 let
adamc@76 473 val b' = case b of
adamc@76 474 Exp.RelC x => RelC x
adamc@76 475 | Exp.NamedC x => NamedC x
adamc@76 476 | Exp.RelE x => RelE x
adamc@76 477 | Exp.NamedE x => NamedE x
adamc@76 478 in
adamc@76 479 bind (ctx, b')
adamc@76 480 end
adamc@76 481 val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind'}
adamc@76 482
adamc@76 483 fun bind' (ctx, b) =
adamc@76 484 let
adamc@76 485 val b' = case b of
adamc@76 486 Sgn.RelC x => RelC x
adamc@76 487 | Sgn.NamedC x => NamedC x
adamc@76 488 | Sgn.Sgn x => Sgn x
adamc@76 489 | Sgn.Str x => Str x
adamc@76 490 in
adamc@76 491 bind (ctx, b')
adamc@76 492 end
adamc@76 493 val mfsg = Sgn.mapfoldB {kind = fk, con = fc, sgn_item = fsgi, sgn = fsg, bind = bind'}
adamc@76 494
adamc@76 495 fun mfst ctx str acc =
adamc@76 496 S.bindP (mfst' ctx str acc, fst ctx)
adamc@76 497
adamc@76 498 and mfst' ctx (strAll as (str, loc)) =
adamc@76 499 case str of
adamc@76 500 StrConst ds =>
adamc@76 501 S.map2 (ListUtil.mapfoldB (fn (ctx, d) =>
adamc@76 502 (case #1 d of
adamc@76 503 DCon (x, _, k, _) =>
adamc@76 504 bind (ctx, NamedC (x, k))
adamc@76 505 | DVal (x, _, c, _) =>
adamc@76 506 bind (ctx, NamedE (x, c))
adamc@76 507 | DSgn (x, _, sgn) =>
adamc@76 508 bind (ctx, Sgn (x, sgn))
adamc@76 509 | DStr (x, _, sgn, _) =>
adamc@76 510 bind (ctx, Str (x, sgn))
adamc@76 511 | DFfiStr (x, _, sgn) =>
adamc@88 512 bind (ctx, Str (x, sgn))
adamc@100 513 | DConstraint _ => ctx
adamc@109 514 | DExport _ => ctx,
adamc@76 515 mfd ctx d)) ctx ds,
adamc@76 516 fn ds' => (StrConst ds', loc))
adamc@76 517 | StrVar _ => S.return2 strAll
adamc@76 518 | StrProj (str, x) =>
adamc@76 519 S.map2 (mfst ctx str,
adamc@76 520 fn str' =>
adamc@76 521 (StrProj (str', x), loc))
adamc@76 522 | StrFun (x, n, sgn1, sgn2, str) =>
adamc@76 523 S.bind2 (mfsg ctx sgn1,
adamc@76 524 fn sgn1' =>
adamc@76 525 S.bind2 (mfsg ctx sgn2,
adamc@76 526 fn sgn2' =>
adamc@76 527 S.map2 (mfst ctx str,
adamc@76 528 fn str' =>
adamc@76 529 (StrFun (x, n, sgn1', sgn2', str'), loc))))
adamc@76 530 | StrApp (str1, str2) =>
adamc@76 531 S.bind2 (mfst ctx str1,
adamc@76 532 fn str1' =>
adamc@76 533 S.map2 (mfst ctx str2,
adamc@76 534 fn str2' =>
adamc@76 535 (StrApp (str1', str2'), loc)))
adamc@76 536 | StrError => S.return2 strAll
adamc@76 537
adamc@76 538 and mfd ctx d acc =
adamc@76 539 S.bindP (mfd' ctx d acc, fd ctx)
adamc@76 540
adamc@76 541 and mfd' ctx (dAll as (d, loc)) =
adamc@76 542 case d of
adamc@76 543 DCon (x, n, k, c) =>
adamc@76 544 S.bind2 (mfk k,
adamc@76 545 fn k' =>
adamc@76 546 S.map2 (mfc ctx c,
adamc@76 547 fn c' =>
adamc@76 548 (DCon (x, n, k', c'), loc)))
adamc@76 549 | DVal (x, n, c, e) =>
adamc@76 550 S.bind2 (mfc ctx c,
adamc@76 551 fn c' =>
adamc@76 552 S.map2 (mfe ctx e,
adamc@76 553 fn e' =>
adamc@76 554 (DVal (x, n, c', e'), loc)))
adamc@76 555 | DSgn (x, n, sgn) =>
adamc@76 556 S.map2 (mfsg ctx sgn,
adamc@76 557 fn sgn' =>
adamc@76 558 (DSgn (x, n, sgn'), loc))
adamc@76 559 | DStr (x, n, sgn, str) =>
adamc@76 560 S.bind2 (mfsg ctx sgn,
adamc@76 561 fn sgn' =>
adamc@76 562 S.map2 (mfst ctx str,
adamc@76 563 fn str' =>
adamc@76 564 (DStr (x, n, sgn', str'), loc)))
adamc@76 565 | DFfiStr (x, n, sgn) =>
adamc@76 566 S.map2 (mfsg ctx sgn,
adamc@76 567 fn sgn' =>
adamc@76 568 (DFfiStr (x, n, sgn'), loc))
adamc@88 569 | DConstraint (c1, c2) =>
adamc@88 570 S.bind2 (mfc ctx c1,
adamc@88 571 fn c1' =>
adamc@88 572 S.map2 (mfc ctx c2,
adamc@88 573 fn c2' =>
adamc@88 574 (DConstraint (c1', c2'), loc)))
adamc@109 575 | DExport (en, sgn, str) =>
adamc@109 576 S.bind2 (mfsg ctx sgn,
adamc@109 577 fn sgn' =>
adamc@109 578 S.map2 (mfst ctx str,
adamc@109 579 fn str' =>
adamc@109 580 (DExport (en, sgn', str'), loc)))
adamc@76 581 in
adamc@76 582 mfd
adamc@76 583 end
adamc@76 584
adamc@76 585 fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} =
adamc@76 586 mapfoldB {kind = kind,
adamc@76 587 con = fn () => con,
adamc@76 588 exp = fn () => exp,
adamc@76 589 sgn_item = fn () => sgn_item,
adamc@76 590 sgn = fn () => sgn,
adamc@76 591 str = fn () => str,
adamc@76 592 decl = fn () => decl,
adamc@76 593 bind = fn ((), _) => ()} ()
adamc@76 594
adamc@76 595 fun exists {kind, con, exp, sgn_item, sgn, str, decl} k =
adamc@76 596 case mapfold {kind = fn k => fn () =>
adamc@76 597 if kind k then
adamc@76 598 S.Return ()
adamc@76 599 else
adamc@76 600 S.Continue (k, ()),
adamc@76 601 con = fn c => fn () =>
adamc@76 602 if con c then
adamc@76 603 S.Return ()
adamc@76 604 else
adamc@76 605 S.Continue (c, ()),
adamc@76 606 exp = fn e => fn () =>
adamc@76 607 if exp e then
adamc@76 608 S.Return ()
adamc@76 609 else
adamc@76 610 S.Continue (e, ()),
adamc@76 611 sgn_item = fn sgi => fn () =>
adamc@76 612 if sgn_item sgi then
adamc@76 613 S.Return ()
adamc@76 614 else
adamc@76 615 S.Continue (sgi, ()),
adamc@76 616 sgn = fn x => fn () =>
adamc@76 617 if sgn x then
adamc@76 618 S.Return ()
adamc@76 619 else
adamc@76 620 S.Continue (x, ()),
adamc@76 621 str = fn x => fn () =>
adamc@76 622 if str x then
adamc@76 623 S.Return ()
adamc@76 624 else
adamc@76 625 S.Continue (x, ()),
adamc@76 626 decl = fn x => fn () =>
adamc@76 627 if decl x then
adamc@76 628 S.Return ()
adamc@76 629 else
adamc@76 630 S.Continue (x, ())} k () of
adamc@76 631 S.Return _ => true
adamc@76 632 | S.Continue _ => false
adamc@76 633
adamc@76 634 fun search {kind, con, exp, sgn_item, sgn, str, decl} k =
adamc@76 635 case mapfold {kind = fn x => fn () =>
adamc@76 636 case kind x of
adamc@76 637 NONE => S.Continue (x, ())
adamc@76 638 | SOME v => S.Return v,
adamc@76 639
adamc@76 640 con = fn x => fn () =>
adamc@76 641 case con x of
adamc@76 642 NONE => S.Continue (x, ())
adamc@76 643 | SOME v => S.Return v,
adamc@76 644
adamc@76 645 exp = fn x => fn () =>
adamc@76 646 case exp x of
adamc@76 647 NONE => S.Continue (x, ())
adamc@76 648 | SOME v => S.Return v,
adamc@76 649
adamc@76 650 sgn_item = fn x => fn () =>
adamc@76 651 case sgn_item x of
adamc@76 652 NONE => S.Continue (x, ())
adamc@76 653 | SOME v => S.Return v,
adamc@76 654
adamc@76 655 sgn = fn x => fn () =>
adamc@76 656 case sgn x of
adamc@76 657 NONE => S.Continue (x, ())
adamc@76 658 | SOME v => S.Return v,
adamc@76 659
adamc@76 660 str = fn x => fn () =>
adamc@76 661 case str x of
adamc@76 662 NONE => S.Continue (x, ())
adamc@76 663 | SOME v => S.Return v,
adamc@76 664
adamc@76 665 decl = fn x => fn () =>
adamc@76 666 case decl x of
adamc@76 667 NONE => S.Continue (x, ())
adamc@76 668 | SOME v => S.Return v
adamc@76 669
adamc@76 670 } k () of
adamc@76 671 S.Return x => SOME x
adamc@76 672 | S.Continue _ => NONE
adamc@76 673
adamc@34 674 end
adamc@76 675
adamc@76 676 end