1 files changed, 78 insertions, 12 deletions
diff --git a/src/Waylean.lean b/src/Waylean.lean
index 3565854..1c89a63 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -2,33 +2,92 @@ import Wayland
 open Wayland
 
 
+def WLCallback.name : InterfaceName := "wl_callback"
 def WLDisplay.name : InterfaceName := "wl_display"
+
 abbrev WLDisplay : Type := Object WLDisplay.name
+abbrev WLCallback : Type := Object WLCallback.name
 
 inductive WLDisplay.Request where
-  | sync : Request
+  | sync : (callback : WLCallback) → Request
 
 inductive WLDisplay.Event where
-  | error : Event
-  | other : Event
+  | error : (code : UInt32) → (message : String) → Event
+
+def WLDisplay.Request.sync.signature : MessageDesc :=
+  { name := "sync"
+    args := #[.newID WLCallback.name]
+    since := 0
+    isDestructor := False }
 
 instance : Request WLDisplay.Request where
-  messages := #[{ name := "sync", args := #[], since := 0, isDestructor := False }]
-  signature _ := sorry
-  marshal _ := do return 0
+  messages := #[WLDisplay.Request.sync.signature]
+  signature
+    | .sync _ => WLDisplay.Request.sync.signature
+  marshal
+    | .sync callback => do
+      ArgumentMarshaller.marshalNewID callback
+      return 0
+
+def WLDisplay.Event.error.signature : MessageDesc :=
+  { name := "error"
+    args := #[.object .notNull WLDisplay.name, .uint, .string .notNull]
+    since := 0
+    isDestructor := False }
+
 instance : Event WLDisplay.Event where
-  messages := #[{ name := "error", args := #[.string .notNull], since := 0, isDestructor := False },
-                { name := "other", args := #[.object .nullable WLDisplay.name], since := 99, isDestructor := False}]
-  signature _ := sorry
-  demarshal _ := do return .error
+  messages := #[WLDisplay.Event.error.signature]
+  signature
+    | .error _ _ => WLDisplay.Event.error.signature
+  demarshal opcode := match opcode with
+    | 0 => do
+      (_ : Option (Object WLDisplay.name)) ← ArgumentDemarshaller.demarshalObject
+      return .error
+        (← ArgumentDemarshaller.demarshalUInt)
+        ((← ArgumentDemarshaller.demarshalString).getD "")
+    | _ => sorry
+
 instance : Interface WLDisplay.name where
   request := WLDisplay.Request
   event := WLDisplay.Event
   version := 1
-instance : ResolvedInterface WLDisplay.name where
-  referencedInterfaces := #[⟨WLDisplay.name, inferInstance⟩]
 
+inductive WLCallback.Request where
+
+inductive WLCallback.Event where
+  | done : (data : UInt32) → Event
+
+def WLCallback.Event.done.signature : MessageDesc :=
+  { name := "done"
+    args := #[.uint]
+    since := 0
+    isDestructor := False }
 
+instance : Request WLCallback.Request where
+  messages := #[]
+  signature req := by cases req
+  marshal req := by cases req
+
+instance : Event WLCallback.Event where
+  messages := #[WLCallback.Event.done.signature]
+  signature
+    | .done _ => WLCallback.Event.done.signature
+  demarshal opcode := match opcode with
+    | 0 => do
+      return .done
+        (← ArgumentDemarshaller.demarshalUInt)
+    | _ => sorry
+
+instance : Interface WLCallback.name where
+  request := WLCallback.Request
+  event := WLCallback.Event
+  version := 1
+
+instance : ResolvedInterface WLDisplay.name where
+  referencedInterfaces := #[⟨WLDisplay.name, inferInstance⟩, ⟨WLCallback.name, inferInstance⟩]
+
+instance : ResolvedInterface WLCallback.name where
+  referencedInterfaces := #[⟨WLCallback.name, inferInstance⟩]
 
 structure State where
   count : Int
@@ -46,5 +105,12 @@ def launch : DisplayM State Unit := do
     DisplayM.requestQuit
   DisplayM.zoom (mk_lens count) nextTimer
 
+  let disp : WLDisplay ← DisplayM.getDisplay
+  let callback : WLCallback ← DisplayM.createObject disp
+  callback.listen fun ev ↦ match ev with
+    | .done _ => DisplayM.liftIO (IO.println "Roundtrip complete")
+  disp.send (.sync callback)
+  DisplayM.liftIO (IO.println "Test 5")
+
 def main : IO Unit :=
   DisplayM.run launch { count := 0 }