Mercurial > urweb

annotate src/corify.sml @ 1726:4df4521fbd3b

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