Add %foreign_impl pragma for augmenting ffi functions

CHANGELOG_NEXT.md

@@ -36,6 +36,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 * Elaborator scripts were made to be able to access the visibility modifier of a
   definition, via `getVis`.
 
+* The language now has a ``%foreign_impl`` pragma to add additional languages
+  to a ``%foreign`` function.
+
 ### Compiler changes
 
 * The compiler now differentiates between "package search path" and "package

docs/source/ffi/ffi.rst

@@ -37,6 +37,15 @@ be ``#include``'d in the C code generated by the Idris2 compiler. For instance:
     %foreign "C:idris2_resetRawMode, libidris2_support, idris_support.h"
     idris2_resetRawMode : (1 x : %World) -> IORes ()
 
+FFI declarations can be extended in another file with the ``%foreign_impl`` pragma.
+This pragma can be used to fill in cases not handled in the standard library when
+using third party backends. In the case of multiple declarations for a given backend
+the one from the last module loaded is used.
+
+.. code-block:: idris
+
+    %foreign_impl Prelude.IO.prim__fork "javascript:lambda:(proc) => { throw new Error() }"
+
 Scheme Details
 ---------------
 

docs/source/reference/pragmas.rst

@@ -281,6 +281,20 @@ Specialise a function according to a list of arguments.
 Declare a foreign function.  It is followed by an indented block of expressions
 that evaluate to strings. See :ref:`ffi-overview` for more details.
 
+
+``%foreign_impl``
+--------------------
+
+Adds an implementation to an existing ``%foreign`` in another file. This pragma can
+be used to fill in an implementation for another backend without changing the original
+file. In the case of multiple declarations for a given backend, the backend will choose
+the one from the most recently loaded module.
+
+.. code-block:: idris
+
+   %foreign_impl Prelude.IO.prim__fork "javascript:lambda:(proc) => { throw new Error() }"
+
+
 ``%export``
 --------------------
 

src/Compiler/Common.idr

@@ -242,6 +242,16 @@ nonErased n
               | Nothing => pure True
          pure (multiplicity gdef /= erased)
 
+export
+addForeignImpl : {auto c : Ref Ctxt Defs} ->
+             Name -> Core ()
+addForeignImpl n
+    = do defs <- get Ctxt
+         Just def <- lookupCtxtExact n (gamma defs)        | Nothing => pure ()
+         let Just (MkForeign cs atys retty) = compexpr def | _ => pure ()
+         let xs = map snd $ filter (\x => fst x == n) defs.options.foreignImpl
+         setCompiled n (MkForeign (xs ++ cs) atys retty)
+
 -- Get the names of the functions we're exporting to the given back end, and
 -- the corresponding name it will have when exported.
 getExported : String -> NameMap (List (String, String)) -> List (Name, String)
@@ -325,6 +335,7 @@ getCompileDataWith exports doLazyAnnots phase_in tm_in
 
          logTime 2 "Merge lambda" $ traverse_ mergeLamDef rcns
          logTime 2 "Fix arity" $ traverse_ fixArityDef rcns
+         logTime 2 "Fix foreign bindings" $ traverse_ addForeignImpl rcns
          compiledtm <- fixArityExp !(compileExp tm)
 
          (cseDefs, csetm) <- logTime 2 "CSE" $ cse rcns compiledtm

src/Core/Binary.idr

@@ -29,7 +29,7 @@ import public Libraries.Utils.Binary
 ||| version number if you're changing the version more than once in the same day.
 export
 ttcVersion : Int
-ttcVersion = 2024_03_29_00
+ttcVersion = 2024_06_08_00
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()
@@ -55,6 +55,7 @@ record TTCFile extra where
   pairnames : Maybe PairNames
   rewritenames : Maybe RewriteNames
   primnames : PrimNames
+  foreignImpl : List (Name, String)
   namedirectives : List (Name, List String)
   cgdirectives : List (CG, String)
   transforms : List (Name, Transform)
@@ -97,7 +98,7 @@ HasNames e => HasNames (TTCFile e) where
                       context userHoles
                       autoHints typeHints
                       imported nextVar currentNS nestedNS
-                      pairnames rewritenames primnames
+                      pairnames rewritenames primnames foreignImpl
                       namedirectives cgdirectives trans
                       fexp extra)
       = pure $ MkTTCFile version totalReq sourceHash ifaceHash iHashes incData
@@ -108,6 +109,7 @@ HasNames e => HasNames (TTCFile e) where
                          !(fullPair gam pairnames)
                          !(fullRW gam rewritenames)
                          !(fullPrim gam primnames)
+                         !(traverse fullForeign foreignImpl)
                          !(full gam namedirectives)
                          cgdirectives
                          !(full gam trans)
@@ -134,6 +136,8 @@ HasNames e => HasNames (TTCFile e) where
                         (full gam mn)
                         (full gam mdl) |]
 
