Export control

CPP.idr

module CPP

import System

%language ElabReflection
%language TypeProviders

export
testFn : Int -> String
testFn x = "testFn: " ++ show x

mkName : IO (Provider String)
mkName = do
  Right v <- readFile "version.txt" | Left e => pure (Error $ show e)
  --Just v <- getEnv "PATH" | _ => pure (Error "ERR")
  pure (Provide $ "testFn_v" ++ (trim v))

%provide (fnName : String) with mkName

mkFnName : Elab ()
mkFnName = do
  fill (RConstant fnName)
  solve

exports : FFI_Export FFI_C "exports.h" []
exports = Fun testFn (%runElab mkFnName) $ End