blob: 6c5dbb7c721975e05063949f1c6bc25ee5b7846c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
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
|
