type map implementation

1 files changed, 0 insertions, 98 deletions

diff --git a/lib/Wayland/Object.lean b/lib/Wayland/Object.lean
deleted file mode 100644
index 6c5dbb7..0000000
--- a/lib/Wayland/Object.lean
+++ /dev/null
@@ -1,98 +0,0 @@
-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