894db6f · Idris-dev · git.iko.soy

contribs/lib/SQLite3/Sqlite3.idr+3−3

compare with master

unifiedsplit

@@ -2,9 +2,9 @@ module Sqlite3

2import Sqlexpr

3

4

5−%lib "sqlite3"

5+%lib C "sqlite3"

6−%link "sqlite3api.o"

6+%link C "sqlite3api.o"

7−%include "sqlite3api.h"

7+%include C "sqlite3api.h"

8

9-----------------------------------------------------------------------------

10-- |

lib/Prelude.idr+2−2

@@ -139,8 +139,8 @@ instance Monad List where

139

140---- some mathematical operations

141

142−%include "math.h"

142+%include C "math.h"

143−%lib "m"

143+%lib C "m"

144

145pow : (Num a) => a -> Nat -> a

146pow x O = 1

samples/javaffi.idr+2−2

@@ -1,7 +1,7 @@

1module Main

2

3−%include "com.google.common.math.IntMath"

3+%include Java "com.google.common.math.IntMath"

4−%lib "com.google.guava:guava:14.0"

4+%lib Java "com.google.guava:guava:14.0"

5

6binom : Int -> Int -> IO Int

7binom n k = mkForeign (FFun "IntMath.binomial" [FInt, FInt] FInt) n k

src/IRTS/Compiler.hs+3−3

@@ -38,9 +38,9 @@ compile target f tm

38 defsIn <- mkDecls tm (concat used)

39 findUnusedArgs (concat used)

40 maindef <- irMain tm

41− objs <- getObjectFiles

41+ objs <- getObjectFiles target

42− libs <- getLibs

42+ libs <- getLibs target

43− hdrs <- getHdrs

43+ hdrs <- getHdrs target

44 let defs = defsIn ++ [(MN 0 "runMain", maindef)]

45 -- iputStrLn $ showSep "\n" (map show defs)

46 let (nexttag, tagged) = addTags 65536 (liftAll defs)

src/Idris/AbsSyntax.hs+15−12

@@ -30,17 +30,20 @@ import Util.System

30getContext :: Idris Context

31getContext = do i <- getIState; return (tt_ctxt i)

32

33−getObjectFiles :: Idris [FilePath]

33+forTarget :: Target -> [(Target, a)] -> [a]

34−getObjectFiles = do i <- getIState; return (idris_objs i)

34+forTarget tgt xs = [x | (tgt', x) <- xs, tgt == tgt']

35

36−addObjectFile :: FilePath -> Idris ()

36+getObjectFiles :: Target -> Idris [FilePath]

37−addObjectFile f = do i <- getIState; putIState $ i { idris_objs = f : idris_objs i }

37+getObjectFiles tgt = do i <- getIState; return (forTarget tgt $ idris_objs i)

38

39−getLibs :: Idris [String]

39+addObjectFile :: Target -> FilePath -> Idris ()

40−getLibs = do i <- getIState; return (idris_libs i)

40+addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = (tgt, f) : idris_objs i }

41

42+getLibs :: Target -> Idris [String]

43+getLibs tgt = do i <- getIState; return (forTarget tgt $ idris_libs i)

44+

42−addLib :: String -> Idris ()

45+addLib :: Target -> String -> Idris ()

43−addLib f = do i <- getIState; putIState $ i { idris_libs = f : idris_libs i }

46+addLib tgt f = do i <- getIState; putIState $ i { idris_libs = (tgt, f) : idris_libs i }

44

47

45addDyLib :: [String] -> Idris (Either DynamicLib String)

48addDyLib :: [String] -> Idris (Either DynamicLib String)

46addDyLib libs = do i <- getIState

49addDyLib libs = do i <- getIState

@@ -52,8 +55,8 @@ addDyLib libs = do i <- getIState

52 putIState $ i { idris_dynamic_libs = x:ls }

55 putIState $ i { idris_dynamic_libs = x:ls }

53 return (Left x)

56 return (Left x)

54

57

55−addHdr :: String -> Idris ()

58+addHdr :: Target -> String -> Idris ()

56−addHdr f = do i <- getIState; putIState $ i { idris_hdrs = f : idris_hdrs i }

59+addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = (tgt, f) : idris_hdrs i }

57

60

58addLangExt :: LanguageExt -> Idris ()

61addLangExt :: LanguageExt -> Idris ()

59addLangExt TypeProviders = do i <- getIState ; putIState $ i { idris_language_extensions = [TypeProviders] }

62addLangExt TypeProviders = do i <- getIState ; putIState $ i { idris_language_extensions = [TypeProviders] }

@@ -160,8 +163,8 @@ addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }

160clearIBC :: Idris ()

163clearIBC :: Idris ()

161clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }

164clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }

162

165

163−getHdrs :: Idris [String]

166+getHdrs :: Target -> Idris [String]

164−getHdrs = do i <- getIState; return (idris_hdrs i)

