Mercurial > urweb

annotate src/core_util.sml @ 1327:1cc67fdac4d3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New argument to transactional free functions, to specify whether we are about to retry
author Adam Chlipala <adam@chlipala.net>
date Sat, 04 Dec 2010 11:15:20 -0500
parents b4480a56cab7
children 0577be31a435
rev   line source
adamc@1185 1 (* Copyright (c) 2008-2010, Adam Chlipala
adamc@16 2 * All rights reserved.
adamc@16 3 *
adamc@16 4 * Redistribution and use in source and binary forms, with or without
adamc@16 5 * modification, are permitted provided that the following conditions are met:
adamc@16 6 *
adamc@16 7 * - Redistributions of source code must retain the above copyright notice,
adamc@16 8 * this list of conditions and the following disclaimer.
adamc@16 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@16 10 * this list of conditions and the following disclaimer in the documentation
adamc@16 11 * and/or other materials provided with the distribution.
adamc@16 12 * - The names of contributors may not be used to endorse or promote products
adamc@16 13 * derived from this software without specific prior written permission.
adamc@16 14 *
adamc@16 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@16 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@16 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@16 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@16 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@16 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@16 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@16 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@16 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@16 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@16 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@16 26 *)
adamc@16 27
adamc@16 28 structure CoreUtil :> CORE_UTIL = struct
adamc@16 29
adamc@16 30 open Core
adamc@16 31
adamc@16 32 structure S = Search
adamc@16 33
adamc@16 34 structure Kind = struct
adamc@16 35
adamc@193 36 open Order
adamc@193 37
adamc@193 38 fun compare ((k1, _), (k2, _)) =
adamc@193 39 case (k1, k2) of
adamc@193 40 (KType, KType) => EQUAL
adamc@193 41 | (KType, _) => LESS
adamc@193 42 | (_, KType) => GREATER
adamc@193 43
adamc@193 44 | (KArrow (d1, r1), KArrow (d2, r2)) => join (compare (d1, d2), fn () => compare (r1, r2))
adamc@193 45 | (KArrow _, _) => LESS
adamc@193 46 | (_, KArrow _) => GREATER
adamc@193 47
adamc@193 48 | (KName, KName) => EQUAL
adamc@193 49 | (KName, _) => LESS
adamc@193 50 | (_, KName) => GREATER
adamc@193 51
adamc@193 52 | (KRecord k1, KRecord k2) => compare (k1, k2)
adamc@193 53 | (KRecord _, _) => LESS
adamc@193 54 | (_, KRecord _) => GREATER
adamc@193 55
adamc@193 56 | (KUnit, KUnit) => EQUAL
adamc@214 57 | (KUnit, _) => LESS
adamc@214 58 | (_, KUnit) => GREATER
adamc@214 59
adamc@214 60 | (KTuple ks1, KTuple ks2) => joinL compare (ks1, ks2)
adamc@626 61 | (KTuple _, _) => LESS
adamc@626 62 | (_, KTuple _) => GREATER
adamc@193 63
adamc@626 64 | (KRel n1, KRel n2) => Int.compare (n1, n2)
adamc@626 65 | (KRel _, _) => LESS
adamc@626 66 | (_, KRel _) => GREATER
adamc@626 67
adamc@626 68 | (KFun (_, k1), KFun (_, k2)) => compare (k1, k2)
adamc@626 69
adamc@626 70 fun mapfoldB {kind = f, bind} =
adamc@16 71 let
adamc@626 72 fun mfk ctx k acc =
adamc@626 73 S.bindP (mfk' ctx k acc, f ctx)
adamc@16 74
adamc@626 75 and mfk' ctx (kAll as (k, loc)) =
adamc@16 76 case k of
adamc@16 77 KType => S.return2 kAll
adamc@16 78
adamc@16 79 | KArrow (k1, k2) =>
adamc@626 80 S.bind2 (mfk ctx k1,
adamc@16 81 fn k1' =>
adamc@626 82 S.map2 (mfk ctx k2,
adamc@16 83 fn k2' =>
adamc@16 84 (KArrow (k1', k2'), loc)))
adamc@16 85
adamc@16 86 | KName => S.return2 kAll
adamc@16 87
adamc@16 88 | KRecord k =>
adamc@626 89 S.map2 (mfk ctx k,
adamc@16 90 fn k' =>
adamc@16 91 (KRecord k', loc))
adamc@87 92
adamc@87 93 | KUnit => S.return2 kAll
adamc@214 94
adamc@214 95 | KTuple ks =>
adamc@626 96 S.map2 (ListUtil.mapfold (mfk ctx) ks,
adamc@214 97 fn ks' =>
adamc@214 98 (KTuple ks', loc))
adamc@626 99
adamc@626 100 | KRel _ => S.return2 kAll
adamc@626 101 | KFun (x, k) =>
adamc@626 102 S.map2 (mfk (bind (ctx, x)) k,
adamc@626 103 fn k' =>
adamc@626 104 (KFun (x, k'), loc))
adamc@16 105 in
adamc@16 106 mfk
adamc@16 107 end
adamc@16 108
adamc@626 109 fun mapfold fk =
adamc@626 110 mapfoldB {kind = fn () => fk,
adamc@626 111 bind = fn ((), _) => ()} ()
adamc@626 112
adamc@16 113 fun map f k =
adamc@16 114 case mapfold (fn k => fn () => S.Continue (f k, ())) k () of
adamc@626 115 S.Return () => raise Fail "CoreUtil.Kind.map"
adamc@16 116 | S.Continue (k, ()) => k
adamc@16 117
adamc@626 118 fun mapB {kind, bind} ctx k =
adamc@626 119 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@626 120 bind = bind} ctx k () of
adamc@626 121 S.Continue (k, ()) => k
adamc@626 122 | S.Return _ => raise Fail "CoreUtil.Kind.mapB: Impossible"
adamc@626 123
adamc@16 124 fun exists f k =
adamc@16 125 case mapfold (fn k => fn () =>
adamc@16 126 if f k then
adamc@16 127 S.Return ()
adamc@16 128 else
adamc@16 129 S.Continue (k, ())) k () of
adamc@16 130 S.Return _ => true
adamc@16 131 | S.Continue _ => false
adamc@16 132
adamc@16 133 end
adamc@16 134
adamc@16 135 structure Con = struct
adamc@16 136
adamc@193 137 open Order
adamc@193 138
adamc@193 139 fun compare ((c1, _), (c2, _)) =
adamc@193 140 case (c1, c2) of
adamc@193 141 (TFun (d1, r1), TFun (d2, r2)) => join (compare (d1, d2), fn () => compare (r1, r2))
adamc@193 142 | (TFun _, _) => LESS
adamc@193 143 | (_, TFun _) => GREATER
adamc@193 144
adamc@193 145 | (TCFun (x1, k1, r1), TCFun (x2, k2, r2)) =>
adamc@193 146 join (String.compare (x1, x2),
adamc@193 147 fn () => join (Kind.compare (k1, k2),
adamc@193 148 fn () => compare (r1, r2)))
adamc@193 149 | (TCFun _, _) => LESS
adamc@193 150 | (_, TCFun _) => GREATER
adamc@193 151
adamc@193 152 | (TRecord c1, TRecord c2) => compare (c1, c2)
adamc@193 153 | (TRecord _, _) => LESS
adamc@193 154 | (_, TRecord _) => GREATER
adamc@193 155
adamc@193 156 | (CRel n1, CRel n2) => Int.compare (n1, n2)
adamc@193 157 | (CRel _, _) => LESS
adamc@193 158 | (_, CRel _) => GREATER
adamc@193 159
adamc@193 160 | (CNamed n1, CNamed n2) => Int.compare (n1, n2)
adamc@193 161 | (CNamed _, _) => LESS
adamc@193 162 | (_, CNamed _) => GREATER
adamc@193 163
adamc@193 164 | (CFfi (m1, s1), CFfi (m2, s2)) => join (String.compare (m1, m2),
adamc@193 165 fn () => String.compare (s1, s2))
adamc@193 166 | (CFfi _, _) => LESS
adamc@193 167 | (_, CFfi _) => GREATER
adamc@193 168
adamc@193 169 | (CApp (f1, x1), CApp (f2, x2)) => join (compare (f1, f2),
adamc@193 170 fn () => compare (x1, x2))
adamc@193 171 | (CApp _, _) => LESS
adamc@193 172 | (_, CApp _) => GREATER
adamc@193 173
adamc@193 174 | (CAbs (x1, k1, b1), CAbs (x2, k2, b2)) =>
adamc@193 175 join (String.compare (x1, x2),
adamc@193 176 fn () => join (Kind.compare (k1, k2),
adamc@193 177 fn () => compare (b1, b2)))
adamc@193 178 | (CAbs _, _) => LESS
adamc@193 179 | (_, CAbs _) => GREATER
adamc@193 180
adamc@193 181 | (CName s1, CName s2) => String.compare (s1, s2)
adamc@193 182 | (CName _, _) => LESS
adamc@193 183 | (_, CName _) => GREATER
adamc@193 184
adamc@193 185 | (CRecord (k1, xvs1), CRecord (k2, xvs2)) =>
adamc@193 186 join (Kind.compare (k1, k2),
adamc@250 187 fn () =>
adamc@250 188 let
adamc@250 189 val sort = ListMergeSort.sort (fn ((x1, _), (x2, _)) =>
adamc@250 190 compare (x1, x2) = GREATER)
adamc@250 191 in
adamc@250 192 joinL (fn ((x1, v1), (x2, v2)) =>
adamc@250 193 join (compare (x1, x2),
adamc@250 194 fn () => compare (v1, v2))) (sort xvs1, sort xvs2)
adamc@250 195 end)
adamc@193 196 | (CRecord _, _) => LESS
adamc@193 197 | (_, CRecord _) => GREATER
adamc@193 198
adamc@193 199 | (CConcat (f1, s1), CConcat (f2, s2)) =>
adamc@193 200 join (compare (f1, f2),
adamc@193 201 fn () => compare (s1, s2))
adamc@193 202 | (CConcat _, _) => LESS
adamc@193 203 | (_, CConcat _) => GREATER
adamc@193 204
adamc@621 205 | (CMap (d1, r1), CMap (d2, r2)) =>
adamc@193 206 join (Kind.compare (d1, r2),
adamc@193 207 fn () => Kind.compare (r1, r2))
adamc@621 208 | (CMap _, _) => LESS
adamc@621 209 | (_, CMap _) => GREATER
adamc@193 210
adamc@193 211 | (CUnit, CUnit) => EQUAL
adamc@214 212 | (CUnit, _) => LESS
adamc@214 213 | (_, CUnit) => GREATER
adamc@214 214
adamc@214 215 | (CTuple cs1, CTuple cs2) => joinL compare (cs1, cs2)
adamc@214 216 | (CTuple _, _) => LESS
adamc@214 217 | (_, CTuple _) => GREATER
adamc@214 218
adamc@214 219 | (CProj (c1, n1), CProj (c2, n2)) => join (Int.compare (n1, n2),
adamc@214 220 fn () => compare (c1, c2))
adamc@626 221 | (CProj _, _) => LESS
adamc@626 222 | (_, CProj _) => GREATER
adamc@626 223
adamc@626 224 | (CKAbs (_, c1), CKAbs (_, c2)) => compare (c1, c2)
adamc@626 225 | (CKAbs _, _) => LESS
adamc@626 226 | (_, CKAbs _) => GREATER
adamc@626 227
adamc@626 228 | (CKApp (c1, k1), CKApp (c2, k2)) =>
adamc@626 229 join (compare (c1, c2),
adamc@626 230 fn () => Kind.compare (k1, k2))
adamc@626 231 | (CKApp _, _) => LESS
adamc@626 232 | (_, CKApp _) => GREATER
adamc@626 233
adamc@626 234 | (TKFun (_, c1), TKFun (_, c2)) => compare (c1, c2)
adamc@193 235
adamc@16 236 datatype binder =
adamc@626 237 RelK of string
adamc@626 238 | RelC of string * kind
adamc@626 239 | NamedC of string * int * kind * con option
adamc@16 240
adamc@16 241 fun mapfoldB {kind = fk, con = fc, bind} =
adamc@16 242 let
adamc@626 243 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@16 244
adamc@16 245 fun mfc ctx c acc =
adamc@16 246 S.bindP (mfc' ctx c acc, fc ctx)
adamc@16 247
adamc@16 248 and mfc' ctx (cAll as (c, loc)) =
adamc@16 249 case c of
adamc@16 250 TFun (c1, c2) =>
adamc@16 251 S.bind2 (mfc ctx c1,
adamc@16 252 fn c1' =>
adamc@16 253 S.map2 (mfc ctx c2,
adamc@16 254 fn c2' =>
adamc@16 255 (TFun (c1', c2'), loc)))
adamc@16 256 | TCFun (x, k, c) =>
adamc@626 257 S.bind2 (mfk ctx k,
adamc@16 258 fn k' =>
adamc@626 259 S.map2 (mfc (bind (ctx, RelC (x, k))) c,
adamc@16 260 fn c' =>
adamc@16 261 (TCFun (x, k', c'), loc)))
adamc@16 262 | TRecord c =>
adamc@16 263 S.map2 (mfc ctx c,
adamc@16 264 fn c' =>
adamc@16 265 (TRecord c', loc))
adamc@16 266
adamc@16 267 | CRel _ => S.return2 cAll
adamc@16 268 | CNamed _ => S.return2 cAll
adamc@48 269 | CFfi _ => S.return2 cAll
adamc@16 270 | CApp (c1, c2) =>
adamc@16 271 S.bind2 (mfc ctx c1,
adamc@16 272 fn c1' =>
adamc@16 273 S.map2 (mfc ctx c2,
adamc@16 274 fn c2' =>
adamc@16 275 (CApp (c1', c2'), loc)))
adamc@16 276 | CAbs (x, k, c) =>
adamc@626 277 S.bind2 (mfk ctx k,
adamc@16 278 fn k' =>
adamc@626 279 S.map2 (mfc (bind (ctx, RelC (x, k))) c,
adamc@16 280 fn c' =>
adamc@16 281 (CAbs (x, k', c'), loc)))
adamc@16 282
adamc@16 283 | CName _ => S.return2 cAll
adamc@16 284
adamc@16 285 | CRecord (k, xcs) =>
adamc@626 286 S.bind2 (mfk ctx k,
adamc@16 287 fn k' =>
adamc@16 288 S.map2 (ListUtil.mapfold (fn (x, c) =>
adamc@16 289 S.bind2 (mfc ctx x,
adamc@16 290 fn x' =>
adamc@16 291 S.map2 (mfc ctx c,
adamc@16 292 fn c' =>
adamc@16 293 (x', c'))))
adamc@16 294 xcs,
adamc@16 295 fn xcs' =>
adamc@16 296 (CRecord (k', xcs'), loc)))
adamc@16 297 | CConcat (c1, c2) =>
adamc@16 298 S.bind2 (mfc ctx c1,
adamc@16 299 fn c1' =>
adamc@16 300 S.map2 (mfc ctx c2,
adamc@16 301 fn c2' =>
adamc@16 302 (CConcat (c1', c2'), loc)))
adamc@621 303 | CMap (k1, k2) =>
adamc@626 304 S.bind2 (mfk ctx k1,
adamc@69 305 fn k1' =>
adamc@626 306 S.map2 (mfk ctx k2,
adamc@69 307 fn k2' =>
adamc@621 308 (CMap (k1', k2'), loc)))
adamc@87 309
adamc@87 310 | CUnit => S.return2 cAll
adamc@214 311
adamc@214 312 | CTuple cs =>
adamc@214 313 S.map2 (ListUtil.mapfold (mfc ctx) cs,
adamc@214 314 fn cs' =>
adamc@214 315 (CTuple cs', loc))
adamc@214 316
adamc@214 317 | CProj (c, n) =>
adamc@214 318 S.map2 (mfc ctx c,
adamc@214 319 fn c' =>
adamc@214 320 (CProj (c', n), loc))
adamc@626 321
adamc@626 322 | CKAbs (x, c) =>
adamc@626 323 S.map2 (mfc (bind (ctx, RelK x)) c,
adamc@626 324 fn c' =>
adamc@626 325 (CKAbs (x, c'), loc))
adamc@626 326 | CKApp (c, k) =>
adamc@626 327 S.bind2 (mfc ctx c,
adamc@626 328 fn c' =>
adamc@626 329 S.map2 (mfk ctx k,
adamc@626 330 fn k' =>
adamc@626 331 (CKApp (c', k'), loc)))
adamc@626 332 | TKFun (x, c) =>
adamc@626 333 S.map2 (mfc (bind (ctx, RelK x)) c,
adamc@626 334 fn c' =>
adamc@626 335 (TKFun (x, c'), loc))
adamc@16 336 in
adamc@16 337 mfc
adamc@16 338 end
adamc@16 339
adamc@16 340 fun mapfold {kind = fk, con = fc} =
adamc@626 341 mapfoldB {kind = fn () => fk,
adamc@16 342 con = fn () => fc,
adamc@16 343 bind = fn ((), _) => ()} ()
adamc@16 344
adamc@16 345 fun map {kind, con} c =
adamc@16 346 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@16 347 con = fn c => fn () => S.Continue (con c, ())} c () of
adamc@16 348 S.Return () => raise Fail "Core_util.Con.map"
adamc@16 349 | S.Continue (c, ()) => c
adamc@16 350
adamc@16 351 fun mapB {kind, con, bind} ctx c =
adamc@626 352 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@16 353 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@16 354 bind = bind} ctx c () of
adamc@16 355 S.Continue (c, ()) => c
adamc@20 356 | S.Return _ => raise Fail "CoreUtil.Con.mapB: Impossible"
adamc@16 357
adamc@23 358 fun fold {kind, con} s c =
adamc@23 359 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
adamc@23 360 con = fn c => fn s => S.Continue (c, con (c, s))} c s of
adamc@23 361 S.Continue (_, s) => s
adamc@23 362 | S.Return _ => raise Fail "CoreUtil.Con.fold: Impossible"
adamc@23 363
adamc@16 364 fun exists {kind, con} k =
adamc@16 365 case mapfold {kind = fn k => fn () =>
adamc@16 366 if kind k then
adamc@16 367 S.Return ()
adamc@16 368 else
adamc@16 369 S.Continue (k, ()),
adamc@16 370 con = fn c => fn () =>
adamc@16 371 if con c then
adamc@16 372 S.Return ()
adamc@16 373 else
adamc@16 374 S.Continue (c, ())} k () of
adamc@16 375 S.Return _ => true
adamc@16 376 | S.Continue _ => false
adamc@16 377
adamc@1185 378 fun existsB {kind, con, bind} ctx c =
adamc@1185 379 case mapfoldB {kind = fn ctx => fn k => fn () =>
adamc@1185 380 if kind (ctx, k) then
adamc@1185 381 S.Return ()
adamc@1185 382 else
adamc@1185 383 S.Continue (k, ()),
adamc@1185 384 con = fn ctx => fn c => fn () =>
adamc@1185 385 if con (ctx, c) then
adamc@1185 386 S.Return ()
adamc@1185 387 else
adamc@1185 388 S.Continue (c, ()),
adamc@1185 389 bind = bind} ctx c () of
adamc@1185 390 S.Return _ => true
adamc@1185 391 | S.Continue _ => false
adamc@1185 392
adamc@193 393 fun foldMap {kind, con} s c =
adamc@193 394 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
adamc@193 395 con = fn c => fn s => S.Continue (con (c, s))} c s of
adamc@193 396 S.Continue v => v
adamc@193 397 | S.Return _ => raise Fail "CoreUtil.Con.foldMap: Impossible"
adamc@193 398
adamc@16 399 end
adamc@16 400
adamc@16 401 structure Exp = struct
adamc@16 402
adamc@479 403 open Order
adamc@479 404
adamc@479 405 fun pcCompare (pc1, pc2) =
adamc@479 406 case (pc1, pc2) of
adamc@479 407 (PConVar n1, PConVar n2) => Int.compare (n1, n2)
adamc@479 408 | (PConVar _, _) => LESS
adamc@479 409 | (_, PConVar _) => GREATER
adamc@479 410
adamc@479 411 | (PConFfi {mod = m1, datatyp = d1, con = c1, ...},
adamc@479 412 PConFfi {mod = m2, datatyp = d2, con = c2, ...}) =>
adamc@479 413 join (String.compare (m1, m2),
adamc@479 414 fn () => join (String.compare (d1, d2),
adamc@479 415 fn () => String.compare (c1, c2)))
adamc@479 416
adamc@479 417 fun pCompare ((p1, _), (p2, _)) =
adamc@479 418 case (p1, p2) of
adamc@479 419 (PWild, PWild) => EQUAL
adamc@479 420 | (PWild, _) => LESS
adamc@479 421 | (_, PWild) => GREATER
adamc@479 422
adamc@479 423 | (PVar _, PVar _) => EQUAL
adamc@479 424 | (PVar _, _) => LESS
adamc@479 425 | (_, PVar _) => GREATER
adamc@479 426
adamc@479 427 | (PPrim p1, PPrim p2) => Prim.compare (p1, p2)
adamc@479 428 | (PPrim _, _) => LESS
adamc@479 429 | (_, PPrim _) => GREATER
adamc@479 430
adamc@479 431 | (PCon (_, pc1, _, po1), PCon (_, pc2, _, po2)) =>
adamc@479 432 join (pcCompare (pc1, pc2),
adamc@479 433 fn () => joinO pCompare (po1, po2))
adamc@479 434 | (PCon _, _) => LESS
adamc@479 435 | (_, PCon _) => GREATER
adamc@479 436
adamc@479 437 | (PRecord xps1, PRecord xps2) =>
adamc@479 438 joinL (fn ((x1, p1, _), (x2, p2, _)) =>
adamc@479 439 join (String.compare (x1, x2),
adamc@479 440 fn () => pCompare (p1, p2))) (xps1, xps2)
adamc@479 441
adamc@479 442 fun compare ((e1, _), (e2, _)) =
adamc@479 443 case (e1, e2) of
adamc@479 444 (EPrim p1, EPrim p2) => Prim.compare (p1, p2)
adamc@479 445 | (EPrim _, _) => LESS
adamc@479 446 | (_, EPrim _) => GREATER
adamc@479 447
adamc@479 448 | (ERel n1, ERel n2) => Int.compare (n1, n2)
adamc@479 449 | (ERel _, _) => LESS
adamc@479 450 | (_, ERel _) => GREATER
adamc@479 451
adamc@479 452 | (ENamed n1, ENamed n2) => Int.compare (n1, n2)
adamc@479 453 | (ENamed _, _) => LESS
adamc@479 454 | (_, ENamed _) => GREATER
adamc@479 455
adamc@479 456 | (ECon (_, pc1, _, eo1), ECon (_, pc2, _, eo2)) =>
adamc@479 457 join (pcCompare (pc1, pc2),
adamc@479 458 fn () => joinO compare (eo1, eo2))
adamc@479 459 | (ECon _, _) => LESS
adamc@479 460 | (_, ECon _) => GREATER
adamc@479 461
adamc@479 462 | (EFfi (f1, x1), EFfi (f2, x2)) =>
adamc@479 463 join (String.compare (f1, f2),
adamc@479 464 fn () => String.compare (x1, x2))
adamc@479 465 | (EFfi _, _) => LESS
adamc@479 466 | (_, EFfi _) => GREATER
adamc@479 467
adamc@479 468 | (EFfiApp (f1, x1, es1), EFfiApp (f2, x2, es2)) =>
adamc@479 469 join (String.compare (f1, f2),
adamc@479 470 fn () => join (String.compare (x1, x2),
adamc@479 471 fn () => joinL compare (es1, es2)))
adamc@479 472 | (EFfiApp _, _) => LESS
adamc@479 473 | (_, EFfiApp _) => GREATER
adamc@479 474
adamc@479 475 | (EApp (f1, x1), EApp (f2, x2)) =>
adamc@479 476 join (compare (f1, f2),
adamc@479 477 fn () => compare (x1, x2))
adamc@479 478 | (EApp _, _) => LESS
adamc@479 479 | (_, EApp _) => GREATER
adamc@479 480
adamc@479 481 | (EAbs (_, _, _, e1), EAbs (_, _, _, e2)) => compare (e1, e2)
adamc@479 482 | (EAbs _, _) => LESS
adamc@479 483 | (_, EAbs _) => GREATER
adamc@479 484
adamc@479 485 | (ECApp (f1, x1), ECApp (f2, x2)) =>
adamc@479 486 join (compare (f1, f2),
adamc@479 487 fn () => Con.compare (x1, x2))
adamc@479 488 | (ECApp _, _) => LESS
adamc@479 489 | (_, ECApp _) => GREATER
adamc@479 490
adamc@479 491 | (ECAbs (_, _, e1), ECAbs (_, _, e2)) => compare (e1, e2)
adamc@479 492 | (ECAbs _, _) => LESS
adamc@479 493 | (_, ECAbs _) => GREATER
adamc@479 494
adamc@479 495 | (ERecord xes1, ERecord xes2) =>
adamc@479 496 joinL (fn ((x1, e1, _), (x2, e2, _)) =>
adamc@479 497 join (Con.compare (x1, x2),
adamc@479 498 fn () => compare (e1, e2))) (xes1, xes2)
adamc@479 499 | (ERecord _, _) => LESS
adamc@479 500 | (_, ERecord _) => GREATER
adamc@479 501
adamc@479 502 | (EField (e1, c1, _), EField (e2, c2, _)) =>
adamc@479 503 join (compare (e1, e2),
adamc@479 504 fn () => Con.compare (c1, c2))
adamc@479 505 | (EField _, _) => LESS
adamc@479 506 | (_, EField _) => GREATER
adamc@479 507
adamc@479 508 | (EConcat (x1, _, y1, _), EConcat (x2, _, y2, _)) =>
adamc@479 509 join (compare (x1, x2),
adamc@479 510 fn () => compare (y1, y2))
adamc@479 511 | (EConcat _, _) => LESS
adamc@479 512 | (_, EConcat _) => GREATER
adamc@479 513
adamc@479 514 | (ECut (e1, c1, _), ECut (e2, c2, _)) =>
adamc@479 515 join (compare (e1, e2),
adamc@493 516 fn () => Con.compare (c1, c2))
adamc@479 517 | (ECut _, _) => LESS
adamc@479 518 | (_, ECut _) => GREATER
adamc@479 519
adamc@493 520 | (ECutMulti (e1, c1, _), ECutMulti (e2, c2, _)) =>
adamc@493 521 join (compare (e1, e2),
adamc@493 522 fn () => Con.compare (c1, c2))
adamc@493 523 | (ECutMulti _, _) => LESS
adamc@493 524 | (_, ECutMulti _) => GREATER
adamc@493 525
adamc@479 526 | (ECase (e1, pes1, _), ECase (e2, pes2, _)) =>
adamc@479 527 join (compare (e1, e2),
adamc@479 528 fn () => joinL (fn ((p1, e1), (p2, e2)) =>
adamc@479 529 join (pCompare (p1, p2),
adamc@479 530 fn () => compare (e1, e2))) (pes1, pes2))
adamc@479 531 | (ECase _, _) => LESS
adamc@479 532 | (_, ECase _) => GREATER
adamc@479 533
adamc@479 534 | (EWrite e1, EWrite e2) => compare (e1, e2)
adamc@479 535 | (EWrite _, _) => LESS
adamc@479 536 | (_, EWrite _) => GREATER
adamc@479 537
adamc@479 538 | (EClosure (n1, es1), EClosure (n2, es2)) =>
adamc@479 539 join (Int.compare (n1, n2),
adamc@479 540 fn () => joinL compare (es1, es2))
adamc@479 541 | (EClosure _, _) => LESS
adamc@479 542 | (_, EClosure _) => GREATER
adamc@479 543
adamc@479 544 | (ELet (_, _, x1, e1), ELet (_, _, x2, e2)) =>
adamc@479 545 join (compare (x1, x2),
adamc@479 546 fn () => compare (e1, e2))
adamc@607 547 | (ELet _, _) => LESS
adamc@607 548 | (_, ELet _) => GREATER
adamc@607 549
adamc@1020 550 | (EServerCall (n1, es1, _), EServerCall (n2, es2, _)) =>
adamc@607 551 join (Int.compare (n1, n2),
adamc@1020 552 fn () => joinL compare (es1, es2))
adamc@626 553 | (EServerCall _, _) => LESS
adamc@626 554 | (_, EServerCall _) => GREATER
adamc@626 555
adamc@626 556 | (EKAbs (_, e1), EKAbs (_, e2)) => compare (e1, e2)
adamc@626 557 | (EKAbs _, _) => LESS
adamc@626 558 | (_, EKAbs _) => GREATER
adamc@626 559
adamc@626 560 | (EKApp (e1, k1), EKApp (e2, k2)) =>
adamc@626 561 join (compare (e1, e2),
adamc@626 562 fn () => Kind.compare (k1, k2))
adamc@479 563
adamc@16 564 datatype binder =
adamc@626 565 RelK of string
adamc@626 566 | RelC of string * kind
adamc@20 567 | NamedC of string * int * kind * con option
adamc@16 568 | RelE of string * con
adamc@109 569 | NamedE of string * int * con * exp option * string
adamc@16 570
adamc@16 571 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
adamc@16 572 let
adamc@626 573 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@16 574
adamc@16 575 fun bind' (ctx, b) =
adamc@16 576 let
adamc@16 577 val b' = case b of
adamc@626 578 Con.RelK x => RelK x
adamc@626 579 | Con.RelC x => RelC x
adamc@626 580 | Con.NamedC x => NamedC x
adamc@16 581 in
adamc@16 582 bind (ctx, b')
adamc@16 583 end
adamc@16 584 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@16 585
adamc@16 586 fun mfe ctx e acc =
adamc@16 587 S.bindP (mfe' ctx e acc, fe ctx)
adamc@16 588
adamc@16 589 and mfe' ctx (eAll as (e, loc)) =
adamc@16 590 case e of
adamc@16 591 EPrim _ => S.return2 eAll
adamc@16 592 | ERel _ => S.return2 eAll
adamc@16 593 | ENamed _ => S.return2 eAll
adamc@192 594 | ECon (dk, pc, cs, NONE) =>
adamc@192 595 S.map2 (ListUtil.mapfold (mfc ctx) cs,
adamc@192 596 fn cs' =>
adamc@192 597 (ECon (dk, pc, cs', NONE), loc))
adamc@192 598 | ECon (dk, n, cs, SOME e) =>
adamc@192 599 S.bind2 (mfe ctx e,
adamc@192 600 fn e' =>
adamc@192 601 S.map2 (ListUtil.mapfold (mfc ctx) cs,
adamc@192 602 fn cs' =>
adamc@192 603 (ECon (dk, n, cs', SOME e'), loc)))
adamc@48 604 | EFfi _ => S.return2 eAll
adamc@48 605 | EFfiApp (m, x, es) =>
adamc@192 606 S.map2 (ListUtil.mapfold (mfe ctx) es,
adamc@48 607 fn es' =>
adamc@48 608 (EFfiApp (m, x, es'), loc))
adamc@16 609 | EApp (e1, e2) =>
adamc@16 610 S.bind2 (mfe ctx e1,
adamc@16 611 fn e1' =>
adamc@16 612 S.map2 (mfe ctx e2,
adamc@16 613 fn e2' =>
adamc@16 614 (EApp (e1', e2'), loc)))
adamc@26 615 | EAbs (x, dom, ran, e) =>
adamc@26 616 S.bind2 (mfc ctx dom,
adamc@26 617 fn dom' =>
adamc@26 618 S.bind2 (mfc ctx ran,
adamc@26 619 fn ran' =>
adamc@26 620 S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
adamc@26 621 fn e' =>
adamc@26 622 (EAbs (x, dom', ran', e'), loc))))
adamc@16 623
adamc@16 624 | ECApp (e, c) =>
adamc@16 625 S.bind2 (mfe ctx e,
adamc@16 626 fn e' =>
adamc@16 627 S.map2 (mfc ctx c,
adamc@16 628 fn c' =>
adamc@16 629 (ECApp (e', c'), loc)))
adamc@16 630 | ECAbs (x, k, e) =>
adamc@626 631 S.bind2 (mfk ctx k,
adamc@16 632 fn k' =>
adamc@16 633 S.map2 (mfe (bind (ctx, RelC (x, k))) e,
adamc@16 634 fn e' =>
adamc@16 635 (ECAbs (x, k', e'), loc)))
adamc@16 636
adamc@16 637 | ERecord xes =>
adamc@29 638 S.map2 (ListUtil.mapfold (fn (x, e, t) =>
adamc@16 639 S.bind2 (mfc ctx x,
adamc@16 640 fn x' =>
adamc@29 641 S.bind2 (mfe ctx e,
adamc@29 642 fn e' =>
adamc@29 643 S.map2 (mfc ctx t,
adamc@29 644 fn t' =>
adamc@29 645 (x', e', t')))))
adamc@16 646 xes,
adamc@16 647 fn xes' =>
adamc@16 648 (ERecord xes', loc))
adamc@16 649 | EField (e, c, {field, rest}) =>
adamc@16 650 S.bind2 (mfe ctx e,
adamc@16 651 fn e' =>
adamc@16 652 S.bind2 (mfc ctx c,
adamc@16 653 fn c' =>
adamc@16 654 S.bind2 (mfc ctx field,
adamc@16 655 fn field' =>
adamc@16 656 S.map2 (mfc ctx rest,
adamc@16 657 fn rest' =>
adamc@16 658 (EField (e', c', {field = field', rest = rest'}), loc)))))
adamc@445 659 | EConcat (e1, c1, e2, c2) =>
adamc@339 660 S.bind2 (mfe ctx e1,
adamc@339 661 fn e1' =>
adamc@445 662 S.bind2 (mfc ctx c1,
adamc@445 663 fn c1' =>
adamc@339 664 S.bind2 (mfe ctx e2,
adamc@339 665 fn e2' =>
adamc@445 666 S.map2 (mfc ctx c2,
adamc@445 667 fn c2' =>
adamc@445 668 (EConcat (e1', c1', e2', c2'),
adamc@445 669 loc)))))
adamc@149 670 | ECut (e, c, {field, rest}) =>
adamc@149 671 S.bind2 (mfe ctx e,
adamc@149 672 fn e' =>
adamc@149 673 S.bind2 (mfc ctx c,
adamc@149 674 fn c' =>
adamc@149 675 S.bind2 (mfc ctx field,
adamc@149 676 fn field' =>
adamc@149 677 S.map2 (mfc ctx rest,
adamc@149 678 fn rest' =>
adamc@149 679 (ECut (e', c', {field = field', rest = rest'}), loc)))))
adamc@493 680 | ECutMulti (e, c, {rest}) =>
adamc@493 681 S.bind2 (mfe ctx e,
adamc@493 682 fn e' =>
adamc@493 683 S.bind2 (mfc ctx c,
adamc@493 684 fn c' =>
adamc@493 685 S.map2 (mfc ctx rest,
adamc@493 686 fn rest' =>
adamc@493 687 (ECutMulti (e', c', {rest = rest'}), loc))))
adamc@102 688
adamc@182 689 | ECase (e, pes, {disc, result}) =>
adamc@177 690 S.bind2 (mfe ctx e,
adamc@177 691 fn e' =>
adamc@177 692 S.bind2 (ListUtil.mapfold (fn (p, e) =>
adamc@193 693 let
adamc@193 694 fun pb ((p, _), ctx) =
adamc@193 695 case p of
adamc@193 696 PWild => ctx
adamc@193 697 | PVar (x, t) => bind (ctx, RelE (x, t))
adamc@193 698 | PPrim _ => ctx
adamc@193 699 | PCon (_, _, _, NONE) => ctx
adamc@193 700 | PCon (_, _, _, SOME p) => pb (p, ctx)
adamc@193 701 | PRecord xps => foldl (fn ((_, p, _), ctx) =>
adamc@193 702 pb (p, ctx)) ctx xps
adamc@193 703 in
adamc@193 704 S.bind2 (mfp ctx p,
adamc@193 705 fn p' =>
adamc@193 706 S.map2 (mfe (pb (p', ctx)) e,
adamc@193 707 fn e' => (p', e')))
adamc@193 708 end) pes,
adamc@177 709 fn pes' =>
adamc@182 710 S.bind2 (mfc ctx disc,
adamc@182 711 fn disc' =>
adamc@182 712 S.map2 (mfc ctx result,
adamc@182 713 fn result' =>
adamc@182 714 (ECase (e', pes', {disc = disc', result = result'}), loc)))))
adamc@177 715
adamc@102 716 | EWrite e =>
adamc@102 717 S.map2 (mfe ctx e,
adamc@102 718 fn e' =>
adamc@102 719 (EWrite e', loc))
adamc@110 720
adamc@110 721 | EClosure (n, es) =>
adamc@110 722 S.map2 (ListUtil.mapfold (mfe ctx) es,
adamc@110 723 fn es' =>
adamc@110 724 (EClosure (n, es'), loc))
adamc@193 725
adamc@450 726 | ELet (x, t, e1, e2) =>
adamc@450 727 S.bind2 (mfc ctx t,
adamc@450 728 fn t' =>
adamc@450 729 S.bind2 (mfe ctx e1,
adamc@450 730 fn e1' =>
adamc@453 731 S.map2 (mfe (bind (ctx, RelE (x, t'))) e2,
adamc@450 732 fn e2' =>
adamc@450 733 (ELet (x, t', e1', e2'), loc))))
adamc@450 734
adamc@1020 735 | EServerCall (n, es, t) =>
adamc@607 736 S.bind2 (ListUtil.mapfold (mfe ctx) es,
adamc@607 737 fn es' =>
adamc@1020 738 S.map2 (mfc ctx t,
adamc@1020 739 fn t' =>
adamc@1020 740 (EServerCall (n, es', t'), loc)))
adamc@954 741
adamc@626 742 | EKAbs (x, e) =>
adamc@626 743 S.map2 (mfe (bind (ctx, RelK x)) e,
adamc@626 744 fn e' =>
adamc@626 745 (EKAbs (x, e'), loc))
adamc@626 746 | EKApp (e, k) =>
adamc@626 747 S.bind2 (mfe ctx e,
adamc@626 748 fn e' =>
adamc@626 749 S.map2 (mfk ctx k,
adamc@626 750 fn k' =>
adamc@626 751 (EKApp (e', k'), loc)))
adamc@607 752
adamc@193 753 and mfp ctx (pAll as (p, loc)) =
adamc@193 754 case p of
adamc@193 755 PWild => S.return2 pAll
adamc@193 756 | PVar (x, t) =>
adamc@193 757 S.map2 (mfc ctx t,
adamc@193 758 fn t' =>
adamc@193 759 (PVar (x, t'), loc))
adamc@193 760 | PPrim _ => S.return2 pAll
adamc@193 761 | PCon (dk, pc, args, po) =>
adamc@193 762 S.bind2 (mfpc ctx pc,
adamc@193 763 fn pc' =>
adamc@193 764 S.bind2 (ListUtil.mapfold (mfc ctx) args,
adamc@193 765 fn args' =>
adamc@193 766 S.map2 ((case po of
adamc@193 767 NONE => S.return2 NONE
adamc@193 768 | SOME p => S.map2 (mfp ctx p, SOME)),
adamc@193 769 fn po' =>
adamc@193 770 (PCon (dk, pc', args', po'), loc))))
adamc@193 771 | PRecord xps =>
adamc@193 772 S.map2 (ListUtil.mapfold (fn (x, p, c) =>
adamc@193 773 S.bind2 (mfp ctx p,
adamc@193 774 fn p' =>
adamc@193 775 S.map2 (mfc ctx c,
adamc@193 776 fn c' =>
adamc@193 777 (x, p', c')))) xps,
adamc@193 778 fn xps' =>
adamc@193 779 (PRecord xps', loc))
adamc@193 780
adamc@193 781 and mfpc ctx pc =
adamc@193 782 case pc of
adamc@193 783 PConVar _ => S.return2 pc
adamc@193 784 | PConFfi {mod = m, datatyp, params, con, arg, kind} =>
adamc@193 785 S.map2 ((case arg of
adamc@193 786 NONE => S.return2 NONE
adamc@796 787 | SOME c =>
adamc@796 788 let
adamc@796 789 val k = (KType, ErrorMsg.dummySpan)
adamc@796 790 val ctx' = foldl (fn (x, ctx) => bind (ctx, RelC (x, k))) ctx params
adamc@796 791 in
adamc@796 792 S.map2 (mfc ctx' c, SOME)
adamc@796 793 end),
adamc@193 794 fn arg' =>
adamc@193 795 PConFfi {mod = m, datatyp = datatyp, params = params,
adamc@193 796 con = con, arg = arg', kind = kind})
adamc@16 797 in
adamc@16 798 mfe
adamc@16 799 end
adamc@16 800
adamc@16 801 fun mapfold {kind = fk, con = fc, exp = fe} =
adamc@626 802 mapfoldB {kind = fn () => fk,
adamc@16 803 con = fn () => fc,
adamc@16 804 exp = fn () => fe,
adamc@16 805 bind = fn ((), _) => ()} ()
adamc@16 806
adamc@21 807 fun mapB {kind, con, exp, bind} ctx e =
adamc@626 808 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@21 809 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@21 810 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
adamc@21 811 bind = bind} ctx e () of
adamc@21 812 S.Continue (e, ()) => e
adamc@21 813 | S.Return _ => raise Fail "CoreUtil.Exp.mapB: Impossible"
adamc@21 814
adamc@16 815 fun map {kind, con, exp} e =
adamc@16 816 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@16 817 con = fn c => fn () => S.Continue (con c, ()),
adamc@16 818 exp = fn e => fn () => S.Continue (exp e, ())} e () of
adamc@16 819 S.Return () => raise Fail "Core_util.Exp.map"
adamc@16 820 | S.Continue (e, ()) => e
adamc@16 821
adamc@23 822 fun fold {kind, con, exp} s e =
adamc@23 823 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
adamc@23 824 con = fn c => fn s => S.Continue (c, con (c, s)),
adamc@23 825 exp = fn e => fn s => S.Continue (e, exp (e, s))} e s of
adamc@23 826 S.Continue (_, s) => s
adamc@23 827 | S.Return _ => raise Fail "CoreUtil.Exp.fold: Impossible"
adamc@23 828
adamc@484 829 fun foldB {kind, con, exp, bind} ctx s e =
adamc@626 830 case mapfoldB {kind = fn ctx => fn k => fn s => S.Continue (k, kind (ctx, k, s)),
adamc@484 831 con = fn ctx => fn c => fn s => S.Continue (c, con (ctx, c, s)),
adamc@484 832 exp = fn ctx => fn e => fn s => S.Continue (e, exp (ctx, e, s)),
adamc@484 833 bind = bind} ctx e s of
adamc@484 834 S.Continue (_, s) => s
adamc@484 835 | S.Return _ => raise Fail "CoreUtil.Exp.foldB: Impossible"
adamc@484 836
adamc@16 837 fun exists {kind, con, exp} k =
adamc@16 838 case mapfold {kind = fn k => fn () =>
adamc@16 839 if kind k then
adamc@16 840 S.Return ()
adamc@16 841 else
adamc@16 842 S.Continue (k, ()),
adamc@16 843 con = fn c => fn () =>
adamc@16 844 if con c then
adamc@16 845 S.Return ()
adamc@16 846 else
adamc@16 847 S.Continue (c, ()),
adamc@16 848 exp = fn e => fn () =>
adamc@16 849 if exp e then
adamc@16 850 S.Return ()
adamc@16 851 else
adamc@16 852 S.Continue (e, ())} k () of
adamc@16 853 S.Return _ => true
adamc@16 854 | S.Continue _ => false
adamc@16 855
adamc@479 856 fun existsB {kind, con, exp, bind} ctx k =
adamc@626 857 case mapfoldB {kind = fn ctx => fn k => fn () =>
adamc@626 858 if kind (ctx, k) then
adamc@626 859 S.Return ()
adamc@626 860 else
adamc@626 861 S.Continue (k, ()),
adamc@479 862 con = fn ctx => fn c => fn () =>
adamc@479 863 if con (ctx, c) then
adamc@479 864 S.Return ()
adamc@479 865 else
adamc@479 866 S.Continue (c, ()),
adamc@479 867 exp = fn ctx => fn e => fn () =>
adamc@479 868 if exp (ctx, e) then
adamc@479 869 S.Return ()
adamc@479 870 else
adamc@479 871 S.Continue (e, ()),
adamc@479 872 bind = bind} ctx k () of
adamc@479 873 S.Return _ => true
adamc@479 874 | S.Continue _ => false
adamc@479 875
adamc@443 876 fun foldMap {kind, con, exp} s e =
adamc@443 877 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
adamc@443 878 con = fn c => fn s => S.Continue (con (c, s)),
adamc@443 879 exp = fn e => fn s => S.Continue (exp (e, s))} e s of
adamc@443 880 S.Continue v => v
adamc@443 881 | S.Return _ => raise Fail "CoreUtil.Exp.foldMap: Impossible"
adamc@443 882
adamc@488 883 fun foldMapB {kind, con, exp, bind} ctx s e =
adamc@626 884 case mapfoldB {kind = fn ctx => fn k => fn s => S.Continue (kind (ctx, k, s)),
adamc@488 885 con = fn ctx => fn c => fn s => S.Continue (con (ctx, c, s)),
adamc@488 886 exp = fn ctx => fn e => fn s => S.Continue (exp (ctx, e, s)),
adamc@488 887 bind = bind} ctx e s of
adamc@488 888 S.Continue v => v
adamc@488 889 | S.Return _ => raise Fail "CoreUtil.Exp.foldMapB: Impossible"
adamc@488 890
adamc@16 891 end
adamc@16 892
adamc@20 893 structure Decl = struct
adamc@20 894
adamc@20 895 datatype binder = datatype Exp.binder
adamc@20 896
adamc@20 897 fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} =
adamc@20 898 let
adamc@626 899 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@20 900
adamc@20 901 fun bind' (ctx, b) =
adamc@20 902 let
adamc@20 903 val b' = case b of
adamc@626 904 Con.RelK x => RelK x
adamc@626 905 | Con.RelC x => RelC x
adamc@626 906 | Con.NamedC x => NamedC x
adamc@20 907 in
adamc@20 908 bind (ctx, b')
adamc@20 909 end
adamc@20 910 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@20 911
adamc@20 912 val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind}
adamc@20 913
adamc@20 914 fun mfd ctx d acc =
adamc@20 915 S.bindP (mfd' ctx d acc, fd ctx)
adamc@20 916
adamc@20 917 and mfd' ctx (dAll as (d, loc)) =
adamc@20 918 case d of
adamc@20 919 DCon (x, n, k, c) =>
adamc@626 920 S.bind2 (mfk ctx k,
adamc@20 921 fn k' =>
adamc@20 922 S.map2 (mfc ctx c,
adamc@20 923 fn c' =>
adamc@20 924 (DCon (x, n, k', c'), loc)))
adamc@807 925 | DDatatype dts =>
adamc@807 926 S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
adamc@807 927 let
adamc@807 928 val k = (KType, loc)
adamc@807 929 val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
adamc@807 930 val ctx' = bind (ctx, NamedC (x, n, k', NONE))
adamc@807 931 in
adamc@807 932 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@807 933 case c of
adamc@807 934 NONE => S.return2 (x, n, c)
adamc@807 935 | SOME c =>
adamc@807 936 S.map2 (mfc ctx' c,
adamc@807 937 fn c' => (x, n, SOME c'))) xncs,
adamc@807 938 fn xncs' => (x, n, xs, xncs'))
adamc@807 939 end) dts,
adamc@807 940 fn dts' =>
adamc@807 941 (DDatatype dts', loc))
adamc@125 942 | DVal vi =>
adamc@125 943 S.map2 (mfvi ctx vi,
adamc@125 944 fn vi' =>
adamc@125 945 (DVal vi', loc))
adamc@125 946 | DValRec vis =>
adamc@127 947 let
adamc@127 948 val ctx = foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s)))
adamc@127 949 ctx vis
adamc@127 950 in
adamc@127 951 S.map2 (ListUtil.mapfold (mfvi ctx) vis,
adamc@127 952 fn vis' =>
adamc@127 953 (DValRec vis', loc))
adamc@127 954 end
adamc@109 955 | DExport _ => S.return2 dAll
adamc@707 956 | DTable (x, n, c, s, pe, pc, ce, cc) =>
adamc@802 957 let
adamc@802 958 val loc = #2 ce
adamc@802 959 val ct = (CFfi ("Basis", "sql_table"), loc)
adamc@802 960 val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc)
adamc@802 961 val ct = (CApp (ct, cc), loc)
adamc@802 962 val ctx' = bind (ctx, NamedE (x, n, ct, NONE, s))
adamc@802 963 in
adamc@802 964 S.bind2 (mfc ctx c,
adamc@802 965 fn c' =>
adamc@802 966 S.bind2 (mfe ctx' pe,
adamc@802 967 fn pe' =>
adamc@802 968 S.bind2 (mfc ctx pc,
adamc@802 969 fn pc' =>
adamc@802 970 S.bind2 (mfe ctx' ce,
adamc@802 971 fn ce' =>
adamc@802 972 S.map2 (mfc ctx cc,
adamc@802 973 fn cc' =>
adamc@802 974 (DTable (x, n, c', s, pe', pc', ce', cc'), loc))))))
adamc@802 975 end
adamc@338 976 | DSequence _ => S.return2 dAll
adamc@754 977 | DView (x, n, s, e, c) =>
adamc@754 978 S.bind2 (mfe ctx e,
adamc@754 979 fn e' =>
adamc@754 980 S.map2 (mfc ctx c,
adamc@754 981 fn c' =>
adamc@754 982 (DView (x, n, s, e', c'), loc)))
adamc@271 983 | DDatabase _ => S.return2 dAll
adamc@461 984 | DCookie (x, n, c, s) =>
adamc@461 985 S.map2 (mfc ctx c,
adamc@461 986 fn c' =>
adamc@461 987 (DCookie (x, n, c', s), loc))
adamc@720 988 | DStyle _ => S.return2 dAll
adamc@1075 989 | DTask (e1, e2) =>
adamc@1075 990 S.bind2 (mfe ctx e1,
adamc@1075 991 fn e1' =>
adamc@1075 992 S.map2 (mfe ctx e2,
adamc@1075 993 fn e2' =>
adamc@1075 994 (DTask (e1', e2'), loc)))
adamc@1199 995 | DPolicy e =>
adamc@1199 996 S.map2 (mfe ctx e,
adamc@1199 997 fn e' =>
adamc@1199 998 (DPolicy e', loc))
adamc@125 999
adam@1294 1000 | DOnError _ => S.return2 dAll
adam@1294 1001
adamc@125 1002 and mfvi ctx (x, n, t, e, s) =
adamc@125 1003 S.bind2 (mfc ctx t,
adamc@125 1004 fn t' =>
adamc@125 1005 S.map2 (mfe ctx e,
adamc@125 1006 fn e' =>
adamc@125 1007 (x, n, t', e', s)))
adamc@20 1008 in
adamc@20 1009 mfd
adamc@20 1010 end
adamc@20 1011
adamc@23 1012 fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} =
adamc@626 1013 mapfoldB {kind = fn () => fk,
adamc@23 1014 con = fn () => fc,
adamc@23 1015 exp = fn () => fe,
adamc@23 1016 decl = fn () => fd,
adamc@23 1017 bind = fn ((), _) => ()} ()
adamc@23 1018
adamc@23 1019 fun fold {kind, con, exp, decl} s d =
adamc@23 1020 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
adamc@23 1021 con = fn c => fn s => S.Continue (c, con (c, s)),
adamc@23 1022 exp = fn e => fn s => S.Continue (e, exp (e, s)),
adamc@23 1023 decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
adamc@23 1024 S.Continue (_, s) => s
adamc@23 1025 | S.Return _ => raise Fail "CoreUtil.Decl.fold: Impossible"
adamc@23 1026
adamc@110 1027 fun foldMap {kind, con, exp, decl} s d =
adamc@110 1028 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
adamc@110 1029 con = fn c => fn s => S.Continue (con (c, s)),
adamc@110 1030 exp = fn e => fn s => S.Continue (exp (e, s)),
adamc@110 1031 decl = fn d => fn s => S.Continue (decl (d, s))} d s of
adamc@110 1032 S.Continue v => v
adamc@110 1033 | S.Return _ => raise Fail "CoreUtil.Decl.foldMap: Impossible"
adamc@110 1034
adamc@484 1035 fun foldMapB {kind, con, exp, decl, bind} ctx s d =
adamc@626 1036 case mapfoldB {kind = fn ctx => fn k => fn s => S.Continue (kind (ctx, k, s)),
adamc@484 1037 con = fn ctx => fn c => fn s => S.Continue (con (ctx, c, s)),
adamc@484 1038 exp = fn ctx => fn e => fn s => S.Continue (exp (ctx, e, s)),
adamc@484 1039 decl = fn ctx => fn d => fn s => S.Continue (decl (ctx, d, s)),
adamc@484 1040 bind = bind} ctx d s of
adamc@484 1041 S.Continue v => v
adamc@484 1042 | S.Return _ => raise Fail "CoreUtil.Decl.foldMapB: Impossible"
adamc@484 1043
adamc@522 1044 fun exists {kind, con, exp, decl} d =
adamc@522 1045 case mapfold {kind = fn k => fn () =>
adamc@522 1046 if kind k then
adamc@522 1047 S.Return ()
adamc@522 1048 else
adamc@522 1049 S.Continue (k, ()),
adamc@522 1050 con = fn c => fn () =>
adamc@522 1051 if con c then
adamc@522 1052 S.Return ()
adamc@522 1053 else
adamc@522 1054 S.Continue (c, ()),
adamc@522 1055 exp = fn e => fn () =>
adamc@522 1056 if exp e then
adamc@522 1057 S.Return ()
adamc@522 1058 else
adamc@522 1059 S.Continue (e, ()),
adamc@522 1060 decl = fn d => fn () =>
adamc@522 1061 if decl d then
adamc@522 1062 S.Return ()
adamc@522 1063 else
adamc@522 1064 S.Continue (d, ())} d () of
adamc@522 1065 S.Return _ => true
adamc@522 1066 | S.Continue _ => false
adamc@522 1067
adamc@16 1068 end
adamc@20 1069
adamc@20 1070 structure File = struct
adamc@20 1071
adamc@20 1072 datatype binder = datatype Exp.binder
adamc@20 1073
adamc@20 1074 fun mapfoldB (all as {bind, ...}) =
adamc@20 1075 let
adamc@20 1076 val mfd = Decl.mapfoldB all
adamc@20 1077
adamc@20 1078 fun mff ctx ds =
adamc@20 1079 case ds of
adamc@20 1080 nil => S.return2 nil
adamc@20 1081 | d :: ds' =>
adamc@20 1082 S.bind2 (mfd ctx d,
adamc@20 1083 fn d' =>
adamc@20 1084 let
adamc@100 1085 val ctx' =
adamc@20 1086 case #1 d' of
adamc@100 1087 DCon (x, n, k, c) => bind (ctx, NamedC (x, n, k, SOME c))
adamc@807 1088 | DDatatype dts =>
adamc@807 1089 foldl (fn ((x, n, xs, xncs), ctx) =>
adamc@807 1090 let
adamc@807 1091 val loc = #2 d'
adamc@807 1092 val k = (KType, loc)
adamc@807 1093 val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
adamc@192 1094
adamc@807 1095 val ctx = bind (ctx, NamedC (x, n, k', NONE))
adamc@807 1096 val t = (CNamed n, #2 d')
adamc@807 1097 val t = ListUtil.foldli (fn (i, _, t) =>
adamc@807 1098 (CApp (t, (CRel i, loc)), loc))
adamc@807 1099 t xs
adamc@807 1100 in
adamc@807 1101 foldl (fn ((x, n, to), ctx) =>
adamc@807 1102 let
adamc@807 1103 val t = case to of
adamc@807 1104 NONE => t
adamc@807 1105 | SOME t' => (TFun (t', t), #2 d')
adamc@807 1106 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc))
adamc@807 1107 t xs
adamc@807 1108 in
adamc@807 1109 bind (ctx, NamedE (x, n, t, NONE, ""))
adamc@807 1110 end)
adamc@807 1111 ctx xncs
adamc@807 1112 end)
adamc@807 1113 ctx dts
adamc@109 1114 | DVal (x, n, t, e, s) => bind (ctx, NamedE (x, n, t, SOME e, s))
adamc@125 1115 | DValRec vis =>
adamc@127 1116 foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s)))
adamc@125 1117 ctx vis
adamc@109 1118 | DExport _ => ctx
adamc@707 1119 | DTable (x, n, c, s, _, pc, _, cc) =>
adamc@247 1120 let
adamc@705 1121 val loc = #2 d'
adamc@705 1122 val ct = (CFfi ("Basis", "sql_table"), loc)
adamc@707 1123 val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc)
adamc@705 1124 val ct = (CApp (ct, cc), loc)
adamc@338 1125 in
adamc@705 1126 bind (ctx, NamedE (x, n, ct, NONE, s))
adamc@338 1127 end
adamc@338 1128 | DSequence (x, n, s) =>
adamc@338 1129 let
adamc@338 1130 val t = (CFfi ("Basis", "sql_sequence"), #2 d')
adamc@247 1131 in
adamc@247 1132 bind (ctx, NamedE (x, n, t, NONE, s))
adamc@247 1133 end
adamc@754 1134 | DView (x, n, s, _, c) =>
adamc@754 1135 let
adamc@754 1136 val loc = #2 d'
adamc@754 1137 val ct = (CFfi ("Basis", "sql_view"), loc)
adamc@754 1138 val ct = (CApp (ct, c), loc)
adamc@754 1139 in
adamc@754 1140 bind (ctx, NamedE (x, n, ct, NONE, s))
adamc@754 1141 end
adamc@271 1142 | DDatabase _ => ctx
adamc@461 1143 | DCookie (x, n, c, s) =>
adamc@461 1144 let
adamc@461 1145 val t = (CApp ((CFfi ("Basis", "http_cookie"), #2 d'), c), #2 d')
adamc@461 1146 in
adamc@461 1147 bind (ctx, NamedE (x, n, t, NONE, s))
adamc@461 1148 end
adamc@720 1149 | DStyle (x, n, s) =>
adamc@718 1150 let
adamc@720 1151 val t = (CFfi ("Basis", "css_class"), #2 d')
adamc@718 1152 in
adamc@718 1153 bind (ctx, NamedE (x, n, t, NONE, s))
adamc@718 1154 end
adamc@1075 1155 | DTask _ => ctx
adamc@1199 1156 | DPolicy _ => ctx
adam@1294 1157 | DOnError _ => ctx
adamc@20 1158 in
adamc@20 1159 S.map2 (mff ctx' ds',
adamc@20 1160 fn ds' =>
adamc@20 1161 d' :: ds')
adamc@20 1162 end)
adamc@20 1163 in
adamc@20 1164 mff
adamc@20 1165 end
adamc@20 1166
adamc@23 1167 fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} =
adamc@626 1168 mapfoldB {kind = fn () => fk,
adamc@23 1169 con = fn () => fc,
adamc@23 1170 exp = fn () => fe,
adamc@23 1171 decl = fn () => fd,
adamc@23 1172 bind = fn ((), _) => ()} ()
adamc@23 1173
adamc@20 1174 fun mapB {kind, con, exp, decl, bind} ctx ds =
adamc@626 1175 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@20 1176 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@20 1177 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
adamc@20 1178 decl = fn ctx => fn d => fn () => S.Continue (decl ctx d, ()),
adamc@20 1179 bind = bind} ctx ds () of
adamc@20 1180 S.Continue (ds, ()) => ds
adamc@20 1181 | S.Return _ => raise Fail "CoreUtil.File.mapB: Impossible"
adamc@20 1182
adamc@482 1183 fun map {kind, con, exp, decl} ds =
adamc@626 1184 mapB {kind = fn () => kind,
adamc@482 1185 con = fn () => con,
adamc@482 1186 exp = fn () => exp,
adamc@482 1187 decl = fn () => decl,
adamc@482 1188 bind = fn _ => ()} () ds
adamc@482 1189
adamc@23 1190 fun fold {kind, con, exp, decl} s d =
adamc@23 1191 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
adamc@23 1192 con = fn c => fn s => S.Continue (c, con (c, s)),
adamc@23 1193 exp = fn e => fn s => S.Continue (e, exp (e, s)),
adamc@23 1194 decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
adamc@23 1195 S.Continue (_, s) => s
adamc@23 1196 | S.Return _ => raise Fail "CoreUtil.File.fold: Impossible"
adamc@23 1197
adamc@110 1198 fun foldMap {kind, con, exp, decl} s d =
adamc@110 1199 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
adamc@110 1200 con = fn c => fn s => S.Continue (con (c, s)),
adamc@110 1201 exp = fn e => fn s => S.Continue (exp (e, s)),
adamc@110 1202 decl = fn d => fn s => S.Continue (decl (d, s))} d s of
adamc@110 1203 S.Continue v => v
adamc@110 1204 | S.Return _ => raise Fail "CoreUtil.File.foldMap: Impossible"
adamc@110 1205
adamc@179 1206 val maxName = foldl (fn ((d, _) : decl, count) =>
adamc@179 1207 case d of
adamc@179 1208 DCon (_, n, _, _) => Int.max (n, count)
adamc@807 1209 | DDatatype dts => foldl (fn ((_, n, _, ns), count) =>
adamc@807 1210 foldl (fn ((_, n', _), m) => Int.max (n', m))
adamc@807 1211 (Int.max (n, count)) ns) count dts
adamc@179 1212 | DVal (_, n, _, _, _) => Int.max (n, count)
adamc@179 1213 | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis
adamc@247 1214 | DExport _ => count
adamc@707 1215 | DTable (_, n, _, _, _, _, _, _) => Int.max (n, count)
adamc@338 1216 | DSequence (_, n, _) => Int.max (n, count)
adamc@754 1217 | DView (_, n, _, _, _) => Int.max (n, count)
adamc@461 1218 | DDatabase _ => count
adamc@718 1219 | DCookie (_, n, _, _) => Int.max (n, count)
adamc@1073 1220 | DStyle (_, n, _) => Int.max (n, count)
adamc@1199 1221 | DTask _ => count
adam@1294 1222 | DPolicy _ => count
adam@1294 1223 | DOnError _ => count) 0
adamc@179 1224
adamc@20 1225 end
adamc@20 1226
adamc@20 1227 end