Mercurial > urweb

annotate src/core_util.sml @ 2101:32e2752390ad

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixing one small issue with changes to signature matching (grandfathered into release)
author Adam Chlipala <adam@chlipala.net>
date Sat, 03 Jan 2015 10:21:26 -0500
parents e15234fbb163
children b90103106177
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)) =>
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
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) =>
adamc@192 610 S.map2 (ListUtil.mapfold (mfc ctx) cs,
adamc@192 611 fn cs' =>
adamc@192 612 (ECon (dk, pc, cs', NONE), loc))
adamc@192 613 | ECon (dk, n, cs, SOME e) =>
adamc@192 614 S.bind2 (mfe ctx e,
adamc@192 615 fn e' =>
adamc@192 616 S.map2 (ListUtil.mapfold (mfc ctx) cs,
adamc@192 617 fn cs' =>
adamc@192 618 (ECon (dk, n, cs', SOME e'), loc)))
adamc@48 619 | EFfi _ => S.return2 eAll
adamc@48 620 | EFfiApp (m, x, es) =>
adam@1663 621 S.map2 (ListUtil.mapfold (mfet ctx) es,
adamc@48 622 fn es' =>
adamc@48 623 (EFfiApp (m, x, es'), loc))
adamc@16 624 | EApp (e1, e2) =>
adamc@16 625 S.bind2 (mfe ctx e1,
adamc@16 626 fn e1' =>
adamc@16 627 S.map2 (mfe ctx e2,
adamc@16 628 fn e2' =>
adamc@16 629 (EApp (e1', e2'), loc)))
adamc@26 630 | EAbs (x, dom, ran, e) =>
adamc@26 631 S.bind2 (mfc ctx dom,
adamc@26 632 fn dom' =>
adamc@26 633 S.bind2 (mfc ctx ran,
adamc@26 634 fn ran' =>
adamc@26 635 S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
adamc@26 636 fn e' =>
adamc@26 637 (EAbs (x, dom', ran', e'), loc))))
adamc@16 638
adamc@16 639 | ECApp (e, c) =>
adamc@16 640 S.bind2 (mfe ctx e,
adamc@16 641 fn e' =>
adamc@16 642 S.map2 (mfc ctx c,
adamc@16 643 fn c' =>
adamc@16 644 (ECApp (e', c'), loc)))
adamc@16 645 | ECAbs (x, k, e) =>
adamc@626 646 S.bind2 (mfk ctx k,
adamc@16 647 fn k' =>
adamc@16 648 S.map2 (mfe (bind (ctx, RelC (x, k))) e,
adamc@16 649 fn e' =>
adamc@16 650 (ECAbs (x, k', e'), loc)))
adamc@16 651
adamc@16 652 | ERecord xes =>
adamc@29 653 S.map2 (ListUtil.mapfold (fn (x, e, t) =>
adamc@16 654 S.bind2 (mfc ctx x,
adamc@16 655 fn x' =>
adamc@29 656 S.bind2 (mfe ctx e,
adamc@29 657 fn e' =>
adamc@29 658 S.map2 (mfc ctx t,
adamc@29 659 fn t' =>
adamc@29 660 (x', e', t')))))
adamc@16 661 xes,
adamc@16 662 fn xes' =>
adamc@16 663 (ERecord xes', loc))
adamc@16 664 | EField (e, c, {field, rest}) =>
adamc@16 665 S.bind2 (mfe ctx e,
adamc@16 666 fn e' =>
adamc@16 667 S.bind2 (mfc ctx c,
adamc@16 668 fn c' =>
adamc@16 669 S.bind2 (mfc ctx field,
adamc@16 670 fn field' =>
adamc@16 671 S.map2 (mfc ctx rest,
adamc@16 672 fn rest' =>
adamc@16 673 (EField (e', c', {field = field', rest = rest'}), loc)))))
adamc@445 674 | EConcat (e1, c1, e2, c2) =>
adamc@339 675 S.bind2 (mfe ctx e1,
adamc@339 676 fn e1' =>
adamc@445 677 S.bind2 (mfc ctx c1,
adamc@445 678 fn c1' =>
adamc@339 679 S.bind2 (mfe ctx e2,
adamc@339 680 fn e2' =>
adamc@445 681 S.map2 (mfc ctx c2,
adamc@445 682 fn c2' =>
adamc@445 683 (EConcat (e1', c1', e2', c2'),
adamc@445 684 loc)))))
adamc@149 685 | ECut (e, c, {field, rest}) =>
adamc@149 686 S.bind2 (mfe ctx e,
adamc@149 687 fn e' =>
adamc@149 688 S.bind2 (mfc ctx c,
adamc@149 689 fn c' =>
adamc@149 690 S.bind2 (mfc ctx field,
adamc@149 691 fn field' =>
adamc@149 692 S.map2 (mfc ctx rest,
adamc@149 693 fn rest' =>
adamc@149 694 (ECut (e', c', {field = field', rest = rest'}), loc)))))
adamc@493 695 | ECutMulti (e, c, {rest}) =>
adamc@493 696 S.bind2 (mfe ctx e,
adamc@493 697 fn e' =>
adamc@493 698 S.bind2 (mfc ctx c,
adamc@493 699 fn c' =>
adamc@493 700 S.map2 (mfc ctx rest,
adamc@493 701 fn rest' =>
adamc@493 702 (ECutMulti (e', c', {rest = rest'}), loc))))
adamc@102 703
adamc@182 704 | ECase (e, pes, {disc, result}) =>
adamc@177 705 S.bind2 (mfe ctx e,
adamc@177 706 fn e' =>
adamc@177 707 S.bind2 (ListUtil.mapfold (fn (p, e) =>
adamc@193 708 let
adamc@193 709 fun pb ((p, _), ctx) =
adamc@193 710 case p of
adamc@193 711 PWild => ctx
adamc@193 712 | PVar (x, t) => bind (ctx, RelE (x, t))
adamc@193 713 | PPrim _ => ctx
adamc@193 714 | PCon (_, _, _, NONE) => ctx
adamc@193 715 | PCon (_, _, _, SOME p) => pb (p, ctx)
adamc@193 716 | PRecord xps => foldl (fn ((_, p, _), ctx) =>
adamc@193 717 pb (p, ctx)) ctx xps
adamc@193 718 in
adamc@193 719 S.bind2 (mfp ctx p,
adamc@193 720 fn p' =>
adamc@193 721 S.map2 (mfe (pb (p', ctx)) e,
adamc@193 722 fn e' => (p', e')))
adamc@193 723 end) pes,
adamc@177 724 fn pes' =>
adamc@182 725 S.bind2 (mfc ctx disc,
adamc@182 726 fn disc' =>
adamc@182 727 S.map2 (mfc ctx result,
adamc@182 728 fn result' =>
adamc@182 729 (ECase (e', pes', {disc = disc', result = result'}), loc)))))
adamc@177 730
adamc@102 731 | EWrite e =>
adamc@102 732 S.map2 (mfe ctx e,
adamc@102 733 fn e' =>
adamc@102 734 (EWrite e', loc))
adamc@110 735
adamc@110 736 | EClosure (n, es) =>
adamc@110 737 S.map2 (ListUtil.mapfold (mfe ctx) es,
adamc@110 738 fn es' =>
adamc@110 739 (EClosure (n, es'), loc))
adamc@193 740
adamc@450 741 | ELet (x, t, e1, e2) =>
adamc@450 742 S.bind2 (mfc ctx t,
adamc@450 743 fn t' =>
adamc@450 744 S.bind2 (mfe ctx e1,
adamc@450 745 fn e1' =>
adamc@453 746 S.map2 (mfe (bind (ctx, RelE (x, t'))) e2,
adamc@450 747 fn e2' =>
adamc@450 748 (ELet (x, t', e1', e2'), loc))))
adamc@450 749
adam@1848 750 | EServerCall (n, es, t, fm) =>
adamc@607 751 S.bind2 (ListUtil.mapfold (mfe ctx) es,
adamc@607 752 fn es' =>
adamc@1020 753 S.map2 (mfc ctx t,
adamc@1020 754 fn t' =>
adam@1848 755 (EServerCall (n, es', t', fm), loc)))
adamc@954 756
adamc@626 757 | EKAbs (x, e) =>
adamc@626 758 S.map2 (mfe (bind (ctx, RelK x)) e,
adamc@626 759 fn e' =>
adamc@626 760 (EKAbs (x, e'), loc))
adamc@626 761 | EKApp (e, k) =>
adamc@626 762 S.bind2 (mfe ctx e,
adamc@626 763 fn e' =>
adamc@626 764 S.map2 (mfk ctx k,
adamc@626 765 fn k' =>
adamc@626 766 (EKApp (e', k'), loc)))
adamc@607 767
adamc@193 768 and mfp ctx (pAll as (p, loc)) =
adamc@193 769 case p of
adamc@193 770 PWild => S.return2 pAll
adamc@193 771 | PVar (x, t) =>
adamc@193 772 S.map2 (mfc ctx t,
adamc@193 773 fn t' =>
adamc@193 774 (PVar (x, t'), loc))
adamc@193 775 | PPrim _ => S.return2 pAll
adamc@193 776 | PCon (dk, pc, args, po) =>
adamc@193 777 S.bind2 (mfpc ctx pc,
adamc@193 778 fn pc' =>
adamc@193 779 S.bind2 (ListUtil.mapfold (mfc ctx) args,
adamc@193 780 fn args' =>
adamc@193 781 S.map2 ((case po of
adamc@193 782 NONE => S.return2 NONE
adamc@193 783 | SOME p => S.map2 (mfp ctx p, SOME)),
adamc@193 784 fn po' =>
adamc@193 785 (PCon (dk, pc', args', po'), loc))))
adamc@193 786 | PRecord xps =>
adamc@193 787 S.map2 (ListUtil.mapfold (fn (x, p, c) =>
adamc@193 788 S.bind2 (mfp ctx p,
adamc@193 789 fn p' =>
adamc@193 790 S.map2 (mfc ctx c,
adamc@193 791 fn c' =>
adamc@193 792 (x, p', c')))) xps,
adamc@193 793 fn xps' =>
adamc@193 794 (PRecord xps', loc))
adamc@193 795
adamc@193 796 and mfpc ctx pc =
adamc@193 797 case pc of
adamc@193 798 PConVar _ => S.return2 pc
adamc@193 799 | PConFfi {mod = m, datatyp, params, con, arg, kind} =>
adamc@193 800 S.map2 ((case arg of
adamc@193 801 NONE => S.return2 NONE
adamc@796 802 | SOME c =>
adamc@796 803 let
adamc@796 804 val k = (KType, ErrorMsg.dummySpan)
adamc@796 805 val ctx' = foldl (fn (x, ctx) => bind (ctx, RelC (x, k))) ctx params
adamc@796 806 in
adamc@796 807 S.map2 (mfc ctx' c, SOME)
adamc@796 808 end),
adamc@193 809 fn arg' =>
adamc@193 810 PConFfi {mod = m, datatyp = datatyp, params = params,
adamc@193 811 con = con, arg = arg', kind = kind})
adamc@16 812 in
adamc@16 813 mfe
adamc@16 814 end
adamc@16 815
adamc@16 816 fun mapfold {kind = fk, con = fc, exp = fe} =
adamc@626 817 mapfoldB {kind = fn () => fk,
adamc@16 818 con = fn () => fc,
adamc@16 819 exp = fn () => fe,
adamc@16 820 bind = fn ((), _) => ()} ()
adamc@16 821
adamc@21 822 fun mapB {kind, con, exp, bind} ctx e =
adamc@626 823 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@21 824 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@21 825 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
adamc@21 826 bind = bind} ctx e () of
adamc@21 827 S.Continue (e, ()) => e
adamc@21 828 | S.Return _ => raise Fail "CoreUtil.Exp.mapB: Impossible"
adamc@21 829
adamc@16 830 fun map {kind, con, exp} e =
adamc@16 831 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@16 832 con = fn c => fn () => S.Continue (con c, ()),
adamc@16 833 exp = fn e => fn () => S.Continue (exp e, ())} e () of
adamc@16 834 S.Return () => raise Fail "Core_util.Exp.map"
adamc@16 835 | S.Continue (e, ()) => e
adamc@16 836
adamc@23 837 fun fold {kind, con, exp} s e =
adamc@23 838 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
adamc@23 839 con = fn c => fn s => S.Continue (c, con (c, s)),
adamc@23 840 exp = fn e => fn s => S.Continue (e, exp (e, s))} e s of
adamc@23 841 S.Continue (_, s) => s
adamc@23 842 | S.Return _ => raise Fail "CoreUtil.Exp.fold: Impossible"
adamc@23 843
adamc@484 844 fun foldB {kind, con, exp, bind} ctx s e =
adamc@626 845 case mapfoldB {kind = fn ctx => fn k => fn s => S.Continue (k, kind (ctx, k, s)),
adamc@484 846 con = fn ctx => fn c => fn s => S.Continue (c, con (ctx, c, s)),
adamc@484 847 exp = fn ctx => fn e => fn s => S.Continue (e, exp (ctx, e, s)),
adamc@484 848 bind = bind} ctx e s of
adamc@484 849 S.Continue (_, s) => s
adamc@484 850 | S.Return _ => raise Fail "CoreUtil.Exp.foldB: Impossible"
adamc@484 851
adamc@16 852 fun exists {kind, con, exp} k =
adamc@16 853 case mapfold {kind = fn k => fn () =>
adamc@16 854 if kind k then
adamc@16 855 S.Return ()
adamc@16 856 else
adamc@16 857 S.Continue (k, ()),
adamc@16 858 con = fn c => fn () =>
adamc@16 859 if con c then
adamc@16 860 S.Return ()
adamc@16 861 else
adamc@16 862 S.Continue (c, ()),
adamc@16 863 exp = fn e => fn () =>
adamc@16 864 if exp e then
adamc@16 865 S.Return ()
adamc@16 866 else
adamc@16 867 S.Continue (e, ())} k () of
adamc@16 868 S.Return _ => true
adamc@16 869 | S.Continue _ => false
adamc@16 870
adamc@479 871 fun existsB {kind, con, exp, bind} ctx k =
adamc@626 872 case mapfoldB {kind = fn ctx => fn k => fn () =>
adamc@626 873 if kind (ctx, k) then
adamc@626 874 S.Return ()
adamc@626 875 else
adamc@626 876 S.Continue (k, ()),
adamc@479 877 con = fn ctx => fn c => fn () =>
adamc@479 878 if con (ctx, c) then
adamc@479 879 S.Return ()
adamc@479 880 else
adamc@479 881 S.Continue (c, ()),
adamc@479 882 exp = fn ctx => fn e => fn () =>
adamc@479 883 if exp (ctx, e) then
adamc@479 884 S.Return ()
adamc@479 885 else
adamc@479 886 S.Continue (e, ()),
adamc@479 887 bind = bind} ctx k () of
adamc@479 888 S.Return _ => true
adamc@479 889 | S.Continue _ => false
adamc@479 890
adamc@443 891 fun foldMap {kind, con, exp} s e =
adamc@443 892 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
adamc@443 893 con = fn c => fn s => S.Continue (con (c, s)),
adamc@443 894 exp = fn e => fn s => S.Continue (exp (e, s))} e s of
adamc@443 895 S.Continue v => v
adamc@443 896 | S.Return _ => raise Fail "CoreUtil.Exp.foldMap: Impossible"
adamc@443 897
adamc@488 898 fun foldMapB {kind, con, exp, bind} ctx s e =
adamc@626 899 case mapfoldB {kind = fn ctx => fn k => fn s => S.Continue (kind (ctx, k, s)),
adamc@488 900 con = fn ctx => fn c => fn s => S.Continue (con (ctx, c, s)),
adamc@488 901 exp = fn ctx => fn e => fn s => S.Continue (exp (ctx, e, s)),
adamc@488 902 bind = bind} ctx e s of
adamc@488 903 S.Continue v => v
adamc@488 904 | S.Return _ => raise Fail "CoreUtil.Exp.foldMapB: Impossible"
adamc@488 905
adamc@16 906 end
adamc@16 907
adamc@20 908 structure Decl = struct
adamc@20 909
adamc@20 910 datatype binder = datatype Exp.binder
adamc@20 911
adamc@20 912 fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} =
adamc@20 913 let
adamc@626 914 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@20 915
adamc@20 916 fun bind' (ctx, b) =
adamc@20 917 let
adamc@20 918 val b' = case b of
adamc@626 919 Con.RelK x => RelK x
adamc@626 920 | Con.RelC x => RelC x
adamc@626 921 | Con.NamedC x => NamedC x
adamc@20 922 in
adamc@20 923 bind (ctx, b')
adamc@20 924 end
adamc@20 925 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@20 926
adamc@20 927 val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind}
adamc@20 928
adamc@20 929 fun mfd ctx d acc =
adamc@20 930 S.bindP (mfd' ctx d acc, fd ctx)
adamc@20 931
adamc@20 932 and mfd' ctx (dAll as (d, loc)) =
adamc@20 933 case d of
adamc@20 934 DCon (x, n, k, c) =>
adamc@626 935 S.bind2 (mfk ctx k,
adamc@20 936 fn k' =>
adamc@20 937 S.map2 (mfc ctx c,
adamc@20 938 fn c' =>
adamc@20 939 (DCon (x, n, k', c'), loc)))
adamc@807 940 | DDatatype dts =>
adamc@807 941 S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
adamc@807 942 let
adamc@807 943 val k = (KType, loc)
adamc@807 944 val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
adamc@807 945 val ctx' = bind (ctx, NamedC (x, n, k', NONE))
adamc@807 946 in
adamc@807 947 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@807 948 case c of
adamc@807 949 NONE => S.return2 (x, n, c)
adamc@807 950 | SOME c =>
adamc@807 951 S.map2 (mfc ctx' c,
adamc@807 952 fn c' => (x, n, SOME c'))) xncs,
adamc@807 953 fn xncs' => (x, n, xs, xncs'))
adamc@807 954 end) dts,
adamc@807 955 fn dts' =>
adamc@807 956 (DDatatype dts', loc))
adamc@125 957 | DVal vi =>
adamc@125 958 S.map2 (mfvi ctx vi,
adamc@125 959 fn vi' =>
adamc@125 960 (DVal vi', loc))
adamc@125 961 | DValRec vis =>
adamc@127 962 let
adamc@127 963 val ctx = foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s)))
adamc@127 964 ctx vis
adamc@127 965 in
adamc@127 966 S.map2 (ListUtil.mapfold (mfvi ctx) vis,
adamc@127 967 fn vis' =>
adamc@127 968 (DValRec vis', loc))
adamc@127 969 end
adamc@109 970 | DExport _ => S.return2 dAll
adamc@707 971 | DTable (x, n, c, s, pe, pc, ce, cc) =>
adamc@802 972 let
adamc@802 973 val loc = #2 ce
adamc@802 974 val ct = (CFfi ("Basis", "sql_table"), loc)
adamc@802 975 val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc)
adamc@802 976 val ct = (CApp (ct, cc), loc)
adamc@802 977 val ctx' = bind (ctx, NamedE (x, n, ct, NONE, s))
adamc@802 978 in
adamc@802 979 S.bind2 (mfc ctx c,
adamc@802 980 fn c' =>
adamc@802 981 S.bind2 (mfe ctx' pe,
adamc@802 982 fn pe' =>
adamc@802 983 S.bind2 (mfc ctx pc,
adamc@802 984 fn pc' =>
adamc@802 985 S.bind2 (mfe ctx' ce,
adamc@802 986 fn ce' =>
adamc@802 987 S.map2 (mfc ctx cc,
adamc@802 988 fn cc' =>
adamc@802 989 (DTable (x, n, c', s, pe', pc', ce', cc'), loc))))))
adamc@802 990 end
adamc@338 991 | DSequence _ => S.return2 dAll
adamc@754 992 | DView (x, n, s, e, c) =>
adamc@754 993 S.bind2 (mfe ctx e,
adamc@754 994 fn e' =>
adamc@754 995 S.map2 (mfc ctx c,
adamc@754 996 fn c' =>
adamc@754 997 (DView (x, n, s, e', c'), loc)))
adamc@271 998 | DDatabase _ => S.return2 dAll
adamc@461 999 | DCookie (x, n, c, s) =>
adamc@461 1000 S.map2 (mfc ctx c,
adamc@461 1001 fn c' =>
adamc@461 1002 (DCookie (x, n, c', s), loc))
adamc@720 1003 | DStyle _ => S.return2 dAll
adamc@1075 1004 | DTask (e1, e2) =>
adamc@1075 1005 S.bind2 (mfe ctx e1,
adamc@1075 1006 fn e1' =>
adamc@1075 1007 S.map2 (mfe ctx e2,
adamc@1075 1008 fn e2' =>
adamc@1075 1009 (DTask (e1', e2'), loc)))
adamc@1199 1010 | DPolicy e =>
adamc@1199 1011 S.map2 (mfe ctx e,
adamc@1199 1012 fn e' =>
adamc@1199 1013 (DPolicy e', loc))
adamc@125 1014
adam@1294 1015 | DOnError _ => S.return2 dAll
adam@1294 1016
adamc@125 1017 and mfvi ctx (x, n, t, e, s) =
adamc@125 1018 S.bind2 (mfc ctx t,
adamc@125 1019 fn t' =>
adamc@125 1020 S.map2 (mfe ctx e,
adamc@125 1021 fn e' =>
adamc@125 1022 (x, n, t', e', s)))
adamc@20 1023 in
adamc@20 1024 mfd
adamc@20 1025 end
adamc@20 1026
adamc@23 1027 fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} =
adamc@626 1028 mapfoldB {kind = fn () => fk,
adamc@23 1029 con = fn () => fc,
adamc@23 1030 exp = fn () => fe,
adamc@23 1031 decl = fn () => fd,
adamc@23 1032 bind = fn ((), _) => ()} ()
adamc@23 1033
adamc@23 1034 fun fold {kind, con, exp, decl} s d =
adamc@23 1035 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
adamc@23 1036 con = fn c => fn s => S.Continue (c, con (c, s)),
adamc@23 1037 exp = fn e => fn s => S.Continue (e, exp (e, s)),
adamc@23 1038 decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
adamc@23 1039 S.Continue (_, s) => s
adamc@23 1040 | S.Return _ => raise Fail "CoreUtil.Decl.fold: Impossible"
adamc@23 1041
adamc@110 1042 fun foldMap {kind, con, exp, decl} s d =
adamc@110 1043 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
adamc@110 1044 con = fn c => fn s => S.Continue (con (c, s)),
adamc@110 1045 exp = fn e => fn s => S.Continue (exp (e, s)),
adamc@110 1046 decl = fn d => fn s => S.Continue (decl (d, s))} d s of
adamc@110 1047 S.Continue v => v
adamc@110 1048 | S.Return _ => raise Fail "CoreUtil.Decl.foldMap: Impossible"
adamc@110 1049
adamc@484 1050 fun foldMapB {kind, con, exp, decl, bind} ctx s d =
adamc@626 1051 case mapfoldB {kind = fn ctx => fn k => fn s => S.Continue (kind (ctx, k, s)),
adamc@484 1052 con = fn ctx => fn c => fn s => S.Continue (con (ctx, c, s)),
adamc@484 1053 exp = fn ctx => fn e => fn s => S.Continue (exp (ctx, e, s)),
adamc@484 1054 decl = fn ctx => fn d => fn s => S.Continue (decl (ctx, d, s)),
adamc@484 1055 bind = bind} ctx d s of
adamc@484 1056 S.Continue v => v
adamc@484 1057 | S.Return _ => raise Fail "CoreUtil.Decl.foldMapB: Impossible"
adamc@484 1058
adamc@522 1059 fun exists {kind, con, exp, decl} d =
adamc@522 1060 case mapfold {kind = fn k => fn () =>
adamc@522 1061 if kind k then
adamc@522 1062 S.Return ()
adamc@522 1063 else
adamc@522 1064 S.Continue (k, ()),
adamc@522 1065 con = fn c => fn () =>
adamc@522 1066 if con c then
adamc@522 1067 S.Return ()
adamc@522 1068 else
adamc@522 1069 S.Continue (c, ()),
adamc@522 1070 exp = fn e => fn () =>
adamc@522 1071 if exp e then
adamc@522 1072 S.Return ()
adamc@522 1073 else
adamc@522 1074 S.Continue (e, ()),
adamc@522 1075 decl = fn d => fn () =>
adamc@522 1076 if decl d then
adamc@522 1077 S.Return ()
adamc@522 1078 else
adamc@522 1079 S.Continue (d, ())} d () of
adamc@522 1080 S.Return _ => true
adamc@522 1081 | S.Continue _ => false
adamc@522 1082
adamc@16 1083 end
adamc@20 1084
adamc@20 1085 structure File = struct
adamc@20 1086
adamc@20 1087 datatype binder = datatype Exp.binder
adamc@20 1088
adamc@20 1089 fun mapfoldB (all as {bind, ...}) =
adamc@20 1090 let
adamc@20 1091 val mfd = Decl.mapfoldB all
adamc@20 1092
adamc@20 1093 fun mff ctx ds =
adamc@20 1094 case ds of
adamc@20 1095 nil => S.return2 nil
adamc@20 1096 | d :: ds' =>
adamc@20 1097 S.bind2 (mfd ctx d,
adamc@20 1098 fn d' =>
adamc@20 1099 let
adamc@100 1100 val ctx' =
adamc@20 1101 case #1 d' of
adamc@100 1102 DCon (x, n, k, c) => bind (ctx, NamedC (x, n, k, SOME c))
adamc@807 1103 | DDatatype dts =>
adamc@807 1104 foldl (fn ((x, n, xs, xncs), ctx) =>
adamc@807 1105 let
adamc@807 1106 val loc = #2 d'
adamc@807 1107 val k = (KType, loc)
adamc@807 1108 val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
adamc@192 1109
adamc@807 1110 val ctx = bind (ctx, NamedC (x, n, k', NONE))
adamc@807 1111 val t = (CNamed n, #2 d')
adamc@807 1112 val t = ListUtil.foldli (fn (i, _, t) =>
adamc@807 1113 (CApp (t, (CRel i, loc)), loc))
adamc@807 1114 t xs
adamc@807 1115 in
adamc@807 1116 foldl (fn ((x, n, to), ctx) =>
adamc@807 1117 let
adamc@807 1118 val t = case to of
adamc@807 1119 NONE => t
adamc@807 1120 | SOME t' => (TFun (t', t), #2 d')
adamc@807 1121 val t = foldr (fn (x, t) => (TCFun (x, k, t), loc))
adamc@807 1122 t xs
adamc@807 1123 in
adamc@807 1124 bind (ctx, NamedE (x, n, t, NONE, ""))
adamc@807 1125 end)
adamc@807 1126 ctx xncs
adamc@807 1127 end)
adamc@807 1128 ctx dts
adamc@109 1129 | DVal (x, n, t, e, s) => bind (ctx, NamedE (x, n, t, SOME e, s))
adamc@125 1130 | DValRec vis =>
adamc@127 1131 foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s)))
adamc@125 1132 ctx vis
adamc@109 1133 | DExport _ => ctx
adamc@707 1134 | DTable (x, n, c, s, _, pc, _, cc) =>
adamc@247 1135 let
adamc@705 1136 val loc = #2 d'
adamc@705 1137 val ct = (CFfi ("Basis", "sql_table"), loc)
adamc@707 1138 val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc)
adamc@705 1139 val ct = (CApp (ct, cc), loc)
adamc@338 1140 in
adamc@705 1141 bind (ctx, NamedE (x, n, ct, NONE, s))
adamc@338 1142 end
adamc@338 1143 | DSequence (x, n, s) =>
adamc@338 1144 let
adamc@338 1145 val t = (CFfi ("Basis", "sql_sequence"), #2 d')
adamc@247 1146 in
adamc@247 1147 bind (ctx, NamedE (x, n, t, NONE, s))
adamc@247 1148 end
adamc@754 1149 | DView (x, n, s, _, c) =>
adamc@754 1150 let
adamc@754 1151 val loc = #2 d'
adamc@754 1152 val ct = (CFfi ("Basis", "sql_view"), loc)
adamc@754 1153 val ct = (CApp (ct, c), loc)
adamc@754 1154 in
adamc@754 1155 bind (ctx, NamedE (x, n, ct, NONE, s))
adamc@754 1156 end
adamc@271 1157 | DDatabase _ => ctx
adamc@461 1158 | DCookie (x, n, c, s) =>
adamc@461 1159 let
adamc@461 1160 val t = (CApp ((CFfi ("Basis", "http_cookie"), #2 d'), c), #2 d')
adamc@461 1161 in
adamc@461 1162 bind (ctx, NamedE (x, n, t, NONE, s))
adamc@461 1163 end
adamc@720 1164 | DStyle (x, n, s) =>
adamc@718 1165 let
adamc@720 1166 val t = (CFfi ("Basis", "css_class"), #2 d')
adamc@718 1167 in
adamc@718 1168 bind (ctx, NamedE (x, n, t, NONE, s))
adamc@718 1169 end
adamc@1075 1170 | DTask _ => ctx
adamc@1199 1171 | DPolicy _ => ctx
adam@1294 1172 | DOnError _ => ctx
adamc@20 1173 in
adamc@20 1174 S.map2 (mff ctx' ds',
adamc@20 1175 fn ds' =>
adamc@20 1176 d' :: ds')
adamc@20 1177 end)
adamc@20 1178 in
adamc@20 1179 mff
adamc@20 1180 end
adamc@20 1181
adamc@23 1182 fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} =
adamc@626 1183 mapfoldB {kind = fn () => fk,
adamc@23 1184 con = fn () => fc,
adamc@23 1185 exp = fn () => fe,
adamc@23 1186 decl = fn () => fd,
adamc@23 1187 bind = fn ((), _) => ()} ()
adamc@23 1188
adamc@20 1189 fun mapB {kind, con, exp, decl, bind} ctx ds =
adamc@626 1190 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@20 1191 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@20 1192 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
adamc@20 1193 decl = fn ctx => fn d => fn () => S.Continue (decl ctx d, ()),
adamc@20 1194 bind = bind} ctx ds () of
adamc@20 1195 S.Continue (ds, ()) => ds
adamc@20 1196 | S.Return _ => raise Fail "CoreUtil.File.mapB: Impossible"
adamc@20 1197
adamc@482 1198 fun map {kind, con, exp, decl} ds =
adamc@626 1199 mapB {kind = fn () => kind,
adamc@482 1200 con = fn () => con,
adamc@482 1201 exp = fn () => exp,
adamc@482 1202 decl = fn () => decl,
adamc@482 1203 bind = fn _ => ()} () ds
adamc@482 1204
adamc@23 1205 fun fold {kind, con, exp, decl} s d =
adamc@23 1206 case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
adamc@23 1207 con = fn c => fn s => S.Continue (c, con (c, s)),
adamc@23 1208 exp = fn e => fn s => S.Continue (e, exp (e, s)),
adamc@23 1209 decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
adamc@23 1210 S.Continue (_, s) => s
adamc@23 1211 | S.Return _ => raise Fail "CoreUtil.File.fold: Impossible"
adamc@23 1212
adamc@110 1213 fun foldMap {kind, con, exp, decl} s d =
adamc@110 1214 case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
adamc@110 1215 con = fn c => fn s => S.Continue (con (c, s)),
adamc@110 1216 exp = fn e => fn s => S.Continue (exp (e, s)),
adamc@110 1217 decl = fn d => fn s => S.Continue (decl (d, s))} d s of
adamc@110 1218 S.Continue v => v
adamc@110 1219 | S.Return _ => raise Fail "CoreUtil.File.foldMap: Impossible"
adamc@110 1220
adamc@179 1221 val maxName = foldl (fn ((d, _) : decl, count) =>
adamc@179 1222 case d of
adamc@179 1223 DCon (_, n, _, _) => Int.max (n, count)
adamc@807 1224 | DDatatype dts => foldl (fn ((_, n, _, ns), count) =>
adamc@807 1225 foldl (fn ((_, n', _), m) => Int.max (n', m))
adamc@807 1226 (Int.max (n, count)) ns) count dts
adamc@179 1227 | DVal (_, n, _, _, _) => Int.max (n, count)
adamc@179 1228 | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis
adamc@247 1229 | DExport _ => count
adamc@707 1230 | DTable (_, n, _, _, _, _, _, _) => Int.max (n, count)
adamc@338 1231 | DSequence (_, n, _) => Int.max (n, count)
adamc@754 1232 | DView (_, n, _, _, _) => Int.max (n, count)
adamc@461 1233 | DDatabase _ => count
adamc@718 1234 | DCookie (_, n, _, _) => Int.max (n, count)
adamc@1073 1235 | DStyle (_, n, _) => Int.max (n, count)
adamc@1199 1236 | DTask _ => count
adam@1294 1237 | DPolicy _ => count
adam@1294 1238 | DOnError _ => count) 0
adamc@179 1239
adamc@20 1240 end
adamc@20 1241
adamc@20 1242 end