6a33c4d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #289 from david-christiansen/multiple-dyn-libs

Enable alternate names for shared libraries

commit6a33c4db2d9c2e0ee2f636bf73eb5cdd7bf82e44 authorEdwin Brady <edwin.brady@gmail.com> dateWed 24 Apr 2013, 06:12 (14 years ago) parent6db701e 7b8ce28

4 files changed+23−13

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+10−8 src/Idris/IBC.hs+5−1 src/Idris/Parser.hs+7−3 test/test022/test022.idr+1−1

src/Idris/AbsSyntax.hs+10−8

@@ -24,7 +24,7 @@ import Data.Either

2424import Debug.Trace

2525

2626import Util.Pretty

27−

27+import Util.System

2828

2929getContext :: Idris Context

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

@@ -41,13 +41,15 @@ getLibs = do i <- getIState; return (idris_libs i)

4141addLib :: String -> Idris ()

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

4343

44−addDyLib :: String -> Idris ()

45−addDyLib lib = do i <- getIState

46− handle <- lift $ tryLoadLib lib

47− case handle of

48− Nothing -> fail $ "Could not load dynamic lib \"" ++ lib ++ "\""

49− Just x -> do let libs = idris_dynamic_libs i

50− putIState $ i { idris_dynamic_libs = x:libs }

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

45+addDyLib libs = do i <- getIState

46+ handle <- lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) libs

47+ case msum handle of

48+ Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++

49+ concat (intersperse "," libs) ++ "\"")

50+ Just x -> do let ls = idris_dynamic_libs i

51+ putIState $ i { idris_dynamic_libs = x:ls }

52+ return (Left x)

5153

5254addHdr :: String -> Idris ()

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

src/Idris/IBC.hs+5−1

@@ -249,7 +249,11 @@ pLibs :: [String] -> Idris ()

249249pLibs ls = mapM_ addLib ls

250250

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

252−pDyLibs ls = mapM_ addDyLib ls

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

253+ mapM_ checkLoad res

254+ return ()

255+ where checkLoad (Left _) = return ()

256+ checkLoad (Right err) = fail err

253257

254258pHdrs :: [String] -> Idris ()

255259pHdrs hs = mapM_ addHdr hs

src/Idris/Parser.hs+7−3

@@ -30,6 +30,7 @@ import qualified Text.Parsec.Token as PTok

3030import Data.List

3131import Data.List.Split(splitOn)

3232import Control.Monad.State

33+import Control.Monad.Error

3334import Debug.Trace

3435import Data.Maybe

3536import System.FilePath

@@ -1512,9 +1513,12 @@ pDirective syn = try (do lchar '%'; reserved "lib"; lib <- strlit;

15121513 putIState (i { default_total = tot }))])

15131514 <|> try (do lchar '%'; reserved "logging"; i <- natural;

15141515 return [PDirective (setLogLevel (fromInteger i))])

1515− <|> try (do lchar '%'; reserved "dynamic"; lib <- strlit;

1516− return [PDirective (do addIBC (IBCDyLib lib)

1517− addDyLib lib)])

1516+ <|> try (do lchar '%'; reserved "dynamic"; libs <- sepBy1 strlit (lchar ',');

1517+ return [PDirective (do added <- addDyLib libs

1518+ case added of

1519+ Left lib -> addIBC (IBCDyLib (lib_name lib))

1520+ Right msg ->

1521+ fail $ msg)])

15181522 <|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders";

15191523 return [PDirective (addLangExt TypeProviders)])

15201524

test/test022/test022.idr+1−1

@@ -1,6 +1,6 @@

11module Main

3−%dynamic "libm"

3+%dynamic "dummy", "libm", "msvcrt"

55x : Float

66x = unsafePerformIO (mkForeign (FFun "sin" [FFloat] FFloat) 1.6)