Experimenting with a new FFI

Functions can be declared as %foreign with a list of calling
conventions, which a backend will work through until it finds one it can
understand. Currently implemented only in Chez backend. If this works
out, I'll implement it for Racket too, and remove the old primitive
functions.

There's a bit more boiler plate here than before, but it has the benefit
of being more extensible and portable between different back ends.

Some examples, pending proper documentation:

%foreign "C:puts,libc" "scheme:display"
putline : String -> PrimIO ()

%foreign "C:exp, libm.so.6, math.h"
fexp : Double -> Double

%foreign "C:initscr, ncurses_glue.so, ncurses.h"
prim_initscr : PrimIO ()

libs/prelude/PrimIO.idr

@@ -21,6 +21,10 @@ io_bind (MkIO fn)
                             MkIO res = k x' in
                             res w')
 
+public export
+PrimIO : Type -> Type
+PrimIO a = (1 x : %World) -> IORes a
+
 %extern prim__putStr : String -> (1 x : %World) -> IORes ()
 %extern prim__getStr : (1 x : %World) -> IORes String
 

src/Compiler/Common.idr

@@ -120,3 +120,27 @@ tmpName = foreign FFI_C "tmpnam" (Ptr -> IO String) null
 export
 chmod : String -> Int -> IO ()
 chmod f m = foreign FFI_C "chmod" (String -> Int -> IO ()) f m
+
+-- Parse a calling convention into a backend/target for the call, and
+-- a comma separated list of any other location data.
+-- e.g. "scheme:display" - call the scheme function 'display'
+--      "C:puts,libc,stdio.h" - call the C function 'puts' which is in
+--      the library libc and the header stdio.h
+-- Returns Nothing if the string is empty (which a backend can interpret
+-- however it likes)
+export
+parseCC : String -> Maybe (String, List String)
+parseCC "" = Nothing
+parseCC str
+    = case span (/= ':') str of
+           (target, "") => Just (trim target, [])
+           (target, opts) => Just (trim target, 
+                                   map trim (getOpts 
+                                       (assert_total (strTail opts))))
+  where
+    getOpts : String -> List String
+    getOpts "" = []
+    getOpts str
+        = case span (/= ',') str of
+               (opt, "") => [opt]
+               (opt, rest) => opt :: getOpts (assert_total (strTail rest))

src/Compiler/CompileExpr.idr

@@ -5,7 +5,9 @@ import public Core.CompileExpr
 import Core.Context
 import Core.Env
 import Core.Name
+import Core.Normalise
 import Core.TT
+import Core.Value
 
 import Data.NameMap
 import Data.Vect
@@ -27,6 +29,7 @@ numArgs defs (Ref _ _ n)
     = case !(lookupDefExact n (gamma defs)) of
            Just (PMDef _ args _ _ _) => pure (length args)
            Just (ExternDef arity) => pure arity
+           Just (ForeignDef arity _) => pure arity
            Just (Builtin {arity} f) => pure arity
            _ => pure 0
 numArgs _ tm = pure 0
@@ -55,12 +58,12 @@ expandToArity : Nat -> CExp vars -> List (CExp vars) -> CExp vars
 -- No point in applying to anything
 expandToArity _ (CErased fc) _ = CErased fc
 -- Overapplied; apply everything as single arguments
-expandToArity Z fn args = applyAll fn args
+expandToArity Z f args = applyAll f args
   where
     applyAll : CExp vars -> List (CExp vars) -> CExp vars
     applyAll fn [] = fn
     applyAll fn (a :: args) = applyAll (CApp (getFC fn) fn [a]) args
-expandToArity (S k) fn (a :: args) = expandToArity k (addArg fn a) args
+expandToArity (S k) f (a :: args) = expandToArity k (addArg f a) args
   where
     addArg : CExp vars -> CExp vars -> CExp vars
     addArg (CApp fc fn args) a = CApp fc fn (args ++ [a])
@@ -270,14 +273,56 @@ mkArgList i (S k)
     = let (_ ** rec) = mkArgList (i + 1) k in
           (_ ** ConsArg (MN "arg" i) rec)
 
