5ae43bb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Support IO in foreign exports

commit5ae43bb26f2743750ae8b2d190d325f589858206 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 7 Mar 2015, 21:59 (12 years ago) parentd4371e6

6 files changed+23−10

compare with master

unifiedsplit

CHANGELOG+2 libs/prelude/IO.idr+5−1 src/IRTS/CodegenC.hs+11−2 src/IRTS/Exports.hs+1−4 src/IRTS/Lang.hs+1−1 src/Idris/Erasure.hs+3−2

CHANGELOG+2

@@ -20,6 +20,8 @@ New in 0.9.17:

2020 an extra argument of type TTName. This allows more understandable

2121 dynamic errors in DSL code and more readable code generation results.

2222* DSL notation can now be applied with $

23+* Added FFI_Export type which allows Idris functions to be exportoed and

24+ called from foreign code

2325

2426New in 0.9.16:

2527--------------

libs/prelude/IO.idr+5−1

@@ -91,8 +91,12 @@ io_return x = MkIO (\w => prim_io_return x)

9191liftPrimIO : (World -> PrimIO a) -> IO' l a

9292liftPrimIO = MkIO

9393

94+call__IO : IO' l a -> PrimIO a

95+call__IO (MkIO f) = f (TheWorld prim__TheWorld)

96+

97+-- Concrete type makes it easier to elaborate at top level

9498run__IO : IO' l () -> PrimIO ()

95−run__IO (MkIO f) = f (TheWorld prim__TheWorld)

99+run__IO f = call__IO f

96100

97101unsafePerformIO : IO' ffi a -> a

98102unsafePerformIO (MkIO f) = unsafePerformPrimIO

src/IRTS/CodegenC.hs+11−2

@@ -589,7 +589,7 @@ ifaceC (ExportFun n cn ret args)

589589 argNames = zipWith (++) (repeat "arg") (map show [0..])

590590

591591mkBody n as t = indent 1 ++ "INITFRAME;\n" ++

592− indent 1 ++ "RESERVE(" ++ show (length as) ++ ");\n" ++

592+ indent 1 ++ "RESERVE(" ++ show (max (length as) 3) ++ ");\n" ++

593593 push 0 as ++ call n ++ retval t

594594 where push i [] = ""

595595 push i ((n, t) : ts) = indent 1 ++ c_irts (toFType t)

@@ -601,6 +601,15 @@ mkBody n as t = indent 1 ++ "INITFRAME;\n" ++

601601 indent 1 ++ "ADDTOP(" ++ show (length as) ++ ");\n" ++

602602 indent 1 ++ "CALL(" ++ cname n ++ ");\n"

603603

604+ retval (FIO t)

605+ = indent 1 ++ "TOP(0) = NULL;\n" ++

606+ indent 1 ++ "TOP(1) = NULL;\n" ++

607+ indent 1 ++ "TOP(2) = RVAL;\n" ++

608+ indent 1 ++ "STOREOLD;\n" ++

609+ indent 1 ++ "BASETOP(0);\n" ++

610+ indent 1 ++ "ADDTOP(3);\n" ++

611+ indent 1 ++ "CALL(" ++ cname (sUN "call__IO") ++ ");\n" ++

612+ retval t

604613 retval t = indent 1 ++ "return " ++ irts_c (toFType t) "RVAL" ++ ";\n"

605614

606615ctype (FCon c)

@@ -615,7 +624,7 @@ ctype (FApp c [_])

615624 | c == sUN "C_Any" = "VAL"

616625ctype (FStr s) = s

617626ctype FUnknown = "void*"

618−ctype FWorld = "void*"

627+ctype (FIO t) = ctype t

619628ctype t = error "Can't happen: Not a valid interface type " ++ show t

620629

621630carith (FCon i)

src/IRTS/Exports.hs+1−4

@@ -74,7 +74,7 @@ toFDescRet tm

7474 = toFDescBase b

7575 | (P _ io _, [_,_,_,b]) <- unApply tm,

7676 io == sNS (sUN "FFI_IO") ["FFI_Export"]

77− = toFDescBase b

77+ = FIO $ toFDescBase b

7878 | (P _ fun _, [_,_,_,_,_,t]) <- unApply tm,

7979 fun == sNS (sUN "FFI_Fun") ["FFI_Export"]

8080 = toFDescRet t

@@ -92,9 +92,6 @@ toFDescBase tm

9292

9393toFDescArgs :: Term -> [FDesc]

9494toFDescArgs tm

95− | (P _ io _, [_,_,_,b]) <- unApply tm,

96− io == sNS (sUN "FFI_IO") ["FFI_Export"]

97− = [FWorld] -- World, unused but needed explicitly as an argument

9895 | (P _ fun _, [_,_,_,_,b,t]) <- unApply tm,

9996 fun == sNS (sUN "FFI_Fun") ["FFI_Export"]

10097 = toFDescBase b : toFDescArgs t

src/IRTS/Lang.hs+1−1

@@ -40,7 +40,7 @@ data LExp = LV LVar

4040data FDesc = FCon Name

4141 | FStr String

4242 | FUnknown

43− | FWorld

43+ | FIO FDesc

4444 | FApp Name [FDesc]

4545 deriving (Show, Eq)

4646

src/Idris/Erasure.hs+3−2

@@ -196,8 +196,9 @@ buildDepMap ci used ctx startNames = addPostulates used $

196196 [ [] ==> concat

197197 -- Main.main ( + export lists) and run__IO, are always evaluated

198198 -- but they elude analysis since they come from the seed term.

199− [(map (\n -> (n, Result)) startNames),

200− [(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]

199+ [(map (\n -> (n, Result)) startNames)

200+ ,[(sUN "run__IO", Result), (sUN "run__IO", Arg 1)]

201+ ,[(sUN "call__IO", Result), (sUN "call__IO", Arg 2)]

201202

202203 -- Explicit usage declarations from a %used pragma

203204 , map (\(n, i) -> (n, Arg i)) used