7b8ce28 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+10−8

compare with master

unifiedsplit

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

24import Debug.Trace

25

26import Util.Pretty

27−

27+import Util.System

28

29getContext :: Idris Context

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

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

41addLib :: String -> Idris ()

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

43

44−addDyLib :: String -> Idris ()

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

45−addDyLib lib = do i <- getIState

45+addDyLib libs = do i <- getIState

46− handle <- lift $ tryLoadLib lib

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

47− case handle of

47+ case msum handle of

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

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

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

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

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

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

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

52+ return (Left x)

51

53

52addHdr :: String -> Idris ()

54addHdr :: String -> Idris ()

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

55addHdr 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 ()

249pLibs ls = mapM_ addLib ls

250

251pDyLibs :: [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

253

257

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

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

255pHdrs hs = mapM_ addHdr hs

259pHdrs hs = mapM_ addHdr hs

src/Idris/Parser.hs+7−3

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

30import Data.List

31import Data.List.Split(splitOn)

32import Control.Monad.State

33+import Control.Monad.Error

33import Debug.Trace

34import Debug.Trace

34import Data.Maybe

35import Data.Maybe

35import System.FilePath

36import System.FilePath

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

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

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

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

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

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

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

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

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

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

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

1517− addDyLib lib)])

1518+ case added of

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

1520+ Right msg ->

1521+ fail $ msg)])

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

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

1519 return [PDirective (addLangExt TypeProviders)])

1523 return [PDirective (addLangExt TypeProviders)])

1520

1524

test/test022/test022.idr+1−1

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

1module Main

2

3−%dynamic "libm"

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

4

5x : Float

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