summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/Scanner.lean38
-rw-r--r--tools/Scanner/Parser.lean216
-rw-r--r--tools/Scanner/Protocol.lean79
3 files changed, 333 insertions, 0 deletions
diff --git a/tools/Scanner.lean b/tools/Scanner.lean
new file mode 100644
index 0000000..d6962c7
--- /dev/null
+++ b/tools/Scanner.lean
@@ -0,0 +1,38 @@
+import Scanner.Protocol
+import Scanner.Parser
+
+open WaylandScanner
+
+def parseProtocol (path : System.FilePath) : IO ProtocolDesc := do
+ parse (← IO.FS.readFile path)
+ |>.mapError (fun ε ↦ s!"{path}: {ε}")
+ |> IO.ofExcept
+
+def process (rootModule : String) (outPath : System.FilePath) (srcPath : System.FilePath) : IO UInt32 := do
+ let protocols ← (← srcPath.readDir)
+ |>.map IO.FS.DirEntry.path
+ |>.mapM parseProtocol
+ let rootModuleComponents := rootModule.split "."
+ |>.map String.Slice.toString
+ |>.toArray
+ let rootModulePath := rootModuleComponents.foldl (· / ·) outPath
+ IO.println (reprStr protocols)
+ IO.FS.createDirAll rootModulePath
+ let indexPath := rootModulePath.addExtension "lean"
+ IO.FS.writeFile indexPath ""
+ return 0
+
+def usage : IO UInt32 := do
+ IO.println "Usage:"
+ IO.println " lake exe WaylandScanner -- <rootModule> <outPath> <srcPath>"
+ IO.println ""
+ IO.println "Description:"
+ IO.println " Read all (XML) protocols from the <srcPath> directory and"
+ IO.println " generate bindings in the <rootModule> namespace, where the"
+ IO.println " root source path is located at <outPath>."
+ return 1
+
+def main (args : List String) : IO UInt32 :=
+ match args with
+ | [rootModule, outPath, srcPath] => process rootModule outPath srcPath
+ | _ => usage
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
generated by cgit v1.3.1 (git 2.54.0) at 2026-11-10 14:33:42 +0000