Mercurial > urweb

annotate src/expl_util.sml @ 2291:50ad02829abd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Make cache flushes happen immediately instead of at end of transaction.
author Ziv Scully <ziv@mit.edu>
date Tue, 17 Nov 2015 02:44:37 -0500
parents 1aa9629e3a4c
children
rev   line source
adamc@38 1 (* Copyright (c) 2008, Adam Chlipala
adamc@38 2 * All rights reserved.
adamc@38 3 *
adamc@38 4 * Redistribution and use in source and binary forms, with or without
adamc@38 5 * modification, are permitted provided that the following conditions are met:
adamc@38 6 *
adamc@38 7 * - Redistributions of source code must retain the above copyright notice,
adamc@38 8 * this list of conditions and the following disclaimer.
adamc@38 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@38 10 * this list of conditions and the following disclaimer in the documentation
adamc@38 11 * and/or other materials provided with the distribution.
adamc@38 12 * - The names of contributors may not be used to endorse or promote products
adamc@38 13 * derived from this software without specific prior written permission.
adamc@38 14 *
adamc@38 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@38 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@38 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@38 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@38 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@38 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@38 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@38 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@38 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@38 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@38 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@38 26 *)
adamc@38 27
adamc@38 28 structure ExplUtil :> EXPL_UTIL = struct
adamc@38 29
adamc@38 30 open Expl
adamc@38 31
adamc@38 32 structure S = Search
adamc@38 33
adamc@38 34 structure Kind = struct
adamc@38 35
adamc@624 36 fun mapfoldB {kind, bind} =
adamc@38 37 let
adamc@624 38 fun mfk ctx k acc =
adamc@624 39 S.bindP (mfk' ctx k acc, kind ctx)
adamc@38 40
adamc@624 41 and mfk' ctx (kAll as (k, loc)) =
adamc@38 42 case k of
adamc@38 43 KType => S.return2 kAll
adamc@38 44
adamc@38 45 | KArrow (k1, k2) =>
adamc@624 46 S.bind2 (mfk ctx k1,
adamc@38 47 fn k1' =>
adamc@624 48 S.map2 (mfk ctx k2,
adamc@38 49 fn k2' =>
adamc@38 50 (KArrow (k1', k2'), loc)))
adamc@38 51
adamc@38 52 | KName => S.return2 kAll
adamc@38 53
adamc@38 54 | KRecord k =>
adamc@624 55 S.map2 (mfk ctx k,
adamc@38 56 fn k' =>
adamc@38 57 (KRecord k', loc))
adamc@87 58
adamc@87 59 | KUnit => S.return2 kAll
adamc@213 60
adamc@213 61 | KTuple ks =>
adamc@624 62 S.map2 (ListUtil.mapfold (mfk ctx) ks,
adamc@213 63 fn ks' =>
adamc@213 64 (KTuple ks', loc))
adamc@624 65
adamc@624 66 | KRel _ => S.return2 kAll
adamc@624 67 | KFun (x, k) =>
adamc@624 68 S.map2 (mfk (bind (ctx, x)) k,
adamc@624 69 fn k' =>
adamc@624 70 (KFun (x, k'), loc))
adamc@38 71 in
adamc@38 72 mfk
adamc@38 73 end
adamc@38 74
adamc@624 75 fun mapfold fk =
adamc@624 76 mapfoldB {kind = fn () => fk,
adamc@624 77 bind = fn ((), _) => ()} ()
adamc@624 78
adamc@624 79 fun mapB {kind, bind} ctx k =
adamc@624 80 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@624 81 bind = bind} ctx k () of
adamc@624 82 S.Continue (k, ()) => k
adamc@624 83 | S.Return _ => raise Fail "ExplUtil.Kind.mapB: Impossible"
adamc@624 84
adamc@38 85 fun exists f k =
adamc@38 86 case mapfold (fn k => fn () =>
adamc@38 87 if f k then
adamc@38 88 S.Return ()
adamc@38 89 else
adamc@38 90 S.Continue (k, ())) k () of
adamc@38 91 S.Return _ => true
adamc@38 92 | S.Continue _ => false
adamc@38 93
adamc@38 94 end
adamc@38 95
adamc@38 96 structure Con = struct
adamc@38 97
adamc@38 98 datatype binder =
adamc@624 99 RelK of string
adamc@624 100 | RelC of string * Expl.kind
adamc@624 101 | NamedC of string * Expl.kind
adamc@38 102
adamc@38 103 fun mapfoldB {kind = fk, con = fc, bind} =
adamc@38 104 let
adamc@624 105 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@38 106
adamc@38 107 fun mfc ctx c acc =
adamc@38 108 S.bindP (mfc' ctx c acc, fc ctx)
adamc@38 109
adamc@38 110 and mfc' ctx (cAll as (c, loc)) =
adamc@38 111 case c of
adamc@38 112 TFun (c1, c2) =>
adamc@38 113 S.bind2 (mfc ctx c1,
adamc@38 114 fn c1' =>
adamc@38 115 S.map2 (mfc ctx c2,
adamc@38 116 fn c2' =>
adamc@38 117 (TFun (c1', c2'), loc)))
adamc@38 118 | TCFun (x, k, c) =>
adamc@624 119 S.bind2 (mfk ctx k,
adamc@38 120 fn k' =>
adamc@624 121 S.map2 (mfc (bind (ctx, RelC (x, k))) c,
adamc@38 122 fn c' =>
adamc@38 123 (TCFun (x, k', c'), loc)))
adamc@38 124 | TRecord c =>
adamc@38 125 S.map2 (mfc ctx c,
adamc@38 126 fn c' =>
adamc@38 127 (TRecord c', loc))
adamc@38 128
adamc@38 129 | CRel _ => S.return2 cAll
adamc@38 130 | CNamed _ => S.return2 cAll
adamc@38 131 | CModProj _ => S.return2 cAll
adamc@38 132 | CApp (c1, c2) =>
adamc@38 133 S.bind2 (mfc ctx c1,
adamc@38 134 fn c1' =>
adamc@38 135 S.map2 (mfc ctx c2,
adamc@38 136 fn c2' =>
adamc@38 137 (CApp (c1', c2'), loc)))
adamc@38 138 | CAbs (x, k, c) =>
adamc@624 139 S.bind2 (mfk ctx k,
adamc@38 140 fn k' =>
adamc@624 141 S.map2 (mfc (bind (ctx, RelC (x, k))) c,
adamc@38 142 fn c' =>
adamc@38 143 (CAbs (x, k', c'), loc)))
adamc@38 144
adamc@38 145 | CName _ => S.return2 cAll
adamc@38 146
adamc@38 147 | CRecord (k, xcs) =>
adamc@624 148 S.bind2 (mfk ctx k,
adamc@38 149 fn k' =>
adamc@38 150 S.map2 (ListUtil.mapfold (fn (x, c) =>
adamc@38 151 S.bind2 (mfc ctx x,
adamc@38 152 fn x' =>
adamc@38 153 S.map2 (mfc ctx c,
adamc@38 154 fn c' =>
adamc@38 155 (x', c'))))
adamc@38 156 xcs,
adamc@38 157 fn xcs' =>
adamc@38 158 (CRecord (k', xcs'), loc)))
adamc@38 159 | CConcat (c1, c2) =>
adamc@38 160 S.bind2 (mfc ctx c1,
adamc@38 161 fn c1' =>
adamc@38 162 S.map2 (mfc ctx c2,
adamc@38 163 fn c2' =>
adamc@38 164 (CConcat (c1', c2'), loc)))
adamc@621 165 | CMap (k1, k2) =>
adamc@624 166 S.bind2 (mfk ctx k1,
adamc@68 167 fn k1' =>
adamc@624 168 S.map2 (mfk ctx k2,
adamc@68 169 fn k2' =>
adamc@621 170 (CMap (k1', k2'), loc)))
adamc@87 171
adamc@87 172 | CUnit => S.return2 cAll
adamc@213 173
adamc@213 174 | CTuple cs =>
adamc@213 175 S.map2 (ListUtil.mapfold (mfc ctx) cs,
adamc@213 176 fn cs' =>
adamc@213 177 (CTuple cs', loc))
adamc@213 178
adamc@213 179 | CProj (c, n) =>
adamc@213 180 S.map2 (mfc ctx c,
adamc@213 181 fn c' =>
adamc@213 182 (CProj (c', n), loc))
adamc@624 183
adamc@624 184 | CKAbs (x, c) =>
adamc@624 185 S.map2 (mfc (bind (ctx, RelK x)) c,
adamc@624 186 fn c' =>
adamc@624 187 (CKAbs (x, c'), loc))
adamc@624 188 | CKApp (c, k) =>
adamc@624 189 S.bind2 (mfc ctx c,
adamc@624 190 fn c' =>
adamc@624 191 S.map2 (mfk ctx k,
adamc@624 192 fn k' =>
adamc@624 193 (CKApp (c', k'), loc)))
adamc@624 194 | TKFun (x, c) =>
adamc@624 195 S.map2 (mfc (bind (ctx, RelK x)) c,
adamc@624 196 fn c' =>
adamc@624 197 (TKFun (x, c'), loc))
adamc@38 198 in
adamc@38 199 mfc
adamc@38 200 end
adamc@38 201
adamc@38 202 fun mapfold {kind = fk, con = fc} =
adamc@624 203 mapfoldB {kind = fn () => fk,
adamc@38 204 con = fn () => fc,
adamc@38 205 bind = fn ((), _) => ()} ()
adamc@38 206
adamc@38 207 fun mapB {kind, con, bind} ctx c =
adamc@624 208 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@38 209 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@38 210 bind = bind} ctx c () of
adamc@38 211 S.Continue (c, ()) => c
adamc@38 212 | S.Return _ => raise Fail "ExplUtil.Con.mapB: Impossible"
adamc@38 213
adamc@38 214 fun map {kind, con} s =
adamc@38 215 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@38 216 con = fn c => fn () => S.Continue (con c, ())} s () of
adamc@38 217 S.Return () => raise Fail "ExplUtil.Con.map: Impossible"
adamc@38 218 | S.Continue (s, ()) => s
adamc@38 219
adamc@38 220 fun exists {kind, con} k =
adamc@38 221 case mapfold {kind = fn k => fn () =>
adamc@38 222 if kind k then
adamc@38 223 S.Return ()
adamc@38 224 else
adamc@38 225 S.Continue (k, ()),
adamc@38 226 con = fn c => fn () =>
adamc@38 227 if con c then
adamc@38 228 S.Return ()
adamc@38 229 else
adamc@38 230 S.Continue (c, ())} k () of
adamc@38 231 S.Return _ => true
adamc@38 232 | S.Continue _ => false
adamc@38 233
adamc@38 234 end
adamc@38 235
adamc@38 236 structure Exp = struct
adamc@38 237
adamc@38 238 datatype binder =
adamc@624 239 RelK of string
adamc@624 240 | RelC of string * Expl.kind
adamc@38 241 | NamedC of string * Expl.kind
adamc@38 242 | RelE of string * Expl.con
adamc@38 243 | NamedE of string * Expl.con
adamc@38 244
adamc@38 245 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
adamc@38 246 let
adamc@624 247 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@38 248
adamc@38 249 fun bind' (ctx, b) =
adamc@38 250 let
adamc@38 251 val b' = case b of
adamc@624 252 Con.RelK x => RelK x
adamc@624 253 | Con.RelC x => RelC x
adamc@624 254 | Con.NamedC x => NamedC x
adamc@38 255 in
adamc@38 256 bind (ctx, b')
adamc@38 257 end
adamc@38 258 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@38 259
adamc@38 260 fun mfe ctx e acc =
adamc@38 261 S.bindP (mfe' ctx e acc, fe ctx)
adamc@38 262
adamc@38 263 and mfe' ctx (eAll as (e, loc)) =
adamc@38 264 case e of
adamc@38 265 EPrim _ => S.return2 eAll
adamc@38 266 | ERel _ => S.return2 eAll
adamc@38 267 | ENamed _ => S.return2 eAll
adamc@38 268 | EModProj _ => S.return2 eAll
adamc@38 269 | EApp (e1, e2) =>
adamc@38 270 S.bind2 (mfe ctx e1,
adamc@38 271 fn e1' =>
adamc@38 272 S.map2 (mfe ctx e2,
adamc@38 273 fn e2' =>
adamc@38 274 (EApp (e1', e2'), loc)))
adamc@38 275 | EAbs (x, dom, ran, e) =>
adamc@38 276 S.bind2 (mfc ctx dom,
adamc@38 277 fn dom' =>
adamc@38 278 S.bind2 (mfc ctx ran,
adamc@38 279 fn ran' =>
adamc@38 280 S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
adamc@38 281 fn e' =>
adamc@38 282 (EAbs (x, dom', ran', e'), loc))))
adamc@38 283
adamc@38 284 | ECApp (e, c) =>
adamc@38 285 S.bind2 (mfe ctx e,
adamc@38 286 fn e' =>
adamc@38 287 S.map2 (mfc ctx c,
adamc@38 288 fn c' =>
adamc@38 289 (ECApp (e', c'), loc)))
adamc@38 290 | ECAbs (x, k, e) =>
adamc@624 291 S.bind2 (mfk ctx k,
adamc@38 292 fn k' =>
adamc@38 293 S.map2 (mfe (bind (ctx, RelC (x, k))) e,
adamc@38 294 fn e' =>
adamc@38 295 (ECAbs (x, k', e'), loc)))
adamc@38 296
adamc@38 297 | ERecord xes =>
adamc@38 298 S.map2 (ListUtil.mapfold (fn (x, e, t) =>
adamc@38 299 S.bind2 (mfc ctx x,
adamc@38 300 fn x' =>
adamc@38 301 S.bind2 (mfe ctx e,
adamc@38 302 fn e' =>
adamc@38 303 S.map2 (mfc ctx t,
adamc@38 304 fn t' =>
adamc@38 305 (x', e', t')))))
adamc@38 306 xes,
adamc@38 307 fn xes' =>
adamc@38 308 (ERecord xes', loc))
adamc@38 309 | EField (e, c, {field, rest}) =>
adamc@38 310 S.bind2 (mfe ctx e,
adamc@38 311 fn e' =>
adamc@38 312 S.bind2 (mfc ctx c,
adamc@38 313 fn c' =>
adamc@38 314 S.bind2 (mfc ctx field,
adamc@38 315 fn field' =>
adamc@38 316 S.map2 (mfc ctx rest,
adamc@38 317 fn rest' =>
adamc@38 318 (EField (e', c', {field = field', rest = rest'}), loc)))))
adamc@445 319 | EConcat (e1, c1, e2, c2) =>
adamc@339 320 S.bind2 (mfe ctx e1,
adamc@339 321 fn e1' =>
adamc@445 322 S.bind2 (mfc ctx c1,
adamc@445 323 fn c1' =>
adamc@339 324 S.bind2 (mfe ctx e2,
adamc@339 325 fn e2' =>
adamc@445 326 S.map2 (mfc ctx c2,
adamc@445 327 fn c2' =>
adamc@445 328 (EConcat (e1', c1', e2', c2'),
adamc@445 329 loc)))))
adamc@149 330 | ECut (e, c, {field, rest}) =>
adamc@149 331 S.bind2 (mfe ctx e,
adamc@149 332 fn e' =>
adamc@149 333 S.bind2 (mfc ctx c,
adamc@149 334 fn c' =>
adamc@149 335 S.bind2 (mfc ctx field,
adamc@149 336 fn field' =>
adamc@149 337 S.map2 (mfc ctx rest,
adamc@149 338 fn rest' =>
adamc@149 339 (ECut (e', c', {field = field', rest = rest'}), loc)))))
adamc@493 340 | ECutMulti (e, c, {rest}) =>
adamc@493 341 S.bind2 (mfe ctx e,
adamc@493 342 fn e' =>
adamc@493 343 S.bind2 (mfc ctx c,
adamc@493 344 fn c' =>
adamc@493 345 S.map2 (mfc ctx rest,
adamc@493 346 fn rest' =>
adamc@493 347 (ECutMulti (e', c', {rest = rest'}), loc))))
adamc@109 348
adamc@109 349 | EWrite e =>
adamc@109 350 S.map2 (mfe ctx e,
adamc@109 351 fn e' =>
adamc@109 352 (EWrite e', loc))
adamc@176 353
adamc@182 354 | ECase (e, pes, {disc, result}) =>
adamc@176 355 S.bind2 (mfe ctx e,
adamc@176 356 fn e' =>
adamc@176 357 S.bind2 (ListUtil.mapfold (fn (p, e) =>
adamc@176 358 S.map2 (mfe ctx e,
adamc@176 359 fn e' => (p, e'))) pes,
adamc@176 360 fn pes' =>
adamc@182 361 S.bind2 (mfc ctx disc,
adamc@182 362 fn disc' =>
adamc@182 363 S.map2 (mfc ctx result,
adamc@182 364 fn result' =>
adamc@182 365 (ECase (e', pes', {disc = disc', result = result'}), loc)))))
adamc@449 366
adamc@449 367 | ELet (x, t, e1, e2) =>
adamc@449 368 S.bind2 (mfc ctx t,
adamc@449 369 fn t' =>
adamc@449 370 S.bind2 (mfe ctx e1,
adamc@449 371 fn e1' =>
adamc@453 372 S.map2 (mfe (bind (ctx, RelE (x, t))) e2,
adamc@449 373 fn e2' =>
adamc@449 374 (ELet (x, t', e1', e2'), loc))))
adamc@624 375
adamc@624 376 | EKAbs (x, e) =>
adamc@624 377 S.map2 (mfe (bind (ctx, RelK x)) e,
adamc@624 378 fn e' =>
adamc@624 379 (EKAbs (x, e'), loc))
adamc@624 380 | EKApp (e, k) =>
adamc@624 381 S.bind2 (mfe ctx e,
adamc@624 382 fn e' =>
adamc@624 383 S.map2 (mfk ctx k,
adamc@624 384 fn k' =>
adamc@624 385 (EKApp (e', k'), loc)))
adamc@38 386 in
adamc@38 387 mfe
adamc@38 388 end
adamc@38 389
adamc@38 390 fun mapfold {kind = fk, con = fc, exp = fe} =
adamc@624 391 mapfoldB {kind = fn () => fk,
adamc@38 392 con = fn () => fc,
adamc@38 393 exp = fn () => fe,
adamc@38 394 bind = fn ((), _) => ()} ()
adamc@38 395
adamc@38 396 fun exists {kind, con, exp} k =
adamc@38 397 case mapfold {kind = fn k => fn () =>
adamc@38 398 if kind k then
adamc@38 399 S.Return ()
adamc@38 400 else
adamc@38 401 S.Continue (k, ()),
adamc@38 402 con = fn c => fn () =>
adamc@38 403 if con c then
adamc@38 404 S.Return ()
adamc@38 405 else
adamc@38 406 S.Continue (c, ()),
adamc@38 407 exp = fn e => fn () =>
adamc@38 408 if exp e then
adamc@38 409 S.Return ()
adamc@38 410 else
adamc@38 411 S.Continue (e, ())} k () of
adamc@38 412 S.Return _ => true
adamc@38 413 | S.Continue _ => false
adamc@38 414
adamc@38 415 end
adamc@38 416
adamc@38 417 structure Sgn = struct
adamc@38 418
adamc@38 419 datatype binder =
adamc@624 420 RelK of string
adamc@624 421 | RelC of string * Expl.kind
adamc@38 422 | NamedC of string * Expl.kind
adamc@38 423 | Str of string * Expl.sgn
adamc@64 424 | Sgn of string * Expl.sgn
adamc@38 425
adamc@38 426 fun mapfoldB {kind, con, sgn_item, sgn, bind} =
adamc@38 427 let
adamc@38 428 fun bind' (ctx, b) =
adamc@38 429 let
adamc@38 430 val b' = case b of
adamc@624 431 Con.RelK x => RelK x
adamc@624 432 | Con.RelC x => RelC x
adamc@624 433 | Con.NamedC x => NamedC x
adamc@38 434 in
adamc@38 435 bind (ctx, b')
adamc@38 436 end
adamc@38 437 val con = Con.mapfoldB {kind = kind, con = con, bind = bind'}
adamc@38 438
adamc@624 439 val kind = Kind.mapfoldB {kind = kind, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@38 440
adamc@38 441 fun sgi ctx si acc =
adamc@38 442 S.bindP (sgi' ctx si acc, sgn_item ctx)
adamc@38 443
adamc@162 444 and sgi' ctx (siAll as (si, loc)) =
adamc@38 445 case si of
adamc@38 446 SgiConAbs (x, n, k) =>
adamc@624 447 S.map2 (kind ctx k,
adamc@38 448 fn k' =>
adamc@38 449 (SgiConAbs (x, n, k'), loc))
adamc@38 450 | SgiCon (x, n, k, c) =>
adamc@624 451 S.bind2 (kind ctx k,
adamc@38 452 fn k' =>
adamc@38 453 S.map2 (con ctx c,
adamc@38 454 fn c' =>
adamc@38 455 (SgiCon (x, n, k', c'), loc)))
adamc@806 456 | SgiDatatype dts =>
adamc@806 457 S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
adamc@806 458 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@806 459 case c of
adamc@806 460 NONE => S.return2 (x, n, c)
adamc@806 461 | SOME c =>
adamc@806 462 S.map2 (con ctx c,
adamc@806 463 fn c' => (x, n, SOME c'))) xncs,
adamc@806 464 fn xncs' => (x, n, xs, xncs'))) dts,
adamc@806 465 fn dts' =>
adamc@806 466 (SgiDatatype dts', loc))
adamc@191 467 | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
adamc@162 468 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@162 469 case c of
adamc@162 470 NONE => S.return2 (x, n, c)
adamc@162 471 | SOME c =>
adamc@162 472 S.map2 (con ctx c,
adamc@162 473 fn c' => (x, n, SOME c'))) xncs,
adamc@162 474 fn xncs' =>
adamc@191 475 (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
adamc@38 476 | SgiVal (x, n, c) =>
adamc@38 477 S.map2 (con ctx c,
adamc@38 478 fn c' =>
adamc@38 479 (SgiVal (x, n, c'), loc))
adamc@38 480 | SgiStr (x, n, s) =>
adamc@38 481 S.map2 (sg ctx s,
adamc@38 482 fn s' =>
adamc@38 483 (SgiStr (x, n, s'), loc))
adamc@64 484 | SgiSgn (x, n, s) =>
adamc@64 485 S.map2 (sg ctx s,
adamc@64 486 fn s' =>
adamc@64 487 (SgiSgn (x, n, s'), loc))
adamc@38 488
adamc@38 489 and sg ctx s acc =
adamc@38 490 S.bindP (sg' ctx s acc, sgn ctx)
adamc@38 491
adamc@38 492 and sg' ctx (sAll as (s, loc)) =
adamc@38 493 case s of
adamc@38 494 SgnConst sgis =>
adamc@38 495 S.map2 (ListUtil.mapfoldB (fn (ctx, si) =>
adamc@38 496 (case #1 si of
adamc@38 497 SgiConAbs (x, _, k) =>
adamc@38 498 bind (ctx, NamedC (x, k))
adamc@38 499 | SgiCon (x, _, k, _) =>
adamc@38 500 bind (ctx, NamedC (x, k))
adamc@806 501 | SgiDatatype dts =>
adamc@806 502 foldl (fn ((x, _, ks, _), ctx) =>
adamc@806 503 let
adamc@806 504 val k' = (KType, loc)
adamc@806 505 val k = foldl (fn (_, k) => (KArrow (k', k), loc))
adamc@806 506 k' ks
adamc@806 507 in
adamc@806 508 bind (ctx, NamedC (x, k))
adamc@806 509 end) ctx dts
adamc@191 510 | SgiDatatypeImp (x, _, _, _, _, _, _) =>
adamc@162 511 bind (ctx, NamedC (x, (KType, loc)))
adamc@38 512 | SgiVal _ => ctx
adamc@38 513 | SgiStr (x, _, sgn) =>
adamc@64 514 bind (ctx, Str (x, sgn))
adamc@64 515 | SgiSgn (x, _, sgn) =>
adamc@460 516 bind (ctx, Sgn (x, sgn)),
adamc@38 517 sgi ctx si)) ctx sgis,
adamc@38 518 fn sgis' =>
adamc@38 519 (SgnConst sgis', loc))
adamc@38 520
adamc@38 521 | SgnVar _ => S.return2 sAll
adamc@45 522
adamc@45 523 | SgnFun (m, n, s1, s2) =>
adamc@45 524 S.bind2 (sg ctx s1,
adamc@45 525 fn s1' =>
adamc@45 526 S.map2 (sg (bind (ctx, Str (m, s1'))) s2,
adamc@45 527 fn s2' =>
adamc@45 528 (SgnFun (m, n, s1', s2'), loc)))
adam@1864 529 | SgnWhere (sgn, ms, x, c) =>
adamc@45 530 S.bind2 (sg ctx sgn,
adamc@45 531 fn sgn' =>
adamc@45 532 S.map2 (con ctx c,
adamc@45 533 fn c' =>
adam@1864 534 (SgnWhere (sgn', ms, x, c'), loc)))
adamc@64 535 | SgnProj _ => S.return2 sAll
adamc@38 536 in
adamc@38 537 sg
adamc@38 538 end
adamc@38 539
adamc@38 540 fun mapfold {kind, con, sgn_item, sgn} =
adamc@624 541 mapfoldB {kind = fn () => kind,
adamc@38 542 con = fn () => con,
adamc@38 543 sgn_item = fn () => sgn_item,
adamc@38 544 sgn = fn () => sgn,
adamc@38 545 bind = fn ((), _) => ()} ()
adamc@38 546
adamc@38 547 fun map {kind, con, sgn_item, sgn} s =
adamc@38 548 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@38 549 con = fn c => fn () => S.Continue (con c, ()),
adamc@38 550 sgn_item = fn si => fn () => S.Continue (sgn_item si, ()),
adamc@38 551 sgn = fn s => fn () => S.Continue (sgn s, ())} s () of
adamc@38 552 S.Return () => raise Fail "Expl_util.Sgn.map"
adamc@38 553 | S.Continue (s, ()) => s
adamc@38 554
adamc@38 555 end
adamc@38 556
adamc@38 557 end