+      fullForeign : (Name, String) -> Core (Name, String)
+      fullForeign (n,s) = pure $ (!(full gam n), s)
 
   -- I don't think we ever actually want to call this, because after we read
   -- from the file we're going to add them to learn what the resolved names
@@ -142,7 +146,7 @@ HasNames e => HasNames (TTCFile e) where
                       context userHoles
                       autoHints typeHints
                       imported nextVar currentNS nestedNS
-                      pairnames rewritenames primnames
+                      pairnames rewritenames primnames foreignImpl
                       namedirectives cgdirectives trans
                       fexp extra)
       = pure $ MkTTCFile version totalReq sourceHash ifaceHash iHashes incData
@@ -153,6 +157,7 @@ HasNames e => HasNames (TTCFile e) where
                          !(resolvedPair gam pairnames)
                          !(resolvedRW gam rewritenames)
                          !(resolvedPrim gam primnames)
+                         !(traverse resolvedForeign foreignImpl)
                          !(resolved gam namedirectives)
                          cgdirectives
                          !(resolved gam trans)
@@ -179,6 +184,9 @@ HasNames e => HasNames (TTCFile e) where
                             !(resolved gam mn)
                             !(resolved gam mdl)
 
+      resolvedForeign : (Name, String) -> Core (Name, String)
+      resolvedForeign (n,s) = pure $ (!(resolved gam n), s)
+
 -- NOTE: TTC files are only compatible if the version number is the same,
 -- *and* the 'annot/extra' type are the same, or there are no holes/constraints
 writeTTCFile : (HasNames extra, TTC extra) =>
@@ -205,6 +213,7 @@ writeTTCFile b file_in
            toBuf b (pairnames file)
            toBuf b (rewritenames file)
            toBuf b (primnames file)
+           toBuf b (foreignImpl file)
            toBuf b (namedirectives file)
            toBuf b (cgdirectives file)
            toBuf b (transforms file)
@@ -234,7 +243,7 @@ readTTCFile readall file as b
                                    0 (mkNamespace "") [] Nothing
                                    Nothing
                                    (MkPrimNs Nothing Nothing Nothing Nothing Nothing Nothing Nothing)
-                                   [] [] [] [] ex)
+                                   [] [] [] [] [] ex)
               else do
                  defs <- fromBuf b
                  uholes <- fromBuf b
@@ -246,6 +255,7 @@ readTTCFile readall file as b
                  pns <- fromBuf b
                  rws <- fromBuf b
                  prims <- fromBuf b
+                 foreignImpl <- fromBuf b
                  nds <- fromBuf b
                  cgds <- fromBuf b
                  trans <- fromBuf b
@@ -254,7 +264,7 @@ readTTCFile readall file as b
                                  sourceFileHash ifaceHash importHashes incData
                                  (map (replaceNS cns) defs) uholes
                                  autohs typehs imp nextv cns nns
-                                 pns rws prims nds cgds trans fexp ex)
+                                 pns rws prims foreignImpl nds cgds trans fexp ex)
   where
     -- We don't store full names in 'defs' - we remove the namespace if it's
     -- the same as the current namespace. So, this puts it back.
@@ -317,6 +327,7 @@ writeToTTC extradata sourceFileName ttcFileName
                               (pairnames (options defs))
                               (rewritenames (options defs))
                               (primnames (options defs))
+                              (foreignImpl (options defs))
                               (NameMap.toList (namedirectives defs))
                               (cgdirectives defs)
                               (saveTransforms defs)
@@ -393,6 +404,10 @@ export
 updatePrims : {auto c : Ref Ctxt Defs} -> PrimNames -> Core ()
 updatePrims p = update Ctxt { options->primnames $= updatePrimNames p }
 
+export
+updateForeignImpl : {auto c : Ref Ctxt Defs} -> List (Name, String) -> Core ()
+updateForeignImpl xs = update Ctxt { options->foreignImpl $= (xs ++) }
+
 export
 updateNameDirectives : {auto c : Ref Ctxt Defs} ->
                        List (Name, List String) -> Core ()
@@ -494,6 +509,7 @@ readFromTTC nestedns loc reexp fname modNS importAs
                     updatePair (pairnames ttc)
                     updateRewrite (rewritenames ttc)
                     updatePrims (primnames ttc)
+                    updateForeignImpl (foreignImpl ttc)
                     updateNameDirectives (reverse (namedirectives ttc))
                     updateCGDirectives (cgdirectives ttc)
                     updateTransforms (transforms ttc)

src/Core/Context.idr

@@ -2307,6 +2307,13 @@ getAutoImplicitLimit
     = do defs <- get Ctxt
          pure (autoImplicitLimit (elabDirectives (options defs)))
 
