Mercurial > urweb

comparison src/elab_env.sml @ 623:588b9d16b00a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 16:10:25 -0500
parents 44958d74c43f
children fab5998b840e
comparison
equal deleted inserted replaced
622:d64533157f40 623:588b9d16b00a
43 43
44 (* AST utility functions *) 44 (* AST utility functions *)
45 45
46 exception SynUnif 46 exception SynUnif
47 47
48 val liftKindInKind =
49 U.Kind.mapB {kind = fn bound => fn k =>
50 case k of
51 KRel xn =>
52 if xn < bound then
53 k
54 else
55 KRel (xn + 1)
56 | _ => k,
57 bind = fn (bound, _) => bound + 1}
58
59 val liftKindInCon =
60 U.Con.mapB {kind = fn bound => fn k =>
61 case k of
62 KRel xn =>
63 if xn < bound then
64 k
65 else
66 KRel (xn + 1)
67 | _ => k,
68 con = fn _ => fn c => c,
69 bind = fn (bound, U.Con.RelK _) => bound + 1
70 | (bound, _) => bound}
71
48 val liftConInCon = 72 val liftConInCon =
49 U.Con.mapB {kind = fn k => k, 73 U.Con.mapB {kind = fn _ => fn k => k,
50 con = fn bound => fn c => 74 con = fn bound => fn c =>
51 case c of 75 case c of
52 CRel xn => 76 CRel xn =>
53 if xn < bound then 77 if xn < bound then
54 c 78 c
55 else 79 else
56 CRel (xn + 1) 80 CRel (xn + 1)
57 (*| CUnif _ => raise SynUnif*) 81 (*| CUnif _ => raise SynUnif*)
58 | _ => c, 82 | _ => c,
59 bind = fn (bound, U.Con.Rel _) => bound + 1 83 bind = fn (bound, U.Con.RelC _) => bound + 1
60 | (bound, _) => bound} 84 | (bound, _) => bound}
61 85
62 val lift = liftConInCon 0 86 val lift = liftConInCon 0
63 87
88 val liftKindInExp =
89 U.Exp.mapB {kind = fn bound => fn k =>
90 case k of
91 KRel xn =>
92 if xn < bound then
93 k
94 else
95 KRel (xn + 1)
96 | _ => k,
97 con = fn _ => fn c => c,
98 exp = fn _ => fn e => e,
99 bind = fn (bound, U.Exp.RelK _) => bound + 1
100 | (bound, _) => bound}
101
64 val liftConInExp = 102 val liftConInExp =
65 U.Exp.mapB {kind = fn k => k, 103 U.Exp.mapB {kind = fn _ => fn k => k,
66 con = fn bound => fn c => 104 con = fn bound => fn c =>
67 case c of 105 case c of
68 CRel xn => 106 CRel xn =>
69 if xn < bound then 107 if xn < bound then
70 c 108 c
74 exp = fn _ => fn e => e, 112 exp = fn _ => fn e => e,
75 bind = fn (bound, U.Exp.RelC _) => bound + 1 113 bind = fn (bound, U.Exp.RelC _) => bound + 1
76 | (bound, _) => bound} 114 | (bound, _) => bound}
77 115
78 val liftExpInExp = 116 val liftExpInExp =
79 U.Exp.mapB {kind = fn k => k, 117 U.Exp.mapB {kind = fn _ => fn k => k,
80 con = fn _ => fn c => c, 118 con = fn _ => fn c => c,
81 exp = fn bound => fn e => 119 exp = fn bound => fn e =>
82 case e of 120 case e of
83 ERel xn => 121 ERel xn =>
84 if xn < bound then 122 if xn < bound then
91 129
92 130
93 val liftExp = liftExpInExp 0 131 val liftExp = liftExpInExp 0
94 132
95 val subExpInExp = 133 val subExpInExp =
96 U.Exp.mapB {kind = fn k => k, 134 U.Exp.mapB {kind = fn _ => fn k => k,
97 con = fn _ => fn c => c, 135 con = fn _ => fn c => c,
98 exp = fn (xn, rep) => fn e => 136 exp = fn (xn, rep) => fn e =>
99 case e of 137 case e of
100 ERel xn' => 138 ERel xn' =>
101 (case Int.compare (xn', xn) of 139 (case Int.compare (xn', xn) of
201 (print (cn2s cn ^ ":"); 239 (print (cn2s cn ^ ":");
202 KM.appi (fn (ck, _) => print (" " ^ ck2s ck)) km; 240 KM.appi (fn (ck, _) => print (" " ^ ck2s ck)) km;
203 print "\n")) cs) 241 print "\n")) cs)
204 242
205 type env = { 243 type env = {
244 renameK : int SM.map,
245 relK : string list,
246
206 renameC : kind var' SM.map, 247 renameC : kind var' SM.map,
207 relC : (string * kind) list, 248 relC : (string * kind) list,
208 namedC : (string * kind * con option) IM.map, 249 namedC : (string * kind * con option) IM.map,
209 250
210 datatypes : datatyp IM.map, 251 datatypes : datatyp IM.map,
232 namedCounter := r + 1; 273 namedCounter := r + 1;
233 r 274 r
234 end 275 end
235 276
236 val empty = { 277 val empty = {
278 renameK = SM.empty,
279 relK = [],
280
237 renameC = SM.empty, 281 renameC = SM.empty,
238 relC = [], 282 relC = [],
239 namedC = IM.empty, 283 namedC = IM.empty,
240 284
241 datatypes = IM.empty, 285 datatypes = IM.empty,
259 CkNamed _ => ck 303 CkNamed _ => ck
260 | CkRel n => CkRel (n + 1) 304 | CkRel n => CkRel (n + 1)
261 | CkProj _ => ck 305 | CkProj _ => ck
262 | CkApp (ck1, ck2) => CkApp (liftClassKey ck1, liftClassKey ck2) 306 | CkApp (ck1, ck2) => CkApp (liftClassKey ck1, liftClassKey ck2)
263 307
308 fun pushKRel (env : env) x =
309 let
310 val renameK = SM.map (fn n => n+1) (#renameK env)
311 in
312 {renameK = SM.insert (renameK, x, 0),
313 relK = x :: #relK env,
314
315 renameC = SM.map (fn Rel' (n, k) => Rel' (n, liftKindInKind 0 k)
316 | x => x) (#renameC env),
317 relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env),
318 namedC = #namedC env,
319
320 datatypes = #datatypes env,
321 constructors = #constructors env,
322
323 classes = #classes env,
324
325 renameE = SM.map (fn Rel' (n, c) => Rel' (n, liftKindInCon 0 c)
326 | Named' (n, c) => Named' (n, c)) (#renameE env),
327 relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env),
328 namedE = #namedE env,
329
330 renameSgn = #renameSgn env,
331 sgn = #sgn env,
332
333 renameStr = #renameStr env,
334 str = #str env
335 }
336 end
337
338 fun lookupKRel (env : env) n =
339 (List.nth (#relK env, n))
340 handle Subscript => raise UnboundRel n
341
342 fun lookupK (env : env) x = SM.find (#renameK env, x)
343
264 fun pushCRel (env : env) x k = 344 fun pushCRel (env : env) x k =
265 let 345 let
266 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k) 346 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
267 | x => x) (#renameC env) 347 | x => x) (#renameC env)
268 in 348 in
269 {renameC = SM.insert (renameC, x, Rel' (0, k)), 349 {renameK = #renameK env,
350 relK = #relK env,
351
352 renameC = SM.insert (renameC, x, Rel' (0, k)),
270 relC = (x, k) :: #relC env, 353 relC = (x, k) :: #relC env,
271 namedC = #namedC env, 354 namedC = #namedC env,
272 355
273 datatypes = #datatypes env, 356 datatypes = #datatypes env,
274 constructors = #constructors env, 357 constructors = #constructors env,
296 fun lookupCRel (env : env) n = 379 fun lookupCRel (env : env) n =
297 (List.nth (#relC env, n)) 380 (List.nth (#relC env, n))
298 handle Subscript => raise UnboundRel n 381 handle Subscript => raise UnboundRel n
299 382
300 fun pushCNamedAs (env : env) x n k co = 383 fun pushCNamedAs (env : env) x n k co =
301 {renameC = SM.insert (#renameC env, x, Named' (n, k)), 384 {renameK = #renameK env,
385 relK = #relK env,
386
387 renameC = SM.insert (#renameC env, x, Named' (n, k)),
302 relC = #relC env, 388 relC = #relC env,
303 namedC = IM.insert (#namedC env, n, (x, k, co)), 389 namedC = IM.insert (#namedC env, n, (x, k, co)),
304 390
305 datatypes = #datatypes env, 391 datatypes = #datatypes env,
306 constructors = #constructors env, 392 constructors = #constructors env,
338 424
339 fun pushDatatype (env : env) n xs xncs = 425 fun pushDatatype (env : env) n xs xncs =
340 let 426 let
341 val dk = U.classifyDatatype xncs 427 val dk = U.classifyDatatype xncs
342 in 428 in
343 {renameC = #renameC env, 429 {renameK = #renameK env,
430 relK = #relK env,
431
432 renameC = #renameC env,
344 relC = #relC env, 433 relC = #relC env,
345 namedC = #namedC env, 434 namedC = #namedC env,
346 435
347 datatypes = IM.insert (#datatypes env, n, 436 datatypes = IM.insert (#datatypes env, n,
348 (xs, foldl (fn ((x, n, to), cons) => 437 (xs, foldl (fn ((x, n, to), cons) =>
378 467
379 fun datatypeArgs (xs, _) = xs 468 fun datatypeArgs (xs, _) = xs
380 fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt 469 fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt
381 470
382 fun pushClass (env : env) n = 471 fun pushClass (env : env) n =
383 {renameC = #renameC env, 472 {renameK = #renameK env,
473 relK = #relK env,
474
475 renameC = #renameC env,
384 relC = #relC env, 476 relC = #relC env,
385 namedC = #namedC env, 477 namedC = #namedC env,
386 478
387 datatypes = #datatypes env, 479 datatypes = #datatypes env,
388 constructors = #constructors env, 480 constructors = #constructors env,
466 } 558 }
467 in 559 in
468 CM.insert (classes, f, class) 560 CM.insert (classes, f, class)
469 end 561 end
470 in 562 in
471 {renameC = #renameC env, 563 {renameK = #renameK env,
564 relK = #relK env,
565
566 renameC = #renameC env,
472 relC = #relC env, 567 relC = #relC env,
473 namedC = #namedC env, 568 namedC = #namedC env,
474 569
475 datatypes = #datatypes env, 570 datatypes = #datatypes env,
476 constructors = #constructors env, 571 constructors = #constructors env,
507 } 602 }
508 in 603 in
509 CM.insert (classes, f, class) 604 CM.insert (classes, f, class)
510 end 605 end
511 in 606 in
512 {renameC = #renameC env, 607 {renameK = #renameK env,
608 relK = #relK env,
609
610 renameC = #renameC env,
513 relC = #relC env, 611 relC = #relC env,
514 namedC = #namedC env, 612 namedC = #namedC env,
515 613
516 datatypes = #datatypes env, 614 datatypes = #datatypes env,
517 constructors = #constructors env, 615 constructors = #constructors env,
550 NONE => NotBound 648 NONE => NotBound
551 | SOME (Rel' x) => Rel x 649 | SOME (Rel' x) => Rel x
552 | SOME (Named' x) => Named x 650 | SOME (Named' x) => Named x
553 651
554 fun pushSgnNamedAs (env : env) x n sgis = 652 fun pushSgnNamedAs (env : env) x n sgis =
555 {renameC = #renameC env, 653 {renameK = #renameK env,
654 relK = #relK env,
655
656 renameC = #renameC env,
556 relC = #relC env, 657 relC = #relC env,
557 namedC = #namedC env, 658 namedC = #namedC env,
558 659
559 datatypes = #datatypes env, 660 datatypes = #datatypes env,
560 constructors = #constructors env, 661 constructors = #constructors env,
866 classes 967 classes
867 end 968 end
868 | _ => classes 969 | _ => classes
869 970
870 fun pushStrNamedAs (env : env) x n sgn = 971 fun pushStrNamedAs (env : env) x n sgn =
871 {renameC = #renameC env, 972 {renameK = #renameK env,
973 relK = #relK env,
974
975 renameC = #renameC env,
872 relC = #relC env, 976 relC = #relC env,
873 namedC = #namedC env, 977 namedC = #namedC env,
874 978
875 datatypes = #datatypes env, 979 datatypes = #datatypes env,
876 constructors = #constructors env, 980 constructors = #constructors env,