Commits

Anonymous committed 150400c

LibFFI bindinings stub

  • Participants
  • Parent commits 34bad40

Comments (0)

Files changed (1)

+module LibFFI where
+{-# IMPORT Foreign.Ptr #-}
+{-# IMPORT Foreign.C #-}
+{-# IMPORT Foreign.LibFFI #-}
+
+postulate
+  RetType FunPtr : Set → Set
+  Arg CDouble : Set 
+{-# BUILTIN FLOAT CDouble #-}
+{-# COMPILED_TYPE FunPtr Foreign.Ptr.FunPtr #-}
+{-# COMPILED_TYPE RetType Foreign.LibFFI.RetType #-}
+{-# COMPILED_TYPE Arg  Foreign.LibFFI.Arg #-}
+{-# COMPILED_TYPE CDouble Foreign.C.CDouble #-}
+
+open import IO.Primitive
+open import Data.Colist
+postulate 
+  callFFI : {A B : Set} → FunPtr A  → RetType B → Colist Arg → IO B
+  retCDouble : RetType CDouble
+  argCDouble : CDouble → Arg
+{-# COMPILED callFFI (\ _ _ -> Foreign.LibFFI.callFFI) #-}
+{-# COMPILED retCDouble Foreign.LibFFI.retCDouble #-}
+{-# COMPILED argCDouble Foreign.LibFFI.argCDouble #-}