Mercurial > urweb

comparison src/core_env.sml @ 626:230654093b51

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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