Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions CHANGELOG_NEXT.md
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,11 @@ should target this file (`CHANGELOG_NEXT`).
* Prefix RefC Idris values with `Idris2_` to prevent name collisions with third
partly libraries.

#### Chez Backend

* Added support for FFI C unions. Added `Union`, `getUnionField` and
`setUnionField` in `System.FFI`.

### Library changes

#### Base
Expand Down
5 changes: 5 additions & 0 deletions docs/source/backends/backend-cookbook.rst
Original file line number Diff line number Diff line change
Expand Up @@ -613,6 +613,11 @@ The foreign types are:
It represents a C like structure in the custom back-end.
``prim__getField`` and ``prim__setField`` primitives should be implemented
to support this CFType.
- ``CFUnion`` of type ``String -> List (String, CFType) -> CFType`` is the
foreign type associated with the ``System.FFI.Union``.
It represents a C like union in the custom back-end.
``prim__getUnionField`` and ``prim__setUnionField`` primitives should be implemented
to support this CFType.
- ``CFUser`` of type ``Name -> List CFType -> CFType``
Types defined with [external] are represented with ``CFUser``. For example
``data MyType : Type where [external]`` will be represented as
Expand Down
13 changes: 12 additions & 1 deletion docs/source/ffi/ffi.rst
Original file line number Diff line number Diff line change
Expand Up @@ -282,7 +282,7 @@ form:
For an example, see the sample :ref:`sect-readline` bindings.

Additionally, foreign functions can take *callbacks*, and take and return
C ``struct`` pointers.
C ``struct`` and ```union``` pointers.

.. _sect-callbacks:

Expand Down Expand Up @@ -508,6 +508,17 @@ can convert between a ``void*`` and a ``char*`` in C:
%foreign (pfn "getString")
getString : Ptr String -> String

Unions
-------

To work with unions is almost the same as with structs above with two differences:

* To define a type for accessing a union in Idris, use ```Union``` type from ```System.FFI```
* In place of ```getField``` and ```setField``` use ```getUnionField``` and ```setUnionField``` to get and set its fields respectively

You must ensure that you are accessing the right union case yourself by e.g. means of a tagged union.

Note that only Chez backend currently supports unions.

Finalisers
----------
Expand Down
35 changes: 35 additions & 0 deletions libs/base/System/FFI.idr
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,13 @@ data Struct : String -> -- C struct name
List (String, Type) -> -- field names and types
Type where

||| A union with a name and a list of key-value pairs of field names and their
||| types.
export
data Union : String -> -- C union name
List (String, Type) -> -- field names and types
Type where

||| A proof that the field exists as an entry in the list of field names and
||| their types.
public export
Expand All @@ -29,6 +36,15 @@ prim__setField : {s : _} -> forall fs, ty .
Struct s fs -> (n : String) ->
FieldType n ty fs -> ty -> PrimIO ()

%extern
prim__getUnionField : {s : _} -> forall fs, ty .
Union s fs -> (n : String) ->
FieldType n ty fs -> ty
%extern
prim__setUnionField : {s : _} -> forall fs, ty .
Union s fs -> (n : String) ->
FieldType n ty fs -> ty -> PrimIO ()

||| Retrieve the value of the specified field in the given `Struct`.
|||
||| @ s the `Struct` to retrieve the value from
Expand All @@ -48,6 +64,25 @@ setField : {sn : _} -> (s : Struct sn fs) -> (n : String) ->
{auto fieldok : FieldType n ty fs} -> (val : ty) -> IO ()
setField s n val = primIO (prim__setField s n fieldok val)

||| Retrieve the value of the specified field in the given `Union`.
|||
||| @ u the `Union` to retrieve the value from
||| @ n the name of the field in the `Union`.
public export %inline
getUnionField : {sn : _} -> (u : Union sn fs) -> (n : String) ->
{auto fieldok : FieldType n ty fs} -> ty
getUnionField u n = prim__getUnionField u n fieldok

