blob: 1c89a6309409110ff0296238bf9fd7c4adaf5417 (
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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
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 : (callback : WLCallback) → Request
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
| 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
| 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
partial def nextTimer : DisplayM Int Unit := do
_ ← DisplayM.registerTimer 16ms do
let newCount := (← get) + 1
set newCount
DisplayM.liftIO (IO.println s!"Timer tick {newCount}")
nextTimer
def launch : DisplayM State Unit := do
_ ← DisplayM.registerSignal .SIGINT do
DisplayM.liftIO (IO.println "Received SIGINT")
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 }
|
