Merge branch 'master' into add-version-command

INSTALL.md

@@ -24,7 +24,9 @@ Chez Scheme is available to build from source:
 
 + https://cisco.github.io/ChezScheme/
 
-Many popular package managers will provide a binary distribution for Chez.
+Many popular package managers will provide a binary distribution for Chez. Note
+that homebrew for Mac OS X provides a version without multithreading support, so
+Mac OS X users will want to build from source.
 
 **Note**: If you install ChezScheme from source files, building it locally, make sure
 you run `./configure --threads` to build multithreading support in.

Makefile

@@ -6,7 +6,7 @@ PATCH=0
 PREFIX ?= ${HOME}/.idris2
 IDRIS_VERSION := $(shell idris --version)
 VALID_IDRIS_VERSION_REGEXP = "1.3.2.*"
-export IDRIS2_PATH = ${CURDIR}/libs/prelude/build:${CURDIR}/libs/base/build
+export IDRIS2_PATH = ${CURDIR}/libs/prelude/build/ttc:${CURDIR}/libs/base/build/ttc
 export IDRIS2_DATA = ${CURDIR}/support
 
 -include custom.mk

Notes/IDE-mode.md

@@ -40,4 +40,3 @@ Generates a pattern matching definition, if it can find one, for the function
 declared with the given name, on the given line. It will only return the
 first definition it finds, as a list of pattern clauses. This works via a
 combination of case splitting and expression search.
-

libs/base/Data/Buffer.idr

@@ -4,12 +4,12 @@ import System.File
 
 export
 data Buffer : Type where
-     MkBuffer : Ptr -> (size : Int) -> (loc : Int) -> Buffer
+     MkBuffer : AnyPtr -> (size : Int) -> (loc : Int) -> Buffer
 
 export
 newBuffer : Int -> IO Buffer
 newBuffer size
-    = do buf <- schemeCall Ptr "blodwen-new-buffer" [size]
+    = do buf <- schemeCall AnyPtr "blodwen-new-buffer" [size]
          pure (MkBuffer buf size 0)
 
 export

libs/network/Makefile

@@ -31,7 +31,6 @@ LIBTARGET = $(LIBNAME).a
 TARGET=${HOME}/.idris2
 
 build: $(DYLIBTARGET) $(IDRIS_SRCS)
-	@if ! [ -d build ]; then echo "creating 'build' directory"; mkdir build ; else echo "directory 'build' exists"; fi
 	@if [ -z "${IDRIS2}" ]; then echo 'variable $$IDRIS2 is not set, aborting'; exit 1; fi
 	${IDRIS2} --build network.ipkg
 

libs/network/Network/Socket.idr

@@ -85,7 +85,7 @@ accept sock = do
   -- We need a pointer to a sockaddr structure. This is then passed into
   -- idrnet_accept and populated. We can then query it for the SocketAddr and free it.
 
-  sockaddr_ptr <- cCall Ptr "idrnet_create_sockaddr" []
+  sockaddr_ptr <- cCall AnyPtr "idrnet_create_sockaddr" []
 
   accept_res <- cCall Int "idrnet_accept" [ descriptor sock, sockaddr_ptr ]
   if accept_res == (-1)
@@ -128,7 +128,7 @@ recv : (sock : Socket)
 recv sock len = do
   -- Firstly make the request, get some kind of recv structure which
   -- contains the result of the recv and possibly the retrieved payload
-  recv_struct_ptr <- cCall Ptr "idrnet_recv" [ descriptor sock, len]
+  recv_struct_ptr <- cCall AnyPtr "idrnet_recv" [ descriptor sock, len]
   recv_res <- cCall Int "idrnet_get_recv_res"  [ recv_struct_ptr ]
 
   if recv_res == (-1)
@@ -202,7 +202,7 @@ recvFrom : (sock : Socket)
         -> (len  : ByteLength)
         -> IO (Either SocketError (UDPAddrInfo, String, ResultCode))
 recvFrom sock bl = do
-  recv_ptr <- cCall Ptr "idrnet_recvfrom"
+  recv_ptr <- cCall AnyPtr "idrnet_recvfrom"
               [ descriptor sock, bl ]
 
   let recv_ptr' = RFPtr recv_ptr

libs/network/Network/Socket/Data.idr

@@ -63,7 +63,7 @@ getErrno : IO SocketError
 getErrno = cCall Int "idrnet_errno" []
 
 export
-nullPtr : Ptr -> IO Bool
+nullPtr : AnyPtr -> IO Bool
 nullPtr p = cCall Bool "isNull" [p]
 
 -- -------------------------------------------------------------- [ Interfaces ]

libs/network/Network/Socket/Raw.idr

@@ -10,16 +10,16 @@ import public Network.Socket.Data
 -- ---------------------------------------------------------------- [ Pointers ]
 
 public export
-data RecvStructPtr     = RSPtr Ptr
+data RecvStructPtr     = RSPtr AnyPtr
 
 public export
-data RecvfromStructPtr = RFPtr Ptr
+data RecvfromStructPtr = RFPtr AnyPtr
 
 public export
-data BufPtr = BPtr Ptr
+data BufPtr = BPtr AnyPtr
 
 public export
-data SockaddrPtr = SAPtr Ptr
+data SockaddrPtr = SAPtr AnyPtr
 
 -- ---------------------------------------------------------- [ Socket Utilies ]
 
@@ -35,7 +35,7 @@ sockaddr_free (SAPtr ptr) = cCall () "idrnet_free" [ptr]
 |||
 ||| Used to allocate a mutable pointer to be given to the Recv functions.
 sock_alloc : ByteLength -> IO BufPtr
-sock_alloc bl = map BPtr $ cCall Ptr "idrnet_malloc" [bl]
+sock_alloc bl = map BPtr $ cCall AnyPtr "idrnet_malloc" [bl]
 
 ||| Retrieves the port the given socket is bound to
 export
@@ -141,14 +141,14 @@ foreignGetRecvfromPayload (RFPtr p) = cCall String "idrnet_get_recvfrom_payload"
 export
 foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress
 foreignGetRecvfromAddr (RFPtr p) = do
-  sockaddr_ptr <- map SAPtr $ cCall Ptr "idrnet_get_recvfrom_sockaddr" [p]
+  sockaddr_ptr <- map SAPtr $ cCall AnyPtr "idrnet_get_recvfrom_sockaddr" [p]
   getSockAddr sockaddr_ptr
 
 ||| Utility function to return sender's IPV4 port.
 export
 foreignGetRecvfromPort : RecvfromStructPtr -> IO Port
 foreignGetRecvfromPort (RFPtr p) = do
