Mercurial > urweb

annotate src/core_util.sml @ 709:0406e9cccb72

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FOREIGN KEY, without ability to link NULL to NOT NULL (and with some lingering problems in row inference)
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 18:47:47 -0400
parents d8217b4cb617
children f152f215a02c
rev   line source
adamc@16 1 (* Copyright (c) 2008, 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@193 378 fun foldMap {kind, con} s c =
adamc@193 379 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
adamc@193 380 con = fn c => fn s => S.Continue (con (c, s))} c s of
adamc@193 381 S.Continue v => v
adamc@193 382 | S.Return _ => raise Fail "CoreUtil.Con.foldMap: Impossible"
adamc@193 383
adamc@16 384 end
adamc@16 385
adamc@16 386 structure Exp = struct
adamc@16 387
adamc@479 388 open Order
adamc@479 389
adamc@479 390 fun pcCompare (pc1, pc2) =
adamc@479 391 case (pc1, pc2) of
adamc@479 392 (PConVar n1, PConVar n2) => Int.compare (n1, n2)
adamc@479 393 | (PConVar _, _) => LESS
adamc@479 394 | (_, PConVar _) => GREATER
adamc@479 395
adamc@479 396 | (PConFfi {mod = m1, datatyp = d1, con = c1, ...},
adamc@479 397 PConFfi {mod = m2, datatyp = d2, con = c2, ...}) =>
adamc@479 398 join (String.compare (m1, m2),
adamc@479 399 fn () => join (String.compare (d1, d2),
adamc@479 400 fn () => String.compare (c1, c2)))
adamc@479 401
adamc@479 402 fun pCompare ((p1, _), (p2, _)) =
adamc@479 403 case (p1, p2) of
adamc@479 404 (PWild, PWild) => EQUAL
adamc@479 405 | (PWild, _) => LESS
adamc@479 406 | (_, PWild) => GREATER
adamc@479 407
adamc@479 408 | (PVar _, PVar _) => EQUAL
adamc@479 409 | (PVar _, _) => LESS
adamc@479 410 | (_, PVar _) => GREATER
adamc@479 411
adamc@479 412 | (PPrim p1, PPrim p2) => Prim.compare (p1, p2)
adamc@479 413 | (PPrim _, _) => LESS
adamc@479 414 | (_, PPrim _) => GREATER
adamc@479 415
adamc@479 416 | (PCon (_, pc1, _, po1), PCon (_, pc2, _, po2)) =>
adamc@479 417 join (pcCompare (pc1, pc2),
adamc@479 418 fn () => joinO pCompare (po1, po2))
adamc@479 419 | (PCon _, _) => LESS
adamc@479 420 | (_, PCon _) => GREATER
adamc@479 421
adamc@479 422 | (PRecord xps1, PRecord xps2) =>
adamc@479 423 joinL (fn ((x1, p1, _), (x2, p2, _)) =>
adamc@479 424 join (String.compare (x1, x2),
adamc@479 425 fn () => pCompare (p1, p2))) (xps1, xps2)
adamc@479 426
adamc@479 427 fun compare ((e1, _), (e2, _)) =
adamc@479 428 case (e1, e2) of
adamc@479 429 (EPrim p1, EPrim p2) => Prim.compare (p1, p2)
adamc@479 430 | (EPrim _, _) => LESS
adamc@479 431 | (_, EPrim _) => GREATER
adamc@479 432
adamc@479 433 | (ERel n1, ERel n2) => Int.compare (n1, n2)
adamc@479 434 | (ERel _, _) => LESS
adamc@479 435 | (_, ERel _) => GREATER
adamc@479 436
adamc@479 437 | (ENamed n1, ENamed n2) => Int.compare (n1, n2)
adamc@479 438 | (ENamed _, _) => LESS
adamc@479 439 | (_, ENamed _) => GREATER
adamc@479 440
adamc@479 441 | (ECon (_, pc1, _, eo1), ECon (_, pc2, _, eo2)) =>
adamc@479 442 join (pcCompare (pc1, pc2),
adamc@479 443 fn () => joinO compare (eo1, eo2))
adamc@479 444 | (ECon _, _) => LESS
adamc@479 445 | (_, ECon _) => GREATER
adamc@479 446
adamc@479 447 | (EFfi (f1, x1), EFfi (f2, x2)) =>
adamc@479 448 join (String.compare (f1, f2),
adamc@479 449 fn () => String.compare (x1, x2))
adamc@479 450 | (EFfi _, _) => LESS
adamc@479 451 | (_, EFfi _) => GREATER
adamc@479 452
adamc@479 453 | (EFfiApp (f1, x1, es1), EFfiApp (f2, x2, es2)) =>
adamc@479 454 join (String.compare (f1, f2),
adamc@479 455 fn () => join (String.compare (x1, x2),
adamc@479 456 fn () => joinL compare (es1, es2)))
adamc@479 457 | (EFfiApp _, _) => LESS
adamc@479 458 | (_, EFfiApp _) => GREATER
adamc@479 459
adamc@479 460 | (EApp (f1, x1), EApp (f2, x2)) =>
adamc@479 461 join (compare (f1, f2),
adamc@479 462 fn () => compare (x1, x2))
adamc@479 463 | (EApp _, _) => LESS
adamc@479 464 | (_, EApp _) => GREATER
adamc@479 465
adamc@479 466 | (EAbs (_, _, _, e1), EAbs (_, _, _, e2)) => compare (e1, e2)
adamc@479 467 | (EAbs _, _) => LESS
adamc@479 468 | (_, EAbs _) => GREATER
adamc@479 469
adamc@479 470 | (ECApp (f1, x1), ECApp (f2, x2)) =>
adamc@479 471 join (compare (f1, f2),
adamc@479 472 fn () => Con.compare (x1, x2))
adamc@479 473 | (ECApp _, _) => LESS
adamc@479 474 | (_, ECApp _) => GREATER
adamc@479 475
adamc@479 476 | (ECAbs (_, _, e1), ECAbs (_, _, e2)) => compare (e1, e2)
adamc@479 477 | (ECAbs _, _) => LESS
adamc@479 478 | (_, ECAbs _) => GREATER
adamc@479 479
adamc@479 480 | (ERecord xes1, ERecord xes2) =>
adamc@479 481 joinL (fn ((x1, e1, _), (x2, e2, _)) =>
adamc@479 482 join (Con.compare (x1, x2),
adamc@479 483 fn () => compare (e1, e2))) (xes1, xes2)
adamc@479 484 | (ERecord _, _) => LESS
adamc@479 485 | (_, ERecord _) => GREATER
adamc@479 486
adamc@479 487 | (EField (e1, c1, _), EField (e2, c2, _)) =>
adamc@479 488 join (compare (e1, e2),
adamc@479 489 fn () => Con.compare (c1, c2))
adamc@479 490 | (EField _, _) => LESS
adamc@479 491 | (_, EField _) => GREATER
adamc@479 492
adamc@479 493 | (EConcat (x1, _, y1, _), EConcat (x2, _, y2, _)) =>
adamc@479 494 join (compare (x1, x2),
adamc@479 495 fn () => compare (y1, y2))
adamc@479 496 | (EConcat _, _) => LESS
adamc@479 497 | (_, EConcat _) => GREATER
adamc@479 498
adamc@479 499 | (ECut (e1, c1, _), ECut (e2, c2, _)) =>
adamc@479 500 join (compare (e1, e2),
adamc@493 501 fn () => Con.compare (c1, c2))
adamc@479 502 | (ECut _, _) => LESS
adamc@479 503 | (_, ECut _) => GREATER
adamc@479 504
adamc@493 505 | (ECutMulti (e1, c1, _), ECutMulti (e2, c2, _)) =>
adamc@493 506 join (compare (e1, e2),
adamc@493 507 fn () => Con.compare (c1, c2))
adamc@493 508 | (ECutMulti _, _) => LESS
adamc@493 509 | (_, ECutMulti _) => GREATER
adamc@493 510
adamc@479 511 | (ECase (e1, pes1, _), ECase (e2, pes2, _)) =>
adamc@479 512 join (compare (e1, e2),
adamc@479 513 fn () => joinL (fn ((p1, e1), (p2, e2)) =>
adamc@479 514 join (pCompare (p1, p2),
adamc@479 515 fn () => compare (e1, e2))) (pes1, pes2))
adamc@479 516 | (ECase _, _) => LESS
adamc@479 517 | (_, ECase _) => GREATER
adamc@479 518
adamc@479 519 | (EWrite e1, EWrite e2) => compare (e1, e2)
adamc@479 520 | (EWrite _, _) => LESS
adamc@479 521 | (_, EWrite _) => GREATER
adamc@479 522
adamc@479 523 | (EClosure (n1, es1), EClosure (n2, es2)) =>
adamc@479 524 join (Int.compare (n1, n2),
adamc@479 525 fn () => joinL compare (es1, es2))
adamc@479 526 | (EClosure _, _) => LESS
adamc@479 527 | (_, EClosure _) => GREATER
adamc@479 528
adamc@479 529 | (ELet (_, _, x1, e1), ELet (_, _, x2, e2)) =>
adamc@479 530 join (compare (x1, x2),
adamc@479 531 fn () => compare (e1, e2))
adamc@607 532 | (ELet _, _) => LESS
adamc@607 533 | (_, ELet _) => GREATER
adamc@607 534
adamc@609 535 | (EServerCall (n1, es1, e1, _), EServerCall (n2, es2, e2, _)) =>
adamc@607 536 join (Int.compare (n1, n2),
adamc@607 537 fn () => join (joinL compare (es1, es2),
adamc@607 538 fn () => compare (e1, e2)))
adamc@626 539 | (EServerCall _, _) => LESS
adamc@626 540 | (_, EServerCall _) => GREATER
adamc@626 541
adamc@626 542 | (EKAbs (_, e1), EKAbs (_, e2)) => compare (e1, e2)
adamc@626 543 | (EKAbs _, _) => LESS
adamc@626 544 | (_, EKAbs _) => GREATER
adamc@626 545
adamc@626 546 | (EKApp (e1, k1), EKApp (e2, k2)) =>
adamc@626 547 join (compare (e1, e2),
adamc@626 548 fn () => Kind.compare (k1, k2))
adamc@479 549
adamc@16 550 datatype binder =
adamc@626 551 RelK of string
adamc@626 552 | RelC of string * kind
adamc@20 553 | NamedC of string * int * kind * con option
adamc@16 554 | RelE of string * con
adamc@109 555 | NamedE of string * int * con * exp option * string
adamc@16 556
adamc@16 557 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
adamc@16 558 let
adamc@626 559 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@16 560
adamc@16 561 fun bind' (ctx, b) =
adamc@16 562 let
adamc@16 563 val b' = case b of
adamc@626 564 Con.RelK x => RelK x
adamc@626 565 | Con.RelC x => RelC x
adamc@626 566 | Con.NamedC x => NamedC x
adamc@16 567 in
adamc@16 568 bind (ctx, b')
adamc@16 569 end
adamc@16 570 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@16 571
adamc@16 572 fun mfe ctx e acc =
adamc@16 573 S.bindP (mfe' ctx e acc, fe ctx)
adamc@16 574
adamc@16 575 and mfe' ctx (eAll as (e, loc)) =
adamc@16 576 case e of
adamc@16 577 EPrim _ => S.return2 eAll
adamc@16 578 | ERel _ => S.return2 eAll
adamc@16 579 | ENamed _ => S.return2 eAll
adamc@192 580 | ECon (dk, pc, cs, NONE) =>
adamc@192 581 S.map2 (ListUtil.mapfold (mfc ctx) cs,
adamc@192 582 fn cs' =>
adamc@192 583 (ECon (dk, pc, cs', NONE), loc))
adamc@192 584 | ECon (dk, n, cs, SOME e) =>
adamc@192 585 S.bind2 (mfe ctx e,
adamc@192 586 fn e' =>
adamc@192 587 S.map2 (ListUtil.mapfold (mfc ctx) cs,
adamc@192 588 fn cs' =>
adamc@192 589 (ECon (dk, n, cs', SOME e'), loc)))
adamc@48 590 | EFfi _ => S.return2 eAll
adamc@48 591 | EFfiApp (m, x, es) =>
adamc@192 592 S.map2 (ListUtil.mapfold (mfe ctx) es,
adamc@48 593 fn es' =>
adamc@48 594 (EFfiApp (m, x, es'), loc))
adamc@16 595 | EApp (e1, e2) =>
adamc@16 596 S.bind2 (mfe ctx e1,
adamc@16 597 fn e1' =>
adamc@16 598 S.map2 (mfe ctx e2,
adamc@16 599 fn e2' =>
adamc@16 600 (EApp (e1', e2'), loc)))
adamc@26 601 | EAbs (x, dom, ran, e) =>
adamc@26 602 S.bind2 (mfc ctx dom,
adamc@26 603 fn dom' =>
adamc@26 604 S.bind2 (mfc ctx ran,
adamc@26 605 fn ran' =>
adamc@26 606 S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
adamc@26 607 fn e' =>
adamc@26 608 (EAbs (x, dom', ran', e'), loc))))
adamc@16 609
adamc@16 610 | ECApp (e, c) =>
adamc@16 611 S.bind2 (mfe ctx e,
adamc@16 612 fn e' =>
adamc@16 613 S.map2 (mfc ctx c,
adamc@16 614 fn c' =>
adamc@16 615 (ECApp (e', c'), loc)))
adamc@16 616 | ECAbs (x, k, e) =>
adamc@626 617 S.bind2 (mfk ctx k,
adamc@16 618 fn k' =>
adamc@16 619 S.map2 (mfe (bind (ctx, RelC (x, k))) e,
adamc@16 620 fn e' =>
adamc@16 621 (ECAbs (x, k', e'), loc)))
adamc@16 622
adamc@16 623 | ERecord xes =>
adamc@29 624 S.map2 (ListUtil.mapfold (fn (x, e, t) =>
adamc@16 625 S.bind2 (mfc ctx x,
adamc@16 626 fn x' =>
adamc@29 627 S.bind2 (mfe ctx e,
adamc@29 628 fn e' =>
adamc@29 629 S.map2 (mfc ctx t,
adamc@29 630 fn t' =>
adamc@29 631 (x', e', t')))))
adamc@16 632 xes,
adamc@16 633 fn xes' =>
adamc@16 634 (ERecord xes', loc))
adamc@16 635 | EField (e, c, {field, rest}) =>
adamc@16 636 S.bind2 (mfe ctx e,
adamc@16 637 fn e' =>
adamc@16 638 S.bind2 (mfc ctx c,
adamc@16 639 fn c' =>
adamc@16 640 S.bind2 (mfc ctx field,
adamc@16 641 fn field' =>
adamc@16 642 S.map2 (mfc ctx rest,
adamc@16 643 fn rest' =>
adamc@16 644 (EField (e', c', {field = field', rest = rest'}), loc)))))
adamc@445 645 | EConcat (e1, c1, e2, c2) =>
adamc@339 646 S.bind2 (mfe ctx e1,
adamc@339 647 fn e1' =>
adamc@445 648 S.bind2 (mfc ctx c1,
adamc@445 649 fn c1' =>
adamc@339 650 S.bind2 (mfe ctx e2,
adamc@339 651 fn e2' =>
adamc@445 652 S.map2 (mfc ctx c2,
adamc@445 653 fn c2' =>
adamc@445 654 (EConcat (e1', c1', e2', c2'),
adamc@445 655 loc)))))
adamc@149 656 | ECut (e, c, {field, rest}) =>
adamc@149 657 S.bind2 (mfe ctx e,
adamc@149 658 fn e' =>
adamc@149 659 S.bind2 (mfc ctx c,
adamc@149 660 fn c' =>
adamc@149 661 S.bind2 (mfc ctx field,
adamc@149 662 fn field' =>
adamc@149 663 S.map2 (mfc ctx rest,
adamc@149 664 fn rest' =>
adamc@149 665 (ECut (e', c', {field = field', rest = rest'}), loc)))))
adamc@493 666 | ECutMulti (e, c, {rest}) =>
adamc@493 667 S.bind2 (mfe ctx e,
adamc@493 668 fn e' =>
adamc@493 669 S.bind2 (mfc ctx c,
adamc@493 670 fn c' =>
adamc@493 671 S.map2 (mfc ctx rest,
adamc@493 672 fn rest' =>
adamc@493 673 (ECutMulti (e', c', {rest = rest'}), loc))))
adamc@102 674
adamc@182 675 | ECase (e, pes, {disc, result}) =>
adamc@177 676 S.bind2 (mfe ctx e,
adamc@177 677 fn e' =>
adamc@177 678 S.bind2 (ListUtil.mapfold (fn (p, e) =>
adamc@193 679 let
adamc@193 680 fun pb ((p, _), ctx) =
adamc@193 681 case p of
adamc@193 682 PWild => ctx
adamc@193 683 | PVar (x, t) => bind (ctx, RelE (x, t))
adamc@193 684 | PPrim _ => ctx
adamc@193 685 | PCon (_, _, _, NONE) => ctx
adamc@193 686 | PCon (_, _, _, SOME p) => pb (p, ctx)
adamc@193 687 | PRecord xps => foldl (fn ((_, p, _), ctx) =>
adamc@193 688 pb (p, ctx)) ctx xps
adamc@193 689 in
adamc@193 690 S.bind2 (mfp ctx p,
adamc@193 691 fn p' =>
adamc@193 692 S.map2 (mfe (pb (p', ctx)) e,
adamc@193 693 fn e' => (p', e')))
adamc@193 694 end) pes,
adamc@177 695 fn pes' =>
adamc@182 696 S.bind2 (mfc ctx disc,
adamc@182 697 fn disc' =>
adamc@182 698 S.map2 (mfc ctx result,
adamc@182 699 fn result' =>
adamc@182 700 (ECase (e', pes', {disc = disc', result = result'}), loc)))))
adamc@177 701
adamc@102 702 | EWrite e =>
adamc@102 703 S.map2 (mfe ctx e,
adamc@102 704 fn e' =>
adamc@102 705 (EWrite e', loc))
adamc@110 706
adamc@110 707 | EClosure (n, es) =>
adamc@110 708 S.map2 (ListUtil.mapfold (mfe ctx) es,
adamc@110 709 fn es' =>
adamc@110 710 (EClosure (n, es'), loc))
adamc@193 711
adamc@450 712 | ELet (x, t, e1, e2) =>
adamc@450 713 S.bind2 (mfc ctx t,
adamc@450 714 fn t' =>
adamc@450 715 S.bind2 (mfe ctx e1,
adamc@450 716 fn e1' =>
adamc@453 717 S.map2 (mfe (bind (ctx, RelE (x, t'))) e2,
adamc@450 718 fn e2' =>
adamc@450 719 (ELet (x, t', e1', e2'), loc))))
adamc@450 720
adamc@609 721 | EServerCall (n, es, e, t) =>
adamc@607 722 S.bind2 (ListUtil.mapfold (mfe ctx) es,
adamc@607 723 fn es' =>
adamc@609 724 S.bind2 (mfe ctx e,
adamc@607 725 fn e' =>
adamc@609 726 S.map2 (mfc ctx t,
adamc@609 727 fn t' =>
adamc@609 728 (EServerCall (n, es', e', t'), loc))))
adamc@626 729
adamc@626 730 | EKAbs (x, e) =>
adamc@626 731 S.map2 (mfe (bind (ctx, RelK x)) e,
adamc@626 732 fn e' =>
adamc@626 733 (EKAbs (x, e'), loc))
adamc@626 734 | EKApp (e, k) =>
adamc@626 735 S.bind2 (mfe ctx e,
adamc@626 736 fn e' =>
adamc@626 737 S.map2 (mfk ctx k,
adamc@626 738 fn k' =>
adamc@626 739 (EKApp (e', k'), loc)))
adamc@607 740
adamc@193 741 and mfp ctx (pAll as (p, loc)) =
adamc@193 742 case p of
adamc@193 743 PWild => S.return2 pAll
adamc@193 744 | PVar (x, t) =>
adamc@193 745 S.map2 (mfc ctx t,
adamc@193 746 fn t' =>
adamc@193 747 (PVar (x, t'), loc))
adamc@193 748 | PPrim _ => S.return2 pAll
adamc@193 749 | PCon (dk, pc, args, po) =>
adamc@193 750 S.bind2 (mfpc ctx pc,
adamc@193 751 fn pc' =>
adamc@193 752 S.bind2 (ListUtil.mapfold (mfc ctx) args,
adamc@193 753 fn args' =>
adamc@193 754 S.map2 ((case po of
adamc@193 755 NONE => S.return2 NONE
adamc@193 756 | SOME p => S.map2 (mfp ctx p, SOME)),
adamc@193 757 fn po' =>
adamc@193 758 (PCon (dk, pc', args', po'), loc))))
adamc@193 759 | PRecord xps =>
adamc@193 760 S.map2 (ListUtil.mapfold (fn (x, p, c) =>
adamc@193 761 S.bind2 (mfp ctx p,
adamc@193 762 fn p' =>
adamc@193 763 S.map2 (mfc ctx c,
adamc@193 764 fn c' =>
adamc@193 765 (x, p', c')))) xps,
adamc@193 766 fn xps' =>
adamc@193 767 (PRecord xps', loc))
adamc@193 768
adamc@193 769 and mfpc ctx pc =
adamc@193 770 case pc of
adamc@193 771 PConVar _ => S.return2 pc
adamc@193 772 | PConFfi {mod = m, datatyp, params, con, arg, kind} =>
adamc@193 773 S.map2 ((case arg of
adamc@193 774 NONE => S.return2 NONE
adamc@193 775 | SOME c => S.map2 (mfc ctx c, SOME)),
adamc@193 776 fn arg' =>
adamc@193 777 PConFfi {mod = m, datatyp = datatyp, params = params,
adamc@193 778 con = con, arg = arg', kind = kind})
adamc@16 779 in
adamc@16 780 mfe
adamc@16 781 end
adamc@16 782
adamc@16 783 fun mapfold {kind = fk, con = fc, exp = fe} =
adamc@626 784 mapfoldB {kind = fn () => fk,
adamc@16 785 con = fn () => fc,
adamc@16 786 exp = fn () => fe,
adamc@16 787 bind = fn ((), _) => ()} ()
adamc@16 788
adamc@21 789 fun mapB {kind, con, exp, bind} ctx e =
adamc@626 790 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@21 791 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@21 792 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
adamc@21 793 bind = bind} ctx e () of
adamc@21 794 S.Continue (e, ()) => e
adamc@21 795 | S.Return _ => raise Fail "CoreUtil.Exp.mapB: Impossible"
adamc@21 796
adamc@16 797 fun map {kind, con, exp} e =
adamc@16 798 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@16 799 con = fn c => fn () => S.Continue (con c, ()),
adamc@16 800 exp = fn e => fn () => S.Continue (exp e, ())} e () of
adamc@16 801 S.Return () => raise Fail "Core_util.Exp.map"
adamc@16 802 | S.Continue (e, ()) => e
adamc@16 803
adamc@23 804 fun fold {kind, con, exp} s e =
adamc@23 805 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
adamc@23 806 con = fn c => fn s => S.Continue (c, con (c, s)),
adamc@23 807 exp = fn e => fn s => S.Continue (e, exp (e, s))} e s of
adamc@23 808 S.Continue (_, s) => s
adamc@23 809 | S.Return _ => raise Fail "CoreUtil.Exp.fold: Impossible"
adamc@23 810
adamc@484 811 fun foldB {kind, con, exp, bind} ctx s e =
adamc@626 812 case mapfoldB {kind = fn ctx => fn k => fn s => S.Continue (k, kind (ctx, k, s)),
adamc@484 813 con = fn ctx => fn c => fn s => S.Continue (c, con (ctx, c, s)),
adamc@484 814 exp = fn ctx => fn e => fn s => S.Continue (e, exp (ctx, e, s)),
adamc@484 815 bind = bind} ctx e s of
adamc@484 816 S.Continue (_, s) => s
adamc@484 817 | S.Return _ => raise Fail "CoreUtil.Exp.foldB: Impossible"
adamc@484 818
adamc@16 819 fun exists {kind, con, exp} k =
adamc@16 820 case mapfold {kind = fn k => fn () =>
adamc@16 821 if kind k then
adamc@16 822 S.Return ()
adamc@16 823 else
adamc@16 824 S.Continue (k, ()),
adamc@16 825 con = fn c => fn () =>
adamc@16 826 if con c then
adamc@16 827 S.Return ()
adamc@16 828 else
adamc@16 829 S.Continue (c, ()),
adamc@16 830 exp = fn e => fn () =>
adamc@16 831 if exp e then
adamc@16 832 S.Return ()
adamc@16 833 else
adamc@16 834 S.Continue (e, ())} k () of
adamc@16 835 S.Return _ => true
adamc@16 836 | S.Continue _ => false
adamc@16 837
adamc@479 838 fun existsB {kind, con, exp, bind} ctx k =
adamc@626 839 case mapfoldB {kind = fn ctx => fn k => fn () =>
adamc@626 840 if kind (ctx, k) then
adamc@626 841 S.Return ()
adamc@626 842 else
adamc@626 843 S.Continue (k, ()),
adamc@479 844 con = fn ctx => fn c => fn () =>
adamc@479 845 if con (ctx, c) then
adamc@479 846 S.Return ()
adamc@479 847 else
adamc@479 848 S.Continue (c, ()),
adamc@479 849 exp = fn ctx => fn e => fn () =>
adamc@479 850 if exp (ctx, e) then
adamc@479 851 S.Return ()
adamc@479 852 else
adamc@479 853 S.Continue (e, ()),
adamc@479 854 bind = bind} ctx k () of
adamc@479 855 S.Return _ => true
adamc@479 856 | S.Continue _ => false
adamc@479 857
adamc@443 858 fun foldMap {kind, con, exp} s e =
adamc@443 859 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
adamc@443 860 con = fn c => fn s => S.Continue (con (c, s)),
adamc@443 861 exp = fn e => fn s => S.Continue (exp (e, s))} e s of
adamc@443 862 S.Continue v => v
adamc@443 863 | S.Return _ => raise Fail "CoreUtil.Exp.foldMap: Impossible"
adamc@443 864
adamc@488 865 fun foldMapB {kind, con, exp, bind} ctx s e =
adamc@626 866 case mapfoldB {kind = fn ctx => fn k => fn s => S.Continue (kind (ctx, k, s)),
adamc@488 867 con = fn ctx => fn c => fn s => S.Continue (con (ctx, c, s)),
adamc@488 868 exp = fn ctx => fn e => fn s => S.Continue (exp (ctx, e, s)),
adamc@488 869 bind = bind} ctx e s of
adamc@488 870 S.Continue v => v
adamc@488 871 | S.Return _ => raise Fail "CoreUtil.Exp.foldMapB: Impossible"
adamc@488 872
adamc@16 873 end
adamc@16 874
adamc@20 875 structure Decl = struct
adamc@20 876
adamc@20 877 datatype binder = datatype Exp.binder
adamc@20 878
adamc@20 879 fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} =
adamc@20 880 let
adamc@626 881 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@20 882
adamc@20 883 fun bind' (ctx, b) =
adamc@20 884 let
adamc@20 885 val b' = case b of
adamc@626 886 Con.RelK x => RelK x
adamc@626 887 | Con.RelC x => RelC x
adamc@626 888 | Con.NamedC x => NamedC x
adamc@20 889 in
adamc@20 890 bind (ctx, b')
adamc@20 891 end
adamc@20 892 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@20 893
adamc@20 894 val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind}
adamc@20 895
adamc@20 896 fun mfd ctx d acc =
adamc@20 897 S.bindP (mfd' ctx d acc, fd ctx)
adamc@20 898
adamc@20 899 and mfd' ctx (dAll as (d, loc)) =
adamc@20 900 case d of
adamc@20 901 DCon (x, n, k, c) =>
adamc@626 902 S.bind2 (mfk ctx k,
adamc@20 903 fn k' =>
adamc@20 904 S.map2 (mfc ctx c,
adamc@20 905 fn c' =>
adamc@20 906 (DCon (x, n, k', c'), loc)))
adamc@192 907 | DDatatype (x, n, xs, xncs) =>
adamc@196 908 let
adamc@196 909 val k = (KType, loc)
adamc@196 910 val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
adamc@196 911 val ctx' = bind (ctx, NamedC (x, n, k', NONE))
adamc@196 912 in
adamc@196 913 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@196 914 case c of
adamc@196 915 NONE => S.return2 (x, n, c)
adamc@196 916 | SOME c =>
adamc@196 917 S.map2 (mfc ctx' c,
adamc@196 918 fn c' => (x, n, SOME c'))) xncs,
adamc@196 919 fn xncs' =>
adamc@196 920 (DDatatype (x, n, xs, xncs'), loc))
adamc@196 921 end
adamc@125 922 | DVal vi =>
adamc@125 923 S.map2 (mfvi ctx vi,
adamc@125 924 fn vi' =>
adamc@125 925 (DVal vi', loc))
adamc@125 926 | DValRec vis =>
adamc@127 927 let
adamc@127 928 val ctx = foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s)))
adamc@127 929 ctx vis
adamc@127 930 in
adamc@127 931 S.map2 (ListUtil.mapfold (mfvi ctx) vis,
adamc@127 932 fn vis' =>
adamc@127 933 (DValRec vis', loc))
adamc@127 934 end
adamc@109 935 | DExport _ => S.return2 dAll
adamc@707 936 | DTable (x, n, c, s, pe, pc, ce, cc) =>
adamc@704 937 S.bind2 (mfc ctx c,
adamc@461 938 fn c' =>
adamc@707 939 S.bind2 (mfe ctx pe,
adamc@707 940 fn pe' =>
adamc@707 941 S.bind2 (mfc ctx pc,
adamc@707 942 fn pc' =>
adamc@707 943 S.bind2 (mfe ctx ce,
adamc@707 944 fn ce' =>
adamc@707 945 S.map2 (mfc ctx cc,
adamc@707 946 fn cc' =>
adamc@707 947 (DTable (x, n, c', s, pe', pc', ce', cc'), loc))))))
adamc@338 948 | DSequence _ => S.return2 dAll
adamc@271 949 | DDatabase _ => S.return2 dAll
adamc@461 950 | DCookie (x, n, c, s) =>
adamc@461 951 S.map2 (mfc ctx c,
adamc@461 952 fn c' =>
adamc@461 953 (DCookie (x, n, c', s), loc))
adamc@125 954
adamc@125 955 and mfvi ctx (x, n, t, e, s) =
adamc@125 956 S.bind2 (mfc ctx t,
adamc@125 957 fn t' =>
adamc@125 958 S.map2 (mfe ctx e,
adamc@125 959 fn e' =>
adamc@125 960 (x, n, t', e', s)))
adamc@20 961 in
adamc@20 962 mfd
adamc@20 963 end
adamc@20 964
adamc@23 965 fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} =
adamc@626 966 mapfoldB {kind = fn () => fk,
adamc@23 967 con = fn () => fc,
adamc@23 968 exp = fn () => fe,
adamc@23 969 decl = fn () => fd,
adamc@23 970 bind = fn ((), _) => ()} ()
adamc@23 971
adamc@23 972 fun fold {kind, con, exp, decl} s d =
adamc@23 973 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
adamc@23 974 con = fn c => fn s => S.Continue (c, con (c, s)),
adamc@23 975 exp = fn e => fn s => S.Continue (e, exp (e, s)),
adamc@23 976 decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
adamc@23 977 S.Continue (_, s) => s
adamc@23 978 | S.Return _ => raise Fail "CoreUtil.Decl.fold: Impossible"
adamc@23 979
adamc@110 980 fun foldMap {kind, con, exp, decl} s d =
adamc@110 981 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
adamc@110 982 con = fn c => fn s => S.Continue (con (c, s)),
adamc@110 983 exp = fn e => fn s => S.Continue (exp (e, s)),
adamc@110 984 decl = fn d => fn s => S.Continue (decl (d, s))} d s of
adamc@110 985 S.Continue v => v
adamc@110 986 | S.Return _ => raise Fail "CoreUtil.Decl.foldMap: Impossible"
adamc@110 987
adamc@484 988 fun foldMapB {kind, con, exp, decl, bind} ctx s d =
adamc@626 989 case mapfoldB {kind = fn ctx => fn k => fn s => S.Continue (kind (ctx, k, s)),
adamc@484 990 con = fn ctx => fn c => fn s => S.Continue (con (ctx, c, s)),
adamc@484 991 exp = fn ctx => fn e => fn s => S.Continue (exp (ctx, e, s)),
adamc@484 992 decl = fn ctx => fn d => fn s => S.Continue (decl (ctx, d, s)),
adamc@484 993 bind = bind} ctx d s of
adamc@484 994 S.Continue v => v
adamc@484 995 | S.Return _ => raise Fail "CoreUtil.Decl.foldMapB: Impossible"
adamc@484 996
adamc@522 997 fun exists {kind, con, exp, decl} d =
adamc@522 998 case mapfold {kind = fn k => fn () =>
adamc@522 999 if kind k then
adamc@522 1000 S.Return ()
adamc@522 1001 else
adamc@522 1002 S.Continue (k, ()),
adamc@522 1003 con = fn c => fn () =>
adamc@522 1004 if con c then
adamc@522 1005 S.Return ()
adamc@522 1006 else
adamc@522 1007 S.Continue (c, ()),
adamc@522 1008 exp = fn e => fn () =>
adamc@522 1009 if exp e then
adamc@522 1010 S.Return ()
adamc@522 1011 else
adamc@522 1012 S.Continue (e, ()),
adamc@522 1013 decl = fn d => fn () =>
adamc@522 1014 if decl d then
adamc@522 1015 S.Return ()
adamc@522 1016 else
adamc@522 1017 S.Continue (d, ())} d () of
adamc@522 1018 S.Return _ => true
adamc@522 1019 | S.Continue _ => false
adamc@522 1020
adamc@16 1021 end
adamc@20 1022
adamc@20 1023 structure File = struct
adamc@20 1024
adamc@20 1025 datatype binder = datatype Exp.binder
adamc@20 1026
adamc@20 1027 fun mapfoldB (all as {bind, ...}) =
adamc@20 1028 let
adamc@20 1029 val mfd = Decl.mapfoldB all
adamc@20 1030
adamc@20 1031 fun mff ctx ds =
adamc@20 1032 case ds of
adamc@20 1033 nil => S.return2 nil
adamc@20 1034 | d :: ds' =>
adamc@20 1035 S.bind2 (mfd ctx d,
adamc@20 1036 fn d' =>
adamc@20 1037 let
adamc@100 1038 val ctx' =
adamc@20 1039 case #1 d' of
adamc@100 1040 DCon (x, n, k, c) => bind (ctx, NamedC (x, n, k, SOME c))
adamc@192 1041 | DDatatype (x, n, xs, xncs) =>
adamc@163 1042 let
adamc@192 1043 val loc = #2 d'
adamc@192 1044 val k = (KType, loc)
adamc@192 1045 val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
adamc@192 1046
adamc@192 1047 val ctx = bind (ctx, NamedC (x, n, k', NONE))
adamc@163 1048 val t = (CNamed n, #2 d')
adamc@192 1049 val t = ListUtil.foldli (fn (i, _, t) => (CApp (t, (CRel i, loc)), loc))
adamc@192 1050 t xs
adamc@163 1051 in
adamc@163 1052 foldl (fn ((x, n, to), ctx) =>
adamc@163 1053 let
adamc@163 1054 val t = case to of
adamc@163 1055 NONE => t
adamc@163 1056 | SOME t' => (TFun (t', t), #2 d')
adamc@192 1057 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc))
adamc@192 1058 t xs
adamc@163 1059 in
adamc@163 1060 bind (ctx, NamedE (x, n, t, NONE, ""))
adamc@163 1061 end)
adamc@163 1062 ctx xncs
adamc@163 1063 end
adamc@109 1064 | DVal (x, n, t, e, s) => bind (ctx, NamedE (x, n, t, SOME e, s))
adamc@125 1065 | DValRec vis =>
adamc@127 1066 foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s)))
adamc@125 1067 ctx vis
adamc@109 1068 | DExport _ => ctx
adamc@707 1069 | DTable (x, n, c, s, _, pc, _, cc) =>
adamc@247 1070 let
adamc@705 1071 val loc = #2 d'
adamc@705 1072 val ct = (CFfi ("Basis", "sql_table"), loc)
adamc@707 1073 val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc)
adamc@705 1074 val ct = (CApp (ct, cc), loc)
adamc@338 1075 in
adamc@705 1076 bind (ctx, NamedE (x, n, ct, NONE, s))
adamc@338 1077 end
adamc@338 1078 | DSequence (x, n, s) =>
adamc@338 1079 let
adamc@338 1080 val t = (CFfi ("Basis", "sql_sequence"), #2 d')
adamc@247 1081 in
adamc@247 1082 bind (ctx, NamedE (x, n, t, NONE, s))
adamc@247 1083 end
adamc@271 1084 | DDatabase _ => ctx
adamc@461 1085 | DCookie (x, n, c, s) =>
adamc@461 1086 let
adamc@461 1087 val t = (CApp ((CFfi ("Basis", "http_cookie"), #2 d'), c), #2 d')
adamc@461 1088 in
adamc@461 1089 bind (ctx, NamedE (x, n, t, NONE, s))
adamc@461 1090 end
adamc@20 1091 in
adamc@20 1092 S.map2 (mff ctx' ds',
adamc@20 1093 fn ds' =>
adamc@20 1094 d' :: ds')
adamc@20 1095 end)
adamc@20 1096 in
adamc@20 1097 mff
adamc@20 1098 end
adamc@20 1099
adamc@23 1100 fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} =
adamc@626 1101 mapfoldB {kind = fn () => fk,
adamc@23 1102 con = fn () => fc,
adamc@23 1103 exp = fn () => fe,
adamc@23 1104 decl = fn () => fd,
adamc@23 1105 bind = fn ((), _) => ()} ()
adamc@23 1106
adamc@20 1107 fun mapB {kind, con, exp, decl, bind} ctx ds =
adamc@626 1108 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@20 1109 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@20 1110 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
adamc@20 1111 decl = fn ctx => fn d => fn () => S.Continue (decl ctx d, ()),
adamc@20 1112 bind = bind} ctx ds () of
adamc@20 1113 S.Continue (ds, ()) => ds
adamc@20 1114 | S.Return _ => raise Fail "CoreUtil.File.mapB: Impossible"
adamc@20 1115
adamc@482 1116 fun map {kind, con, exp, decl} ds =
adamc@626 1117 mapB {kind = fn () => kind,
adamc@482 1118 con = fn () => con,
adamc@482 1119 exp = fn () => exp,
adamc@482 1120 decl = fn () => decl,
adamc@482 1121 bind = fn _ => ()} () ds
adamc@482 1122
adamc@23 1123 fun fold {kind, con, exp, decl} s d =
adamc@23 1124 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
adamc@23 1125 con = fn c => fn s => S.Continue (c, con (c, s)),
adamc@23 1126 exp = fn e => fn s => S.Continue (e, exp (e, s)),
adamc@23 1127 decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
adamc@23 1128 S.Continue (_, s) => s
adamc@23 1129 | S.Return _ => raise Fail "CoreUtil.File.fold: Impossible"
adamc@23 1130
adamc@110 1131 fun foldMap {kind, con, exp, decl} s d =
adamc@110 1132 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
adamc@110 1133 con = fn c => fn s => S.Continue (con (c, s)),
adamc@110 1134 exp = fn e => fn s => S.Continue (exp (e, s)),
adamc@110 1135 decl = fn d => fn s => S.Continue (decl (d, s))} d s of
adamc@110 1136 S.Continue v => v
adamc@110 1137 | S.Return _ => raise Fail "CoreUtil.File.foldMap: Impossible"
adamc@110 1138
adamc@179 1139 val maxName = foldl (fn ((d, _) : decl, count) =>
adamc@179 1140 case d of
adamc@179 1141 DCon (_, n, _, _) => Int.max (n, count)
adamc@398 1142 | DDatatype (_, n, _, ns) =>
adamc@398 1143 foldl (fn ((_, n', _), m) => Int.max (n', m))
adamc@398 1144 (Int.max (n, count)) ns
adamc@179 1145 | DVal (_, n, _, _, _) => Int.max (n, count)
adamc@179 1146 | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis
adamc@247 1147 | DExport _ => count
adamc@707 1148 | DTable (_, n, _, _, _, _, _, _) => Int.max (n, count)
adamc@338 1149 | DSequence (_, n, _) => Int.max (n, count)
adamc@461 1150 | DDatabase _ => count
adamc@461 1151 | DCookie (_, n, _, _) => Int.max (n, count)) 0
adamc@179 1152
adamc@20 1153 end
adamc@20 1154
adamc@20 1155 end