From 09be9fb2701f0560aeb714f89fe0d1e750915ae0 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Fri, 3 Apr 2026 21:40:46 +0200 Subject: parse wayland protocols --- tools/Scanner/Parser.lean | 216 ++++++++++++++++++++++++++++++++++++++++++++ tools/Scanner/Protocol.lean | 79 ++++++++++++++++ 2 files changed, 295 insertions(+) create mode 100644 tools/Scanner/Parser.lean create mode 100644 tools/Scanner/Protocol.lean (limited to 'tools/Scanner') 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 diff --git a/tools/Scanner/Protocol.lean b/tools/Scanner/Protocol.lean new file mode 100644 index 0000000..6c9a838 --- /dev/null +++ b/tools/Scanner/Protocol.lean @@ -0,0 +1,79 @@ +namespace WaylandScanner + +structure Description where + summary : Option String + body : Option String + deriving Repr + +def Description.ofSummary (s : String) : Description := + { summary := s + body := .none } + +structure EnumEntryDesc where + name : String + value : Int + description : Option Description + since : Nat + deprecatedSince : Option Nat + deriving Repr + +structure EnumDesc where + name : String + description : Option Description + since : Nat + bitfield : Bool + entries: Array EnumEntryDesc + deriving Repr + +inductive ArgumentType where +| int +| uInt +| fixed +| string +| array +| fd +| newID +| object +deriving Repr + +structure ArgumentDesc where + name : String + type : ArgumentType + description : Option Description + interface : Option String + enum : Option String + allowNull : Bool + deriving Repr + +inductive MessageType where +| normal +| destructor +deriving Repr + +structure MessageDesc where + name : String + opcode : Nat + description : Option Description + type : MessageType + since : Nat + deprecatedSince : Option Nat + arguments : Array ArgumentDesc + deriving Repr + +structure InterfaceDesc where + name : String + version : Nat + description : Option Description + enums : Array EnumDesc + requests : Array MessageDesc + events : Array MessageDesc + deriving Repr + +structure ProtocolDesc where + name : String + copyright : Option String + description : Option Description + interfaces : Array InterfaceDesc + deriving Repr + +end WaylandScanner -- cgit v1.3.1