Mercurial > urweb

annotate src/expl_util.sml @ 109:813e5a52063d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove closure conversion in favor of zany fun with modules, which also replaces 'page'
author Adam Chlipala <adamc@hcoop.net>
date Sun, 13 Jul 2008 10:17:06 -0400
parents 275aaeb73f1f
children 7420fa18d657
rev   line source
adamc@38 1 (* Copyright (c) 2008, Adam Chlipala
adamc@38 2 * All rights reserved.
adamc@38 3 *
adamc@38 4 * Redistribution and use in source and binary forms, with or without
adamc@38 5 * modification, are permitted provided that the following conditions are met:
adamc@38 6 *
adamc@38 7 * - Redistributions of source code must retain the above copyright notice,
adamc@38 8 * this list of conditions and the following disclaimer.
adamc@38 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@38 10 * this list of conditions and the following disclaimer in the documentation
adamc@38 11 * and/or other materials provided with the distribution.
adamc@38 12 * - The names of contributors may not be used to endorse or promote products
adamc@38 13 * derived from this software without specific prior written permission.
adamc@38 14 *
adamc@38 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@38 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@38 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@38 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@38 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@38 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@38 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@38 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@38 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@38 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@38 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@38 26 *)
adamc@38 27
adamc@38 28 structure ExplUtil :> EXPL_UTIL = struct
adamc@38 29
adamc@38 30 open Expl
adamc@38 31
adamc@38 32 structure S = Search
adamc@38 33
adamc@38 34 structure Kind = struct
adamc@38 35
adamc@38 36 fun mapfold f =
adamc@38 37 let
adamc@38 38 fun mfk k acc =
adamc@38 39 S.bindP (mfk' k acc, f)
adamc@38 40
adamc@38 41 and mfk' (kAll as (k, loc)) =
adamc@38 42 case k of
adamc@38 43 KType => S.return2 kAll
adamc@38 44
adamc@38 45 | KArrow (k1, k2) =>
adamc@38 46 S.bind2 (mfk k1,
adamc@38 47 fn k1' =>
adamc@38 48 S.map2 (mfk k2,
adamc@38 49 fn k2' =>
adamc@38 50 (KArrow (k1', k2'), loc)))
adamc@38 51
adamc@38 52 | KName => S.return2 kAll
adamc@38 53
adamc@38 54 | KRecord k =>
adamc@38 55 S.map2 (mfk k,
adamc@38 56 fn k' =>
adamc@38 57 (KRecord k', loc))
adamc@87 58
adamc@87 59 | KUnit => S.return2 kAll
adamc@38 60 in
adamc@38 61 mfk
adamc@38 62 end
adamc@38 63
adamc@38 64 fun exists f k =
adamc@38 65 case mapfold (fn k => fn () =>
adamc@38 66 if f k then
adamc@38 67 S.Return ()
adamc@38 68 else
adamc@38 69 S.Continue (k, ())) k () of
adamc@38 70 S.Return _ => true
adamc@38 71 | S.Continue _ => false
adamc@38 72
adamc@38 73 end
adamc@38 74
adamc@38 75 structure Con = struct
adamc@38 76
adamc@38 77 datatype binder =
adamc@38 78 Rel of string * Expl.kind
adamc@38 79 | Named of string * Expl.kind
adamc@38 80
adamc@38 81 fun mapfoldB {kind = fk, con = fc, bind} =
adamc@38 82 let
adamc@38 83 val mfk = Kind.mapfold fk
adamc@38 84
adamc@38 85 fun mfc ctx c acc =
adamc@38 86 S.bindP (mfc' ctx c acc, fc ctx)
adamc@38 87
adamc@38 88 and mfc' ctx (cAll as (c, loc)) =
adamc@38 89 case c of
adamc@38 90 TFun (c1, c2) =>
adamc@38 91 S.bind2 (mfc ctx c1,
adamc@38 92 fn c1' =>
adamc@38 93 S.map2 (mfc ctx c2,
adamc@38 94 fn c2' =>
adamc@38 95 (TFun (c1', c2'), loc)))
adamc@38 96 | TCFun (x, k, c) =>
adamc@38 97 S.bind2 (mfk k,
adamc@38 98 fn k' =>
adamc@38 99 S.map2 (mfc (bind (ctx, Rel (x, k))) c,
adamc@38 100 fn c' =>
adamc@38 101 (TCFun (x, k', c'), loc)))
adamc@38 102 | TRecord c =>
adamc@38 103 S.map2 (mfc ctx c,
adamc@38 104 fn c' =>
adamc@38 105 (TRecord c', loc))
adamc@38 106
adamc@38 107 | CRel _ => S.return2 cAll
adamc@38 108 | CNamed _ => S.return2 cAll
adamc@38 109 | CModProj _ => S.return2 cAll
adamc@38 110 | CApp (c1, c2) =>
adamc@38 111 S.bind2 (mfc ctx c1,
adamc@38 112 fn c1' =>
adamc@38 113 S.map2 (mfc ctx c2,
adamc@38 114 fn c2' =>
adamc@38 115 (CApp (c1', c2'), loc)))
adamc@38 116 | CAbs (x, k, c) =>
adamc@38 117 S.bind2 (mfk k,
adamc@38 118 fn k' =>
adamc@38 119 S.map2 (mfc (bind (ctx, Rel (x, k))) c,
adamc@38 120 fn c' =>
adamc@38 121 (CAbs (x, k', c'), loc)))
adamc@38 122
adamc@38 123 | CName _ => S.return2 cAll
adamc@38 124
adamc@38 125 | CRecord (k, xcs) =>
adamc@38 126 S.bind2 (mfk k,
adamc@38 127 fn k' =>
adamc@38 128 S.map2 (ListUtil.mapfold (fn (x, c) =>
adamc@38 129 S.bind2 (mfc ctx x,
adamc@38 130 fn x' =>
adamc@38 131 S.map2 (mfc ctx c,
adamc@38 132 fn c' =>
adamc@38 133 (x', c'))))
adamc@38 134 xcs,
adamc@38 135 fn xcs' =>
adamc@38 136 (CRecord (k', xcs'), loc)))
adamc@38 137 | CConcat (c1, c2) =>
adamc@38 138 S.bind2 (mfc ctx c1,
adamc@38 139 fn c1' =>
adamc@38 140 S.map2 (mfc ctx c2,
adamc@38 141 fn c2' =>
adamc@38 142 (CConcat (c1', c2'), loc)))
adamc@68 143 | CFold (k1, k2) =>
adamc@68 144 S.bind2 (mfk k1,
adamc@68 145 fn k1' =>
adamc@68 146 S.map2 (mfk k2,
adamc@68 147 fn k2' =>
adamc@68 148 (CFold (k1', k2'), loc)))
adamc@87 149
adamc@87 150 | CUnit => S.return2 cAll
adamc@38 151 in
adamc@38 152 mfc
adamc@38 153 end
adamc@38 154
adamc@38 155 fun mapfold {kind = fk, con = fc} =
adamc@38 156 mapfoldB {kind = fk,
adamc@38 157 con = fn () => fc,
adamc@38 158 bind = fn ((), _) => ()} ()
adamc@38 159
adamc@38 160 fun mapB {kind, con, bind} ctx c =
adamc@38 161 case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@38 162 con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@38 163 bind = bind} ctx c () of
adamc@38 164 S.Continue (c, ()) => c
adamc@38 165 | S.Return _ => raise Fail "ExplUtil.Con.mapB: Impossible"
adamc@38 166
adamc@38 167 fun map {kind, con} s =
adamc@38 168 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@38 169 con = fn c => fn () => S.Continue (con c, ())} s () of
adamc@38 170 S.Return () => raise Fail "ExplUtil.Con.map: Impossible"
adamc@38 171 | S.Continue (s, ()) => s
adamc@38 172
adamc@38 173 fun exists {kind, con} k =
adamc@38 174 case mapfold {kind = fn k => fn () =>
adamc@38 175 if kind k then
adamc@38 176 S.Return ()
adamc@38 177 else
adamc@38 178 S.Continue (k, ()),
adamc@38 179 con = fn c => fn () =>
adamc@38 180 if con c then
adamc@38 181 S.Return ()
adamc@38 182 else
adamc@38 183 S.Continue (c, ())} k () of
adamc@38 184 S.Return _ => true
adamc@38 185 | S.Continue _ => false
adamc@38 186
adamc@38 187 end
adamc@38 188
adamc@38 189 structure Exp = struct
adamc@38 190
adamc@38 191 datatype binder =
adamc@38 192 RelC of string * Expl.kind
adamc@38 193 | NamedC of string * Expl.kind
adamc@38 194 | RelE of string * Expl.con
adamc@38 195 | NamedE of string * Expl.con
adamc@38 196
adamc@38 197 fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
adamc@38 198 let
adamc@38 199 val mfk = Kind.mapfold fk
adamc@38 200
adamc@38 201 fun bind' (ctx, b) =
adamc@38 202 let
adamc@38 203 val b' = case b of
adamc@38 204 Con.Rel x => RelC x
adamc@38 205 | Con.Named x => NamedC x
adamc@38 206 in
adamc@38 207 bind (ctx, b')
adamc@38 208 end
adamc@38 209 val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@38 210
adamc@38 211 fun mfe ctx e acc =
adamc@38 212 S.bindP (mfe' ctx e acc, fe ctx)
adamc@38 213
adamc@38 214 and mfe' ctx (eAll as (e, loc)) =
adamc@38 215 case e of
adamc@38 216 EPrim _ => S.return2 eAll
adamc@38 217 | ERel _ => S.return2 eAll
adamc@38 218 | ENamed _ => S.return2 eAll
adamc@38 219 | EModProj _ => S.return2 eAll
adamc@38 220 | EApp (e1, e2) =>
adamc@38 221 S.bind2 (mfe ctx e1,
adamc@38 222 fn e1' =>
adamc@38 223 S.map2 (mfe ctx e2,
adamc@38 224 fn e2' =>
adamc@38 225 (EApp (e1', e2'), loc)))
adamc@38 226 | EAbs (x, dom, ran, e) =>
adamc@38 227 S.bind2 (mfc ctx dom,
adamc@38 228 fn dom' =>
adamc@38 229 S.bind2 (mfc ctx ran,
adamc@38 230 fn ran' =>
adamc@38 231 S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
adamc@38 232 fn e' =>
adamc@38 233 (EAbs (x, dom', ran', e'), loc))))
adamc@38 234
adamc@38 235 | ECApp (e, c) =>
adamc@38 236 S.bind2 (mfe ctx e,
adamc@38 237 fn e' =>
adamc@38 238 S.map2 (mfc ctx c,
adamc@38 239 fn c' =>
adamc@38 240 (ECApp (e', c'), loc)))
adamc@38 241 | ECAbs (x, k, e) =>
adamc@38 242 S.bind2 (mfk k,
adamc@38 243 fn k' =>
adamc@38 244 S.map2 (mfe (bind (ctx, RelC (x, k))) e,
adamc@38 245 fn e' =>
adamc@38 246 (ECAbs (x, k', e'), loc)))
adamc@38 247
adamc@38 248 | ERecord xes =>
adamc@38 249 S.map2 (ListUtil.mapfold (fn (x, e, t) =>
adamc@38 250 S.bind2 (mfc ctx x,
adamc@38 251 fn x' =>
adamc@38 252 S.bind2 (mfe ctx e,
adamc@38 253 fn e' =>
adamc@38 254 S.map2 (mfc ctx t,
adamc@38 255 fn t' =>
adamc@38 256 (x', e', t')))))
adamc@38 257 xes,
adamc@38 258 fn xes' =>
adamc@38 259 (ERecord xes', loc))
adamc@38 260 | EField (e, c, {field, rest}) =>
adamc@38 261 S.bind2 (mfe ctx e,
adamc@38 262 fn e' =>
adamc@38 263 S.bind2 (mfc ctx c,
adamc@38 264 fn c' =>
adamc@38 265 S.bind2 (mfc ctx field,
adamc@38 266 fn field' =>
adamc@38 267 S.map2 (mfc ctx rest,
adamc@38 268 fn rest' =>
adamc@38 269 (EField (e', c', {field = field', rest = rest'}), loc)))))
adamc@72 270 | EFold k =>
adamc@72 271 S.map2 (mfk k,
adamc@72 272 fn k' =>
adamc@72 273 (EFold k', loc))
adamc@109 274
adamc@109 275 | EWrite e =>
adamc@109 276 S.map2 (mfe ctx e,
adamc@109 277 fn e' =>
adamc@109 278 (EWrite e', loc))
adamc@38 279 in
adamc@38 280 mfe
adamc@38 281 end
adamc@38 282
adamc@38 283 fun mapfold {kind = fk, con = fc, exp = fe} =
adamc@38 284 mapfoldB {kind = fk,
adamc@38 285 con = fn () => fc,
adamc@38 286 exp = fn () => fe,
adamc@38 287 bind = fn ((), _) => ()} ()
adamc@38 288
adamc@38 289 fun exists {kind, con, exp} k =
adamc@38 290 case mapfold {kind = fn k => fn () =>
adamc@38 291 if kind k then
adamc@38 292 S.Return ()
adamc@38 293 else
adamc@38 294 S.Continue (k, ()),
adamc@38 295 con = fn c => fn () =>
adamc@38 296 if con c then
adamc@38 297 S.Return ()
adamc@38 298 else
adamc@38 299 S.Continue (c, ()),
adamc@38 300 exp = fn e => fn () =>
adamc@38 301 if exp e then
adamc@38 302 S.Return ()
adamc@38 303 else
adamc@38 304 S.Continue (e, ())} k () of
adamc@38 305 S.Return _ => true
adamc@38 306 | S.Continue _ => false
adamc@38 307
adamc@38 308 end
adamc@38 309
adamc@38 310 structure Sgn = struct
adamc@38 311
adamc@38 312 datatype binder =
adamc@38 313 RelC of string * Expl.kind
adamc@38 314 | NamedC of string * Expl.kind
adamc@38 315 | Str of string * Expl.sgn
adamc@64 316 | Sgn of string * Expl.sgn
adamc@38 317
adamc@38 318 fun mapfoldB {kind, con, sgn_item, sgn, bind} =
adamc@38 319 let
adamc@38 320 fun bind' (ctx, b) =
adamc@38 321 let
adamc@38 322 val b' = case b of
adamc@38 323 Con.Rel x => RelC x
adamc@38 324 | Con.Named x => NamedC x
adamc@38 325 in
adamc@38 326 bind (ctx, b')
adamc@38 327 end
adamc@38 328 val con = Con.mapfoldB {kind = kind, con = con, bind = bind'}
adamc@38 329
adamc@38 330 val kind = Kind.mapfold kind
adamc@38 331
adamc@38 332 fun sgi ctx si acc =
adamc@38 333 S.bindP (sgi' ctx si acc, sgn_item ctx)
adamc@38 334
adamc@38 335 and sgi' ctx (si, loc) =
adamc@38 336 case si of
adamc@38 337 SgiConAbs (x, n, k) =>
adamc@38 338 S.map2 (kind k,
adamc@38 339 fn k' =>
adamc@38 340 (SgiConAbs (x, n, k'), loc))
adamc@38 341 | SgiCon (x, n, k, c) =>
adamc@38 342 S.bind2 (kind k,
adamc@38 343 fn k' =>
adamc@38 344 S.map2 (con ctx c,
adamc@38 345 fn c' =>
adamc@38 346 (SgiCon (x, n, k', c'), loc)))
adamc@38 347 | SgiVal (x, n, c) =>
adamc@38 348 S.map2 (con ctx c,
adamc@38 349 fn c' =>
adamc@38 350 (SgiVal (x, n, c'), loc))
adamc@38 351 | SgiStr (x, n, s) =>
adamc@38 352 S.map2 (sg ctx s,
adamc@38 353 fn s' =>
adamc@38 354 (SgiStr (x, n, s'), loc))
adamc@64 355 | SgiSgn (x, n, s) =>
adamc@64 356 S.map2 (sg ctx s,
adamc@64 357 fn s' =>
adamc@64 358 (SgiSgn (x, n, s'), loc))
adamc@38 359
adamc@38 360 and sg ctx s acc =
adamc@38 361 S.bindP (sg' ctx s acc, sgn ctx)
adamc@38 362
adamc@38 363 and sg' ctx (sAll as (s, loc)) =
adamc@38 364 case s of
adamc@38 365 SgnConst sgis =>
adamc@38 366 S.map2 (ListUtil.mapfoldB (fn (ctx, si) =>
adamc@38 367 (case #1 si of
adamc@38 368 SgiConAbs (x, _, k) =>
adamc@38 369 bind (ctx, NamedC (x, k))
adamc@38 370 | SgiCon (x, _, k, _) =>
adamc@38 371 bind (ctx, NamedC (x, k))
adamc@38 372 | SgiVal _ => ctx
adamc@38 373 | SgiStr (x, _, sgn) =>
adamc@64 374 bind (ctx, Str (x, sgn))
adamc@64 375 | SgiSgn (x, _, sgn) =>
adamc@64 376 bind (ctx, Sgn (x, sgn)),
adamc@38 377 sgi ctx si)) ctx sgis,
adamc@38 378 fn sgis' =>
adamc@38 379 (SgnConst sgis', loc))
adamc@38 380
adamc@38 381 | SgnVar _ => S.return2 sAll
adamc@45 382
adamc@45 383 | SgnFun (m, n, s1, s2) =>
adamc@45 384 S.bind2 (sg ctx s1,
adamc@45 385 fn s1' =>
adamc@45 386 S.map2 (sg (bind (ctx, Str (m, s1'))) s2,
adamc@45 387 fn s2' =>
adamc@45 388 (SgnFun (m, n, s1', s2'), loc)))
adamc@45 389 | SgnWhere (sgn, x, c) =>
adamc@45 390 S.bind2 (sg ctx sgn,
adamc@45 391 fn sgn' =>
adamc@45 392 S.map2 (con ctx c,
adamc@45 393 fn c' =>
adamc@45 394 (SgnWhere (sgn', x, c'), loc)))
adamc@64 395 | SgnProj _ => S.return2 sAll
adamc@38 396 in
adamc@38 397 sg
adamc@38 398 end
adamc@38 399
adamc@38 400 fun mapfold {kind, con, sgn_item, sgn} =
adamc@38 401 mapfoldB {kind = kind,
adamc@38 402 con = fn () => con,
adamc@38 403 sgn_item = fn () => sgn_item,
adamc@38 404 sgn = fn () => sgn,
adamc@38 405 bind = fn ((), _) => ()} ()
adamc@38 406
adamc@38 407 fun map {kind, con, sgn_item, sgn} s =
adamc@38 408 case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@38 409 con = fn c => fn () => S.Continue (con c, ()),
adamc@38 410 sgn_item = fn si => fn () => S.Continue (sgn_item si, ()),
adamc@38 411 sgn = fn s => fn () => S.Continue (sgn s, ())} s () of
adamc@38 412 S.Return () => raise Fail "Expl_util.Sgn.map"
adamc@38 413 | S.Continue (s, ()) => s
adamc@38 414
adamc@38 415 end
adamc@38 416
adamc@38 417 end