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