Mercurial > urweb

comparison src/expl_env.sml @ 38:d16ef24de78b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Explify
author Adam Chlipala <adamc@hcoop.net>
date Thu, 19 Jun 2008 10:06:59 -0400
parents
children 0a5c312de09a
comparison
equal deleted inserted replaced
37:367f058aba23 38:d16ef24de78b
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 ExplEnv :> EXPL_ENV = struct
29
30 open Expl
31
32 structure U = ExplUtil
33
34 structure IM = IntBinaryMap
35 structure SM = BinaryMapFn(struct
36 type ord_key = string
37 val compare = String.compare
38 end)
39
40 exception UnboundRel of int
41 exception UnboundNamed of int
42
43
44 (* AST utility functions *)
45
46 exception SynUnif
47
48 val liftConInCon =
49 U.Con.mapB {kind = fn k => k,
50 con = fn bound => fn c =>
51 case c of
52 CRel xn =>
53 if xn < bound then
54 c
55 else
56 CRel (xn + 1)
57 (*| CUnif _ => raise SynUnif*)
58 | _ => c,
59 bind = fn (bound, U.Con.Rel _) => bound + 1
60 | (bound, _) => bound}
61
62 val lift = liftConInCon 0
63
64
65 (* Back to environments *)
66
67 datatype 'a var' =
68 Rel' of int * 'a
69 | Named' of int * 'a
70
71 datatype 'a var =
72 NotBound
73 | Rel of int * 'a
74 | Named of int * 'a
75
76 type env = {
77 renameC : kind var' SM.map,
78 relC : (string * kind) list,
79 namedC : (string * kind * con option) IM.map,
80
81 renameE : con var' SM.map,
82 relE : (string * con) list,
83 namedE : (string * con) IM.map,
84
85 renameSgn : (int * sgn) SM.map,
86 sgn : (string * sgn) IM.map,
87
88 renameStr : (int * sgn) SM.map,
89 str : (string * sgn) IM.map
90 }
91
92 val namedCounter = ref 0
93
94 val empty = {
95 renameC = SM.empty,
96 relC = [],
97 namedC = IM.empty,
98
99 renameE = SM.empty,
100 relE = [],
101 namedE = IM.empty,
102
103 renameSgn = SM.empty,
104 sgn = IM.empty,
105
106 renameStr = SM.empty,
107 str = IM.empty
108 }
109
110 fun pushCRel (env : env) x k =
111 let
112 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
113 | x => x) (#renameC env)
114 in
115 {renameC = SM.insert (renameC, x, Rel' (0, k)),
116 relC = (x, k) :: #relC env,
117 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
118
119 renameE = #renameE env,
120 relE = map (fn (x, c) => (x, lift c)) (#relE env),
121 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
122
123 renameSgn = #renameSgn env,
124 sgn = #sgn env,
125
126 renameStr = #renameStr env,
127 str = #str env
128 }
129 end
130
131 fun lookupCRel (env : env) n =
132 (List.nth (#relC env, n))
133 handle Subscript => raise UnboundRel n
134
135 fun pushCNamed (env : env) x n k co =
136 {renameC = SM.insert (#renameC env, x, Named' (n, k)),
137 relC = #relC env,
138 namedC = IM.insert (#namedC env, n, (x, k, co)),
139
140 renameE = #renameE env,
141 relE = #relE env,
142 namedE = #namedE env,
143
144 renameSgn = #renameSgn env,
145 sgn = #sgn env,
146
147 renameStr = #renameStr env,
148 str = #str env}
149
150 fun lookupCNamed (env : env) n =
151 case IM.find (#namedC env, n) of
152 NONE => raise UnboundNamed n
153 | SOME x => x
154
155 fun pushERel (env : env) x t =
156 let
157 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
158 | x => x) (#renameE env)
159 in
160 {renameC = #renameC env,
161 relC = #relC env,
162 namedC = #namedC env,
163
164 renameE = SM.insert (renameE, x, Rel' (0, t)),
165 relE = (x, t) :: #relE env,
166 namedE = #namedE env,
167
168 renameSgn = #renameSgn env,
169 sgn = #sgn env,
170
171 renameStr = #renameStr env,
172 str = #str env}
173 end
174
175 fun lookupERel (env : env) n =
176 (List.nth (#relE env, n))
177 handle Subscript => raise UnboundRel n
178
179 fun pushENamed (env : env) x n t =
180 {renameC = #renameC env,
181 relC = #relC env,
182 namedC = #namedC env,
183
184 renameE = SM.insert (#renameE env, x, Named' (n, t)),
185 relE = #relE env,
186 namedE = IM.insert (#namedE env, n, (x, t)),
187
188 renameSgn = #renameSgn env,
189 sgn = #sgn env,
190
191 renameStr = #renameStr env,
192 str = #str env}
193
194 fun lookupENamed (env : env) n =
195 case IM.find (#namedE env, n) of
196 NONE => raise UnboundNamed n
197 | SOME x => x
198
199 fun pushSgnNamed (env : env) x n sgis =
200 {renameC = #renameC env,
201 relC = #relC env,
202 namedC = #namedC env,
203
204 renameE = #renameE env,
205 relE = #relE env,
206 namedE = #namedE env,
207
208 renameSgn = SM.insert (#renameSgn env, x, (n, sgis)),
209 sgn = IM.insert (#sgn env, n, (x, sgis)),
210
211 renameStr = #renameStr env,
212 str = #str env}
213
214 fun lookupSgnNamed (env : env) n =
215 case IM.find (#sgn env, n) of
216 NONE => raise UnboundNamed n
217 | SOME x => x
218
219 fun pushStrNamed (env : env) x n sgis =
220 {renameC = #renameC env,
221 relC = #relC env,
222 namedC = #namedC env,
223
224 renameE = #renameE env,
225 relE = #relE env,
226 namedE = #namedE env,
227
228 renameSgn = #renameSgn env,
229 sgn = #sgn env,
230
231 renameStr = SM.insert (#renameStr env, x, (n, sgis)),
232 str = IM.insert (#str env, n, (x, sgis))}
233
234 fun lookupStrNamed (env : env) n =
235 case IM.find (#str env, n) of
236 NONE => raise UnboundNamed n
237 | SOME x => x
238
239 fun declBinds env (d, _) =
240 case d of
241 DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
242 | DVal (x, n, t, _) => pushENamed env x n t
243 | DSgn (x, n, sgn) => pushSgnNamed env x n sgn
244 | DStr (x, n, sgn, _) => pushStrNamed env x n sgn
245
246 fun sgiBinds env (sgi, _) =
247 case sgi of
248 SgiConAbs (x, n, k) => pushCNamed env x n k NONE
249 | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c)
250 | SgiVal (x, n, t) => pushENamed env x n t
251 | SgiStr (x, n, sgn) => pushStrNamed env x n sgn
252
253
254 val ktype = (KType, ErrorMsg.dummySpan)
255
256 fun bbind env x =
257 case ElabEnv.lookupC ElabEnv.basis x of
258 ElabEnv.NotBound => raise Fail "CoreEnv.bbind: Not bound"
259 | ElabEnv.Rel _ => raise Fail "CoreEnv.bbind: Rel"
260 | ElabEnv.Named (n, _) => pushCNamed env x n ktype NONE
261
262 val basis = empty
263 val basis = bbind basis "int"
264 val basis = bbind basis "float"
265 val basis = bbind basis "string"
266
267 end