Mercurial > urweb

annotate src/elab_util.sml @ 1739:c414850f206f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add support for -boot flag, which allows in-tree execution of Ur/Web The boot flag rewrites most hardcoded paths to point to the build directory, and also forces static compilation. This is convenient for developing Ur/Web, or if you cannot 'sudo make install' Ur/Web. The following changes were made: * Header files were moved to include/urweb instead of include; this lets FFI users point their C_INCLUDE_PATH at this directory at write <urweb/urweb.h>. For internal Ur/Web executables, we simply pass -I$PATH/include/urweb as normal. * Differentiate between LIB and SRCLIB; SRCLIB is Ur and JavaScript source files, while LIB is compiled products from libtool. For in-tree compilation these live in different places. * No longer reference Config for paths; instead use Settings; these settings can be changed dynamically by Compiler.enableBoot () (TODO: add a disableBoot function.) * config.h is now generated directly in include/urweb/config.h, for consistency's sake (especially since it gets installed along with the rest of the headers!) * All of the autotools build products got updated. * The linkStatic field in protocols now only contains the name of the build product, and not the absolute path. Future users have to be careful not to reference the Settings files to early, lest they get an old version (this was the source of two bugs during development of this patch.)
author Edward Z. Yang <ezyang@mit.edu>
date Wed, 02 May 2012 17:17:57 -0400
parents 4a03aa3251cb
children d28adceef22a
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
adamc@10 571 fun exists {kind, con, exp} k =
adamc@10 572 case mapfold {kind = fn k => fn () =>
adamc@10 573 if kind k then
adamc@10 574 S.Return ()
adamc@10 575 else
adamc@10 576 S.Continue (k, ()),
adamc@10 577 con = fn c => fn () =>
adamc@10 578 if con c then
adamc@10 579 S.Return ()
adamc@10 580 else
adamc@10 581 S.Continue (c, ()),
adamc@10 582 exp = fn e => fn () =>
adamc@10 583 if exp e then
adamc@10 584 S.Return ()
adamc@10 585 else
adamc@10 586 S.Continue (e, ())} k () of
adamc@10 587 S.Return _ => true
adamc@10 588 | S.Continue _ => false
adamc@10 589
adamc@211 590 fun mapB {kind, con, exp, bind} ctx e =
adamc@623 591 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@211 592 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@211 593 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
adamc@211 594 bind = bind} ctx e () of
adamc@211 595 S.Continue (e, ()) => e
adamc@211 596 | S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible"
adamc@211 597
adamc@448 598 fun foldB {kind, con, exp, bind} ctx st e =
adamc@623 599 case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, k, st)),
adamc@448 600 con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)),
adamc@448 601 exp = fn ctx => fn e => fn st => S.Continue (e, exp (ctx, e, st)),
adamc@448 602 bind = bind} ctx e st of
adamc@448 603 S.Continue (_, st) => st
adamc@448 604 | S.Return _ => raise Fail "ElabUtil.Exp.foldB: Impossible"
adamc@448 605
adamc@10 606 end
adamc@10 607
adamc@34 608 structure Sgn = struct
adamc@34 609
adamc@34 610 datatype binder =
adamc@623 611 RelK of string
adamc@623 612 | RelC of string * Elab.kind
adamc@792 613 | NamedC of string * int * Elab.kind * Elab.con option
adamc@792 614 | Str of string * int * Elab.sgn
adamc@792 615 | Sgn of string * int * Elab.sgn
adamc@34 616
adamc@34 617 fun mapfoldB {kind, con, sgn_item, sgn, bind} =
adamc@34 618 let
adamc@34 619 fun bind' (ctx, b) =
adamc@34 620 let
adamc@34 621 val b' = case b of
adamc@623 622 Con.RelK x => RelK x
adamc@623 623 | Con.RelC x => RelC x
adamc@623 624 | Con.NamedC x => NamedC x
adamc@34 625 in
adamc@34 626 bind (ctx, b')
adamc@34 627 end
adamc@34 628 val con = Con.mapfoldB {kind = kind, con = con, bind = bind'}
adamc@34 629
adamc@623 630 val kind = Kind.mapfoldB {kind = kind, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@34 631
adamc@34 632 fun sgi ctx si acc =
adamc@34 633 S.bindP (sgi' ctx si acc, sgn_item ctx)
adamc@34 634
adamc@156 635 and sgi' ctx (siAll as (si, loc)) =
adamc@34 636 case si of
adamc@34 637 SgiConAbs (x, n, k) =>
adamc@623 638 S.map2 (kind ctx k,
adamc@34 639 fn k' =>
adamc@34 640 (SgiConAbs (x, n, k'), loc))
adamc@34 641 | SgiCon (x, n, k, c) =>
adamc@623 642 S.bind2 (kind ctx k,
adamc@34 643 fn k' =>
adamc@34 644 S.map2 (con ctx c,
adamc@34 645 fn c' =>
adamc@34 646 (SgiCon (x, n, k', c'), loc)))
adamc@805 647 | SgiDatatype dts =>
adamc@805 648 S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
adamc@805 649 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@805 650 case c of
adamc@805 651 NONE => S.return2 (x, n, c)
adamc@805 652 | SOME c =>
adamc@805 653 S.map2 (con ctx c,
adamc@805 654 fn c' => (x, n, SOME c'))) xncs,
adamc@805 655 fn xncs' => (x, n, xs, xncs'))) dts,
adamc@805 656 fn dts' =>
adamc@805 657 (SgiDatatype dts', loc))
adamc@191 658 | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
adamc@162 659 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@162 660 case c of
adamc@162 661 NONE => S.return2 (x, n, c)
adamc@162 662 | SOME c =>
adamc@162 663 S.map2 (con ctx c,
adamc@162 664 fn c' => (x, n, SOME c'))) xncs,
adamc@162 665 fn xncs' =>
adamc@191 666 (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
adamc@34 667 | SgiVal (x, n, c) =>
adamc@34 668 S.map2 (con ctx c,
adamc@34 669 fn c' =>
adamc@34 670 (SgiVal (x, n, c'), loc))
adamc@34 671 | SgiStr (x, n, s) =>
adamc@34 672 S.map2 (sg ctx s,
adamc@34 673 fn s' =>
adamc@34 674 (SgiStr (x, n, s'), loc))
adamc@59 675 | SgiSgn (x, n, s) =>
adamc@59 676 S.map2 (sg ctx s,
adamc@59 677 fn s' =>
adamc@59 678 (SgiSgn (x, n, s'), loc))
adamc@88 679 | SgiConstraint (c1, c2) =>
adamc@88 680 S.bind2 (con ctx c1,
adamc@88 681 fn c1' =>
adamc@88 682 S.map2 (con ctx c2,
adamc@88 683 fn c2' =>
adamc@88 684 (SgiConstraint (c1', c2'), loc)))
adamc@563 685 | SgiClassAbs (x, n, k) =>
adamc@623 686 S.map2 (kind ctx k,
adamc@563 687 fn k' =>
adamc@563 688 (SgiClassAbs (x, n, k'), loc))
adamc@563 689 | SgiClass (x, n, k, c) =>
adamc@623 690 S.bind2 (kind ctx k,
adamc@563 691 fn k' =>
adamc@563 692 S.map2 (con ctx c,
adamc@563 693 fn c' =>
adamc@563 694 (SgiClass (x, n, k', c'), loc)))
adamc@34 695
adamc@34 696 and sg ctx s acc =
adamc@34 697 S.bindP (sg' ctx s acc, sgn ctx)
adamc@34 698
adamc@34 699 and sg' ctx (sAll as (s, loc)) =
adamc@34 700 case s of
adamc@34 701 SgnConst sgis =>
adamc@34 702 S.map2 (ListUtil.mapfoldB (fn (ctx, si) =>
adamc@34 703 (case #1 si of
adamc@329 704 SgiConAbs (x, n, k) =>
adamc@792 705 bind (ctx, NamedC (x, n, k, NONE))
adamc@792 706 | SgiCon (x, n, k, c) =>
adamc@792 707 bind (ctx, NamedC (x, n, k, SOME c))
adamc@805 708 | SgiDatatype dts =>
adamc@805 709 foldl (fn ((x, n, ks, _), ctx) =>
adamc@805 710 let
adamc@805 711 val k' = (KType, loc)
adamc@805 712 val k = foldl (fn (_, k) => (KArrow (k', k), loc))
adamc@805 713 k' ks
adamc@805 714 in
adamc@805 715 bind (ctx, NamedC (x, n, k, NONE))
adamc@805 716 end) ctx dts
adamc@792 717 | SgiDatatypeImp (x, n, m1, ms, s, _, _) =>
adamc@792 718 bind (ctx, NamedC (x, n, (KType, loc),
adamc@792 719 SOME (CModProj (m1, ms, s), loc)))
adamc@34 720 | SgiVal _ => ctx
adamc@792 721 | SgiStr (x, n, sgn) =>
adamc@792 722 bind (ctx, Str (x, n, sgn))
adamc@792 723 | SgiSgn (x, n, sgn) =>
adamc@792 724 bind (ctx, Sgn (x, n, sgn))
adamc@203 725 | SgiConstraint _ => ctx
adamc@563 726 | SgiClassAbs (x, n, k) =>
adamc@792 727 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), NONE))
adamc@792 728 | SgiClass (x, n, k, c) =>
adamc@792 729 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), SOME c)),
adamc@34 730 sgi ctx si)) ctx sgis,
adamc@34 731 fn sgis' =>
adamc@34 732 (SgnConst sgis', loc))
adamc@34 733
adamc@34 734 | SgnVar _ => S.return2 sAll
adamc@41 735 | SgnFun (m, n, s1, s2) =>
adamc@41 736 S.bind2 (sg ctx s1,
adamc@41 737 fn s1' =>
adamc@792 738 S.map2 (sg (bind (ctx, Str (m, n, s1'))) s2,
adamc@41 739 fn s2' =>
adamc@41 740 (SgnFun (m, n, s1', s2'), loc)))
adamc@59 741 | SgnProj _ => S.return2 sAll
adamc@42 742 | SgnWhere (sgn, x, c) =>
adamc@42 743 S.bind2 (sg ctx sgn,
adamc@42 744 fn sgn' =>
adamc@42 745 S.map2 (con ctx c,
adamc@42 746 fn c' =>
adamc@42 747 (SgnWhere (sgn', x, c'), loc)))
adamc@34 748 | SgnError => S.return2 sAll
adamc@34 749 in
adamc@34 750 sg
adamc@34 751 end
adamc@34 752
adamc@34 753 fun mapfold {kind, con, sgn_item, sgn} =
adamc@623 754 mapfoldB {kind = fn () => kind,
adamc@34 755 con = fn () => con,
adamc@34 756 sgn_item = fn () => sgn_item,
adamc@34 757 sgn = fn () => sgn,
adamc@34 758 bind = fn ((), _) => ()} ()
adamc@34 759
adamc@792 760 fun mapB {kind, con, sgn_item, sgn, bind} ctx s =
adamc@792 761 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adamc@792 762 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@792 763 sgn_item = fn ctx => fn sgi => fn () => S.Continue (sgn_item ctx sgi, ()),
adamc@792 764 sgn = fn ctx => fn s => fn () => S.Continue (sgn ctx s, ()),
adamc@792 765 bind = bind} ctx s () of
adamc@792 766 S.Continue (s, ()) => s
adamc@792 767 | S.Return _ => raise Fail "ElabUtil.Sgn.mapB: Impossible"
adamc@792 768
adamc@34 769 fun map {kind, con, sgn_item, sgn} s =
adamc@34 770 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@34 771 con = fn c => fn () => S.Continue (con c, ()),
adamc@34 772 sgn_item = fn si => fn () => S.Continue (sgn_item si, ()),
adamc@34 773 sgn = fn s => fn () => S.Continue (sgn s, ())} s () of
adamc@34 774 S.Return () => raise Fail "Elab_util.Sgn.map"
adamc@34 775 | S.Continue (s, ()) => s
adamc@34 776
adamc@2 777 end
adamc@34 778
adamc@76 779 structure Decl = struct
adamc@76 780
adamc@76 781 datatype binder =
adamc@623 782 RelK of string
adamc@623 783 | RelC of string * Elab.kind
adamc@792 784 | NamedC of string * int * Elab.kind * Elab.con option
adamc@76 785 | RelE of string * Elab.con
adamc@76 786 | NamedE of string * Elab.con
adam@1345 787 | Str of string * int * Elab.sgn
adam@1345 788 | Sgn of string * int * Elab.sgn
adamc@76 789
adamc@76 790 fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} =
adamc@76 791 let
adamc@623 792 val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)}
adamc@76 793
adamc@76 794 fun bind' (ctx, b) =
adamc@76 795 let
adamc@76 796 val b' = case b of
adamc@623 797 Con.RelK x => RelK x
adamc@623 798 | Con.RelC x => RelC x
adamc@623 799 | Con.NamedC x => NamedC x
adamc@76 800 in
adamc@76 801 bind (ctx, b')
adamc@76 802 end
adamc@76 803 val mfc = Con.mapfoldB {kind = fk, con = fc, 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 Exp.RelK x => RelK x
adamc@623 809 | Exp.RelC x => RelC x
adamc@76 810 | Exp.NamedC x => NamedC x
adamc@76 811 | Exp.RelE x => RelE x
adamc@76 812 | Exp.NamedE x => NamedE x
adamc@76 813 in
adamc@76 814 bind (ctx, b')
adamc@76 815 end
adamc@76 816 val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind'}
adamc@76 817
adamc@76 818 fun bind' (ctx, b) =
adamc@76 819 let
adamc@76 820 val b' = case b of
adamc@623 821 Sgn.RelK x => RelK x
adamc@623 822 | Sgn.RelC x => RelC x
adamc@76 823 | Sgn.NamedC x => NamedC x
adam@1345 824 | Sgn.Sgn x => Sgn x
adam@1345 825 | Sgn.Str x => Str x
adamc@76 826 in
adamc@76 827 bind (ctx, b')
adamc@76 828 end
adamc@76 829 val mfsg = Sgn.mapfoldB {kind = fk, con = fc, sgn_item = fsgi, sgn = fsg, bind = bind'}
adamc@76 830
adamc@76 831 fun mfst ctx str acc =
adamc@76 832 S.bindP (mfst' ctx str acc, fst ctx)
adamc@76 833
adamc@76 834 and mfst' ctx (strAll as (str, loc)) =
adamc@76 835 case str of
adamc@76 836 StrConst ds =>
adamc@76 837 S.map2 (ListUtil.mapfoldB (fn (ctx, d) =>
adamc@76 838 (case #1 d of
adamc@792 839 DCon (x, n, k, c) =>
adamc@792 840 bind (ctx, NamedC (x, n, k, SOME c))
adamc@805 841 | DDatatype dts =>
adamc@156 842 let
adamc@805 843 fun doOne ((x, n, xs, xncs), ctx) =
adamc@805 844 let
adamc@805 845 val ctx = bind (ctx, NamedC (x, n, (KType, loc), NONE))
adamc@805 846 in
adamc@805 847 foldl (fn ((x, _, co), ctx) =>
adamc@805 848 let
adamc@805 849 val t =
adamc@805 850 case co of
adamc@805 851 NONE => CNamed n
adamc@805 852 | SOME t => TFun (t, (CNamed n, loc))
adamc@805 853
adamc@805 854 val k = (KType, loc)
adamc@805 855 val t = (t, loc)
adamc@805 856 val t = foldr (fn (x, t) =>
adamc@805 857 (TCFun (Explicit,
adamc@805 858 x,
adamc@805 859 k,
adamc@805 860 t), loc))
adamc@805 861 t xs
adamc@805 862 in
adamc@805 863 bind (ctx, NamedE (x, t))
adamc@805 864 end)
adamc@805 865 ctx xncs
adamc@805 866 end
adamc@156 867 in
adamc@805 868 foldl doOne ctx dts
adamc@156 869 end
adamc@191 870 | DDatatypeImp (x, n, m, ms, x', _, _) =>
adamc@792 871 bind (ctx, NamedC (x, n, (KType, loc),
adamc@792 872 SOME (CModProj (m, ms, x'), loc)))
adamc@76 873 | DVal (x, _, c, _) =>
adamc@76 874 bind (ctx, NamedE (x, c))
adamc@123 875 | DValRec vis =>
adamc@123 876 foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis
adam@1345 877 | DSgn (x, n, sgn) =>
adam@1345 878 bind (ctx, Sgn (x, n, sgn))
adam@1345 879 | DStr (x, n, sgn, _) =>
adam@1345 880 bind (ctx, Str (x, n, sgn))
adam@1345 881 | DFfiStr (x, n, sgn) =>
adam@1345 882 bind (ctx, Str (x, n, sgn))
adamc@100 883 | DConstraint _ => ctx
adamc@203 884 | DExport _ => ctx
adamc@707 885 | DTable (tn, x, n, c, _, pc, _, cc) =>
adamc@705 886 let
adamc@705 887 val ct = (CModProj (n, [], "sql_table"), loc)
adamc@705 888 val ct = (CApp (ct, c), loc)
adamc@707 889 val ct = (CApp (ct, (CConcat (pc, cc), loc)), loc)
adamc@705 890 in
adamc@705 891 bind (ctx, NamedE (x, ct))
adamc@705 892 end
adamc@338 893 | DSequence (tn, x, n) =>
adamc@338 894 bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc)))
adamc@754 895 | DView (tn, x, n, _, c) =>
adamc@754 896 let
adamc@754 897 val ct = (CModProj (n, [], "sql_view"), loc)
adamc@754 898 val ct = (CApp (ct, c), loc)
adamc@754 899 in
adamc@754 900 bind (ctx, NamedE (x, ct))
adamc@754 901 end
adamc@792 902 | DClass (x, n, k, c) =>
adamc@792 903 bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc), SOME c))
adamc@459 904 | DDatabase _ => ctx
adamc@459 905 | DCookie (tn, x, n, c) =>
adamc@459 906 bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc),
adamc@718 907 c), loc)))
adamc@720 908 | DStyle (tn, x, n) =>
adamc@1073 909 bind (ctx, NamedE (x, (CModProj (n, [], "css_class"), loc)))
adamc@1199 910 | DTask _ => ctx
adam@1294 911 | DPolicy _ => ctx
adam@1294 912 | DOnError _ => ctx,
adamc@76 913 mfd ctx d)) ctx ds,
adamc@76 914 fn ds' => (StrConst ds', loc))
adamc@76 915 | StrVar _ => S.return2 strAll
adamc@76 916 | StrProj (str, x) =>
adamc@76 917 S.map2 (mfst ctx str,
adamc@76 918 fn str' =>
adamc@76 919 (StrProj (str', x), loc))
adamc@76 920 | StrFun (x, n, sgn1, sgn2, str) =>
adamc@76 921 S.bind2 (mfsg ctx sgn1,
adamc@76 922 fn sgn1' =>
adamc@76 923 S.bind2 (mfsg ctx sgn2,
adamc@76 924 fn sgn2' =>
adamc@76 925 S.map2 (mfst ctx str,
adamc@76 926 fn str' =>
adamc@76 927 (StrFun (x, n, sgn1', sgn2', str'), loc))))
adamc@76 928 | StrApp (str1, str2) =>
adamc@76 929 S.bind2 (mfst ctx str1,
adamc@76 930 fn str1' =>
adamc@76 931 S.map2 (mfst ctx str2,
adamc@76 932 fn str2' =>
adamc@76 933 (StrApp (str1', str2'), loc)))
adamc@76 934 | StrError => S.return2 strAll
adamc@76 935
adamc@76 936 and mfd ctx d acc =
adamc@76 937 S.bindP (mfd' ctx d acc, fd ctx)
adamc@76 938
adamc@76 939 and mfd' ctx (dAll as (d, loc)) =
adamc@76 940 case d of
adamc@76 941 DCon (x, n, k, c) =>
adamc@623 942 S.bind2 (mfk ctx k,
adamc@76 943 fn k' =>
adamc@76 944 S.map2 (mfc ctx c,
adamc@76 945 fn c' =>
adamc@76 946 (DCon (x, n, k', c'), loc)))
adamc@805 947 | DDatatype dts =>
adamc@805 948 S.map2 (ListUtil.mapfold (fn (x, n, xs, xncs) =>
adamc@805 949 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@805 950 case c of
adamc@805 951 NONE => S.return2 (x, n, c)
adamc@805 952 | SOME c =>
adamc@805 953 S.map2 (mfc ctx c,
adamc@805 954 fn c' => (x, n, SOME c'))) xncs,
adamc@805 955 fn xncs' =>
adamc@805 956 (x, n, xs, xncs'))) dts,
adamc@805 957 fn dts' =>
adamc@805 958 (DDatatype dts', loc))
adamc@191 959 | DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
adamc@162 960 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@162 961 case c of
adamc@162 962 NONE => S.return2 (x, n, c)
adamc@162 963 | SOME c =>
adamc@162 964 S.map2 (mfc ctx c,
adamc@162 965 fn c' => (x, n, SOME c'))) xncs,
adamc@162 966 fn xncs' =>
adamc@191 967 (DDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
adamc@123 968 | DVal vi =>
adamc@123 969 S.map2 (mfvi ctx vi,
adamc@123 970 fn vi' =>
adamc@123 971 (DVal vi', loc))
adamc@123 972 | DValRec vis =>
adamc@123 973 S.map2 (ListUtil.mapfold (mfvi ctx) vis,
adamc@123 974 fn vis' =>
adamc@123 975 (DValRec vis', loc))
adamc@76 976 | DSgn (x, n, sgn) =>
adamc@76 977 S.map2 (mfsg ctx sgn,
adamc@76 978 fn sgn' =>
adamc@76 979 (DSgn (x, n, sgn'), loc))
adamc@76 980 | DStr (x, n, sgn, str) =>
adamc@76 981 S.bind2 (mfsg ctx sgn,
adamc@76 982 fn sgn' =>
adamc@76 983 S.map2 (mfst ctx str,
adamc@76 984 fn str' =>
adamc@76 985 (DStr (x, n, sgn', str'), loc)))
adamc@76 986 | DFfiStr (x, n, sgn) =>
adamc@76 987 S.map2 (mfsg ctx sgn,
adamc@76 988 fn sgn' =>
adamc@76 989 (DFfiStr (x, n, sgn'), loc))
adamc@88 990 | DConstraint (c1, c2) =>
adamc@88 991 S.bind2 (mfc ctx c1,
adamc@88 992 fn c1' =>
adamc@88 993 S.map2 (mfc ctx c2,
adamc@88 994 fn c2' =>
adamc@88 995 (DConstraint (c1', c2'), loc)))
adamc@109 996 | DExport (en, sgn, str) =>
adamc@109 997 S.bind2 (mfsg ctx sgn,
adamc@109 998 fn sgn' =>
adamc@109 999 S.map2 (mfst ctx str,
adamc@109 1000 fn str' =>
adamc@109 1001 (DExport (en, sgn', str'), loc)))
adamc@123 1002
adamc@707 1003 | DTable (tn, x, n, c, pe, pc, ce, cc) =>
adamc@704 1004 S.bind2 (mfc ctx c,
adamc@203 1005 fn c' =>
adamc@707 1006 S.bind2 (mfe ctx pe,
adamc@707 1007 fn pe' =>
adamc@707 1008 S.bind2 (mfc ctx pc,
adamc@707 1009 fn pc' =>
adamc@707 1010 S.bind2 (mfe ctx ce,
adamc@707 1011 fn ce' =>
adamc@707 1012 S.map2 (mfc ctx cc,
adamc@707 1013 fn cc' =>
adamc@707 1014 (DTable (tn, x, n, c', pe', pc', ce', cc'), loc))))))
adamc@338 1015 | DSequence _ => S.return2 dAll
adamc@754 1016 | DView (tn, x, n, e, c) =>
adamc@754 1017 S.bind2 (mfe ctx e,
adamc@754 1018 fn e' =>
adamc@754 1019 S.map2 (mfc ctx c,
adamc@754 1020 fn c' =>
adamc@754 1021 (DView (tn, x, n, e', c'), loc)))
adamc@203 1022
adamc@563 1023 | DClass (x, n, k, c) =>
adamc@623 1024 S.bind2 (mfk ctx k,
adamc@563 1025 fn k' =>
adamc@563 1026 S.map2 (mfc ctx c,
adamc@563 1027 fn c' =>
adamc@563 1028 (DClass (x, n, k', c'), loc)))
adamc@213 1029
adamc@338 1030 | DDatabase _ => S.return2 dAll
adamc@271 1031
adamc@459 1032 | DCookie (tn, x, n, c) =>
adamc@459 1033 S.map2 (mfc ctx c,
adamc@459 1034 fn c' =>
adamc@459 1035 (DCookie (tn, x, n, c'), loc))
adamc@720 1036 | DStyle _ => S.return2 dAll
adamc@1075 1037 | DTask (e1, e2) =>
adamc@1075 1038 S.bind2 (mfe ctx e1,
adamc@1075 1039 fn e1' =>
adamc@1075 1040 S.map2 (mfe ctx e2,
adamc@1075 1041 fn e2' =>
adamc@1075 1042 (DTask (e1', e2'), loc)))
adamc@1199 1043 | DPolicy e1 =>
adamc@1199 1044 S.map2 (mfe ctx e1,
adamc@1199 1045 fn e1' =>
adamc@1199 1046 (DPolicy e1', loc))
adam@1294 1047 | DOnError _ => S.return2 dAll
adamc@459 1048
adamc@123 1049 and mfvi ctx (x, n, c, e) =
adamc@123 1050 S.bind2 (mfc ctx c,
adamc@123 1051 fn c' =>
adamc@123 1052 S.map2 (mfe ctx e,
adamc@123 1053 fn e' =>
adamc@123 1054 (x, n, c', e')))
adamc@76 1055 in
adamc@76 1056 mfd
adamc@76 1057 end
adamc@76 1058
adamc@76 1059 fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} =
adamc@623 1060 mapfoldB {kind = fn () => kind,
adamc@76 1061 con = fn () => con,
adamc@76 1062 exp = fn () => exp,
adamc@76 1063 sgn_item = fn () => sgn_item,
adamc@76 1064 sgn = fn () => sgn,
adamc@76 1065 str = fn () => str,
adamc@76 1066 decl = fn () => decl,
adamc@76 1067 bind = fn ((), _) => ()} ()
adamc@76 1068
adamc@76 1069 fun exists {kind, con, exp, sgn_item, sgn, str, decl} k =
adamc@76 1070 case mapfold {kind = fn k => fn () =>
adamc@76 1071 if kind k then
adamc@76 1072 S.Return ()
adamc@76 1073 else
adamc@76 1074 S.Continue (k, ()),
adamc@76 1075 con = fn c => fn () =>
adamc@76 1076 if con c then
adamc@76 1077 S.Return ()
adamc@76 1078 else
adamc@76 1079 S.Continue (c, ()),
adamc@76 1080 exp = fn e => fn () =>
adamc@76 1081 if exp e then
adamc@76 1082 S.Return ()
adamc@76 1083 else
adamc@76 1084 S.Continue (e, ()),
adamc@76 1085 sgn_item = fn sgi => fn () =>
adamc@76 1086 if sgn_item sgi then
adamc@76 1087 S.Return ()
adamc@76 1088 else
adamc@76 1089 S.Continue (sgi, ()),
adamc@76 1090 sgn = fn x => fn () =>
adamc@76 1091 if sgn x then
adamc@76 1092 S.Return ()
adamc@76 1093 else
adamc@76 1094 S.Continue (x, ()),
adamc@76 1095 str = fn x => fn () =>
adamc@76 1096 if str x then
adamc@76 1097 S.Return ()
adamc@76 1098 else
adamc@76 1099 S.Continue (x, ()),
adamc@76 1100 decl = fn x => fn () =>
adamc@76 1101 if decl x then
adamc@76 1102 S.Return ()
adamc@76 1103 else
adamc@76 1104 S.Continue (x, ())} k () of
adamc@76 1105 S.Return _ => true
adamc@76 1106 | S.Continue _ => false
adamc@76 1107
adamc@76 1108 fun search {kind, con, exp, sgn_item, sgn, str, decl} k =
adamc@76 1109 case mapfold {kind = fn x => fn () =>
adamc@76 1110 case kind x of
adamc@76 1111 NONE => S.Continue (x, ())
adamc@76 1112 | SOME v => S.Return v,
adamc@76 1113
adamc@76 1114 con = fn x => fn () =>
adamc@76 1115 case con x of
adamc@76 1116 NONE => S.Continue (x, ())
adamc@76 1117 | SOME v => S.Return v,
adamc@76 1118
adamc@76 1119 exp = fn x => fn () =>
adamc@76 1120 case exp x of
adamc@76 1121 NONE => S.Continue (x, ())
adamc@76 1122 | SOME v => S.Return v,
adamc@76 1123
adamc@76 1124 sgn_item = fn x => fn () =>
adamc@76 1125 case sgn_item x of
adamc@76 1126 NONE => S.Continue (x, ())
adamc@76 1127 | SOME v => S.Return v,
adamc@76 1128
adamc@76 1129 sgn = fn x => fn () =>
adamc@76 1130 case sgn x of
adamc@76 1131 NONE => S.Continue (x, ())
adamc@76 1132 | SOME v => S.Return v,
adamc@76 1133
adamc@76 1134 str = fn x => fn () =>
adamc@76 1135 case str x of
adamc@76 1136 NONE => S.Continue (x, ())
adamc@76 1137 | SOME v => S.Return v,
adamc@76 1138
adamc@76 1139 decl = fn x => fn () =>
adamc@76 1140 case decl x of
adamc@76 1141 NONE => S.Continue (x, ())
adamc@76 1142 | SOME v => S.Return v
adamc@76 1143
adamc@76 1144 } k () of
adamc@76 1145 S.Return x => SOME x
adamc@76 1146 | S.Continue _ => NONE
adamc@76 1147
adamc@448 1148 fun foldMapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx st d =
adamc@623 1149 case mapfoldB {kind = fn ctx => fn x => fn st => S.Continue (kind (ctx, x, st)),
adamc@448 1150 con = fn ctx => fn x => fn st => S.Continue (con (ctx, x, st)),
adamc@448 1151 exp = fn ctx => fn x => fn st => S.Continue (exp (ctx, x, st)),
adamc@448 1152 sgn_item = fn ctx => fn x => fn st => S.Continue (sgn_item (ctx, x, st)),
adamc@448 1153 sgn = fn ctx => fn x => fn st => S.Continue (sgn (ctx, x, st)),
adamc@448 1154 str = fn ctx => fn x => fn st => S.Continue (str (ctx, x, st)),
adamc@448 1155 decl = fn ctx => fn x => fn st => S.Continue (decl (ctx, x, st)),
adamc@448 1156 bind = bind} ctx d st of
adamc@448 1157 S.Continue x => x
adamc@448 1158 | S.Return _ => raise Fail "ElabUtil.Decl.foldMapB: Impossible"
adamc@448 1159
adam@1345 1160 fun map {kind, con, exp, sgn_item, sgn, str, decl} s =
adam@1345 1161 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adam@1345 1162 con = fn c => fn () => S.Continue (con c, ()),
adam@1345 1163 exp = fn e => fn () => S.Continue (exp e, ()),
adam@1345 1164 sgn_item = fn si => fn () => S.Continue (sgn_item si, ()),
adam@1345 1165 sgn = fn s => fn () => S.Continue (sgn s, ()),
adam@1345 1166 str = fn si => fn () => S.Continue (str si, ()),
adam@1345 1167 decl = fn s => fn () => S.Continue (decl s, ())} s () of
adam@1345 1168 S.Return () => raise Fail "Elab_util.Decl.map"
adam@1345 1169 | S.Continue (s, ()) => s
adam@1345 1170
adam@1345 1171 fun mapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx s =
adam@1345 1172 case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()),
adam@1345 1173 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adam@1345 1174 exp = fn ctx => fn c => fn () => S.Continue (exp ctx c, ()),
adam@1345 1175 sgn_item = fn ctx => fn sgi => fn () => S.Continue (sgn_item ctx sgi, ()),
adam@1345 1176 sgn = fn ctx => fn s => fn () => S.Continue (sgn ctx s, ()),
adam@1345 1177 str = fn ctx => fn sgi => fn () => S.Continue (str ctx sgi, ()),
adam@1345 1178 decl = fn ctx => fn s => fn () => S.Continue (decl ctx s, ()),
adam@1345 1179 bind = bind} ctx s () of
adam@1345 1180 S.Continue (s, ()) => s
adam@1345 1181 | S.Return _ => raise Fail "ElabUtil.Decl.mapB: Impossible"
adam@1345 1182
adam@1732 1183 fun fold {kind, con, exp, sgn_item, sgn, str, decl} (st : 'a) d : 'a =
adam@1732 1184 case mapfold {kind = fn k => fn st => S.Continue (k, kind (k, st)),
adam@1732 1185 con = fn c => fn st => S.Continue (c, con (c, st)),
adam@1732 1186 exp = fn e => fn st => S.Continue (e, exp (e, st)),
adam@1732 1187 sgn_item = fn sgi => fn st => S.Continue (sgi, sgn_item (sgi, st)),
adam@1732 1188 sgn = fn s => fn st => S.Continue (s, sgn (s, st)),
adam@1732 1189 str = fn str' => fn st => S.Continue (str', str (str', st)),
adam@1732 1190 decl = fn d => fn st => S.Continue (d, decl (d, st))} d st of
adam@1732 1191 S.Continue (_, st) => st
adam@1732 1192 | S.Return _ => raise Fail "ElabUtil.Decl.fold: Impossible"
adam@1732 1193
adamc@448 1194 end
adamc@448 1195
adamc@448 1196 structure File = struct
adamc@448 1197
adamc@448 1198 fun maxName ds = foldl (fn (d, count) => Int.max (maxNameDecl d, count)) 0 ds
adamc@448 1199
adamc@448 1200 and maxNameDecl (d, _) =
adamc@448 1201 case d of
adamc@448 1202 DCon (_, n, _, _) => n
adamc@805 1203 | DDatatype dts =>
adamc@805 1204 foldl (fn ((_, n, _, ns), max) =>
adamc@448 1205 foldl (fn ((_, n', _), m) => Int.max (n', m))
adamc@805 1206 (Int.max (n, max)) ns) 0 dts
adamc@448 1207 | DDatatypeImp (_, n1, n2, _, _, _, ns) =>
adamc@448 1208 foldl (fn ((_, n', _), m) => Int.max (n', m))
adamc@448 1209 (Int.max (n1, n2)) ns
adamc@448 1210 | DVal (_, n, _, _) => n
adamc@448 1211 | DValRec vis => foldl (fn ((_, n, _, _), count) => Int.max (n, count)) 0 vis
adamc@448 1212 | DStr (_, n, sgn, str) => Int.max (n, Int.max (maxNameSgn sgn, maxNameStr str))
adamc@448 1213 | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
adamc@448 1214 | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
adamc@448 1215 | DConstraint _ => 0
adamc@563 1216 | DClass (_, n, _, _) => n
adamc@448 1217 | DExport _ => 0
adamc@707 1218 | DTable (n1, _, n2, _, _, _, _, _) => Int.max (n1, n2)
adamc@459 1219 | DSequence (n1, _, n2) => Int.max (n1, n2)
adamc@754 1220 | DView (n1, _, n2, _, _) => Int.max (n1, n2)
adamc@448 1221 | DDatabase _ => 0
adamc@459 1222 | DCookie (n1, _, n2, _) => Int.max (n1, n2)
adamc@720 1223 | DStyle (n1, _, n2) => Int.max (n1, n2)
adamc@1075 1224 | DTask _ => 0
adamc@1199 1225 | DPolicy _ => 0
adam@1294 1226 | DOnError _ => 0
adamc@448 1227 and maxNameStr (str, _) =
adamc@448 1228 case str of
adamc@448 1229 StrConst ds => maxName ds
adamc@448 1230 | StrVar n => n
adamc@448 1231 | StrProj (str, _) => maxNameStr str
adamc@448 1232 | StrFun (_, n, dom, ran, str) => foldl Int.max n [maxNameSgn dom, maxNameSgn ran, maxNameStr str]
adamc@448 1233 | StrApp (str1, str2) => Int.max (maxNameStr str1, maxNameStr str2)
adamc@448 1234 | StrError => 0
adamc@448 1235
adamc@448 1236 and maxNameSgn (sgn, _) =
adamc@448 1237 case sgn of
adamc@448 1238 SgnConst sgis => foldl (fn (sgi, count) => Int.max (maxNameSgi sgi, count)) 0 sgis
adamc@448 1239 | SgnVar n => n
adamc@448 1240 | SgnFun (_, n, dom, ran) => Int.max (n, Int.max (maxNameSgn dom, maxNameSgn ran))
adamc@448 1241 | SgnWhere (sgn, _, _) => maxNameSgn sgn
adamc@448 1242 | SgnProj (n, _, _) => n
adamc@448 1243 | SgnError => 0
adamc@448 1244
adamc@448 1245 and maxNameSgi (sgi, _) =
adamc@448 1246 case sgi of
adamc@448 1247 SgiConAbs (_, n, _) => n
adamc@448 1248 | SgiCon (_, n, _, _) => n
adamc@805 1249 | SgiDatatype dts =>
adamc@805 1250 foldl (fn ((_, n, _, ns), max) =>
adamc@805 1251 foldl (fn ((_, n', _), m) => Int.max (n', m))
adamc@805 1252 (Int.max (n, max)) ns) 0 dts
adamc@448 1253 | SgiDatatypeImp (_, n1, n2, _, _, _, ns) =>
adamc@448 1254 foldl (fn ((_, n', _), m) => Int.max (n', m))
adamc@448 1255 (Int.max (n1, n2)) ns
adamc@448 1256 | SgiVal (_, n, _) => n
adamc@448 1257 | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn)
adamc@448 1258 | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn)
adamc@448 1259 | SgiConstraint _ => 0
adamc@563 1260 | SgiClassAbs (_, n, _) => n
adamc@563 1261 | SgiClass (_, n, _, _) => n
adam@1584 1262
adam@1584 1263 fun findDecl pred file =
adam@1584 1264 let
adam@1584 1265 fun decl d =
adam@1584 1266 let
adam@1584 1267 val r = case #1 d of
adam@1584 1268 DStr (_, _, _, s) => str s
adam@1584 1269 | _ => NONE
adam@1584 1270 in
adam@1584 1271 case r of
adam@1584 1272 NONE => if pred d then SOME d else NONE
adam@1584 1273 | _ => r
adam@1584 1274 end
adam@1584 1275
adam@1584 1276 and str s =
adam@1584 1277 case #1 s of
adam@1584 1278 StrConst ds => ListUtil.search decl ds
adam@1584 1279 | StrFun (_, _, _, _, s) => str s
adam@1584 1280 | StrApp (s1, s2) =>
adam@1584 1281 (case str s1 of
adam@1584 1282 NONE => str s2
adam@1584 1283 | r => r)
adam@1584 1284 | _ => NONE
adam@1584 1285 in
adam@1584 1286 ListUtil.search decl file
adam@1584 1287 end
adamc@448 1288
adamc@34 1289 end
adamc@76 1290
adamc@76 1291 end