cleanup: Add Current.param/Current.result

.github/workflows/docs.yml

@@ -42,7 +42,7 @@ jobs:
       - name: Upload artifact
         uses: actions/upload-pages-artifact@v2
         with:
-          path: '.lake/build/docs'
+          path: '.lake/build/doc'
       - name: Deploy to GitHub Pages
         id: deployment
         uses: actions/deploy-pages@v2

Extism/Bindings.lean

@@ -7,6 +7,7 @@ import Extism.Types
 
 open Extism
 
+/-- Returns the version of the Extism shared object -/
 @[extern "l_extism_version"]
 opaque version : IO String
 
@@ -18,37 +19,75 @@ private def PluginRef : Type := PluginPointed.type
 instance : Nonempty PluginRef := PluginPointed.property
 
 private opaque FunctionPointed : NonemptyType
+/-- Host function type -/
 def Extism.Function : Type := FunctionPointed.type
 instance : Nonempty Extism.Function := FunctionPointed.property
 
 private opaque CurrentPointed : NonemptyType
+/-- The current plugin, from within a host function -/
 def Extism.Current : Type := CurrentPointed.type
 instance : Nonempty Extism.Current := CurrentPointed.property
 
+/-- Set result to i64 from inside a host function -/
 @[extern "l_extism_current_set_result_i64"]
-opaque Current.setResultI64 : @& Extism.Current -> @& Int64 -> @& Int64 -> IO Unit
+opaque Current.setResultI64 : @& Extism.Current -> UInt64 -> UInt64 -> IO Unit
 
+/-- Get i64 param from inside a host function -/
 @[extern "l_extism_current_get_param_i64"]
-opaque Current.getParamI64 : @& Extism.Current -> @& Int64 -> IO Int64
+opaque Current.getParamI64 : @& Extism.Current -> UInt64 -> IO UInt64
 
+/-- Set result to i32 from inside a host function -/
 @[extern "l_extism_current_set_result_i32"]
-opaque Current.setResultI32 : @& Extism.Current -> @& Int64 -> @& Int32 -> IO Unit
+opaque Current.setResultI32 : @& Extism.Current -> UInt64 -> UInt32 -> IO Unit
 
+/-- Get i32 param from inside a host function -/
 @[extern "l_extism_current_get_param_i32"]
-opaque Current.getParamI32 : @& Extism.Current -> @& Int64 -> IO Int32
+opaque Current.getParamI32 : @& Extism.Current -> UInt64 -> IO UInt32
 
+/-- Set result to f64 from inside a host function -/
 @[extern "l_extism_current_set_result_f64"]
-opaque Current.setResultF64 : @& Extism.Current -> @& Int64 -> @& Float -> IO Unit
+opaque Current.setResultF64 : @& Extism.Current -> UInt64 -> Float -> IO Unit
 
+/-- Get f64 param from inside a host function -/
 @[extern "l_extism_current_get_param_f64"]
-opaque Current.getParamF64 : @& Extism.Current -> @& Int64 -> IO Float
+opaque Current.getParamF64 : @& Extism.Current -> UInt64 -> IO Float
 
+/-- Set result to f32 from inside a host function -/
 @[extern "l_extism_current_set_result_f32"]
-opaque Current.setResultF32 : @& Extism.Current -> @& Int64 -> @& Float -> IO Unit
+opaque Current.setResultF32 : @& Extism.Current -> UInt64 -> Float -> IO Unit
 
+/-- Get f32 param from inside a host function -/
 @[extern "l_extism_current_get_param_f32"]
-opaque Current.getParamF32 : @& Extism.Current -> @& Int64 -> IO Float
+opaque Current.getParamF32 : @& Extism.Current -> UInt64 -> IO Float
 
