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

CHANGELOG+2

compare with master

unifiedsplit

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

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

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

22* 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

23

25

24New in 0.9.16:

26New in 0.9.16:

25--------------

27--------------

libs/prelude/IO.idr+5−1

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

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

92liftPrimIO = MkIO

93

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

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

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

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

99+run__IO f = call__IO f

96

100

97unsafePerformIO : IO' ffi a -> a

101unsafePerformIO : IO' ffi a -> a

98unsafePerformIO (MkIO f) = unsafePerformPrimIO

102unsafePerformIO (MkIO f) = unsafePerformPrimIO

src/IRTS/CodegenC.hs+11−2

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

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

590

591mkBody 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" ++

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

594 where push i [] = ""

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

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

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

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

603

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

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

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

605

614

606ctype (FCon c)

615ctype (FCon c)

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

615 | c == sUN "C_Any" = "VAL"

624 | c == sUN "C_Any" = "VAL"

616ctype (FStr s) = s

625ctype (FStr s) = s

617ctype FUnknown = "void*"

626ctype FUnknown = "void*"

618−ctype FWorld = "void*"

627+ctype (FIO t) = ctype t

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

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

620

629

621carith (FCon i)

630carith (FCon i)

src/IRTS/Exports.hs+1−4

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

74 = toFDescBase b

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

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

77− = toFDescBase b

77+ = FIO $ toFDescBase b

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

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

80 = toFDescRet t

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

92

93toFDescArgs :: Term -> [FDesc]

94toFDescArgs 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

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

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

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

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

100 = toFDescBase b : toFDescArgs t

97 = toFDescBase b : toFDescArgs t

src/IRTS/Lang.hs+1−1

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

40data FDesc = FCon Name

41 | FStr String

42 | FUnknown

43− | FWorld

43+ | FIO FDesc

44 | FApp Name [FDesc]

45 deriving (Show, Eq)

46

src/Idris/Erasure.hs+3−2

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

196 [ [] ==> concat

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

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

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

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

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

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

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

201

202

202 -- Explicit usage declarations from a %used pragma

203 -- Explicit usage declarations from a %used pragma

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

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