Mercurial > urweb

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