+export
+addForeignImpl : {auto c : Ref Ctxt Defs} ->
+          FC -> (fullName : Name) -> (def : String) -> Core ()
+addForeignImpl fc name def
+   = do name <- toFullNames name
+        update Ctxt { options $= addForeignImpl name def }
+
 export
 setPair : {auto c : Ref Ctxt Defs} ->
           FC -> (pairType : Name) -> (fstn : Name) -> (sndn : Name) ->

src/Core/Options.idr

@@ -197,6 +197,8 @@ record Options where
   extensions : List LangExt
   additionalCGs : List (String, CG)
   hashFn : Maybe String
+  -- fullName and definition for %foreign_impl
+  foreignImpl : List (Name, String)
 
 export
 availableCGs : Options -> List (String, CG)
@@ -256,17 +258,22 @@ defaults
          -- it to fail gracefully.
          pure $ MkOptions
            defaultDirs defaultPPrint defaultSession defaultElab Nothing Nothing
-           (MkPrimNs Nothing Nothing Nothing Nothing Nothing Nothing Nothing) [] [] Nothing
+           (MkPrimNs Nothing Nothing Nothing Nothing Nothing Nothing Nothing) [] [] Nothing []
 
 -- Reset the options which are set by source files
 export
 clearNames : Options -> Options
 clearNames = { pairnames := Nothing,
                rewritenames := Nothing,
                primnames := MkPrimNs Nothing Nothing Nothing Nothing Nothing Nothing Nothing,
+               foreignImpl := [],
                extensions := []
              }
 
+export
+addForeignImpl : (fullName : Name) -> (def : String) -> Options -> Options
+addForeignImpl fullName def = { foreignImpl $= ((fullName, def) ::) }
+
 export
 setPair : (pairType : Name) -> (fstn : Name) -> (sndn : Name) ->
           Options -> Options

src/Idris/Desugar.idr

@@ -2,6 +2,7 @@ module Idris.Desugar
 
 import Core.Context
 import Core.Context.Log
+import Core.CompileExpr
 import Core.Core
 import Core.Env
 import Core.Metadata
@@ -31,6 +32,7 @@ import Parser.Support
 
 import TTImp.BindImplicits
 import TTImp.Parser
+import TTImp.ProcessType
 import TTImp.TTImp
 import TTImp.Utils
 
@@ -1332,6 +1334,19 @@ mutual
              Overloadable n => pure [IPragma fc [] (\nest, env => setNameFlag fc n Overloadable)]
              Extension e => pure [IPragma fc [] (\nest, env => setExtension e)]
              DefaultTotality tot => pure [IPragma fc [] (\_, _ => setDefaultTotalityOption tot)]
+             ForeignImpl n cs => do
+               cs' <- traverse (desugar AnyExpr ps) cs
+               pure [IPragma fc [] (\nest, env => do
+                      defs <- get Ctxt
+                      calls <- traverse getFnString cs'
+                      [(n',_,gdef)] <- lookupCtxtName n (gamma defs)
+                        | [] => throw (UndefinedName fc n)
+                        | xs => throw (AmbiguousName fc (map fst xs))
+                      let ForeignDef arity xs = gdef.definition
+                        | _ => throw (GenericMsg fc "\{show n} is not a foreign definition")
+
+                      update Ctxt { options->foreignImpl $= (map (n',) calls ++) }
+                    )]
   desugarDecl ps (PBuiltin fc type name) = pure [IBuiltin fc type name]
 
   export

src/Idris/Parser.idr

@@ -1437,6 +1437,11 @@ directive fname indents
          n <- name
          atEnd indents
          pure (Unhide n)
+  <|> do decoratedPragma fname "foreign_impl"
+         n <- name
+         cs <- block (expr pdef fname)
+         atEnd indents
+         pure (ForeignImpl n cs)
 --   <|> do pragma "hide_export"
 --          n <- name
 --          atEnd indents

src/Idris/Syntax.idr

@@ -381,6 +381,8 @@ mutual
        AutoImplicitDepth : Nat -> Directive
        NFMetavarThreshold : Nat -> Directive
        SearchTimeout : Integer -> Directive
+       -- There is no nm on Directive
+       ForeignImpl : Name -> List PTerm -> Directive
 
   public export
   PField : Type

src/TTImp/ProcessType.idr

@@ -28,7 +28,7 @@ import Libraries.Data.StringMap
 import Libraries.Data.WithDefault
 
 %default covering
-
+export
 getFnString : {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->

tests/node/ffi001/Foreign.idr

@@ -0,0 +1,10 @@
+import Control.App
+import Control.App.Console
+
+%foreign_impl Prelude.IO.prim__fork "javascript:lambda:(proc) => { throw new Error() }"
+
+prog : (Console es) => App es ()
+prog = putStrLn "hello, world"
+
+main : IO ()
+main = run prog

tests/node/ffi001/expected

@@ -0,0 +1 @@
+hello, world

tests/node/ffi001/run

@@ -0,0 +1,2 @@
+. ../../testutils.sh
+run --cg node Foreign.idr