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
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
|
import Scanner.Protocol
import Std.Data.TreeMap
import Std.Data.TreeSet
/-!
# Processing of Protocol Descriptions
This is mainly used to resolve interface/enum references within protocols, converting a `Raw.ProtocolDesc` into a
`Client.ProtocolDesc`. Note that this requires a global view of all protocols since interfaces can mention interfaces
from other protocols. Thus, this needs to be done after parsing all protocols.
-/
namespace WaylandScanner
private structure InterfaceInfo where
moduleName : Identifier
enums : Array Identifier
private abbrev InterfaceMap := Std.TreeMap String InterfaceInfo
private structure Context where
interfaces : InterfaceMap
currentInterface : Client.InterfaceRef
referencedInterfaces : Std.TreeSet Client.InterfaceRef
private abbrev Processor : Type → Type := StateT Context (Except String)
private def processEnumEntry (raw : Raw.EnumEntryDesc) : Processor Client.EnumEntryDesc := do
return {
name := raw.name
value := raw.value
description := raw.description
since := raw.since
deprecatedSince := raw.deprecatedSince
}
private def interfaceInfo (name : String) : Processor InterfaceInfo := do
match (← get).interfaces.get? name with
| .some info => pure info
| .none => .error s!"Unable to find referenced interface {name}"
private def resolveInterface (name : String) : Processor Client.InterfaceRef := do
let info ← interfaceInfo name
let ref := {
moduleName := info.moduleName
typeName := name
}
let old ← get
set { old with referencedInterfaces := old.referencedInterfaces.insert ref }
return ref
private def resolveEnum (name : String) : Processor Client.EnumRef := do
let (interface, enum) ←
match (name.split ".").toArray with
| #[enum] => pure ((← get).currentInterface.typeName, enum.toString)
| #[interface, enum] => pure (interface.toString, enum.toString)
| _ => throw s!"Malformed enum reference {name}"
let info ← interfaceInfo interface
if not (info.enums.contains enum) then
throw s!"Interface {repr interface} does not contain enum {repr enum}"
return {
moduleName := info.moduleName
typeName := interface
enumName := enum
}
private def processEnum (raw : Raw.EnumDesc) : Processor Client.EnumDesc := do
return {
name := raw.name
description := raw.description
since := raw.since
bitfield := raw.bitfield
entries := ← raw.entries.mapM processEnumEntry
}
private def processArgument (raw : Raw.ArgumentDesc) : Processor Client.ArgumentDesc := do
return {
name := raw.name
type :=
← match raw.type with
| .int => Client.ArgumentType.int <$> raw.enum.mapM resolveEnum
| .uInt => Client.ArgumentType.uInt <$> raw.enum.mapM resolveEnum
| .fixed => Client.ArgumentType.fixed |> pure
| .string => Client.ArgumentType.string (.ofAllowNull raw.allowNull) |> pure
| .array => Client.ArgumentType.array |> pure
| .fd => Client.ArgumentType.fd |> pure
| .newID => Client.ArgumentType.object .notNull <$> raw.interface.mapM resolveInterface
| .object => Client.ArgumentType.object (.ofAllowNull raw.allowNull) <$> raw.interface.mapM resolveInterface
description := raw.description
}
private def processRequest (raw : Raw.MessageDesc) : Processor Client.RequestDesc := do
let newIDArgs := raw.arguments.filter fun arg ↦ arg.type == .newID
let otherArgs := raw.arguments.filter fun arg ↦ arg.type != .newID
let returnType ←
match newIDArgs with
| #[] => Client.ReturnType.unit |> pure
| #[arg] => Client.ReturnType.object <$> arg.interface.mapM resolveInterface
| _ => throw s!"Expected at most one new_id argument for request in {raw.name}"
return {
name := raw.name
opcode := raw.opcode
description := raw.description
isDestructor := raw.type == .destructor
since := raw.since
deprecatedSince := raw.deprecatedSince
arguments := ← otherArgs.mapM processArgument
returnType := returnType
}
private def processEvent (raw : Raw.MessageDesc) : Processor Client.EventDesc := do
return {
name := raw.name
opcode := raw.opcode
description := raw.description
isDestructor := raw.type == .destructor
since := raw.since
deprecatedSince := raw.deprecatedSince
arguments := ← raw.arguments.mapM processArgument
}
private def processInterface (raw : Raw.InterfaceDesc) : Processor Client.InterfaceDesc := do
let requests ← raw.requests.mapM processRequest
let events ← raw.events.mapM processEvent
let state ← get
let referencedInterfaces := state.referencedInterfaces.insert state.currentInterface
return {
name := raw.name
version := raw.version
description := raw.description
enums := ← raw.enums.mapM processEnum
requests := requests
events := events
referencedInterfaces := referencedInterfaces
}
private def processProtocol (interfaces : InterfaceMap) (raw : Raw.ProtocolDesc) : Except String Client.ProtocolDesc := do
return {
name := raw.name
copyright := raw.copyright
description := raw.description
interfaces := ← raw.interfaces.mapM
fun iface ↦ (processInterface iface).run' {
interfaces := interfaces
currentInterface := { moduleName := raw.name, typeName := iface.name }
referencedInterfaces := .empty
}
}
/-! Compute the transitive closure w.r.t. `referencedInterfaces`. -/
private partial def transitiveClosure (protocols : Array Client.ProtocolDesc) : Array Client.ProtocolDesc :=
let successors : Std.TreeMap Client.InterfaceRef (List Client.InterfaceRef) := .ofArray <| protocols.flatMap
fun protocol ↦ protocol.interfaces.map
fun iface ↦ ((⟨protocol.name, iface.name⟩ : Client.InterfaceRef), iface.referencedInterfaces.toList)
let rec dfs : Std.TreeSet Client.InterfaceRef → List Client.InterfaceRef → Std.TreeSet Client.InterfaceRef
| visited, [] => visited
| visited, (x::xs) =>
if visited.contains x
then dfs visited xs
else dfs (visited.insert x) (successors.get! x ++ xs)
let interfaceClosure (iface : Client.InterfaceDesc) : Client.InterfaceDesc :=
{ iface with referencedInterfaces := dfs .empty iface.referencedInterfaces.toList }
let protocolClosure (protocol : Client.ProtocolDesc) : Client.ProtocolDesc :=
{ protocol with interfaces := protocol.interfaces.map interfaceClosure }
protocols.map protocolClosure
-- TODO: Correctness proof for `transitiveClosure`
def processProtocols (raw : Array Raw.ProtocolDesc) : Except String (Array Client.ProtocolDesc) := do
let interfaces : InterfaceMap := .ofArray <| raw.flatMap
fun protocol ↦ protocol.interfaces.map
fun iface ↦ (iface.name, (⟨protocol.name, iface.enums.map Raw.EnumDesc.name⟩ : InterfaceInfo))
let res ← raw.mapM (processProtocol interfaces)
return transitiveClosure res
end WaylandScanner
|
