Mercurial > urweb

annotate src/elab_util.sml @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hooks for measuring how much interesting proving is going on in elaboration
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Nov 2009 12:44:14 -0500
parents b2413e4dd109
children b2311dfb3158
rev   line source
adamc@2 1 (* Copyright (c) 2008, 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
adamc@623 81 | KRel _ => S.return2 kAll
adamc@623 82 | KFun (x, k) =>
adamc@623 83 S.map2 (mfk (bind (ctx, x)) k,
adamc@623 84 fn k' =>
adamc@623 85 (KFun (x, k'), loc))
adamc@2 86 in
adamc@2 87 mfk
adamc@2 88 end
adamc@2 89
adamc@623 90 fun mapfold fk =
adamc@623 91 mapfoldB {kind = fn () => fk,
adamc@623 92 bind = fn ((), _) => ()} ()
adamc@623 93
adamc@623 94 fun mapB {kind, bind} ctx k =
adamc@623 95 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@623 96 bind = bind} ctx k () of
adamc@623 97 S.Continue (k, ()) => k
adamc@623 98 | S.Return _ => raise Fail "ElabUtil.Kind.mapB: Impossible"
adamc@623 99
adamc@2 100 fun exists f k =
adamc@6 101 case mapfold (fn k => fn () =>
adamc@6 102 if f k then
adamc@6 103 S.Return ()
adamc@6 104 else
adamc@6 105 S.Continue (k, ())) k () of
adamc@6 106 S.Return _ => true
adamc@6 107 | S.Continue _ => false
adamc@6 108
adamc@6 109 end
adamc@6 110
adamc@6 111 structure Con = struct
adamc@6 112
adamc@11 113 datatype binder =
adamc@623 114 RelK of string
adamc@623 115 | RelC of string * Elab.kind
adamc@792 116 | NamedC of string * int * Elab.kind * Elab.con option
adamc@11 117
adamc@11 118 fun mapfoldB {kind = fk, con = fc, bind} =
adamc@6 119 let
adamc@623 120 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, s) => bind (ctx, RelK s)}
adamc@6 121
adamc@11 122 fun mfc ctx c acc =
adamc@11 123 S.bindP (mfc' ctx c acc, fc ctx)
adamc@6 124
adamc@11 125 and mfc' ctx (cAll as (c, loc)) =
adamc@6 126 case c of
adamc@6 127 TFun (c1, c2) =>
adamc@11 128 S.bind2 (mfc ctx c1,
adamc@6 129 fn c1' =>
adamc@11 130 S.map2 (mfc ctx c2,
adamc@6 131 fn c2' =>
adamc@6 132 (TFun (c1', c2'), loc)))
adamc@6 133 | TCFun (e, x, k, c) =>
adamc@623 134 S.bind2 (mfk ctx k,
adamc@6 135 fn k' =>
adamc@623 136 S.map2 (mfc (bind (ctx, RelC (x, k))) c,
adamc@6 137 fn c' =>
adamc@6 138 (TCFun (e, x, k', c'), loc)))
adamc@628 139 | TDisjoint (c1, c2, c3) =>
adamc@85 140 S.bind2 (mfc ctx c1,
adamc@85 141 fn c1' =>
adamc@85 142 S.bind2 (mfc ctx c2,
adamc@85 143 fn c2' =>
adamc@85 144 S.map2 (mfc ctx c3,
adamc@85 145 fn c3' =>
adamc@628 146 (TDisjoint (c1', c2', c3'), loc))))
adamc@6 147 | TRecord c =>
adamc@11 148 S.map2 (mfc ctx c,
adamc@6 149 fn c' =>
adamc@6 150 (TRecord c', loc))
adamc@6 151
adamc@6 152 | CRel _ => S.return2 cAll
adamc@6 153 | CNamed _ => S.return2 cAll
adamc@34 154 | CModProj _ => S.return2 cAll
adamc@6 155 | CApp (c1, c2) =>
adamc@11 156 S.bind2 (mfc ctx c1,
adamc@6 157 fn c1' =>
adamc@11 158 S.map2 (mfc ctx c2,
adamc@6 159 fn c2' =>
adamc@6 160 (CApp (c1', c2'), loc)))
adamc@8 161 | CAbs (x, k, c) =>
adamc@623 162 S.bind2 (mfk ctx k,
adamc@6 163 fn k' =>
adamc@623 164 S.map2 (mfc (bind (ctx, RelC (x, k))) c,
adamc@6 165 fn c' =>
adamc@8 166 (CAbs (x, k', c'), loc)))
adamc@6 167
adamc@6 168 | CName _ => S.return2 cAll
adamc@6 169
adamc@6 170 | CRecord (k, xcs) =>
adamc@623 171 S.bind2 (mfk ctx k,
adamc@6 172 fn k' =>
adamc@6 173 S.map2 (ListUtil.mapfold (fn (x, c) =>
adamc@11 174 S.bind2 (mfc ctx x,
adamc@6 175 fn x' =>
adamc@11 176 S.map2 (mfc ctx c,
adamc@6 177 fn c' =>
adamc@6 178 (x', c'))))
adamc@6 179 xcs,
adamc@6 180 fn xcs' =>
adamc@6 181 (CRecord (k', xcs'), loc)))
adamc@6 182 | CConcat (c1, c2) =>
adamc@11 183 S.bind2 (mfc ctx c1,
adamc@6 184 fn c1' =>
adamc@11 185 S.map2 (mfc ctx c2,
adamc@6 186 fn c2' =>
adamc@6 187 (CConcat (c1', c2'), loc)))
adamc@621 188 | CMap (k1, k2) =>
adamc@623 189 S.bind2 (mfk ctx k1,
adamc@67 190 fn k1' =>
adamc@623 191 S.map2 (mfk ctx k2,
adamc@67 192 fn k2' =>
adamc@621 193 (CMap (k1', k2'), loc)))
adamc@6 194
adamc@82 195 | CUnit => S.return2 cAll
adamc@82 196
adamc@207 197 | CTuple cs =>
adamc@207 198 S.map2 (ListUtil.mapfold (mfc ctx) cs,
adamc@207 199 fn cs' =>
adamc@207 200 (CTuple cs', loc))
adamc@207 201
adamc@207 202 | CProj (c, n) =>
adamc@207 203 S.map2 (mfc ctx c,
adamc@207 204 fn c' =>
adamc@207 205 (CProj (c', n), loc))
adamc@207 206
adamc@6 207 | CError => S.return2 cAll
adamc@76 208 | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c
adamc@6 209 | CUnif _ => S.return2 cAll
adamc@623 210
adamc@623 211 | CKAbs (x, c) =>
adamc@623 212 S.map2 (mfc (bind (ctx, RelK x)) c,
adamc@623 213 fn c' =>
adamc@623 214 (CKAbs (x, c'), loc))
adamc@623 215 | CKApp (c, k) =>
adamc@623 216 S.bind2 (mfc ctx c,
adamc@623 217 fn c' =>
adamc@623 218 S.map2 (mfk ctx k,
adamc@623 219 fn k' =>
adamc@623 220 (CKApp (c', k'), loc)))
adamc@623 221 | TKFun (x, c) =>
adamc@623 222 S.map2 (mfc (bind (ctx, RelK x)) c,
adamc@623 223 fn c' =>
adamc@623 224 (TKFun (x, c'), loc))
adamc@6 225 in
adamc@6 226 mfc
adamc@6 227 end
adamc@6 228
adamc@11 229 fun mapfold {kind = fk, con = fc} =
adamc@623 230 mapfoldB {kind = fn () => fk,
adamc@11 231 con = fn () => fc,
adamc@11 232 bind = fn ((), _) => ()} ()
adamc@11 233
adamc@11 234 fun mapB {kind, con, bind} ctx c =
adamc@623 235 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@11 236 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@11 237 bind = bind} ctx c () of
adamc@11 238 S.Continue (c, ()) => c
adamc@34 239 | S.Return _ => raise Fail "ElabUtil.Con.mapB: Impossible"
adamc@34 240
adamc@34 241 fun map {kind, con} s =
adamc@34 242 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@34 243 con = fn c => fn () => S.Continue (con c, ())} s () of
adamc@34 244 S.Return () => raise Fail "ElabUtil.Con.map: Impossible"
adamc@34 245 | S.Continue (s, ()) => s
adamc@11 246
adamc@711 247 fun existsB {kind, con, bind} ctx c =
adamc@711 248 case mapfoldB {kind = fn ctx => fn k => fn () =>
adamc@711 249 if kind (ctx, k) then
adamc@711 250 S.Return ()
adamc@711 251 else
adamc@711 252 S.Continue (k, ()),
adamc@711 253 con = fn ctx => fn c => fn () =>
adamc@711 254 if con (ctx, c) then
adamc@711 255 S.Return ()
adamc@711 256 else
adamc@711 257 S.Continue (c, ()),
adamc@711 258 bind = bind} ctx c () of
adamc@711 259 S.Return _ => true
adamc@711 260 | S.Continue _ => false
adamc@711 261
adamc@711 262 fun exists {kind, con} c =
adamc@6 263 case mapfold {kind = fn k => fn () =>
adamc@6 264 if kind k then
adamc@6 265 S.Return ()
adamc@6 266 else
adamc@6 267 S.Continue (k, ()),
adamc@6 268 con = fn c => fn () =>
adamc@6 269 if con c then
adamc@6 270 S.Return ()
adamc@6 271 else
adamc@711 272 S.Continue (c, ())} c () of
adamc@2 273 S.Return _ => true
adamc@2 274 | S.Continue _ => false
adamc@2 275
adamc@448 276 fun foldB {kind, con, bind} ctx st c =
adamc@623 277 case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)),
adamc@448 278 con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
adamc@448 279 bind = bind} ctx c st of
adamc@448 280 S.Continue (_, st) => st
adamc@448 281 | S.Return _ => raise Fail "ElabUtil.Con.foldB: Impossible"
adamc@448 282
adamc@839 283 fun fold {kind, con} st c =
adamc@839 284 case mapfoldB {kind = fn () => fn k => fn st => S.Continue (k, kind (k, st)),
adamc@839 285 con = fn () => fn c => fn st => S.Continue (c, con (c, st)),
adamc@839 286 bind = fn ((), _) => ()} () c st of
adamc@839 287 S.Continue (_, st) => st
adamc@839 288 | S.Return _ => raise Fail "ElabUtil.Con.fold: Impossible"
adamc@839 289
adamc@2 290 end
adamc@2 291
adamc@10 292 structure Exp = struct
adamc@10 293
adamc@11 294 datatype binder =
adamc@623 295 RelK of string
adamc@623 296 | RelC of string * Elab.kind
adamc@792 297 | NamedC of string * int * Elab.kind * Elab.con option
adamc@11 298 | RelE of string * Elab.con
adamc@11 299 | NamedE of string * Elab.con
adamc@11 300
adamc@11 301 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
adamc@10 302 let
adamc@623 303 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@10 304
adamc@11 305 fun bind' (ctx, b) =
adamc@11 306 let
adamc@11 307 val b' = case b of
adamc@623 308 Con.RelK x => RelK x
adamc@623 309 | Con.RelC x => RelC x
adamc@623 310 | Con.NamedC x => NamedC x
adamc@11 311 in
adamc@11 312 bind (ctx, b')
adamc@11 313 end
adamc@11 314 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@10 315
adamc@825 316 fun doVars ((p, _), ctx) =
adamc@825 317 case p of
adamc@825 318 PWild => ctx
adamc@825 319 | PVar xt => bind (ctx, RelE xt)
adamc@825 320 | PPrim _ => ctx
adamc@825 321 | PCon (_, _, _, NONE) => ctx
adamc@825 322 | PCon (_, _, _, SOME p) => doVars (p, ctx)
adamc@825 323 | PRecord xpcs =>
adamc@825 324 foldl (fn ((_, p, _), ctx) => doVars (p, ctx))
adamc@825 325 ctx xpcs
adamc@825 326
adamc@11 327 fun mfe ctx e acc =
adamc@11 328 S.bindP (mfe' ctx e acc, fe ctx)
adamc@11 329
adamc@11 330 and mfe' ctx (eAll as (e, loc)) =
adamc@10 331 case e of
adamc@14 332 EPrim _ => S.return2 eAll
adamc@14 333 | ERel _ => S.return2 eAll
adamc@10 334 | ENamed _ => S.return2 eAll
adamc@34 335 | EModProj _ => S.return2 eAll
adamc@10 336 | EApp (e1, e2) =>
adamc@11 337 S.bind2 (mfe ctx e1,
adamc@10 338 fn e1' =>
adamc@11 339 S.map2 (mfe ctx e2,
adamc@10 340 fn e2' =>
adamc@10 341 (EApp (e1', e2'), loc)))
adamc@26 342 | EAbs (x, dom, ran, e) =>
adamc@26 343 S.bind2 (mfc ctx dom,
adamc@26 344 fn dom' =>
adamc@26 345 S.bind2 (mfc ctx ran,
adamc@26 346 fn ran' =>
adamc@26 347 S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
adamc@26 348 fn e' =>
adamc@26 349 (EAbs (x, dom', ran', e'), loc))))
adamc@26 350
adamc@10 351 | ECApp (e, c) =>
adamc@11 352 S.bind2 (mfe ctx e,
adamc@10 353 fn e' =>
adamc@11 354 S.map2 (mfc ctx c,
adamc@10 355 fn c' =>
adamc@10 356 (ECApp (e', c'), loc)))
adamc@10 357 | ECAbs (expl, x, k, e) =>
adamc@623 358 S.bind2 (mfk ctx k,
adamc@10 359 fn k' =>
adamc@11 360 S.map2 (mfe (bind (ctx, RelC (x, k))) e,
adamc@10 361 fn e' =>
adamc@10 362 (ECAbs (expl, x, k', e'), loc)))
adamc@10 363
adamc@12 364 | ERecord xes =>
adamc@29 365 S.map2 (ListUtil.mapfold (fn (x, e, t) =>
adamc@12 366 S.bind2 (mfc ctx x,
adamc@12 367 fn x' =>
adamc@29 368 S.bind2 (mfe ctx e,
adamc@12 369 fn e' =>
adamc@29 370 S.map2 (mfc ctx t,
adamc@29 371 fn t' =>
adamc@29 372 (x', e', t')))))
adamc@12 373 xes,
adamc@12 374 fn xes' =>
adamc@12 375 (ERecord xes', loc))
adamc@12 376 | EField (e, c, {field, rest}) =>
adamc@12 377 S.bind2 (mfe ctx e,
adamc@12 378 fn e' =>
adamc@12 379 S.bind2 (mfc ctx c,
adamc@12 380 fn c' =>
adamc@12 381 S.bind2 (mfc ctx field,
adamc@12 382 fn field' =>
adamc@12 383 S.map2 (mfc ctx rest,
adamc@12 384 fn rest' =>
adamc@12 385 (EField (e', c', {field = field', rest = rest'}), loc)))))
adamc@445 386 | EConcat (e1, c1, e2, c2) =>
adamc@339 387 S.bind2 (mfe ctx e1,
adamc@339 388 fn e1' =>
adamc@445 389 S.bind2 (mfc ctx c1,
adamc@445 390 fn c1' =>
adamc@339 391 S.bind2 (mfe ctx e2,
adamc@339 392 fn e2' =>
adamc@445 393 S.map2 (mfc ctx c2,
adamc@445 394 fn c2' =>
adamc@445 395 (EConcat (e1', c1', e2', c2'),
adamc@445 396 loc)))))
adamc@149 397 | ECut (e, c, {field, rest}) =>
adamc@149 398 S.bind2 (mfe ctx e,
adamc@149 399 fn e' =>
adamc@149 400 S.bind2 (mfc ctx c,
adamc@149 401 fn c' =>
adamc@149 402 S.bind2 (mfc ctx field,
adamc@149 403 fn field' =>
adamc@149 404 S.map2 (mfc ctx rest,
adamc@149 405 fn rest' =>
adamc@149 406 (ECut (e', c', {field = field', rest = rest'}), loc)))))
adamc@12 407
adamc@493 408 | ECutMulti (e, c, {rest}) =>
adamc@493 409 S.bind2 (mfe ctx e,
adamc@493 410 fn e' =>
adamc@493 411 S.bind2 (mfc ctx c,
adamc@493 412 fn c' =>
adamc@493 413 S.map2 (mfc ctx rest,
adamc@493 414 fn rest' =>
adamc@493 415 (ECutMulti (e', c', {rest = rest'}), loc))))
adamc@493 416
adamc@182 417 | ECase (e, pes, {disc, result}) =>
adamc@171 418 S.bind2 (mfe ctx e,
adamc@171 419 fn e' =>
adamc@171 420 S.bind2 (ListUtil.mapfold (fn (p, e) =>
adamc@448 421 let
adamc@448 422 fun pb ((p, _), ctx) =
adamc@448 423 case p of
adamc@448 424 PWild => ctx
adamc@448 425 | PVar (x, t) => bind (ctx, RelE (x, t))
adamc@448 426 | PPrim _ => ctx
adamc@448 427 | PCon (_, _, _, NONE) => ctx
adamc@448 428 | PCon (_, _, _, SOME p) => pb (p, ctx)
adamc@448 429 | PRecord xps => foldl (fn ((_, p, _), ctx) =>
adamc@448 430 pb (p, ctx)) ctx xps
adamc@448 431 in
adamc@448 432 S.map2 (mfe (pb (p, ctx)) e,
adamc@448 433 fn e' => (p, e'))
adamc@448 434 end) pes,
adamc@171 435 fn pes' =>
adamc@182 436 S.bind2 (mfc ctx disc,
adamc@182 437 fn disc' =>
adamc@182 438 S.map2 (mfc ctx result,
adamc@182 439 fn result' =>
adamc@182 440 (ECase (e', pes', {disc = disc', result = result'}), loc)))))
adamc@171 441
adamc@10 442 | EError => S.return2 eAll
adamc@228 443 | EUnif (ref (SOME e)) => mfe ctx e
adamc@228 444 | EUnif _ => S.return2 eAll
adamc@447 445
adamc@825 446 | ELet (des, e, t) =>
adamc@447 447 let
adamc@826 448 val (des, ctx') = foldl (fn (ed, (des, ctx)) =>
adamc@826 449 let
adamc@826 450 val ctx' =
adamc@826 451 case #1 ed of
adamc@826 452 EDVal (p, _, _) => doVars (p, ctx)
adamc@826 453 | EDValRec vis =>
adamc@826 454 foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t)))
adamc@826 455 ctx vis
adamc@826 456 in
adamc@826 457 (S.bind2 (des,
adamc@826 458 fn des' =>
adamc@826 459 S.map2 (mfed ctx ed,
adamc@826 460 fn ed' => ed' :: des')),
adamc@826 461 ctx')
adamc@826 462 end)
adamc@447 463 (S.return2 [], ctx) des
adamc@447 464 in
adamc@447 465 S.bind2 (des,
adamc@447 466 fn des' =>
adamc@826 467 S.bind2 (mfe ctx' e,
adamc@447 468 fn e' =>
adamc@825 469 S.map2 (mfc ctx t,
adamc@825 470 fn t' =>
adamc@826 471 (ELet (rev des', e', t'), loc))))
adamc@447 472 end
adamc@447 473
adamc@623 474 | EKAbs (x, e) =>
adamc@623 475 S.map2 (mfe (bind (ctx, RelK x)) e,
adamc@623 476 fn e' =>
adamc@623 477 (EKAbs (x, e'), loc))
adamc@623 478 | EKApp (e, k) =>
adamc@623 479 S.bind2 (mfe ctx e,
adamc@623 480 fn e' =>
adamc@623 481 S.map2 (mfk ctx k,
adamc@623 482 fn k' =>
adamc@623 483 (EKApp (e', k'), loc)))
adamc@623 484
adamc@447 485 and mfed ctx (dAll as (d, loc)) =
adamc@447 486 case d of
adamc@825 487 EDVal (p, t, e) =>
adamc@825 488 S.bind2 (mfc ctx t,
adamc@825 489 fn t' =>
adamc@826 490 S.map2 (mfe ctx e,
adamc@825 491 fn e' =>
adamc@825 492 (EDVal (p, t', e'), loc)))
adamc@447 493 | EDValRec vis =>
adamc@447 494 let
adamc@453 495 val ctx = foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis
adamc@447 496 in
adamc@447 497 S.map2 (ListUtil.mapfold (mfvi ctx) vis,
adamc@447 498 fn vis' =>
adamc@447 499 (EDValRec vis', loc))
adamc@447 500 end
adamc@447 501
adamc@447 502 and mfvi ctx (x, c, e) =
adamc@447 503 S.bind2 (mfc ctx c,
adamc@447 504 fn c' =>
adamc@447 505 S.map2 (mfe ctx e,
adamc@447 506 fn e' =>
adamc@447 507 (x, c', e')))
adamc@10 508 in
adamc@10 509 mfe
adamc@10 510 end
adamc@10 511
adamc@11 512 fun mapfold {kind = fk, con = fc, exp = fe} =
adamc@623 513 mapfoldB {kind = fn () => fk,
adamc@11 514 con = fn () => fc,
adamc@11 515 exp = fn () => fe,
adamc@11 516 bind = fn ((), _) => ()} ()
adamc@11 517
adamc@10 518 fun exists {kind, con, exp} k =
adamc@10 519 case mapfold {kind = fn k => fn () =>
adamc@10 520 if kind k then
adamc@10 521 S.Return ()
adamc@10 522 else
adamc@10 523 S.Continue (k, ()),
adamc@10 524 con = fn c => fn () =>
adamc@10 525 if con c then
adamc@10 526 S.Return ()
adamc@10 527 else
adamc@10 528 S.Continue (c, ()),
adamc@10 529 exp = fn e => fn () =>
adamc@10 530 if exp e then
adamc@10 531 S.Return ()
adamc@10 532 else
adamc@10 533 S.Continue (e, ())} k () of
adamc@10 534 S.Return _ => true
adamc@10 535 | S.Continue _ => false
adamc@10 536
adamc@211 537 fun mapB {kind, con, exp, bind} ctx e =
adamc@623 538 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@211 539 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@211 540 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
adamc@211 541 bind = bind} ctx e () of
adamc@211 542 S.Continue (e, ()) => e
adamc@211 543 | S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible"
adamc@211 544
adamc@448 545 fun foldB {kind, con, exp, bind} ctx st e =
adamc@623 546 case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)),
adamc@448 547 con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
adamc@448 548 exp = fn ctx => fn e => fn st => S.Continue (e, exp (ctx, e, st)),
adamc@448 549 bind = bind} ctx e st of
adamc@448 550 S.Continue (_, st) => st
adamc@448 551 | S.Return _ => raise Fail "ElabUtil.Exp.foldB: Impossible"
adamc@448 552
adamc@10 553 end
adamc@10 554
adamc@34 555 structure Sgn = struct
adamc@34 556
adamc@34 557 datatype binder =
adamc@623 558 RelK of string
adamc@623 559 | RelC of string * Elab.kind
adamc@792 560 | NamedC of string * int * Elab.kind * Elab.con option
adamc@792 561 | Str of string * int * Elab.sgn
adamc@792 562 | Sgn of string * int * Elab.sgn
adamc@34 563
adamc@34 564 fun mapfoldB {kind, con, sgn_item, sgn, bind} =
adamc@34 565 let
adamc@34 566 fun bind' (ctx, b) =
adamc@34 567 let
adamc@34 568 val b' = case b of
adamc@623 569 Con.RelK x => RelK x
adamc@623 570 | Con.RelC x => RelC x
adamc@623 571 | Con.NamedC x => NamedC x
adamc@34 572 in
adamc@34 573 bind (ctx, b')
adamc@34 574 end
adamc@34 575 val con = Con.mapfoldB {kind = kind, con = con, bind = bind'}
adamc@34 576
adamc@623 577 val kind = Kind.mapfoldB {kind = kind, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@34 578
adamc@34 579 fun sgi ctx si acc =
adamc@34 580 S.bindP (sgi' ctx si acc, sgn_item ctx)
adamc@34 581
adamc@156 582 and sgi' ctx (siAll as (si, loc)) =
adamc@34 583 case si of
adamc@34 584 SgiConAbs (x, n, k) =>
adamc@623 585 S.map2 (kind ctx k,
adamc@34 586 fn k' =>
adamc@34 587 (SgiConAbs (x, n, k'), loc))
adamc@34 588 | SgiCon (x, n, k, c) =>
adamc@623 589 S.bind2 (kind ctx k,
adamc@34 590 fn k' =>
adamc@34 591 S.map2 (con ctx c,
adamc@34 592 fn c' =>
adamc@34 593 (SgiCon (x, n, k', c'), loc)))
adamc@805 594 | SgiDatatype dts =>
adamc@805 595 S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
adamc@805 596 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@805 597 case c of
adamc@805 598 NONE => S.return2 (x, n, c)
adamc@805 599 | SOME c =>
adamc@805 600 S.map2 (con ctx c,
adamc@805 601 fn c' => (x, n, SOME c'))) xncs,
adamc@805 602 fn xncs' => (x, n, xs, xncs'))) dts,
adamc@805 603 fn dts' =>
adamc@805 604 (SgiDatatype dts', loc))
adamc@191 605 | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
adamc@162 606 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@162 607 case c of
adamc@162 608 NONE => S.return2 (x, n, c)
adamc@162 609 | SOME c =>
adamc@162 610 S.map2 (con ctx c,
adamc@162 611 fn c' => (x, n, SOME c'))) xncs,
adamc@162 612 fn xncs' =>
adamc@191 613 (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
adamc@34 614 | SgiVal (x, n, c) =>
adamc@34 615 S.map2 (con ctx c,
adamc@34 616 fn c' =>
adamc@34 617 (SgiVal (x, n, c'), loc))
adamc@34 618 | SgiStr (x, n, s) =>
adamc@34 619 S.map2 (sg ctx s,
adamc@34 620 fn s' =>
adamc@34 621 (SgiStr (x, n, s'), loc))
adamc@59 622 | SgiSgn (x, n, s) =>
adamc@59 623 S.map2 (sg ctx s,
adamc@59 624 fn s' =>
adamc@59 625 (SgiSgn (x, n, s'), loc))
adamc@88 626 | SgiConstraint (c1, c2) =>
adamc@88 627 S.bind2 (con ctx c1,
adamc@88 628 fn c1' =>
adamc@88 629 S.map2 (con ctx c2,
adamc@88 630 fn c2' =>
adamc@88 631 (SgiConstraint (c1', c2'), loc)))
adamc@563 632 | SgiClassAbs (x, n, k) =>
adamc@623 633 S.map2 (kind ctx k,
adamc@563 634 fn k' =>
adamc@563 635 (SgiClassAbs (x, n, k'), loc))
adamc@563 636 | SgiClass (x, n, k, c) =>
adamc@623 637 S.bind2 (kind ctx k,
adamc@563 638 fn k' =>
adamc@563 639 S.map2 (con ctx c,
adamc@563 640 fn c' =>
adamc@563 641 (SgiClass (x, n, k', c'), loc)))
adamc@34 642
adamc@34 643 and sg ctx s acc =
adamc@34 644 S.bindP (sg' ctx s acc, sgn ctx)
adamc@34 645
adamc@34 646 and sg' ctx (sAll as (s, loc)) =
adamc@34 647 case s of
adamc@34 648 SgnConst sgis =>
adamc@34 649 S.map2 (ListUtil.mapfoldB (fn (ctx, si) =>
adamc@34 650 (case #1 si of
adamc@329 651 SgiConAbs (x, n, k) =>
adamc@792 652 bind (ctx, NamedC (x, n, k, NONE))
adamc@792 653 | SgiCon (x, n, k, c) =>
adamc@792 654 bind (ctx, NamedC (x, n, k, SOME c))
adamc@805 655 | SgiDatatype dts =>
adamc@805 656 foldl (fn ((x, n, ks, _), ctx) =>
adamc@805 657 let
adamc@805 658 val k' = (KType, loc)
adamc@805 659 val k = foldl (fn (_, k) => (KArrow (k', k), loc))
adamc@805 660 k' ks
adamc@805 661 in
adamc@805 662 bind (ctx, NamedC (x, n, k, NONE))
adamc@805 663 end) ctx dts
adamc@792 664 | SgiDatatypeImp (x, n, m1, ms, s, _, _) =>
adamc@792 665 bind (ctx, NamedC (x, n, (KType, loc),
adamc@792 666 SOME (CModProj (m1, ms, s), loc)))
adamc@34 667 | SgiVal _ => ctx
adamc@792 668 | SgiStr (x, n, sgn) =>
adamc@792 669 bind (ctx, Str (x, n, sgn))
adamc@792 670 | SgiSgn (x, n, sgn) =>
adamc@792 671 bind (ctx, Sgn (x, n, sgn))
adamc@203 672 | SgiConstraint _ => ctx
adamc@563 673 | SgiClassAbs (x, n, k) =>
adamc@792 674 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), NONE))
adamc@792 675 | SgiClass (x, n, k, c) =>
adamc@792 676 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), SOME c)),
adamc@34 677 sgi ctx si)) ctx sgis,
adamc@34 678 fn sgis' =>
adamc@34 679 (SgnConst sgis', loc))
adamc@34 680
adamc@34 681 | SgnVar _ => S.return2 sAll
adamc@41 682 | SgnFun (m, n, s1, s2) =>
adamc@41 683 S.bind2 (sg ctx s1,
adamc@41 684 fn s1' =>
adamc@792 685 S.map2 (sg (bind (ctx, Str (m, n, s1'))) s2,
adamc@41 686 fn s2' =>
adamc@41 687 (SgnFun (m, n, s1', s2'), loc)))
adamc@59 688 | SgnProj _ => S.return2 sAll
adamc@42 689 | SgnWhere (sgn, x, c) =>
adamc@42 690 S.bind2 (sg ctx sgn,
adamc@42 691 fn sgn' =>
adamc@42 692 S.map2 (con ctx c,
adamc@42 693 fn c' =>
adamc@42 694 (SgnWhere (sgn', x, c'), loc)))
adamc@34 695 | SgnError => S.return2 sAll
adamc@34 696 in
adamc@34 697 sg
adamc@34 698 end
adamc@34 699
adamc@34 700 fun mapfold {kind, con, sgn_item, sgn} =
adamc@623 701 mapfoldB {kind = fn () => kind,
adamc@34 702 con = fn () => con,
adamc@34 703 sgn_item = fn () => sgn_item,
adamc@34 704 sgn = fn () => sgn,
adamc@34 705 bind = fn ((), _) => ()} ()
adamc@34 706
adamc@792 707 fun mapB {kind, con, sgn_item, sgn, bind} ctx s =
adamc@792 708 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@792 709 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@792 710 sgn_item = fn ctx => fn sgi => fn () => S.Continue (sgn_item ctx sgi, ()),
adamc@792 711 sgn = fn ctx => fn s => fn () => S.Continue (sgn ctx s, ()),
adamc@792 712 bind = bind} ctx s () of
adamc@792 713 S.Continue (s, ()) => s
adamc@792 714 | S.Return _ => raise Fail "ElabUtil.Sgn.mapB: Impossible"
adamc@792 715
adamc@34 716 fun map {kind, con, sgn_item, sgn} s =
adamc@34 717 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@34 718 con = fn c => fn () => S.Continue (con c, ()),
adamc@34 719 sgn_item = fn si => fn () => S.Continue (sgn_item si, ()),
adamc@34 720 sgn = fn s => fn () => S.Continue (sgn s, ())} s () of
adamc@34 721 S.Return () => raise Fail "Elab_util.Sgn.map"
adamc@34 722 | S.Continue (s, ()) => s
adamc@34 723
adamc@2 724 end
adamc@34 725
adamc@76 726 structure Decl = struct
adamc@76 727
adamc@76 728 datatype binder =
adamc@623 729 RelK of string
adamc@623 730 | RelC of string * Elab.kind
adamc@792 731 | NamedC of string * int * Elab.kind * Elab.con option
adamc@76 732 | RelE of string * Elab.con
adamc@76 733 | NamedE of string * Elab.con
adamc@76 734 | Str of string * Elab.sgn
adamc@76 735 | Sgn of string * Elab.sgn
adamc@76 736
adamc@76 737 fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} =
adamc@76 738 let
adamc@623 739 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@76 740
adamc@76 741 fun bind' (ctx, b) =
adamc@76 742 let
adamc@76 743 val b' = case b of
adamc@623 744 Con.RelK x => RelK x
adamc@623 745 | Con.RelC x => RelC x
adamc@623 746 | Con.NamedC x => NamedC x
adamc@76 747 in
adamc@76 748 bind (ctx, b')
adamc@76 749 end
adamc@76 750 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@76 751
adamc@76 752 fun bind' (ctx, b) =
adamc@76 753 let
adamc@76 754 val b' = case b of
adamc@623 755 Exp.RelK x => RelK x
adamc@623 756 | Exp.RelC x => RelC x
adamc@76 757 | Exp.NamedC x => NamedC x
adamc@76 758 | Exp.RelE x => RelE x
adamc@76 759 | Exp.NamedE x => NamedE x
adamc@76 760 in
adamc@76 761 bind (ctx, b')
adamc@76 762 end
adamc@76 763 val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind'}
adamc@76 764
adamc@76 765 fun bind' (ctx, b) =
adamc@76 766 let
adamc@76 767 val b' = case b of
adamc@623 768 Sgn.RelK x => RelK x
adamc@623 769 | Sgn.RelC x => RelC x
adamc@76 770 | Sgn.NamedC x => NamedC x
adamc@792 771 | Sgn.Sgn (x, _, y) => Sgn (x, y)
adamc@792 772 | Sgn.Str (x, _, y) => Str (x, y)
adamc@76 773 in
adamc@76 774 bind (ctx, b')
adamc@76 775 end
adamc@76 776 val mfsg = Sgn.mapfoldB {kind = fk, con = fc, sgn_item = fsgi, sgn = fsg, bind = bind'}
adamc@76 777
adamc@76 778 fun mfst ctx str acc =
adamc@76 779 S.bindP (mfst' ctx str acc, fst ctx)
adamc@76 780
adamc@76 781 and mfst' ctx (strAll as (str, loc)) =
adamc@76 782 case str of
adamc@76 783 StrConst ds =>
adamc@76 784 S.map2 (ListUtil.mapfoldB (fn (ctx, d) =>
adamc@76 785 (case #1 d of
adamc@792 786 DCon (x, n, k, c) =>
adamc@792 787 bind (ctx, NamedC (x, n, k, SOME c))
adamc@805 788 | DDatatype dts =>
adamc@156 789 let
adamc@805 790 fun doOne ((x, n, xs, xncs), ctx) =
adamc@805 791 let
adamc@805 792 val ctx = bind (ctx, NamedC (x, n, (KType, loc), NONE))
adamc@805 793 in
adamc@805 794 foldl (fn ((x, _, co), ctx) =>
adamc@805 795 let
adamc@805 796 val t =
adamc@805 797 case co of
adamc@805 798 NONE => CNamed n
adamc@805 799 | SOME t => TFun (t, (CNamed n, loc))
adamc@805 800
adamc@805 801 val k = (KType, loc)
adamc@805 802 val t = (t, loc)
adamc@805 803 val t = foldr (fn (x, t) =>
adamc@805 804 (TCFun (Explicit,
adamc@805 805 x,
adamc@805 806 k,
adamc@805 807 t), loc))
adamc@805 808 t xs
adamc@805 809 in
adamc@805 810 bind (ctx, NamedE (x, t))
adamc@805 811 end)
adamc@805 812 ctx xncs
adamc@805 813 end
adamc@156 814 in
adamc@805 815 foldl doOne ctx dts
adamc@156 816 end
adamc@191 817 | DDatatypeImp (x, n, m, ms, x', _, _) =>
adamc@792 818 bind (ctx, NamedC (x, n, (KType, loc),
adamc@792 819 SOME (CModProj (m, ms, x'), loc)))
adamc@76 820 | DVal (x, _, c, _) =>
adamc@76 821 bind (ctx, NamedE (x, c))
adamc@123 822 | DValRec vis =>
adamc@123 823 foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis
adamc@76 824 | DSgn (x, _, sgn) =>
adamc@76 825 bind (ctx, Sgn (x, sgn))
adamc@76 826 | DStr (x, _, sgn, _) =>
adamc@76 827 bind (ctx, Str (x, sgn))
adamc@76 828 | DFfiStr (x, _, sgn) =>
adamc@88 829 bind (ctx, Str (x, sgn))
adamc@100 830 | DConstraint _ => ctx
adamc@203 831 | DExport _ => ctx
adamc@707 832 | DTable (tn, x, n, c, _, pc, _, cc) =>
adamc@705 833 let
adamc@705 834 val ct = (CModProj (n, [], "sql_table"), loc)
adamc@705 835 val ct = (CApp (ct, c), loc)
adamc@707 836 val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc)
adamc@705 837 in
adamc@705 838 bind (ctx, NamedE (x, ct))
adamc@705 839 end
adamc@338 840 | DSequence (tn, x, n) =>
adamc@338 841 bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc)))
adamc@754 842 | DView (tn, x, n, _, c) =>
adamc@754 843 let
adamc@754 844 val ct = (CModProj (n, [], "sql_view"), loc)
adamc@754 845 val ct = (CApp (ct, c), loc)
adamc@754 846 in
adamc@754 847 bind (ctx, NamedE (x, ct))
adamc@754 848 end
adamc@792 849 | DClass (x, n, k, c) =>
adamc@792 850 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), SOME c))
adamc@459 851 | DDatabase _ => ctx
adamc@459 852 | DCookie (tn, x, n, c) =>
adamc@459 853 bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc),
adamc@718 854 c), loc)))
adamc@720 855 | DStyle (tn, x, n) =>
adamc@720 856 bind (ctx, NamedE (x, (CModProj (n, [], "css_class"), loc))),
adamc@76 857 mfd ctx d)) ctx ds,
adamc@76 858 fn ds' => (StrConst ds', loc))
adamc@76 859 | StrVar _ => S.return2 strAll
adamc@76 860 | StrProj (str, x) =>
adamc@76 861 S.map2 (mfst ctx str,
adamc@76 862 fn str' =>
adamc@76 863 (StrProj (str', x), loc))
adamc@76 864 | StrFun (x, n, sgn1, sgn2, str) =>
adamc@76 865 S.bind2 (mfsg ctx sgn1,
adamc@76 866 fn sgn1' =>
adamc@76 867 S.bind2 (mfsg ctx sgn2,
adamc@76 868 fn sgn2' =>
adamc@76 869 S.map2 (mfst ctx str,
adamc@76 870 fn str' =>
adamc@76 871 (StrFun (x, n, sgn1', sgn2', str'), loc))))
adamc@76 872 | StrApp (str1, str2) =>
adamc@76 873 S.bind2 (mfst ctx str1,
adamc@76 874 fn str1' =>
adamc@76 875 S.map2 (mfst ctx str2,
adamc@76 876 fn str2' =>
adamc@76 877 (StrApp (str1', str2'), loc)))
adamc@76 878 | StrError => S.return2 strAll
adamc@76 879
adamc@76 880 and mfd ctx d acc =
adamc@76 881 S.bindP (mfd' ctx d acc, fd ctx)
adamc@76 882
adamc@76 883 and mfd' ctx (dAll as (d, loc)) =
adamc@76 884 case d of
adamc@76 885 DCon (x, n, k, c) =>
adamc@623 886 S.bind2 (mfk ctx k,
adamc@76 887 fn k' =>
adamc@76 888 S.map2 (mfc ctx c,
adamc@76 889 fn c' =>
adamc@76 890 (DCon (x, n, k', c'), loc)))
adamc@805 891 | DDatatype dts =>
adamc@805 892 S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
adamc@805 893 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@805 894 case c of
adamc@805 895 NONE => S.return2 (x, n, c)
adamc@805 896 | SOME c =>
adamc@805 897 S.map2 (mfc ctx c,
adamc@805 898 fn c' => (x, n, SOME c'))) xncs,
adamc@805 899 fn xncs' =>
adamc@805 900 (x, n, xs, xncs'))) dts,
adamc@805 901 fn dts' =>
adamc@805 902 (DDatatype dts', loc))
adamc@191 903 | DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
adamc@162 904 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@162 905 case c of
adamc@162 906 NONE => S.return2 (x, n, c)
adamc@162 907 | SOME c =>
adamc@162 908 S.map2 (mfc ctx c,
adamc@162 909 fn c' => (x, n, SOME c'))) xncs,
adamc@162 910 fn xncs' =>
adamc@191 911 (DDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
adamc@123 912 | DVal vi =>
adamc@123 913 S.map2 (mfvi ctx vi,
adamc@123 914 fn vi' =>
adamc@123 915 (DVal vi', loc))
adamc@123 916 | DValRec vis =>
adamc@123 917 S.map2 (ListUtil.mapfold (mfvi ctx) vis,
adamc@123 918 fn vis' =>
adamc@123 919 (DValRec vis', loc))
adamc@76 920 | DSgn (x, n, sgn) =>
adamc@76 921 S.map2 (mfsg ctx sgn,
adamc@76 922 fn sgn' =>
adamc@76 923 (DSgn (x, n, sgn'), loc))
adamc@76 924 | DStr (x, n, sgn, str) =>
adamc@76 925 S.bind2 (mfsg ctx sgn,
adamc@76 926 fn sgn' =>
adamc@76 927 S.map2 (mfst ctx str,
adamc@76 928 fn str' =>
adamc@76 929 (DStr (x, n, sgn', str'), loc)))
adamc@76 930 | DFfiStr (x, n, sgn) =>
adamc@76 931 S.map2 (mfsg ctx sgn,
adamc@76 932 fn sgn' =>
adamc@76 933 (DFfiStr (x, n, sgn'), loc))
adamc@88 934 | DConstraint (c1, c2) =>
adamc@88 935 S.bind2 (mfc ctx c1,
adamc@88 936 fn c1' =>
adamc@88 937 S.map2 (mfc ctx c2,
adamc@88 938 fn c2' =>
adamc@88 939 (DConstraint (c1', c2'), loc)))
adamc@109 940 | DExport (en, sgn, str) =>
adamc@109 941 S.bind2 (mfsg ctx sgn,
adamc@109 942 fn sgn' =>
adamc@109 943 S.map2 (mfst ctx str,
adamc@109 944 fn str' =>
adamc@109 945 (DExport (en, sgn', str'), loc)))
adamc@123 946
adamc@707 947 | DTable (tn, x, n, c, pe, pc, ce, cc) =>
adamc@704 948 S.bind2 (mfc ctx c,
adamc@203 949 fn c' =>
adamc@707 950 S.bind2 (mfe ctx pe,
adamc@707 951 fn pe' =>
adamc@707 952 S.bind2 (mfc ctx pc,
adamc@707 953 fn pc' =>
adamc@707 954 S.bind2 (mfe ctx ce,
adamc@707 955 fn ce' =>
adamc@707 956 S.map2 (mfc ctx cc,
adamc@707 957 fn cc' =>
adamc@707 958 (DTable (tn, x, n, c', pe', pc', ce', cc'), loc))))))
adamc@338 959 | DSequence _ => S.return2 dAll
adamc@754 960 | DView (tn, x, n, e, c) =>
adamc@754 961 S.bind2 (mfe ctx e,
adamc@754 962 fn e' =>
adamc@754 963 S.map2 (mfc ctx c,
adamc@754 964 fn c' =>
adamc@754 965 (DView (tn, x, n, e', c'), loc)))
adamc@203 966
adamc@563 967 | DClass (x, n, k, c) =>
adamc@623 968 S.bind2 (mfk ctx k,
adamc@563 969 fn k' =>
adamc@563 970 S.map2 (mfc ctx c,
adamc@563 971 fn c' =>
adamc@563 972 (DClass (x, n, k', c'), loc)))
adamc@213 973
adamc@338 974 | DDatabase _ => S.return2 dAll
adamc@271 975
adamc@459 976 | DCookie (tn, x, n, c) =>
adamc@459 977 S.map2 (mfc ctx c,
adamc@459 978 fn c' =>
adamc@459 979 (DCookie (tn, x, n, c'), loc))
adamc@720 980 | DStyle _ => S.return2 dAll
adamc@459 981
adamc@123 982 and mfvi ctx (x, n, c, e) =
adamc@123 983 S.bind2 (mfc ctx c,
adamc@123 984 fn c' =>
adamc@123 985 S.map2 (mfe ctx e,
adamc@123 986 fn e' =>
adamc@123 987 (x, n, c', e')))
adamc@76 988 in
adamc@76 989 mfd
adamc@76 990 end
adamc@76 991
adamc@76 992 fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} =
adamc@623 993 mapfoldB {kind = fn () => kind,
adamc@76 994 con = fn () => con,
adamc@76 995 exp = fn () => exp,
adamc@76 996 sgn_item = fn () => sgn_item,
adamc@76 997 sgn = fn () => sgn,
adamc@76 998 str = fn () => str,
adamc@76 999 decl = fn () => decl,
adamc@76 1000 bind = fn ((), _) => ()} ()
adamc@76 1001
adamc@76 1002 fun exists {kind, con, exp, sgn_item, sgn, str, decl} k =
adamc@76 1003 case mapfold {kind = fn k => fn () =>
adamc@76 1004 if kind k then
adamc@76 1005 S.Return ()
adamc@76 1006 else
adamc@76 1007 S.Continue (k, ()),
adamc@76 1008 con = fn c => fn () =>
adamc@76 1009 if con c then
adamc@76 1010 S.Return ()
adamc@76 1011 else
adamc@76 1012 S.Continue (c, ()),
adamc@76 1013 exp = fn e => fn () =>
adamc@76 1014 if exp e then
adamc@76 1015 S.Return ()
adamc@76 1016 else
adamc@76 1017 S.Continue (e, ()),
adamc@76 1018 sgn_item = fn sgi => fn () =>
adamc@76 1019 if sgn_item sgi then
adamc@76 1020 S.Return ()
adamc@76 1021 else
adamc@76 1022 S.Continue (sgi, ()),
adamc@76 1023 sgn = fn x => fn () =>
adamc@76 1024 if sgn x then
adamc@76 1025 S.Return ()
adamc@76 1026 else
adamc@76 1027 S.Continue (x, ()),
adamc@76 1028 str = fn x => fn () =>
adamc@76 1029 if str x then
adamc@76 1030 S.Return ()
adamc@76 1031 else
adamc@76 1032 S.Continue (x, ()),
adamc@76 1033 decl = fn x => fn () =>
adamc@76 1034 if decl x then
adamc@76 1035 S.Return ()
adamc@76 1036 else
adamc@76 1037 S.Continue (x, ())} k () of
adamc@76 1038 S.Return _ => true
adamc@76 1039 | S.Continue _ => false
adamc@76 1040
adamc@76 1041 fun search {kind, con, exp, sgn_item, sgn, str, decl} k =
adamc@76 1042 case mapfold {kind = fn x => fn () =>
adamc@76 1043 case kind x of
adamc@76 1044 NONE => S.Continue (x, ())
adamc@76 1045 | SOME v => S.Return v,
adamc@76 1046
adamc@76 1047 con = fn x => fn () =>
adamc@76 1048 case con x of
adamc@76 1049 NONE => S.Continue (x, ())
adamc@76 1050 | SOME v => S.Return v,
adamc@76 1051
adamc@76 1052 exp = fn x => fn () =>
adamc@76 1053 case exp x of
adamc@76 1054 NONE => S.Continue (x, ())
adamc@76 1055 | SOME v => S.Return v,
adamc@76 1056
adamc@76 1057 sgn_item = fn x => fn () =>
adamc@76 1058 case sgn_item x of
adamc@76 1059 NONE => S.Continue (x, ())
adamc@76 1060 | SOME v => S.Return v,
adamc@76 1061
adamc@76 1062 sgn = fn x => fn () =>
adamc@76 1063 case sgn x of
adamc@76 1064 NONE => S.Continue (x, ())
adamc@76 1065 | SOME v => S.Return v,
adamc@76 1066
adamc@76 1067 str = fn x => fn () =>
adamc@76 1068 case str x of
adamc@76 1069 NONE => S.Continue (x, ())
adamc@76 1070 | SOME v => S.Return v,
adamc@76 1071
adamc@76 1072 decl = fn x => fn () =>
adamc@76 1073 case decl x of
adamc@76 1074 NONE => S.Continue (x, ())
adamc@76 1075 | SOME v => S.Return v
adamc@76 1076
adamc@76 1077 } k () of
adamc@76 1078 S.Return x => SOME x
adamc@76 1079 | S.Continue _ => NONE
adamc@76 1080
adamc@448 1081 fun foldMapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx st d =
adamc@623 1082 case mapfoldB {kind = fn ctx => fn x => fn st => S.Continue (kind (ctx, x, st)),
adamc@448 1083 con = fn ctx => fn x => fn st => S.Continue (con (ctx, x, st)),
adamc@448 1084 exp = fn ctx => fn x => fn st => S.Continue (exp (ctx, x, st)),
adamc@448 1085 sgn_item = fn ctx => fn x => fn st => S.Continue (sgn_item (ctx, x, st)),
adamc@448 1086 sgn = fn ctx => fn x => fn st => S.Continue (sgn (ctx, x, st)),
adamc@448 1087 str = fn ctx => fn x => fn st => S.Continue (str (ctx, x, st)),
adamc@448 1088 decl = fn ctx => fn x => fn st => S.Continue (decl (ctx, x, st)),
adamc@448 1089 bind = bind} ctx d st of
adamc@448 1090 S.Continue x => x
adamc@448 1091 | S.Return _ => raise Fail "ElabUtil.Decl.foldMapB: Impossible"
adamc@448 1092
adamc@448 1093 end
adamc@448 1094
adamc@448 1095 structure File = struct
adamc@448 1096
adamc@448 1097 fun maxName ds = foldl (fn (d, count) => Int.max (maxNameDecl d, count)) 0 ds
adamc@448 1098
adamc@448 1099 and maxNameDecl (d, _) =
adamc@448 1100 case d of
adamc@448 1101 DCon (_, n, _, _) => n
adamc@805 1102 | DDatatype dts =>
adamc@805 1103 foldl (fn ((_, n, _, ns), max) =>
adamc@448 1104 foldl (fn ((_, n', _), m) => Int.max (n', m))
adamc@805 1105 (Int.max (n, max)) ns) 0 dts
adamc@448 1106 | DDatatypeImp (_, n1, n2, _, _, _, ns) =>
adamc@448 1107 foldl (fn ((_, n', _), m) => Int.max (n', m))
adamc@448 1108 (Int.max (n1, n2)) ns
adamc@448 1109 | DVal (_, n, _, _) => n
adamc@448 1110 | DValRec vis => foldl (fn ((_, n, _, _), count) => Int.max (n, count)) 0 vis
adamc@448 1111 | DStr (_, n, sgn, str) => Int.max (n, Int.max (maxNameSgn sgn, maxNameStr str))
adamc@448 1112 | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
adamc@448 1113 | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
adamc@448 1114 | DConstraint _ => 0
adamc@563 1115 | DClass (_, n, _, _) => n
adamc@448 1116 | DExport _ => 0
adamc@707 1117 | DTable (n1, _, n2, _, _, _, _, _) => Int.max (n1, n2)
adamc@459 1118 | DSequence (n1, _, n2) => Int.max (n1, n2)
adamc@754 1119 | DView (n1, _, n2, _, _) => Int.max (n1, n2)
adamc@448 1120 | DDatabase _ => 0
adamc@459 1121 | DCookie (n1, _, n2, _) => Int.max (n1, n2)
adamc@720 1122 | DStyle (n1, _, n2) => Int.max (n1, n2)
adamc@448 1123 and maxNameStr (str, _) =
adamc@448 1124 case str of
adamc@448 1125 StrConst ds => maxName ds
adamc@448 1126 | StrVar n => n
adamc@448 1127 | StrProj (str, _) => maxNameStr str
adamc@448 1128 | StrFun (_, n, dom, ran, str) => foldl Int.max n [maxNameSgn dom, maxNameSgn ran, maxNameStr str]
adamc@448 1129 | StrApp (str1, str2) => Int.max (maxNameStr str1, maxNameStr str2)
adamc@448 1130 | StrError => 0
adamc@448 1131
adamc@448 1132 and maxNameSgn (sgn, _) =
adamc@448 1133 case sgn of
adamc@448 1134 SgnConst sgis => foldl (fn (sgi, count) => Int.max (maxNameSgi sgi, count)) 0 sgis
adamc@448 1135 | SgnVar n => n
adamc@448 1136 | SgnFun (_, n, dom, ran) => Int.max (n, Int.max (maxNameSgn dom, maxNameSgn ran))
adamc@448 1137 | SgnWhere (sgn, _, _) => maxNameSgn sgn
adamc@448 1138 | SgnProj (n, _, _) => n
adamc@448 1139 | SgnError => 0
adamc@448 1140
adamc@448 1141 and maxNameSgi (sgi, _) =
adamc@448 1142 case sgi of
adamc@448 1143 SgiConAbs (_, n, _) => n
adamc@448 1144 | SgiCon (_, n, _, _) => n
adamc@805 1145 | SgiDatatype dts =>
adamc@805 1146 foldl (fn ((_, n, _, ns), max) =>
adamc@805 1147 foldl (fn ((_, n', _), m) => Int.max (n', m))
adamc@805 1148 (Int.max (n, max)) ns) 0 dts
adamc@448 1149 | SgiDatatypeImp (_, n1, n2, _, _, _, ns) =>
adamc@448 1150 foldl (fn ((_, n', _), m) => Int.max (n', m))
adamc@448 1151 (Int.max (n1, n2)) ns
adamc@448 1152 | SgiVal (_, n, _) => n
adamc@448 1153 | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
adamc@448 1154 | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
adamc@448 1155 | SgiConstraint _ => 0
adamc@563 1156 | SgiClassAbs (_, n, _) => n
adamc@563 1157 | SgiClass (_, n, _, _) => n
adamc@448 1158
adamc@34 1159 end
adamc@76 1160
adamc@76 1161 end