Mercurial > urweb

annotate src/core_util.sml @ 2191:849404a3af27

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