+@[extern "l_extism_current_alloc"]
+private opaque currentAlloc : @& Extism.Current -> UInt64 -> IO UInt64
+
+@[extern "l_extism_current_length"]
+private opaque currentLength : @& Extism.Current -> UInt64 -> IO UInt64
+
+@[extern "l_extism_current_free"]
+private opaque currentFree : @& Extism.Current -> UInt64 -> IO Unit
+
+@[extern "l_extism_current_read"]
+private opaque currentRead : @& Extism.Current -> UInt64 -> IO ByteArray
+
+@[extern "l_extism_current_write"]
+private opaque currentWrite : @& Extism.Current -> UInt64 -> @& ByteArray -> IO Unit
+
+def Current.result [ToBytes a] (current: Extism.Current) (index: USize) (v: a) : IO Unit := do
+  let data := ToBytes.toBytes v
+  let len := data.size
+  let n := <- currentAlloc current len.toUInt64
+  currentWrite current n data
+  Current.setResultI64 current index.toUInt64 n
+
+def Current.param [FromBytes a] (current: Extism.Current) (index: USize) : IO a := do
+  let n := <- Current.getParamI64 current index.toUInt64
+  let res := <- currentRead current n
+  let bytes := FromBytes.fromBytes? res
+  IO.ofExcept bytes
+
 @[extern "l_extism_plugin_new"]
 private opaque newPluginRef : @& ByteArray -> @& Array Function -> Bool -> IO PluginRef
 
@@ -59,7 +98,7 @@ private opaque pluginRefCall : @& PluginRef -> @& String -> @& ByteArray -> IO B
 private opaque functionNew :
   @& String -> @& String -> @& Array UInt8 -> @& Array UInt8 -> (Current -> IO Unit) -> IO Function
 
--- ValType represents the possible types for host function params/results
+/-- ValType represents the possible types for host function params/results -/
 inductive Extism.ValType where
   | i32
   | i64
@@ -86,7 +125,7 @@ private def newPluginFromFile
   newPluginRef data functions wasi
 
 
--- Create a new host function in the specified namespace
+/-- Create a new host function in the specified namespace -/
 def Extism.Function.newInNamespace
   (ns : String)
   (name: String)
@@ -98,7 +137,7 @@ def Extism.Function.newInNamespace
   let results := Array.map ValType.toInt results
   functionNew ns name params results f
 
--- Create a new host function in the default namespace
+/-- Create a new host function in the default namespace -/
 def Extism.Function.new
   (name: String)
   (params: Array ValType)
@@ -107,12 +146,12 @@ def Extism.Function.new
 :=
   Function.newInNamespace "extism:host/user" name params results f
 
--- Plugin struct
+/-- Plugin type -/
 structure Extism.Plugin where
   inner: PluginRef
   functions: Array Function
 
--- Create a new plugin from a `PluginInput`
+/-- Create a new plugin from a `PluginInput` -/
 def Extism.Plugin.new [PluginInput a]
   (data: a)
   (functions: Array Function)
