Mercurial > urweb
comparison src/core_env.sml @ 626:230654093b51
demo/hello compiles with kind polymorphism
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 22 Feb 2009 17:17:01 -0500 |
parents | 5c9606deacb6 |
children | 4a125bbc602d |
comparison
equal
deleted
inserted
replaced
625:47947d6e9750 | 626:230654093b51 |
---|---|
34 structure IM = IntBinaryMap | 34 structure IM = IntBinaryMap |
35 | 35 |
36 | 36 |
37 (* AST utility functions *) | 37 (* AST utility functions *) |
38 | 38 |
39 val liftKindInKind = | |
40 U.Kind.mapB {kind = fn bound => fn k => | |
41 case k of | |
42 KRel xn => | |
43 if xn < bound then | |
44 k | |
45 else | |
46 KRel (xn + 1) | |
47 | _ => k, | |
48 bind = fn (bound, _) => bound + 1} | |
49 | |
50 val liftKindInCon = | |
51 U.Con.mapB {kind = fn bound => fn k => | |
52 case k of | |
53 KRel xn => | |
54 if xn < bound then | |
55 k | |
56 else | |
57 KRel (xn + 1) | |
58 | _ => k, | |
59 con = fn _ => fn c => c, | |
60 bind = fn (bound, U.Con.RelK _) => bound + 1 | |
61 | (bound, _) => bound} | |
62 | |
63 val liftKindInExp = | |
64 U.Exp.mapB {kind = fn bound => fn k => | |
65 case k of | |
66 KRel xn => | |
67 if xn < bound then | |
68 k | |
69 else | |
70 KRel (xn + 1) | |
71 | _ => k, | |
72 con = fn _ => fn c => c, | |
73 exp = fn _ => fn e => e, | |
74 bind = fn (bound, U.Exp.RelK _) => bound + 1 | |
75 | (bound, _) => bound} | |
76 | |
39 val liftConInCon = | 77 val liftConInCon = |
40 U.Con.mapB {kind = fn k => k, | 78 U.Con.mapB {kind = fn _ => fn k => k, |
41 con = fn bound => fn c => | 79 con = fn bound => fn c => |
42 case c of | 80 case c of |
43 CRel xn => | 81 CRel xn => |
44 if xn < bound then | 82 if xn < bound then |
45 c | 83 c |
46 else | 84 else |
47 CRel (xn + 1) | 85 CRel (xn + 1) |
48 | _ => c, | 86 | _ => c, |
49 bind = fn (bound, U.Con.Rel _) => bound + 1 | 87 bind = fn (bound, U.Con.RelC _) => bound + 1 |
50 | (bound, _) => bound} | 88 | (bound, _) => bound} |
51 | 89 |
52 val lift = liftConInCon 0 | 90 val lift = liftConInCon 0 |
53 | 91 |
54 val subConInCon = | 92 val subConInCon = |
55 U.Con.mapB {kind = fn k => k, | 93 U.Con.mapB {kind = fn _ => fn k => k, |
56 con = fn (xn, rep) => fn c => | 94 con = fn (xn, rep) => fn c => |
57 case c of | 95 case c of |
58 CRel xn' => | 96 CRel xn' => |
59 (case Int.compare (xn', xn) of | 97 (case Int.compare (xn', xn) of |
60 EQUAL => #1 rep | 98 EQUAL => #1 rep |
61 | GREATER => CRel (xn' - 1) | 99 | GREATER => CRel (xn' - 1) |
62 | LESS => c) | 100 | LESS => c) |
63 | _ => c, | 101 | _ => c, |
64 bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) | 102 bind = fn ((xn, rep), U.Con.RelC _) => (xn+1, liftConInCon 0 rep) |
65 | (ctx, _) => ctx} | 103 | (ctx, _) => ctx} |
66 | 104 |
67 | 105 |
68 val liftConInExp = | 106 val liftConInExp = |
69 U.Exp.mapB {kind = fn k => k, | 107 U.Exp.mapB {kind = fn _ => fn k => k, |
70 con = fn bound => fn c => | 108 con = fn bound => fn c => |
71 case c of | 109 case c of |
72 CRel xn => | 110 CRel xn => |
73 if xn < bound then | 111 if xn < bound then |
74 c | 112 c |
78 exp = fn _ => fn e => e, | 116 exp = fn _ => fn e => e, |
79 bind = fn (bound, U.Exp.RelC _) => bound + 1 | 117 bind = fn (bound, U.Exp.RelC _) => bound + 1 |
80 | (bound, _) => bound} | 118 | (bound, _) => bound} |
81 | 119 |
82 val subConInExp = | 120 val subConInExp = |
83 U.Exp.mapB {kind = fn k => k, | 121 U.Exp.mapB {kind = fn _ => fn k => k, |
84 con = fn (xn, rep) => fn c => | 122 con = fn (xn, rep) => fn c => |
85 case c of | 123 case c of |
86 CRel xn' => | 124 CRel xn' => |
87 (case Int.compare (xn', xn) of | 125 (case Int.compare (xn', xn) of |
88 EQUAL => #1 rep | 126 EQUAL => #1 rep |
92 exp = fn _ => fn e => e, | 130 exp = fn _ => fn e => e, |
93 bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep) | 131 bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep) |
94 | (ctx, _) => ctx} | 132 | (ctx, _) => ctx} |
95 | 133 |
96 val liftExpInExp = | 134 val liftExpInExp = |
97 U.Exp.mapB {kind = fn k => k, | 135 U.Exp.mapB {kind = fn _ => fn k => k, |
98 con = fn _ => fn c => c, | 136 con = fn _ => fn c => c, |
99 exp = fn bound => fn e => | 137 exp = fn bound => fn e => |
100 case e of | 138 case e of |
101 ERel xn => | 139 ERel xn => |
102 if xn < bound then | 140 if xn < bound then |
106 | _ => e, | 144 | _ => e, |
107 bind = fn (bound, U.Exp.RelE _) => bound + 1 | 145 bind = fn (bound, U.Exp.RelE _) => bound + 1 |
108 | (bound, _) => bound} | 146 | (bound, _) => bound} |
109 | 147 |
110 val subExpInExp = | 148 val subExpInExp = |
111 U.Exp.mapB {kind = fn k => k, | 149 U.Exp.mapB {kind = fn _ => fn k => k, |
112 con = fn _ => fn c => c, | 150 con = fn _ => fn c => c, |
113 exp = fn (xn, rep) => fn e => | 151 exp = fn (xn, rep) => fn e => |
114 case e of | 152 case e of |
115 ERel xn' => | 153 ERel xn' => |
116 (case Int.compare (xn', xn) of | 154 (case Int.compare (xn', xn) of |
126 | 164 |
127 exception UnboundRel of int | 165 exception UnboundRel of int |
128 exception UnboundNamed of int | 166 exception UnboundNamed of int |
129 | 167 |
130 type env = { | 168 type env = { |
169 relK : string list, | |
170 | |
131 relC : (string * kind) list, | 171 relC : (string * kind) list, |
132 namedC : (string * kind * con option) IM.map, | 172 namedC : (string * kind * con option) IM.map, |
133 | 173 |
134 datatypes : (string * string list * (string * int * con option) list) IM.map, | 174 datatypes : (string * string list * (string * int * con option) list) IM.map, |
135 constructors : (string * string list * con option * int) IM.map, | 175 constructors : (string * string list * con option * int) IM.map, |
137 relE : (string * con) list, | 177 relE : (string * con) list, |
138 namedE : (string * con * exp option * string) IM.map | 178 namedE : (string * con * exp option * string) IM.map |
139 } | 179 } |
140 | 180 |
141 val empty = { | 181 val empty = { |
182 relK = [], | |
183 | |
142 relC = [], | 184 relC = [], |
143 namedC = IM.empty, | 185 namedC = IM.empty, |
144 | 186 |
145 datatypes = IM.empty, | 187 datatypes = IM.empty, |
146 constructors = IM.empty, | 188 constructors = IM.empty, |
147 | 189 |
148 relE = [], | 190 relE = [], |
149 namedE = IM.empty | 191 namedE = IM.empty |
150 } | 192 } |
151 | 193 |
194 fun pushKRel (env : env) x = | |
195 {relK = x :: #relK env, | |
196 | |
197 relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env), | |
198 namedC = #namedC env, | |
199 | |
200 relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env), | |
201 namedE = #namedE env, | |
202 | |
203 datatypes = #datatypes env, | |
204 constructors = #constructors env | |
205 } | |
206 | |
207 fun lookupKRel (env : env) n = | |
208 (List.nth (#relK env, n)) | |
209 handle Subscript => raise UnboundRel n | |
210 | |
152 fun pushCRel (env : env) x k = | 211 fun pushCRel (env : env) x k = |
153 {relC = (x, k) :: #relC env, | 212 {relK = #relK env, |
213 | |
214 relC = (x, k) :: #relC env, | |
154 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), | 215 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), |
155 | 216 |
156 datatypes = #datatypes env, | 217 datatypes = #datatypes env, |
157 constructors = #constructors env, | 218 constructors = #constructors env, |
158 | 219 |
162 fun lookupCRel (env : env) n = | 223 fun lookupCRel (env : env) n = |
163 (List.nth (#relC env, n)) | 224 (List.nth (#relC env, n)) |
164 handle Subscript => raise UnboundRel n | 225 handle Subscript => raise UnboundRel n |
165 | 226 |
166 fun pushCNamed (env : env) x n k co = | 227 fun pushCNamed (env : env) x n k co = |
167 {relC = #relC env, | 228 {relK = #relK env, |
229 | |
230 relC = #relC env, | |
168 namedC = IM.insert (#namedC env, n, (x, k, co)), | 231 namedC = IM.insert (#namedC env, n, (x, k, co)), |
169 | 232 |
170 datatypes = #datatypes env, | 233 datatypes = #datatypes env, |
171 constructors = #constructors env, | 234 constructors = #constructors env, |
172 | 235 |
177 case IM.find (#namedC env, n) of | 240 case IM.find (#namedC env, n) of |
178 NONE => raise UnboundNamed n | 241 NONE => raise UnboundNamed n |
179 | SOME x => x | 242 | SOME x => x |
180 | 243 |
181 fun pushDatatype (env : env) x n xs xncs = | 244 fun pushDatatype (env : env) x n xs xncs = |
182 {relC = #relC env, | 245 {relK = #relK env, |
246 | |
247 relC = #relC env, | |
183 namedC = #namedC env, | 248 namedC = #namedC env, |
184 | 249 |
185 datatypes = IM.insert (#datatypes env, n, (x, xs, xncs)), | 250 datatypes = IM.insert (#datatypes env, n, (x, xs, xncs)), |
186 constructors = foldl (fn ((x, n', to), constructors) => | 251 constructors = foldl (fn ((x, n', to), constructors) => |
187 IM.insert (constructors, n', (x, xs, to, n))) | 252 IM.insert (constructors, n', (x, xs, to, n))) |
199 case IM.find (#constructors env, n) of | 264 case IM.find (#constructors env, n) of |
200 NONE => raise UnboundNamed n | 265 NONE => raise UnboundNamed n |
201 | SOME x => x | 266 | SOME x => x |
202 | 267 |
203 fun pushERel (env : env) x t = | 268 fun pushERel (env : env) x t = |
204 {relC = #relC env, | 269 {relK = #relK env, |
270 | |
271 relC = #relC env, | |
205 namedC = #namedC env, | 272 namedC = #namedC env, |
206 | 273 |
207 datatypes = #datatypes env, | 274 datatypes = #datatypes env, |
208 constructors = #constructors env, | 275 constructors = #constructors env, |
209 | 276 |
213 fun lookupERel (env : env) n = | 280 fun lookupERel (env : env) n = |
214 (List.nth (#relE env, n)) | 281 (List.nth (#relE env, n)) |
215 handle Subscript => raise UnboundRel n | 282 handle Subscript => raise UnboundRel n |
216 | 283 |
217 fun pushENamed (env : env) x n t eo s = | 284 fun pushENamed (env : env) x n t eo s = |
218 {relC = #relC env, | 285 {relK = #relK env, |
286 | |
287 relC = #relC env, | |
219 namedC = #namedC env, | 288 namedC = #namedC env, |
220 | 289 |
221 datatypes = #datatypes env, | 290 datatypes = #datatypes env, |
222 constructors = #constructors env, | 291 constructors = #constructors env, |
223 | 292 |