167+getHdrs tgt = do i <- getIState; return (forTarget tgt $ idris_hdrs i)

165

168

166setErrLine :: Int -> Idris ()

169setErrLine :: Int -> Idris ()

167setErrLine x = do i <- getIState;

170setErrLine x = do i <- getIState;

src/Idris/AbsSyntaxTree.hs+6−6

@@ -95,9 +95,9 @@ data IState = IState {

95 syntax_keywords :: [String],

96 imported :: [FilePath], -- ^ The imported modules

97 idris_scprims :: [(Name, (Int, PrimFn))],

98− idris_objs :: [FilePath],

98+ idris_objs :: [(Target, FilePath)],

99− idris_libs :: [String],

99+ idris_libs :: [(Target, String)],

100− idris_hdrs :: [String],

100+ idris_hdrs :: [(Target, String)],

101 proof_list :: [(Name, [String])],

102 errLine :: Maybe Int,

103 lastParse :: Maybe Name,

@@ -145,10 +145,10 @@ data IBCWrite = IBCFix FixDecl

145 | IBCSyntax Syntax

146 | IBCKeyword String

147 | IBCImport FilePath

148− | IBCObj FilePath

148+ | IBCObj Target FilePath

149− | IBCLib String

149+ | IBCLib Target String

150 | IBCDyLib String

151− | IBCHeader String

151+ | IBCHeader Target String

152 | IBCAccess Name Accessibility

153 | IBCTotal Name Totality

154 | IBCFlags Name [FnOpt]

src/Idris/IBC.hs+32−13

@@ -23,7 +23,7 @@ import Debug.Trace

23import Paths_idris

24

25ibcVersion :: Word8

26−ibcVersion = 29

26+ibcVersion = 30

27

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

@@ -38,10 +38,10 @@ data IBCFile = IBCFile { ver :: Word8,

38 ibc_optimise :: [(Name, OptInfo)],

39 ibc_syntax :: [Syntax],

40 ibc_keywords :: [String],

41− ibc_objs :: [FilePath],

41+ ibc_objs :: [(Target, FilePath)],

42− ibc_libs :: [String],

42+ ibc_libs :: [(Target, String)],

43 ibc_dynamic_libs :: [String],

44− ibc_hdrs :: [String],

44+ ibc_hdrs :: [(Target, String)],

45 ibc_access :: [(Name, Accessibility)],

46 ibc_total :: [(Name, Totality)],

47 ibc_flags :: [(Name, [FnOpt])],

@@ -112,10 +112,10 @@ ibc i (IBCOpt n) f = case lookupCtxt n (idris_optimisation i) of

112ibc i (IBCSyntax n) f = return f { ibc_syntax = n : ibc_syntax f }

113ibc i (IBCKeyword n) f = return f { ibc_keywords = n : ibc_keywords f }

114ibc i (IBCImport n) f = return f { ibc_imports = n : ibc_imports f }

115−ibc i (IBCObj n) f = return f { ibc_objs = n : ibc_objs f }

115+ibc i (IBCObj tgt n) f = return f { ibc_objs = (tgt, n) : ibc_objs f }

116−ibc i (IBCLib n) f = return f { ibc_libs = n : ibc_libs f }

116+ibc i (IBCLib tgt n) f = return f { ibc_libs = (tgt, n) : ibc_libs f }

117ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

118−ibc i (IBCHeader n) f = return f { ibc_hdrs = n : ibc_hdrs f }

118+ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }

119ibc i (IBCDef n) f = case lookupDef n (tt_ctxt i) of

120 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

121 _ -> fail "IBC write failed"

@@ -242,11 +242,11 @@ pKeywords :: [String] -> Idris ()

242pKeywords k = do i <- getIState

243 putIState (i { syntax_keywords = k ++ syntax_keywords i })

244

245−pObjs :: [FilePath] -> Idris ()

245+pObjs :: [(Target, FilePath)] -> Idris ()

246−pObjs os = mapM_ addObjectFile os

246+pObjs os = mapM_ (uncurry addObjectFile) os

247

248−pLibs :: [String] -> Idris ()

248+pLibs :: [(Target, String)] -> Idris ()

249−pLibs ls = mapM_ addLib ls

249+pLibs ls = mapM_ (uncurry addLib) ls

250

251pDyLibs :: [String] -> Idris ()

252pDyLibs ls = do res <- mapM (addDyLib . return) ls

@@ -255,8 +255,8 @@ pDyLibs ls = do res <- mapM (addDyLib . return) ls

255 where checkLoad (Left _) = return ()

256 checkLoad (Right err) = fail err

257

258−pHdrs :: [String] -> Idris ()

258+pHdrs :: [(Target, String)] -> Idris ()

259−pHdrs hs = mapM_ addHdr hs

259+pHdrs hs = mapM_ (uncurry addHdr) hs

260

261pDefs :: [(Name, Def)] -> Idris ()

262pDefs ds = mapM_ (\ (n, d) ->

@@ -1676,3 +1676,22 @@ instance Binary SSymbol where

1676 4 -> do x1 <- get

1677 return (Binding x1)

1678 _ -> error "Corrupted binary data for SSymbol"

1679+

1680+instance Binary Target where

1681+ put x

1682+ = case x of

1683+ ViaC -> putWord8 0

1684+ ViaJava -> putWord8 1

1685+ ViaNode -> putWord8 2

1686+ ViaJavaScript -> putWord8 3

1687+ Bytecode -> putWord8 4

1688+ get

1689+ = do i <- getWord8

1690+ case i of

1691+ 0 -> return ViaC

1692+ 1 -> return ViaJava

1693+ 2 -> return ViaNode

1694+ 3 -> return ViaJavaScript

1695+ 4 -> return Bytecode

1696+ _ -> error "Corrupted binary data for Target"

1697+

src/Idris/Parser.hs+16−9

@@ -1499,18 +1499,25 @@ pWhereblock n syn

1499 closeBlock

1500 return (concat ds, map (\x -> (x, decoration syn x)) dns)

1501

1502+pTarget :: IParser Target

1503+pTarget = try (do reserved "C"; return ViaC)

1504+ <|> try (do reserved "Java"; return ViaJava)

1505+ <|> try (do reserved "JavaScript"; return ViaJavaScript)

1506+ <|> try (do reserved "Node"; return ViaNode)

1507+ <|> try (do reserved "Bytecode"; return Bytecode)

1508+

1502pDirective :: SyntaxInfo -> IParser [PDecl]

1509pDirective :: SyntaxInfo -> IParser [PDecl]

1503−pDirective syn = try (do lchar '%'; reserved "lib"; lib <- strlit;

1510+pDirective syn = try (do lchar '%'; reserved "lib"; tgt <- pTarget; lib <- strlit;

1504− return [PDirective (do addLib lib

1511+ return [PDirective (do addLib tgt lib

1505− addIBC (IBCLib lib))])

1512+ addIBC (IBCLib tgt lib))])

1506− <|> try (do lchar '%'; reserved "link"; obj <- strlit;

1513+ <|> try (do lchar '%'; reserved "link"; tgt <- pTarget; obj <- strlit;

1507 return [PDirective (do datadir <- liftIO getDataDir

1514 return [PDirective (do datadir <- liftIO getDataDir

1508 o <- liftIO $ findInPath [".", datadir] obj

1515 o <- liftIO $ findInPath [".", datadir] obj

1509− addIBC (IBCObj o)

1516+ addIBC (IBCObj tgt o)

1510− addObjectFile o)])

1517+ addObjectFile tgt o)])

1511− <|> try (do lchar '%'; reserved "include"; hdr <- strlit;

1518+ <|> try (do lchar '%'; reserved "include"; tgt <- pTarget; hdr <- strlit;

1512− return [PDirective (do addHdr hdr

1519+ return [PDirective (do addHdr tgt hdr

1513− addIBC (IBCHeader hdr))])

1520+ addIBC (IBCHeader tgt hdr))])

1514 <|> try (do lchar '%'; reserved "hide"; n <- iName []

1521 <|> try (do lchar '%'; reserved "hide"; n <- iName []

1515 return [PDirective (do setAccessibility n Hidden

1522 return [PDirective (do setAccessibility n Hidden

1516 addIBC (IBCAccess n Hidden))])

1523 addIBC (IBCAccess n Hidden))])

tutorial/miscellany.tex+5−4

@@ -224,10 +224,11 @@ Often this will require extra libraries to be linked in, or extra header and obj

224This is made possible through the following directives:

225

226\begin{itemize}

227−\item \texttt{\%lib "x"} --- include the \texttt{libx} library, equivalent to passing the

227+\item \texttt{\%lib target "x"} --- include the \texttt{libx} library. If the target is \texttt{C} this is equivalent to passing the

228−\texttt{-lx} option to \texttt{gcc}.

228+\texttt{-lx} option to \texttt{gcc}. If the target is Java the library will be interpreted as a

229+"groupId:artifactId:packaging:version" dependency coordinate for maven.

229−\item \texttt{\%include "x.h"} --- use the header file \texttt{x.h}.

230+\item \texttt{\%include target "x"} --- use the header file or import \texttt{x} for the given back end target.

230−\item \texttt{\%link "x.o"} --- link with the object file \texttt{x.o}.

231+\item \texttt{\%link target "x.o"} --- link with the object file \texttt{x.o} when using the given back end target.

231\item \texttt{\%dynamic "x.so"} --- dynamically link the interpreter with the shared object \texttt{x.so}.

232\item \texttt{\%dynamic "x.so"} --- dynamically link the interpreter with the shared object \texttt{x.so}.

232\end{itemize}

233\end{itemize}

233

234