@@ -122,7 +161,7 @@ def Extism.Plugin.new [PluginInput a]
   let x := <- newPluginRef input functions wasi
   return (Extism.Plugin.mk x #[])
 
--- Create a new plugin from a file
+/-- Create a new plugin from a file -/
 def Extism.Plugin.fromFile
   (path: System.FilePath)
   (functions: Array Function)
@@ -131,7 +170,7 @@ def Extism.Plugin.fromFile
   let x := <- newPluginFromFile path functions wasi
   return (Extism.Plugin.mk x #[])
 
--- Call a plugin function, performing conversion of input and output
+/-- Call a plugin function, performing conversion of input and output -/
 def Extism.Plugin.call [ToBytes a] [FromBytes b]
   (plugin: Extism.Plugin)
   (funcName: String)
@@ -141,7 +180,7 @@ def Extism.Plugin.call [ToBytes a] [FromBytes b]
   let res := <- pluginRefCall plugin.inner funcName data
   IO.ofExcept (FromBytes.fromBytes? res)
 
--- Call multiple plugins, piping the output from the last into the next
+/-- Call multiple plugins, piping the output from the last into the next -/
 def Extism.Plugin.pipe [ToBytes a] [FromBytes b]
   (plugin: Plugin)
   (names: List String)

Extism/Manifest.lean

@@ -1,11 +1,11 @@
-import Lean.Data.RBMap
 import Lean.Data.Json.Basic
 import Lean.Data.Json.FromToJson
 import Lean.Data.Json.Printer
 import Lean.Data.Json.Parser
 
 private def Pair := String × Lean.Json
 
+/-- Wasm file -/
 structure Extism.WasmFile where
   path: System.FilePath
   name: Option String
@@ -27,10 +27,7 @@ instance : Lean.ToJson Extism.WasmFile where
     let m := addIfSome m "hash" x.hash
     Lean.Json.mkObj m
 
-structure Extism.Memory where
-  maxPages: Int
-deriving Lean.FromJson, Lean.ToJson, Inhabited, Repr
-
+/-- Wasm URL -/
 structure Extism.WasmUrl where
   url: String
   headers: Option (List (String × String))
@@ -57,6 +54,7 @@ instance : Lean.ToJson Extism.WasmUrl where
     let m := addIfSome m "hash" x.hash
     Lean.Json.mkObj m
 
+/-- Wasm type -/
 inductive Extism.Wasm where
   | wasmFile: Extism.WasmFile -> Extism.Wasm
   | wasmUrl: Extism.WasmUrl -> Extism.Wasm
@@ -75,16 +73,24 @@ instance : Lean.ToJson Extism.Wasm where
     | Extism.Wasm.wasmFile f => Lean.ToJson.toJson f
     | Extism.Wasm.wasmUrl u => Lean.ToJson.toJson u
 
+/-- Create a new `Wasm` from a path on disk -/
 def Extism.Wasm.file (path: System.FilePath) : Wasm :=
   Extism.Wasm.wasmFile (WasmFile.mk path none none)
 
+/-- Create a new `Wasm` from a URL -/
 def Extism.Wasm.url (url: String) : Wasm :=
   Extism.Wasm.wasmUrl (WasmUrl.mk url none none none none)
 
+/-- Memory limits -/
+structure Extism.Memory where
+  maxPages: Int
+deriving Lean.FromJson, Lean.ToJson, Inhabited, Repr
+
+/-- Extism Manifest, used to link and configure plugins -/
 structure Extism.Manifest: Type where
   wasm: Array Wasm
   allowedHosts: Option (List String)
-  allowedPaths: Option (List (String × String))
+  allowedPaths: Option (List (System.FilePath × System.FilePath))
   memory: Option Memory
   config: Option (List (String × String))
   timeoutMs: Option Int
@@ -105,7 +111,7 @@ instance : Lean.ToJson Extism.Manifest where
     let paths := match x.allowedPaths with
       | Option.some x =>
         List.map (fun (k, v) =>
-          (k, Lean.toJson v)) x
+          (k.toString, Lean.toJson v)) x
         |> Lean.Json.mkObj
         |> Option.some
       | Option.none => Option.none
@@ -117,37 +123,48 @@ instance : Lean.ToJson Extism.Manifest where
     Lean.Json.mkObj m
 
 
+/-- Create a new Manifest from an array of `Wasm` -/
 def Extism.Manifest.new (wasm: Array Extism.Wasm) : Extism.Manifest :=
   Extism.Manifest.mk wasm none none none none none
 
-def Extism.Manifest.withMemoryMax (max: Int) (m: Extism.Manifest) : Extism.Manifest :=
+/-- Set memory max pages -/
+def Extism.Manifest.withMaxPages (max: Int) (m: Extism.Manifest) : Extism.Manifest :=
   {m with memory := some (Extism.Memory.mk max)}
 
+/-- Set configuration key -/
 def Extism.Manifest.withConfig (k: String) (v: String) (m: Extism.Manifest) :=
   let c := match m.config with
     | Option.none => []
     | Option.some x => x
   {m with config := (k, v) :: c}
 
+/-- Set timeout in milliseconds -/
 def Extism.Manifest.withTimeout (ms: Int) (m: Extism.Manifest) :=
   {m with timeoutMs := Option.some ms}
 
-def Extism.Manifest.allowPath (k: String) (v: String) (m: Extism.Manifest) :=
+/-- Allow access to a path on disk -/
+def Extism.Manifest.allowPath (k: System.FilePath) (v: Option System.FilePath) (m: Extism.Manifest) :=
   let c := match m.allowedPaths with
     | Option.none => []
     | Option.some x => x
+  let v := match v with
+    | Option.none => k
+    | Option.some v => v
   {m with allowedPaths := (k, v) :: c}
 
+/-- Allow host -/
 def Extism.Manifest.allowHost (k: String) (m: Extism.Manifest) :=
   let c := match m.allowedHosts with
     | Option.none => []
     | Option.some x => x
   {m with allowedHosts := k :: c}
 
+/-- Convenience function to convert an `Extism.Manifest` to a JSON string -/
 def Extism.Manifest.json (m: Extism.Manifest) : String :=
   let x := Lean.ToJson.toJson m
   Lean.Json.pretty x
 
+/-- Convenience function to parse an `Extism.Manifest` from a string -/
 def Extism.Manifest.parseJson (s: String) : Except String Extism.Manifest := do
   let x := <- Lean.Json.parse s
   Lean.FromJson.fromJson? x

Extism/Types.lean

@@ -5,12 +5,19 @@ import Lean.Data.Json.Printer
 
 import Extism.Manifest
 
+/-- `PluginInput` is implemented by types that can be accepted as the wasm input to
+    `Plugin.new` --/
 class Extism.PluginInput (a: Type) where
   toPluginInput: a -> ByteArray
 
+/-- `ToBytes` is used to convert input data into bytes -/
 class Extism.ToBytes (a: Type) where
   toBytes: a -> ByteArray
 
+/-- `FromBytes` is used to convert from bytes to output data -/
+class Extism.FromBytes (a: Type) where
+  fromBytes?: ByteArray -> Except String a
+
 instance : Extism.ToBytes ByteArray where
   toBytes (x: ByteArray) := x
 
@@ -20,9 +27,6 @@ instance : Extism.ToBytes String where
 instance [Lean.ToJson a] : Extism.ToBytes a where
   toBytes x := (Lean.Json.compress (Lean.ToJson.toJson x)).toUTF8
 
-class Extism.FromBytes (a: Type) where
-  fromBytes?: ByteArray -> Except String a
-
 instance : Extism.FromBytes ByteArray where
   fromBytes? (x: ByteArray) := Except.ok x
 

Test.lean

@@ -3,8 +3,9 @@ import Extism
 open Extism
 
 def helloWorld (curr: Current) : IO Unit := do
-  let a := <- Current.getParamI64 curr 0
-  let _ := <- Current.setResultI64 curr 0 a
+  let s: String := <- Current.param curr 0
+  IO.println s!"Input: {s}"
+  Current.result curr 0 s
   IO.println "Hello world!!!"
   IO.println "Hello world!!!"
   IO.println "Hello world!!!"
@@ -16,9 +17,8 @@ def hostFunction: IO Unit := do
     |> 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 := <- plugin.pipe ["count_vowels", "count_vowels"] input
-  IO.println s!"{res}"
+  let res: String := <- plugin.pipe ["count_vowels", "count_vowels"] "this is a test"
+  IO.println s!"Result: {res}"
 
 def fromUrl : IO Unit := do
   let url := "https://github.com/extism/plugins/releases/latest/download/count_vowels.wasm"
@@ -28,5 +28,5 @@ def fromUrl : IO Unit := do
   IO.println s!"{res}"
 
 def main : IO Unit := do
-  fromUrl
+  -- fromUrl
   hostFunction