||| Set the value of the specified field in the given `Union`.
|||
||| @ u the `Union` in which the field exists
||| @ n the name of the field to set
||| @ val the value to set the field to
public export %inline
setUnionField : {sn : _} -> (u : Union sn fs) -> (n : String) ->
{auto fieldok : FieldType n ty fs} -> (val : ty) -> IO ()
setUnionField u n val = primIO (prim__setUnionField u n fieldok val)

%foreign "C:idris2_malloc, libidris2_support, idris_memory.h"
prim__malloc : (size : Int) -> PrimIO AnyPtr

Expand Down
12 changes: 12 additions & 0 deletions src/Compiler/CompileExpr.idr
Original file line number Diff line number Diff line change
Expand Up @@ -380,6 +380,7 @@ getVars (S rest) = first :: map weakenVar (getVars rest)
data NArgs : Type where
User : Name -> List ClosedClosure -> NArgs
Struct : String -> List (String, ClosedClosure) -> NArgs
Union : String -> List (String, ClosedClosure) -> NArgs
NUnit : NArgs
NPtr : NArgs
NGCPtr : NArgs
Expand Down Expand Up @@ -427,6 +428,10 @@ getNArgs defs (NS _ (UN $ Basic "Struct")) [n, args]
= do NPrimVal _ (Str n') <- evalClosure defs n
| nf => throw (GenericMsg (getLoc nf) "Unknown name for struct")
pure (Struct n' !(getFieldArgs defs args))
getNArgs defs (NS _ (UN $ Basic "Union")) [n, args]
= do NPrimVal _ (Str n') <- evalClosure defs n
| nf => throw (GenericMsg (getLoc nf) "Unknown name for union")
pure (Union n' !(getFieldArgs defs args))
getNArgs defs n args = pure $ User n args

-- The order of the arguments have a big effect on case-tree size
Expand Down Expand Up @@ -471,6 +476,13 @@ nfToCFType _ (NTCon fc n_in _ args) s
tycf <- nfToCFType fc tynf False
pure (n, tycf)) fs
pure (CFStruct n fs')
Union n fs =>
do fs' <- traverse
(\ (n, ty) =>
do tynf <- evalClosure defs ty
tycf <- nfToCFType fc tynf False
pure (n, tycf)) fs
pure (CFUnion n fs')
NUnit => pure CFUnit
NPtr => pure CFPtr
NGCPtr => pure CFGCPtr
Expand Down
6 changes: 5 additions & 1 deletion src/Compiler/RefC/RefC.idr
Original file line number Diff line number Diff line change
Expand Up @@ -555,7 +555,8 @@ mutual
let prims : List String =
["prim__newIORef", "prim__readIORef", "prim__writeIORef", "prim__newArray",
"prim__arrayGet", "prim__arraySet", "prim__getField", "prim__setField",
"prim__os", "prim__codegen", "prim__onCollect", "prim__onCollectAny" ]
"prim__getUnionField", "prim__setUnionField", "prim__os", "prim__codegen",
"prim__onCollect", "prim__onCollectAny" ]
case p of
NS _ (UN (Basic pn)) =>
unless (elem pn prims) $ throw $ InternalError $ "[refc] Unknown primitive: " ++ cName p
Expand Down Expand Up @@ -708,6 +709,7 @@ cTypeOfCFType CFWorld = "void *"
cTypeOfCFType (CFFun x y) = "void *"
cTypeOfCFType (CFIORes x) = "void *"
cTypeOfCFType (CFStruct x ys) = "void *"
cTypeOfCFType (CFUnion x ys) = "void *"
cTypeOfCFType (CFUser x ys) = "void *"
cTypeOfCFType n = assert_total $ idris_crash ("INTERNAL ERROR: Unknown FFI type in C backend: " ++ show n)

Expand Down Expand Up @@ -761,6 +763,7 @@ extractValue _ CFWorld _ = "(Idris2_Value *)NULL"
extractValue _ (CFFun x y) varName = "(Idris2_Closure*)" ++ varName
extractValue c (CFIORes x) varName = extractValue c x varName
extractValue _ (CFStruct x xs) varName = assert_total $ idris_crash ("INTERNAL ERROR: Struct access not implemented: " ++ varName)
extractValue _ (CFUnion x xs) varName = assert_total $ idris_crash ("INTERNAL ERROR: Union access not implemented: " ++ varName)
-- not really total but this way this internal error does not contaminate everything else
extractValue _ (CFUser x xs) varName = "(Idris2_Value*)" ++ varName
extractValue _ n _ = assert_total $ idris_crash ("INTERNAL ERROR: Unknown FFI type in C backend: " ++ show n)
Expand All @@ -786,6 +789,7 @@ packCFType CFWorld _ = "(Idris2_Value *)NULL"
packCFType (CFFun x y) varName = "makeFunction(" ++ varName ++ ")"
packCFType (CFIORes x) varName = packCFType x varName
packCFType (CFStruct x xs) varName = "makeStruct(" ++ varName ++ ")"
packCFType (CFUnion x xs) varName = "makeUnion(" ++ varName ++ ")"
packCFType (CFUser x xs) varName = varName
packCFType n _ = assert_total $ idris_crash ("INTERNAL ERROR: Unknown FFI type in C backend: " ++ show n)

Expand Down
14 changes: 13 additions & 1 deletion src/Compiler/Scheme/Chez.idr
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,7 @@ chezExtPrim cs schLazy i prim args
export
data Loaded : Type where

-- Label for noting which struct types are declared
-- Label for noting which struct and union types are declared
export
data Structs : Type where

Expand All @@ -194,6 +194,7 @@ cftySpec fc CFBuffer = pure "u8*"
cftySpec fc (CFFun s t) = pure "void*"
cftySpec fc (CFIORes t) = cftySpec fc t
cftySpec fc (CFStruct n t) = pure $ "(* " ++ fromString n ++ ")"
cftySpec fc (CFUnion n t) = pure $ "(* " ++ fromString n ++ ")"
cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++
" to foreign function"))

Expand Down Expand Up @@ -354,6 +355,17 @@ mkStruct (CFStruct n flds)
where
showFld : (String, CFType) -> Core Builder
showFld (n, ty) = pure $ "[" ++ fromString n ++ " " ++ !(cftySpec emptyFC ty) ++ "]"
mkStruct (CFUnion n flds)
= do defs <- traverse mkStruct (map snd flds)
strs <- get Structs
if n `elem` strs
then pure (concat defs)
else do put Structs (n :: strs)
pure $ concat defs ++ "(define-ftype " ++ fromString n ++ " (union\n\t"
++ sepBy "\n\t" !(traverse showFld flds) ++ "))\n"
where
showFld : (String, CFType) -> Core Builder
showFld (n, ty) = pure $ "[" ++ fromString n ++ " " ++ !(cftySpec emptyFC ty) ++ "]"
mkStruct (CFIORes t) = mkStruct t
mkStruct (CFFun a b) = do [| mkStruct a ++ mkStruct b |]
mkStruct _ = pure ""
Expand Down
2 changes: 2 additions & 0 deletions src/Compiler/Scheme/Common.idr
Original file line number Diff line number Diff line change
Expand Up @@ -233,6 +233,8 @@ toPrim pn@(NS _ n)
(n == UN (Basic "prim__arraySet"), ArraySet),
(n == UN (Basic "prim__getField"), GetField),
(n == UN (Basic "prim__setField"), SetField),
(n == UN (Basic "prim__getUnionField"), GetField),
(n == UN (Basic "prim__setUnionField"), SetField),
(n == UN (Basic "prim__os"), SysOS),
(n == UN (Basic "prim__codegen"), SysCodegen),
(n == UN (Basic "prim__onCollect"), OnCollect),
Expand Down
7 changes: 6 additions & 1 deletion src/Compiler/Scheme/Gambit.idr
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ gambitPrim cs schLazy i prim args
-- Reference label for keeping track of loaded external libraries
data Loaded : Type where

-- Label for noting which struct types are declared
-- Label for noting which struct and union types are declared
data Structs : Type where

notWorld : CFType -> Bool
Expand All @@ -116,6 +116,7 @@ cType fc CFChar = pure "char"
cType fc CFPtr = pure "void *"
cType fc (CFIORes t) = cType fc t
cType fc (CFStruct n t) = pure $ "struct " ++ fromString n
cType fc (CFUnion n t) = pure $ "union " ++ fromString n
cType fc (CFFun s t) = funTySpec [s] t
where
funTySpec : List CFType -> CFType -> Core Builder
Expand Down Expand Up @@ -145,6 +146,7 @@ cftySpec fc CFChar = pure "char"
cftySpec fc CFPtr = pure "(pointer void)"
cftySpec fc (CFIORes t) = cftySpec fc t
cftySpec fc (CFStruct n t) = pure $ fromString n ++ "*/nonnull"
cftySpec fc (CFUnion n t) = throw (GenericMsg fc "Union types are not yet supported")
cftySpec fc (CFFun s t) = funTySpec [s] t
where
funTySpec : List CFType -> CFType -> Core Builder
Expand Down Expand Up @@ -320,6 +322,9 @@ mkStruct (CFStruct n flds)
where
showFld : (String, CFType) -> Core Builder
showFld (n, ty) = pure $ "(" ++ fromString n ++ " " ++ !(cftySpec emptyFC ty) ++ ")"
mkStruct (CFUnion n flds)
-- TODO: add Union support
= pure ""
mkStruct (CFIORes t) = mkStruct t
mkStruct (CFFun a b) = [| mkStruct a ++ mkStruct b |]
mkStruct _ = pure ""
Expand Down
4 changes: 4 additions & 0 deletions src/Compiler/Scheme/Racket.idr
Original file line number Diff line number Diff line change
Expand Up @@ -135,6 +135,7 @@ cftySpec fc CFGCPtr = pure "_pointer"
cftySpec fc CFBuffer = pure "_bytes"
cftySpec fc (CFIORes t) = cftySpec fc t
cftySpec fc (CFStruct n t) = pure $ "_" ++ fromString n ++ "-pointer"
cftySpec fc (CFUnion n t) = throw (GenericMsg fc "Union types are not yet supported")
cftySpec fc (CFFun s t) = funTySpec [s] t
where
funTySpec : List CFType -> CFType -> Core Builder
Expand Down Expand Up @@ -301,6 +302,9 @@ mkStruct (CFStruct n flds)
where
showFld : (String, CFType) -> Core Builder
showFld (n, ty) = pure $ "[" ++ fromString n ++ " " ++ !(cftySpec emptyFC ty) ++ "]"
mkStruct (CFUnion n flds)
-- TODO: add Union support
= pure ""
mkStruct (CFIORes t) = mkStruct t
mkStruct (CFFun a b) = [| mkStruct a ++ mkStruct b |]
mkStruct _ = pure ""
Expand Down
2 changes: 2 additions & 0 deletions src/Core/CompileExpr.idr
Original file line number Diff line number Diff line change
Expand Up @@ -197,6 +197,7 @@ data CFType : Type where
CFFun : CFType -> CFType -> CFType
CFIORes : CFType -> CFType
CFStruct : String -> List (String, CFType) -> CFType
CFUnion : String -> List (String, CFType) -> CFType
CFUser : Name -> List CFType -> CFType

public export
Expand Down Expand Up @@ -398,6 +399,7 @@ Show CFType where
show (CFFun s t) = show s ++ " -> " ++ show t
show (CFIORes t) = "IORes " ++ show t
show (CFStruct n args) = "struct " ++ show n ++ " " ++ showSep " " (map show args)
show (CFUnion n args) = "union " ++ show n ++ " " ++ showSep " " (map show args)
show (CFUser n args) = show n ++ " " ++ showSep " " (map show args)

export
Expand Down
2 changes: 2 additions & 0 deletions src/Core/Hash.idr
Original file line number Diff line number Diff line change
Expand Up @@ -273,6 +273,8 @@ Hashable CFType where
h `hashWithSalt` 21
CFInteger =>
h `hashWithSalt` 22
CFUnion n fs =>
h `hashWithSalt` 23 `hashWithSalt` n `hashWithSalt` fs

export
Hashable PrimType where
Expand Down
2 changes: 2 additions & 0 deletions src/Core/TTC.idr
Original file line number Diff line number Diff line change
Expand Up @@ -847,6 +847,7 @@ TTC CFType where
toBuf CFInt64 = tag 20
toBuf CFForeignObj = tag 21
toBuf CFInteger = tag 22
toBuf (CFUnion n a) = do tag 23; toBuf n; toBuf a

fromBuf
= case !getTag of
Expand All @@ -873,6 +874,7 @@ TTC CFType where
20 => pure CFInt64
21 => pure CFForeignObj
22 => pure CFInteger
23 => do n <- fromBuf; a <- fromBuf; pure (CFUnion n a)
_ => corrupt "CFType"

export
Expand Down
7 changes: 7 additions & 0 deletions tests/chez/chez039/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
*.d
*.o
*.obj
*.so
*.dylib
*.dll
*.a
31 changes: 31 additions & 0 deletions tests/chez/chez039/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
include ../../../config.mk

TARGET = libunion

SRCS = $(wildcard *.c)
OBJS = $(SRCS:.c=.o)
DEPS = $(OBJS:.o=.d)


all: $(TARGET)$(SHLIB_SUFFIX)

$(TARGET)$(SHLIB_SUFFIX): $(OBJS)
$(CC) -shared $(LDFLAGS) -o $@ $^

$(TARGET).a: $(OBJS)
ar rcs $@ $(OBJS)


-include $(DEPS)

%.d: %.c
@$(CPP) $(CFLAGS) $< -MM -MT $(@:.d=.o) >$@


.PHONY: clean

clean :
$(RM) $(OBJS) $(TARGET)$(SHLIB_SUFFIX)

cleandep: clean
$(RM) $(DEPS)
42 changes: 42 additions & 0 deletions tests/chez/chez039/Union.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
import System.FFI

pfn : String -> String
pfn fn = "C:" ++ fn ++ ",libunion"

IntOrDouble : Type
IntOrDouble = Union "intOrDouble" [("x", Int), ("y", Double)]

%foreign (pfn "mkInt")
mkInt : Int -> IntOrDouble

%foreign (pfn "mkDouble")
mkDouble : Double -> IntOrDouble

%foreign (pfn "freeIntOrDouble")
freeIntOrDouble : IntOrDouble -> PrimIO ()

showInt : IntOrDouble -> String
showInt u =
let x : Int = getUnionField u "x"
in show x

showDouble : IntOrDouble -> String
showDouble u =
let y : Double = getUnionField u "y"
in show y

main : IO ()
main = do
let
u1 = mkInt 20
u2 = mkInt 20
u3 = mkDouble 2.1
setUnionField u1 "x" (the Int 40)
setUnionField u2 "y" (the Double 3.14)
putStrLn $ showInt u1
putStrLn $ showDouble u2
putStrLn $ showDouble u3

primIO $ freeIntOrDouble u1
primIO $ freeIntOrDouble u2
primIO $ freeIntOrDouble u3
3 changes: 3 additions & 0 deletions tests/chez/chez039/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
40
3.14
2.1
Loading
Loading