+data NArgs : Type where
+     User : Name -> List (Closure []) -> NArgs
+     NUnit : NArgs
+     NIORes : Closure [] -> NArgs
+
+getNArgs : Name -> List (Closure []) -> NArgs
+getNArgs (NS _ (UN "IORes")) [arg] = NIORes arg
+getNArgs (NS _ (UN "Unit")) [] = NUnit
+getNArgs n args = User n args
+
+nfToCFType : {auto c : Ref Ctxt Defs} ->
+             NF [] -> Core CFType
+nfToCFType (NPrimVal _ IntType) = pure CFInt 
+nfToCFType (NPrimVal _ StringType) = pure CFString
+nfToCFType (NPrimVal _ DoubleType) = pure CFDouble
+nfToCFType (NPrimVal _ CharType) = pure CFChar
+nfToCFType (NPrimVal _ WorldType) = pure CFWorld 
+nfToCFType (NTCon _ n _ _ args)
+    = do defs <- get Ctxt
+         case getNArgs !(toFullNames n) args of
+              User un uargs =>
+                do nargs <- traverse (evalClosure defs) uargs
+                   cargs <- traverse nfToCFType nargs
+                   pure (CFUser n cargs)
+              NUnit => pure CFUnit
+              NIORes uarg =>
+                do narg <- evalClosure defs uarg
+                   carg <- nfToCFType narg
+                   pure (CFIORes carg)
+nfToCFType _ = pure CFUnit
+
+getCFTypes : {auto c : Ref Ctxt Defs} ->
+             List CFType -> NF [] ->
+             Core (List CFType, CFType)
+getCFTypes args (NBind fc _ (Pi _ _ ty) sc)
+    = do aty <- nfToCFType ty
+         defs <- get Ctxt
+         sc' <- sc defs (toClosure defaultOpts [] (Erased fc))
+         getCFTypes (aty :: args) sc'
+getCFTypes args t
+    = pure (reverse args, !(nfToCFType t))
+
 toCDef : {auto c : Ref Ctxt Defs} -> 
-         NameTags -> Name -> Def -> 
+         NameTags -> Name -> ClosedTerm -> Def -> 
          Core CDef
-toCDef tags n None
+toCDef tags n ty None
     = pure $ MkError $ CCrash emptyFC ("Encountered undefined name " ++ show !(getFullName n))
-toCDef tags n (PMDef _ args _ tree _)
+toCDef tags n ty (PMDef _ args _ tree _)
     = pure $ MkFun _ !(toCExpTree tags n tree)
-toCDef tags n (ExternDef arity)
+toCDef tags n ty (ExternDef arity)
     = let (ns ** args) = mkArgList 0 arity in
           pure $ MkFun _ (CExtPrim emptyFC !(getFullName n) (map toArgExp (getVars args)))
   where
@@ -287,7 +332,11 @@ toCDef tags n (ExternDef arity)
     getVars : ArgList k ns -> List (Var ns)
     getVars NoArgs = []
     getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest)
-toCDef tags n (Builtin {arity} op)
+toCDef tags n ty (ForeignDef arity cs)
+    = do defs <- get Ctxt
+         (atys, retty) <- getCFTypes [] !(nf defs [] ty)
+         pure $ MkForeign cs atys retty
+toCDef tags n ty (Builtin {arity} op)
     = let (ns ** args) = mkArgList 0 arity in
           pure $ MkFun _ (COp emptyFC op (map toArgExp (getVars args)))
   where
@@ -297,26 +346,26 @@ toCDef tags n (Builtin {arity} op)
     getVars : ArgList k ns -> Vect k (Var ns)
     getVars NoArgs = []
     getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest)
-toCDef tags n (DCon tag arity)
+toCDef tags n ty (DCon tag arity)
     = case lookup n tags of
            Just t => pure $ MkCon t arity
            _ => pure $ MkCon tag arity
-toCDef tags n (TCon tag arity _ _ _ _)
+toCDef tags n ty (TCon tag arity _ _ _ _)
     = case lookup n tags of
            Just t => pure $ MkCon t arity
            _ => pure $ MkCon tag arity
 -- We do want to be able to compile these, but also report an error at run time
 -- (and, TODO: warn at compile time)
-toCDef tags n (Hole _ _)
+toCDef tags n ty (Hole _ _)
     = pure $ MkError $ CCrash emptyFC ("Encountered unimplemented hole " ++ 
                                        show !(getFullName n))
-toCDef tags n (Guess _ _)
+toCDef tags n ty (Guess _ _)
     = pure $ MkError $ CCrash emptyFC ("Encountered constrained hole " ++ 
                                        show !(getFullName n))
-toCDef tags n (BySearch _ _ _)
+toCDef tags n ty (BySearch _ _ _)
     = pure $ MkError $ CCrash emptyFC ("Encountered incomplete proof search " ++ 
                                        show !(getFullName n))
