Mercurial > urweb

annotate src/corify.sml @ 1327:1cc67fdac4d3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New argument to transactional free functions, to specify whether we are about to retry
author Adam Chlipala <adam@chlipala.net>
date Sat, 04 Dec 2010 11:15:20 -0500
parents 6c2e565adca6
children b106ca8200b1
rev   line source
adamc@1146 1 (* Copyright (c) 2008-2010, Adam Chlipala
adamc@16 2 * All rights reserved.
adamc@16 3 *
adamc@16 4 * Redistribution and use in source and binary forms, with or without
adamc@16 5 * modification, are permitted provided that the following conditions are met:
adamc@16 6 *
adamc@16 7 * - Redistributions of source code must retain the above copyright notice,
adamc@16 8 * this list of conditions and the following disclaimer.
adamc@16 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@16 10 * this list of conditions and the following disclaimer in the documentation
adamc@16 11 * and/or other materials provided with the distribution.
adamc@16 12 * - The names of contributors may not be used to endorse or promote products
adamc@16 13 * derived from this software without specific prior written permission.
adamc@16 14 *
adamc@16 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@16 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@16 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@16 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@16 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@16 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@16 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@16 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@16 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@16 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@16 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@16 26 *)
adamc@16 27
adamc@16 28 structure Corify :> CORIFY = struct
adamc@16 29
adamc@16 30 structure EM = ErrorMsg
adamc@39 31 structure L = Expl
adamc@16 32 structure L' = Core
adamc@16 33
adamc@39 34 structure IM = IntBinaryMap
adamc@39 35 structure SM = BinaryMapFn(struct
adamc@39 36 type ord_key = string
adamc@39 37 val compare = String.compare
adamc@39 38 end)
adamc@39 39
adamc@768 40 fun doRestify k (mods, s) =
adamc@376 41 let
adamc@376 42 val s = if String.isPrefix "wrap_" s then
adamc@376 43 String.extract (s, 5, NONE)
adamc@376 44 else
adamc@376 45 s
adamc@1023 46 val s = String.concatWith "/" (rev (s :: mods))
adamc@1023 47 val s = String.implode (List.filter (fn ch => ch <> #"$") (String.explode s))
adamc@376 48 in
adamc@1023 49 Settings.rewrite k s
adamc@376 50 end
adamc@376 51
adamc@377 52 val relify = CharVector.map (fn #"/" => #"_"
adamc@377 53 | ch => ch)
adamc@377 54
adamc@39 55 local
adamc@39 56 val count = ref 0
adamc@39 57 in
adamc@39 58
adamc@39 59 fun reset v = count := v
adamc@39 60
adamc@39 61 fun alloc () =
adamc@39 62 let
adamc@39 63 val r = !count
adamc@39 64 in
adamc@39 65 count := r + 1;
adamc@39 66 r
adamc@39 67 end
adamc@39 68
adamc@39 69 end
adamc@39 70
adamc@39 71 structure St : sig
adamc@39 72 type t
adamc@39 73
adamc@39 74 val empty : t
adamc@39 75
adamc@146 76 val debug : t -> unit
adamc@146 77
adamc@376 78 val name : t -> string list
adamc@376 79
adamc@376 80 val enter : t * string list -> t
adamc@39 81 val leave : t -> {outer : t, inner : t}
adamc@192 82 val ffi : string -> L'.con SM.map -> (string * string list * L'.con option * L'.datatype_kind) SM.map -> t
adamc@39 83
adamc@249 84 val basisIs : t * int -> t
adamc@249 85 val lookupBasis : t -> int option
adamc@249 86
adamc@73 87 datatype core_con =
adamc@73 88 CNormal of int
adamc@73 89 | CFfi of string
adamc@73 90 val bindCon : t -> string -> int -> t * int
adamc@73 91 val lookupConById : t -> int -> int option
adamc@73 92 val lookupConByName : t -> string -> core_con
adamc@48 93
adamc@177 94 val bindConstructor : t -> string -> int -> L'.patCon -> t
adamc@186 95 val lookupConstructorByNameOpt : t -> string -> L'.patCon option
adamc@177 96 val lookupConstructorByName : t -> string -> L'.patCon
adamc@177 97 val lookupConstructorById : t -> int -> L'.patCon
adamc@249 98
adamc@249 99 datatype core_val =
adamc@249 100 ENormal of int
adamc@249 101 | EFfi of string * L'.con
adamc@249 102 val bindVal : t -> string -> int -> t * int
adamc@249 103 val bindConstructorVal : t -> string -> int -> t
adamc@249 104 val lookupValById : t -> int -> int option
adamc@249 105 val lookupValByName : t -> string -> core_val
adamc@177 106
adamc@249 107 val bindStr : t -> string -> int -> t -> t
adamc@249 108 val lookupStrById : t -> int -> t
adamc@249 109 val lookupStrByName : string * t -> t
adamc@339 110 val lookupStrByNameOpt : string * t -> t option
adamc@39 111
adamc@423 112 val bindFunctor : t -> string -> int -> string -> int -> L.str -> t
adamc@423 113 val lookupFunctorById : t -> int -> string * int * L.str
adamc@423 114 val lookupFunctorByName : string * t -> string * int * L.str
adamc@249 115 end = struct
adamc@46 116
adamc@249 117 datatype flattening =
adamc@376 118 FNormal of {name : string list,
adamc@376 119 cons : int SM.map,
adamc@249 120 constructors : L'.patCon SM.map,
adamc@249 121 vals : int SM.map,
adamc@249 122 strs : flattening SM.map,
adamc@423 123 funs : (string * int * L.str) SM.map}
adamc@249 124 | FFfi of {mod : string,
adamc@249 125 vals : L'.con SM.map,
adamc@249 126 constructors : (string * string list * L'.con option * L'.datatype_kind) SM.map}
adamc@39 127
adamc@249 128 type t = {
adamc@249 129 basis : int option,
adamc@249 130 cons : int IM.map,
adamc@249 131 constructors : L'.patCon IM.map,
adamc@249 132 vals : int IM.map,
adamc@249 133 strs : flattening IM.map,
adamc@423 134 funs : (string * int * L.str) IM.map,
adamc@249 135 current : flattening,
adamc@249 136 nested : flattening list
adamc@249 137 }
adamc@39 138
adamc@249 139 val empty = {
adamc@249 140 basis = NONE,
adamc@249 141 cons = IM.empty,
adamc@249 142 constructors = IM.empty,
adamc@249 143 vals = IM.empty,
adamc@249 144 strs = IM.empty,
adamc@249 145 funs = IM.empty,
adamc@376 146 current = FNormal { name = [], cons = SM.empty, constructors = SM.empty,
adamc@376 147 vals = SM.empty, strs = SM.empty, funs = SM.empty },
adamc@249 148 nested = []
adamc@249 149 }
adamc@39 150
adamc@376 151 fun debug ({current = FNormal {cons, constructors, vals, strs, funs, ...}, ...} : t) =
adamc@249 152 print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; "
adamc@249 153 ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; "
adamc@249 154 ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; "
adamc@249 155 ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; "
adamc@249 156 ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n")
adamc@249 157 | debug _ = print "Not normal!\n"
adamc@146 158
adamc@376 159 fun name ({current = FNormal {name, ...}, ...} : t) = name
adamc@376 160 | name {current = FFfi {mod = name, ...}, ...} = [name]
adamc@376 161
adamc@249 162 fun basisIs ({cons, constructors, vals, strs, funs, current, nested, ...} : t, basis) =
adamc@249 163 {basis = SOME basis,
adamc@249 164 cons = cons,
adamc@249 165 constructors = constructors,
adamc@249 166 vals = vals,
adamc@249 167 strs = strs,
adamc@249 168 funs = funs,
adamc@249 169 current = current,
adamc@249 170 nested = nested}
adamc@48 171
adamc@249 172 fun lookupBasis ({basis, ...} : t) = basis
adamc@73 173
adamc@249 174 datatype core_con =
adamc@249 175 CNormal of int
adamc@249 176 | CFfi of string
adamc@39 177
adamc@249 178 datatype core_val =
adamc@249 179 ENormal of int
adamc@249 180 | EFfi of string * L'.con
adamc@188 181
adamc@249 182 fun bindCon {basis, cons, constructors, vals, strs, funs, current, nested} s n =
adamc@249 183 let
adamc@249 184 val n' = alloc ()
adamc@188 185
adamc@249 186 val current =
adamc@249 187 case current of
adamc@249 188 FFfi _ => raise Fail "Binding inside FFfi"
adamc@376 189 | FNormal {name, cons, constructors, vals, strs, funs} =>
adamc@376 190 FNormal {name = name,
adamc@376 191 cons = SM.insert (cons, s, n'),
adamc@249 192 constructors = constructors,
adamc@249 193 vals = vals,
adamc@249 194 strs = strs,
adamc@249 195 funs = funs}
adamc@249 196 in
adamc@249 197 ({basis = basis,
adamc@249 198 cons = IM.insert (cons, n, n'),
adamc@177 199 constructors = constructors,
adamc@73 200 vals = vals,
adamc@39 201 strs = strs,
adamc@46 202 funs = funs,
adamc@39 203 current = current,
adamc@249 204 nested = nested},
adamc@249 205 n')
adamc@249 206 end
adamc@39 207
adamc@249 208 fun lookupConById ({cons, ...} : t) n = IM.find (cons, n)
adamc@39 209
adamc@249 210 fun lookupConByName ({current, ...} : t) x =
adamc@249 211 case current of
adamc@249 212 FFfi {mod = m, ...} => CFfi m
adamc@249 213 | FNormal {cons, ...} =>
adamc@249 214 case SM.find (cons, x) of
adamc@249 215 NONE => raise Fail "Corify.St.lookupConByName"
adamc@249 216 | SOME n => CNormal n
adamc@249 217
adamc@249 218 fun bindVal {basis, cons, constructors, vals, strs, funs, current, nested} s n =
adamc@249 219 let
adamc@249 220 val n' = alloc ()
adamc@249 221
adamc@249 222 val current =
adamc@249 223 case current of
adamc@249 224 FFfi _ => raise Fail "Binding inside FFfi"
adamc@376 225 | FNormal {name, cons, constructors, vals, strs, funs} =>
adamc@376 226 FNormal {name = name,
adamc@376 227 cons = cons,
adamc@249 228 constructors = constructors,
adamc@249 229 vals = SM.insert (vals, s, n'),
adamc@249 230 strs = strs,
adamc@249 231 funs = funs}
adamc@249 232 in
adamc@249 233 ({basis = basis,
adamc@249 234 cons = cons,
adamc@249 235 constructors = constructors,
adamc@249 236 vals = IM.insert (vals, n, n'),
adamc@249 237 strs = strs,
adamc@249 238 funs = funs,
adamc@249 239 current = current,
adamc@249 240 nested = nested},
adamc@249 241 n')
adamc@249 242 end
adamc@249 243
adamc@249 244 fun bindConstructorVal {basis, cons, constructors, vals, strs, funs, current, nested} s n =
adamc@249 245 let
adamc@249 246 val current =
adamc@249 247 case current of
adamc@249 248 FFfi _ => raise Fail "Binding inside FFfi"
adamc@376 249 | FNormal {name, cons, constructors, vals, strs, funs} =>
adamc@376 250 FNormal {name = name,
adamc@376 251 cons = cons,
adamc@249 252 constructors = constructors,
adamc@249 253 vals = SM.insert (vals, s, n),
adamc@249 254 strs = strs,
adamc@249 255 funs = funs}
adamc@249 256 in
adamc@249 257 {basis = basis,
adamc@249 258 cons = cons,
adamc@249 259 constructors = constructors,
adamc@249 260 vals = IM.insert (vals, n, n),
adamc@249 261 strs = strs,
adamc@249 262 funs = funs,
adamc@249 263 current = current,
adamc@249 264 nested = nested}
adamc@249 265 end
adamc@249 266
adamc@249 267
adamc@249 268 fun lookupValById ({vals, ...} : t) n = IM.find (vals, n)
adamc@249 269
adamc@249 270 fun lookupValByName ({current, ...} : t) x =
adamc@249 271 case current of
adamc@249 272 FFfi {mod = m, vals, ...} =>
adamc@249 273 (case SM.find (vals, x) of
adam@1314 274 NONE => raise Fail ("Corify.St.lookupValByName: no type for FFI val " ^ x)
adamc@249 275 | SOME t => EFfi (m, t))
adam@1314 276 | FNormal {name, vals, ...} =>
adamc@249 277 case SM.find (vals, x) of
adam@1314 278 NONE => raise Fail ("Corify.St.lookupValByName " ^ String.concatWith "." name ^ "." ^ x)
adamc@249 279 | SOME n => ENormal n
adamc@249 280
adamc@249 281 fun bindConstructor {basis, cons, constructors, vals, strs, funs, current, nested} s n n' =
adamc@249 282 let
adamc@249 283 val current =
adamc@249 284 case current of
adamc@249 285 FFfi _ => raise Fail "Binding inside FFfi"
adamc@376 286 | FNormal {name, cons, constructors, vals, strs, funs} =>
adamc@376 287 FNormal {name = name,
adamc@376 288 cons = cons,
adamc@249 289 constructors = SM.insert (constructors, s, n'),
adamc@249 290 vals = vals,
adamc@249 291 strs = strs,
adamc@249 292 funs = funs}
adamc@249 293 in
adamc@249 294 {basis = basis,
adamc@249 295 cons = cons,
adamc@249 296 constructors = IM.insert (constructors, n, n'),
adamc@249 297 vals = vals,
adamc@249 298 strs = strs,
adamc@249 299 funs = funs,
adamc@249 300 current = current,
adamc@249 301 nested = nested}
adamc@249 302 end
adamc@249 303
adamc@249 304 fun lookupConstructorById ({constructors, ...} : t) n =
adamc@249 305 case IM.find (constructors, n) of
adamc@249 306 NONE => raise Fail "Corify.St.lookupConstructorById"
adamc@249 307 | SOME x => x
adamc@249 308
adamc@249 309 fun lookupConstructorByNameOpt ({current, ...} : t) x =
adamc@249 310 case current of
adamc@249 311 FFfi {mod = m, constructors, ...} =>
adamc@249 312 (case SM.find (constructors, x) of
adamc@188 313 NONE => NONE
adamc@249 314 | SOME (n, xs, to, dk) => SOME (L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk}))
adamc@249 315 | FNormal {constructors, ...} =>
adamc@249 316 case SM.find (constructors, x) of
adamc@249 317 NONE => NONE
adamc@249 318 | SOME n => SOME n
adamc@39 319
adamc@249 320 fun lookupConstructorByName ({current, ...} : t) x =
adamc@249 321 case current of
adamc@249 322 FFfi {mod = m, constructors, ...} =>
adamc@249 323 (case SM.find (constructors, x) of
adamc@249 324 NONE => raise Fail "Corify.St.lookupConstructorByName [1]"
adamc@249 325 | SOME (n, xs, to, dk) => L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk})
adamc@249 326 | FNormal {constructors, ...} =>
adamc@249 327 case SM.find (constructors, x) of
adamc@249 328 NONE => raise Fail "Corify.St.lookupConstructorByName [2]"
adamc@249 329 | SOME n => n
adamc@73 330
adamc@376 331 fun enter ({basis, cons, constructors, vals, strs, funs, current, nested}, name) =
adamc@249 332 {basis = basis,
adamc@249 333 cons = cons,
adamc@249 334 constructors = constructors,
adamc@249 335 vals = vals,
adamc@249 336 strs = strs,
adamc@249 337 funs = funs,
adamc@376 338 current = FNormal {name = name,
adamc@376 339 cons = SM.empty,
adamc@249 340 constructors = SM.empty,
adamc@249 341 vals = SM.empty,
adamc@249 342 strs = SM.empty,
adamc@249 343 funs = SM.empty},
adamc@249 344 nested = current :: nested}
adamc@73 345
adamc@249 346 fun dummy (b, f) = {basis = b,
adamc@249 347 cons = IM.empty,
adamc@249 348 constructors = IM.empty,
adamc@249 349 vals = IM.empty,
adamc@249 350 strs = IM.empty,
adamc@249 351 funs = IM.empty,
adamc@249 352 current = f,
adamc@249 353 nested = []}
adamc@163 354
adamc@249 355 fun leave {basis, cons, constructors, vals, strs, funs, current, nested = m1 :: rest} =
adamc@249 356 {outer = {basis = basis,
adamc@249 357 cons = cons,
adamc@249 358 constructors = constructors,
adamc@249 359 vals = vals,
adamc@249 360 strs = strs,
adamc@249 361 funs = funs,
adamc@249 362 current = m1,
adamc@249 363 nested = rest},
adamc@249 364 inner = dummy (basis, current)}
adamc@249 365 | leave _ = raise Fail "Corify.St.leave"
adamc@177 366
adamc@249 367 fun ffi m vals constructors = dummy (NONE, FFfi {mod = m, vals = vals, constructors = constructors})
adamc@73 368
adamc@249 369 fun bindStr ({basis, cons, constructors, vals, strs, funs,
adamc@376 370 current = FNormal {name, cons = mcons, constructors = mconstructors,
adamc@249 371 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
adamc@249 372 x n ({current = f, ...} : t) =
adamc@249 373 {basis = basis,
adamc@249 374 cons = cons,
adamc@249 375 constructors = constructors,
adamc@249 376 vals = vals,
adamc@249 377 strs = IM.insert (strs, n, f),
adamc@249 378 funs = funs,
adamc@376 379 current = FNormal {name = name,
adamc@376 380 cons = mcons,
adamc@249 381 constructors = mconstructors,
adamc@249 382 vals = mvals,
adamc@249 383 strs = SM.insert (mstrs, x, f),
adamc@249 384 funs = mfuns},
adamc@249 385 nested = nested}
adamc@249 386 | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr"
adamc@73 387
adamc@249 388 fun lookupStrById ({basis, strs, ...} : t) n =
adamc@249 389 case IM.find (strs, n) of
adamc@480 390 NONE => raise Fail ("Corify.St.lookupStrById(" ^ Int.toString n ^ ")")
adamc@249 391 | SOME f => dummy (basis, f)
adamc@177 392
adamc@249 393 fun lookupStrByName (m, {basis, current = FNormal {strs, ...}, ...} : t) =
adamc@249 394 (case SM.find (strs, m) of
adamc@339 395 NONE => raise Fail "Corify.St.lookupStrByName [1]"
adamc@249 396 | SOME f => dummy (basis, f))
adamc@339 397 | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName [2]"
adamc@339 398
adamc@339 399 fun lookupStrByNameOpt (m, {basis, current = FNormal {strs, ...}, ...} : t) =
adamc@339 400 (case SM.find (strs, m) of
adamc@339 401 NONE => NONE
adamc@339 402 | SOME f => SOME (dummy (basis, f)))
adamc@339 403 | lookupStrByNameOpt _ = NONE
adamc@177 404
adamc@249 405 fun bindFunctor ({basis, cons, constructors, vals, strs, funs,
adamc@376 406 current = FNormal {name, cons = mcons, constructors = mconstructors,
adamc@249 407 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
adamc@423 408 x n xa na str =
adamc@249 409 {basis = basis,
adamc@249 410 cons = cons,
adamc@249 411 constructors = constructors,
adamc@249 412 vals = vals,
adamc@249 413 strs = strs,
adamc@423 414 funs = IM.insert (funs, n, (xa, na, str)),
adamc@376 415 current = FNormal {name = name,
adamc@376 416 cons = mcons,
adamc@249 417 constructors = mconstructors,
adamc@249 418 vals = mvals,
adamc@249 419 strs = mstrs,
adamc@423 420 funs = SM.insert (mfuns, x, (xa, na, str))},
adamc@249 421 nested = nested}
adamc@423 422 | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
adamc@186 423
adamc@249 424 fun lookupFunctorById ({funs, ...} : t) n =
adamc@249 425 case IM.find (funs, n) of
adamc@249 426 NONE => raise Fail "Corify.St.lookupFunctorById"
adamc@249 427 | SOME v => v
adamc@177 428
adamc@249 429 fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) =
adamc@249 430 (case SM.find (funs, m) of
adamc@1146 431 NONE => raise Fail ("Corify.St.lookupFunctorByName " ^ m ^ "[1]")
adamc@249 432 | SOME v => v)
adamc@339 433 | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName [2]"
adamc@39 434
adamc@249 435 end
adamc@39 436
adamc@39 437
adamc@249 438 fun corifyKind (k, loc) =
adamc@249 439 case k of
adamc@249 440 L.KType => (L'.KType, loc)
adamc@249 441 | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc)
adamc@249 442 | L.KName => (L'.KName, loc)
adamc@249 443 | L.KRecord k => (L'.KRecord (corifyKind k), loc)
adamc@249 444 | L.KUnit => (L'.KUnit, loc)
adamc@249 445 | L.KTuple ks => (L'.KTuple (map corifyKind ks), loc)
adamc@48 446
adamc@626 447 | L.KRel n => (L'.KRel n, loc)
adamc@626 448 | L.KFun (x, k) => (L'.KFun (x, corifyKind k), loc)
adamc@626 449
adamc@249 450 fun corifyCon st (c, loc) =
adamc@249 451 case c of
adamc@249 452 L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc)
adamc@249 453 | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc)
adamc@626 454 | L.TKFun (x, t) => (L'.TKFun (x, corifyCon st t), loc)
adamc@249 455 | L.TRecord c => (L'.TRecord (corifyCon st c), loc)
adamc@39 456
adamc@249 457 | L.CRel n => (L'.CRel n, loc)
adamc@249 458 | L.CNamed n =>
adamc@249 459 (case St.lookupConById st n of
adamc@249 460 NONE => (L'.CNamed n, loc)
adamc@249 461 | SOME n => (L'.CNamed n, loc))
adamc@249 462 | L.CModProj (m, ms, x) =>
adamc@249 463 let
adamc@249 464 val st = St.lookupStrById st m
adamc@249 465 val st = foldl St.lookupStrByName st ms
adamc@249 466 in
adamc@249 467 case St.lookupConByName st x of
adamc@249 468 St.CNormal n => (L'.CNamed n, loc)
adamc@249 469 | St.CFfi m => (L'.CFfi (m, x), loc)
adamc@249 470 end
adamc@39 471
adamc@249 472 | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc)
adamc@249 473 | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc)
adamc@39 474
adamc@626 475 | L.CKApp (c1, k) => (L'.CKApp (corifyCon st c1, corifyKind k), loc)
adamc@626 476 | L.CKAbs (x, c) => (L'.CKAbs (x, corifyCon st c), loc)
adamc@626 477
adamc@249 478 | L.CName s => (L'.CName s, loc)
adamc@46 479
adamc@249 480 | L.CRecord (k, xcs) =>
adamc@249 481 (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc)
adamc@249 482 | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc)
adamc@621 483 | L.CMap (k1, k2) => (L'.CMap (corifyKind k1, corifyKind k2), loc)
adamc@249 484 | L.CUnit => (L'.CUnit, loc)
adamc@46 485
adamc@249 486 | L.CTuple cs => (L'.CTuple (map (corifyCon st) cs), loc)
adamc@249 487 | L.CProj (c, n) => (L'.CProj (corifyCon st c, n), loc)
adamc@213 488
adamc@249 489 fun corifyPatCon st pc =
adamc@249 490 case pc of
adamc@249 491 L.PConVar n => St.lookupConstructorById st n
adamc@249 492 | L.PConProj (m1, ms, x) =>
adamc@249 493 let
adamc@249 494 val st = St.lookupStrById st m1
adamc@249 495 val st = foldl St.lookupStrByName st ms
adamc@249 496 in
adamc@249 497 St.lookupConstructorByName st x
adamc@249 498 end
adamc@46 499
adamc@249 500 fun corifyPat st (p, loc) =
adamc@249 501 case p of
adamc@249 502 L.PWild => (L'.PWild, loc)
adamc@249 503 | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc)
adamc@249 504 | L.PPrim p => (L'.PPrim p, loc)
adamc@249 505 | L.PCon (dk, pc, ts, po) => (L'.PCon (dk, corifyPatCon st pc, map (corifyCon st) ts,
adamc@249 506 Option.map (corifyPat st) po), loc)
adamc@249 507 | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc)
adamc@39 508
adamc@249 509 fun corifyExp st (e, loc) =
adamc@249 510 case e of
adamc@249 511 L.EPrim p => (L'.EPrim p, loc)
adamc@249 512 | L.ERel n => (L'.ERel n, loc)
adamc@249 513 | L.ENamed n =>
adamc@249 514 (case St.lookupValById st n of
adamc@249 515 NONE => (L'.ENamed n, loc)
adamc@249 516 | SOME n => (L'.ENamed n, loc))
adamc@249 517 | L.EModProj (m, ms, x) =>
adamc@249 518 let
adamc@249 519 val st = St.lookupStrById st m
adamc@249 520 val st = foldl St.lookupStrByName st ms
adamc@249 521 in
adamc@249 522 case St.lookupConstructorByNameOpt st x of
adamc@249 523 SOME (pc as L'.PConFfi {mod = m, datatyp, params, arg, kind, ...}) =>
adamc@249 524 let
adamc@249 525 val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) params
adamc@249 526 val e = case arg of
adamc@249 527 NONE => (L'.ECon (kind, pc, args, NONE), loc)
adamc@249 528 | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc),
adamc@249 529 (L'.ECon (kind, pc, args, SOME (L'.ERel 0, loc)), loc)), loc)
adamc@192 530
adamc@249 531 val k = (L'.KType, loc)
adamc@249 532 in
adamc@249 533 foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e params
adamc@249 534 end
adamc@249 535 | _ =>
adamc@249 536 case St.lookupValByName st x of
adamc@249 537 St.ENormal n => (L'.ENamed n, loc)
adamc@249 538 | St.EFfi (m, t) =>
adamc@249 539 case t of
adamc@249 540 (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) =>
adamc@249 541 (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc)
adamc@765 542 | (L'.CApp ((L'.CFfi ("Basis", "transaction"), _), dom), _) =>
adamc@765 543 (L'.EAbs ("arg", dom, (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc),
adamc@765 544 (L'.EFfiApp (m, x, []), loc)), loc)
adamc@249 545 | t as (L'.TFun _, _) =>
adamc@249 546 let
adamc@249 547 fun getArgs (all as (t, _), args) =
adamc@249 548 case t of
adamc@249 549 L'.TFun (dom, ran) => getArgs (ran, dom :: args)
adamc@249 550 | _ => (all, rev args)
adamc@39 551
adamc@249 552 val (result, args) = getArgs (t, [])
adamc@456 553 val (isTransaction, result) =
adamc@456 554 case result of
adamc@456 555 (L'.CApp ((L'.CFfi ("Basis", "transaction"), _),
adamc@456 556 result), _) => (true, result)
adamc@456 557 | _ => (false, result)
adamc@16 558
adamc@456 559 fun makeApp n =
adamc@456 560 let
adamc@456 561 val (actuals, _) = foldr (fn (_, (actuals, n)) =>
adamc@456 562 ((L'.ERel n, loc) :: actuals,
adamc@456 563 n + 1)) ([], n) args
adamc@456 564 in
adamc@456 565 (L'.EFfiApp (m, x, actuals), loc)
adamc@456 566 end
adamc@456 567 val unit = (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc)
adamc@456 568 val (result, app) =
adamc@456 569 if isTransaction then
adamc@456 570 ((L'.TFun (unit, result), loc),
adamc@456 571 (L'.EAbs ("_",
adamc@456 572 unit,
adamc@456 573 result,
adamc@456 574 makeApp 1), loc))
adamc@456 575 else
adamc@456 576 (result, makeApp 0)
adamc@456 577
adamc@249 578 val (abs, _, _) = foldr (fn (t, (abs, ran, n)) =>
adamc@249 579 ((L'.EAbs ("arg" ^ Int.toString n,
adamc@249 580 t,
adamc@249 581 ran,
adamc@249 582 abs), loc),
adamc@249 583 (L'.TFun (t, ran), loc),
adamc@249 584 n - 1)) (app, result, length args - 1) args
adamc@249 585 in
adamc@249 586 abs
adamc@249 587 end
adamc@249 588 | _ => (L'.EFfi (m, x), loc)
adamc@249 589 end
adamc@249 590 | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc)
adamc@249 591 | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc)
adamc@249 592 | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc)
adamc@249 593 | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc)
adamc@626 594 | L.EKApp (e1, k) => (L'.EKApp (corifyExp st e1, corifyKind k), loc)
adamc@626 595 | L.EKAbs (x, e1) => (L'.EKAbs (x, corifyExp st e1), loc)
adamc@16 596
adamc@249 597 | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) =>
adamc@249 598 (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc)
adamc@249 599 | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c,
adamc@249 600 {field = corifyCon st field, rest = corifyCon st rest}), loc)
adamc@445 601 | L.EConcat (e1, c1, e2, c2) => (L'.EConcat (corifyExp st e1, corifyCon st c1, corifyExp st e2,
adamc@445 602 corifyCon st c2), loc)
adamc@249 603 | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c,
adamc@249 604 {field = corifyCon st field, rest = corifyCon st rest}), loc)
adamc@493 605 | L.ECutMulti (e1, c, {rest}) => (L'.ECutMulti (corifyExp st e1, corifyCon st c,
adamc@493 606 {rest = corifyCon st rest}), loc)
adamc@34 607
adamc@249 608 | L.ECase (e, pes, {disc, result}) =>
adamc@249 609 (L'.ECase (corifyExp st e,
adamc@249 610 map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes,
adamc@249 611 {disc = corifyCon st disc, result = corifyCon st result}),
adamc@249 612 loc)
adamc@16 613
adamc@249 614 | L.EWrite e => (L'.EWrite (corifyExp st e), loc)
adamc@16 615
adamc@450 616 | L.ELet (x, t, e1, e2) => (L'.ELet (x, corifyCon st t, corifyExp st e1, corifyExp st e2), loc)
adamc@450 617
adamc@480 618 fun corifyDecl mods (all as (d, loc : EM.span), st) =
adamc@249 619 case d of
adamc@249 620 L.DCon (x, n, k, c) =>
adamc@249 621 let
adamc@249 622 val (st, n) = St.bindCon st x n
adamc@249 623 in
adamc@249 624 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
adamc@249 625 end
adamc@807 626 | L.DDatatype dts =>
adamc@249 627 let
adamc@807 628 val (dts, st) = ListUtil.foldlMap (fn ((x, n, xs, xncs), st) =>
adamc@807 629 let
adamc@807 630 val (st, n) = St.bindCon st x n
adamc@807 631 in
adamc@807 632 ((x, n, xs, xncs), st)
adamc@807 633 end)
adamc@807 634 st dts
adamc@16 635
adamc@807 636 val (dts, (st, dcons)) =
adamc@807 637 ListUtil.foldlMap
adamc@807 638 (fn ((x, n, xs, xncs), (st, dcons)) =>
adamc@807 639 let
adamc@807 640 val (xncs, st) = ListUtil.foldlMap
adamc@807 641 (fn ((x, n, co), st) =>
adamc@807 642 let
adamc@807 643 val st = St.bindConstructor st x n (L'.PConVar n)
adamc@807 644 val st = St.bindConstructorVal st x n
adamc@807 645 val co = Option.map (corifyCon st) co
adamc@807 646 in
adamc@807 647 ((x, n, co), st)
adamc@807 648 end) st xncs
adamc@192 649
adamc@807 650 val dk = ElabUtil.classifyDatatype xncs
adamc@807 651 val t = (L'.CNamed n, loc)
adamc@807 652 val nxs = length xs - 1
adamc@807 653 val t = ListUtil.foldli
adamc@807 654 (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
adamc@807 655 val k = (L'.KType, loc)
adamc@807 656 val dcons' = map (fn (x, n, to) =>
adamc@807 657 let
adamc@807 658 val args = ListUtil.mapi
adamc@807 659 (fn (i, _) => (L'.CRel (nxs - i), loc)) xs
adamc@807 660 val (e, t) =
adamc@807 661 case to of
adamc@807 662 NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE),
adamc@807 663 loc), t)
adamc@807 664 | SOME t' => ((L'.EAbs ("x", t', t,
adamc@807 665 (L'.ECon (dk, L'.PConVar n,
adamc@807 666 args,
adamc@807 667 SOME (L'.ERel 0,
adamc@807 668 loc)),
adamc@807 669 loc)),
adamc@807 670 loc),
adamc@807 671 (L'.TFun (t', t), loc))
adamc@807 672
adamc@807 673 val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
adamc@807 674 val e = foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
adamc@807 675 in
adamc@807 676 (L'.DVal (x, n, t, e, ""), loc)
adamc@807 677 end) xncs
adamc@807 678 in
adamc@807 679 ((x, n, xs, xncs), (st, dcons' @ dcons))
adamc@807 680 end)
adamc@807 681 (st, []) dts
adamc@249 682 in
adamc@807 683 ((L'.DDatatype dts, loc) :: dcons, st)
adamc@807 684 end
adamc@249 685 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
adamc@249 686 let
adamc@249 687 val (st, n) = St.bindCon st x n
adamc@249 688 val c = corifyCon st (L.CModProj (m1, ms, s), loc)
adamc@177 689
adamc@249 690 val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms
adamc@376 691 val (_, {inner, ...}) = corifyStr mods (m, st)
adamc@177 692
adamc@249 693 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
adamc@249 694 let
adamc@249 695 val n' = St.lookupConstructorByName inner x
adamc@249 696 val st = St.bindConstructor st x n n'
adamc@249 697 val (st, n) = St.bindVal st x n
adamc@249 698 val co = Option.map (corifyCon st) co
adamc@249 699 in
adamc@249 700 ((x, n, co), st)
adamc@249 701 end) st xncs
adamc@49 702
adamc@249 703 val nxs = length xs - 1
adamc@288 704 val cBase = c
adamc@249 705 val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel (nxs - i), loc)), loc)) c xs
adamc@249 706 val k = (L'.KType, loc)
adamc@249 707 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@192 708
adamc@249 709 val cds = map (fn (x, n, co) =>
adamc@249 710 let
adamc@249 711 val t = case co of
adamc@249 712 NONE => c
adamc@249 713 | SOME t' => (L'.TFun (t', c), loc)
adamc@249 714 val e = corifyExp st (L.EModProj (m1, ms, x), loc)
adamc@192 715
adamc@249 716 val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
adamc@249 717 in
adamc@249 718 (L'.DVal (x, n, t, e, x), loc)
adamc@249 719 end) xncs
adamc@249 720 in
adamc@288 721 ((L'.DCon (x, n, k', cBase), loc) :: cds, st)
adamc@249 722 end
adamc@249 723 | L.DVal (x, n, t, e) =>
adamc@249 724 let
adamc@249 725 val (st, n) = St.bindVal st x n
adamc@768 726 val s = doRestify Settings.Url (mods, x)
adamc@249 727 in
adamc@249 728 ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st)
adamc@249 729 end
adamc@249 730 | L.DValRec vis =>
adamc@249 731 let
adamc@249 732 val (vis, st) = ListUtil.foldlMap
adamc@249 733 (fn ((x, n, t, e), st) =>
adamc@249 734 let
adamc@249 735 val (st, n) = St.bindVal st x n
adamc@249 736 in
adamc@249 737 ((x, n, t, e), st)
adamc@249 738 end)
adamc@249 739 st vis
adamc@16 740
adamc@249 741 val vis = map
adamc@249 742 (fn (x, n, t, e) =>
adamc@249 743 let
adamc@768 744 val s = doRestify Settings.Url (mods, x)
adamc@249 745 in
adamc@249 746 (x, n, corifyCon st t, corifyExp st e, s)
adamc@249 747 end)
adamc@249 748 vis
adamc@249 749 in
adamc@249 750 ([(L'.DValRec vis, loc)], st)
adamc@249 751 end
adamc@249 752 | L.DSgn _ => ([], st)
adamc@177 753
adamc@249 754 | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) =>
adamc@423 755 ([], St.bindFunctor st x n xa na str)
adamc@177 756
adamc@339 757 | L.DStr (x, n, _, (L.StrProj (str, x'), _)) =>
adamc@339 758 let
adamc@376 759 val (ds, {inner, outer}) = corifyStr mods (str, st)
adamc@339 760
adamc@339 761 val st = case St.lookupStrByNameOpt (x', inner) of
adamc@339 762 SOME st' => St.bindStr st x n st'
adamc@339 763 | NONE =>
adamc@339 764 let
adamc@423 765 val (x', n', str') = St.lookupFunctorByName (x', inner)
adamc@339 766 in
adamc@423 767 St.bindFunctor st x n x' n' str'
adamc@339 768 end
adamc@339 769 in
adamc@339 770 ([], st)
adamc@339 771 end
adamc@339 772
adamc@249 773 | L.DStr (x, n, _, str) =>
adamc@249 774 let
adamc@377 775 val mods' =
adamc@377 776 if x = "anon" then
adamc@377 777 mods
adamc@377 778 else
adamc@377 779 x :: mods
adamc@377 780
adamc@377 781 val (ds, {inner, outer}) = corifyStr mods' (str, st)
adamc@249 782 val st = St.bindStr outer x n inner
adamc@249 783 in
adamc@249 784 (ds, st)
adamc@249 785 end
adamc@16 786
adamc@249 787 | L.DFfiStr (m, n, (sgn, _)) =>
adamc@249 788 (case sgn of
adamc@249 789 L.SgnConst sgis =>
adamc@249 790 let
adamc@456 791 val (ds, cmap, conmap, st, _) =
adamc@456 792 foldl (fn ((sgi, _), (ds, cmap, conmap, st, trans)) =>
adamc@249 793 case sgi of
adamc@249 794 L.SgiConAbs (x, n, k) =>
adamc@249 795 let
adamc@249 796 val (st, n') = St.bindCon st x n
adamc@456 797
adamc@456 798 val trans =
adamc@456 799 if x = "transaction" then
adamc@456 800 SOME n
adamc@456 801 else
adamc@456 802 trans
adamc@249 803 in
adamc@249 804 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
adamc@249 805 cmap,
adamc@249 806 conmap,
adamc@456 807 st,
adamc@456 808 trans)
adamc@249 809 end
adamc@249 810 | L.SgiCon (x, n, k, _) =>
adamc@249 811 let
adamc@249 812 val (st, n') = St.bindCon st x n
adamc@249 813 in
adamc@249 814 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
adamc@249 815 cmap,
adamc@249 816 conmap,
adamc@456 817 st,
adamc@456 818 trans)
adamc@249 819 end
adamc@177 820
adamc@807 821 | L.SgiDatatype dts =>
adamc@249 822 let
adamc@249 823 val k = (L'.KType, loc)
adamc@807 824
adamc@807 825 val (dts, (ds', st, cmap, conmap)) =
adamc@249 826 ListUtil.foldlMap
adamc@807 827 (fn ((x, n, xs, xnts), (ds', st, cmap, conmap)) =>
adamc@249 828 let
adamc@813 829 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc))
adamc@813 830 k xs
adamc@813 831
adamc@807 832 val dk = ElabUtil.classifyDatatype xnts
adamc@807 833 val (st, n') = St.bindCon st x n
adamc@807 834 val (xnts, (ds', st, cmap, conmap)) =
adamc@807 835 ListUtil.foldlMap
adamc@807 836 (fn ((x', n, to), (ds', st, cmap, conmap)) =>
adamc@807 837 let
adamc@807 838 val dt = (L'.CNamed n', loc)
adamc@807 839 val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs
adamc@163 840
adamc@807 841 val to = Option.map (corifyCon st) to
adamc@177 842
adamc@807 843 val pc = L'.PConFfi {mod = m,
adamc@807 844 datatyp = x,
adamc@807 845 params = xs,
adamc@807 846 con = x',
adamc@807 847 arg = to,
adamc@807 848 kind = dk}
adamc@130 849
adamc@807 850 fun wrapT t =
adamc@807 851 foldr (fn (x, t) => (L'.TCFun (x, k, t), loc))
adamc@807 852 t xs
adamc@807 853 fun wrapE e =
adamc@807 854 foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc))
adamc@807 855 e xs
adamc@192 856
adamc@807 857 val (cmap, d) =
adamc@807 858 case to of
adamc@807 859 NONE => (SM.insert (cmap, x', wrapT dt),
adamc@807 860 (L'.DVal (x', n, wrapT dt,
adamc@807 861 wrapE
adamc@807 862 (L'.ECon (dk, pc,
adamc@807 863 args,
adamc@807 864 NONE),
adamc@807 865 loc),
adamc@807 866 ""), loc))
adamc@807 867 | SOME t =>
adamc@807 868 let
adamc@807 869 val tf = (L'.TFun (t, dt), loc)
adamc@807 870 val e = wrapE
adamc@807 871 (L'.EAbs ("x", t, tf,
adamc@807 872 (L'.ECon (dk,
adamc@807 873 pc,
adamc@807 874 args,
adamc@807 875 SOME
adamc@807 876 (L'.ERel 0,
adamc@807 877 loc)),
adamc@807 878 loc)), loc)
adamc@807 879 val d = (L'.DVal (x', n, wrapT tf,
adamc@807 880 e, ""), loc)
adamc@807 881 in
adamc@807 882 (SM.insert (cmap, x', wrapT tf), d)
adamc@807 883 end
adamc@185 884
adamc@807 885 val st = St.bindConstructor st x' n pc
adamc@807 886
adamc@807 887 val conmap = SM.insert (conmap, x',
adamc@807 888 (x, xs, to, dk))
adamc@807 889 in
adamc@807 890 ((x', n, to),
adamc@807 891 (d :: ds', st, cmap, conmap))
adamc@807 892 end) (ds', st, cmap, conmap) xnts
adamc@813 893
adamc@813 894 val d = (L'.DCon (x, n', k', (L'.CFfi (m, x), loc)), loc)
adamc@185 895 in
adamc@813 896 ((x, n', xs, xnts), (d :: ds', st, cmap, conmap))
adamc@807 897 end)
adamc@807 898 ([], st, cmap, conmap) dts
adamc@185 899 in
adamc@813 900 (List.revAppend (ds', ds),
adamc@185 901 cmap,
adamc@185 902 conmap,
adamc@456 903 st,
adamc@456 904 trans)
adamc@807 905 end
adamc@49 906
adamc@49 907 | L.SgiVal (x, _, c) =>
adamc@456 908 let
adamc@456 909 val c =
adamc@456 910 case trans of
adamc@456 911 NONE => corifyCon st c
adamc@456 912 | SOME trans =>
adamc@456 913 let
adamc@456 914 fun transactify (all as (c, loc)) =
adamc@456 915 case c of
adamc@456 916 L.TFun (dom, ran) =>
adamc@456 917 (L'.TFun (corifyCon st dom, transactify ran), loc)
adamc@456 918 | L.CApp ((L.CNamed trans', _), t) =>
adamc@456 919 if trans' = trans then
adamc@456 920 (L'.CApp ((L'.CFfi (m, "transaction"), loc),
adamc@456 921 corifyCon st t), loc)
adamc@456 922 else
adamc@456 923 corifyCon st all
adamc@456 924 | _ => corifyCon st all
adamc@456 925 in
adamc@456 926 transactify c
adamc@456 927 end
adamc@456 928 in
adamc@456 929 (ds,
adamc@456 930 SM.insert (cmap, x, c),
adamc@456 931 conmap,
adamc@456 932 st,
adamc@456 933 trans)
adamc@456 934 end
adamc@456 935 | _ => (ds, cmap, conmap, st, trans))
adamc@456 936 ([], SM.empty, SM.empty, st, NONE) sgis
adamc@49 937
adamc@185 938 val st = St.bindStr st m n (St.ffi m cmap conmap)
adamc@49 939 in
adamc@764 940 (rev ds, if m = "Basis" then St.basisIs (st, n) else st)
adamc@49 941 end
adamc@49 942 | _ => raise Fail "Non-const signature for FFI structure")
adamc@48 943
adamc@109 944 | L.DExport (en, sgn, str) =>
adamc@109 945 (case #1 sgn of
adamc@109 946 L.SgnConst sgis =>
adamc@109 947 let
adamc@109 948 fun pathify (str, _) =
adamc@109 949 case str of
adamc@109 950 L.StrVar m => SOME (m, [])
adamc@109 951 | L.StrProj (str, s) =>
adamc@109 952 Option.map (fn (m, ms) => (m, ms @ [s])) (pathify str)
adamc@109 953 | _ => NONE
adamc@109 954 in
adamc@109 955 case pathify str of
adamc@109 956 NONE => (ErrorMsg.errorAt loc "Structure is too fancy to export";
adamc@109 957 ([], st))
adamc@109 958 | SOME (m, ms) =>
adamc@109 959 let
adamc@249 960 val basis_n = case St.lookupBasis st of
adamc@249 961 NONE => raise Fail "Corify: Don't know number of Basis"
adamc@249 962 | SOME n => n
adamc@249 963
adamc@109 964 fun wrapSgi ((sgi, _), (wds, eds)) =
adamc@109 965 case sgi of
adamc@1125 966 L.SgiVal (s, _, t) =>
adamc@1125 967 let
adamc@1125 968 fun getPage (t, args) =
adamc@1125 969 case #1 t of
adamc@1125 970 L.CApp ((L.CModProj (basis, [], "transaction"), _),
adamc@1125 971 t' as
adamc@1125 972 (L.CApp
adamc@1125 973 ((L.CApp
adamc@1125 974 ((L.CApp ((L.CModProj (basis', [], "xml"), _),
adamc@1125 975 (L.CRecord (_, [((L.CName "Html", _),
adamc@1125 976 _)]), _)), _), _),
adamc@1125 977 _), _), _)) =>
adamc@1125 978 if basis = basis_n andalso basis' = basis_n then
adamc@1125 979 SOME (t', rev args)
adamc@1125 980 else
adamc@1125 981 NONE
adamc@1125 982 | L.TFun (dom, ran) => getPage (ran, dom :: args)
adamc@1125 983 | _ => NONE
adamc@1125 984 in
adamc@1125 985 case getPage (t, []) of
adamc@1125 986 NONE => (wds, eds)
adamc@1125 987 | SOME (ran', args) =>
adamc@1125 988 let
adamc@1125 989 val ran = (L.TRecord (L.CRecord ((L.KType, loc), []), loc), loc)
adamc@1125 990 val ranT = (L.CApp ((L.CModProj (basis_n, [], "transaction"), loc),
adamc@1125 991 ran), loc)
adamc@1125 992 val e = (L.EModProj (m, ms, s), loc)
adamc@249 993
adamc@1125 994 val ef = (L.EModProj (basis_n, [], "bind"), loc)
adamc@1125 995 val ef = (L.ECApp (ef, (L.CModProj (basis_n, [], "transaction"), loc)), loc)
adamc@1125 996 val ef = (L.ECApp (ef, ran'), loc)
adamc@1125 997 val ef = (L.ECApp (ef, ran), loc)
adamc@1125 998 val ef = (L.EApp (ef, (L.EModProj (basis_n, [], "transaction_monad"), loc)),
adamc@1125 999 loc)
adamc@1125 1000 val ea = ListUtil.foldri (fn (i, _, ea) =>
adamc@1125 1001 (L.EApp (ea, (L.ERel i, loc)), loc)) e args
adamc@1125 1002 val ef = (L.EApp (ef, ea), loc)
adamc@249 1003
adamc@1125 1004 val eat = (L.CApp ((L.CModProj (basis_n, [], "transaction"), loc),
adamc@1125 1005 ran), loc)
adamc@1125 1006 val ea = (L.EAbs ("p", ran', eat,
adamc@1125 1007 (L.EWrite (L.ERel 0, loc), loc)), loc)
adamc@249 1008
adamc@1125 1009 val (e, tf) = ListUtil.foldri (fn (i, t, (e, tf)) =>
adamc@1125 1010 ((L.EAbs ("x" ^ Int.toString i,
adamc@1125 1011 t, tf, e), loc),
adamc@1125 1012 (L.TFun (t, tf), loc)))
adamc@1125 1013 ((L.EApp (ef, ea), loc), ranT) args
adamc@1125 1014 in
adamc@1125 1015 ((L.DVal ("wrap_" ^ s, 0, tf, e), loc) :: wds,
adamc@1125 1016 (fn st =>
adamc@1125 1017 case #1 (corifyExp st (L.EModProj (en, [], "wrap_" ^ s), loc)) of
adamc@1125 1018 L'.ENamed n => (L'.DExport (L'.Link, n, false), loc)
adamc@1125 1019 | _ => raise Fail "Corify: Value to export didn't corify properly")
adamc@1125 1020 :: eds)
adamc@1125 1021 end
adamc@1125 1022 end
adamc@109 1023 | _ => (wds, eds)
adamc@102 1024
adamc@109 1025 val (wds, eds) = foldl wrapSgi ([], []) sgis
adamc@109 1026 val wrapper = (L.StrConst wds, loc)
adamc@376 1027 val mst = St.lookupStrById st m
adamc@1126 1028 val mst = foldl St.lookupStrByName mst ms
adamc@376 1029 val (ds, {inner, outer}) = corifyStr (St.name mst) (wrapper, st)
adamc@109 1030 val st = St.bindStr outer "wrapper" en inner
adamc@249 1031
adamc@109 1032 val ds = ds @ map (fn f => f st) eds
adamc@109 1033 in
adamc@109 1034 (ds, st)
adamc@109 1035 end
adamc@109 1036 end
adamc@109 1037 | _ => raise Fail "Non-const signature for 'export'")
adamc@48 1038
adamc@707 1039 | L.DTable (_, x, n, c, pe, pc, ce, cc) =>
adamc@249 1040 let
adamc@249 1041 val (st, n) = St.bindVal st x n
adamc@768 1042 val s = relify (doRestify Settings.Table (mods, x))
adamc@249 1043 in
adamc@707 1044 ([(L'.DTable (x, n, corifyCon st c, s,
adamc@707 1045 corifyExp st pe, corifyCon st pc,
adamc@707 1046 corifyExp st ce, corifyCon st cc), loc)], st)
adamc@249 1047 end
adamc@338 1048 | L.DSequence (_, x, n) =>
adamc@338 1049 let
adamc@338 1050 val (st, n) = St.bindVal st x n
adamc@768 1051 val s = relify (doRestify Settings.Sequence (mods, x))
adamc@338 1052 in
adamc@338 1053 ([(L'.DSequence (x, n, s), loc)], st)
adamc@338 1054 end
adamc@754 1055 | L.DView (_, x, n, e, c) =>
adamc@754 1056 let
adamc@754 1057 val (st, n) = St.bindVal st x n
adamc@768 1058 val s = relify (doRestify Settings.View (mods, x))
adamc@754 1059 in
adamc@754 1060 ([(L'.DView (x, n, s, corifyExp st e, corifyCon st c), loc)], st)
adamc@754 1061 end
adamc@246 1062
adamc@271 1063 | L.DDatabase s => ([(L'.DDatabase s, loc)], st)
adamc@271 1064
adamc@461 1065 | L.DCookie (_, x, n, c) =>
adamc@461 1066 let
adamc@461 1067 val (st, n) = St.bindVal st x n
adamc@768 1068 val s = doRestify Settings.Cookie (mods, x)
adamc@461 1069 in
adamc@461 1070 ([(L'.DCookie (x, n, corifyCon st c, s), loc)], st)
adamc@461 1071 end
adamc@720 1072 | L.DStyle (_, x, n) =>
adamc@718 1073 let
adamc@718 1074 val (st, n) = St.bindVal st x n
adamc@768 1075 val s = relify (doRestify Settings.Style (mods, x))
adamc@718 1076 in
adamc@720 1077 ([(L'.DStyle (x, n, s), loc)], st)
adamc@718 1078 end
adamc@461 1079
adamc@1075 1080 | L.DTask (e1, e2) =>
adamc@1075 1081 ([(L'.DTask (corifyExp st e1, corifyExp st e2), loc)], st)
adamc@1073 1082
adamc@1199 1083 | L.DPolicy e1 =>
adamc@1199 1084 ([(L'.DPolicy (corifyExp st e1), loc)], st)
adamc@1199 1085
adam@1294 1086 | L.DOnError (m, ms, x) =>
adam@1294 1087 let
adam@1294 1088 val st = St.lookupStrById st m
adam@1294 1089 val st = foldl St.lookupStrByName st ms
adam@1294 1090 in
adam@1294 1091 case St.lookupValByName st x of
adam@1294 1092 St.ENormal n => ([(L'.DOnError n, loc)], st)
adam@1294 1093 | _ => (ErrorMsg.errorAt loc "Wrong type of identifier for 'onError'";
adam@1294 1094 ([], st))
adam@1294 1095 end
adam@1294 1096
adamc@376 1097 and corifyStr mods ((str, _), st) =
adamc@39 1098 case str of
adamc@39 1099 L.StrConst ds =>
adamc@39 1100 let
adamc@376 1101 val st = St.enter (st, mods)
adamc@376 1102 val (ds, st) = ListUtil.foldlMapConcat (corifyDecl mods) st ds
adamc@39 1103 in
adamc@39 1104 (ds, St.leave st)
adamc@39 1105 end
adamc@39 1106 | L.StrVar n => ([], {inner = St.lookupStrById st n, outer = st})
adamc@39 1107 | L.StrProj (str, x) =>
adamc@39 1108 let
adamc@376 1109 val (ds, {inner, outer}) = corifyStr mods (str, st)
adamc@39 1110 in
adamc@39 1111 (ds, {inner = St.lookupStrByName (x, inner), outer = outer})
adamc@39 1112 end
adamc@46 1113 | L.StrFun _ => raise Fail "Corify of nested functor definition"
adamc@46 1114 | L.StrApp (str1, str2) =>
adamc@46 1115 let
adamc@46 1116 fun unwind' (str, _) =
adamc@46 1117 case str of
adamc@46 1118 L.StrVar n => St.lookupStrById st n
adamc@46 1119 | L.StrProj (str, x) => St.lookupStrByName (x, unwind' str)
adamc@46 1120 | _ => raise Fail "Corify of fancy functor application [1]"
adamc@46 1121
adamc@46 1122 fun unwind (str, _) =
adamc@46 1123 case str of
adamc@46 1124 L.StrVar n => St.lookupFunctorById st n
adamc@46 1125 | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str)
adamc@46 1126 | _ => raise Fail "Corify of fancy functor application [2]"
adamc@46 1127
adamc@423 1128 val (xa, na, body) = unwind str1
adamc@46 1129
adamc@376 1130 val (ds1, {inner = inner', outer}) = corifyStr mods (str2, st)
adamc@376 1131
adamc@423 1132 val (ds2, {inner, outer}) = corifyStr mods (body, St.bindStr outer xa na inner')
adamc@46 1133 in
adamc@146 1134 (ds1 @ ds2, {inner = St.bindStr inner xa na inner', outer = outer})
adamc@46 1135 end
adamc@31 1136
adamc@39 1137 fun maxName ds = foldl (fn ((d, _), n) =>
adamc@39 1138 case d of
adamc@39 1139 L.DCon (_, n', _, _) => Int.max (n, n')
adamc@806 1140 | L.DDatatype dts => foldl (fn ((_, n', _, _), n) => Int.max (n, n')) n dts
adamc@191 1141 | L.DDatatypeImp (_, n', _, _, _, _, _) => Int.max (n, n')
adamc@124 1142 | L.DVal (_, n', _, _) => Int.max (n, n')
adamc@124 1143 | L.DValRec vis => foldl (fn ((_, n', _, _), n) => Int.max (n, n)) n vis
adamc@39 1144 | L.DSgn (_, n', _) => Int.max (n, n')
adamc@48 1145 | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str))
adamc@100 1146 | L.DFfiStr (_, n', _) => Int.max (n, n')
adamc@246 1147 | L.DExport _ => n
adamc@707 1148 | L.DTable (_, _, n', _, _, _, _, _) => Int.max (n, n')
adamc@338 1149 | L.DSequence (_, _, n') => Int.max (n, n')
adamc@754 1150 | L.DView (_, _, n', _, _) => Int.max (n, n')
adamc@461 1151 | L.DDatabase _ => n
adamc@718 1152 | L.DCookie (_, _, n', _) => Int.max (n, n')
adamc@1073 1153 | L.DStyle (_, _, n') => Int.max (n, n')
adamc@1199 1154 | L.DTask _ => n
adam@1294 1155 | L.DPolicy _ => n
adam@1294 1156 | L.DOnError _ => n)
adamc@249 1157 0 ds
adamc@39 1158
adamc@39 1159 and maxNameStr (str, _) =
adamc@39 1160 case str of
adamc@39 1161 L.StrConst ds => maxName ds
adamc@39 1162 | L.StrVar n => n
adamc@39 1163 | L.StrProj (str, _) => maxNameStr str
adamc@45 1164 | L.StrFun (_, _, _, _, str) => maxNameStr str
adamc@45 1165 | L.StrApp (str1, str2) => Int.max (maxNameStr str1, maxNameStr str2)
adamc@39 1166
adamc@39 1167 fun corify ds =
adamc@39 1168 let
adamc@39 1169 val () = reset (maxName ds + 1)
adamc@146 1170
adamc@376 1171 val (ds, _) = ListUtil.foldlMapConcat (corifyDecl []) St.empty ds
adamc@39 1172 in
adamc@39 1173 ds
adamc@39 1174 end
adamc@16 1175
adamc@16 1176 end