object api sketch

1 files changed, 98 insertions, 0 deletions

diff --git a/lib/Wayland/Object.lean b/lib/Wayland/Object.lean
new file mode 100644
index 0000000..6c5dbb7
--- /dev/null
+++ b/lib/Wayland/Object.lean
@@ -0,0 +1,98 @@
+import Wayland.Display
+
+namespace Wayland
+
+def InterfaceName : Type := String
+  deriving Repr, BEq
+
+def OpCode : Type := UInt32
+  deriving Repr, BEq
+
+structure Object (ι : InterfaceName) where
+
+structure NewID (ι : InterfaceName) where
+
+class ArgumentMarshaller (m : Type → Type) extends Monad m where
+  marshalInt                        : Int32             → m Unit
+  marshalUInt                       : UInt32            → m Unit
+  marshalFixed                      : Float32           → m Unit
+  marshalString                     : Option String     → m Unit
+  marshalObject {ι : InterfaceName} : Option (Object ι) → m Unit
+  marshalNewID {ι : InterfaceName}  : NewID ι           → m Unit
+  marshalArray                      : ByteArray         → m Unit
+  marshalFD                         : Int32             → m Unit
+
+class ArgumentDemarshaller (m : Type → Type) extends Monad m where
+  demarshalInt                        : m Int32
+  demarshalUInt                       : m UInt32
+  demarshalFixed                      : m Float32
+  demarshalString                     : m (Option String)
+  demarshalObject {ι : InterfaceName} : m (Option (Object ι))
+  demarshalNewID {ι : InterfaceName}  : m (NewID ι)
+  demarshalArray                      : m ByteArray
+  demarshalFD                         : m Int32
+
+inductive Nullability where
+  | nullable
+  | notNull
+
+inductive Argument where
+  | int : Argument
+  | uint : Argument
+  | fixed : Argument
+  | string : Nullability → Argument
+  | object : Nullability → InterfaceName → Argument
+  | newID : InterfaceName → Argument
+  | array : Argument
+  | fd : Argument
+
+structure Message where
+  name : String
+  args : Array Argument
+  since : UInt32
+  isDestructor : Bool
+
+class Request (α : Type) where
+  messages : Array Message
+  signature : α → Message
+  marshal {m : Type → Type} [ArgumentMarshaller m] : α → m OpCode
+
+class Event (α : Type) where
+  messages : Array Message
+  signature : α → Message
+  demarshal {m : Type → Type} [ArgumentDemarshaller m] : OpCode → m α
+
+class Interface (ι : InterfaceName) where
+  request : Type
+  [requestClass : Request request]
+  event : Type
+  [eventClass : Event event]
+  version : UInt32
+
+variable {σ : Type} {ι : InterfaceName}
+
+def Object.send [iface : Interface ι] (obj : Object ι) (req : iface.request) : DisplayM σ Unit := sorry
+def Object.listen [iface : Interface ι] (obj : Object ι) (handler : iface.event → DisplayM σ Unit) : DisplayM σ Unit := sorry
+
+-- def WLDisplay.name : InterfaceName := "wl_display"
+-- abbrev WLDisplay : Type := Object WLDisplay.name
+
+-- inductive WLDisplay.Request where
+--   | sync : Request
+
+-- inductive WLDisplay.Event where
+--   | error : Event
+
+-- instance : Request WLDisplay.Request := sorry
+-- instance : Event WLDisplay.Event := sorry
+-- instance : Interface WLDisplay.name where
+--   request := WLDisplay.Request
+--   event := WLDisplay.Event
+--   version := 1
+
+-- def test (disp : WLDisplay) : DisplayM σ Unit := do
+--   disp.listen fun
+--     | .error => DisplayM.liftIO (IO.println "error!")
+--   disp.send .sync
+
+end Wayland