on master help sign in
Top-level directive for dynamic linking

Now the syntax: %dynamic "libfoo.so" causes libfoo to be dynamically linked.

commit04267d6ea7f5878b39c0eb3f53da3490a5a58534 authorDavid Christiansen <david@davidchristiansen.dk> dateFri 15 Mar 2013, 11:55 (14 years ago) parent3262127
1 file changed+11
src/Idris/Parser.hs+11
src/Idris/Parser.hs+11
@@ -14,6 +14,8 @@ import Idris.Unlit
1414import Idris.Providers
1515import Paths_idris
1616
17+import Util.DynamicLinker
18+
1719import Core.CoreParser
1820import Core.TT
1921import Core.Evaluate
@@ -1486,6 +1488,15 @@ pDirective syn = try (do lchar '%'; reserved "lib"; lib <- strlit;
14861488 putIState (i { default_total = tot }))])
14871489 <|> try (do lchar '%'; reserved "logging"; i <- natural;
14881490 return [PDirective (setLogLevel (fromInteger i))])
1491+ <|> try (do lchar '%'; reserved "dynamic"; lib <- strlit;
1492+ return [PDirective (do i <- getIState
1493+ handle <- lift $ tryLoadLib lib
1494+ case handle of
1495+ Nothing ->
1496+ fail $ "Could not load dynamic lib \"" ++ lib ++ "\""
1497+ Just x ->
1498+ do let libs = idris_dynamic_libs i
1499+ putIState $ i { idris_dynamic_libs = x:libs })])
14891500
14901501pProvider :: SyntaxInfo -> IParser [PDecl]
14911502pProvider syn = do lchar '%'; reserved "provide";