blob: 18a05fa4c7fe27119cef80a4a3fce6379c896a07 (
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
|
import Wayland.Native
namespace Wayland
def EventSource := Native.EventSource
structure PosixSignal where
private signum : UInt32
deriving Repr, BEq, Inhabited
def PosixSignal.SIGINT : PosixSignal := ⟨Native.SIGINT⟩
def PosixSignal.SIGUSR1 : PosixSignal := ⟨Native.SIGUSR1⟩
def PosixSignal.SIGUSR2 : PosixSignal := ⟨Native.SIGUSR2⟩
structure Duration where
private milliseconds : UInt32
deriving Repr, BEq, Inhabited
def Duration.ofMilliseconds (val : UInt32) : Duration := ⟨val⟩
def Duration.ofSeconds (val : UInt32) : Duration := .ofMilliseconds (val * 1000)
def Duration.ofMinutes (val : UInt32) : Duration := .ofSeconds (val * 60)
def Duration.toMilliseconds (val : Duration) : UInt32 := val.milliseconds
def Duration.toSeconds (val : Duration) : UInt32 := val.toMilliseconds / 1000
def Duration.toMinutes (val : Duration) : UInt32 := val.toSeconds / 60
notation:2000 val "ms" => Duration.ofMilliseconds val
notation:2000 val "sec" => Duration.ofSeconds val
notation:2000 val "min" => Duration.ofMinutes val
structure Lens (O I : Type) where
get : O → I
set : I → O → O
macro "mk_lens " field:ident : term => do
let lvalNode := Lean.mkNode `Lean.Parser.Term.structInstLVal #[field.raw, Lean.mkNullNode #[]]
let lval : Lean.TSyntax `Lean.Parser.Term.structInstLVal := ⟨lvalNode⟩
`({ get := fun x => x.$field, set := fun i x => { x with $lval := i } })
abbrev Handler (σ : Type) := StateT σ IO Unit
structure Display (σ : Type) where
disp : Native.Display
addTimer : (delayMs : UInt32) → (msg : Handler σ) → IO EventSource
addSignal : (signum : UInt32) → (msg : Handler σ) → IO EventSource
remove : (source : EventSource) → IO Unit
quit : IO Unit
variable {σ α : Type}
def DisplayM (σ : Type) : Type → Type :=
ReaderT (Display σ) (StateT σ IO)
deriving instance Monad for DisplayM σ
deriving instance MonadState σ for DisplayM σ
private instance : MonadLift (ReaderT (Display σ) (StateT σ IO)) (DisplayM σ) where
monadLift := id
partial def DisplayM.run' (setUp : DisplayM σ Unit) (initialState : σ) (name : Option String := .none) : IO σ := do
let disp ← Native.Display.new name
let loop ← Native.EventLoop.new
_ ← loop.addDisplay disp
let global : Display σ :=
{ disp := disp
addTimer := loop.addTimer
addSignal := loop.addSignal
remove := loop.remove
quit := loop.quit }
let rec inner : StateT σ IO Unit := do
match (← loop.poll) with
| .none => return
| .some msg => msg; inner
let main : StateT σ IO Unit := do
setUp.run global
inner
main.run initialState |>.map Prod.snd
def DisplayM.run (setUp : DisplayM σ Unit) (initialState : σ) (name : Option String := .none) : IO Unit :=
DisplayM.run' setUp initialState (name := name) |> discard
def DisplayM.liftIO (io : IO α) : DisplayM σ α :=
io
def DisplayM.requestQuit : DisplayM σ Unit := do
(← read).quit
def DisplayM.registerSignal (signal : PosixSignal) (handler : DisplayM σ Unit) : DisplayM σ EventSource := do
let global ← read
global.addSignal signal.signum (ReaderT.run handler global)
def DisplayM.registerTimer (timeout : Duration) (handler : DisplayM σ Unit) : DisplayM σ EventSource := do
let global ← read
global.addTimer timeout.toMilliseconds (ReaderT.run handler global)
def DisplayM.unregister (source : EventSource) : DisplayM σ Unit := do
(← read).remove source
private def zoomState {σ₁ σ₂ : Type} {m : Type → Type} [Monad m] (lens : Lens σ₁ σ₂) (inner : StateT σ₂ m α) : StateT σ₁ m α := do
let oldOuter ← get
let (res, newInner) ← inner.run (lens.get oldOuter)
set (lens.set newInner oldOuter)
return res
def DisplayM.zoom {σ₁ σ₂ : Type} (lens : Lens σ₁ σ₂) (inner : DisplayM σ₂ α) : DisplayM σ₁ α := do
let global₁ : Display σ₁ ← read
let global₂ : Display σ₂ :=
{ disp := global₁.disp
addTimer := fun x y ↦ global₁.addTimer x (zoomState lens y)
addSignal := fun x y ↦ global₁.addSignal x (zoomState lens y)
remove := global₁.remove
quit := global₁.quit }
zoomState lens (ReaderT.run inner global₂)
end Wayland
|
