Idris-JVM Spigot plugin

Main.idr

module Main

import IdrisJvm.FFI
import IdrisJvm.IO
import Java.Lang

%default total


record Java a ret where
  constructor MkJava
  runJava : a -> JVM_IO ret
  
Functor (Java a) where
  map f (MkJava action) = MkJava ((map f) . action)
  
Applicative (Java a) where
  pure = MkJava . const . pure
  (<*>) (MkJava action1) (MkJava action2) =
    MkJava
      (\a => (action1 a) <*> action2 a)
      
Monad (Java a) where
  (>>=) (MkJava action) f =
    MkJava
      (\a => do
        ret <- action a
        let (MkJava action2) = f ret
        action2 a
      )
      
javaWith : a -> Java a ret -> JVM_IO ret
javaWith = flip runJava

io : JVM_IO ret -> Java a ret
io action = MkJava (const action)

withObject : a -> Java a ret -> Java b ret
withObject obj j =
  io $ javaWith obj j


CommandSender : Type
CommandSender = javaInterface "org/bukkit/command/CommandSender"

Command : Type
Command = javaClass "org/bukkit/command/Command"

getSenderName : Java CommandSender String
getSenderName =
  MkJava $ invokeInstance "getName" (CommandSender -> JVM_IO String)

sendMessage : String -> Java CommandSender ()
sendMessage =
  MkJava .
    (flip $ invokeInstance "sendMessage" (CommandSender -> String -> JVM_IO ()))


onEnable : JVM_IO ()
onEnable = putStrLn "MyPlugin enabled. Wow!"

thankSender : Java CommandSender ()
thankSender = do
  senderName <- getSenderName
  sendMessage ("Thanks for command, " ++ senderName)


onCommand : () -> CommandSender -> Command -> String -> StringArray -> JVM_IO Bool
onCommand _ sender cmd alias args = do
  javaWith sender thankSender
  pure True


partial
exports1 : FFI_Export FFI_JVM "okkero/test/MyPlugin extends org/bukkit/plugin/java/JavaPlugin" []
exports1 =
  Fun onEnable (ExportInstance "onEnable") $
  Fun onCommand (ExportInstance "onCommand")
  End


main : IO ()
main = pure ()