Mercurial > urweb

annotate src/elab_util.sml @ 223:bbe5899a9585

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Queries back to working as well as before, after start of refactoring to support grouping
author Adam Chlipala <adamc@hcoop.net>
date Thu, 21 Aug 2008 12:49:29 -0400
parents 0343557355fc
children 19e5791923d0
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@6 46 fun mapfold f =
adamc@2 47 let
adamc@2 48 fun mfk k acc =
adamc@2 49 S.bindP (mfk' k acc, f)
adamc@2 50
adamc@2 51 and mfk' (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@2 56 S.bind2 (mfk k1,
adamc@2 57 fn k1' =>
adamc@2 58 S.map2 (mfk 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@2 65 S.map2 (mfk 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@207 72 S.map2 (ListUtil.mapfold mfk 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@76 78 | KUnif (_, _, ref (SOME k)) => mfk' k
adamc@2 79 | KUnif _ => S.return2 kAll
adamc@2 80 in
adamc@2 81 mfk
adamc@2 82 end
adamc@2 83
adamc@2 84 fun exists f k =
adamc@6 85 case mapfold (fn k => fn () =>
adamc@6 86 if f k then
adamc@6 87 S.Return ()
adamc@6 88 else
adamc@6 89 S.Continue (k, ())) k () of
adamc@6 90 S.Return _ => true
adamc@6 91 | S.Continue _ => false
adamc@6 92
adamc@6 93 end
adamc@6 94
adamc@6 95 structure Con = struct
adamc@6 96
adamc@11 97 datatype binder =
adamc@11 98 Rel of string * Elab.kind
adamc@11 99 | Named of string * Elab.kind
adamc@11 100
adamc@11 101 fun mapfoldB {kind = fk, con = fc, bind} =
adamc@6 102 let
adamc@6 103 val mfk = Kind.mapfold fk
adamc@6 104
adamc@11 105 fun mfc ctx c acc =
adamc@11 106 S.bindP (mfc' ctx c acc, fc ctx)
adamc@6 107
adamc@11 108 and mfc' ctx (cAll as (c, loc)) =
adamc@6 109 case c of
adamc@6 110 TFun (c1, c2) =>
adamc@11 111 S.bind2 (mfc ctx c1,
adamc@6 112 fn c1' =>
adamc@11 113 S.map2 (mfc ctx c2,
adamc@6 114 fn c2' =>
adamc@6 115 (TFun (c1', c2'), loc)))
adamc@6 116 | TCFun (e, x, k, c) =>
adamc@6 117 S.bind2 (mfk k,
adamc@6 118 fn k' =>
adamc@11 119 S.map2 (mfc (bind (ctx, Rel (x, k))) c,
adamc@6 120 fn c' =>
adamc@6 121 (TCFun (e, x, k', c'), loc)))
adamc@85 122 | TDisjoint (c1, c2, c3) =>
adamc@85 123 S.bind2 (mfc ctx c1,
adamc@85 124 fn c1' =>
adamc@85 125 S.bind2 (mfc ctx c2,
adamc@85 126 fn c2' =>
adamc@85 127 S.map2 (mfc ctx c3,
adamc@85 128 fn c3' =>
adamc@85 129 (TDisjoint (c1', c2', c3'), loc))))
adamc@6 130 | TRecord c =>
adamc@11 131 S.map2 (mfc ctx c,
adamc@6 132 fn c' =>
adamc@6 133 (TRecord c', loc))
adamc@6 134
adamc@6 135 | CRel _ => S.return2 cAll
adamc@6 136 | CNamed _ => S.return2 cAll
adamc@34 137 | CModProj _ => S.return2 cAll
adamc@6 138 | CApp (c1, c2) =>
adamc@11 139 S.bind2 (mfc ctx c1,
adamc@6 140 fn c1' =>
adamc@11 141 S.map2 (mfc ctx c2,
adamc@6 142 fn c2' =>
adamc@6 143 (CApp (c1', c2'), loc)))
adamc@8 144 | CAbs (x, k, c) =>
adamc@6 145 S.bind2 (mfk k,
adamc@6 146 fn k' =>
adamc@11 147 S.map2 (mfc (bind (ctx, Rel (x, k))) c,
adamc@6 148 fn c' =>
adamc@8 149 (CAbs (x, k', c'), loc)))
adamc@84 150 | CDisjoint (c1, c2, c3) =>
adamc@84 151 S.bind2 (mfc ctx c1,
adamc@84 152 fn c1' =>
adamc@84 153 S.bind2 (mfc ctx c2,
adamc@84 154 fn c2' =>
adamc@84 155 S.map2 (mfc ctx c3,
adamc@84 156 fn c3' =>
adamc@84 157 (CDisjoint (c1', c2', c3'), loc))))
adamc@6 158
adamc@6 159 | CName _ => S.return2 cAll
adamc@6 160
adamc@6 161 | CRecord (k, xcs) =>
adamc@6 162 S.bind2 (mfk k,
adamc@6 163 fn k' =>
adamc@6 164 S.map2 (ListUtil.mapfold (fn (x, c) =>
adamc@11 165 S.bind2 (mfc ctx x,
adamc@6 166 fn x' =>
adamc@11 167 S.map2 (mfc ctx c,
adamc@6 168 fn c' =>
adamc@6 169 (x', c'))))
adamc@6 170 xcs,
adamc@6 171 fn xcs' =>
adamc@6 172 (CRecord (k', xcs'), loc)))
adamc@6 173 | CConcat (c1, c2) =>
adamc@11 174 S.bind2 (mfc ctx c1,
adamc@6 175 fn c1' =>
adamc@11 176 S.map2 (mfc ctx c2,
adamc@6 177 fn c2' =>
adamc@6 178 (CConcat (c1', c2'), loc)))
adamc@67 179 | CFold (k1, k2) =>
adamc@67 180 S.bind2 (mfk k1,
adamc@67 181 fn k1' =>
adamc@67 182 S.map2 (mfk k2,
adamc@67 183 fn k2' =>
adamc@67 184 (CFold (k1', k2'), loc)))
adamc@6 185
adamc@82 186 | CUnit => S.return2 cAll
adamc@82 187
adamc@207 188 | CTuple cs =>
adamc@207 189 S.map2 (ListUtil.mapfold (mfc ctx) cs,
adamc@207 190 fn cs' =>
adamc@207 191 (CTuple cs', loc))
adamc@207 192
adamc@207 193 | CProj (c, n) =>
adamc@207 194 S.map2 (mfc ctx c,
adamc@207 195 fn c' =>
adamc@207 196 (CProj (c', n), loc))
adamc@207 197
adamc@6 198 | CError => S.return2 cAll
adamc@76 199 | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c
adamc@6 200 | CUnif _ => S.return2 cAll
adamc@6 201 in
adamc@6 202 mfc
adamc@6 203 end
adamc@6 204
adamc@11 205 fun mapfold {kind = fk, con = fc} =
adamc@11 206 mapfoldB {kind = fk,
adamc@11 207 con = fn () => fc,
adamc@11 208 bind = fn ((), _) => ()} ()
adamc@11 209
adamc@11 210 fun mapB {kind, con, bind} ctx c =
adamc@11 211 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@11 212 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@11 213 bind = bind} ctx c () of
adamc@11 214 S.Continue (c, ()) => c
adamc@34 215 | S.Return _ => raise Fail "ElabUtil.Con.mapB: Impossible"
adamc@34 216
adamc@34 217 fun map {kind, con} s =
adamc@34 218 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@34 219 con = fn c => fn () => S.Continue (con c, ())} s () of
adamc@34 220 S.Return () => raise Fail "ElabUtil.Con.map: Impossible"
adamc@34 221 | S.Continue (s, ()) => s
adamc@11 222
adamc@6 223 fun exists {kind, con} k =
adamc@6 224 case mapfold {kind = fn k => fn () =>
adamc@6 225 if kind k then
adamc@6 226 S.Return ()
adamc@6 227 else
adamc@6 228 S.Continue (k, ()),
adamc@6 229 con = fn c => fn () =>
adamc@6 230 if con c then
adamc@6 231 S.Return ()
adamc@6 232 else
adamc@6 233 S.Continue (c, ())} k () of
adamc@2 234 S.Return _ => true
adamc@2 235 | S.Continue _ => false
adamc@2 236
adamc@2 237 end
adamc@2 238
adamc@10 239 structure Exp = struct
adamc@10 240
adamc@11 241 datatype binder =
adamc@11 242 RelC of string * Elab.kind
adamc@11 243 | NamedC of string * Elab.kind
adamc@11 244 | RelE of string * Elab.con
adamc@11 245 | NamedE of string * Elab.con
adamc@11 246
adamc@11 247 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
adamc@10 248 let
adamc@10 249 val mfk = Kind.mapfold fk
adamc@10 250
adamc@11 251 fun bind' (ctx, b) =
adamc@11 252 let
adamc@11 253 val b' = case b of
adamc@11 254 Con.Rel x => RelC x
adamc@11 255 | Con.Named x => NamedC x
adamc@11 256 in
adamc@11 257 bind (ctx, b')
adamc@11 258 end
adamc@11 259 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@10 260
adamc@11 261 fun mfe ctx e acc =
adamc@11 262 S.bindP (mfe' ctx e acc, fe ctx)
adamc@11 263
adamc@11 264 and mfe' ctx (eAll as (e, loc)) =
adamc@10 265 case e of
adamc@14 266 EPrim _ => S.return2 eAll
adamc@14 267 | ERel _ => S.return2 eAll
adamc@10 268 | ENamed _ => S.return2 eAll
adamc@34 269 | EModProj _ => S.return2 eAll
adamc@10 270 | EApp (e1, e2) =>
adamc@11 271 S.bind2 (mfe ctx e1,
adamc@10 272 fn e1' =>
adamc@11 273 S.map2 (mfe ctx e2,
adamc@10 274 fn e2' =>
adamc@10 275 (EApp (e1', e2'), loc)))
adamc@26 276 | EAbs (x, dom, ran, e) =>
adamc@26 277 S.bind2 (mfc ctx dom,
adamc@26 278 fn dom' =>
adamc@26 279 S.bind2 (mfc ctx ran,
adamc@26 280 fn ran' =>
adamc@26 281 S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
adamc@26 282 fn e' =>
adamc@26 283 (EAbs (x, dom', ran', e'), loc))))
adamc@26 284
adamc@10 285 | ECApp (e, c) =>
adamc@11 286 S.bind2 (mfe ctx e,
adamc@10 287 fn e' =>
adamc@11 288 S.map2 (mfc ctx c,
adamc@10 289 fn c' =>
adamc@10 290 (ECApp (e', c'), loc)))
adamc@10 291 | ECAbs (expl, x, k, e) =>
adamc@10 292 S.bind2 (mfk k,
adamc@10 293 fn k' =>
adamc@11 294 S.map2 (mfe (bind (ctx, RelC (x, k))) e,
adamc@10 295 fn e' =>
adamc@10 296 (ECAbs (expl, x, k', e'), loc)))
adamc@10 297
adamc@12 298 | ERecord xes =>
adamc@29 299 S.map2 (ListUtil.mapfold (fn (x, e, t) =>
adamc@12 300 S.bind2 (mfc ctx x,
adamc@12 301 fn x' =>
adamc@29 302 S.bind2 (mfe ctx e,
adamc@12 303 fn e' =>
adamc@29 304 S.map2 (mfc ctx t,
adamc@29 305 fn t' =>
adamc@29 306 (x', e', t')))))
adamc@12 307 xes,
adamc@12 308 fn xes' =>
adamc@12 309 (ERecord xes', loc))
adamc@12 310 | EField (e, c, {field, rest}) =>
adamc@12 311 S.bind2 (mfe ctx e,
adamc@12 312 fn e' =>
adamc@12 313 S.bind2 (mfc ctx c,
adamc@12 314 fn c' =>
adamc@12 315 S.bind2 (mfc ctx field,
adamc@12 316 fn field' =>
adamc@12 317 S.map2 (mfc ctx rest,
adamc@12 318 fn rest' =>
adamc@12 319 (EField (e', c', {field = field', rest = rest'}), loc)))))
adamc@149 320 | ECut (e, c, {field, rest}) =>
adamc@149 321 S.bind2 (mfe ctx e,
adamc@149 322 fn e' =>
adamc@149 323 S.bind2 (mfc ctx c,
adamc@149 324 fn c' =>
adamc@149 325 S.bind2 (mfc ctx field,
adamc@149 326 fn field' =>
adamc@149 327 S.map2 (mfc ctx rest,
adamc@149 328 fn rest' =>
adamc@149 329 (ECut (e', c', {field = field', rest = rest'}), loc)))))
adamc@12 330
adamc@71 331 | EFold k =>
adamc@71 332 S.map2 (mfk k,
adamc@71 333 fn k' =>
adamc@71 334 (EFold k', loc))
adamc@71 335
adamc@182 336 | ECase (e, pes, {disc, result}) =>
adamc@171 337 S.bind2 (mfe ctx e,
adamc@171 338 fn e' =>
adamc@171 339 S.bind2 (ListUtil.mapfold (fn (p, e) =>
adamc@171 340 S.map2 (mfe ctx e,
adamc@171 341 fn e' => (p, e'))) pes,
adamc@171 342 fn pes' =>
adamc@182 343 S.bind2 (mfc ctx disc,
adamc@182 344 fn disc' =>
adamc@182 345 S.map2 (mfc ctx result,
adamc@182 346 fn result' =>
adamc@182 347 (ECase (e', pes', {disc = disc', result = result'}), loc)))))
adamc@171 348
adamc@10 349 | EError => S.return2 eAll
adamc@10 350 in
adamc@10 351 mfe
adamc@10 352 end
adamc@10 353
adamc@11 354 fun mapfold {kind = fk, con = fc, exp = fe} =
adamc@11 355 mapfoldB {kind = fk,
adamc@11 356 con = fn () => fc,
adamc@11 357 exp = fn () => fe,
adamc@11 358 bind = fn ((), _) => ()} ()
adamc@11 359
adamc@10 360 fun exists {kind, con, exp} k =
adamc@10 361 case mapfold {kind = fn k => fn () =>
adamc@10 362 if kind k then
adamc@10 363 S.Return ()
adamc@10 364 else
adamc@10 365 S.Continue (k, ()),
adamc@10 366 con = fn c => fn () =>
adamc@10 367 if con c then
adamc@10 368 S.Return ()
adamc@10 369 else
adamc@10 370 S.Continue (c, ()),
adamc@10 371 exp = fn e => fn () =>
adamc@10 372 if exp e then
adamc@10 373 S.Return ()
adamc@10 374 else
adamc@10 375 S.Continue (e, ())} k () of
adamc@10 376 S.Return _ => true
adamc@10 377 | S.Continue _ => false
adamc@10 378
adamc@211 379 fun mapB {kind, con, exp, bind} ctx e =
adamc@211 380 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@211 381 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@211 382 exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
adamc@211 383 bind = bind} ctx e () of
adamc@211 384 S.Continue (e, ()) => e
adamc@211 385 | S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible"
adamc@211 386
adamc@10 387 end
adamc@10 388
adamc@34 389 structure Sgn = struct
adamc@34 390
adamc@34 391 datatype binder =
adamc@34 392 RelC of string * Elab.kind
adamc@34 393 | NamedC of string * Elab.kind
adamc@34 394 | Str of string * Elab.sgn
adamc@59 395 | Sgn of string * Elab.sgn
adamc@34 396
adamc@34 397 fun mapfoldB {kind, con, sgn_item, sgn, bind} =
adamc@34 398 let
adamc@34 399 fun bind' (ctx, b) =
adamc@34 400 let
adamc@34 401 val b' = case b of
adamc@34 402 Con.Rel x => RelC x
adamc@34 403 | Con.Named x => NamedC x
adamc@34 404 in
adamc@34 405 bind (ctx, b')
adamc@34 406 end
adamc@34 407 val con = Con.mapfoldB {kind = kind, con = con, bind = bind'}
adamc@34 408
adamc@34 409 val kind = Kind.mapfold kind
adamc@34 410
adamc@34 411 fun sgi ctx si acc =
adamc@34 412 S.bindP (sgi' ctx si acc, sgn_item ctx)
adamc@34 413
adamc@156 414 and sgi' ctx (siAll as (si, loc)) =
adamc@34 415 case si of
adamc@34 416 SgiConAbs (x, n, k) =>
adamc@34 417 S.map2 (kind k,
adamc@34 418 fn k' =>
adamc@34 419 (SgiConAbs (x, n, k'), loc))
adamc@34 420 | SgiCon (x, n, k, c) =>
adamc@34 421 S.bind2 (kind k,
adamc@34 422 fn k' =>
adamc@34 423 S.map2 (con ctx c,
adamc@34 424 fn c' =>
adamc@34 425 (SgiCon (x, n, k', c'), loc)))
adamc@191 426 | SgiDatatype (x, n, xs, xncs) =>
adamc@156 427 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@156 428 case c of
adamc@156 429 NONE => S.return2 (x, n, c)
adamc@156 430 | SOME c =>
adamc@156 431 S.map2 (con ctx c,
adamc@156 432 fn c' => (x, n, SOME c'))) xncs,
adamc@156 433 fn xncs' =>
adamc@191 434 (SgiDatatype (x, n, xs, xncs'), loc))
adamc@191 435 | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
adamc@162 436 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@162 437 case c of
adamc@162 438 NONE => S.return2 (x, n, c)
adamc@162 439 | SOME c =>
adamc@162 440 S.map2 (con ctx c,
adamc@162 441 fn c' => (x, n, SOME c'))) xncs,
adamc@162 442 fn xncs' =>
adamc@191 443 (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
adamc@34 444 | SgiVal (x, n, c) =>
adamc@34 445 S.map2 (con ctx c,
adamc@34 446 fn c' =>
adamc@34 447 (SgiVal (x, n, c'), loc))
adamc@34 448 | SgiStr (x, n, s) =>
adamc@34 449 S.map2 (sg ctx s,
adamc@34 450 fn s' =>
adamc@34 451 (SgiStr (x, n, s'), loc))
adamc@59 452 | SgiSgn (x, n, s) =>
adamc@59 453 S.map2 (sg ctx s,
adamc@59 454 fn s' =>
adamc@59 455 (SgiSgn (x, n, s'), loc))
adamc@88 456 | SgiConstraint (c1, c2) =>
adamc@88 457 S.bind2 (con ctx c1,
adamc@88 458 fn c1' =>
adamc@88 459 S.map2 (con ctx c2,
adamc@88 460 fn c2' =>
adamc@88 461 (SgiConstraint (c1', c2'), loc)))
adamc@205 462 | SgiTable (tn, x, n, c) =>
adamc@203 463 S.map2 (con ctx c,
adamc@203 464 fn c' =>
adamc@205 465 (SgiTable (tn, x, n, c'), loc))
adamc@211 466 | SgiClassAbs _ => S.return2 siAll
adamc@211 467 | SgiClass (x, n, c) =>
adamc@211 468 S.map2 (con ctx c,
adamc@211 469 fn c' =>
adamc@211 470 (SgiClass (x, n, c'), loc))
adamc@34 471
adamc@34 472 and sg ctx s acc =
adamc@34 473 S.bindP (sg' ctx s acc, sgn ctx)
adamc@34 474
adamc@34 475 and sg' ctx (sAll as (s, loc)) =
adamc@34 476 case s of
adamc@34 477 SgnConst sgis =>
adamc@34 478 S.map2 (ListUtil.mapfoldB (fn (ctx, si) =>
adamc@34 479 (case #1 si of
adamc@34 480 SgiConAbs (x, _, k) =>
adamc@34 481 bind (ctx, NamedC (x, k))
adamc@34 482 | SgiCon (x, _, k, _) =>
adamc@34 483 bind (ctx, NamedC (x, k))
adamc@191 484 | SgiDatatype (x, n, _, xncs) =>
adamc@156 485 bind (ctx, NamedC (x, (KType, loc)))
adamc@191 486 | SgiDatatypeImp (x, _, _, _, _, _, _) =>
adamc@156 487 bind (ctx, NamedC (x, (KType, loc)))
adamc@34 488 | SgiVal _ => ctx
adamc@34 489 | SgiStr (x, _, sgn) =>
adamc@59 490 bind (ctx, Str (x, sgn))
adamc@59 491 | SgiSgn (x, _, sgn) =>
adamc@88 492 bind (ctx, Sgn (x, sgn))
adamc@203 493 | SgiConstraint _ => ctx
adamc@211 494 | SgiTable _ => ctx
adamc@211 495 | SgiClassAbs (x, _) =>
adamc@211 496 bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc)))
adamc@211 497 | SgiClass (x, _, _) =>
adamc@211 498 bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))),
adamc@34 499 sgi ctx si)) ctx sgis,
adamc@34 500 fn sgis' =>
adamc@34 501 (SgnConst sgis', loc))
adamc@34 502
adamc@34 503 | SgnVar _ => S.return2 sAll
adamc@41 504 | SgnFun (m, n, s1, s2) =>
adamc@41 505 S.bind2 (sg ctx s1,
adamc@41 506 fn s1' =>
adamc@41 507 S.map2 (sg (bind (ctx, Str (m, s1'))) s2,
adamc@41 508 fn s2' =>
adamc@41 509 (SgnFun (m, n, s1', s2'), loc)))
adamc@59 510 | SgnProj _ => S.return2 sAll
adamc@42 511 | SgnWhere (sgn, x, c) =>
adamc@42 512 S.bind2 (sg ctx sgn,
adamc@42 513 fn sgn' =>
adamc@42 514 S.map2 (con ctx c,
adamc@42 515 fn c' =>
adamc@42 516 (SgnWhere (sgn', x, c'), loc)))
adamc@34 517 | SgnError => S.return2 sAll
adamc@34 518 in
adamc@34 519 sg
adamc@34 520 end
adamc@34 521
adamc@34 522 fun mapfold {kind, con, sgn_item, sgn} =
adamc@34 523 mapfoldB {kind = kind,
adamc@34 524 con = fn () => con,
adamc@34 525 sgn_item = fn () => sgn_item,
adamc@34 526 sgn = fn () => sgn,
adamc@34 527 bind = fn ((), _) => ()} ()
adamc@34 528
adamc@34 529 fun map {kind, con, sgn_item, sgn} s =
adamc@34 530 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@34 531 con = fn c => fn () => S.Continue (con c, ()),
adamc@34 532 sgn_item = fn si => fn () => S.Continue (sgn_item si, ()),
adamc@34 533 sgn = fn s => fn () => S.Continue (sgn s, ())} s () of
adamc@34 534 S.Return () => raise Fail "Elab_util.Sgn.map"
adamc@34 535 | S.Continue (s, ()) => s
adamc@34 536
adamc@2 537 end
adamc@34 538
adamc@76 539 structure Decl = struct
adamc@76 540
adamc@76 541 datatype binder =
adamc@76 542 RelC of string * Elab.kind
adamc@76 543 | NamedC of string * Elab.kind
adamc@76 544 | RelE of string * Elab.con
adamc@76 545 | NamedE of string * Elab.con
adamc@76 546 | Str of string * Elab.sgn
adamc@76 547 | Sgn of string * Elab.sgn
adamc@76 548
adamc@76 549 fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} =
adamc@76 550 let
adamc@76 551 val mfk = Kind.mapfold fk
adamc@76 552
adamc@76 553 fun bind' (ctx, b) =
adamc@76 554 let
adamc@76 555 val b' = case b of
adamc@76 556 Con.Rel x => RelC x
adamc@76 557 | Con.Named x => NamedC x
adamc@76 558 in
adamc@76 559 bind (ctx, b')
adamc@76 560 end
adamc@76 561 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@76 562
adamc@76 563 fun bind' (ctx, b) =
adamc@76 564 let
adamc@76 565 val b' = case b of
adamc@76 566 Exp.RelC x => RelC x
adamc@76 567 | Exp.NamedC x => NamedC x
adamc@76 568 | Exp.RelE x => RelE x
adamc@76 569 | Exp.NamedE x => NamedE x
adamc@76 570 in
adamc@76 571 bind (ctx, b')
adamc@76 572 end
adamc@76 573 val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind'}
adamc@76 574
adamc@76 575 fun bind' (ctx, b) =
adamc@76 576 let
adamc@76 577 val b' = case b of
adamc@76 578 Sgn.RelC x => RelC x
adamc@76 579 | Sgn.NamedC x => NamedC x
adamc@76 580 | Sgn.Sgn x => Sgn x
adamc@76 581 | Sgn.Str x => Str x
adamc@76 582 in
adamc@76 583 bind (ctx, b')
adamc@76 584 end
adamc@76 585 val mfsg = Sgn.mapfoldB {kind = fk, con = fc, sgn_item = fsgi, sgn = fsg, bind = bind'}
adamc@76 586
adamc@76 587 fun mfst ctx str acc =
adamc@76 588 S.bindP (mfst' ctx str acc, fst ctx)
adamc@76 589
adamc@76 590 and mfst' ctx (strAll as (str, loc)) =
adamc@76 591 case str of
adamc@76 592 StrConst ds =>
adamc@76 593 S.map2 (ListUtil.mapfoldB (fn (ctx, d) =>
adamc@76 594 (case #1 d of
adamc@76 595 DCon (x, _, k, _) =>
adamc@76 596 bind (ctx, NamedC (x, k))
adamc@191 597 | DDatatype (x, n, xs, xncs) =>
adamc@156 598 let
adamc@156 599 val ctx = bind (ctx, NamedC (x, (KType, loc)))
adamc@156 600 in
adamc@156 601 foldl (fn ((x, _, co), ctx) =>
adamc@156 602 let
adamc@156 603 val t =
adamc@156 604 case co of
adamc@156 605 NONE => CNamed n
adamc@156 606 | SOME t => TFun (t, (CNamed n, loc))
adamc@191 607
adamc@191 608 val k = (KType, loc)
adamc@191 609 val t = (t, loc)
adamc@191 610 val t = foldr (fn (x, t) =>
adamc@191 611 (TCFun (Explicit,
adamc@191 612 x,
adamc@191 613 k,
adamc@191 614 t), loc))
adamc@191 615 t xs
adamc@156 616 in
adamc@191 617 bind (ctx, NamedE (x, t))
adamc@156 618 end)
adamc@156 619 ctx xncs
adamc@156 620 end
adamc@191 621 | DDatatypeImp (x, n, m, ms, x', _, _) =>
adamc@156 622 bind (ctx, NamedC (x, (KType, loc)))
adamc@76 623 | DVal (x, _, c, _) =>
adamc@76 624 bind (ctx, NamedE (x, c))
adamc@123 625 | DValRec vis =>
adamc@123 626 foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis
adamc@76 627 | DSgn (x, _, sgn) =>
adamc@76 628 bind (ctx, Sgn (x, sgn))
adamc@76 629 | DStr (x, _, sgn, _) =>
adamc@76 630 bind (ctx, Str (x, sgn))
adamc@76 631 | DFfiStr (x, _, sgn) =>
adamc@88 632 bind (ctx, Str (x, sgn))
adamc@100 633 | DConstraint _ => ctx
adamc@203 634 | DExport _ => ctx
adamc@205 635 | DTable (tn, x, n, c) =>
adamc@205 636 bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "table"), loc),
adamc@213 637 c), loc)))
adamc@213 638 | DClass (x, _, _) =>
adamc@213 639 bind (ctx, NamedC (x, (KArrow ((KType, loc), (KType, loc)), loc))),
adamc@76 640 mfd ctx d)) ctx ds,
adamc@76 641 fn ds' => (StrConst ds', loc))
adamc@76 642 | StrVar _ => S.return2 strAll
adamc@76 643 | StrProj (str, x) =>
adamc@76 644 S.map2 (mfst ctx str,
adamc@76 645 fn str' =>
adamc@76 646 (StrProj (str', x), loc))
adamc@76 647 | StrFun (x, n, sgn1, sgn2, str) =>
adamc@76 648 S.bind2 (mfsg ctx sgn1,
adamc@76 649 fn sgn1' =>
adamc@76 650 S.bind2 (mfsg ctx sgn2,
adamc@76 651 fn sgn2' =>
adamc@76 652 S.map2 (mfst ctx str,
adamc@76 653 fn str' =>
adamc@76 654 (StrFun (x, n, sgn1', sgn2', str'), loc))))
adamc@76 655 | StrApp (str1, str2) =>
adamc@76 656 S.bind2 (mfst ctx str1,
adamc@76 657 fn str1' =>
adamc@76 658 S.map2 (mfst ctx str2,
adamc@76 659 fn str2' =>
adamc@76 660 (StrApp (str1', str2'), loc)))
adamc@76 661 | StrError => S.return2 strAll
adamc@76 662
adamc@76 663 and mfd ctx d acc =
adamc@76 664 S.bindP (mfd' ctx d acc, fd ctx)
adamc@76 665
adamc@76 666 and mfd' ctx (dAll as (d, loc)) =
adamc@76 667 case d of
adamc@76 668 DCon (x, n, k, c) =>
adamc@76 669 S.bind2 (mfk k,
adamc@76 670 fn k' =>
adamc@76 671 S.map2 (mfc ctx c,
adamc@76 672 fn c' =>
adamc@76 673 (DCon (x, n, k', c'), loc)))
adamc@191 674 | DDatatype (x, n, xs, xncs) =>
adamc@156 675 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@156 676 case c of
adamc@156 677 NONE => S.return2 (x, n, c)
adamc@156 678 | SOME c =>
adamc@156 679 S.map2 (mfc ctx c,
adamc@156 680 fn c' => (x, n, SOME c'))) xncs,
adamc@156 681 fn xncs' =>
adamc@191 682 (DDatatype (x, n, xs, xncs'), loc))
adamc@191 683 | DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
adamc@162 684 S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@162 685 case c of
adamc@162 686 NONE => S.return2 (x, n, c)
adamc@162 687 | SOME c =>
adamc@162 688 S.map2 (mfc ctx c,
adamc@162 689 fn c' => (x, n, SOME c'))) xncs,
adamc@162 690 fn xncs' =>
adamc@191 691 (DDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc))
adamc@123 692 | DVal vi =>
adamc@123 693 S.map2 (mfvi ctx vi,
adamc@123 694 fn vi' =>
adamc@123 695 (DVal vi', loc))
adamc@123 696 | DValRec vis =>
adamc@123 697 S.map2 (ListUtil.mapfold (mfvi ctx) vis,
adamc@123 698 fn vis' =>
adamc@123 699 (DValRec vis', loc))
adamc@76 700 | DSgn (x, n, sgn) =>
adamc@76 701 S.map2 (mfsg ctx sgn,
adamc@76 702 fn sgn' =>
adamc@76 703 (DSgn (x, n, sgn'), loc))
adamc@76 704 | DStr (x, n, sgn, str) =>
adamc@76 705 S.bind2 (mfsg ctx sgn,
adamc@76 706 fn sgn' =>
adamc@76 707 S.map2 (mfst ctx str,
adamc@76 708 fn str' =>
adamc@76 709 (DStr (x, n, sgn', str'), loc)))
adamc@76 710 | DFfiStr (x, n, sgn) =>
adamc@76 711 S.map2 (mfsg ctx sgn,
adamc@76 712 fn sgn' =>
adamc@76 713 (DFfiStr (x, n, sgn'), loc))
adamc@88 714 | DConstraint (c1, c2) =>
adamc@88 715 S.bind2 (mfc ctx c1,
adamc@88 716 fn c1' =>
adamc@88 717 S.map2 (mfc ctx c2,
adamc@88 718 fn c2' =>
adamc@88 719 (DConstraint (c1', c2'), loc)))
adamc@109 720 | DExport (en, sgn, str) =>
adamc@109 721 S.bind2 (mfsg ctx sgn,
adamc@109 722 fn sgn' =>
adamc@109 723 S.map2 (mfst ctx str,
adamc@109 724 fn str' =>
adamc@109 725 (DExport (en, sgn', str'), loc)))
adamc@123 726
adamc@205 727 | DTable (tn, x, n, c) =>
adamc@203 728 S.map2 (mfc ctx c,
adamc@203 729 fn c' =>
adamc@205 730 (DTable (tn, x, n, c'), loc))
adamc@203 731
adamc@213 732 | DClass (x, n, c) =>
adamc@213 733 S.map2 (mfc ctx c,
adamc@213 734 fn c' =>
adamc@213 735 (DClass (x, n, c'), loc))
adamc@213 736
adamc@123 737 and mfvi ctx (x, n, c, e) =
adamc@123 738 S.bind2 (mfc ctx c,
adamc@123 739 fn c' =>
adamc@123 740 S.map2 (mfe ctx e,
adamc@123 741 fn e' =>
adamc@123 742 (x, n, c', e')))
adamc@76 743 in
adamc@76 744 mfd
adamc@76 745 end
adamc@76 746
adamc@76 747 fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} =
adamc@76 748 mapfoldB {kind = kind,
adamc@76 749 con = fn () => con,
adamc@76 750 exp = fn () => exp,
adamc@76 751 sgn_item = fn () => sgn_item,
adamc@76 752 sgn = fn () => sgn,
adamc@76 753 str = fn () => str,
adamc@76 754 decl = fn () => decl,
adamc@76 755 bind = fn ((), _) => ()} ()
adamc@76 756
adamc@76 757 fun exists {kind, con, exp, sgn_item, sgn, str, decl} k =
adamc@76 758 case mapfold {kind = fn k => fn () =>
adamc@76 759 if kind k then
adamc@76 760 S.Return ()
adamc@76 761 else
adamc@76 762 S.Continue (k, ()),
adamc@76 763 con = fn c => fn () =>
adamc@76 764 if con c then
adamc@76 765 S.Return ()
adamc@76 766 else
adamc@76 767 S.Continue (c, ()),
adamc@76 768 exp = fn e => fn () =>
adamc@76 769 if exp e then
adamc@76 770 S.Return ()
adamc@76 771 else
adamc@76 772 S.Continue (e, ()),
adamc@76 773 sgn_item = fn sgi => fn () =>
adamc@76 774 if sgn_item sgi then
adamc@76 775 S.Return ()
adamc@76 776 else
adamc@76 777 S.Continue (sgi, ()),
adamc@76 778 sgn = fn x => fn () =>
adamc@76 779 if sgn x then
adamc@76 780 S.Return ()
adamc@76 781 else
adamc@76 782 S.Continue (x, ()),
adamc@76 783 str = fn x => fn () =>
adamc@76 784 if str x then
adamc@76 785 S.Return ()
adamc@76 786 else
adamc@76 787 S.Continue (x, ()),
adamc@76 788 decl = fn x => fn () =>
adamc@76 789 if decl x then
adamc@76 790 S.Return ()
adamc@76 791 else
adamc@76 792 S.Continue (x, ())} k () of
adamc@76 793 S.Return _ => true
adamc@76 794 | S.Continue _ => false
adamc@76 795
adamc@76 796 fun search {kind, con, exp, sgn_item, sgn, str, decl} k =
adamc@76 797 case mapfold {kind = fn x => fn () =>
adamc@76 798 case kind x of
adamc@76 799 NONE => S.Continue (x, ())
adamc@76 800 | SOME v => S.Return v,
adamc@76 801
adamc@76 802 con = fn x => fn () =>
adamc@76 803 case con x of
adamc@76 804 NONE => S.Continue (x, ())
adamc@76 805 | SOME v => S.Return v,
adamc@76 806
adamc@76 807 exp = fn x => fn () =>
adamc@76 808 case exp x of
adamc@76 809 NONE => S.Continue (x, ())
adamc@76 810 | SOME v => S.Return v,
adamc@76 811
adamc@76 812 sgn_item = fn x => fn () =>
adamc@76 813 case sgn_item x of
adamc@76 814 NONE => S.Continue (x, ())
adamc@76 815 | SOME v => S.Return v,
adamc@76 816
adamc@76 817 sgn = fn x => fn () =>
adamc@76 818 case sgn x of
adamc@76 819 NONE => S.Continue (x, ())
adamc@76 820 | SOME v => S.Return v,
adamc@76 821
adamc@76 822 str = fn x => fn () =>
adamc@76 823 case str x of
adamc@76 824 NONE => S.Continue (x, ())
adamc@76 825 | SOME v => S.Return v,
adamc@76 826
adamc@76 827 decl = fn x => fn () =>
adamc@76 828 case decl x of
adamc@76 829 NONE => S.Continue (x, ())
adamc@76 830 | SOME v => S.Return v
adamc@76 831
adamc@76 832 } k () of
adamc@76 833 S.Return x => SOME x
adamc@76 834 | S.Continue _ => NONE
adamc@76 835
adamc@34 836 end
adamc@76 837
adamc@76 838 end