-  sockaddr_ptr <- cCall Ptr "idrnet_get_recvfrom_sockaddr" [p]
+  sockaddr_ptr <- cCall AnyPtr "idrnet_get_recvfrom_sockaddr" [p]
   port         <- cCall Int "idrnet_sockaddr_ipv4_port" [sockaddr_ptr]
   pure port
 
@@ -169,7 +169,7 @@ recvFromBuf : (sock : Socket)
            -> (len  : ByteLength)
            -> IO (Either SocketError (UDPAddrInfo, ResultCode))
 recvFromBuf sock (BPtr ptr) bl = do
-  recv_ptr <- cCall Ptr "idrnet_recvfrom_buf" [ descriptor sock, ptr, bl]
+  recv_ptr <- cCall AnyPtr "idrnet_recvfrom_buf" [ descriptor sock, ptr, bl]
 
   let recv_ptr' = RFPtr recv_ptr
 

libs/prelude/PrimIO.idr

@@ -21,11 +21,22 @@ 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
 
+-- A pointer representing a given parameter type
+-- The parameter is a phantom type, to help differentiate between
+-- different pointer types
 public export
-data Ptr : Type where
+data Ptr : Type -> Type where
+
+-- A pointer to any type (representing a void* in foreign calls)
+public export
+data AnyPtr : Type where
 
 public export
 data ThreadID : Type where

src/Compiler/Common.idr

@@ -8,6 +8,8 @@ import Core.TT
 
 import Data.NameMap
 
+import System.Info
+
 %include C "sys/stat.h"
 
 ||| Generic interface to some code generator
@@ -120,3 +122,34 @@ 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))
+
+export
+dylib_suffix : String
+dylib_suffix
+    = cond [(os `elem` ["windows", "mingw32", "cygwin32"], "dll"),
+            (os == "darwin", "dylib")]
+           "so"

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,60 @@ 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
+     NPtr : NArgs
+     NIORes : Closure [] -> NArgs
+
+getNArgs : Name -> List (Closure []) -> NArgs
+getNArgs (NS _ (UN "IORes")) [arg] = NIORes arg
+getNArgs (NS _ (UN "Ptr")) [arg] = NPtr
+getNArgs (NS _ (UN "AnyPtr")) [] = NPtr
+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
+              NPtr => pure CFPtr
+              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 +336,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 +350,22 @@ 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 _ (DCon tag arity)
-    = case lookup n tags of
+    = pure $ MkCon (fromMaybe tag $ lookup n tags) arity
-           Just t => pure $ MkCon t arity
+toCDef tags n _ (TCon tag arity _ _ _ _)
-           _ => pure $ MkCon tag arity
+    = pure $ MkCon (fromMaybe tag $ lookup n tags) arity
-toCDef tags n (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

@@ -18,10 +18,6 @@ import System.Info
 
 %default covering
 
-firstExists : List String -> IO (Maybe String)
-firstExists [] = pure Nothing
-firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs
-
 findChez : IO String
 findChez
     = do env <- getEnv "CHEZ"
@@ -29,7 +25,33 @@ findChez
             Just n => pure n
             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
+                          pure $ fromMaybe "/usr/bin/env -S scheme" e
+
+locate : {auto c : Ref Ctxt Defs} ->
+         String -> Core (String, String)
+locate libspec
+    = do -- Attempt to turn libspec into an appropriate filename for the system
+         let fname
+              = case words libspec of
+                     [] => ""
+                     [fn] => if '.' `elem` unpack fn
+                                then fn -- full filename given
+                                else -- add system extension
+                                     fn ++ "." ++ dylib_suffix
+                     (fn :: ver :: _) =>
+                          -- library and version given, build path name as
+                          -- appropriate for the system
+                          cond [(dylib_suffix == "dll",
+                                      fn ++ "-" ++ ver ++ ".dll"),
+                                (dylib_suffix == "dylib",
+                                      fn ++ "." ++ ver ++ ".dylib")]
+                                (fn ++ "." ++ dylib_suffix ++ "." ++ ver)
+
+         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 +65,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
@@ -87,9 +101,12 @@ mutual
   tySpec (CCon fc (UN "String") _ []) = pure "string"
   tySpec (CCon fc (UN "Double") _ []) = pure "double"
   tySpec (CCon fc (UN "Char") _ []) = pure "char"
+  tySpec (CCon fc (NS _ n) _ [_])
+     = cond [(n == UN "Ptr", pure "void*")]
+          (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function")))
   tySpec (CCon fc (NS _ n) _ [])
      = cond [(n == UN "Unit", pure "void"),
-             (n == UN "Ptr", pure "void*")]
+             (n == UN "AnyPtr", pure "void*")]
           (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function")))
   tySpec ty = throw (GenericMsg (getFC ty) ("Can't pass argument of type " ++ show ty ++ " to foreign function"))
 
@@ -119,6 +136,104 @@ 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 : String) ->
+        List (Name, CFType) -> CFType -> Core (String, String)
+cCall fc cfn clib args ret
+    = do loaded <- get Loaded
+         lib <- if clib `elem` loaded
+                   then pure ""
+                   else do (fname, fullname) <- locate clib
+                           put Loaded (clib :: loaded)
+                           pure $ "(load-shared-object \""
+                                    ++ escapeQuotes fullname
+                                    ++ "\")\n"
+         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, clib]) => cCall fc cfn clib args ret
+           Just ("C", [cfn, clib, chdr]) => cCall fc cfn 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 +242,17 @@ compileToSS c tm outfile
          libs <- findLibs ds
          (ns, tags) <- findUsedNames tm
          defs <- get Ctxt
+         l <- newRef {t = List String} Loaded ["libc", "libc 6"]
+         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
@@ -177,4 +296,3 @@ executeExpr c tm
 export
 codegenChez : Codegen
 codegenChez = MkCG compileExpr executeExpr
-

src/Compiler/Scheme/Chicken.idr

@@ -18,10 +18,6 @@ import System.Info
 
 %default covering
 
-firstExists : List String -> IO (Maybe String)
-firstExists [] = pure Nothing
-firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs
-
 findCSI : IO String
 findCSI = pure "/usr/bin/env csi"
 

src/Compiler/Scheme/Common.idr

@@ -13,6 +13,11 @@ import Data.Vect
 
 %default covering
 
+export
+firstExists : List String -> IO (Maybe String)
+firstExists [] = pure Nothing
+firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs
+
 schString : String -> String
 schString s = concatMap okchar (unpack s)
   where
@@ -21,6 +26,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 +54,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 []
 
@@ -216,6 +223,12 @@ 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
     schConAlt : Int -> SVars vars -> String -> CConAlt vars -> Core String
@@ -338,11 +351,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 +359,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/Compiler/Scheme/Racket.idr

