Mercurial > urweb

annotate src/elab_util.sml @ 2257:28a541bd2d23

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