-toCDef tags n def
+toCDef tags n ty def
     = pure $ MkError $ CCrash emptyFC ("Encountered uncompilable name " ++ 
                                        show (!(getFullName n), def))
 
@@ -333,5 +382,6 @@ compileDef tags n
     = do defs <- get Ctxt
          Just gdef <- lookupCtxtExact n (gamma defs)
               | Nothing => throw (InternalError ("Trying to compile unknown name " ++ show n))
-         ce <- toCDef tags n !(toFullNames (definition gdef))
+         ce <- toCDef tags n (type gdef)
+                             !(toFullNames (definition gdef))
          setCompiled n ce

src/Compiler/Inline.idr

@@ -58,6 +58,7 @@ unloadApp n args e = unload (drop n args) (CApp (getFC e) e (take n args))
 getArity : CDef -> Nat
 getArity (MkFun args _) = length args
 getArity (MkCon _ arity) = arity
+getArity (MkForeign _ args _) = length args
 getArity (MkError _) = 0
 
 takeFromStack : EEnv free vars -> Stack free -> (args : List Name) -> 

src/Compiler/Scheme/Chez.idr

@@ -30,6 +30,15 @@ findChez
             Nothing => do e <- firstExists [p ++ x | p <- ["/usr/bin/", "/usr/local/bin/"],
                                     x <- ["scheme", "chez", "chezscheme9.5"]]
                           maybe (pure "/usr/bin/env scheme") pure e
+    
+locate : {auto c : Ref Ctxt Defs} ->
+         String -> Core (String, String)
+locate fname
+    = do fullname <- catch (findLibraryFile fname)
+                           (\err => -- assume a system library so not
+                                    -- in our library path
+                                    pure fname)
+         pure (fname, fullname)
 
 -- Given the chez compiler directives, return a list of pairs of:
 --   - the library file name
@@ -43,14 +52,6 @@ findLibs ds
     = do let libs = mapMaybe (isLib . trim) ds
          traverse locate (nub libs)
   where
-    locate : String -> Core (String, String)
-    locate fname
-        = do fullname <- catch (findLibraryFile fname)
-                               (\err => -- assume a system library so not
-                                        -- in our library path
-                                        pure fname)
-             pure (fname, fullname)
-
     isLib : String -> Maybe String
     isLib d
         = if isPrefixOf "lib" d
@@ -119,6 +120,108 @@ mutual
   chezExtPrim i vs prim args
       = schExtCommon chezExtPrim i vs prim args
 