@@ -17,20 +17,18 @@ import System.Info
 
 %default covering
 
-firstExists : List String -> IO (Maybe String)
-firstExists [] = pure Nothing
-firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs
-
 findRacket : IO String
 findRacket = pure "/usr/bin/env racket"
 
 findRacoExe : IO String
 findRacoExe = pure "raco exe"
 
-schHeader : String
+schHeader : String -> String
-schHeader
+schHeader libs
   = "#lang racket/base\n" ++
     "(require racket/promise)\n" ++ -- for force/delay
+    "(require ffi/unsafe ffi/unsafe/define)\n" ++ -- for calling C
+    libs ++
     "(let ()\n"
 
 schFooter : String
@@ -43,16 +41,151 @@ mutual
   racketPrim i vs prim args 
       = schExtCommon racketPrim 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/utf-8"
+cftySpec fc CFDouble = pure "_double"
+cftySpec fc CFChar = pure "_int8"
+cftySpec fc CFPtr = pure "_pointer"
+cftySpec fc (CFIORes t) = cftySpec fc t
+cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++
+                         " to foreign function"))
+
+loadlib : String -> String -> String
+loadlib libn ver
+    = "(define-ffi-definer define-" ++ libn ++ 
+      " (ffi-lib \"" ++ libn ++ "\" " ++ ver ++ "))\n"
+
+getLibVers : String -> (String, String)
+getLibVers libspec
+    = case words libspec of
+           [] => ("", "")
+           [fn] => case span (/='.') libspec of
+                        (root, rest) => (root, "")
+           (fn :: vers) =>
+               (fst (span (/='.') fn),
+                  "'(" ++ showSep " " (map show vers) ++ " #f)" )
+
+cToRkt : CFType -> String -> String
+cToRkt CFChar op = "(integer->char " ++ op ++ ")"
+cToRkt _ op = op
+
+rktToC : CFType -> String -> String
+rktToC CFChar op = "(char->integer " ++ op ++ ")"
+rktToC _ op = op
+
+handleRet : CFType -> String -> String
+handleRet CFUnit op = op ++ " " ++ mkWorld (schConstructor 0 [])
+handleRet ret op = mkWorld (cToRkt ret op)
+
+useArg : (Name, CFType) -> String
+useArg (n, ty)
+    = rktToC ty (schName n)
+
+cCall : {auto c : Ref Ctxt Defs} ->
+        {auto l : Ref Loaded (List String)} ->
+        FC -> (cfn : String) -> (clib : String) ->
+        List (Name, CFType) -> CFType -> Core (String, String)
+cCall fc cfn libspec args ret
+    = do loaded <- get Loaded
+         let (libn, vers) = getLibVers libspec
+         lib <- if libn `elem` loaded
+                   then pure ""
+                   else do put Loaded (libn :: loaded)
+                           pure (loadlib libn vers)
+
+         argTypes <- traverse (\a => do s <- cftySpec fc (snd a)
+                                        pure (a, s)) args
+         retType <- cftySpec fc ret
+         let cbind = "(define-" ++ libn ++ " " ++ cfn ++ 
+                     " (_fun " ++ showSep " " (map snd argTypes) ++ " -> " ++ 
+                         retType ++ "))\n"
+         let call = "(" ++ cfn ++ " " ++
+                    showSep " " (map (useArg . fst) argTypes) ++ ")"
+
+         pure (lib ++ cbind, case ret of
+                                  CFIORes rt => handleRet rt 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, clib]) => cCall fc cfn clib args ret
+           Just ("C", [cfn, clib, chdr]) => cCall fc cfn 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
+
 compileToRKT : Ref Ctxt Defs ->
                ClosedTerm -> (outfile : String) -> Core ()
 compileToRKT c tm outfile
     = do (ns, tags) <- findUsedNames tm
          defs <- get Ctxt
+         l <- newRef {t = List String} Loaded []
+         fgndefs <- traverse getFgnCall ns
          compdefs <- traverse (getScheme racketPrim defs) ns
-         let code = concat compdefs
+         let code = concat (map snd fgndefs) ++ concat compdefs
          main <- schExp racketPrim 0 [] !(compileExp tags tm)
          support <- readDataFile "racket/support.rkt"
-         let scm = schHeader ++ support ++ code ++ "(void " ++ main ++ ")\n" ++ schFooter
+         let scm = schHeader (concat (map fst fgndefs)) ++ 
+                   support ++ code ++ 
+                   "(void " ++ main ++ ")\n" ++ 
+                   schFooter
          Right () <- coreLift $ writeFile outfile scm
             | Left err => throw (FileErr outfile err)
          coreLift $ chmod outfile 0o755

src/Core/AutoSearch.idr

