Mercurial > urweb

annotate src/elab_util.sml @ 1327:1cc67fdac4d3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New argument to transactional free functions, to specify whether we are about to retry
author Adam Chlipala <adam@chlipala.net>
date Sat, 04 Dec 2010 11:15:20 -0500
parents c7b9a33c26c8
children 9e0fa4f6ac93
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
adamc@623 78 | KUnif (_, _, ref (SOME k)) => mfk' ctx k
adamc@2 79 | KUnif _ => S.return2 kAll
adamc@623 80
adam@1302 81 | KTupleUnif (_, _, ref (SOME 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@1303 220 | CUnif (nl, _, _, _, ref (SOME 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
adamc@711 259 fun existsB {kind, con, bind} ctx c =
adamc@711 260 case mapfoldB {kind = fn ctx => fn k => fn () =>
adamc@711 261 if kind (ctx, k) then
adamc@711 262 S.Return ()
adamc@711 263 else
adamc@711 264 S.Continue (k, ()),
adamc@711 265 con = fn ctx => fn c => fn () =>
adamc@711 266 if con (ctx, c) then
adamc@711 267 S.Return ()
adamc@711 268 else
adamc@711 269 S.Continue (c, ()),
adamc@711 270 bind = bind} ctx c () of
adamc@711 271 S.Return _ => true
adamc@711 272 | S.Continue _ => false
adamc@711 273
adamc@711 274 fun exists {kind, con} c =
adamc@6 275 case mapfold {kind = fn k => fn () =>
adamc@6 276 if kind k then
adamc@6 277 S.Return ()
adamc@6 278 else
adamc@6 279 S.Continue (k, ()),
adamc@6 280 con = fn c => fn () =>
adamc@6 281 if con c then
adamc@6 282 S.Return ()
adamc@6 283 else
adamc@711 284 S.Continue (c, ())} c () of
adamc@2 285 S.Return _ => true
adamc@2 286 | S.Continue _ => false
adamc@2 287
adamc@448 288 fun foldB {kind, con, bind} ctx st c =
adamc@623 289 case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)),
adamc@448 290 con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
adamc@448 291 bind = bind} ctx c st of
adamc@448 292 S.Continue (_, st) => st
adamc@448 293 | S.Return _ => raise Fail "ElabUtil.Con.foldB: Impossible"
adamc@448 294
adamc@839 295 fun fold {kind, con} st c =
adamc@839 296 case mapfoldB {kind = fn () => fn k => fn st => S.Continue (k, kind (k, st)),
adamc@839 297 con = fn () => fn c => fn st => S.Continue (c, con (c, st)),
adamc@839 298 bind = fn ((), _) => ()} () c st of
adamc@839 299 S.Continue (_, st) => st
adamc@839 300 | S.Return _ => raise Fail "ElabUtil.Con.fold: Impossible"
adamc@839 301
adamc@2 302 end
adamc@2 303
adamc@10 304 structure Exp = struct
adamc@10 305
adamc@11 306 datatype binder =
adamc@623 307 RelK of string
adamc@623 308 | RelC of string * Elab.kind
adamc@792 309 | NamedC of string * int * Elab.kind * Elab.con option
adamc@11 310 | RelE of string * Elab.con
adamc@11 311 | NamedE of string * Elab.con
adamc@11 312
adamc@11 313 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
adamc@10 314 let
adamc@623 315 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@10 316
adamc@11 317 fun bind' (ctx, b) =
adamc@11 318 let
adamc@11 319 val b' = case b of
adamc@623 320 Con.RelK x => RelK x
adamc@623 321 | Con.RelC x => RelC x
adamc@623 322 | Con.NamedC x => NamedC x
adamc@11 323 in
adamc@11 324 bind (ctx, b')
adamc@11 325 end
adamc@11 326 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@10 327
adamc@825 328 fun doVars ((p, _), ctx) =
adamc@825 329 case p of
adamc@825 330 PWild => ctx
adamc@825 331 | PVar xt => bind (ctx, RelE xt)
adamc@825 332 | PPrim _ => ctx
adamc@825 333 | PCon (_, _, _, NONE) => ctx
adamc@825 334 | PCon (_, _, _, SOME p) => doVars (p, ctx)
adamc@825 335 | PRecord xpcs =>
adamc@825 336 foldl (fn ((_, p, _), ctx) => doVars (p, ctx))
adamc@825 337 ctx xpcs
adamc@825 338
adamc@11 339 fun mfe ctx e acc =
adamc@11 340 S.bindP (mfe' ctx e acc, fe ctx)
adamc@11 341
adamc@11 342 and mfe' ctx (eAll as (e, loc)) =
adamc@10 343 case e of
adamc@14 344 EPrim _ => S.return2 eAll
adamc@14 345 | ERel _ => S.return2 eAll
adamc@10 346 | ENamed _ => S.return2 eAll
adamc@34 347 | EModProj _ => S.return2 eAll
adamc@10 348 | EApp (e1, e2) =>
adamc@11 349 S.bind2 (mfe ctx e1,
adamc@10 350 fn e1' =>
adamc@11 351 S.map2 (mfe ctx e2,
adamc@10 352 fn e2' =>
adamc@10 353 (EApp (e1', e2'), loc)))
adamc@26 354 | EAbs (x, dom, ran, e) =>
adamc@26 355 S.bind2 (mfc ctx dom,
adamc@26 356 fn dom' =>
adamc@26 357 S.bind2 (mfc ctx ran,
adamc@26 358 fn ran' =>
adamc@26 359 S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
adamc@26 360 fn e' =>
adamc@26 361 (EAbs (x, dom', ran', e'), loc))))
adamc@26 362
adamc@10 363 | ECApp (e, c) =>
adamc@11 364 S.bind2 (mfe ctx e,
adamc@10 365 fn e' =>
adamc@11 366 S.map2 (mfc ctx c,
adamc@10 367 fn c' =>
adamc@10 368 (ECApp (e', c'), loc)))
adamc@10 369 | ECAbs (expl, x, k, e) =>
adamc@623 370 S.bind2 (mfk ctx k,
adamc@10 371 fn k' =>
adamc@11 372 S.map2 (mfe (bind (ctx, RelC (x, k))) e,
adamc@10 373 fn e' =>
adamc@10 374 (ECAbs (expl, x, k', e'), loc)))
adamc@10 375
adamc@12 376 | ERecord xes =>
adamc@29 377 S.map2 (ListUtil.mapfold (fn (x, e, t) =>
adamc@12 378 S.bind2 (mfc ctx x,
adamc@12 379 fn x' =>
adamc@29 380 S.bind2 (mfe ctx e,
adamc@12 381 fn e' =>
adamc@29 382 S.map2 (mfc ctx t,
adamc@29 383 fn t' =>
adamc@29 384 (x', e', t')))))
adamc@12 385 xes,
adamc@12 386 fn xes' =>
adamc@12 387 (ERecord xes', loc))
adamc@12 388 | EField (e, c, {field, rest}) =>
adamc@12 389 S.bind2 (mfe ctx e,
adamc@12 390 fn e' =>
adamc@12 391 S.bind2 (mfc ctx c,
adamc@12 392 fn c' =>
adamc@12 393 S.bind2 (mfc ctx field,
adamc@12 394 fn field' =>
adamc@12 395 S.map2 (mfc ctx rest,
adamc@12 396 fn rest' =>
adamc@12 397 (EField (e', c', {field = field', rest = rest'}), loc)))))
adamc@445 398 | EConcat (e1, c1, e2, c2) =>
adamc@339 399 S.bind2 (mfe ctx e1,
adamc@339 400 fn e1' =>
adamc@445 401 S.bind2 (mfc ctx c1,
adamc@445 402 fn c1' =>
adamc@339 403 S.bind2 (mfe ctx e2,
adamc@339 404 fn e2' =>
adamc@445 405 S.map2 (mfc ctx c2,
adamc@445 406 fn c2' =>
adamc@445 407 (EConcat (e1', c1', e2', c2'),
adamc@445 408 loc)))))
adamc@149 409 | ECut (e, c, {field, rest}) =>
adamc@149 410 S.bind2 (mfe ctx e,
adamc@149 411 fn e' =>
adamc@149 412 S.bind2 (mfc ctx c,
adamc@149 413 fn c' =>
adamc@149 414 S.bind2 (mfc ctx field,
adamc@149 415 fn field' =>
adamc@149 416 S.map2 (mfc ctx rest,
adamc@149 417 fn rest' =>
adamc@149 418 (ECut (e', c', {field = field', rest = rest'}), loc)))))
adamc@12 419
adamc@493 420 | ECutMulti (e, c, {rest}) =>
adamc@493 421 S.bind2 (mfe ctx e,
adamc@493 422 fn e' =>
adamc@493 423 S.bind2 (mfc ctx c,
adamc@493 424 fn c' =>
adamc@493 425 S.map2 (mfc ctx rest,
adamc@493 426 fn rest' =>
adamc@493 427 (ECutMulti (e', c', {rest = rest'}), loc))))
adamc@493 428
adamc@182 429 | ECase (e, pes, {disc, result}) =>
adamc@171 430 S.bind2 (mfe ctx e,
adamc@171 431 fn e' =>
adamc@171 432 S.bind2 (ListUtil.mapfold (fn (p, e) =>
adamc@448 433 let
adamc@448 434 fun pb ((p, _), ctx) =
adamc@448 435 case p of
adamc@448 436 PWild => ctx
adamc@448 437 | PVar (x, t) => bind (ctx, RelE (x, t))
adamc@448 438 | PPrim _ => ctx
adamc@448 439 | PCon (_, _, _, NONE) => ctx
adamc@448 440 | PCon (_, _, _, SOME p) => pb (p, ctx)
adamc@448 441 | PRecord xps => foldl (fn ((_, p, _), ctx) =>
adamc@448 442 pb (p, ctx)) ctx xps
adamc@448 443 in
adamc@1272 444 S.bind2 (mfp ctx p,
adamc@1272 445 fn p' =>
adamc@1272 446 S.map2 (mfe (pb (p', ctx)) e,
adamc@1272 447 fn e' => (p', e')))
adamc@448 448 end) pes,
adamc@171 449 fn pes' =>
adamc@182 450 S.bind2 (mfc ctx disc,
adamc@182 451 fn disc' =>
adamc@182 452 S.map2 (mfc ctx result,
adamc@182 453 fn result' =>
adamc@182 454 (ECase (e', pes', {disc = disc', result = result'}), loc)))))
adamc@171 455
adamc@10 456 | EError => S.return2 eAll
adamc@228 457 | EUnif (ref (SOME e)) => mfe ctx e
adamc@228 458 | EUnif _ => S.return2 eAll
adamc@447 459
adamc@825 460 | ELet (des, e, t) =>
adamc@447 461 let
adamc@826 462 val (des, ctx') = foldl (fn (ed, (des, ctx)) =>
adamc@826 463 let
adamc@826 464 val ctx' =
adamc@826 465 case #1 ed of
adamc@826 466 EDVal (p, _, _) => doVars (p, ctx)
adamc@826 467 | EDValRec vis =>
adamc@826 468 foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t)))
adamc@826 469 ctx vis
adamc@826 470 in
adamc@826 471 (S.bind2 (des,
adamc@826 472 fn des' =>
adamc@826 473 S.map2 (mfed ctx ed,
adamc@826 474 fn ed' => ed' :: des')),
adamc@826 475 ctx')
adamc@826 476 end)
adamc@447 477 (S.return2 [], ctx) des
adamc@447 478 in
adamc@447 479 S.bind2 (des,
adamc@447 480 fn des' =>
adamc@826 481 S.bind2 (mfe ctx' e,
adamc@447 482 fn e' =>
adamc@825 483 S.map2 (mfc ctx t,
adamc@825 484 fn t' =>
adamc@826 485 (ELet (rev des', e', t'), loc))))
adamc@447 486 end
adamc@447 487
adamc@623 488 | EKAbs (x, e) =>
adamc@623 489 S.map2 (mfe (bind (ctx, RelK x)) e,
adamc@623 490 fn e' =>
adamc@623 491 (EKAbs (x, e'), loc))
adamc@623 492 | EKApp (e, k) =>
adamc@623 493 S.bind2 (mfe ctx e,
adamc@623 494 fn e' =>
adamc@623 495 S.map2 (mfk ctx k,
adamc@623 496 fn k' =>
adamc@623 497 (EKApp (e', k'), loc)))
adamc@623 498
adamc@1272 499 and mfp ctx (pAll as (p, loc)) =
adamc@1272 500 case p of
adamc@1272 501 PWild => S.return2 pAll
adamc@1272 502 | PVar (x, t) =>
adamc@1272 503 S.map2 (mfc ctx t,
adamc@1272 504 fn t' =>
adamc@1272 505 (PVar (x, t'), loc))
adamc@1272 506 | PPrim _ => S.return2 pAll
adamc@1272 507 | PCon (dk, pc, args, po) =>
adamc@1272 508 S.bind2 (ListUtil.mapfold (mfc ctx) args,
adamc@1272 509 fn args' =>
adamc@1272 510 S.map2 ((case po of
adamc@1272 511 NONE => S.return2 NONE
adamc@1272 512 | SOME p => S.map2 (mfp ctx p, SOME)),
adamc@1272 513 fn po' =>
adamc@1272 514 (PCon (dk, pc, args', po'), loc)))
adamc@1272 515 | PRecord xps =>
adamc@1272 516 S.map2 (ListUtil.mapfold (fn (x, p, c) =>
adamc@1272 517 S.bind2 (mfp ctx p,
adamc@1272 518 fn p' =>
adamc@1272 519 S.map2 (mfc ctx c,
adamc@1272 520 fn c' =>
adamc@1272 521 (x, p', c')))) xps,
adamc@1272 522 fn xps' =>
adamc@1272 523 (PRecord xps', loc))
adamc@1272 524
adamc@447 525 and mfed ctx (dAll as (d, loc)) =
adamc@447 526 case d of
adamc@825 527 EDVal (p, t, e) =>
adamc@825 528 S.bind2 (mfc ctx t,
adamc@825 529 fn t' =>
adamc@826 530 S.map2 (mfe ctx e,
adamc@825 531 fn e' =>
adamc@825 532 (EDVal (p, t', e'), loc)))
adamc@447 533 | EDValRec vis =>
adamc@447 534 let
adamc@453 535 val ctx = foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis
adamc@447 536 in
adamc@447 537 S.map2 (ListUtil.mapfold (mfvi ctx) vis,
adamc@447 538 fn vis' =>
adamc@447 539 (EDValRec vis', loc))
adamc@447 540 end
adamc@447 541
adamc@447 542 and mfvi ctx (x, c, e) =
adamc@447 543 S.bind2 (mfc ctx c,
adamc@447 544 fn c' =>
adamc@447 545 S.map2 (mfe ctx e,
adamc@447 546 fn e' =>
adamc@447 547 (x, c', e')))
adamc@10 548 in
adamc@10 549 mfe
adamc@10 550 end
adamc@10 551
adamc@11 552 fun mapfold {kind = fk, con = fc, exp = fe} =
adamc@623 553 mapfoldB {kind = fn () => fk,
adamc@11 554 con = fn () => fc,
adamc@11 555 exp = fn () => fe,
adamc@11 556 bind = fn ((), _) => ()} ()
adamc@11 557
adamc@10 558 fun exists {kind, con, exp} k =
adamc@10 559 case mapfold {kind = fn k => fn () =>
adamc@10 560 if kind k then
adamc@10 561 S.Return ()
adamc@10 562 else
adamc@10 563 S.Continue (k, ()),
adamc@10 564 con = fn c => fn () =>
adamc@10 565 if con c then
adamc@10 566 S.Return ()
adamc@10 567 else
adamc@10 568 S.Continue (c, ()),
adamc@10 569 exp = fn e => fn () =>
adamc@10 570 if exp e then
adamc@10 571 S.Return ()
adamc@10 572 else
adamc@10 573 S.Continue (e, ())} k () of
adamc@10 574 S.Return _ => true
adamc@10 575 | S.Continue _ => false
adamc@10 576
adamc@211 577 fun mapB {kind, con, exp, bind} ctx e =
adamc@623 578 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@211 579 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@211 580 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
adamc@211 581 bind = bind} ctx e () of
adamc@211 582 S.Continue (e, ()) => e
adamc@211 583 | S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible"
adamc@211 584
adamc@448 585 fun foldB {kind, con, exp, bind} ctx st e =
adamc@623 586 case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)),
adamc@448 587 con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
adamc@448 588 exp = fn ctx => fn e => fn st => S.Continue (e, exp (ctx, e, st)),
adamc@448 589 bind = bind} ctx e st of
adamc@448 590 S.Continue (_, st) => st
adamc@448 591 | S.Return _ => raise Fail "ElabUtil.Exp.foldB: Impossible"
adamc@448 592
adamc@10 593 end
adamc@10 594
adamc@34 595 structure Sgn = struct
adamc@34 596
adamc@34 597 datatype binder =
adamc@623 598 RelK of string
adamc@623 599 | RelC of string * Elab.kind
adamc@792 600 | NamedC of string * int * Elab.kind * Elab.con option
adamc@792 601 | Str of string * int * Elab.sgn
adamc@792 602 | Sgn of string * int * Elab.sgn
adamc@34 603
adamc@34 604 fun mapfoldB {kind, con, sgn_item, sgn, bind} =
adamc@34 605 let
adamc@34 606 fun bind' (ctx, b) =
adamc@34 607 let
adamc@34 608 val b' = case b of
adamc@623 609 Con.RelK x => RelK x
adamc@623 610 | Con.RelC x => RelC x
adamc@623 611 | Con.NamedC x => NamedC x
adamc@34 612 in
adamc@34 613 bind (ctx, b')
adamc@34 614 end
adamc@34 615 val con = Con.mapfoldB {kind = kind, con = con, bind = bind'}
adamc@34 616
adamc@623 617 val kind = Kind.mapfoldB {kind = kind, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@34 618
adamc@34 619 fun sgi ctx si acc =
adamc@34 620 S.bindP (sgi' ctx si acc, sgn_item ctx)
adamc@34 621
adamc@156 622 and sgi' ctx (siAll as (si, loc)) =
adamc@34 623 case si of
adamc@34 624 SgiConAbs (x, n, k) =>
adamc@623 625 S.map2 (kind ctx k,
adamc@34 626 fn k' =>
adamc@34 627 (SgiConAbs (x, n, k'), loc))
adamc@34 628 | SgiCon (x, n, k, c) =>
adamc@623 629 S.bind2 (kind ctx k,
adamc@34 630 fn k' =>
adamc@34 631 S.map2 (con ctx c,
adamc@34 632 fn c' =>
adamc@34 633 (SgiCon (x, n, k', c'), loc)))
adamc@805 634 | SgiDatatype dts =>
adamc@805 635 S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
adamc@805 636 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@805 637 case c of
adamc@805 638 NONE => S.return2 (x, n, c)
adamc@805 639 | SOME c =>
adamc@805 640 S.map2 (con ctx c,
adamc@805 641 fn c' => (x, n, SOME c'))) xncs,
adamc@805 642 fn xncs' => (x, n, xs, xncs'))) dts,
adamc@805 643 fn dts' =>
adamc@805 644 (SgiDatatype dts', loc))
adamc@191 645 | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
adamc@162 646 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@162 647 case c of
adamc@162 648 NONE => S.return2 (x, n, c)
adamc@162 649 | SOME c =>
adamc@162 650 S.map2 (con ctx c,
adamc@162 651 fn c' => (x, n, SOME c'))) xncs,
adamc@162 652 fn xncs' =>
adamc@191 653 (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
adamc@34 654 | SgiVal (x, n, c) =>
adamc@34 655 S.map2 (con ctx c,
adamc@34 656 fn c' =>
adamc@34 657 (SgiVal (x, n, c'), loc))
adamc@34 658 | SgiStr (x, n, s) =>
adamc@34 659 S.map2 (sg ctx s,
adamc@34 660 fn s' =>
adamc@34 661 (SgiStr (x, n, s'), loc))
adamc@59 662 | SgiSgn (x, n, s) =>
adamc@59 663 S.map2 (sg ctx s,
adamc@59 664 fn s' =>
adamc@59 665 (SgiSgn (x, n, s'), loc))
adamc@88 666 | SgiConstraint (c1, c2) =>
adamc@88 667 S.bind2 (con ctx c1,
adamc@88 668 fn c1' =>
adamc@88 669 S.map2 (con ctx c2,
adamc@88 670 fn c2' =>
adamc@88 671 (SgiConstraint (c1', c2'), loc)))
adamc@563 672 | SgiClassAbs (x, n, k) =>
adamc@623 673 S.map2 (kind ctx k,
adamc@563 674 fn k' =>
adamc@563 675 (SgiClassAbs (x, n, k'), loc))
adamc@563 676 | SgiClass (x, n, k, c) =>
adamc@623 677 S.bind2 (kind ctx k,
adamc@563 678 fn k' =>
adamc@563 679 S.map2 (con ctx c,
adamc@563 680 fn c' =>
adamc@563 681 (SgiClass (x, n, k', c'), loc)))
adamc@34 682
adamc@34 683 and sg ctx s acc =
adamc@34 684 S.bindP (sg' ctx s acc, sgn ctx)
adamc@34 685
adamc@34 686 and sg' ctx (sAll as (s, loc)) =
adamc@34 687 case s of
adamc@34 688 SgnConst sgis =>
adamc@34 689 S.map2 (ListUtil.mapfoldB (fn (ctx, si) =>
adamc@34 690 (case #1 si of
adamc@329 691 SgiConAbs (x, n, k) =>
adamc@792 692 bind (ctx, NamedC (x, n, k, NONE))
adamc@792 693 | SgiCon (x, n, k, c) =>
adamc@792 694 bind (ctx, NamedC (x, n, k, SOME c))
adamc@805 695 | SgiDatatype dts =>
adamc@805 696 foldl (fn ((x, n, ks, _), ctx) =>
adamc@805 697 let
adamc@805 698 val k' = (KType, loc)
adamc@805 699 val k = foldl (fn (_, k) => (KArrow (k', k), loc))
adamc@805 700 k' ks
adamc@805 701 in
adamc@805 702 bind (ctx, NamedC (x, n, k, NONE))
adamc@805 703 end) ctx dts
adamc@792 704 | SgiDatatypeImp (x, n, m1, ms, s, _, _) =>
adamc@792 705 bind (ctx, NamedC (x, n, (KType, loc),
adamc@792 706 SOME (CModProj (m1, ms, s), loc)))
adamc@34 707 | SgiVal _ => ctx
adamc@792 708 | SgiStr (x, n, sgn) =>
adamc@792 709 bind (ctx, Str (x, n, sgn))
adamc@792 710 | SgiSgn (x, n, sgn) =>
adamc@792 711 bind (ctx, Sgn (x, n, sgn))
adamc@203 712 | SgiConstraint _ => ctx
adamc@563 713 | SgiClassAbs (x, n, k) =>
adamc@792 714 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), NONE))
adamc@792 715 | SgiClass (x, n, k, c) =>
adamc@792 716 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), SOME c)),
adamc@34 717 sgi ctx si)) ctx sgis,
adamc@34 718 fn sgis' =>
adamc@34 719 (SgnConst sgis', loc))
adamc@34 720
adamc@34 721 | SgnVar _ => S.return2 sAll
adamc@41 722 | SgnFun (m, n, s1, s2) =>
adamc@41 723 S.bind2 (sg ctx s1,
adamc@41 724 fn s1' =>
adamc@792 725 S.map2 (sg (bind (ctx, Str (m, n, s1'))) s2,
adamc@41 726 fn s2' =>
adamc@41 727 (SgnFun (m, n, s1', s2'), loc)))
adamc@59 728 | SgnProj _ => S.return2 sAll
adamc@42 729 | SgnWhere (sgn, x, c) =>
adamc@42 730 S.bind2 (sg ctx sgn,
adamc@42 731 fn sgn' =>
adamc@42 732 S.map2 (con ctx c,
adamc@42 733 fn c' =>
adamc@42 734 (SgnWhere (sgn', x, c'), loc)))
adamc@34 735 | SgnError => S.return2 sAll
adamc@34 736 in
adamc@34 737 sg
adamc@34 738 end
adamc@34 739
adamc@34 740 fun mapfold {kind, con, sgn_item, sgn} =
adamc@623 741 mapfoldB {kind = fn () => kind,
adamc@34 742 con = fn () => con,
adamc@34 743 sgn_item = fn () => sgn_item,
adamc@34 744 sgn = fn () => sgn,
adamc@34 745 bind = fn ((), _) => ()} ()
adamc@34 746
adamc@792 747 fun mapB {kind, con, sgn_item, sgn, bind} ctx s =
adamc@792 748 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@792 749 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@792 750 sgn_item = fn ctx => fn sgi => fn () => S.Continue (sgn_item ctx sgi, ()),
adamc@792 751 sgn = fn ctx => fn s => fn () => S.Continue (sgn ctx s, ()),
adamc@792 752 bind = bind} ctx s () of
adamc@792 753 S.Continue (s, ()) => s
adamc@792 754 | S.Return _ => raise Fail "ElabUtil.Sgn.mapB: Impossible"
adamc@792 755
adamc@34 756 fun map {kind, con, sgn_item, sgn} s =
adamc@34 757 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@34 758 con = fn c => fn () => S.Continue (con c, ()),
adamc@34 759 sgn_item = fn si => fn () => S.Continue (sgn_item si, ()),
adamc@34 760 sgn = fn s => fn () => S.Continue (sgn s, ())} s () of
adamc@34 761 S.Return () => raise Fail "Elab_util.Sgn.map"
adamc@34 762 | S.Continue (s, ()) => s
adamc@34 763
adamc@2 764 end
adamc@34 765
adamc@76 766 structure Decl = struct
adamc@76 767
adamc@76 768 datatype binder =
adamc@623 769 RelK of string
adamc@623 770 | RelC of string * Elab.kind
adamc@792 771 | NamedC of string * int * Elab.kind * Elab.con option
adamc@76 772 | RelE of string * Elab.con
adamc@76 773 | NamedE of string * Elab.con
adamc@76 774 | Str of string * Elab.sgn
adamc@76 775 | Sgn of string * Elab.sgn
adamc@76 776
adamc@76 777 fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} =
adamc@76 778 let
adamc@623 779 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@76 780
adamc@76 781 fun bind' (ctx, b) =
adamc@76 782 let
adamc@76 783 val b' = case b of
adamc@623 784 Con.RelK x => RelK x
adamc@623 785 | Con.RelC x => RelC x
adamc@623 786 | Con.NamedC x => NamedC x
adamc@76 787 in
adamc@76 788 bind (ctx, b')
adamc@76 789 end
adamc@76 790 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@76 791
adamc@76 792 fun bind' (ctx, b) =
adamc@76 793 let
adamc@76 794 val b' = case b of
adamc@623 795 Exp.RelK x => RelK x
adamc@623 796 | Exp.RelC x => RelC x
adamc@76 797 | Exp.NamedC x => NamedC x
adamc@76 798 | Exp.RelE x => RelE x
adamc@76 799 | Exp.NamedE x => NamedE x
adamc@76 800 in
adamc@76 801 bind (ctx, b')
adamc@76 802 end
adamc@76 803 val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind'}
adamc@76 804
adamc@76 805 fun bind' (ctx, b) =
adamc@76 806 let
adamc@76 807 val b' = case b of
adamc@623 808 Sgn.RelK x => RelK x
adamc@623 809 | Sgn.RelC x => RelC x
adamc@76 810 | Sgn.NamedC x => NamedC x
adamc@792 811 | Sgn.Sgn (x, _, y) => Sgn (x, y)
adamc@792 812 | Sgn.Str (x, _, y) => Str (x, y)
adamc@76 813 in
adamc@76 814 bind (ctx, b')
adamc@76 815 end
adamc@76 816 val mfsg = Sgn.mapfoldB {kind = fk, con = fc, sgn_item = fsgi, sgn = fsg, bind = bind'}
adamc@76 817
adamc@76 818 fun mfst ctx str acc =
adamc@76 819 S.bindP (mfst' ctx str acc, fst ctx)
adamc@76 820
adamc@76 821 and mfst' ctx (strAll as (str, loc)) =
adamc@76 822 case str of
adamc@76 823 StrConst ds =>
adamc@76 824 S.map2 (ListUtil.mapfoldB (fn (ctx, d) =>
adamc@76 825 (case #1 d of
adamc@792 826 DCon (x, n, k, c) =>
adamc@792 827 bind (ctx, NamedC (x, n, k, SOME c))
adamc@805 828 | DDatatype dts =>
adamc@156 829 let
adamc@805 830 fun doOne ((x, n, xs, xncs), ctx) =
adamc@805 831 let
adamc@805 832 val ctx = bind (ctx, NamedC (x, n, (KType, loc), NONE))
adamc@805 833 in
adamc@805 834 foldl (fn ((x, _, co), ctx) =>
adamc@805 835 let
adamc@805 836 val t =
adamc@805 837 case co of
adamc@805 838 NONE => CNamed n
adamc@805 839 | SOME t => TFun (t, (CNamed n, loc))
adamc@805 840
adamc@805 841 val k = (KType, loc)
adamc@805 842 val t = (t, loc)
adamc@805 843 val t = foldr (fn (x, t) =>
adamc@805 844 (TCFun (Explicit,
adamc@805 845 x,
adamc@805 846 k,
adamc@805 847 t), loc))
adamc@805 848 t xs
adamc@805 849 in
adamc@805 850 bind (ctx, NamedE (x, t))
adamc@805 851 end)
adamc@805 852 ctx xncs
adamc@805 853 end
adamc@156 854 in
adamc@805 855 foldl doOne ctx dts
adamc@156 856 end
adamc@191 857 | DDatatypeImp (x, n, m, ms, x', _, _) =>
adamc@792 858 bind (ctx, NamedC (x, n, (KType, loc),
adamc@792 859 SOME (CModProj (m, ms, x'), loc)))
adamc@76 860 | DVal (x, _, c, _) =>
adamc@76 861 bind (ctx, NamedE (x, c))
adamc@123 862 | DValRec vis =>
adamc@123 863 foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis
adamc@76 864 | DSgn (x, _, sgn) =>
adamc@76 865 bind (ctx, Sgn (x, sgn))
adamc@76 866 | DStr (x, _, sgn, _) =>
adamc@76 867 bind (ctx, Str (x, sgn))
adamc@76 868 | DFfiStr (x, _, sgn) =>
adamc@88 869 bind (ctx, Str (x, sgn))
adamc@100 870 | DConstraint _ => ctx
adamc@203 871 | DExport _ => ctx
adamc@707 872 | DTable (tn, x, n, c, _, pc, _, cc) =>
adamc@705 873 let
adamc@705 874 val ct = (CModProj (n, [], "sql_table"), loc)
adamc@705 875 val ct = (CApp (ct, c), loc)
adamc@707 876 val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc)
adamc@705 877 in
adamc@705 878 bind (ctx, NamedE (x, ct))
adamc@705 879 end
adamc@338 880 | DSequence (tn, x, n) =>
adamc@338 881 bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc)))
adamc@754 882 | DView (tn, x, n, _, c) =>
adamc@754 883 let
adamc@754 884 val ct = (CModProj (n, [], "sql_view"), loc)
adamc@754 885 val ct = (CApp (ct, c), loc)
adamc@754 886 in
adamc@754 887 bind (ctx, NamedE (x, ct))
adamc@754 888 end
adamc@792 889 | DClass (x, n, k, c) =>
adamc@792 890 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), SOME c))
adamc@459 891 | DDatabase _ => ctx
adamc@459 892 | DCookie (tn, x, n, c) =>
adamc@459 893 bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc),
adamc@718 894 c), loc)))
adamc@720 895 | DStyle (tn, x, n) =>
adamc@1073 896 bind (ctx, NamedE (x, (CModProj (n, [], "css_class"), loc)))
adamc@1199 897 | DTask _ => ctx
adam@1294 898 | DPolicy _ => ctx
adam@1294 899 | DOnError _ => ctx,
adamc@76 900 mfd ctx d)) ctx ds,
adamc@76 901 fn ds' => (StrConst ds', loc))
adamc@76 902 | StrVar _ => S.return2 strAll
adamc@76 903 | StrProj (str, x) =>
adamc@76 904 S.map2 (mfst ctx str,
adamc@76 905 fn str' =>
adamc@76 906 (StrProj (str', x), loc))
adamc@76 907 | StrFun (x, n, sgn1, sgn2, str) =>
adamc@76 908 S.bind2 (mfsg ctx sgn1,
adamc@76 909 fn sgn1' =>
adamc@76 910 S.bind2 (mfsg ctx sgn2,
adamc@76 911 fn sgn2' =>
adamc@76 912 S.map2 (mfst ctx str,
adamc@76 913 fn str' =>
adamc@76 914 (StrFun (x, n, sgn1', sgn2', str'), loc))))
adamc@76 915 | StrApp (str1, str2) =>
adamc@76 916 S.bind2 (mfst ctx str1,
adamc@76 917 fn str1' =>
adamc@76 918 S.map2 (mfst ctx str2,
adamc@76 919 fn str2' =>
adamc@76 920 (StrApp (str1', str2'), loc)))
adamc@76 921 | StrError => S.return2 strAll
adamc@76 922
adamc@76 923 and mfd ctx d acc =
adamc@76 924 S.bindP (mfd' ctx d acc, fd ctx)
adamc@76 925
adamc@76 926 and mfd' ctx (dAll as (d, loc)) =
adamc@76 927 case d of
adamc@76 928 DCon (x, n, k, c) =>
adamc@623 929 S.bind2 (mfk ctx k,
adamc@76 930 fn k' =>
adamc@76 931 S.map2 (mfc ctx c,
adamc@76 932 fn c' =>
adamc@76 933 (DCon (x, n, k', c'), loc)))
adamc@805 934 | DDatatype dts =>
adamc@805 935 S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
adamc@805 936 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@805 937 case c of
adamc@805 938 NONE => S.return2 (x, n, c)
adamc@805 939 | SOME c =>
adamc@805 940 S.map2 (mfc ctx c,
adamc@805 941 fn c' => (x, n, SOME c'))) xncs,
adamc@805 942 fn xncs' =>
adamc@805 943 (x, n, xs, xncs'))) dts,
adamc@805 944 fn dts' =>
adamc@805 945 (DDatatype dts', loc))
adamc@191 946 | DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
adamc@162 947 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@162 948 case c of
adamc@162 949 NONE => S.return2 (x, n, c)
adamc@162 950 | SOME c =>
adamc@162 951 S.map2 (mfc ctx c,
adamc@162 952 fn c' => (x, n, SOME c'))) xncs,
adamc@162 953 fn xncs' =>
adamc@191 954 (DDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
adamc@123 955 | DVal vi =>
adamc@123 956 S.map2 (mfvi ctx vi,
adamc@123 957 fn vi' =>
adamc@123 958 (DVal vi', loc))
adamc@123 959 | DValRec vis =>
adamc@123 960 S.map2 (ListUtil.mapfold (mfvi ctx) vis,
adamc@123 961 fn vis' =>
adamc@123 962 (DValRec vis', loc))
adamc@76 963 | DSgn (x, n, sgn) =>
adamc@76 964 S.map2 (mfsg ctx sgn,
adamc@76 965 fn sgn' =>
adamc@76 966 (DSgn (x, n, sgn'), loc))
adamc@76 967 | DStr (x, n, sgn, str) =>
adamc@76 968 S.bind2 (mfsg ctx sgn,
adamc@76 969 fn sgn' =>
adamc@76 970 S.map2 (mfst ctx str,
adamc@76 971 fn str' =>
adamc@76 972 (DStr (x, n, sgn', str'), loc)))
adamc@76 973 | DFfiStr (x, n, sgn) =>
adamc@76 974 S.map2 (mfsg ctx sgn,
adamc@76 975 fn sgn' =>
adamc@76 976 (DFfiStr (x, n, sgn'), loc))
adamc@88 977 | DConstraint (c1, c2) =>
adamc@88 978 S.bind2 (mfc ctx c1,
adamc@88 979 fn c1' =>
adamc@88 980 S.map2 (mfc ctx c2,
adamc@88 981 fn c2' =>
adamc@88 982 (DConstraint (c1', c2'), loc)))
adamc@109 983 | DExport (en, sgn, str) =>
adamc@109 984 S.bind2 (mfsg ctx sgn,
adamc@109 985 fn sgn' =>
adamc@109 986 S.map2 (mfst ctx str,
adamc@109 987 fn str' =>
adamc@109 988 (DExport (en, sgn', str'), loc)))
adamc@123 989
adamc@707 990 | DTable (tn, x, n, c, pe, pc, ce, cc) =>
adamc@704 991 S.bind2 (mfc ctx c,
adamc@203 992 fn c' =>
adamc@707 993 S.bind2 (mfe ctx pe,
adamc@707 994 fn pe' =>
adamc@707 995 S.bind2 (mfc ctx pc,
adamc@707 996 fn pc' =>
adamc@707 997 S.bind2 (mfe ctx ce,
adamc@707 998 fn ce' =>
adamc@707 999 S.map2 (mfc ctx cc,
adamc@707 1000 fn cc' =>
adamc@707 1001 (DTable (tn, x, n, c', pe', pc', ce', cc'), loc))))))
adamc@338 1002 | DSequence _ => S.return2 dAll
adamc@754 1003 | DView (tn, x, n, e, c) =>
adamc@754 1004 S.bind2 (mfe ctx e,
adamc@754 1005 fn e' =>
adamc@754 1006 S.map2 (mfc ctx c,
adamc@754 1007 fn c' =>
adamc@754 1008 (DView (tn, x, n, e', c'), loc)))
adamc@203 1009
adamc@563 1010 | DClass (x, n, k, c) =>
adamc@623 1011 S.bind2 (mfk ctx k,
adamc@563 1012 fn k' =>
adamc@563 1013 S.map2 (mfc ctx c,
adamc@563 1014 fn c' =>
adamc@563 1015 (DClass (x, n, k', c'), loc)))
adamc@213 1016
adamc@338 1017 | DDatabase _ => S.return2 dAll
adamc@271 1018
adamc@459 1019 | DCookie (tn, x, n, c) =>
adamc@459 1020 S.map2 (mfc ctx c,
adamc@459 1021 fn c' =>
adamc@459 1022 (DCookie (tn, x, n, c'), loc))
adamc@720 1023 | DStyle _ => S.return2 dAll
adamc@1075 1024 | DTask (e1, e2) =>
adamc@1075 1025 S.bind2 (mfe ctx e1,
adamc@1075 1026 fn e1' =>
adamc@1075 1027 S.map2 (mfe ctx e2,
adamc@1075 1028 fn e2' =>
adamc@1075 1029 (DTask (e1', e2'), loc)))
adamc@1199 1030 | DPolicy e1 =>
adamc@1199 1031 S.map2 (mfe ctx e1,
adamc@1199 1032 fn e1' =>
adamc@1199 1033 (DPolicy e1', loc))
adam@1294 1034 | DOnError _ => S.return2 dAll
adamc@459 1035
adamc@123 1036 and mfvi ctx (x, n, c, e) =
adamc@123 1037 S.bind2 (mfc ctx c,
adamc@123 1038 fn c' =>
adamc@123 1039 S.map2 (mfe ctx e,
adamc@123 1040 fn e' =>
adamc@123 1041 (x, n, c', e')))
adamc@76 1042 in
adamc@76 1043 mfd
adamc@76 1044 end
adamc@76 1045
adamc@76 1046 fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} =
adamc@623 1047 mapfoldB {kind = fn () => kind,
adamc@76 1048 con = fn () => con,
adamc@76 1049 exp = fn () => exp,
adamc@76 1050 sgn_item = fn () => sgn_item,
adamc@76 1051 sgn = fn () => sgn,
adamc@76 1052 str = fn () => str,
adamc@76 1053 decl = fn () => decl,
adamc@76 1054 bind = fn ((), _) => ()} ()
adamc@76 1055
adamc@76 1056 fun exists {kind, con, exp, sgn_item, sgn, str, decl} k =
adamc@76 1057 case mapfold {kind = fn k => fn () =>
adamc@76 1058 if kind k then
adamc@76 1059 S.Return ()
adamc@76 1060 else
adamc@76 1061 S.Continue (k, ()),
adamc@76 1062 con = fn c => fn () =>
adamc@76 1063 if con c then
adamc@76 1064 S.Return ()
adamc@76 1065 else
adamc@76 1066 S.Continue (c, ()),
adamc@76 1067 exp = fn e => fn () =>
adamc@76 1068 if exp e then
adamc@76 1069 S.Return ()
adamc@76 1070 else
adamc@76 1071 S.Continue (e, ()),
adamc@76 1072 sgn_item = fn sgi => fn () =>
adamc@76 1073 if sgn_item sgi then
adamc@76 1074 S.Return ()
adamc@76 1075 else
adamc@76 1076 S.Continue (sgi, ()),
adamc@76 1077 sgn = fn x => fn () =>
adamc@76 1078 if sgn x then
adamc@76 1079 S.Return ()
adamc@76 1080 else
adamc@76 1081 S.Continue (x, ()),
adamc@76 1082 str = fn x => fn () =>
adamc@76 1083 if str x then
adamc@76 1084 S.Return ()
adamc@76 1085 else
adamc@76 1086 S.Continue (x, ()),
adamc@76 1087 decl = fn x => fn () =>
adamc@76 1088 if decl x then
adamc@76 1089 S.Return ()
adamc@76 1090 else
adamc@76 1091 S.Continue (x, ())} k () of
adamc@76 1092 S.Return _ => true
adamc@76 1093 | S.Continue _ => false
adamc@76 1094
adamc@76 1095 fun search {kind, con, exp, sgn_item, sgn, str, decl} k =
adamc@76 1096 case mapfold {kind = fn x => fn () =>
adamc@76 1097 case kind x of
adamc@76 1098 NONE => S.Continue (x, ())
adamc@76 1099 | SOME v => S.Return v,
adamc@76 1100
adamc@76 1101 con = fn x => fn () =>
adamc@76 1102 case con x of
adamc@76 1103 NONE => S.Continue (x, ())
adamc@76 1104 | SOME v => S.Return v,
adamc@76 1105
adamc@76 1106 exp = fn x => fn () =>
adamc@76 1107 case exp x of
adamc@76 1108 NONE => S.Continue (x, ())
adamc@76 1109 | SOME v => S.Return v,
adamc@76 1110
adamc@76 1111 sgn_item = fn x => fn () =>
adamc@76 1112 case sgn_item x of
adamc@76 1113 NONE => S.Continue (x, ())
adamc@76 1114 | SOME v => S.Return v,
adamc@76 1115
adamc@76 1116 sgn = fn x => fn () =>
adamc@76 1117 case sgn x of
adamc@76 1118 NONE => S.Continue (x, ())
adamc@76 1119 | SOME v => S.Return v,
adamc@76 1120
adamc@76 1121 str = fn x => fn () =>
adamc@76 1122 case str x of
adamc@76 1123 NONE => S.Continue (x, ())
adamc@76 1124 | SOME v => S.Return v,
adamc@76 1125
adamc@76 1126 decl = fn x => fn () =>
adamc@76 1127 case decl x of
adamc@76 1128 NONE => S.Continue (x, ())
adamc@76 1129 | SOME v => S.Return v
adamc@76 1130
adamc@76 1131 } k () of
adamc@76 1132 S.Return x => SOME x
adamc@76 1133 | S.Continue _ => NONE
adamc@76 1134
adamc@448 1135 fun foldMapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx st d =
adamc@623 1136 case mapfoldB {kind = fn ctx => fn x => fn st => S.Continue (kind (ctx, x, st)),
adamc@448 1137 con = fn ctx => fn x => fn st => S.Continue (con (ctx, x, st)),
adamc@448 1138 exp = fn ctx => fn x => fn st => S.Continue (exp (ctx, x, st)),
adamc@448 1139 sgn_item = fn ctx => fn x => fn st => S.Continue (sgn_item (ctx, x, st)),
adamc@448 1140 sgn = fn ctx => fn x => fn st => S.Continue (sgn (ctx, x, st)),
adamc@448 1141 str = fn ctx => fn x => fn st => S.Continue (str (ctx, x, st)),
adamc@448 1142 decl = fn ctx => fn x => fn st => S.Continue (decl (ctx, x, st)),
adamc@448 1143 bind = bind} ctx d st of
adamc@448 1144 S.Continue x => x
adamc@448 1145 | S.Return _ => raise Fail "ElabUtil.Decl.foldMapB: Impossible"
adamc@448 1146
adamc@448 1147 end
adamc@448 1148
adamc@448 1149 structure File = struct
adamc@448 1150
adamc@448 1151 fun maxName ds = foldl (fn (d, count) => Int.max (maxNameDecl d, count)) 0 ds
adamc@448 1152
adamc@448 1153 and maxNameDecl (d, _) =
adamc@448 1154 case d of
adamc@448 1155 DCon (_, n, _, _) => n
adamc@805 1156 | DDatatype dts =>
adamc@805 1157 foldl (fn ((_, n, _, ns), max) =>
adamc@448 1158 foldl (fn ((_, n', _), m) => Int.max (n', m))
adamc@805 1159 (Int.max (n, max)) ns) 0 dts
adamc@448 1160 | DDatatypeImp (_, n1, n2, _, _, _, ns) =>
adamc@448 1161 foldl (fn ((_, n', _), m) => Int.max (n', m))
adamc@448 1162 (Int.max (n1, n2)) ns
adamc@448 1163 | DVal (_, n, _, _) => n
adamc@448 1164 | DValRec vis => foldl (fn ((_, n, _, _), count) => Int.max (n, count)) 0 vis
adamc@448 1165 | DStr (_, n, sgn, str) => Int.max (n, Int.max (maxNameSgn sgn, maxNameStr str))
adamc@448 1166 | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
adamc@448 1167 | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
adamc@448 1168 | DConstraint _ => 0
adamc@563 1169 | DClass (_, n, _, _) => n
adamc@448 1170 | DExport _ => 0
adamc@707 1171 | DTable (n1, _, n2, _, _, _, _, _) => Int.max (n1, n2)
adamc@459 1172 | DSequence (n1, _, n2) => Int.max (n1, n2)
adamc@754 1173 | DView (n1, _, n2, _, _) => Int.max (n1, n2)
adamc@448 1174 | DDatabase _ => 0
adamc@459 1175 | DCookie (n1, _, n2, _) => Int.max (n1, n2)
adamc@720 1176 | DStyle (n1, _, n2) => Int.max (n1, n2)
adamc@1075 1177 | DTask _ => 0
adamc@1199 1178 | DPolicy _ => 0
adam@1294 1179 | DOnError _ => 0
adamc@448 1180 and maxNameStr (str, _) =
adamc@448 1181 case str of
adamc@448 1182 StrConst ds => maxName ds
adamc@448 1183 | StrVar n => n
adamc@448 1184 | StrProj (str, _) => maxNameStr str
adamc@448 1185 | StrFun (_, n, dom, ran, str) => foldl Int.max n [maxNameSgn dom, maxNameSgn ran, maxNameStr str]
adamc@448 1186 | StrApp (str1, str2) => Int.max (maxNameStr str1, maxNameStr str2)
adamc@448 1187 | StrError => 0
adamc@448 1188
adamc@448 1189 and maxNameSgn (sgn, _) =
adamc@448 1190 case sgn of
adamc@448 1191 SgnConst sgis => foldl (fn (sgi, count) => Int.max (maxNameSgi sgi, count)) 0 sgis
adamc@448 1192 | SgnVar n => n
adamc@448 1193 | SgnFun (_, n, dom, ran) => Int.max (n, Int.max (maxNameSgn dom, maxNameSgn ran))
adamc@448 1194 | SgnWhere (sgn, _, _) => maxNameSgn sgn
adamc@448 1195 | SgnProj (n, _, _) => n
adamc@448 1196 | SgnError => 0
adamc@448 1197
adamc@448 1198 and maxNameSgi (sgi, _) =
adamc@448 1199 case sgi of
adamc@448 1200 SgiConAbs (_, n, _) => n
adamc@448 1201 | SgiCon (_, n, _, _) => n
adamc@805 1202 | SgiDatatype dts =>
adamc@805 1203 foldl (fn ((_, n, _, ns), max) =>
adamc@805 1204 foldl (fn ((_, n', _), m) => Int.max (n', m))
adamc@805 1205 (Int.max (n, max)) ns) 0 dts
adamc@448 1206 | SgiDatatypeImp (_, n1, n2, _, _, _, ns) =>
adamc@448 1207 foldl (fn ((_, n', _), m) => Int.max (n', m))
adamc@448 1208 (Int.max (n1, n2)) ns
adamc@448 1209 | SgiVal (_, n, _) => n
adamc@448 1210 | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
adamc@448 1211 | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
adamc@448 1212 | SgiConstraint _ => 0
adamc@563 1213 | SgiClassAbs (_, n, _) => n
adamc@563 1214 | SgiClass (_, n, _, _) => n
adamc@448 1215
adamc@34 1216 end
adamc@76 1217
adamc@76 1218 end