blob: b595672f53bfcfcf6f23c4f30fa6a6e1f9616312 (
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
|
import Wayland
open Wayland
def WLCallback.name : InterfaceName := "wl_callback"
def WLDisplay.name : InterfaceName := "wl_display"
def WLDisplay : Type := Object WLDisplay.name
def WLCallback : Type := Object WLCallback.name
inductive WLDisplay.Event where
| error : (code : UInt32) → (message : String) → Event
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
version := 1
inductive WLCallback.Event where
| done : (data : UInt32) → Event
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
version := 1
instance : ResolvedInterface WLDisplay.name where
referencedInterfaces := #[⟨WLDisplay.name, inferInstance⟩, ⟨WLCallback.name, inferInstance⟩]
instance : ResolvedInterface WLCallback.name where
referencedInterfaces := #[⟨WLCallback.name, inferInstance⟩]
def WLDisplay.sync {σ : Type} (display : WLDisplay) (handler : DisplayM σ Unit) : DisplayM σ Unit := do
let callback : WLCallback ← display.sendConstructor do
return 0
callback.listen fun
| .done _ => do
callback.keep
handler
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
disp.sync do
DisplayM.liftIO (IO.println "Roundtrip complete")
def main : IO Unit :=
DisplayM.run launch { count := 0 }
|
