blob: 378b6dcca2fc1055cdff859304f9d33eba6bfa95 (
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
|
import Wayland
import Std.Data.HashMap
open Wayland Protocols
namespace Waylean
set_option linter.unusedVariables false
def Global (ι : InterfaceName) : Type := UInt32
deriving BEq
set_option linter.unusedVariables true
variable {ι : InterfaceName} [ResolvedInterface ι]
namespace Registry
private structure GlobalInfo where
ι : InterfaceName
name : Global ι
version : UInt32
structure State where
private globals : Array GlobalInfo := #[]
private registry : Option WlRegistry := .none
def State.new : State := {}
/-- Initialize the registry and start observing globals. -/
def init : DisplayM State Unit := do
let registry ← DisplayM.getRegistry
set ({ registry } : State)
registry.listen fun
| .global name iface version => do
let s ← get
set { s with
globals := s.globals ++ #[
({ ι := iface, name, version } : GlobalInfo)
]
}
| .globalRemove name => do
let s ← get
set { s with
globals := s.globals.filter fun info ↦
info.name != name
}
/-- Get a list of globals for a certain interface type. -/
def getGlobals : DisplayM State (Array (Global ι)) := do
let minVersion := (inferInstance : Interface ι).version
let globals := (← get).globals
return globals.filterMap fun g ↦
if g.ι == ι && g.version >= minVersion
then .some g.name
else .none
/-- Get a singleton instance for a global of a certain interface type. -/
def getSingleton? : DisplayM State (Option (Global ι)) := do
match (← getGlobals) with
| #[g] => pure (.some g)
| _ => pure .none
/-- Require a singleton instance for a global of a certain interface type. -/
def requireSingleton : DisplayM State (Global ι) := do
match (← getSingleton?) with
| .some g => pure g
| .none => throw (.userError s!"No singleton instance for interface {ι}")
end Registry
/-- Bind a global instance. -/
def Global.bind (global : Global ι) : DisplayM Registry.State (Object ι) := do
let registry ← (← get).registry
|>.map pure
|>.getD (throw (.userError "Registry not initialized"))
registry.bind global
def Registry.bindSingleton : DisplayM Registry.State (Object ι) := do
(← requireSingleton).bind
end Waylean
|
