Mercurial > urweb
comparison src/corify.sml @ 49:874e877d2c51
Detecting FFI functions
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 22 Jun 2008 10:00:25 -0400 |
parents | 0a5c312de09a |
children | d37518b67bd2 |
comparison
equal
deleted
inserted
replaced
48:0a5c312de09a | 49:874e877d2c51 |
---|---|
58 | 58 |
59 val empty : t | 59 val empty : t |
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 -> t | 63 val ffi : string -> L'.con SM.map -> t |
64 | 64 |
65 val bindCore : t -> string -> int -> t * int | 65 val bindCore : t -> string -> int -> t * int |
66 val lookupCoreById : t -> int -> int option | 66 val lookupCoreById : t -> int -> int option |
67 | 67 |
68 datatype core = | 68 datatype core = |
69 Normal of int | 69 Normal of int |
70 | Ffi of string | 70 | Ffi of string * L'.con option |
71 val lookupCoreByName : t -> string -> core | 71 val lookupCoreByName : t -> string -> core |
72 | 72 |
73 val bindStr : t -> string -> int -> t -> t | 73 val bindStr : t -> string -> int -> t -> t |
74 val lookupStrById : t -> int -> t | 74 val lookupStrById : t -> int -> t |
75 val lookupStrByName : string * t -> t | 75 val lookupStrByName : string * t -> t |
81 | 81 |
82 datatype flattening = | 82 datatype flattening = |
83 FNormal of {core : int SM.map, | 83 FNormal of {core : int SM.map, |
84 strs : flattening SM.map, | 84 strs : flattening SM.map, |
85 funs : (int * L.str) SM.map} | 85 funs : (int * L.str) SM.map} |
86 | FFfi of string | 86 | FFfi of string * L'.con SM.map |
87 | 87 |
88 type t = { | 88 type t = { |
89 core : int IM.map, | 89 core : int IM.map, |
90 strs : flattening IM.map, | 90 strs : flattening IM.map, |
91 funs : (int * L.str) IM.map, | 91 funs : (int * L.str) IM.map, |
101 nested = [] | 101 nested = [] |
102 } | 102 } |
103 | 103 |
104 datatype core = | 104 datatype core = |
105 Normal of int | 105 Normal of int |
106 | Ffi of string | 106 | Ffi of string * L'.con option |
107 | 107 |
108 fun bindCore {core, strs, funs, current, nested} s n = | 108 fun bindCore {core, strs, funs, current, nested} s n = |
109 let | 109 let |
110 val n' = alloc () | 110 val n' = alloc () |
111 | 111 |
127 | 127 |
128 fun lookupCoreById ({core, ...} : t) n = IM.find (core, n) | 128 fun lookupCoreById ({core, ...} : t) n = IM.find (core, n) |
129 | 129 |
130 fun lookupCoreByName ({current, ...} : t) x = | 130 fun lookupCoreByName ({current, ...} : t) x = |
131 case current of | 131 case current of |
132 FFfi m => Ffi m | 132 FFfi (m, cmap) => Ffi (m, SM.find (cmap, x)) |
133 | FNormal {core, ...} => | 133 | FNormal {core, ...} => |
134 case SM.find (core, x) of | 134 case SM.find (core, x) of |
135 NONE => raise Fail "Corify.St.lookupCoreByName" | 135 NONE => raise Fail "Corify.St.lookupCoreByName" |
136 | SOME n => Normal n | 136 | SOME n => Normal n |
137 | 137 |
157 current = m1, | 157 current = m1, |
158 nested = rest}, | 158 nested = rest}, |
159 inner = dummy current} | 159 inner = dummy current} |
160 | leave _ = raise Fail "Corify.St.leave" | 160 | leave _ = raise Fail "Corify.St.leave" |
161 | 161 |
162 fun ffi m = dummy (FFfi m) | 162 fun ffi m cmap = dummy (FFfi (m, cmap)) |
163 | 163 |
164 fun bindStr ({core, strs, funs, current = FNormal {core = mcore, strs = mstrs, funs = mfuns}, nested} : t) | 164 fun bindStr ({core, strs, funs, current = FNormal {core = mcore, strs = mstrs, funs = mfuns}, nested} : t) |
165 x n ({current = f, ...} : t) = | 165 x n ({current = f, ...} : t) = |
166 {core = core, | 166 {core = core, |
167 strs = IM.insert (strs, n, f), | 167 strs = IM.insert (strs, n, f), |
231 val st = St.lookupStrById st m | 231 val st = St.lookupStrById st m |
232 val st = foldl St.lookupStrByName st ms | 232 val st = foldl St.lookupStrByName st ms |
233 in | 233 in |
234 case St.lookupCoreByName st x of | 234 case St.lookupCoreByName st x of |
235 St.Normal n => (L'.CNamed n, loc) | 235 St.Normal n => (L'.CNamed n, loc) |
236 | St.Ffi m => (L'.CFfi (m, x), loc) | 236 | St.Ffi (m, _) => (L'.CFfi (m, x), loc) |
237 end | 237 end |
238 | 238 |
239 | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc) | 239 | 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) | 240 | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon st c), loc) |
241 | 241 |
258 val st = St.lookupStrById st m | 258 val st = St.lookupStrById st m |
259 val st = foldl St.lookupStrByName st ms | 259 val st = foldl St.lookupStrByName st ms |
260 in | 260 in |
261 case St.lookupCoreByName st x of | 261 case St.lookupCoreByName st x of |
262 St.Normal n => (L'.ENamed n, loc) | 262 St.Normal n => (L'.ENamed n, loc) |
263 | St.Ffi m => (L'.EFfi (m, x), loc) | 263 | St.Ffi (_, NONE) => raise Fail "corifyExp: Unknown type for FFI expression variable" |
264 | St.Ffi (m, SOME t) => | |
265 case t of | |
266 t as (L'.TFun _, _) => | |
267 let | |
268 fun getArgs (all as (t, _), args) = | |
269 case t of | |
270 L'.TFun (dom, ran) => getArgs (ran, dom :: args) | |
271 | _ => (all, rev args) | |
272 | |
273 val (result, args) = getArgs (t, []) | |
274 | |
275 val (app, _) = foldl (fn (_, (app, n)) => | |
276 ((L'.EApp (app, (L'.ERel n, loc)), loc), | |
277 n - 1)) ((L'.EFfi (m, x), loc), | |
278 length args - 1) args | |
279 val (abs, _, _) = foldr (fn (t, (abs, ran, n)) => | |
280 ((L'.EAbs ("arg" ^ Int.toString n, | |
281 t, | |
282 ran, | |
283 abs), loc), | |
284 (L'.TFun (t, ran), loc), | |
285 n - 1)) (app, result, length args - 1) args | |
286 in | |
287 abs | |
288 end | |
289 | _ => (L'.EFfi (m, x), loc) | |
264 end | 290 end |
265 | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc) | 291 | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc) |
266 | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc) | 292 | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc) |
267 | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc) | 293 | L.ECApp (e1, c) => (L'.ECApp (corifyExp st e1, corifyCon st c), loc) |
268 | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc) | 294 | L.ECAbs (x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp st e1), loc) |
297 val st = St.bindStr outer x n inner | 323 val st = St.bindStr outer x n inner |
298 in | 324 in |
299 (ds, st) | 325 (ds, st) |
300 end | 326 end |
301 | 327 |
302 | L.DFfiStr (x, n, _) => | 328 | L.DFfiStr (m, n, (sgn, _)) => |
303 let | 329 (case sgn of |
304 val st = St.bindStr st x n (St.ffi x) | 330 L.SgnConst sgis => |
305 in | 331 let |
306 ([], st) | 332 val (ds, cmap, st) = |
307 end | 333 foldl (fn ((sgi, _), (ds, cmap, st)) => |
334 case sgi of | |
335 L.SgiConAbs (x, n, k) => | |
336 let | |
337 val (st, n') = St.bindCore st x n | |
338 in | |
339 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, | |
340 cmap, | |
341 st) | |
342 end | |
343 | L.SgiCon (x, n, k, _) => | |
344 let | |
345 val (st, n') = St.bindCore st x n | |
346 in | |
347 ((L'.DCon (x, n', corifyKind k, (L'.CFfi (m, x), loc)), loc) :: ds, | |
348 cmap, | |
349 st) | |
350 end | |
351 | |
352 | L.SgiVal (x, _, c) => | |
353 (ds, | |
354 SM.insert (cmap, x, corifyCon st c), | |
355 st) | |
356 | _ => (ds, cmap, st)) ([], SM.empty, st) sgis | |
357 | |
358 val st = St.bindStr st m n (St.ffi m cmap) | |
359 in | |
360 (rev ds, st) | |
361 end | |
362 | _ => raise Fail "Non-const signature for FFI structure") | |
308 | 363 |
309 | 364 |
310 and corifyStr ((str, _), st) = | 365 and corifyStr ((str, _), st) = |
311 case str of | 366 case str of |
312 L.StrConst ds => | 367 L.StrConst ds => |