parse wayland protocols

1 files changed, 216 insertions, 0 deletions

diff --git a/tools/Scanner/Parser.lean b/tools/Scanner/Parser.lean
new file mode 100644
index 0000000..3bdb7b6
--- /dev/null
+++ b/tools/Scanner/Parser.lean
@@ -0,0 +1,216 @@
+import Scanner.Protocol
+import Lean.Data.Xml.Basic
+import Lean.Data.Xml.Parser
+
+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
+
+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"
+  return {
+    summary := el.getAttribute "summary"
+    body := el.textContent
+  }
+
+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