feat: add type conversions

Extism/Bindings.lean

@@ -1,3 +1,8 @@
+import Lean.Data.Json
+import Lean.Data.Json.Basic
+import Lean.Data.Json.Parser
+import Lean.Data.Json.Printer
+
 @[extern "l_extism_version"]
 opaque version : IO String
 
@@ -50,6 +55,32 @@ private opaque functionNew : String -> String -> Array UInt8 -> Array UInt8 -> (
 class PluginInput (a: Type) where
   toPluginInput: a -> ByteArray
 
+class ToBytes (a: Type) where
+  toBytes: a -> ByteArray
+
+instance : ToBytes ByteArray where
+  toBytes x := x
+
+instance : ToBytes String where
+  toBytes := String.toUTF8
+
+instance [Lean.ToJson a] : ToBytes a where
+  toBytes x := (Lean.Json.compress (Lean.ToJson.toJson x)).toUTF8
+
+class FromBytes (a: Type) where
+  fromBytes?: ByteArray -> Except String a
+
+instance : FromBytes ByteArray where
+  fromBytes? x := Except.ok x
+
+instance : FromBytes String where
+  fromBytes? x := Except.ok (String.fromUTF8Unchecked x)
+
+instance [Lean.FromJson a] : FromBytes a where
+  fromBytes? x := do
+    let j := <- Lean.Json.parse (String.fromUTF8Unchecked x)
+    Lean.FromJson.fromJson? j
+
 instance : PluginInput ByteArray where
   toPluginInput x := x
 
@@ -68,17 +99,16 @@ structure Plugin where
 
 def Plugin.new [PluginInput a] (data: a) (functions: Array Function) (wasi : Bool) : IO Plugin := do
   let input := PluginInput.toPluginInput data
-  let s := String.fromUTF8Unchecked input
-  IO.println s!"Input {s}"
   let x := <- newPluginRef input functions wasi
   return (Plugin.mk x #[])
 
 def Plugin.fromFile (path: System.FilePath) (functions: Array Function) (wasi : Bool) : IO Plugin := do
   let x := <- newPluginFromFile path functions wasi
   return (Plugin.mk x #[])
 
-def Plugin.call (plugin: Plugin) (funcName: String) (data: ByteArray) : IO ByteArray :=
-  pluginRefCall plugin.inner funcName data
+def Plugin.call [ToBytes a] [FromBytes b] (plugin: Plugin) (funcName: String) (data: a) : IO b := do
+  let res := <- pluginRefCall plugin.inner funcName (ToBytes.toBytes data)
+  IO.ofExcept (FromBytes.fromBytes? res)
 
 def Plugin.pipe (plugin: Plugin) (names: List String) (data: ByteArray) : IO ByteArray :=
   List.foldlM (fun acc x =>

Extism/Manifest.lean

@@ -43,7 +43,10 @@ instance : Lean.ToJson WasmUrl where
     let m := [
       ("url", Lean.ToJson.toJson x.url)
     ]
-    let m := addIfSome m "headers" x.headers 
+    let h := match x.headers with
+      | Option.some x => List.map (fun (k, v) => (k, Lean.toJson v)) x |> Lean.Json.mkObj |> Option.some
+      | Option.none => Option.none
+    let m := addIfSome m "headers" h
     let m := addIfSome m "method" x.method
     let m := addIfSome m "name" x.name
     let m := addIfSome m "hash" x.hash
@@ -78,25 +81,39 @@ structure Manifest: Type where
   allowedHosts: Option (Array String)
   allowedPaths: Option (List (String × String))
   memory: Option Memory
+  config: Option (List (String × String))
 deriving Lean.FromJson, Inhabited, Repr
 
 instance : Lean.ToJson Manifest where
   toJson x := 
     let m := [
       ("wasm", Lean.ToJson.toJson x.wasm)
     ]
+    let config := match x.config with
+      | Option.some x => List.map (fun (k, v) => (k, Lean.toJson v)) x |> Lean.Json.mkObj |> Option.some
+      | Option.none => Option.none
+    let paths := match x.allowedPaths with
+      | Option.some x => List.map (fun (k, v) => (k, Lean.toJson v)) x |> Lean.Json.mkObj |> Option.some
+      | Option.none => Option.none
     let m := addIfSome m "memory" x.memory
     let m := addIfSome m "allowed_hosts" x.allowedHosts
-    let m := addIfSome m "allowed_paths" x.allowedPaths
+    let m := addIfSome m "allowed_paths" paths
+    let m := addIfSome m "config" config
     Lean.Json.mkObj m
 
 
 def Manifest.new (wasm: Array Wasm) : Manifest :=
-  Manifest.mk wasm none none none
+  Manifest.mk wasm none none none none
 
-def Manifest.withMemoryMax (m: Manifest) (max: Int) : Manifest :=
+def Manifest.withMemoryMax (max: Int) (m: Manifest) : Manifest :=
   {m with memory := some (Memory.mk max)}
 
+def Manifest.withConfig (k: String) (v: String) (m: Manifest) :=
+  let c := match m.config with
+    | Option.none => []
+    | Option.some x => x
+  {m with config := (k, v) :: c}
+
 def Manifest.json (m: Manifest) : String :=
   let x := Lean.ToJson.toJson m
   Lean.Json.pretty x

Main.lean

@@ -9,12 +9,21 @@ def helloWorld (curr: Current) : IO Unit := do
   IO.println "Hello world!!!"
   IO.println "Hello world!!!"
 
-def main : IO Unit := do
-  let m := Manifest.new #[Wasm.file "code-functions.wasm"]
-  let s := m.json
-  IO.println s!"{s}"
+def hostFunction: IO Unit := do
+  let m := Manifest.new #[Wasm.file "wasm/code-functions.wasm"] |> Manifest.withConfig "vowels" "aeiouyAEIOUY"
   let f := <- Function.new "hello_world" #[ValType.i64] #[ValType.i64] helloWorld
   let plugin := <- Plugin.new m #[f] True
   let input := String.toUTF8 "this is a test"
   let res := <- String.fromUTF8Unchecked <$> plugin.call "count_vowels" input
   IO.println s!"{res}"
+
+def fromUrl : IO Unit := do
+  let url := "https://github.com/extism/plugins/releases/latest/download/count_vowels.wasm"
+  let m := Manifest.new #[Wasm.url url]
+  let plugin := <- Plugin.new m #[] True
+  let res: String := <- Plugin.call plugin "count_vowels" "Hello, world!"
+  IO.println s!"{res}"
+
+def main : IO Unit := do
+  fromUrl
+  hostFunction

README.md

@@ -2,3 +2,61 @@
 
 This repo contains the [Lean 4](https://github.com/leanprover/lean4) package for integrating with [Extism](https://github.com/extism/extism)
 
+## Building
+
+The Extism shared object is required for these bindings to work, see our [https://extism.org/docs/install/](installation instructions).
+
+From the root of the repository run:
+
+```sh
+lake build
+```
+
+To run the tests:
+
+```sh
+lake exe test
+```
+
+## Getting started
+
+Add the following to your `lakefile.lean`:
+
+```
+require extism from git "https://github.com/extism/lean4-sdk" @ "main"
+```
+
+### Loading a Plug-in
+
+
+The primary concept in Extism is the [plug-in](https://extism.org/docs/concepts/plug-in). A plug-in is a code module stored in a `.wasm` file.
+
+Plug-in code can come from a file on disk, object storage or any number of places. Since you may not have one handy, let's load a demo plug-in from the web. Let's
+start by creating a main function that loads a plug-in:
+
+```
+import Extism
+
+def main : IO Unit := do
+  let url := "https://github.com/extism/plugins/releases/latest/download/count_vowels.wasm"
+  let m := Manifest.new #[Wasm.url url]
+  let plugin := <- Plugin.new m #[] True
+```
+
+### Calling A Plug-in's Exports
+
+This plug-in was written in Rust and it does one thing, it counts vowels in a string. It exposes one "export" function: `count_vowels`. We can call exports using `Plugin::call`.
+Let's add code to call `count_vowels` to our main func:
+
+```
+import Extism
+
+def main : IO Unit := do
+  let url := "https://github.com/extism/plugins/releases/latest/download/count_vowels.wasm"
+  let m := Manifest.new #[Wasm.url url]
+  let plugin := <- Plugin.new m #[] True
+  let res: String := <- Plugin.call plugin "count_vowels" "Hello, world!"
+  IO.println s!"{res}"
+  // => {"count":3,"total":3,"vowels":"aeiouAEIOU"}
+```
+