Mercurial > urweb

annotate src/corify.sml @ 2227:adb49db02af4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix type in flush FFI call to option string (rather than string).
author Ziv Scully <ziv@mit.edu>
date Tue, 31 Mar 2015 04:10:46 -0400
parents 3d10ae22abd6
children
rev   line source
adam@1704 1 (* Copyright (c) 2008-2012, 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
adam@1989 67 end
adam@1989 68
adam@1989 69 fun getCounter () = !count
adam@1989 70 fun setCounter n = count := n
adamc@39 71
adamc@39 72 end
adamc@39 73
adamc@39 74 structure St : sig
adamc@39 75 type t
adamc@39 76
adamc@39 77 val empty : t
adamc@39 78
adamc@146 79 val debug : t -> unit
adamc@146 80
adamc@376 81 val name : t -> string list
adamc@376 82
adamc@376 83 val enter : t * string list -> t
adamc@39 84 val leave : t -> {outer : t, inner : t}
adamc@192 85 val ffi : string -> L'.con SM.map -> (string * string list * L'.con option * L'.datatype_kind) SM.map -> t
adamc@39 86
adamc@249 87 val basisIs : t * int -> t
adamc@249 88 val lookupBasis : t -> int option
adamc@249 89
adamc@73 90 datatype core_con =
adamc@73 91 CNormal of int
adamc@73 92 | CFfi of string
adamc@73 93 val bindCon : t -> string -> int -> t * int
adamc@73 94 val lookupConById : t -> int -> int option
adamc@73 95 val lookupConByName : t -> string -> core_con
adamc@48 96
adam@1704 97 val bindConstructor : t -> string -> int -> t * int
adam@1704 98 val bindConstructorAs : t -> string -> int -> L'.patCon -> t
adamc@186 99 val lookupConstructorByNameOpt : t -> string -> L'.patCon option
adamc@177 100 val lookupConstructorByName : t -> string -> L'.patCon
adamc@177 101 val lookupConstructorById : t -> int -> L'.patCon
adam@1990 102 val lookupConstructorByIdOpt : t -> int -> L'.patCon option
adamc@249 103
adamc@249 104 datatype core_val =
adamc@249 105 ENormal of int
adamc@249 106 | EFfi of string * L'.con
adamc@249 107 val bindVal : t -> string -> int -> t * int
adam@1704 108 val bindConstructorVal : t -> string -> int -> int -> t
adamc@249 109 val lookupValById : t -> int -> int option
adamc@249 110 val lookupValByName : t -> string -> core_val
adamc@177 111
adamc@249 112 val bindStr : t -> string -> int -> t -> t
adamc@249 113 val lookupStrById : t -> int -> t
adam@1989 114 val lookupStrByIdOpt : t -> int -> t option
adamc@249 115 val lookupStrByName : string * t -> t
adamc@339 116 val lookupStrByNameOpt : string * t -> t option
adamc@39 117
adamc@423 118 val bindFunctor : t -> string -> int -> string -> int -> L.str -> t
adamc@423 119 val lookupFunctorById : t -> int -> string * int * L.str
adam@1989 120 val lookupFunctorByIdOpt : t -> int -> (string * int * L.str) option
adamc@423 121 val lookupFunctorByName : string * t -> string * int * L.str
adamc@249 122 end = struct
adamc@46 123
adamc@249 124 datatype flattening =
adamc@376 125 FNormal of {name : string list,
adamc@376 126 cons : int SM.map,
adamc@249 127 constructors : L'.patCon SM.map,
adamc@249 128 vals : int SM.map,
adamc@249 129 strs : flattening SM.map,
adamc@423 130 funs : (string * int * L.str) SM.map}
adamc@249 131 | FFfi of {mod : string,
adamc@249 132 vals : L'.con SM.map,
adamc@249 133 constructors : (string * string list * L'.con option * L'.datatype_kind) SM.map}
adamc@39 134
adamc@249 135 type t = {
adamc@249 136 basis : int option,
adamc@249 137 cons : int IM.map,
adamc@249 138 constructors : L'.patCon IM.map,
adamc@249 139 vals : int IM.map,
adamc@249 140 strs : flattening IM.map,
adamc@423 141 funs : (string * int * L.str) IM.map,
adamc@249 142 current : flattening,
adamc@249 143 nested : flattening list
adamc@249 144 }
adamc@39 145
adamc@249 146 val empty = {
adamc@249 147 basis = NONE,
adamc@249 148 cons = IM.empty,
adamc@249 149 constructors = IM.empty,
adamc@249 150 vals = IM.empty,
adamc@249 151 strs = IM.empty,
adamc@249 152 funs = IM.empty,
adamc@376 153 current = FNormal { name = [], cons = SM.empty, constructors = SM.empty,
adamc@376 154 vals = SM.empty, strs = SM.empty, funs = SM.empty },
adamc@249 155 nested = []
adamc@249 156 }
adamc@39 157
adamc@376 158 fun debug ({current = FNormal {cons, constructors, vals, strs, funs, ...}, ...} : t) =
adamc@249 159 print ("cons: " ^ Int.toString (SM.numItems cons) ^ "; "
adamc@249 160 ^ "constructors: " ^ Int.toString (SM.numItems constructors) ^ "; "
adamc@249 161 ^ "vals: " ^ Int.toString (SM.numItems vals) ^ "; "
adamc@249 162 ^ "strs: " ^ Int.toString (SM.numItems strs) ^ "; "
adamc@249 163 ^ "funs: " ^ Int.toString (SM.numItems funs) ^ "\n")
adamc@249 164 | debug _ = print "Not normal!\n"
adamc@146 165
adamc@376 166 fun name ({current = FNormal {name, ...}, ...} : t) = name
adamc@376 167 | name {current = FFfi {mod = name, ...}, ...} = [name]
adamc@376 168
adamc@249 169 fun basisIs ({cons, constructors, vals, strs, funs, current, nested, ...} : t, basis) =
adamc@249 170 {basis = SOME basis,
adamc@249 171 cons = cons,
adamc@249 172 constructors = constructors,
adamc@249 173 vals = vals,
adamc@249 174 strs = strs,
adamc@249 175 funs = funs,
adamc@249 176 current = current,
adamc@249 177 nested = nested}
adamc@48 178
adamc@249 179 fun lookupBasis ({basis, ...} : t) = basis
adamc@73 180
adamc@249 181 datatype core_con =
adamc@249 182 CNormal of int
adamc@249 183 | CFfi of string
adamc@39 184
adamc@249 185 datatype core_val =
adamc@249 186 ENormal of int
adamc@249 187 | EFfi of string * L'.con
adamc@188 188
adamc@249 189 fun bindCon {basis, cons, constructors, vals, strs, funs, current, nested} s n =
adamc@249 190 let
adamc@249 191 val n' = alloc ()
adamc@188 192
adamc@249 193 val current =
adamc@249 194 case current of
adamc@249 195 FFfi _ => raise Fail "Binding inside FFfi"
adamc@376 196 | FNormal {name, cons, constructors, vals, strs, funs} =>
adamc@376 197 FNormal {name = name,
adamc@376 198 cons = SM.insert (cons, s, n'),
adamc@249 199 constructors = constructors,
adamc@249 200 vals = vals,
adamc@249 201 strs = strs,
adamc@249 202 funs = funs}
adamc@249 203 in
adamc@249 204 ({basis = basis,
adamc@249 205 cons = IM.insert (cons, n, n'),
adamc@177 206 constructors = constructors,
adamc@73 207 vals = vals,
adamc@39 208 strs = strs,
adamc@46 209 funs = funs,
adamc@39 210 current = current,
adamc@249 211 nested = nested},
adamc@249 212 n')
adamc@249 213 end
adamc@39 214
adamc@249 215 fun lookupConById ({cons, ...} : t) n = IM.find (cons, n)
adamc@39 216
adamc@249 217 fun lookupConByName ({current, ...} : t) x =
adamc@249 218 case current of
adamc@249 219 FFfi {mod = m, ...} => CFfi m
adamc@249 220 | FNormal {cons, ...} =>
adamc@249 221 case SM.find (cons, x) of
adam@1527 222 NONE => raise Fail ("Corify.St.lookupConByName " ^ x)
adamc@249 223 | SOME n => CNormal n
adamc@249 224
adamc@249 225 fun bindVal {basis, cons, constructors, vals, strs, funs, current, nested} s n =
adamc@249 226 let
adamc@249 227 val n' = alloc ()
adamc@249 228
adamc@249 229 val current =
adamc@249 230 case current of
adamc@249 231 FFfi _ => raise Fail "Binding inside FFfi"
adamc@376 232 | FNormal {name, cons, constructors, vals, strs, funs} =>
adamc@376 233 FNormal {name = name,
adamc@376 234 cons = cons,
adamc@249 235 constructors = constructors,
adamc@249 236 vals = SM.insert (vals, s, n'),
adamc@249 237 strs = strs,
adamc@249 238 funs = funs}
adamc@249 239 in
adamc@249 240 ({basis = basis,
adamc@249 241 cons = cons,
adamc@249 242 constructors = constructors,
adamc@249 243 vals = IM.insert (vals, n, n'),
adamc@249 244 strs = strs,
adamc@249 245 funs = funs,
adamc@249 246 current = current,
adamc@249 247 nested = nested},
adamc@249 248 n')
adamc@249 249 end
adamc@249 250
adam@1704 251 fun bindConstructorVal {basis, cons, constructors, vals, strs, funs, current, nested} s n n' =
adamc@249 252 let
adamc@249 253 val current =
adamc@249 254 case current of
adamc@249 255 FFfi _ => raise Fail "Binding inside FFfi"
adamc@376 256 | FNormal {name, cons, constructors, vals, strs, funs} =>
adamc@376 257 FNormal {name = name,
adamc@376 258 cons = cons,
adamc@249 259 constructors = constructors,
adam@1704 260 vals = SM.insert (vals, s, n'),
adamc@249 261 strs = strs,
adamc@249 262 funs = funs}
adamc@249 263 in
adamc@249 264 {basis = basis,
adamc@249 265 cons = cons,
adamc@249 266 constructors = constructors,
adam@1704 267 vals = IM.insert (vals, n, n'),
adamc@249 268 strs = strs,
adamc@249 269 funs = funs,
adamc@249 270 current = current,
adamc@249 271 nested = nested}
adamc@249 272 end
adamc@249 273
adamc@249 274
adamc@249 275 fun lookupValById ({vals, ...} : t) n = IM.find (vals, n)
adamc@249 276
adamc@249 277 fun lookupValByName ({current, ...} : t) x =
adamc@249 278 case current of
adamc@249 279 FFfi {mod = m, vals, ...} =>
adamc@249 280 (case SM.find (vals, x) of
adam@1314 281 NONE => raise Fail ("Corify.St.lookupValByName: no type for FFI val " ^ x)
adamc@249 282 | SOME t => EFfi (m, t))
adam@1314 283 | FNormal {name, vals, ...} =>
adamc@249 284 case SM.find (vals, x) of
adam@1527 285 NONE => raise Fail ("Corify.St.lookupValByName " ^ String.concatWith "." (rev name) ^ "." ^ x)
adamc@249 286 | SOME n => ENormal n
adamc@249 287
adam@1704 288 fun bindConstructorAs {basis, cons, constructors, vals, strs, funs, current, nested} s n c' =
adamc@249 289 let
adamc@249 290 val current =
adamc@249 291 case current of
adamc@249 292 FFfi _ => raise Fail "Binding inside FFfi"
adamc@376 293 | FNormal {name, cons, constructors, vals, strs, funs} =>
adamc@376 294 FNormal {name = name,
adamc@376 295 cons = cons,
adam@1704 296 constructors = SM.insert (constructors, s, c'),
adamc@249 297 vals = vals,
adamc@249 298 strs = strs,
adamc@249 299 funs = funs}
adamc@249 300 in
adamc@249 301 {basis = basis,
adamc@249 302 cons = cons,
adam@1704 303 constructors = IM.insert (constructors, n, c'),
adamc@249 304 vals = vals,
adamc@249 305 strs = strs,
adamc@249 306 funs = funs,
adamc@249 307 current = current,
adamc@249 308 nested = nested}
adamc@249 309 end
adamc@249 310
adam@1704 311 fun bindConstructor st s n =
adam@1704 312 let
adam@1704 313 val n' = alloc ()
adam@1704 314 val c' = L'.PConVar n'
adam@1704 315 in
adam@1704 316 (bindConstructorAs st s n c', n')
adam@1704 317 end
adam@1704 318
adamc@249 319 fun lookupConstructorById ({constructors, ...} : t) n =
adamc@249 320 case IM.find (constructors, n) of
adamc@249 321 NONE => raise Fail "Corify.St.lookupConstructorById"
adamc@249 322 | SOME x => x
adamc@249 323
adam@1990 324 fun lookupConstructorByIdOpt ({constructors, ...} : t) n =
adam@1990 325 IM.find (constructors, n)
adam@1990 326
adamc@249 327 fun lookupConstructorByNameOpt ({current, ...} : t) x =
adamc@249 328 case current of
adamc@249 329 FFfi {mod = m, constructors, ...} =>
adamc@249 330 (case SM.find (constructors, x) of
adamc@188 331 NONE => NONE
adamc@249 332 | SOME (n, xs, to, dk) => SOME (L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk}))
adamc@249 333 | FNormal {constructors, ...} =>
adamc@249 334 case SM.find (constructors, x) of
adamc@249 335 NONE => NONE
adamc@249 336 | SOME n => SOME n
adamc@39 337
adamc@249 338 fun lookupConstructorByName ({current, ...} : t) x =
adamc@249 339 case current of
adamc@249 340 FFfi {mod = m, constructors, ...} =>
adamc@249 341 (case SM.find (constructors, x) of
adamc@249 342 NONE => raise Fail "Corify.St.lookupConstructorByName [1]"
adamc@249 343 | SOME (n, xs, to, dk) => L'.PConFfi {mod = m, datatyp = n, params = xs, con = x, arg = to, kind = dk})
adamc@249 344 | FNormal {constructors, ...} =>
adamc@249 345 case SM.find (constructors, x) of
adamc@249 346 NONE => raise Fail "Corify.St.lookupConstructorByName [2]"
adamc@249 347 | SOME n => n
adamc@73 348
adamc@376 349 fun enter ({basis, cons, constructors, vals, strs, funs, current, nested}, name) =
adamc@249 350 {basis = basis,
adamc@249 351 cons = cons,
adamc@249 352 constructors = constructors,
adamc@249 353 vals = vals,
adamc@249 354 strs = strs,
adamc@249 355 funs = funs,
adamc@376 356 current = FNormal {name = name,
adamc@376 357 cons = SM.empty,
adamc@249 358 constructors = SM.empty,
adamc@249 359 vals = SM.empty,
adamc@249 360 strs = SM.empty,
adamc@249 361 funs = SM.empty},
adamc@249 362 nested = current :: nested}
adamc@73 363
adamc@249 364 fun dummy (b, f) = {basis = b,
adamc@249 365 cons = IM.empty,
adamc@249 366 constructors = IM.empty,
adamc@249 367 vals = IM.empty,
adamc@249 368 strs = IM.empty,
adamc@249 369 funs = IM.empty,
adamc@249 370 current = f,
adamc@249 371 nested = []}
adamc@163 372
adamc@249 373 fun leave {basis, cons, constructors, vals, strs, funs, current, nested = m1 :: rest} =
adamc@249 374 {outer = {basis = basis,
adamc@249 375 cons = cons,
adamc@249 376 constructors = constructors,
adamc@249 377 vals = vals,
adamc@249 378 strs = strs,
adamc@249 379 funs = funs,
adamc@249 380 current = m1,
adamc@249 381 nested = rest},
adamc@249 382 inner = dummy (basis, current)}
adamc@249 383 | leave _ = raise Fail "Corify.St.leave"
adamc@177 384
adamc@249 385 fun ffi m vals constructors = dummy (NONE, FFfi {mod = m, vals = vals, constructors = constructors})
adamc@73 386
adamc@249 387 fun bindStr ({basis, cons, constructors, vals, strs, funs,
adamc@376 388 current = FNormal {name, cons = mcons, constructors = mconstructors,
adamc@249 389 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
adamc@249 390 x n ({current = f, ...} : t) =
adamc@249 391 {basis = basis,
adamc@249 392 cons = cons,
adamc@249 393 constructors = constructors,
adamc@249 394 vals = vals,
adamc@249 395 strs = IM.insert (strs, n, f),
adamc@249 396 funs = funs,
adamc@376 397 current = FNormal {name = name,
adamc@376 398 cons = mcons,
adamc@249 399 constructors = mconstructors,
adamc@249 400 vals = mvals,
adamc@249 401 strs = SM.insert (mstrs, x, f),
adamc@249 402 funs = mfuns},
adamc@249 403 nested = nested}
adamc@249 404 | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr"
adamc@73 405
adamc@249 406 fun lookupStrById ({basis, strs, ...} : t) n =
adamc@249 407 case IM.find (strs, n) of
adamc@480 408 NONE => raise Fail ("Corify.St.lookupStrById(" ^ Int.toString n ^ ")")
adamc@249 409 | SOME f => dummy (basis, f)
adamc@177 410
adam@1989 411 fun lookupStrByIdOpt ({basis, strs, ...} : t) n =
adam@1989 412 case IM.find (strs, n) of
adam@1989 413 NONE => NONE
adam@1989 414 | SOME f => SOME (dummy (basis, f))
adam@1989 415
adamc@249 416 fun lookupStrByName (m, {basis, current = FNormal {strs, ...}, ...} : t) =
adamc@249 417 (case SM.find (strs, m) of
adamc@339 418 NONE => raise Fail "Corify.St.lookupStrByName [1]"
adamc@249 419 | SOME f => dummy (basis, f))
adamc@339 420 | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName [2]"
adamc@339 421
adamc@339 422 fun lookupStrByNameOpt (m, {basis, current = FNormal {strs, ...}, ...} : t) =
adamc@339 423 (case SM.find (strs, m) of
adamc@339 424 NONE => NONE
adamc@339 425 | SOME f => SOME (dummy (basis, f)))
adamc@339 426 | lookupStrByNameOpt _ = NONE
adamc@177 427
adamc@249 428 fun bindFunctor ({basis, cons, constructors, vals, strs, funs,
adamc@376 429 current = FNormal {name, cons = mcons, constructors = mconstructors,
adamc@249 430 vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
adamc@423 431 x n xa na str =
adamc@249 432 {basis = basis,
adamc@249 433 cons = cons,
adamc@249 434 constructors = constructors,
adamc@249 435 vals = vals,
adamc@249 436 strs = strs,
adamc@423 437 funs = IM.insert (funs, n, (xa, na, str)),
adamc@376 438 current = FNormal {name = name,
adamc@376 439 cons = mcons,
adamc@249 440 constructors = mconstructors,
adamc@249 441 vals = mvals,
adamc@249 442 strs = mstrs,
adamc@423 443 funs = SM.insert (mfuns, x, (xa, na, str))},
adamc@249 444 nested = nested}
adamc@423 445 | bindFunctor _ _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
adamc@186 446
adamc@249 447 fun lookupFunctorById ({funs, ...} : t) n =
adamc@249 448 case IM.find (funs, n) of
adamc@249 449 NONE => raise Fail "Corify.St.lookupFunctorById"
adamc@249 450 | SOME v => v
adamc@177 451
adam@1989 452 fun lookupFunctorByIdOpt ({funs, ...} : t) n =
adam@1989 453 IM.find (funs, n)
adam@1989 454
adamc@249 455 fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) =
adamc@249 456 (case SM.find (funs, m) of
adamc@1146 457 NONE => raise Fail ("Corify.St.lookupFunctorByName " ^ m ^ "[1]")
adamc@249 458 | SOME v => v)
adamc@339 459 | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName [2]"
adamc@39 460
adamc@249 461 end
adamc@39 462
adamc@39 463
adamc@249 464 fun corifyKind (k, loc) =
adamc@249 465 case k of
adamc@249 466 L.KType => (L'.KType, loc)
adamc@249 467 | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc)
adamc@249 468 | L.KName => (L'.KName, loc)
adamc@249 469 | L.KRecord k => (L'.KRecord (corifyKind k), loc)
adamc@249 470 | L.KUnit => (L'.KUnit, loc)
adamc@249 471 | L.KTuple ks => (L'.KTuple (map corifyKind ks), loc)
adamc@48 472
adamc@626 473 | L.KRel n => (L'.KRel n, loc)
adamc@626 474 | L.KFun (x, k) => (L'.KFun (x, corifyKind k), loc)
adamc@626 475
adamc@249 476 fun corifyCon st (c, loc) =
adamc@249 477 case c of
adamc@249 478 L.TFun (t1, t2) => (L'.TFun (corifyCon st t1, corifyCon st t2), loc)
adamc@249 479 | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc)
adamc@626 480 | L.TKFun (x, t) => (L'.TKFun (x, corifyCon st t), loc)
adamc@249 481 | L.TRecord c => (L'.TRecord (corifyCon st c), loc)
adamc@39 482
adamc@249 483 | L.CRel n => (L'.CRel n, loc)
adamc@249 484 | L.CNamed n =>
adamc@249 485 (case St.lookupConById st n of
adamc@249 486 NONE => (L'.CNamed n, loc)
adamc@249 487 | SOME n => (L'.CNamed n, loc))
adamc@249 488 | L.CModProj (m, ms, x) =>
adamc@249 489 let
adamc@249 490 val st = St.lookupStrById st m
adamc@249 491 val st = foldl St.lookupStrByName st ms
adamc@249 492 in
adamc@249 493 case St.lookupConByName st x of
adamc@249 494 St.CNormal n => (L'.CNamed n, loc)
kkallio@1455 495 | St.CFfi m =>
kkallio@1455 496 if (m, x) = ("Basis", "unit") then
kkallio@1455 497 (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc)
kkallio@1455 498 else
kkallio@1455 499 (L'.CFfi (m, x), loc)
adamc@249 500 end
adamc@39 501
adamc@249 502 | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc)
adamc@249 503 | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc)
adamc@39 504
adamc@626 505 | L.CKApp (c1, k) => (L'.CKApp (corifyCon st c1, corifyKind k), loc)
adamc@626 506 | L.CKAbs (x, c) => (L'.CKAbs (x, corifyCon st c), loc)
adamc@626 507
adamc@249 508 | L.CName s => (L'.CName s, loc)
adamc@46 509
adamc@249 510 | L.CRecord (k, xcs) =>
adamc@249 511 (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon st c1, corifyCon st c2)) xcs), loc)
adamc@249 512 | L.CConcat (c1, c2) => (L'.CConcat (corifyCon st c1, corifyCon st c2), loc)
adamc@621 513 | L.CMap (k1, k2) => (L'.CMap (corifyKind k1, corifyKind k2), loc)
adamc@249 514 | L.CUnit => (L'.CUnit, loc)
adamc@46 515
adamc@249 516 | L.CTuple cs => (L'.CTuple (map (corifyCon st) cs), loc)
adamc@249 517 | L.CProj (c, n) => (L'.CProj (corifyCon st c, n), loc)
adamc@213 518
adamc@249 519 fun corifyPatCon st pc =
adamc@249 520 case pc of
adamc@249 521 L.PConVar n => St.lookupConstructorById st n
adamc@249 522 | L.PConProj (m1, ms, x) =>
adamc@249 523 let
adamc@249 524 val st = St.lookupStrById st m1
adamc@249 525 val st = foldl St.lookupStrByName st ms
adamc@249 526 in
adamc@249 527 St.lookupConstructorByName st x
adamc@249 528 end
adamc@46 529
adamc@249 530 fun corifyPat st (p, loc) =
adamc@249 531 case p of
adamc@249 532 L.PWild => (L'.PWild, loc)
adamc@249 533 | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc)
adamc@249 534 | L.PPrim p => (L'.PPrim p, loc)
adamc@249 535 | L.PCon (dk, pc, ts, po) => (L'.PCon (dk, corifyPatCon st pc, map (corifyCon st) ts,
adamc@249 536 Option.map (corifyPat st) po), loc)
adamc@249 537 | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc)
adamc@39 538
adamc@249 539 fun corifyExp st (e, loc) =
adamc@249 540 case e of
adamc@249 541 L.EPrim p => (L'.EPrim p, loc)
adamc@249 542 | L.ERel n => (L'.ERel n, loc)
adamc@249 543 | L.ENamed n =>
adamc@249 544 (case St.lookupValById st n of
adamc@249 545 NONE => (L'.ENamed n, loc)
adamc@249 546 | SOME n => (L'.ENamed n, loc))
adamc@249 547 | L.EModProj (m, ms, x) =>
adamc@249 548 let
adamc@249 549 val st = St.lookupStrById st m
adamc@249 550 val st = foldl St.lookupStrByName st ms
adamc@249 551 in
adamc@249 552 case St.lookupConstructorByNameOpt st x of
adamc@249 553 SOME (pc as L'.PConFfi {mod = m, datatyp, params, arg, kind, ...}) =>
adamc@249 554 let
adamc@249 555 val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) params
adamc@249 556 val e = case arg of
adamc@249 557 NONE => (L'.ECon (kind, pc, args, NONE), loc)
adamc@249 558 | SOME dom => (L'.EAbs ("x", dom, (L'.CFfi (m, datatyp), loc),
adamc@249 559 (L'.ECon (kind, pc, args, SOME (L'.ERel 0, loc)), loc)), loc)
adamc@192 560
adamc@249 561 val k = (L'.KType, loc)
adamc@249 562 in
adamc@249 563 foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e params
adamc@249 564 end
adamc@249 565 | _ =>
adamc@249 566 case St.lookupValByName st x of
adamc@249 567 St.ENormal n => (L'.ENamed n, loc)
adamc@249 568 | St.EFfi (m, t) =>
adamc@249 569 case t of
adam@1701 570 (L'.CApp ((L'.CFfi ("Basis", "transaction"), _), dom), _) =>
adamc@765 571 (L'.EAbs ("arg", dom, (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc),
adamc@765 572 (L'.EFfiApp (m, x, []), loc)), loc)
adamc@249 573 | t as (L'.TFun _, _) =>
adamc@249 574 let
adamc@249 575 fun getArgs (all as (t, _), args) =
adamc@249 576 case t of
adamc@249 577 L'.TFun (dom, ran) => getArgs (ran, dom :: args)
adamc@249 578 | _ => (all, rev args)
adamc@39 579
adamc@249 580 val (result, args) = getArgs (t, [])
adamc@456 581 val (isTransaction, result) =
adamc@456 582 case result of
adamc@456 583 (L'.CApp ((L'.CFfi ("Basis", "transaction"), _),
adamc@456 584 result), _) => (true, result)
adamc@456 585 | _ => (false, result)
adamc@16 586
adamc@456 587 fun makeApp n =
adamc@456 588 let
adam@1663 589 val (actuals, _) = foldr (fn (t, (actuals, n)) =>
adam@1663 590 (((L'.ERel n, loc), t) :: actuals,
adamc@456 591 n + 1)) ([], n) args
adamc@456 592 in
adamc@456 593 (L'.EFfiApp (m, x, actuals), loc)
adamc@456 594 end
adamc@456 595 val unit = (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc)
adamc@456 596 val (result, app) =
adamc@456 597 if isTransaction then
adamc@456 598 ((L'.TFun (unit, result), loc),
adamc@456 599 (L'.EAbs ("_",
adamc@456 600 unit,
adamc@456 601 result,
adamc@456 602 makeApp 1), loc))
adamc@456 603 else
adamc@456 604 (result, makeApp 0)
adamc@456 605
adamc@249 606 val (abs, _, _) = foldr (fn (t, (abs, ran, n)) =>
adamc@249 607 ((L'.EAbs ("arg" ^ Int.toString n,
adamc@249 608 t,
adamc@249 609 ran,
adamc@249 610 abs), loc),
adamc@249 611 (L'.TFun (t, ran), loc),
adamc@249 612 n - 1)) (app, result, length args - 1) args
adamc@249 613 in
adamc@249 614 abs
adamc@249 615 end
adamc@249 616 | _ => (L'.EFfi (m, x), loc)
adamc@249 617 end
adamc@249 618 | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc)
adamc@249 619 | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc)
adamc@249 620 | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc)
adamc@249 621 | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc)
adamc@626 622 | L.EKApp (e1, k) => (L'.EKApp (corifyExp st e1, corifyKind k), loc)
adamc@626 623 | L.EKAbs (x, e1) => (L'.EKAbs (x, corifyExp st e1), loc)
adamc@16 624
adamc@249 625 | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) =>
adamc@249 626 (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc)
adamc@249 627 | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c,
adamc@249 628 {field = corifyCon st field, rest = corifyCon st rest}), loc)
adamc@445 629 | L.EConcat (e1, c1, e2, c2) => (L'.EConcat (corifyExp st e1, corifyCon st c1, corifyExp st e2,
adamc@445 630 corifyCon st c2), loc)
adamc@249 631 | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c,
adamc@249 632 {field = corifyCon st field, rest = corifyCon st rest}), loc)
adamc@493 633 | L.ECutMulti (e1, c, {rest}) => (L'.ECutMulti (corifyExp st e1, corifyCon st c,
adamc@493 634 {rest = corifyCon st rest}), loc)
adamc@34 635
adamc@249 636 | L.ECase (e, pes, {disc, result}) =>
adamc@249 637 (L'.ECase (corifyExp st e,
adamc@249 638 map (fn (p, e) => (corifyPat st p, corifyExp st e)) pes,
adamc@249 639 {disc = corifyCon st disc, result = corifyCon st result}),
adamc@249 640 loc)
adamc@16 641
adamc@249 642 | L.EWrite e => (L'.EWrite (corifyExp st e), loc)
adamc@16 643
adamc@450 644 | L.ELet (x, t, e1, e2) => (L'.ELet (x, corifyCon st t, corifyExp st e1, corifyExp st e2), loc)
adamc@450 645
adam@2010 646 fun isTransactional (c, _) =
adam@2010 647 case c of
adam@2010 648 L'.TFun (_, c) => isTransactional c
adam@2010 649 | L'.CApp ((L'.CFfi ("Basis", "transaction"), _), _) => true
adam@2010 650 | _ => false
adam@2010 651
adamc@480 652 fun corifyDecl mods (all as (d, loc : EM.span), st) =
adamc@249 653 case d of
adamc@249 654 L.DCon (x, n, k, c) =>
adamc@249 655 let
adamc@249 656 val (st, n) = St.bindCon st x n
adamc@249 657 in
adamc@249 658 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
adamc@249 659 end
adamc@807 660 | L.DDatatype dts =>
adamc@249 661 let
adamc@807 662 val (dts, st) = ListUtil.foldlMap (fn ((x, n, xs, xncs), st) =>
adamc@807 663 let
adamc@807 664 val (st, n) = St.bindCon st x n
adamc@807 665 in
adamc@807 666 ((x, n, xs, xncs), st)
adamc@807 667 end)
adamc@807 668 st dts
adamc@16 669
adamc@807 670 val (dts, (st, dcons)) =
adamc@807 671 ListUtil.foldlMap
adamc@807 672 (fn ((x, n, xs, xncs), (st, dcons)) =>
adamc@807 673 let
adamc@807 674 val (xncs, st) = ListUtil.foldlMap
adamc@807 675 (fn ((x, n, co), st) =>
adamc@807 676 let
adam@1704 677 val (st, n') = St.bindConstructor st x n
adam@1704 678 val st = St.bindConstructorVal st x n n'
adamc@807 679 val co = Option.map (corifyCon st) co
adamc@807 680 in
adam@1704 681 ((x, n', co), st)
adamc@807 682 end) st xncs
adamc@192 683
adamc@807 684 val dk = ElabUtil.classifyDatatype xncs
adamc@807 685 val t = (L'.CNamed n, loc)
adamc@807 686 val nxs = length xs - 1
adamc@807 687 val t = ListUtil.foldli
adamc@807 688 (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
adamc@807 689 val k = (L'.KType, loc)
adamc@807 690 val dcons' = map (fn (x, n, to) =>
adamc@807 691 let
adamc@807 692 val args = ListUtil.mapi
adamc@807 693 (fn (i, _) => (L'.CRel (nxs - i), loc)) xs
adamc@807 694 val (e, t) =
adamc@807 695 case to of
adamc@807 696 NONE => ((L'.ECon (dk, L'.PConVar n, args, NONE),
adamc@807 697 loc), t)
adamc@807 698 | SOME t' => ((L'.EAbs ("x", t', t,
adamc@807 699 (L'.ECon (dk, L'.PConVar n,
adamc@807 700 args,
adamc@807 701 SOME (L'.ERel 0,
adamc@807 702 loc)),
adamc@807 703 loc)),
adamc@807 704 loc),
adamc@807 705 (L'.TFun (t', t), loc))
adamc@807 706
adamc@807 707 val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
adamc@807 708 val e = foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc)) e xs
adamc@807 709 in
adamc@807 710 (L'.DVal (x, n, t, e, ""), loc)
adamc@807 711 end) xncs
adamc@807 712 in
adamc@807 713 ((x, n, xs, xncs), (st, dcons' @ dcons))
adamc@807 714 end)
adamc@807 715 (st, []) dts
adamc@249 716 in
adamc@807 717 ((L'.DDatatype dts, loc) :: dcons, st)
adamc@807 718 end
adamc@249 719 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
adamc@249 720 let
adamc@249 721 val (st, n) = St.bindCon st x n
adamc@249 722 val c = corifyCon st (L.CModProj (m1, ms, s), loc)
adamc@177 723
adamc@249 724 val m = foldl (fn (x, m) => (L.StrProj (m, x), loc)) (L.StrVar m1, loc) ms
adamc@376 725 val (_, {inner, ...}) = corifyStr mods (m, st)
adamc@177 726
adamc@249 727 val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) =>
adamc@249 728 let
adamc@249 729 val n' = St.lookupConstructorByName inner x
adam@1704 730 val st = St.bindConstructorAs st x n n'
adamc@249 731 val (st, n) = St.bindVal st x n
adamc@249 732 val co = Option.map (corifyCon st) co
adamc@249 733 in
adamc@249 734 ((x, n, co), st)
adamc@249 735 end) st xncs
adamc@49 736
adamc@249 737 val nxs = length xs - 1
adamc@288 738 val cBase = c
adamc@249 739 val c = ListUtil.foldli (fn (i, _, c) => (L'.CApp (c, (L'.CRel (nxs - i), loc)), loc)) c xs
adamc@249 740 val k = (L'.KType, loc)
adamc@249 741 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@192 742
adamc@249 743 val cds = map (fn (x, n, co) =>
adamc@249 744 let
adamc@249 745 val t = case co of
adamc@249 746 NONE => c
adamc@249 747 | SOME t' => (L'.TFun (t', c), loc)
adamc@249 748 val e = corifyExp st (L.EModProj (m1, ms, x), loc)
adamc@192 749
adamc@249 750 val t = foldr (fn (x, t) => (L'.TCFun (x, k, t), loc)) t xs
adamc@249 751 in
adamc@249 752 (L'.DVal (x, n, t, e, x), loc)
adamc@249 753 end) xncs
adamc@249 754 in
adamc@288 755 ((L'.DCon (x, n, k', cBase), loc) :: cds, st)
adamc@249 756 end
adam@1990 757 | L.DVal (x, n, t, e as (L.ENamed n', _)) =>
adam@1990 758 let
adam@1990 759 val st =
adam@1990 760 case St.lookupConstructorByIdOpt st n' of
adam@1990 761 SOME pc => St.bindConstructorAs st x n pc
adam@1990 762 | _ => st
adam@1990 763
adam@1990 764 val (st, n) = St.bindVal st x n
adam@1990 765 val s = doRestify Settings.Url (mods, x)
adam@1990 766 in
adam@1990 767 ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st)
adam@1990 768 end
adamc@249 769 | L.DVal (x, n, t, e) =>
adamc@249 770 let
adamc@249 771 val (st, n) = St.bindVal st x n
adamc@768 772 val s = doRestify Settings.Url (mods, x)
adamc@249 773 in
adamc@249 774 ([(L'.DVal (x, n, corifyCon st t, corifyExp st e, s), loc)], st)
adamc@249 775 end
adamc@249 776 | L.DValRec vis =>
adamc@249 777 let
adamc@249 778 val (vis, st) = ListUtil.foldlMap
adamc@249 779 (fn ((x, n, t, e), st) =>
adamc@249 780 let
adamc@249 781 val (st, n) = St.bindVal st x n
adamc@249 782 in
adamc@249 783 ((x, n, t, e), st)
adamc@249 784 end)
adamc@249 785 st vis
adamc@16 786
adamc@249 787 val vis = map
adamc@249 788 (fn (x, n, t, e) =>
adamc@249 789 let
adamc@768 790 val s = doRestify Settings.Url (mods, x)
adamc@249 791 in
adamc@249 792 (x, n, corifyCon st t, corifyExp st e, s)
adamc@249 793 end)
adamc@249 794 vis
adamc@249 795 in
adamc@249 796 ([(L'.DValRec vis, loc)], st)
adamc@249 797 end
adamc@249 798 | L.DSgn _ => ([], st)
adamc@177 799
adamc@249 800 | L.DStr (x, n, _, (L.StrFun (xa, na, _, _, str), _)) =>
adamc@423 801 ([], St.bindFunctor st x n xa na str)
adamc@177 802
adamc@339 803 | L.DStr (x, n, _, (L.StrProj (str, x'), _)) =>
adamc@339 804 let
adamc@376 805 val (ds, {inner, outer}) = corifyStr mods (str, st)
adamc@339 806
adamc@339 807 val st = case St.lookupStrByNameOpt (x', inner) of
adamc@339 808 SOME st' => St.bindStr st x n st'
adamc@339 809 | NONE =>
adamc@339 810 let
adamc@423 811 val (x', n', str') = St.lookupFunctorByName (x', inner)
adamc@339 812 in
adamc@423 813 St.bindFunctor st x n x' n' str'
adamc@339 814 end
adamc@339 815 in
adamc@339 816 ([], st)
adamc@339 817 end
adamc@339 818
adam@1989 819 | L.DStr (x, n, _, (L.StrVar n', _)) =>
adam@1989 820 (case St.lookupFunctorByIdOpt st n' of
adam@1989 821 SOME (arg, dom, body) => ([], St.bindFunctor st x n arg dom body)
adam@1989 822 | NONE => ([], St.bindStr st x n (St.lookupStrById st n')))
adam@1989 823
adamc@249 824 | L.DStr (x, n, _, str) =>
adamc@249 825 let
adamc@377 826 val mods' =
adamc@377 827 if x = "anon" then
adamc@377 828 mods
adamc@377 829 else
adamc@377 830 x :: mods
adamc@377 831
adamc@377 832 val (ds, {inner, outer}) = corifyStr mods' (str, st)
adamc@249 833 val st = St.bindStr outer x n inner
adamc@249 834 in
adamc@249 835 (ds, st)
adamc@249 836 end
adamc@16 837
adamc@249 838 | L.DFfiStr (m, n, (sgn, _)) =>
adam@1879 839 (case sgn of
adamc@249 840 L.SgnConst sgis =>
adamc@249 841 let
adamc@456 842 val (ds, cmap, conmap, st, _) =
adamc@456 843 foldl (fn ((sgi, _), (ds, cmap, conmap, st, trans)) =>
adamc@249 844 case sgi of
adamc@249 845 L.SgiConAbs (x, n, k) =>
adamc@249 846 let
adamc@249 847 val (st, n') = St.bindCon st x n
adamc@456 848
adamc@456 849 val trans =
adamc@456 850 if x = "transaction" then
adamc@456 851 SOME n
adamc@456 852 else
adamc@456 853 trans
adamc@249 854 in
adamc@249 855 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
adamc@249 856 cmap,
adamc@249 857 conmap,
adamc@456 858 st,
adamc@456 859 trans)
adamc@249 860 end
adamc@249 861 | L.SgiCon (x, n, k, _) =>
adamc@249 862 let
adamc@249 863 val (st, n') = St.bindCon st x n
adamc@249 864 in
adamc@249 865 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
adamc@249 866 cmap,
adamc@249 867 conmap,
adamc@456 868 st,
adamc@456 869 trans)
adamc@249 870 end
adamc@177 871
adamc@807 872 | L.SgiDatatype dts =>
adamc@249 873 let
adamc@249 874 val k = (L'.KType, loc)
adamc@807 875
adamc@807 876 val (dts, (ds', st, cmap, conmap)) =
adamc@249 877 ListUtil.foldlMap
adamc@807 878 (fn ((x, n, xs, xnts), (ds', st, cmap, conmap)) =>
adamc@249 879 let
adamc@813 880 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc))
adamc@813 881 k xs
adamc@813 882
adamc@807 883 val dk = ElabUtil.classifyDatatype xnts
adamc@807 884 val (st, n') = St.bindCon st x n
adamc@807 885 val (xnts, (ds', st, cmap, conmap)) =
adamc@807 886 ListUtil.foldlMap
adamc@807 887 (fn ((x', n, to), (ds', st, cmap, conmap)) =>
adamc@807 888 let
adamc@807 889 val dt = (L'.CNamed n', loc)
adamc@807 890 val args = ListUtil.mapi (fn (i, _) => (L'.CRel i, loc)) xs
adamc@163 891
adamc@807 892 val to = Option.map (corifyCon st) to
adamc@177 893
adamc@807 894 val pc = L'.PConFfi {mod = m,
adamc@807 895 datatyp = x,
adamc@807 896 params = xs,
adamc@807 897 con = x',
adamc@807 898 arg = to,
adamc@807 899 kind = dk}
adamc@130 900
adamc@807 901 fun wrapT t =
adamc@807 902 foldr (fn (x, t) => (L'.TCFun (x, k, t), loc))
adamc@807 903 t xs
adamc@807 904 fun wrapE e =
adamc@807 905 foldr (fn (x, e) => (L'.ECAbs (x, k, e), loc))
adamc@807 906 e xs
adamc@192 907
adamc@807 908 val (cmap, d) =
adamc@807 909 case to of
adamc@807 910 NONE => (SM.insert (cmap, x', wrapT dt),
adamc@807 911 (L'.DVal (x', n, wrapT dt,
adamc@807 912 wrapE
adamc@807 913 (L'.ECon (dk, pc,
adamc@807 914 args,
adamc@807 915 NONE),
adamc@807 916 loc),
adamc@807 917 ""), loc))
adamc@807 918 | SOME t =>
adamc@807 919 let
adamc@807 920 val tf = (L'.TFun (t, dt), loc)
adamc@807 921 val e = wrapE
adamc@807 922 (L'.EAbs ("x", t, tf,
adamc@807 923 (L'.ECon (dk,
adamc@807 924 pc,
adamc@807 925 args,
adamc@807 926 SOME
adamc@807 927 (L'.ERel 0,
adamc@807 928 loc)),
adamc@807 929 loc)), loc)
adamc@807 930 val d = (L'.DVal (x', n, wrapT tf,
adamc@807 931 e, ""), loc)
adamc@807 932 in
adamc@807 933 (SM.insert (cmap, x', wrapT tf), d)
adamc@807 934 end
adamc@185 935
adam@1704 936 val st = St.bindConstructorAs st x' n pc
adamc@807 937
adamc@807 938 val conmap = SM.insert (conmap, x',
adamc@807 939 (x, xs, to, dk))
adamc@807 940 in
adamc@807 941 ((x', n, to),
adamc@807 942 (d :: ds', st, cmap, conmap))
adamc@807 943 end) (ds', st, cmap, conmap) xnts
adamc@813 944
adamc@813 945 val d = (L'.DCon (x, n', k', (L'.CFfi (m, x), loc)), loc)
adamc@185 946 in
adamc@813 947 ((x, n', xs, xnts), (d :: ds', st, cmap, conmap))
adamc@807 948 end)
adamc@807 949 ([], st, cmap, conmap) dts
adamc@185 950 in
adamc@813 951 (List.revAppend (ds', ds),
adamc@185 952 cmap,
adamc@185 953 conmap,
adamc@456 954 st,
adamc@456 955 trans)
adamc@807 956 end
adamc@49 957
adamc@49 958 | L.SgiVal (x, _, c) =>
adamc@456 959 let
adamc@456 960 val c =
adamc@456 961 case trans of
adamc@456 962 NONE => corifyCon st c
adamc@456 963 | SOME trans =>
adamc@456 964 let
adamc@456 965 fun transactify (all as (c, loc)) =
adamc@456 966 case c of
adamc@456 967 L.TFun (dom, ran) =>
adamc@456 968 (L'.TFun (corifyCon st dom, transactify ran), loc)
adamc@456 969 | L.CApp ((L.CNamed trans', _), t) =>
adamc@456 970 if trans' = trans then
adamc@456 971 (L'.CApp ((L'.CFfi (m, "transaction"), loc),
adamc@456 972 corifyCon st t), loc)
adamc@456 973 else
adamc@456 974 corifyCon st all
adamc@456 975 | _ => corifyCon st all
adamc@456 976 in
adamc@456 977 transactify c
adamc@456 978 end
adamc@456 979 in
adam@1878 980 if isTransactional c then
adam@1878 981 let
adam@1878 982 val ffi = (m, x)
adam@1878 983 in
adam@1878 984 if Settings.isBenignEffectful ffi then
adam@1878 985 ()
adam@1878 986 else
adam@1878 987 Settings.addEffectful ffi
adam@1878 988 end
adam@1878 989 else
adam@1878 990 ();
adamc@456 991 (ds,
adamc@456 992 SM.insert (cmap, x, c),
adamc@456 993 conmap,
adamc@456 994 st,
adamc@456 995 trans)
adamc@456 996 end
adamc@456 997 | _ => (ds, cmap, conmap, st, trans))
adamc@456 998 ([], SM.empty, SM.empty, st, NONE) sgis
adamc@49 999
adamc@185 1000 val st = St.bindStr st m n (St.ffi m cmap conmap)
adamc@49 1001 in
adamc@764 1002 (rev ds, if m = "Basis" then St.basisIs (st, n) else st)
adamc@49 1003 end
adamc@49 1004 | _ => raise Fail "Non-const signature for FFI structure")
adamc@48 1005
adamc@109 1006 | L.DExport (en, sgn, str) =>
adamc@109 1007 (case #1 sgn of
adamc@109 1008 L.SgnConst sgis =>
adamc@109 1009 let
adamc@109 1010 fun pathify (str, _) =
adamc@109 1011 case str of
adamc@109 1012 L.StrVar m => SOME (m, [])
adamc@109 1013 | L.StrProj (str, s) =>
adamc@109 1014 Option.map (fn (m, ms) => (m, ms @ [s])) (pathify str)
adamc@109 1015 | _ => NONE
adamc@109 1016 in
adamc@109 1017 case pathify str of
adamc@109 1018 NONE => (ErrorMsg.errorAt loc "Structure is too fancy to export";
adamc@109 1019 ([], st))
adamc@109 1020 | SOME (m, ms) =>
adamc@109 1021 let
adamc@249 1022 val basis_n = case St.lookupBasis st of
adamc@249 1023 NONE => raise Fail "Corify: Don't know number of Basis"
adamc@249 1024 | SOME n => n
adamc@249 1025
adamc@109 1026 fun wrapSgi ((sgi, _), (wds, eds)) =
adamc@109 1027 case sgi of
adamc@1125 1028 L.SgiVal (s, _, t) =>
adamc@1125 1029 let
adamc@1125 1030 fun getPage (t, args) =
adamc@1125 1031 case #1 t of
adamc@1125 1032 L.CApp ((L.CModProj (basis, [], "transaction"), _),
adamc@1125 1033 t' as
adamc@1125 1034 (L.CApp
adamc@1125 1035 ((L.CApp
adamc@1125 1036 ((L.CApp ((L.CModProj (basis', [], "xml"), _),
adamc@1125 1037 (L.CRecord (_, [((L.CName "Html", _),
adamc@1125 1038 _)]), _)), _), _),
adamc@1125 1039 _), _), _)) =>
adamc@1125 1040 if basis = basis_n andalso basis' = basis_n then
adamc@1125 1041 SOME (t', rev args)
adamc@1125 1042 else
adamc@1125 1043 NONE
adamc@1125 1044 | L.TFun (dom, ran) => getPage (ran, dom :: args)
adamc@1125 1045 | _ => NONE
adamc@1125 1046 in
adamc@1125 1047 case getPage (t, []) of
adamc@1125 1048 NONE => (wds, eds)
adamc@1125 1049 | SOME (ran', args) =>
adamc@1125 1050 let
adamc@1125 1051 val ran = (L.TRecord (L.CRecord ((L.KType, loc), []), loc), loc)
adamc@1125 1052 val ranT = (L.CApp ((L.CModProj (basis_n, [], "transaction"), loc),
adamc@1125 1053 ran), loc)
adamc@1125 1054 val e = (L.EModProj (m, ms, s), loc)
adamc@249 1055
adamc@1125 1056 val ef = (L.EModProj (basis_n, [], "bind"), loc)
adamc@1125 1057 val ef = (L.ECApp (ef, (L.CModProj (basis_n, [], "transaction"), loc)), loc)
adamc@1125 1058 val ef = (L.ECApp (ef, ran'), loc)
adamc@1125 1059 val ef = (L.ECApp (ef, ran), loc)
adamc@1125 1060 val ef = (L.EApp (ef, (L.EModProj (basis_n, [], "transaction_monad"), loc)),
adamc@1125 1061 loc)
adamc@1125 1062 val ea = ListUtil.foldri (fn (i, _, ea) =>
adamc@1125 1063 (L.EApp (ea, (L.ERel i, loc)), loc)) e args
adamc@1125 1064 val ef = (L.EApp (ef, ea), loc)
adamc@249 1065
adamc@1125 1066 val eat = (L.CApp ((L.CModProj (basis_n, [], "transaction"), loc),
adamc@1125 1067 ran), loc)
adamc@1125 1068 val ea = (L.EAbs ("p", ran', eat,
adamc@1125 1069 (L.EWrite (L.ERel 0, loc), loc)), loc)
adamc@249 1070
adamc@1125 1071 val (e, tf) = ListUtil.foldri (fn (i, t, (e, tf)) =>
adamc@1125 1072 ((L.EAbs ("x" ^ Int.toString i,
adamc@1125 1073 t, tf, e), loc),
adamc@1125 1074 (L.TFun (t, tf), loc)))
adamc@1125 1075 ((L.EApp (ef, ea), loc), ranT) args
adam@1347 1076
adam@1347 1077 val expKind = if List.exists (fn t =>
adam@1347 1078 case corifyCon st t of
adam@1347 1079 (L'.CFfi ("Basis", "postBody"), _) => true
adam@1347 1080 | _ => false) args then
adam@1347 1081 L'.Extern L'.ReadCookieWrite
adam@1347 1082 else
adam@1936 1083 L'.Link L'.ReadCookieWrite
adamc@1125 1084 in
adamc@1125 1085 ((L.DVal ("wrap_" ^ s, 0, tf, e), loc) :: wds,
adamc@1125 1086 (fn st =>
adamc@1125 1087 case #1 (corifyExp st (L.EModProj (en, [], "wrap_" ^ s), loc)) of
adam@1347 1088 L'.ENamed n => (L'.DExport (expKind, n, false), loc)
adamc@1125 1089 | _ => raise Fail "Corify: Value to export didn't corify properly")
adamc@1125 1090 :: eds)
adamc@1125 1091 end
adamc@1125 1092 end
adamc@109 1093 | _ => (wds, eds)
adamc@102 1094
adamc@109 1095 val (wds, eds) = foldl wrapSgi ([], []) sgis
adamc@109 1096 val wrapper = (L.StrConst wds, loc)
adamc@376 1097 val mst = St.lookupStrById st m
adamc@1126 1098 val mst = foldl St.lookupStrByName mst ms
adamc@376 1099 val (ds, {inner, outer}) = corifyStr (St.name mst) (wrapper, st)
adamc@109 1100 val st = St.bindStr outer "wrapper" en inner
adamc@249 1101
adamc@109 1102 val ds = ds @ map (fn f => f st) eds
adamc@109 1103 in
adamc@109 1104 (ds, st)
adamc@109 1105 end
adamc@109 1106 end
adamc@109 1107 | _ => raise Fail "Non-const signature for 'export'")
adamc@48 1108
adamc@707 1109 | L.DTable (_, x, n, c, pe, pc, ce, cc) =>
adamc@249 1110 let
adamc@249 1111 val (st, n) = St.bindVal st x n
adamc@768 1112 val s = relify (doRestify Settings.Table (mods, x))
adamc@249 1113 in
adamc@707 1114 ([(L'.DTable (x, n, corifyCon st c, s,
adamc@707 1115 corifyExp st pe, corifyCon st pc,
adamc@707 1116 corifyExp st ce, corifyCon st cc), loc)], st)
adamc@249 1117 end
adamc@338 1118 | L.DSequence (_, x, n) =>
adamc@338 1119 let
adamc@338 1120 val (st, n) = St.bindVal st x n
adamc@768 1121 val s = relify (doRestify Settings.Sequence (mods, x))
adamc@338 1122 in
adamc@338 1123 ([(L'.DSequence (x, n, s), loc)], st)
adamc@338 1124 end
adamc@754 1125 | L.DView (_, x, n, e, c) =>
adamc@754 1126 let
adamc@754 1127 val (st, n) = St.bindVal st x n
adamc@768 1128 val s = relify (doRestify Settings.View (mods, x))
adamc@754 1129 in
adamc@754 1130 ([(L'.DView (x, n, s, corifyExp st e, corifyCon st c), loc)], st)
adamc@754 1131 end
adamc@246 1132
adamc@271 1133 | L.DDatabase s => ([(L'.DDatabase s, loc)], st)
adamc@271 1134
adamc@461 1135 | L.DCookie (_, x, n, c) =>
adamc@461 1136 let
adamc@461 1137 val (st, n) = St.bindVal st x n
adamc@768 1138 val s = doRestify Settings.Cookie (mods, x)
adamc@461 1139 in
adamc@461 1140 ([(L'.DCookie (x, n, corifyCon st c, s), loc)], st)
adamc@461 1141 end
adamc@720 1142 | L.DStyle (_, x, n) =>
adamc@718 1143 let
adamc@718 1144 val (st, n) = St.bindVal st x n
adamc@768 1145 val s = relify (doRestify Settings.Style (mods, x))
adamc@718 1146 in
adamc@720 1147 ([(L'.DStyle (x, n, s), loc)], st)
adamc@718 1148 end
adamc@461 1149
adamc@1075 1150 | L.DTask (e1, e2) =>
adamc@1075 1151 ([(L'.DTask (corifyExp st e1, corifyExp st e2), loc)], st)
adamc@1073 1152
adamc@1199 1153 | L.DPolicy e1 =>
adamc@1199 1154 ([(L'.DPolicy (corifyExp st e1), loc)], st)
adamc@1199 1155
adam@1294 1156 | L.DOnError (m, ms, x) =>
adam@1294 1157 let
adam@1294 1158 val st = St.lookupStrById st m
adam@1294 1159 val st = foldl St.lookupStrByName st ms
adam@1294 1160 in
adam@1294 1161 case St.lookupValByName st x of
adam@1294 1162 St.ENormal n => ([(L'.DOnError n, loc)], st)
adam@1294 1163 | _ => (ErrorMsg.errorAt loc "Wrong type of identifier for 'onError'";
adam@1294 1164 ([], st))
adam@1294 1165 end
adam@1294 1166
adam@2010 1167 | L.DFfi (x, n, modes, t) =>
adam@2010 1168 let
adam@2010 1169 val m = case St.name st of
adam@2010 1170 [m] => m
adam@2010 1171 | _ => (ErrorMsg.errorAt loc "Used 'ffi' declaration beneath module top level";
adam@2010 1172 "")
adam@2010 1173
adam@2010 1174 val name = (m, x)
adam@2010 1175
adam@2010 1176 val (st, n) = St.bindVal st x n
adam@2010 1177 val s = doRestify Settings.Url (mods, x)
adam@2010 1178
adam@2010 1179 val t' = corifyCon st t
adam@2010 1180
adam@2010 1181 fun numArgs (t : L'.con) =
adam@2010 1182 case #1 t of
adam@2010 1183 L'.TFun (_, ran) => 1 + numArgs ran
adam@2010 1184 | _ => 0
adam@2010 1185
adam@2010 1186 fun makeArgs (i, t : L'.con, acc) =
adam@2010 1187 case #1 t of
adam@2010 1188 L'.TFun (dom, ran) => makeArgs (i-1, ran, ((L'.ERel i, loc), dom) :: acc)
adam@2010 1189 | _ => rev acc
adam@2010 1190
adam@2010 1191 fun wrapAbs (i, t : L'.con, tTrans, e) =
adam@2010 1192 case (#1 t, #1 tTrans) of
adam@2010 1193 (L'.TFun (dom, ran), L'.TFun (_, ran')) => (L'.EAbs ("x" ^ Int.toString i, dom, ran, wrapAbs (i+1, ran, ran', e)), loc)
adam@2010 1194 | _ => e
adam@2010 1195
adam@2010 1196 fun getRan (t : L'.con) =
adam@2010 1197 case #1 t of
adam@2010 1198 L'.TFun (_, ran) => getRan ran
adam@2010 1199 | _ => t
adam@2010 1200
adam@2010 1201 fun addLastBit (t : L'.con) =
adam@2010 1202 case #1 t of
adam@2010 1203 L'.TFun (dom, ran) => (L'.TFun (dom, addLastBit ran), #2 t)
adam@2010 1204 | _ => (L'.TFun ((L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc), t), loc)
adam@2010 1205
adam@2038 1206 val isTrans = isTransactional t'
adam@2038 1207 val e = (L'.EFfiApp (m, x, makeArgs (numArgs t' -
adam@2038 1208 (if isTrans then
adam@2038 1209 0
adam@2038 1210 else
adam@2038 1211 1), t', [])), loc)
adam@2038 1212 val (e, tTrans) = if isTrans then
adam@2010 1213 ((L'.EAbs ("_", (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc), getRan t', e), loc), addLastBit t')
adam@2010 1214 else
adam@2010 1215 (e, t')
adam@2010 1216 val e = wrapAbs (0, t', tTrans, e)
adam@2010 1217 in
adam@2010 1218 app (fn Source.Effectful => Settings.addEffectful name
adam@2010 1219 | Source.BenignEffectful => Settings.addBenignEffectful name
adam@2010 1220 | Source.ClientOnly => Settings.addClientOnly name
adam@2010 1221 | Source.ServerOnly => Settings.addServerOnly name
adam@2010 1222 | Source.JsFunc s => Settings.addJsFunc (name, s)) modes;
adam@2010 1223
adam@2039 1224 if List.exists (fn Source.JsFunc _ => true | _ => false) modes then
adam@2039 1225 ()
adam@2039 1226 else
adam@2039 1227 Settings.addJsFunc (name, #2 name);
adam@2039 1228
adam@2038 1229 if isTrans andalso not (Settings.isBenignEffectful name) then
adam@2010 1230 Settings.addEffectful name
adam@2010 1231 else
adam@2010 1232 ();
adam@2010 1233
adam@2010 1234 ([(L'.DVal (x, n, t', e, s), loc)], st)
adam@2010 1235 end
adam@2010 1236
adam@1989 1237 and corifyStr mods ((str, loc), st) =
adamc@39 1238 case str of
adamc@39 1239 L.StrConst ds =>
adamc@39 1240 let
adamc@376 1241 val st = St.enter (st, mods)
adamc@376 1242 val (ds, st) = ListUtil.foldlMapConcat (corifyDecl mods) st ds
adamc@39 1243 in
adamc@39 1244 (ds, St.leave st)
adamc@39 1245 end
adamc@39 1246 | L.StrVar n => ([], {inner = St.lookupStrById st n, outer = st})
adamc@39 1247 | L.StrProj (str, x) =>
adamc@39 1248 let
adamc@376 1249 val (ds, {inner, outer}) = corifyStr mods (str, st)
adamc@39 1250 in
adamc@39 1251 (ds, {inner = St.lookupStrByName (x, inner), outer = outer})
adamc@39 1252 end
adamc@46 1253 | L.StrFun _ => raise Fail "Corify of nested functor definition"
adamc@46 1254 | L.StrApp (str1, str2) =>
adamc@46 1255 let
adamc@46 1256 fun unwind' (str, _) =
adamc@46 1257 case str of
adamc@46 1258 L.StrVar n => St.lookupStrById st n
adamc@46 1259 | L.StrProj (str, x) => St.lookupStrByName (x, unwind' str)
adamc@46 1260 | _ => raise Fail "Corify of fancy functor application [1]"
adamc@46 1261
adamc@46 1262 fun unwind (str, _) =
adamc@46 1263 case str of
adamc@46 1264 L.StrVar n => St.lookupFunctorById st n
adamc@46 1265 | L.StrProj (str, x) => St.lookupFunctorByName (x, unwind' str)
adamc@46 1266 | _ => raise Fail "Corify of fancy functor application [2]"
adamc@46 1267
adamc@423 1268 val (xa, na, body) = unwind str1
adamc@46 1269
adam@1989 1270 (* An important step to make sure that nested functors
adam@1989 1271 * "close under their environments": *)
adam@1989 1272 val (next, body') = ExplRename.rename {NextId = getCounter (),
adam@1989 1273 FormalName = xa,
adam@1989 1274 FormalId = na,
adam@1989 1275 Body = body}
adam@1989 1276
adam@1989 1277 (*val () = Print.prefaces ("RENAME " ^ ErrorMsg.spanToString loc)
adam@1989 1278 [("FROM", ExplPrint.p_str ExplEnv.empty body),
adam@1989 1279 ("TO", ExplPrint.p_str ExplEnv.empty body')]*)
adam@1989 1280 val body = body'
adam@1989 1281
adam@1989 1282 val () = setCounter next
adam@1989 1283
adamc@376 1284 val (ds1, {inner = inner', outer}) = corifyStr mods (str2, st)
adamc@376 1285
adamc@423 1286 val (ds2, {inner, outer}) = corifyStr mods (body, St.bindStr outer xa na inner')
adamc@46 1287 in
adamc@146 1288 (ds1 @ ds2, {inner = St.bindStr inner xa na inner', outer = outer})
adamc@46 1289 end
adamc@31 1290
adamc@39 1291 fun maxName ds = foldl (fn ((d, _), n) =>
adamc@39 1292 case d of
adamc@39 1293 L.DCon (_, n', _, _) => Int.max (n, n')
adamc@806 1294 | L.DDatatype dts => foldl (fn ((_, n', _, _), n) => Int.max (n, n')) n dts
adamc@191 1295 | L.DDatatypeImp (_, n', _, _, _, _, _) => Int.max (n, n')
adamc@124 1296 | L.DVal (_, n', _, _) => Int.max (n, n')
adamc@124 1297 | L.DValRec vis => foldl (fn ((_, n', _, _), n) => Int.max (n, n)) n vis
adamc@39 1298 | L.DSgn (_, n', _) => Int.max (n, n')
adamc@48 1299 | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str))
adamc@100 1300 | L.DFfiStr (_, n', _) => Int.max (n, n')
adamc@246 1301 | L.DExport _ => n
adamc@707 1302 | L.DTable (_, _, n', _, _, _, _, _) => Int.max (n, n')
adamc@338 1303 | L.DSequence (_, _, n') => Int.max (n, n')
adamc@754 1304 | L.DView (_, _, n', _, _) => Int.max (n, n')
adamc@461 1305 | L.DDatabase _ => n
adamc@718 1306 | L.DCookie (_, _, n', _) => Int.max (n, n')
adamc@1073 1307 | L.DStyle (_, _, n') => Int.max (n, n')
adamc@1199 1308 | L.DTask _ => n
adam@1294 1309 | L.DPolicy _ => n
adam@2010 1310 | L.DOnError _ => n
adam@2010 1311 | L.DFfi (_, n', _, _) => Int.max (n, n'))
adamc@249 1312 0 ds
adamc@39 1313
adamc@39 1314 and maxNameStr (str, _) =
adamc@39 1315 case str of
adamc@39 1316 L.StrConst ds => maxName ds
adamc@39 1317 | L.StrVar n => n
adamc@39 1318 | L.StrProj (str, _) => maxNameStr str
adamc@45 1319 | L.StrFun (_, _, _, _, str) => maxNameStr str
adamc@45 1320 | L.StrApp (str1, str2) => Int.max (maxNameStr str1, maxNameStr str2)
adamc@39 1321
adamc@39 1322 fun corify ds =
adamc@39 1323 let
adamc@39 1324 val () = reset (maxName ds + 1)
adamc@146 1325
adamc@376 1326 val (ds, _) = ListUtil.foldlMapConcat (corifyDecl []) St.empty ds
adamc@39 1327 in
adamc@39 1328 ds
adamc@39 1329 end
adamc@16 1330
adamc@16 1331 end