Mercurial > urweb

comparison src/elab_env.sml @ 157:adc4e42e3adc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Basic datatype importing works
author Adam Chlipala <adamc@hcoop.net>
date Thu, 24 Jul 2008 15:49:30 -0400
parents 34ccd7d2bea8
children b4b70de488e9
comparison
equal deleted inserted replaced
156:34ccd7d2bea8 157:adc4e42e3adc
71 datatype 'a var = 71 datatype 'a var =
72 NotBound 72 NotBound
73 | Rel of int * 'a 73 | Rel of int * 'a
74 | Named of int * 'a 74 | Named of int * 'a
75 75
76 type datatyp = (string * con option) IM.map
77
76 type env = { 78 type env = {
77 renameC : kind var' SM.map, 79 renameC : kind var' SM.map,
78 relC : (string * kind) list, 80 relC : (string * kind) list,
79 namedC : (string * kind * con option) IM.map, 81 namedC : (string * kind * con option) IM.map,
80 82
83 datatypes : datatyp IM.map,
84
81 renameE : con var' SM.map, 85 renameE : con var' SM.map,
82 relE : (string * con) list, 86 relE : (string * con) list,
83 namedE : (string * con) IM.map, 87 namedE : (string * con) IM.map,
84 88
85 renameSgn : (int * sgn) SM.map, 89 renameSgn : (int * sgn) SM.map,
102 val empty = { 106 val empty = {
103 renameC = SM.empty, 107 renameC = SM.empty,
104 relC = [], 108 relC = [],
105 namedC = IM.empty, 109 namedC = IM.empty,
106 110
111 datatypes = IM.empty,
112
107 renameE = SM.empty, 113 renameE = SM.empty,
108 relE = [], 114 relE = [],
109 namedE = IM.empty, 115 namedE = IM.empty,
110 116
111 renameSgn = SM.empty, 117 renameSgn = SM.empty,
121 | x => x) (#renameC env) 127 | x => x) (#renameC env)
122 in 128 in
123 {renameC = SM.insert (renameC, x, Rel' (0, k)), 129 {renameC = SM.insert (renameC, x, Rel' (0, k)),
124 relC = (x, k) :: #relC env, 130 relC = (x, k) :: #relC env,
125 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), 131 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
132
133 datatypes = #datatypes env,
126 134
127 renameE = #renameE env, 135 renameE = #renameE env,
128 relE = map (fn (x, c) => (x, lift c)) (#relE env), 136 relE = map (fn (x, c) => (x, lift c)) (#relE env),
129 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env), 137 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
130 138
142 150
143 fun pushCNamedAs (env : env) x n k co = 151 fun pushCNamedAs (env : env) x n k co =
144 {renameC = SM.insert (#renameC env, x, Named' (n, k)), 152 {renameC = SM.insert (#renameC env, x, Named' (n, k)),
145 relC = #relC env, 153 relC = #relC env,
146 namedC = IM.insert (#namedC env, n, (x, k, co)), 154 namedC = IM.insert (#namedC env, n, (x, k, co)),
155
156 datatypes = #datatypes env,
147 157
148 renameE = #renameE env, 158 renameE = #renameE env,
149 relE = #relE env, 159 relE = #relE env,
150 namedE = #namedE env, 160 namedE = #namedE env,
151 161
172 case SM.find (#renameC env, x) of 182 case SM.find (#renameC env, x) of
173 NONE => NotBound 183 NONE => NotBound
174 | SOME (Rel' x) => Rel x 184 | SOME (Rel' x) => Rel x
175 | SOME (Named' x) => Named x 185 | SOME (Named' x) => Named x
176 186
187 fun pushDatatype (env : env) n xncs =
188 {renameC = #renameC env,
189 relC = #relC env,
190 namedC = #namedC env,
191
192 datatypes = IM.insert (#datatypes env, n,
193 foldl (fn ((x, n, to), cons) =>
194 IM.insert (cons, n, (x, to))) IM.empty xncs),
195
196 renameE = #renameE env,
197 relE = #relE env,
198 namedE = #namedE env,
199
200 renameSgn = #renameSgn env,
201 sgn = #sgn env,
202
203 renameStr = #renameStr env,
204 str = #str env}
205
206 fun lookupDatatype (env : env) n =
207 case IM.find (#datatypes env, n) of
208 NONE => raise UnboundNamed n
209 | SOME x => x
210
211 fun lookupConstructor dt n =
212 case IM.find (dt, n) of
213 NONE => raise UnboundNamed n
214 | SOME x => x
215
216 fun constructors dt = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt
217
177 fun pushERel (env : env) x t = 218 fun pushERel (env : env) x t =
178 let 219 let
179 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) 220 val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t)
180 | x => x) (#renameE env) 221 | x => x) (#renameE env)
181 in 222 in
182 {renameC = #renameC env, 223 {renameC = #renameC env,
183 relC = #relC env, 224 relC = #relC env,
184 namedC = #namedC env, 225 namedC = #namedC env,
226
227 datatypes = #datatypes env,
185 228
186 renameE = SM.insert (renameE, x, Rel' (0, t)), 229 renameE = SM.insert (renameE, x, Rel' (0, t)),
187 relE = (x, t) :: #relE env, 230 relE = (x, t) :: #relE env,
188 namedE = #namedE env, 231 namedE = #namedE env,
189 232
200 243
201 fun pushENamedAs (env : env) x n t = 244 fun pushENamedAs (env : env) x n t =
202 {renameC = #renameC env, 245 {renameC = #renameC env,
203 relC = #relC env, 246 relC = #relC env,
204 namedC = #namedC env, 247 namedC = #namedC env,
248
249 datatypes = #datatypes env,
205 250
206 renameE = SM.insert (#renameE env, x, Named' (n, t)), 251 renameE = SM.insert (#renameE env, x, Named' (n, t)),
207 relE = #relE env, 252 relE = #relE env,
208 namedE = IM.insert (#namedE env, n, (x, t)), 253 namedE = IM.insert (#namedE env, n, (x, t)),
209 254
235 fun pushSgnNamedAs (env : env) x n sgis = 280 fun pushSgnNamedAs (env : env) x n sgis =
236 {renameC = #renameC env, 281 {renameC = #renameC env,
237 relC = #relC env, 282 relC = #relC env,
238 namedC = #namedC env, 283 namedC = #namedC env,
239 284
285 datatypes = #datatypes env,
286
240 renameE = #renameE env, 287 renameE = #renameE env,
241 relE = #relE env, 288 relE = #relE env,
242 namedE = #namedE env, 289 namedE = #namedE env,
243 290
244 renameSgn = SM.insert (#renameSgn env, x, (n, sgis)), 291 renameSgn = SM.insert (#renameSgn env, x, (n, sgis)),
265 fun pushStrNamedAs (env : env) x n sgis = 312 fun pushStrNamedAs (env : env) x n sgis =
266 {renameC = #renameC env, 313 {renameC = #renameC env,
267 relC = #relC env, 314 relC = #relC env,
268 namedC = #namedC env, 315 namedC = #namedC env,
269 316
317 datatypes = #datatypes env,
318
270 renameE = #renameE env, 319 renameE = #renameE env,
271 relE = #relE env, 320 relE = #relE env,
272 namedE = #namedE env, 321 namedE = #namedE env,
273 322
274 renameSgn = #renameSgn env, 323 renameSgn = #renameSgn env,
289 case IM.find (#str env, n) of 338 case IM.find (#str env, n) of
290 NONE => raise UnboundNamed n 339 NONE => raise UnboundNamed n
291 | SOME x => x 340 | SOME x => x
292 341
293 fun lookupStr (env : env) x = SM.find (#renameStr env, x) 342 fun lookupStr (env : env) x = SM.find (#renameStr env, x)
294
295 fun declBinds env (d, loc) =
296 case d of
297 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
298 | DDatatype (x, n, xncs) =>
299 let
300 val env = pushCNamedAs env x n (KType, loc) NONE
301 in
302 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc)
303 | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc))
304 env xncs
305 end
306 | DDatatypeImp (x, n, m, ms, x') => pushCNamedAs env x n (KType, loc) (SOME (CModProj (m, ms, x'), loc))
307 | DVal (x, n, t, _) => pushENamedAs env x n t
308 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis
309 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
310 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
311 | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
312 | DConstraint _ => env
313 | DExport _ => env
314 343
315 fun sgiBinds env (sgi, loc) = 344 fun sgiBinds env (sgi, loc) =
316 case sgi of 345 case sgi of
317 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE 346 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
318 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) 347 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
477 fun projectCon env {sgn, str, field} = 506 fun projectCon env {sgn, str, field} =
478 case #1 (hnormSgn env sgn) of 507 case #1 (hnormSgn env sgn) of
479 SgnConst sgis => 508 SgnConst sgis =>
480 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE 509 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
481 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE 510 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
511 | SgiDatatype (x, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE
482 | _ => NONE) sgis of 512 | _ => NONE) sgis of
483 NONE => NONE 513 NONE => NONE
484 | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co)) 514 | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co))
485 | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan)) 515 | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan))
516 | _ => NONE
517
518 fun projectDatatype env {sgn, str, field} =
519 case #1 (hnormSgn env sgn) of
520 SgnConst sgis =>
521 (case sgnSeek (fn SgiDatatype (x, _, xncs) => if x = field then SOME xncs else NONE
522 | _ => NONE) sgis of
523 NONE => NONE
524 | SOME (xncs, subs) => SOME (map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs))
486 | _ => NONE 525 | _ => NONE
487 526
488 fun projectVal env {sgn, str, field} = 527 fun projectVal env {sgn, str, field} =
489 case #1 (hnormSgn env sgn) of 528 case #1 (hnormSgn env sgn) of
490 SgnConst sgis => 529 SgnConst sgis =>
522 case #1 (hnormSgn env sgn) of 561 case #1 (hnormSgn env sgn) of
523 SgnConst sgis => SOME (sgnSeekConstraints (str, sgis)) 562 SgnConst sgis => SOME (sgnSeekConstraints (str, sgis))
524 | SgnError => SOME [] 563 | SgnError => SOME []
525 | _ => NONE 564 | _ => NONE
526 565
566 fun declBinds env (d, loc) =
567 case d of
568 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
569 | DDatatype (x, n, xncs) =>
570 let
571 val env = pushCNamedAs env x n (KType, loc) NONE
572 in
573 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc)
574 | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc))
575 env xncs
576 end
577 | DDatatypeImp (x, n, m, ms, x') =>
578 let
579 val t = (CModProj (m, ms, x'), loc)
580 val env = pushCNamedAs env x n (KType, loc) (SOME t)
581 val (_, sgn) = lookupStrNamed env m
582 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
583 case projectStr env {sgn = sgn, str = str, field = m} of
584 NONE => raise Fail "ElabEnv.declBinds: Couldn't projectStr"
585 | SOME sgn => ((StrProj (str, m), loc), sgn))
586 ((StrVar m, loc), sgn) ms
587 val xncs = case projectDatatype env {sgn = sgn, str = str, field = x'} of
588 NONE => raise Fail "ElabEnv.declBinds: Couldn't projectDatatype"
589 | SOME xncs => xncs
590
591 val t = (CNamed n, loc)
592 in
593 foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' t
594 | ((x', n', SOME t'), env) => pushENamedAs env x' n' (TFun (t', t), loc))
595 env xncs
596 end
597 | DVal (x, n, t, _) => pushENamedAs env x n t
598 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis
599 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
600 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
601 | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn
602 | DConstraint _ => env
603 | DExport _ => env
604
527 end 605 end