+-- Reference label for keeping track of loaded external libraries
+data Loaded : Type where
+
+cftySpec : FC -> CFType -> Core String
+cftySpec fc CFUnit = pure "void"
+cftySpec fc CFInt = pure "int"
+cftySpec fc CFString = pure "string"
+cftySpec fc CFDouble = pure "double"
+cftySpec fc CFChar = pure "char"
+cftySpec fc CFPtr = pure "void*"
+cftySpec fc (CFIORes t) = cftySpec fc t
+cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++
+                         " to foreign function"))
+
+cCall : {auto c : Ref Ctxt Defs} ->
+        {auto l : Ref Loaded (List String)} ->
+        FC -> (cfn : String) -> (clib : Maybe String) ->
+        List (Name, CFType) -> CFType -> Core (String, String)
+cCall fc cfn mclib args ret
+    = do loaded <- get Loaded
+         lib <- maybe (pure "")
+                  (\clib => 
+                      if clib `elem` loaded
+                         then pure ""
+                         else do (fname, fullname) <- locate clib
+                                 put Loaded (clib :: loaded)
+                                 pure $ "(load-shared-object \"" 
+                                          ++ escapeQuotes fullname
+                                          ++ "\")\n")
+                  mclib
+         argTypes <- traverse (\a => do s <- cftySpec fc (snd a)
+                                        pure (fst a, s)) args
+         retType <- cftySpec fc ret
+         let call = "((foreign-procedure #f " ++ show cfn ++ " ("
+                      ++ showSep " " (map snd argTypes) ++ ") " ++ retType ++ ") "
+                      ++ showSep " " (map (schName . fst) argTypes) ++ ")"
+
+         pure (lib, case ret of
+                         CFIORes _ => handleRet retType call
+                         _ => call)
+
+schemeCall : FC -> (sfn : String) ->
+             List Name -> CFType -> Core String
+schemeCall fc sfn argns ret
+    = let call = "(" ++ sfn ++ " " ++ showSep " " (map schName argns) ++ ")" in
+          case ret of
+               CFIORes _ => pure $ mkWorld call
+               _ => pure call
+
+-- Use a calling convention to compile a foreign def.
+-- Returns any preamble needed for loading libraries, and the body of the
+-- function call.
+useCC : {auto c : Ref Ctxt Defs} ->
+        {auto l : Ref Loaded (List String)} ->
+        FC -> List String -> List (Name, CFType) -> CFType -> Core (String, String)
+useCC fc [] args ret
+    = throw (GenericMsg fc "No recognised foreign calling convention")
+useCC fc (cc :: ccs) args ret
+    = case parseCC cc of
+           Nothing => useCC fc ccs args ret
+           Just ("scheme", [sfn]) => 
+               do body <- schemeCall fc sfn (map fst args) ret
+                  pure ("", body)
+           Just ("C", [cfn]) => cCall fc cfn Nothing args ret
+           Just ("C", [cfn, clib]) => cCall fc cfn (Just clib) args ret
+           Just ("C", [cfn, clib, chdr]) => cCall fc cfn (Just clib) args ret
+           _ => useCC fc ccs args ret
+
+-- For every foreign arg type, return a name, and whether to pass it to the
+-- foreign call (we don't pass '%World')
+mkArgs : Int -> List CFType -> List (Name, Bool)
+mkArgs i [] = []
+mkArgs i (CFWorld :: cs) = (MN "farg" i, False) :: mkArgs i cs
+mkArgs i (c :: cs) = (MN "farg" i, True) :: mkArgs (i + 1) cs
+
+schFgnDef : {auto c : Ref Ctxt Defs} ->
+            {auto l : Ref Loaded (List String)} ->
+            FC -> Name -> CDef -> Core (String, String)
+schFgnDef fc n (MkForeign cs args ret) 
+    = do let argns = mkArgs 0 args
+         let allargns = map fst argns
+         let useargns = map fst (filter snd argns)
+         (load, body) <- useCC fc cs (zip useargns args) ret
+         defs <- get Ctxt
+         pure (load,
+                "(define " ++ schName !(full (gamma defs) n) ++
+                " (lambda (" ++ showSep " " (map schName allargns) ++ ") " ++
+                body ++ "))\n")
+schFgnDef _ _ _ = pure ("", "")
+
+getFgnCall : {auto c : Ref Ctxt Defs} ->
+             {auto l : Ref Loaded (List String)} ->
+             Name -> Core (String, String)
+getFgnCall n
+    = do defs <- get Ctxt
+         case !(lookupCtxtExact n (gamma defs)) of
+           Nothing => throw (InternalError ("Compiling undefined name " ++ show n))
+           Just def => case compexpr def of
+                          Nothing =>
+                             throw (InternalError ("No compiled definition for " ++ show n))
+                          Just d => schFgnDef (location def) n d
+
 ||| Compile a TT expression to Chez Scheme
 compileToSS : Ref Ctxt Defs ->
               ClosedTerm -> (outfile : String) -> Core ()
@@ -127,13 +230,17 @@ compileToSS c tm outfile
          libs <- findLibs ds
          (ns, tags) <- findUsedNames tm
          defs <- get Ctxt
+         l <- newRef {t = List String} Loaded []
+         fgndefs <- traverse getFgnCall ns
          compdefs <- traverse (getScheme chezExtPrim defs) ns
-         let code = concat compdefs
+         let code = concat (map snd fgndefs) ++ concat compdefs
          main <- schExp chezExtPrim 0 [] !(compileExp tags tm)
          chez <- coreLift findChez
          support <- readDataFile "chez/support.ss"
          let scm = schHeader chez (map snd libs) ++ 
-                   support ++ code ++ main ++ schFooter
+                   support ++ code ++ 
+                   concat (map fst fgndefs) ++
+                   main ++ schFooter
          Right () <- coreLift $ writeFile outfile scm
             | Left err => throw (FileErr outfile err)
          coreLift $ chmod outfile 0o755

src/Compiler/Scheme/Common.idr

@@ -21,6 +21,7 @@ schString s = concatMap okchar (unpack s)
                   then cast c
                   else "C-" ++ show (cast {to=Int} c)
 
+export
 schName : Name -> String
 schName (NS ns n) = showSep "-" ns ++ "-" ++ schName n
 schName (UN n) = schString n
@@ -48,6 +49,7 @@ extendSVars {ns} xs vs = extSVars' (cast (length ns)) xs vs
     extSVars' i [] vs = vs
     extSVars' i (x :: xs) vs = schName (MN "v" i) :: extSVars' (i + 1) xs vs
 
+export
 initSVars : (xs : List Name) -> SVars xs
 initSVars xs = rewrite sym (appendNilRightNeutral xs) in extendSVars xs []
 
@@ -215,6 +217,12 @@ schConstant WorldType = "#t"
 schCaseDef : Maybe String -> String
 schCaseDef Nothing = ""
 schCaseDef (Just tm) = "(else " ++ tm ++ ")"
+  
+export
+schArglist : SVars ns -> String
+schArglist [] = ""
+schArglist [x] = x
+schArglist (x :: xs) = x ++ " " ++ schArglist xs
 
 parameters (schExtPrim : {vars : _} -> Int -> SVars vars -> ExtPrim -> List (CExp vars) -> Core String)
   mutual
@@ -338,11 +346,6 @@ parameters (schExtPrim : {vars : _} -> Int -> SVars vars -> ExtPrim -> List (CEx
       = throw (InternalError ("Badly formed external primitive " ++ show prim
                                 ++ " " ++ show args))
 
-  schArglist : SVars ns -> String
-  schArglist [] = ""
-  schArglist [x] = x
-  schArglist (x :: xs) = x ++ " " ++ schArglist xs
-
   schDef : {auto c : Ref Ctxt Defs} ->
            Name -> CDef -> Core String
   schDef n (MkFun args exp)
@@ -351,6 +354,7 @@ parameters (schExtPrim : {vars : _} -> Int -> SVars vars -> ExtPrim -> List (CEx
                       ++ !(schExp 0 vs exp) ++ "))\n"
   schDef n (MkError exp)
      = pure $ "(define (" ++ schName !(getFullName n) ++ " . any-args) " ++ !(schExp 0 [] exp) ++ ")\n"
+  schDef n (MkForeign _ _ _) = pure "" -- compiled by specific back end
   schDef n (MkCon t a) = pure "" -- Nothing to compile here
   
 -- Convert the name to scheme code

src/Core/Binary.idr

@@ -27,7 +27,7 @@ import Data.Buffer
 -- TTC files can only be compatible if the version number is the same
 export
 ttcVersion : Int
-ttcVersion = 6
+ttcVersion = 7
 
 export
 checkTTCVersion : Int -> Int -> Core ()

src/Core/CompileExpr.idr

@@ -8,7 +8,7 @@ import Core.TT
 
 import Data.Vect
 
-%default total
+%default covering
 
 mutual
   ||| CExp - an expression ready for compiling.
@@ -53,12 +53,30 @@ mutual
   data CConstAlt : List Name -> Type where
        MkConstAlt : Constant -> CExp vars -> CConstAlt vars
 
+-- Argument type descriptors for foreign function calls
+public export
+data CFType : Type where
+     CFUnit : CFType
+     CFInt : CFType
+     CFString : CFType
+     CFDouble : CFType
+     CFChar : CFType
+     CFPtr : CFType
+     CFWorld : CFType
+     CFIORes : CFType -> CFType
+     CFUser : Name -> List CFType -> CFType
+
 public export
 data CDef : Type where
      -- Normal function definition
      MkFun : (args : List Name) -> CExp args -> CDef
      -- Constructor
      MkCon : (tag : Int) -> (arity : Nat) -> CDef
+     -- Foreign definition
+     MkForeign : (ccs : List String) -> 
+                 (fargs : List CFType) -> 
+                 CFType ->
+                 CDef
      -- A function which will fail at runtime (usually due to being a hole) so needs
      -- to run, discarding arguments, no matter how many arguments are passed
      MkError : CExp [] -> CDef
@@ -99,10 +117,25 @@ mutual
     show (MkConstAlt x exp)
          = "(%constcase " ++ show x ++ " " ++ show exp ++ ")"
 
+export
+Show CFType where
+  show CFUnit = "Unit"
+  show CFInt = "Int"
+  show CFString = "String"
+  show CFDouble = "Double"
+  show CFChar = "Char"
+  show CFPtr = "Ptr"
+  show CFWorld = "%World"
+  show (CFIORes t) = "IORes " ++ show t
+  show (CFUser n args) = show n ++ " " ++ show args
+
 export
 Show CDef where
   show (MkFun args exp) = show args ++ ": " ++ show exp
   show (MkCon tag arity) = "Constructor tag " ++ show tag ++ " arity " ++ show arity
+  show (MkForeign ccs args ret) 
+      = "Foreign call " ++ show ccs ++ " " ++ 
+        show args ++ " -> " ++ show ret
   show (MkError exp) = "Error: " ++ show exp
 
 mutual

src/Core/Context.idr

@@ -34,6 +34,10 @@ data Def : Type where
                 -- find size changes in termination checking
             Def -- Ordinary function definition
     ExternDef : (arity : Nat) -> Def
+    ForeignDef : (arity : Nat) -> 
+                 List String -> -- supported calling conventions,
+                                -- e.g "C:printf,libc,stdlib.h", "scheme:display", ...
+                 Def
     Builtin : {arity : Nat} -> PrimFn arity -> Def
     DCon : (tag : Int) -> (arity : Nat) -> Def -- data constructor
     TCon : (tag : Int) -> (arity : Nat) ->
@@ -65,7 +69,9 @@ Show Def where
       = "TyCon " ++ show t ++ " " ++ show a ++ " params: " ++ show ps ++ 
         " constructors: " ++ show cons ++ 
         " mutual with: " ++ show ms
-  show (ExternDef arity) = "<external def with arith " ++ show arity ++ ">"
+  show (ExternDef arity) = "<external def with arity " ++ show arity ++ ">"
+  show (ForeignDef a cs) = "<foreign def with arity " ++ show a ++ 
+                           " " ++ show cs ++">"
   show (Builtin {arity} _) = "<builtin with arith " ++ show arity ++ ">"
   show (Hole _ p) = "Hole" ++ if p then " [impl]" else ""
   show (BySearch c depth def) = "Search in " ++ show def

src/Core/TTC.idr

@@ -638,20 +638,48 @@ mutual
              pure (MkConstAlt c sc)
 
 export
-  TTC CDef where
+TTC CFType where
-    toBuf b (MkFun args cexpr) = do tag 0; toBuf b args; toBuf b cexpr
+  toBuf b CFUnit = tag 0
-    toBuf b (MkCon t arity) = do tag 1; toBuf b t; toBuf b arity
+  toBuf b CFInt = tag 1
-    toBuf b (MkError cexpr) = do tag 2; toBuf b cexpr
+  toBuf b CFString = tag 2
+  toBuf b CFDouble = tag 3
+  toBuf b CFChar = tag 4
+  toBuf b CFPtr = tag 5
+  toBuf b CFWorld = tag 6
+  toBuf b (CFIORes t) = do tag 7; toBuf b t
+  toBuf b (CFUser n a) = do tag 8; toBuf b n; toBuf b a
 
-    fromBuf b 
+  fromBuf b
-        = case !getTag of
+      = case !getTag of
-               0 => do args <- fromBuf b; cexpr <- fromBuf b
+             0 => pure CFUnit
-                       pure (MkFun args cexpr)
+             1 => pure CFInt
-               1 => do t <- fromBuf b; arity <- fromBuf b
+             2 => pure CFString
-                       pure (MkCon t arity)
+             3 => pure CFDouble
-               2 => do cexpr <- fromBuf b
+             4 => pure CFChar
-                       pure (MkError cexpr)
+             5 => pure CFPtr
-               _ => corrupt "CDef"
+             6 => pure CFWorld
+             7 => do t <- fromBuf b; pure (CFIORes t)
+             8 => do n <- fromBuf b; a <- fromBuf b; pure (CFUser n a)
+             _ => corrupt "CFType"
+
+export
+TTC CDef where
+  toBuf b (MkFun args cexpr) = do tag 0; toBuf b args; toBuf b cexpr
+  toBuf b (MkCon t arity) = do tag 1; toBuf b t; toBuf b arity
+  toBuf b (MkForeign cs args ret) = do tag 2; toBuf b cs; toBuf b args; toBuf b ret
+  toBuf b (MkError cexpr) = do tag 3; toBuf b cexpr
+
+  fromBuf b 
+      = case !getTag of
+             0 => do args <- fromBuf b; cexpr <- fromBuf b
+                     pure (MkFun args cexpr)
+             1 => do t <- fromBuf b; arity <- fromBuf b
+                     pure (MkCon t arity)
+             2 => do cs <- fromBuf b; args <- fromBuf b; ret <- fromBuf b
+                     pure (MkForeign cs args ret)
+             3 => do cexpr <- fromBuf b
+                     pure (MkError cexpr)
+             _ => corrupt "CDef"
 
 export
 TTC CG where
@@ -708,19 +736,21 @@ TTC Def where
       = do tag 1; toBuf b args; toBuf b ct; toBuf b rt; toBuf b pats
   toBuf b (ExternDef a)
       = do tag 2; toBuf b a
+  toBuf b (ForeignDef a cs)
+      = do tag 3; toBuf b a; toBuf b cs
   toBuf b (Builtin a)
       = throw (InternalError "Trying to serialise a Builtin")
-  toBuf b (DCon t arity) = do tag 3; toBuf b t; toBuf b arity
+  toBuf b (DCon t arity) = do tag 4; toBuf b t; toBuf b arity
   toBuf b (TCon t arity parampos detpos ms datacons) 
-      = do tag 4; toBuf b t; toBuf b arity; toBuf b parampos
+      = do tag 5; toBuf b t; toBuf b arity; toBuf b parampos
            toBuf b detpos; toBuf b ms; toBuf b datacons
   toBuf b (Hole locs p) 
-      = do tag 5; toBuf b locs; toBuf b p
+      = do tag 6; toBuf b locs; toBuf b p
   toBuf b (BySearch c depth def) 
-      = do tag 6; toBuf b c; toBuf b depth; toBuf b def
+      = do tag 7; toBuf b c; toBuf b depth; toBuf b def
-  toBuf b (Guess guess constraints) = do tag 7; toBuf b guess; toBuf b constraints
+  toBuf b (Guess guess constraints) = do tag 8; toBuf b guess; toBuf b constraints
-  toBuf b ImpBind = tag 8
+  toBuf b ImpBind = tag 9
-  toBuf b Delayed = tag 9
+  toBuf b Delayed = tag 10
 
   fromBuf b 
       = case !getTag of
@@ -732,22 +762,25 @@ TTC Def where
                      pure (PMDef False args ct rt pats)
              2 => do a <- fromBuf b
                      pure (ExternDef a)
-             3 => do t <- fromBuf b; a <- fromBuf b
+             3 => do a <- fromBuf b
-                     pure (DCon t a)
+                     cs <- fromBuf b
+                     pure (ForeignDef a cs)
              4 => do t <- fromBuf b; a <- fromBuf b
+                     pure (DCon t a)
+             5 => do t <- fromBuf b; a <- fromBuf b
                      ps <- fromBuf b; dets <- fromBuf b; 
                      ms <- fromBuf b; cs <- fromBuf b
                      pure (TCon t a ps dets ms cs)
-             5 => do l <- fromBuf b
+             6 => do l <- fromBuf b
                      p <- fromBuf b
                      pure (Hole l p)
-             6 => do c <- fromBuf b; depth <- fromBuf b
+             7 => do c <- fromBuf b; depth <- fromBuf b
                      def <- fromBuf b
                      pure (BySearch c depth def)
-             7 => do g <- fromBuf b; cs <- fromBuf b
+             8 => do g <- fromBuf b; cs <- fromBuf b
                      pure (Guess g cs)
-             8 => pure ImpBind
+             9 => pure ImpBind
-             9 => pure Context.Delayed
+             10 => pure Context.Delayed
              _ => corrupt "Def"
 
 TTC TotalReq where

src/Idris/Parser.idr

@@ -1024,6 +1024,9 @@ fnDirectOpt
          pure Inline
   <|> do exactIdent "extern"
          pure ExternFn
+  <|> do exactIdent "foreign"
+         cs <- many strLit
+         pure (ForeignFn cs)
 
 visOpt : Rule (Either Visibility FnOpt)
 visOpt

src/TTImp/ProcessType.idr

@@ -17,6 +17,8 @@ import TTImp.TTImp
 
 import Data.NameMap
 
+%default covering
+
 getRetTy : Defs -> NF [] -> Core Name
 getRetTy defs (NBind fc _ (Pi _ _ _) sc)
     = getRetTy defs !(sc defs (toClosure defaultOpts [] (Erased fc)))
@@ -39,6 +41,8 @@ processFnOpt fc ndef (GlobalHint a)
     = addGlobalHint ndef a
 processFnOpt fc ndef ExternFn
     = setFlag fc ndef Inline -- if externally defined, inline when compiling
+processFnOpt fc ndef (ForeignFn _)
+    = setFlag fc ndef Inline -- if externally defined, inline when compiling
 processFnOpt fc ndef Invertible
     = setFlag fc ndef Invertible
 processFnOpt fc ndef Total
@@ -48,6 +52,25 @@ processFnOpt fc ndef Covering
 processFnOpt fc ndef PartialOK
     = setFlag fc ndef (SetTotal PartialOK)
 
+-- If it's declared as externally defined, set the definition to
+-- ExternFn <arity>, where the arity is assumed to be fixed (i.e.
+-- not dependent on any of the arguments)
+-- Similarly set foreign definitions. Possibly combine these?
+initDef : {auto c : Ref Ctxt Defs} ->
+          Name -> Env Term vars -> Term vars -> List FnOpt -> Core Def
+initDef n env ty [] 
+    = do addUserHole n
+         pure None
+initDef n env ty (ExternFn :: opts)
+    = do defs <- get Ctxt
+         a <- getArity defs env ty
+         pure (ExternDef a)
+initDef n env ty (ForeignFn cs :: opts)
+    = do defs <- get Ctxt
+         a <- getArity defs env ty
+         pure (ForeignDef a cs)
+initDef n env ty (_ :: opts) = initDef n env ty opts
+
 export
 processType : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
@@ -76,16 +99,8 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
                              (gType fc)
          logTermNF 5 ("Type of " ++ show n) [] (abstractEnvType tfc env ty)
          -- TODO: Check name visibility
-         -- If it's declared as externally defined, set the definition to
-         -- ExternFn <arity>, where the arity is assumed to be fixed (i.e.
-         -- not dependent on any of the arguments)
-         def <- if ExternFn `elem` opts
-                   then do defs <- get Ctxt
-                           a <- getArity defs env ty
-                           pure (ExternDef a)
-                   else do addUserHole n
-                           pure None
 
+         def <- initDef n env ty opts
          addDef (Resolved idx) (newDef fc n rig vars (abstractEnvType tfc env ty) vis def)
          -- Flag it as checked, because we're going to check the clauses 
          -- from the top level.

src/TTImp/TTImp.idr

@@ -163,6 +163,8 @@ mutual
        -- Flag means to use as a default if all else fails
        GlobalHint : Bool -> FnOpt
        ExternFn : FnOpt
+       -- Defined externally, list calling conventions
+       ForeignFn : List String -> FnOpt 
        -- assume safe to cancel arguments in unification
        Invertible : FnOpt
        Total : FnOpt
@@ -175,6 +177,7 @@ mutual
     show (Hint t) = "%hint " ++ show t
     show (GlobalHint t) = "%globalhint " ++ show t
     show ExternFn = "%extern"
+    show (ForeignFn cs) = "%foreign " ++ showSep " " (map show cs)
     show Invertible = "%invertible"
     show Total = "total"
     show Covering = "covering"
@@ -186,6 +189,7 @@ mutual
     (Hint x) == (Hint y) = x == y
     (GlobalHint x) == (GlobalHint y) = x == y
     ExternFn == ExternFn = True
+    (ForeignFn xs) == (ForeignFn ys) = xs == ys
     Invertible == Invertible = True
     Total == Total = True
     Covering == Covering = True
@@ -789,10 +793,11 @@ mutual
     toBuf b (Hint t) = do tag 1; toBuf b t
     toBuf b (GlobalHint t) = do tag 2; toBuf b t
     toBuf b ExternFn = tag 3
-    toBuf b Invertible = tag 4
+    toBuf b (ForeignFn cs) = do tag 4; toBuf b cs
-    toBuf b Total = tag 5
+    toBuf b Invertible = tag 5
-    toBuf b Covering = tag 6
+    toBuf b Total = tag 6
-    toBuf b PartialOK = tag 7
+    toBuf b Covering = tag 7
+    toBuf b PartialOK = tag 8
 
     fromBuf b
         = case !getTag of
@@ -800,10 +805,11 @@ mutual
                1 => do t <- fromBuf b; pure (Hint t)
                2 => do t <- fromBuf b; pure (GlobalHint t)
                3 => pure ExternFn
-               4 => pure Invertible
+               4 => do cs <- fromBuf b; pure (ForeignFn cs)
-               5 => pure Total
+               5 => pure Invertible
-               6 => pure Covering
+               6 => pure Total
-               7 => pure PartialOK
+               7 => pure Covering
+               8 => pure PartialOK
                _ => corrupt "FnOpt"
 
   export

support/chez/support.ss

@@ -45,6 +45,7 @@
 (define blodwen-error-quit
   (lambda (msg)
     (display msg)
+    (newline)
     (exit 1)))
 
 ;; Buffers

support/chicken/support.scm

@@ -45,6 +45,7 @@
 (define blodwen-error-quit
   (lambda (msg)
     (display msg)
+    (newline)
     (exit 1)))
 
 ;; Files: Much of the following adapted from idris-chez, thanks to Niklas

support/racket/support.rkt

@@ -45,6 +45,7 @@
 (define blodwen-error-quit
   (lambda (msg)
     (display msg)
+    (newline)
     (exit 1)))
 
 ;; Files : Much of the following adapted from idris-chez, thanks to Niklas