fix: make sure to call io result constructor in C bindings

Extism/Types.lean

@@ -24,19 +24,30 @@ instance : Extism.ToBytes ByteArray where
 instance : Extism.ToBytes String where
   toBytes := String.toUTF8
 
-instance [Lean.ToJson a] : Extism.ToBytes a where
-  toBytes x := (Lean.Json.compress (Lean.ToJson.toJson x)).toUTF8
+
+inductive Json (a: Type) where
+  | val: a -> Json a
+
+def Json.inner: Json a -> a
+  | Json.val x => x
+
+def Json.mk: a -> Json a := Json.val
+
+instance [Lean.ToJson a] : Extism.ToBytes (Json a) where
+  toBytes
+    | Json.val x => (Lean.Json.compress (Lean.ToJson.toJson x)).toUTF8
 
 instance : Extism.FromBytes ByteArray where
   fromBytes? (x: ByteArray) := Except.ok x
 
 instance : Extism.FromBytes String where
   fromBytes? x := Except.ok (String.fromUTF8Unchecked x)
 
-instance [Lean.FromJson a] : Extism.FromBytes a where
+instance [Lean.FromJson a] : Extism.FromBytes (Json a) where
   fromBytes? x := do
     let j <- Lean.Json.parse (String.fromUTF8Unchecked x)
-    Lean.FromJson.fromJson? j
+    let j <- Lean.FromJson.fromJson? j
+    Except.ok (Json.val j)
 
 instance : Extism.FromBytes UInt64 where
   fromBytes? x :=

Test.lean

@@ -2,6 +2,8 @@ import Extism
 
 open Extism
 
+--/ Example host function, takes one parameter and returns one result
+--/ In this case we are just logging the input and returning it
 def helloWorld (curr: Current) : IO Unit := do
   let s: String <- Current.param curr 0
   IO.println s!"Input: {s}"
@@ -12,6 +14,7 @@ def helloWorld (curr: Current) : IO Unit := do
   IO.println "Hello world!!!"
   IO.println "Hello world!!!"
 
+--/ Example with host functions
 def hostFunction: IO Unit := do
   let m := Manifest.new #[Wasm.file "wasm/code-functions.wasm"]
     |> Manifest.withConfig "vowels" "aeiouyAEIOUY"
@@ -20,13 +23,31 @@ def hostFunction: IO Unit := do
   let res: String <- plugin.pipe ["count_vowels", "count_vowels"] "this is a test"
   IO.println s!"Result: {res}"
 
+--/ Example loading a plugin from a URL
 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}"
 
+namespace proc
+  --/ Process status type
+  structure Status where
+    name: String
+  deriving Lean.FromJson
+
+  --/ Get name of process using /proc/self/status
+  def test : IO Unit := do
+    let m := 
+      Manifest.new #[Wasm.file "wasm/extproc.wasm"]
+      |> Manifest.allowPath "/proc" "/proc"
+    let plugin <- Plugin.new m #[] True
+    let res: Json Status <- Plugin.call plugin "status" ""
+    IO.println s!"Name: {res.inner.name}"
+end proc
+
 def main : IO Unit := do
   fromUrl
   hostFunction
+  proc.test

c/bindings.c

@@ -107,8 +107,8 @@ lean_obj_res l_extism_plugin_new(b_lean_obj_arg data, lean_obj_arg functions,
                                            nFunctions, wasi == 1, &err);
   if (plugin == NULL) {
     const char *err_s =
-        err == NULL ? "Unknown error occured in call to Extism plugin" : err;
-    __auto_type e = lean_mk_io_user_error(lean_mk_string(err_s));
+        err == NULL ? "Unknown error occured when creating Extism plugin" : err;
+    lean_obj_res e = lean_mk_io_user_error(lean_mk_string(err_s));
     if (err != NULL) {
       extism_plugin_new_error_free(err);
     }
@@ -128,8 +128,8 @@ lean_obj_res l_extism_plugin_call(b_lean_obj_arg pluginArg,
   int32_t rc = extism_plugin_call(plugin, name, dataBytes, dataLen);
   if (rc != 0) {
     const char *err = extism_plugin_error(plugin);
-    return lean_mk_io_user_error(lean_mk_string(
-        err == NULL ? "Unknown error occured in call to Extism plugin" : err));
+    return lean_io_result_mk_error(lean_mk_io_user_error(lean_mk_string(
+        err == NULL ? "Unknown error occured in call to Extism plugin" : err)));
   }
 
   size_t length = extism_plugin_output_length(plugin);
@@ -178,7 +178,8 @@ lean_obj_res l_extism_function_new(b_lean_obj_arg funcNamespace,
       extism_function_new(name, paramVals, paramsLen, resultVals, resultsLen,
                           generic_function_callback, f, (void *)lean_dec);
   if (func == NULL) {
-    return lean_mk_io_user_error(lean_mk_string("Unable to create function"));
+    return lean_io_result_mk_error(
+        lean_mk_io_user_error(lean_mk_string("Unable to create function")));
   }
   extism_function_set_namespace(func, ns);
   return lean_io_result_mk_ok(function_box(func));