blob: 35658547c50ef9fdf8d3666e883e04a288ac0f66 (
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
|
import Wayland
open Wayland
def WLDisplay.name : InterfaceName := "wl_display"
abbrev WLDisplay : Type := Object WLDisplay.name
inductive WLDisplay.Request where
| sync : Request
inductive WLDisplay.Event where
| error : Event
| other : Event
instance : Request WLDisplay.Request where
messages := #[{ name := "sync", args := #[], since := 0, isDestructor := False }]
signature _ := sorry
marshal _ := do return 0
instance : Event WLDisplay.Event where
messages := #[{ name := "error", args := #[.string .notNull], since := 0, isDestructor := False },
{ name := "other", args := #[.object .nullable WLDisplay.name], since := 99, isDestructor := False}]
signature _ := sorry
demarshal _ := do return .error
instance : Interface WLDisplay.name where
request := WLDisplay.Request
event := WLDisplay.Event
version := 1
instance : ResolvedInterface WLDisplay.name where
referencedInterfaces := #[⟨WLDisplay.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
def main : IO Unit :=
DisplayM.run launch { count := 0 }
|