@@ -498,7 +498,7 @@ searchType {vars} fc rigc defaults trying depth def checkdets top env target
                  logNF 5 "For target" env nty
                  searchNames fc rigc defaults (target :: trying) depth def top env ambigok g nty)
              (\err => if ambig err then throw err
-                         else tryGroups (maybe (Just err) Just merr) nty gs)
+                         else tryGroups (Just $ fromMaybe err merr) nty gs)
 
 -- Declared in Core.Unify as:
 -- search : {auto c : Ref Ctxt Defs} ->

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 ++ " " ++ showSep " " (map 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
@@ -111,7 +144,7 @@ mutual
   thin n (CLocal fc prf) 
       = let MkVar var' = insertVar {n} _ prf in
             CLocal fc var'
-  thin n (CRef fc x) = CRef fc x
+  thin _ (CRef fc x) = CRef fc x
   thin {outer} {inner} n (CLam fc x sc)
       = let sc' = thin {outer = x :: outer} {inner} n sc in
             CLam fc x sc'
@@ -134,9 +167,9 @@ mutual
   thin n (CConstCase fc sc xs def)
       = CConstCase fc (thin n sc) (assert_total (map (thinConstAlt n) xs))
                    (assert_total (map (thin n) def))
-  thin n (CPrimVal fc x) = CPrimVal fc x
+  thin _ (CPrimVal fc x) = CPrimVal fc x
-  thin n (CErased fc) = CErased fc
+  thin _ (CErased fc) = CErased fc
-  thin n (CCrash fc x) = CCrash fc x
+  thin _ (CCrash fc x) = CCrash fc x
 
   thinConAlt : (n : Name) -> CConAlt (outer ++ inner) -> CConAlt (outer ++ n :: inner)
   thinConAlt {outer} {inner} n (MkConAlt x tag args sc)
@@ -186,18 +219,18 @@ mutual
 
 export
 getFC : CExp args -> FC
-getFC (CLocal fc y) = fc
+getFC (CLocal fc _) = fc
-getFC (CRef fc x) = fc
+getFC (CRef fc _) = fc
-getFC (CLam fc x y) = fc
+getFC (CLam fc _ _) = fc
-getFC (CLet fc x y z) = fc
+getFC (CLet fc _ _ _) = fc
-getFC (CApp fc x xs) = fc
+getFC (CApp fc _ _) = fc
-getFC (CCon fc x tag xs) = fc
+getFC (CCon fc _ _ _) = fc
-getFC (COp fc x xs) = fc
+getFC (COp fc _ _) = fc
-getFC (CExtPrim fc p xs) = fc
+getFC (CExtPrim fc _ _) = fc
-getFC (CForce fc x) = fc
+getFC (CForce fc _) = fc
-getFC (CDelay fc x) = fc
+getFC (CDelay fc _) = fc
-getFC (CConCase fc sc xs x) = fc
+getFC (CConCase fc _ _ _) = fc
-getFC (CConstCase fc sc xs x) = fc
+getFC (CConstCase fc _ _ _) = fc
-getFC (CPrimVal fc x) = fc
+getFC (CPrimVal fc _) = fc
 getFC (CErased fc) = fc
-getFC (CCrash fc x) = fc
+getFC (CCrash fc _) = fc

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/Core.idr

@@ -248,65 +248,65 @@ Show Error where
 export
 getErrorLoc : Error -> Maybe FC
 getErrorLoc (Fatal err) = getErrorLoc err
-getErrorLoc (CantConvert loc env tm y) = Just loc
+getErrorLoc (CantConvert loc _ _ _) = Just loc
-getErrorLoc (CantSolveEq loc env tm y) = Just loc
+getErrorLoc (CantSolveEq loc _ _ _) = Just loc
-getErrorLoc (PatternVariableUnifies loc env n x) = Just loc
+getErrorLoc (PatternVariableUnifies loc _ _ _) = Just loc
-getErrorLoc (CyclicMeta loc n) = Just loc
+getErrorLoc (CyclicMeta loc _) = Just loc
-getErrorLoc (WhenUnifying loc env tm y z) = Just loc
+getErrorLoc (WhenUnifying loc _ _ _ _) = Just loc
-getErrorLoc (ValidCase loc env y) = Just loc
+getErrorLoc (ValidCase loc _ _) = Just loc
-getErrorLoc (UndefinedName loc y) = Just loc
+getErrorLoc (UndefinedName loc _) = Just loc
-getErrorLoc (InvisibleName loc y _) = Just loc
+getErrorLoc (InvisibleName loc _ _) = Just loc
-getErrorLoc (BadTypeConType loc y) = Just loc
+getErrorLoc (BadTypeConType loc _) = Just loc
-getErrorLoc (BadDataConType loc y z) = Just loc
+getErrorLoc (BadDataConType loc _ _) = Just loc
 getErrorLoc (NotCovering loc _ _) = Just loc
 getErrorLoc (NotTotal loc _ _) = Just loc
-getErrorLoc (LinearUsed loc k y) = Just loc
+getErrorLoc (LinearUsed loc _ _) = Just loc
-getErrorLoc (LinearMisuse loc y z w) = Just loc
+getErrorLoc (LinearMisuse loc _ _ _) = Just loc
 getErrorLoc (BorrowPartial loc _ _ _) = Just loc
 getErrorLoc (BorrowPartialType loc _ _) = Just loc
-getErrorLoc (AmbiguousName loc xs) = Just loc
+getErrorLoc (AmbiguousName loc _) = Just loc
-getErrorLoc (AmbiguousElab loc _ xs) = Just loc
+getErrorLoc (AmbiguousElab loc _ _) = Just loc
-getErrorLoc (AmbiguousSearch loc _ xs) = Just loc
+getErrorLoc (AmbiguousSearch loc _ _) = Just loc
-getErrorLoc (AllFailed ((_, x) :: xs)) = getErrorLoc x
+getErrorLoc (AllFailed ((_, x) :: _)) = getErrorLoc x
 getErrorLoc (AllFailed []) = Nothing
 getErrorLoc (RecordTypeNeeded loc _) = Just loc
 getErrorLoc (NotRecordField loc _ _) = Just loc
 getErrorLoc (NotRecordType loc _) = Just loc
 getErrorLoc (IncompatibleFieldUpdate loc _) = Just loc
-getErrorLoc (InvalidImplicits loc _ y tm) = Just loc
+getErrorLoc (InvalidImplicits loc _ _ _) = Just loc
 getErrorLoc (TryWithImplicits loc _ _) = Just loc
 getErrorLoc (BadUnboundImplicit loc _ _ _) = Just loc
-getErrorLoc (CantSolveGoal loc _ tm) = Just loc
+getErrorLoc (CantSolveGoal loc _ _) = Just loc
-getErrorLoc (DeterminingArg loc n y env tm) = Just loc
+getErrorLoc (DeterminingArg loc _ _ _ _) = Just loc
-getErrorLoc (UnsolvedHoles ((loc, _) :: xs)) = Just loc
+getErrorLoc (UnsolvedHoles ((loc, _) :: _)) = Just loc
 getErrorLoc (UnsolvedHoles []) = Nothing
-getErrorLoc (CantInferArgType loc _ y z tm) = Just loc
+getErrorLoc (CantInferArgType loc _ _ _ _) = Just loc
-getErrorLoc (SolvedNamedHole loc _ _ y) = Just loc
+getErrorLoc (SolvedNamedHole loc _ _ _) = Just loc
-getErrorLoc (VisibilityError loc y z w s) = Just loc
+getErrorLoc (VisibilityError loc _ _ _ _) = Just loc
-getErrorLoc (NonLinearPattern loc y) = Just loc
+getErrorLoc (NonLinearPattern loc _) = Just loc
-getErrorLoc (BadPattern loc y) = Just loc
+getErrorLoc (BadPattern loc _) = Just loc
-getErrorLoc (NoDeclaration loc y) = Just loc
+getErrorLoc (NoDeclaration loc _) = Just loc
-getErrorLoc (AlreadyDefined loc y) = Just loc
+getErrorLoc (AlreadyDefined loc _) = Just loc
-getErrorLoc (NotFunctionType loc _ tm) = Just loc
+getErrorLoc (NotFunctionType loc _ _) = Just loc
-getErrorLoc (RewriteNoChange loc _ tm ty) = Just loc
+getErrorLoc (RewriteNoChange loc _ _ _) = Just loc
-getErrorLoc (NotRewriteRule loc _ ty) = Just loc
+getErrorLoc (NotRewriteRule loc _ _) = Just loc
-getErrorLoc (CaseCompile loc y z) = Just loc
+getErrorLoc (CaseCompile loc _ _) = Just loc
-getErrorLoc (MatchTooSpecific loc y tm) = Just loc
+getErrorLoc (MatchTooSpecific loc _ _) = Just loc
-getErrorLoc (BadDotPattern loc _ y tm z) = Just loc
+getErrorLoc (BadDotPattern loc _ _ _ _) = Just loc
-getErrorLoc (BadImplicit loc y) = Just loc
+getErrorLoc (BadImplicit loc _) = Just loc
-getErrorLoc (BadRunElab loc _ tm) = Just loc
+getErrorLoc (BadRunElab loc _ _) = Just loc
-getErrorLoc (GenericMsg loc y) = Just loc
+getErrorLoc (GenericMsg loc _) = Just loc
-getErrorLoc (TTCError x) = Nothing
+getErrorLoc (TTCError _) = Nothing
-getErrorLoc (FileErr x y) = Nothing
+getErrorLoc (FileErr _ _) = Nothing
-getErrorLoc (ParseFail loc x) = Just loc
+getErrorLoc (ParseFail loc _) = Just loc
-getErrorLoc (ModuleNotFound loc xs) = Just loc
+getErrorLoc (ModuleNotFound loc _) = Just loc
-getErrorLoc (CyclicImports xs) = Nothing
+getErrorLoc (CyclicImports _) = Nothing
 getErrorLoc ForceNeeded = Nothing
-getErrorLoc (InternalError x) = Nothing
+getErrorLoc (InternalError _) = Nothing
-getErrorLoc (InType x y err) = getErrorLoc err
+getErrorLoc (InType _ _ err) = getErrorLoc err
-getErrorLoc (InCon x y err) = getErrorLoc err
+getErrorLoc (InCon _ _ err) = getErrorLoc err
-getErrorLoc (InLHS x y err) = getErrorLoc err
+getErrorLoc (InLHS _ _ err) = getErrorLoc err
-getErrorLoc (InRHS x y err) = getErrorLoc err
+getErrorLoc (InRHS _ _ err) = getErrorLoc err
 
 -- Core is a wrapper around IO that is specialised for efficiency.
 export

src/Core/Directory.idr

@@ -81,7 +81,7 @@ nsToPath loc ns
     = do d <- getDirs
          let fnameBase = showSep (cast sep) (reverse ns)
          let fs = map (\p => p ++ cast sep ++ fnameBase ++ ".ttc")
-                      (build_dir d :: extra_dirs d)
+                      ((build_dir d ++ cast sep ++ "ttc") :: extra_dirs d)
          Just f <- firstAvailable fs
             | Nothing => pure (Left (ModuleNotFound loc ns))
          pure (Right f)
@@ -151,7 +151,7 @@ makeBuildDirectory ns
                           [] => []
                           (n :: ns) => ns -- first item is file name
          let fname = showSep (cast sep) (reverse ndirs)
-         Right _ <- coreLift $ mkdirs (build_dir d :: reverse ndirs)
+         Right _ <- coreLift $ mkdirs (build_dir d :: "ttc" :: reverse ndirs)
             | Left err => throw (FileErr (bdir ++ cast sep ++ fname) err)
          pure ()
 
@@ -167,7 +167,7 @@ getTTCFileName inp ext
          let ns = pathToNS (working_dir d) inp
          let fname = showSep (cast sep) (reverse ns) ++ ext
          let bdir = build_dir d
-         pure $ bdir ++ cast sep ++ fname
+         pure $ bdir ++ cast sep ++ "ttc" ++ cast sep ++ fname
 
 -- Given a root executable name, return the name in the build directory
 export

src/Core/Env.idr

@@ -15,7 +15,7 @@ extend x = (::) {x}
 export
 length : Env tm xs -> Nat
 length [] = 0
-length (x :: xs) = S (length xs)
+length (_ :: xs) = S (length xs)
 
 public export
 data IsDefined : Name -> List Name -> Type where
@@ -118,11 +118,6 @@ letToLam (Let c val ty :: env) = Lam c Explicit ty :: letToLam env
 letToLam (b :: env) = b :: letToLam env
 
 mutual
-  dropS : List Nat -> List Nat
-  dropS [] = []
-  dropS (Z :: xs) = dropS xs
-  dropS (S p :: xs) = p :: dropS xs
-
 	-- Quicker, if less safe, to store variables as a Nat, for quick comparison
   findUsed : Env Term vars -> List Nat -> Term vars -> List Nat
   findUsed env used (Local fc r idx p) 
@@ -145,6 +140,11 @@ mutual
           dropS (findUsed (b :: env)
                           (map S (findUsedInBinder env used b))
                           tm)
+    where 
+      dropS : List Nat -> List Nat
+      dropS [] = []
+      dropS (Z :: xs) = dropS xs
+      dropS (S p :: xs) = p :: dropS xs
   findUsed env used (App fc fn arg) 
       = findUsed env (findUsed env used fn) arg
   findUsed env used (As fc a p) 

src/Core/InitPrimitives.idr

@@ -17,5 +17,4 @@ addPrim p
 export
 addPrimitives : {auto c : Ref Ctxt Defs} -> Core ()
 addPrimitives 
-    = do traverse addPrim allPrimitives
+    = traverse_ addPrim allPrimitives
-         pure ()

src/Core/Name.idr

@@ -36,9 +36,9 @@ nameRoot (UN n) = n
 nameRoot (MN n _) = n
 nameRoot (PV n _) = nameRoot n
 nameRoot (DN _ n) = nameRoot n
-nameRoot (Nested n inner) = nameRoot inner
+nameRoot (Nested _ inner) = nameRoot inner
-nameRoot (CaseBlock n inner) = "$" ++ show n
+nameRoot (CaseBlock n _) = "$" ++ show n
-nameRoot (WithBlock n inner) = "$" ++ show n
+nameRoot (WithBlock n _) = "$" ++ show n
 nameRoot (Resolved i) = "$" ++ show i
 
 --- Drop a namespace from a name

src/Core/TT.idr

@@ -407,16 +407,16 @@ data Term : List Name -> Type where
 
 export
 getLoc : Term vars -> FC
-getLoc (Local fc x idx y) = fc
+getLoc (Local fc _ _ _) = fc
-getLoc (Ref fc x name) = fc
+getLoc (Ref fc _ _) = fc
-getLoc (Meta fc x y xs) = fc
+getLoc (Meta fc _ _ _) = fc
-getLoc (Bind fc x b scope) = fc
+getLoc (Bind fc _ _ _) = fc
-getLoc (App fc fn arg) = fc
+getLoc (App fc _ _) = fc
-getLoc (As fc x y) = fc
+getLoc (As fc _ _) = fc
-getLoc (TDelayed fc x y) = fc
+getLoc (TDelayed fc _ _) = fc
-getLoc (TDelay fc x t y) = fc
+getLoc (TDelay fc _ _ _) = fc
-getLoc (TForce fc x) = fc
+getLoc (TForce fc _) = fc
-getLoc (PrimVal fc c) = fc
+getLoc (PrimVal fc _) = fc
 getLoc (Erased fc) = fc
 getLoc (TType fc) = fc
 

src/Core/TTC.idr

@@ -637,11 +637,37 @@ mutual
         = do c <- fromBuf b; sc <- fromBuf b
              pure (MkConstAlt c sc)
 
+export
+TTC CFType where
+  toBuf b CFUnit = tag 0
+  toBuf b CFInt = tag 1
+  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
+      = case !getTag of
+             0 => pure CFUnit
+             1 => pure CFInt
+             2 => pure CFString
+             3 => pure CFDouble
+             4 => pure CFChar
+             5 => pure CFPtr
+             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 (MkError cexpr) = do tag 2; toBuf b cexpr
+  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
@@ -649,7 +675,9 @@ export
                      pure (MkFun args cexpr)
              1 => do t <- fromBuf b; arity <- fromBuf b
                      pure (MkCon t arity)
-               2 => do cexpr <- fromBuf b
+             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"
 
@@ -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/CommandLine.idr

@@ -52,7 +52,7 @@ data CLOpt
    ||| Whether or not to run in IdeMode (easily parsable for other tools)
   IdeMode |
    ||| Whether or not to run IdeMode (using a socket instead of stdin/stdout)
-  IdeModeSocket |
+  IdeModeSocket String |
    ||| Run as a checker for the core language TTImp
   Yaffle String |
   Timing |
@@ -87,8 +87,11 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
            MkOpt ["--ide-mode"] [] [IdeMode]
               (Just "Run the REPL with machine-readable syntax"),
 
-           MkOpt ["--ide-mode-socket"] [] [IdeModeSocket]
+           MkOpt ["--ide-mode-socket"] [] [IdeModeSocket "localhost:38398"]
-              (Just "Run the ide socket mode"),
+              (Just "Run the ide socket mode on default host and port (localhost:38398"),
+
+           MkOpt ["--ide-mode-socket-with"] ["host:port"] (\hp => [IdeModeSocket hp])
+              (Just "Run the ide socket mode on given host and port"),
 
            MkOpt ["--prefix"] [] [ShowPrefix]
               (Just "Show installation prefix"),
@@ -182,3 +185,19 @@ getCmdOpts : IO (Either String (List CLOpt))
 getCmdOpts = do (_ :: opts) <- getArgs
                     | pure (Left "Invalid command line")
                 pure $ getOpts opts
+
+portPart : String -> Maybe String
+portPart p with (not $ p == "") proof prf
+  portPart p | False  = Nothing
+  portPart p | True = Just $ strTail' p (sym prf)
+
+||| Extract the host and port to bind the IDE socket to
+public export
+ideSocketModeHostPort : List CLOpt -> (String, Int)
+ideSocketModeHostPort []  = ("localhost", 38398)
+ideSocketModeHostPort (IdeModeSocket hp :: _) =
+  let (h, p) = Strings.break (== ':') hp
+      port = fromMaybe 38398 (portPart p >>= parsePositive)
+      host = if h == "" then "localhost" else h
+  in (host, port)
+ideSocketModeHostPort (_ :: rest) = ideSocketModeHostPort rest

src/Idris/Desugar.idr

@@ -464,18 +464,18 @@ mutual
       = Just (PNamespace fc ns (mapMaybe (getDecl p) ds))
 
   getDecl AsType d@(PClaim _ _ _ _ _) = Just d
-  getDecl AsType (PData fc vis (MkPData dfc tyn tyc opts cons))
+  getDecl AsType (PData fc vis (MkPData dfc tyn tyc _ _))
       = Just (PData fc vis (MkPLater dfc tyn tyc))
-  getDecl AsType d@(PInterface fc vis cons n ps det cname ds) = Just d
+  getDecl AsType d@(PInterface _ _ _ _ _ _ _ _) = Just d
-  getDecl AsType d@(PRecord fc vis n ps con fs) = Just d
+  getDecl AsType d@(PRecord _ _ _ _ _ _) = Just d
   getDecl AsType d@(PFixity _ _ _ _) = Just d
   getDecl AsType d@(PDirective _ _) = Just d
   getDecl AsType d = Nothing
 
   getDecl AsDef (PClaim _ _ _ _ _) = Nothing
-  getDecl AsDef d@(PData fc vis (MkPLater dfc tyn tyc)) = Just d
+  getDecl AsDef d@(PData _ _ (MkPLater _ _ _)) = Just d
-  getDecl AsDef (PInterface fc vis cons n ps det cname ds) = Nothing
+  getDecl AsDef (PInterface _ _ _ _ _ _ _ _) = Nothing
-  getDecl AsDef (PRecord fc vis n ps con fs) = Nothing
+  getDecl AsDef (PRecord _ _ _ _ _ _) = Nothing
   getDecl AsDef (PFixity _ _ _ _) = Nothing
   getDecl AsDef (PDirective _ _) = Nothing
   getDecl AsDef d = Just d
@@ -504,8 +504,8 @@ mutual
     where
       getFn : RawImp -> Core Name
       getFn (IVar _ n) = pure n
-      getFn (IApp _ f a) = getFn f
+      getFn (IApp _ f _) = getFn f
-      getFn (IImplicitApp _ f _ a) = getFn f
+      getFn (IImplicitApp _ f _ _) = getFn f
       getFn tm = throw (InternalError (show tm ++ " is not a function application"))
 
       toIDef : ImpClause -> Core ImpDecl
@@ -559,7 +559,7 @@ mutual
       -- is a bit of a hack, but it's necessary to build parent constraint
       -- chasing functions correctly
       pairToCons : PTerm -> List PTerm
-      pairToCons (PPair fc l r) = pairToCons l ++ pairToCons r
+      pairToCons (PPair _ l r) = pairToCons l ++ pairToCons r
       pairToCons t = [t]
 
       expandConstraint : (Maybe Name, PTerm) -> List (Maybe Name, PTerm)

src/Idris/IDEMode/Client.idr

@@ -0,0 +1,143 @@
+module Idris.IDEMode.Client
+
+import Data.Primitives.Views
+import System
+import Idris.IDEMode.Commands
+import Idris.IDEMode.Parser
+import Idris.Socket
+import Idris.Syntax
+import Idris.REPL
+import Idris.Socket.Data
+import Idris.IDEMode.REPL
+import Parser.Support
+
+hexDigit : Int -> Char
+hexDigit 0 = '0'
+hexDigit 1 = '1'
+hexDigit 2 = '2'
+hexDigit 3 = '3'
+hexDigit 4 = '4'
+hexDigit 5 = '5'
+hexDigit 6 = '6'
+hexDigit 7 = '7'
+hexDigit 8 = '8'
+hexDigit 9 = '9'
+hexDigit 10 = 'a'
+hexDigit 11 = 'b'
+hexDigit 12 = 'c'
+hexDigit 13 = 'd'
+hexDigit 14 = 'e'
+hexDigit 15 = 'f'
+
+||| Convert a positive integer into a list of (lower case) hexadecimal characters
+asHex : Int -> String
+asHex n = pack $ asHex' n []
+  where
+    asHex' : Int -> List Char -> List Char
+    asHex' 0 hex = hex
+    asHex' n hex with (n `divides` 16)
+      asHex' (16 * div + rem) hex | DivBy {div} {rem} _ = asHex' div (hexDigit rem :: hex)
+
+connectTo : String -> Int -> IO (Either String Socket)
+connectTo host port = do
+  osock <- socket AF_INET Stream 0
+  case osock of
+    Left fail => do
+      pure $ Left ("Failed to open client socket " ++ show fail)
+    Right sock => do
+      res <- connect sock (Hostname host) port
+      if res /= 0
+      then pure $ Left ("Failed to connect to :" ++ host ++ ":" ++ show port ++", " ++ show res)
+      else pure (Right sock)
+
+||| Runs an ide-mode client to execute one command against a given server
+serialize : IDECommand -> Maybe String
+serialize cmd =
+  let scmd = show $ SExpList [ toSExp cmd, toSExp 1 ]
+      hexLen = asHex $ cast $ Strings.length scmd
+      len = case isLTE (length hexLen) 6 of
+                 (Yes _) => Just $ cast (replicate (6 - length hexLen) '0') ++  hexLen
+                 (No  _) => Nothing
+  in (++) <$> len <*> Just scmd
+
+
+readOutput : Socket -> IO (Either String  SExp)
+readOutput sock = do
+  Right (len, _) <- recv sock 6 | Left err => pure (Left $ "failed to read from socket, error: " ++ show err)
+  case toHex 1 (reverse $ cast len) of
+    Nothing => pure $ Left ("expected a length in six-digits hexadecimal, got " ++ len)
+    Just num => do
+      Right (msg, _) <- recv sock num | Left err => pure (Left $ "failed to read from socket, error: " ++ show err)
+      pure $ either (Left . show) Right $ parseSExp msg
+
+data IDEResult : Type where
+  IDEReturn : List SExp -> IDEResult
+  NetworkError : String -> IDEResult
+  InputError : String -> IDEResult
+  OutputError : String -> IDEResult
+
+implementation Show IDEResult where
+  show (IDEReturn exprs) = unlines $ map show exprs
+  show (NetworkError reason) = reason
+  show (InputError reason) = reason
+  show (OutputError reason) = reason
+
+
+readResult: Socket -> List SExp -> IO IDEResult
+readResult sock outputs = do
+  Right output <- readOutput sock | Left err => pure (OutputError err)
+  case output of
+    SExpList (SymbolAtom "return" :: rest) => pure (IDEReturn (SExpList rest :: outputs))
+    res => do
+      readResult sock (res :: outputs)
+
+execute : Socket -> IDECommand -> IO IDEResult
+execute cnx command = do
+      let cmdString = serialize command
+      case cmdString of
+        Just cmd => do
+          Right sent <- send cnx cmd
+            | Left err => pure (NetworkError ("Failed to send command, error: " ++ show err))
+          readResult cnx []
+        Nothing => pure $ InputError "Command is too long"
+
+connect : String -> Int -> IO Socket
+connect host port = do
+  Right sock <- connectTo host port
+    | Left fail => do
+      putStrLn $ "fail to connect to " ++ host ++ ":" ++ show port ++", error: " ++ fail
+      exit 1
+  pure sock
+
+makeIDECommand : REPLCmd -> Either String IDECommand
+makeIDECommand (Eval term)            = Right $ Interpret (show term)
+makeIDECommand (Check term)           = Right $ TypeOf (show term) Nothing
+makeIDECommand (Load file)            = Right $ LoadFile file Nothing
+makeIDECommand (Editing (TypeAt line col name)) = Right $ TypeOf (show name) (Just (cast line, cast col))
+makeIDECommand other                  = Left "Don't know how to interpret command"
+
+parseCommand : String -> Either String IDECommand
+parseCommand = either (Left . show) makeIDECommand . parseRepl
+
+repl : Socket -> IO ()
+repl cnx
+    = do putStr prompt
+         Right input <- map parseCommand getLine
+           | Left err => do
+                  putStrLn err
+                  repl cnx
+         end <- fEOF stdin
+         if end
+            then putStrLn "Bye!"
+            else do
+              result <- execute cnx input
+              putStrLn $ show result
+              repl cnx
+
+  where
+    prompt : String
+    prompt = "λ> "
+
+export
+client : String -> Int -> IO ()
+client host port = connect host port  >>= repl

src/Idris/IDEMode/Commands.idr

@@ -125,6 +125,10 @@ public export
 interface SExpable a where
   toSExp : a -> SExp
 
+export
+SExpable IDECommand where
+  toSExp = putIDECommand
+
 export
 SExpable SExp where
   toSExp = id

src/Idris/IDEMode/REPL.idr

@@ -45,8 +45,8 @@ socketToFile (MkSocket f _ _ _) = do
   else pure (Right file)
 
 export
-initIDESocketFile : Int -> IO (Either String File)
+initIDESocketFile : String -> Int -> IO (Either String File)
-initIDESocketFile p = do
+initIDESocketFile h p = do
   osock <- socket AF_INET Stream 0
   case osock of
     Left fail => do
@@ -54,7 +54,7 @@ initIDESocketFile p = do
       putStrLn "Failed to open socket"
       exit 1
     Right sock => do
-      res <- bind sock (Just (Hostname "localhost")) p
+      res <- bind sock (Just (Hostname h)) p
       if res /= 0
       then
         pure (Left ("Failed to bind socket with error: " ++ show res))
@@ -118,11 +118,13 @@ hex 'e' = Just 14
 hex 'f' = Just 15
 hex _ = Nothing
 
+export
 toHex : Int -> List Char -> Maybe Int
 toHex _ [] = Just 0
 toHex m (d :: ds)
     = pure $ !(hex (toLower d)) * m + !(toHex (m*16) ds)
 
+
 -- Read 6 characters. If they're a hex number, read that many characters.
 -- Otherwise, just read to newline
 getInput : File -> IO String
@@ -257,4 +259,3 @@ replIDE
               IDEMode _ inf outf => do
                 send outf (version 2 0)
                 loop
-

src/Idris/Main.idr

@@ -144,7 +144,8 @@ stMain opts
                        setOutput (IDEMode 0 stdin stdout)
                        replIDE {c} {u} {m}
                      else do
-                       f <- coreLift $ initIDESocketFile 38398
+                       let (host, port) = ideSocketModeHostPort opts
+                       f <- coreLift $ initIDESocketFile host port
                        case f of
                          Left err => do
                            coreLift $ putStrLn err

src/Idris/Package.idr

@@ -234,9 +234,9 @@ installFrom : {auto c : Ref Ctxt Defs} ->
               String -> String -> String -> List String -> Core ()
 installFrom _ _ _ [] = pure ()
 installFrom pname builddir destdir ns@(m :: dns)
-    = do let ttcfile = showSep "/" (reverse ns)
+    = do let ttcfile = showSep dirSep (reverse ns)
-         let ttcPath = builddir ++ dirSep ++ ttcfile ++ ".ttc"
+         let ttcPath = builddir ++ dirSep ++ "ttc" ++ dirSep ++ ttcfile ++ ".ttc"
-         let destPath = destdir ++ dirSep ++ showSep "/" (reverse dns)
+         let destPath = destdir ++ dirSep ++ showSep dirSep (reverse dns)
          let destFile = destdir ++ dirSep ++ ttcfile ++ ".ttc"
          Right _ <- coreLift $ mkdirs (reverse dns)
              | Left err => throw (FileErr pname err)

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/Idris/REPLCommon.idr

@@ -87,7 +87,7 @@ updateErrorLine : {auto o : Ref ROpts REPLOpts} ->
 updateErrorLine []
     = do opts <- get ROpts
          put ROpts (record { errorLine = Nothing } opts)
-updateErrorLine (e :: es)
+updateErrorLine (e :: _)
     = do opts <- get ROpts
          put ROpts (record { errorLine = map getFCLine (getErrorLoc e) } opts)
 

src/Idris/SetOptions.idr

@@ -81,6 +81,5 @@ ideMode (_ :: xs) = ideMode xs
 export
 ideModeSocket : List CLOpt -> Bool
 ideModeSocket [] = False
-ideModeSocket (IdeModeSocket :: _) = True
+ideModeSocket (IdeModeSocket _ :: _) = True
 ideModeSocket (_ :: xs) = ideModeSocket xs
-

src/Parser/Lexer.idr

@@ -30,8 +30,8 @@ Show Token where
   show (Symbol x) = "symbol " ++ x
   show (Keyword x) = x
   show (Unrecognised x) = "Unrecognised " ++ x
-  show (Comment x) = "comment"
+  show (Comment _) = "comment"
-  show (DocComment x) = "doc comment"
+  show (DocComment _) = "doc comment"
   show (CGDirective x) = "CGDirective " ++ x
   show EndInput = "end of input"
 

src/TTImp/BindImplicits.idr

@@ -10,9 +10,6 @@ import Control.Monad.State
 
 %default covering
 
-getUnique : List String -> String -> String
-getUnique xs x = if x `elem` xs then getUnique xs (x ++ "'") else x
-
 -- Rename the IBindVars in a term. Anything which appears in the list 'renames'
 -- should be renamed, to something which is *not* in the list 'used'
 export

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

src/TTImp/Utils.idr

@@ -10,6 +10,7 @@ lowerFirst : String -> Bool
 lowerFirst "" = False
 lowerFirst str = assert_total (isLower (strHead str))
 
+export
 getUnique : List String -> String -> String
 getUnique xs x = if x `elem` xs then getUnique xs (x ++ "'") else x
 

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

tests/Main.idr

@@ -66,7 +66,7 @@ chezTests
 
 ideModeTests : List String
 ideModeTests
-  =  [ "ideMode002" ]
+  =  [ "ideMode001", "ideMode002" ]
 
 chdir : String -> IO Bool
 chdir dir

tests/ideMode/ideMode001/LocType.idr

@@ -0,0 +1,7 @@
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+append : Vect n a -> Vect m a -> Vect (n + m) a
+append [] ys = ys
+append (x :: xs) ys = x :: append xs ys

tests/ideMode/ideMode001/expected

@@ -0,0 +1,4 @@
+000018(:protocol-version 2 0)
+000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
+00002a(:return (:ok "Loaded LocType.idr" ()) 1)
+Alas the file is done, aborting

tests/ideMode/ideMode001/input

@@ -0,0 +1 @@
+00001e((:load-file "LocType.idr") 1)

tests/ideMode/ideMode001/run

@@ -0,0 +1,3 @@
+$1 --ide-mode < input
+
+rm -rf build

tests/ttimp/basic001/run

@@ -1,4 +1,4 @@
 $1 --yaffle Interp.yaff < input
-$1 --yaffle build/Interp.ttc < input
+$1 --yaffle build/ttc/Interp.ttc < input
 
 rm -rf build

tests/ttimp/basic003/run

@@ -1,4 +1,4 @@
 $1 --yaffle Hole.yaff < input
-$1 --yaffle build/Hole.ttc < input
+$1 --yaffle build/ttc/Hole.ttc < input
 
 rm -rf build

tests/ttimp/lazy001/run

@@ -1,5 +1,5 @@
 $1 --yaffle Lazy.yaff < input
 $1 --yaffle LazyInf.yaff < input
-$1 --yaffle build/LazyInf.ttc < input
+$1 --yaffle build/ttc/LazyInf.ttc < input
 
 rm -rf build

tests/ttimp/record001/run

@@ -1,4 +1,4 @@
 $1 --yaffle Record.yaff < input
-$1 --yaffle build/Record.ttc < input
+$1 --yaffle build/ttc/Record.ttc < input
 
 rm -rf build

tests/ttimp/search002/run

@@ -1,4 +1,4 @@
 $1 --yaffle Auto.yaff < input
-$1 --yaffle build/Auto.ttc < input
+$1 --yaffle build/ttc/Auto.ttc < input
 
 rm -rf build

tests/ttimp/search003/run

@@ -1,4 +1,4 @@
 $1 --yaffle FakeTC.yaff < input
-$1 --yaffle build/FakeTC.ttc < input
+$1 --yaffle build/ttc/FakeTC.ttc < input
 
 rm -rf build

tests/ttimp/search004/run

@@ -1,4 +1,4 @@
 $1 --yaffle Functor.yaff < input
-$1 --yaffle build/Functor.ttc < input
+$1 --yaffle build/ttc/Functor.ttc < input
 
 rm -rf build