git.iko.soy/Idris-dev
on master help sign in
Make functions work in JS FFI
commit00118357ae8c5492a60349fba84a4d7ba330f222 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 21 Jan 2015, 13:06 (12 years ago) parent1950393
2 files changed+17−1
compare with master
unifiedsplit
src/IRTS/CodegenJavaScript.hs+10 src/Idris/Erasure.hs+7−1
src/IRTS/CodegenJavaScript.hs+10
@@ -1351,6 +1351,14 @@ toAType (FCon i)
13511351 | i == sUN "JS_IntNative" = ATInt ITNative
13521352toAType t = error (show t ++ " not defined in toAType")
13531353
1354+toFnType (FApp c [_,_,s,t])
1355+ | c == sUN "JS_Fn" = toFnType t
1356+toFnType (FApp c [_,_,r])
1357+ | c == sUN "JS_FnIO" = FFunctionIO
1358+toFnType (FApp c [_,r])
1359+ | c == sUN "JS_FnBase" = FFunction
1360+toFnType t = error (show t ++ " not defined in toFnType")
1361+
13541362toFType (FCon c)
13551363 | c == sUN "JS_Str" = FString
13561364 | c == sUN "JS_Float" = FArith ATFloat
@@ -1358,5 +1366,7 @@ toFType (FCon c)
13581366 | c == sUN "JS_Unit" = FUnit
13591367toFType (FApp c [_,ity])
13601368 | c == sUN "JS_IntT" = FArith (toAType ity)
1369+toFType (FApp c [_,fty])
1370+ | c == sUN "JS_FnT" = toFnType fty
13611371toFType t = error (show t ++ " not yet defined in toFType")
13621372
src/Idris/Erasure.hs+7−1
@@ -199,8 +199,14 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
199199 , it "MkIO" [2]
200200 , it "prim__IO" [1]
201201
202+ -- temporary hacks for preventing erasure of these in foreign
203+ -- calls. TODO: make this not a hack, and possible to set
204+ -- in Idris source
205+ , it "MkJsFn" [1]
206+ , it "MkRaw" [1]
207+
202208 , [(pairCon, Arg 2),
203− (pairCon, Arg 3)] -- TMP HACK
209+ (pairCon, Arg 3)] -- Used in foreign calls
204210
205211 -- these have been discovered as builtins but are not listed
206212 -- among Idris.Primitives.primitives