blob: 7b6482224f2b8c39a224a40bf13beb8631a26920 (
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
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
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
|
import Scanner.Protocol
import Scanner.Xml.Basic
import Scanner.Xml.Parser
/-!
# Parsing of Protocol Description
This converts a protocol description XML into a `Raw.ProtocolDesc`.
-/
private def String.toNat (s : String) : Except String Nat :=
match Lean.Syntax.decodeNatLitVal? s with
| .some n => .ok n
| .none => .error s!"Expected a natural number, but got {s}"
private def String.toBool : String → Except String Bool
| "true" => .ok true
| "false" => .ok false
| s => .error s!"Expected a boolean value, but got {s}"
namespace Lean.Xml
private def Element.name : Xml.Element → String
| .Element name _ _ => name
private def Element.attributes : Xml.Element → Xml.Attributes
| .Element _ attrs _ => attrs
private def Element.content : Xml.Element → Array Xml.Content
| .Element _ _ content => content
private def Element.ensureName (el : Xml.Element) (name : String) : Except String Unit :=
if name == el.name
then .ok ()
else .error s!"Invalid tag: Expected {name}, but got {el.name}"
private def Element.textContent (el : Xml.Element) : String :=
let reformat (str : String) : String :=
str
|>.split "\n"
|>.map (String.Slice.trimAscii)
|>.map (String.Slice.toString)
|>.toList
|> String.intercalate "\n"
|>.trimAscii
|>.toString
reformat <| String.join <| Array.toList <| el.content.flatMap fun
| .Element _ => #[]
| .Comment _ => #[]
| .Character s => #[s]
private def Element.getChildrenByName (el : Xml.Element) (name : String) : Array Xml.Element :=
el.content.flatMap fun
| .Element child => if child.name == name then #[child] else #[]
| .Comment _ => #[]
| .Character _ => #[]
private def Element.getChildByName (el : Xml.Element) (name : String) : Option Xml.Element :=
match el.getChildrenByName name with
| #[single] => .some single
| _ => .none
private def Element.getAttribute (el : Xml.Element) (attr : String) : Option String :=
el.attributes.get? attr
private def Element.getRequiredAttribute (el : Xml.Element) (attr : String) : Except String String :=
el.getAttribute attr
|>.map pure
|>.getD (.error s!"Missing required attribute {attr}")
end Lean.Xml
open Lean
namespace WaylandScanner
open Raw
private def MessageType.ofString : String → Except String MessageType
| "destructor" => .ok .destructor
| s => .error s!"Expected \"destructor\", but got {s}"
private def ArgumentType.ofString : String → Except String ArgumentType
| "int" => .ok .int
| "uint" => .ok .uint
| "fixed" => .ok .fixed
| "string" => .ok .string
| "array" => .ok .array
| "fd" => .ok .fd
| "new_id" => .ok .newID
| "object" => .ok .object
| s => .error s!"Expected an argument type, but got {s}"
private def processDescription (el : Xml.Element) : Except String Description := do
el.ensureName "description"
let body := el.textContent
return {
summary := el.getAttribute "summary"
body := if body.isEmpty then .none else .some body
}
private def processEnumEntry (el : Xml.Element) : Except String EnumEntryDesc := do
el.ensureName "entry"
let name ← el.getRequiredAttribute "name"
let value ← (← el.getRequiredAttribute "value")
|>.toNat
let description ← el.getChildByName "description"
|>.mapM processDescription
let summary := el.getAttribute "summary"
let since ← el.getAttribute "since"
|>.mapM String.toNat
let deprecatedSince ← el.getAttribute "deprecated-since"
|>.mapM String.toNat
return {
name := name
value := value
description := description <|> summary.map Description.ofSummary
since := since.getD 1
deprecatedSince := deprecatedSince
}
private def processEnum (el : Xml.Element) : Except String EnumDesc := do
el.ensureName "enum"
let name ← el.getRequiredAttribute "name"
let description ← el.getChildByName "description"
|>.mapM processDescription
let since ← el.getAttribute "since"
|>.mapM String.toNat
let bitfield ← el.getAttribute "bitfield"
|>.mapM String.toBool
let entries ← el.getChildrenByName "entry"
|>.mapM processEnumEntry
return {
name := name
description := description
since := since.getD 1
bitfield := bitfield.getD false
entries := entries
}
private def processArgument (el : Xml.Element) : Except String ArgumentDesc := do
el.ensureName "arg"
let name ← el.getRequiredAttribute "name"
let type ← (← el.getRequiredAttribute "type")
|> ArgumentType.ofString
let description ← el.getChildByName "description"
|>.mapM processDescription
let summary := el.getAttribute "summary"
let interface := el.getAttribute "interface"
let enum := el.getAttribute "enum"
let allowNull ← el.getAttribute "allow-null"
|>.mapM String.toBool
return {
name := name
type := type
description := description <|> summary.map Description.ofSummary
interface := interface
enum := enum
allowNull := allowNull.getD false
}
private def processMessage (opcode : Nat) (el : Xml.Element) : Except String MessageDesc := do
let name ← el.getRequiredAttribute "name"
let description ← el.getChildByName "description"
|>.mapM processDescription
let type ← el.getAttribute "type"
|>.mapM MessageType.ofString
let since ← el.getAttribute "since"
|>.mapM String.toNat
let deprecatedSince ← el.getAttribute "deprecated-since"
|>.mapM String.toNat
let args ← el.getChildrenByName "arg"
|>.mapM processArgument
return {
name := name
opcode := opcode
description := description
type := type.getD .normal
since := since.getD 1
deprecatedSince := deprecatedSince
arguments := args
}
private def processInterface (el : Xml.Element) : Except String InterfaceDesc := do
el.ensureName "interface"
let name ← el.getRequiredAttribute "name"
let version ← (← el.getRequiredAttribute "version")
|>.toNat
let description ← el.getChildByName "description"
|>.mapM processDescription
let enums ← el.getChildrenByName "enum"
|>.mapM processEnum
let requests ← el.getChildrenByName "request"
|>.mapIdxM processMessage
let events ← el.getChildrenByName "event"
|>.mapIdxM processMessage
return {
name := name
version := version
description := description
enums := enums
requests := requests
events := events
}
private def processProtocol (el : Xml.Element) : Except String ProtocolDesc := do
el.ensureName "protocol"
let name ← el.getRequiredAttribute "name"
let copyright := el.getChildByName "copyright"
|>.map Xml.Element.textContent
let description ← el.getChildByName "description"
|>.mapM processDescription
let interfaces ← el.getChildrenByName "interface"
|>.mapM processInterface
return {
name := name
copyright := copyright
description := description
interfaces := interfaces
}
def parse (text : String) : Except String ProtocolDesc :=
Xml.parse text >>= processProtocol
end WaylandScanner
|
