Mercurial > urweb

comparison src/corify.sml @ 73:8b611ecc5f2d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Corify efold
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Jun 2008 11:32:29 -0400
parents 0ee10f4d73cf
children 275aaeb73f1f
comparison
equal deleted inserted replaced
72:0ee10f4d73cf 73:8b611ecc5f2d
60 60
61 val enter : t -> t 61 val enter : t -> t
62 val leave : t -> {outer : t, inner : t} 62 val leave : t -> {outer : t, inner : t}
63 val ffi : string -> L'.con SM.map -> t 63 val ffi : string -> L'.con SM.map -> t
64 64
65 val bindCore : t -> string -> int -> t * int 65 datatype core_con =
66 val lookupCoreById : t -> int -> int option 66 CNormal of int
67 67 | CFfi of string
68 datatype core = 68 val bindCon : t -> string -> int -> t * int
69 Normal of int 69 val lookupConById : t -> int -> int option
70 | Ffi of string * L'.con option 70 val lookupConByName : t -> string -> core_con
71 val lookupCoreByName : t -> string -> core 71
72 datatype core_val =
73 ENormal of int
74 | EFfi of string * L'.con
75 val bindVal : t -> string -> int -> t * int
76 val lookupValById : t -> int -> int option
77 val lookupValByName : t -> string -> core_val
72 78
73 val bindStr : t -> string -> int -> t -> t 79 val bindStr : t -> string -> int -> t -> t
74 val lookupStrById : t -> int -> t 80 val lookupStrById : t -> int -> t
75 val lookupStrByName : string * t -> t 81 val lookupStrByName : string * t -> t
76 82
78 val lookupFunctorById : t -> int -> int * L.str 84 val lookupFunctorById : t -> int -> int * L.str
79 val lookupFunctorByName : string * t -> int * L.str 85 val lookupFunctorByName : string * t -> int * L.str
80 end = struct 86 end = struct
81 87
82 datatype flattening = 88 datatype flattening =
83 FNormal of {core : int SM.map, 89 FNormal of {cons : int SM.map,
90 vals : int SM.map,
84 strs : flattening SM.map, 91 strs : flattening SM.map,
85 funs : (int * L.str) SM.map} 92 funs : (int * L.str) SM.map}
86 | FFfi of string * L'.con SM.map 93 | FFfi of {mod : string,
94 vals : L'.con SM.map}
87 95
88 type t = { 96 type t = {
89 core : int IM.map, 97 cons : int IM.map,
98 vals : int IM.map,
90 strs : flattening IM.map, 99 strs : flattening IM.map,
91 funs : (int * L.str) IM.map, 100 funs : (int * L.str) IM.map,
92 current : flattening, 101 current : flattening,
93 nested : flattening list 102 nested : flattening list
94 } 103 }
95 104
96 val empty = { 105 val empty = {
97 core = IM.empty, 106 cons = IM.empty,
107 vals = IM.empty,
98 strs = IM.empty, 108 strs = IM.empty,
99 funs = IM.empty, 109 funs = IM.empty,
100 current = FNormal { core = SM.empty, strs = SM.empty, funs = SM.empty }, 110 current = FNormal { cons = SM.empty, vals = SM.empty, strs = SM.empty, funs = SM.empty },
101 nested = [] 111 nested = []
102 } 112 }
103 113
104 datatype core = 114 datatype core_con =
105 Normal of int 115 CNormal of int
106 | Ffi of string * L'.con option 116 | CFfi of string
107 117
108 fun bindCore {core, strs, funs, current, nested} s n = 118 datatype core_val =
119 ENormal of int
120 | EFfi of string * L'.con
121
122 fun bindCon {cons, vals, strs, funs, current, nested} s n =
109 let 123 let
110 val n' = alloc () 124 val n' = alloc ()
111 125
112 val current = 126 val current =
113 case current of 127 case current of
114 FFfi _ => raise Fail "Binding inside FFfi" 128 FFfi _ => raise Fail "Binding inside FFfi"
115 | FNormal {core, strs, funs} => 129 | FNormal {cons, vals, strs, funs} =>
116 FNormal {core = SM.insert (core, s, n'), 130 FNormal {cons = SM.insert (cons, s, n'),
131 vals = vals,
117 strs = strs, 132 strs = strs,
118 funs = funs} 133 funs = funs}
119 in 134 in
120 ({core = IM.insert (core, n, n'), 135 ({cons = IM.insert (cons, n, n'),
136 vals = vals,
121 strs = strs, 137 strs = strs,
122 funs = funs, 138 funs = funs,
123 current = current, 139 current = current,
124 nested = nested}, 140 nested = nested},
125 n') 141 n')
126 end 142 end
127 143
128 fun lookupCoreById ({core, ...} : t) n = IM.find (core, n) 144 fun lookupConById ({cons, ...} : t) n = IM.find (cons, n)
129 145
130 fun lookupCoreByName ({current, ...} : t) x = 146 fun lookupConByName ({current, ...} : t) x =
131 case current of 147 case current of
132 FFfi (m, cmap) => Ffi (m, SM.find (cmap, x)) 148 FFfi {mod = m, ...} => CFfi m
133 | FNormal {core, ...} => 149 | FNormal {cons, ...} =>
134 case SM.find (core, x) of 150 case SM.find (cons, x) of
135 NONE => raise Fail "Corify.St.lookupCoreByName" 151 NONE => raise Fail "Corify.St.lookupConByName"
136 | SOME n => Normal n 152 | SOME n => CNormal n
137 153
138 fun enter {core, strs, funs, current, nested} = 154 fun bindVal {cons, vals, strs, funs, current, nested} s n =
139 {core = core, 155 let
156 val n' = alloc ()
157
158 val current =
159 case current of
160 FFfi _ => raise Fail "Binding inside FFfi"
161 | FNormal {cons, vals, strs, funs} =>
162 FNormal {cons = cons,
163 vals = SM.insert (vals, s, n'),
164 strs = strs,
165 funs = funs}
166 in
167 ({cons = cons,
168 vals = IM.insert (vals, n, n'),
169 strs = strs,
170 funs = funs,
171 current = current,
172 nested = nested},
173 n')
174 end
175
176 fun lookupValById ({vals, ...} : t) n = IM.find (vals, n)
177
178 fun lookupValByName ({current, ...} : t) x =
179 case current of
180 FFfi {mod = m, vals, ...} =>
181 (case SM.find (vals, x) of
182 NONE => raise Fail "Corify.St.lookupValByName: no type for FFI val"
183 | SOME t => EFfi (m, t))
184 | FNormal {vals, ...} =>
185 case SM.find (vals, x) of
186 NONE => raise Fail "Corify.St.lookupValByName"
187 | SOME n => ENormal n
188
189 fun enter {cons, vals, strs, funs, current, nested} =
190 {cons = cons,
191 vals = vals,
140 strs = strs, 192 strs = strs,
141 funs = funs, 193 funs = funs,
142 current = FNormal {core = SM.empty, 194 current = FNormal {cons = SM.empty,
195 vals = SM.empty,
143 strs = SM.empty, 196 strs = SM.empty,
144 funs = SM.empty}, 197 funs = SM.empty},
145 nested = current :: nested} 198 nested = current :: nested}
146 199
147 fun dummy f = {core = IM.empty, 200 fun dummy f = {cons = IM.empty,
201 vals = IM.empty,
148 strs = IM.empty, 202 strs = IM.empty,
149 funs = IM.empty, 203 funs = IM.empty,
150 current = f, 204 current = f,
151 nested = []} 205 nested = []}
152 206
153 fun leave {core, strs, funs, current, nested = m1 :: rest} = 207 fun leave {cons, vals, strs, funs, current, nested = m1 :: rest} =
154 {outer = {core = core, 208 {outer = {cons = cons,
209 vals = vals,
155 strs = strs, 210 strs = strs,
156 funs = funs, 211 funs = funs,
157 current = m1, 212 current = m1,
158 nested = rest}, 213 nested = rest},
159 inner = dummy current} 214 inner = dummy current}
160 | leave _ = raise Fail "Corify.St.leave" 215 | leave _ = raise Fail "Corify.St.leave"
161 216
162 fun ffi m cmap = dummy (FFfi (m, cmap)) 217 fun ffi m vals = dummy (FFfi {mod = m, vals = vals})
163 218
164 fun bindStr ({core, strs, funs, current = FNormal {core = mcore, strs = mstrs, funs = mfuns}, nested} : t) 219 fun bindStr ({cons, vals, strs, funs,
220 current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
165 x n ({current = f, ...} : t) = 221 x n ({current = f, ...} : t) =
166 {core = core, 222 {cons = cons,
223 vals = vals,
167 strs = IM.insert (strs, n, f), 224 strs = IM.insert (strs, n, f),
168 funs = funs, 225 funs = funs,
169 current = FNormal {core = mcore, 226 current = FNormal {cons = mcons,
170 strs = SM.insert (mstrs, x, f), 227 vals = mvals,
171 funs = mfuns}, 228 strs = SM.insert (mstrs, x, f),
229 funs = mfuns},
172 nested = nested} 230 nested = nested}
173 | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr" 231 | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr"
174 232
175 fun lookupStrById ({strs, ...} : t) n = 233 fun lookupStrById ({strs, ...} : t) n =
176 case IM.find (strs, n) of 234 case IM.find (strs, n) of
181 (case SM.find (strs, m) of 239 (case SM.find (strs, m) of
182 NONE => raise Fail "Corify.St.lookupStrByName" 240 NONE => raise Fail "Corify.St.lookupStrByName"
183 | SOME f => dummy f) 241 | SOME f => dummy f)
184 | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName" 242 | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName"
185 243
186 fun bindFunctor ({core, strs, funs, current = FNormal {core = mcore, strs = mstrs, funs = mfuns}, nested} : t) 244 fun bindFunctor ({cons, vals, strs, funs,
245 current = FNormal {cons = mcons, vals = mvals, strs = mstrs, funs = mfuns}, nested} : t)
187 x n na str = 246 x n na str =
188 {core = core, 247 {cons = cons,
248 vals = vals,
189 strs = strs, 249 strs = strs,
190 funs = IM.insert (funs, n, (na, str)), 250 funs = IM.insert (funs, n, (na, str)),
191 current = FNormal {core = mcore, 251 current = FNormal {cons = mcons,
252 vals = mvals,
192 strs = mstrs, 253 strs = mstrs,
193 funs = SM.insert (mfuns, x, (na, str))}, 254 funs = SM.insert (mfuns, x, (na, str))},
194 nested = nested} 255 nested = nested}
195 | bindFunctor _ _ _ _ _ = raise Fail "Corify.St.bindFunctor" 256 | bindFunctor _ _ _ _ _ = raise Fail "Corify.St.bindFunctor"
196 257
221 | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc) 282 | L.TCFun (x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon st t), loc)
222 | L.TRecord c => (L'.TRecord (corifyCon st c), loc) 283 | L.TRecord c => (L'.TRecord (corifyCon st c), loc)
223 284
224 | L.CRel n => (L'.CRel n, loc) 285 | L.CRel n => (L'.CRel n, loc)
225 | L.CNamed n => 286 | L.CNamed n =>
226 (case St.lookupCoreById st n of 287 (case St.lookupConById st n of
227 NONE => (L'.CNamed n, loc) 288 NONE => (L'.CNamed n, loc)
228 | SOME n => (L'.CNamed n, loc)) 289 | SOME n => (L'.CNamed n, loc))
229 | L.CModProj (m, ms, x) => 290 | L.CModProj (m, ms, x) =>
230 let 291 let
231 val st = St.lookupStrById st m 292 val st = St.lookupStrById st m
232 val st = foldl St.lookupStrByName st ms 293 val st = foldl St.lookupStrByName st ms
233 in 294 in
234 case St.lookupCoreByName st x of 295 case St.lookupConByName st x of
235 St.Normal n => (L'.CNamed n, loc) 296 St.CNormal n => (L'.CNamed n, loc)
236 | St.Ffi (m, _) => (L'.CFfi (m, x), loc) 297 | St.CFfi m => (L'.CFfi (m, x), loc)
237 end 298 end
238 299
239 | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc) 300 | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc)
240 | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc) 301 | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc)
241 302
249 fun corifyExp st (e, loc) = 310 fun corifyExp st (e, loc) =
250 case e of 311 case e of
251 L.EPrim p => (L'.EPrim p, loc) 312 L.EPrim p => (L'.EPrim p, loc)
252 | L.ERel n => (L'.ERel n, loc) 313 | L.ERel n => (L'.ERel n, loc)
253 | L.ENamed n => 314 | L.ENamed n =>
254 (case St.lookupCoreById st n of 315 (case St.lookupValById st n of
255 NONE => (L'.ENamed n, loc) 316 NONE => (L'.ENamed n, loc)
256 | SOME n => (L'.ENamed n, loc)) 317 | SOME n => (L'.ENamed n, loc))
257 | L.EModProj (m, ms, x) => 318 | L.EModProj (m, ms, x) =>
258 let 319 let
259 val st = St.lookupStrById st m 320 val st = St.lookupStrById st m
260 val st = foldl St.lookupStrByName st ms 321 val st = foldl St.lookupStrByName st ms
261 in 322 in
262 case St.lookupCoreByName st x of 323 case St.lookupValByName st x of
263 St.Normal n => (L'.ENamed n, loc) 324 St.ENormal n => (L'.ENamed n, loc)
264 | St.Ffi (_, NONE) => raise Fail "corifyExp: Unknown type for FFI expression variable" 325 | St.EFfi (m, t) =>
265 | St.Ffi (m, SOME t) =>
266 case t of 326 case t of
267 (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) => 327 (L'.TFun (dom as (L'.TRecord (L'.CRecord (_, []), _), _), ran), _) =>
268 (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc) 328 (L'.EAbs ("arg", dom, ran, (L'.EFfiApp (m, x, []), loc)), loc)
269 | t as (L'.TFun _, _) => 329 | t as (L'.TFun _, _) =>
270 let 330 let
297 | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc) 357 | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc)
298 358
299 | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc) 359 | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc)
300 | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c, 360 | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c,
301 {field = corifyCon st field, rest = corifyCon st rest}), loc) 361 {field = corifyCon st field, rest = corifyCon st rest}), loc)
302 | L.EFold _ => raise Fail "Corify EFold" 362 | L.EFold k => (L'.EFold (corifyKind k), loc)
303 363
304 fun corifyDecl ((d, loc : EM.span), st) = 364 fun corifyDecl ((d, loc : EM.span), st) =
305 case d of 365 case d of
306 L.DCon (x, n, k, c) => 366 L.DCon (x, n, k, c) =>
307 let 367 let
308 val (st, n) = St.bindCore st x n 368 val (st, n) = St.bindCon st x n
309 in 369 in
310 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) 370 ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st)
311 end 371 end
312 | L.DVal (x, n, t, e) => 372 | L.DVal (x, n, t, e) =>
313 let 373 let
314 val (st, n) = St.bindCore st x n 374 val (st, n) = St.bindVal st x n
315 in 375 in
316 ([(L'.DVal (x, n, corifyCon st t, corifyExp st e), loc)], st) 376 ([(L'.DVal (x, n, corifyCon st t, corifyExp st e), loc)], st)
317 end 377 end
318 378
319 | L.DSgn _ => ([], st) 379 | L.DSgn _ => ([], st)
336 val (ds, cmap, st) = 396 val (ds, cmap, st) =
337 foldl (fn ((sgi, _), (ds, cmap, st)) => 397 foldl (fn ((sgi, _), (ds, cmap, st)) =>
338 case sgi of 398 case sgi of
339 L.SgiConAbs (x, n, k) => 399 L.SgiConAbs (x, n, k) =>
340 let 400 let
341 val (st, n') = St.bindCore st x n 401 val (st, n') = St.bindCon st x n
342 in 402 in
343 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, 403 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
344 cmap, 404 cmap,
345 st) 405 st)
346 end 406 end
347 | L.SgiCon (x, n, k, _) => 407 | L.SgiCon (x, n, k, _) =>
348 let 408 let
349 val (st, n') = St.bindCore st x n 409 val (st, n') = St.bindCon st x n
350 in 410 in
351 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, 411 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds,
352 cmap, 412 cmap,
353 st) 413 st)
354 end 414 end