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 =>