try to properly deal with constructors

1 files changed, 30 insertions, 60 deletions

diff --git a/src/Waylean.lean b/src/Waylean.lean
index 1c89a63..0cbd6f8 100644
--- a/src/Waylean.lean
+++ b/src/Waylean.lean
@@ -5,82 +5,50 @@ 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 : (callback : WLCallback) → Request
+def WLDisplay : Type := Object WLDisplay.name
+def WLCallback : Type := Object WLCallback.name
 
 inductive WLDisplay.Event where
   | 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 := #[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 := #[WLDisplay.Event.error.signature]
-  signature
-    | .error _ _ => WLDisplay.Event.error.signature
-  demarshal opcode := match opcode with
+instance : Interface WLDisplay.name where
+  event := WLDisplay.Event
+  requests :=
+    #[ { name := "sync"
+         args := #[.newID WLCallback.name]
+         since := 0
+         isDestructor := False } ]
+  events :=
+    #[ { name := "error"
+         args := #[.object .notNull WLDisplay.name, .uint, .string .notNull]
+         since := 0
+         isDestructor := False } ]
+  demarshalEvent
     | 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
 
-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
+instance : Interface WLCallback.name where
+  event := WLCallback.Event
+  requests :=
+    #[]
+  events :=
+    #[ { name := "done"
+         args := #[.uint]
+         since := 0
+         isDestructor := False } ]
+  demarshalEvent
     | 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
@@ -89,6 +57,10 @@ instance : ResolvedInterface WLDisplay.name where
 instance : ResolvedInterface WLCallback.name where
   referencedInterfaces := #[⟨WLCallback.name, inferInstance⟩]
 
+def WLDisplay.sync {σ : Type} (display : WLDisplay) : DisplayM σ WLCallback :=
+  display.sendConstructor do
+    return 0
+
 structure State where
   count : Int
 
@@ -106,11 +78,9 @@ def launch : DisplayM State Unit := do
   DisplayM.zoom (mk_lens count) nextTimer
 
   let disp : WLDisplay ← DisplayM.getDisplay
-  let callback : WLCallback ← DisplayM.createObject disp
+  let callback : WLCallback ← disp.sync
   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 }