| test : List String -> String | |
| test xs = ?something |
| %dynamic "./../target/x86_64-apple-darwin/lib/libidrisfs-ba8d5852-0.0.dylib" | |
| getSizeInt : IO Int | |
| getSizeInt = mkForeign (FFun "sizeof_int" [] FInt) | |
| WARNING: Cannot load './../target/x86_64-apple-darwin/lib/libidrisfs-ba8d5852-0.0.dylib' at compile time because Idris was compiled without libffi support. |
Trying to link to FFI .dylib on OSX
Getting the warning:
WARNING: Cannot load './../target/x86_64-apple-darwin/lib/libidrisfs-ba8d5852-0.0.dylib' at compile time because Idris was compiled without libffi support.
Followed instructions at https://github.com/idris-lang/Idris-dev/wiki/Idris-on-OS-X-using-Homebrew
| Resolving dependencies... | |
| Configuring cabal-install-1.18.0.3... | |
| /var/folders/_t/g72k9vzd30b5svvyd1nxpwp40000gn/T/56759.c:1:12: | |
| warning: control reaches end of non-void function [-Wreturn-type] | |
| int foo() {} | |
| ^ | |
| 1 warning generated. | |
| Building cabal-install-1.18.0.3... | |
| Preprocessing executable 'cabal' for cabal-install-1.18.0.3... |
| Resolving dependencies... | |
| Configuring cabal-install-1.18.0.3... | |
| /var/folders/_t/g72k9vzd30b5svvyd1nxpwp40000gn/T/57145.c:1:12: | |
| warning: control reaches end of non-void function [-Wreturn-type] | |
| int foo() {} | |
| ^ | |
| 1 warning generated. | |
| Building cabal-install-1.18.0.3... | |
| Preprocessing executable 'cabal' for cabal-install-1.18.0.3... |
| module Main | |
| -- %dynamic "./../target/x86_64-apple-darwin/lib/libidrisfs-ba8d5852-0.0.dylib" | |
| %include C "idrisfs.h" | |
| %link C "idrisfs.o" | |
| getSizeInt : IO Int | |
| getSizeInt = mkForeign (FFun "sizeof_int" [] FInt) |
| -- describes an Integer representation of Bools | |
| -- that also specify how many bits are used | |
| data BitVector : Integer -> Integer -> Type | |
| -- I want to make sure that the value of the integer | |
| -- is always less than 2^first_argument. | |
| -- Is this possible? | |
| -- takes two Bool and return an Integer. | |
| pairOfBoolsToInteger : Bool -> Bool -> BitVector 2 Integer |
| Main.idr:3:18:When elaborating right hand side of numTuple: | |
| When elaborating an application of constructor __MkPair: | |
| Can't unify | |
| Type | |
| with | |
| b | |
| Specifically: |
| ./Main.idr:2:27: error: not a | |
| terminator, expected: "$", "$>", | |
| "&&", "*", "+", "++", "-", "->", | |
| ".", "/", "/=", "::", ";", "<", | |
| "<$", "<$>", "<*>", "<+>", | |
| "<->", "<<", "<=", "<|>", "==", | |
| ">", ">=", ">>", ">>=", "`", | |
| "||", | |
| ambiguous use of a left-associative operator, | |
| ambiguous use of a non-associative operator, |
| NumPair : Type -> Type -> Type | |
| NumPair a b = (Num a, Num b) | |
| numTriple : (NumPair a b, Num c) => a -> b -> c -> (a, b, c) | |
| numTriple x y z = (x, y, z) |