Mercurial > urweb

annotate src/elab_env.sml @ 2:64f09f7822c3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of elaboration
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Jan 2008 14:27:33 -0500
parents
children 258261a53842
rev   line source
adamc@2 1 (* Copyright (c) 2008, Adam Chlipala
adamc@2 2 * All rights reserved.
adamc@2 3 *
adamc@2 4 * Redistribution and use in source and binary forms, with or without
adamc@2 5 * modification, are permitted provided that the following conditions are met:
adamc@2 6 *
adamc@2 7 * - Redistributions of source code must retain the above copyright notice,
adamc@2 8 * this list of conditions and the following disclaimer.
adamc@2 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@2 10 * this list of conditions and the following disclaimer in the documentation
adamc@2 11 * and/or other materials provided with the distribution.
adamc@2 12 * - The names of contributors may not be used to endorse or promote products
adamc@2 13 * derived from this software without specific prior written permission.
adamc@2 14 *
adamc@2 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@2 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@2 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@2 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@2 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@2 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@2 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@2 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@2 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@2 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@2 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@2 26 *)
adamc@2 27
adamc@2 28 structure ElabEnv :> ELAB_ENV = struct
adamc@2 29
adamc@2 30 open Elab
adamc@2 31
adamc@2 32 structure IM = IntBinaryMap
adamc@2 33 structure SM = BinaryMapFn(struct
adamc@2 34 type ord_key = string
adamc@2 35 val compare = String.compare
adamc@2 36 end)
adamc@2 37
adamc@2 38 exception UnboundRel of int
adamc@2 39 exception UnboundNamed of int
adamc@2 40
adamc@2 41 datatype var' =
adamc@2 42 CRel' of int * kind
adamc@2 43 | CNamed' of int * kind
adamc@2 44
adamc@2 45 datatype var =
adamc@2 46 CNotBound
adamc@2 47 | CRel of int * kind
adamc@2 48 | CNamed of int * kind
adamc@2 49
adamc@2 50 type env = {
adamc@2 51 renameC : var' SM.map,
adamc@2 52 relC : (string * kind) list,
adamc@2 53 namedC : (string * kind) IM.map
adamc@2 54 }
adamc@2 55
adamc@2 56 val namedCounter = ref 0
adamc@2 57
adamc@2 58 val empty = {
adamc@2 59 renameC = SM.empty,
adamc@2 60 relC = [],
adamc@2 61 namedC = IM.empty
adamc@2 62 }
adamc@2 63
adamc@2 64 fun pushCRel (env : env) x k =
adamc@2 65 let
adamc@2 66 val renameC = SM.map (fn CRel' (n, k) => CRel' (n+1, k)
adamc@2 67 | x => x) (#renameC env)
adamc@2 68 in
adamc@2 69 {renameC = SM.insert (renameC, x, CRel' (0, k)),
adamc@2 70 relC = (x, k) :: #relC env,
adamc@2 71 namedC = #namedC env}
adamc@2 72 end
adamc@2 73
adamc@2 74 fun lookupCRel (env : env) n =
adamc@2 75 (List.nth (#relC env, n))
adamc@2 76 handle Subscript => raise UnboundRel n
adamc@2 77
adamc@2 78 fun pushCNamed (env : env) x k =
adamc@2 79 let
adamc@2 80 val n = !namedCounter
adamc@2 81 in
adamc@2 82 namedCounter := n + 1;
adamc@2 83 ({renameC = SM.insert (#renameC env, x, CNamed' (n, k)),
adamc@2 84 relC = #relC env,
adamc@2 85 namedC = IM.insert (#namedC env, n, (x, k))},
adamc@2 86 n)
adamc@2 87 end
adamc@2 88
adamc@2 89 fun lookupCNamed (env : env) n =
adamc@2 90 case IM.find (#namedC env, n) of
adamc@2 91 NONE => raise UnboundNamed n
adamc@2 92 | SOME x => x
adamc@2 93
adamc@2 94 fun lookupC (env : env) x =
adamc@2 95 case SM.find (#renameC env, x) of
adamc@2 96 NONE => CNotBound
adamc@2 97 | SOME (CRel' x) => CRel x
adamc@2 98 | SOME (CNamed' x) => CNamed x
adamc@2 99
adamc@2 100 end