summaryrefslogtreecommitdiff
path: root/tools/Scanner
diff options
context:
space:
mode:
Diffstat (limited to 'tools/Scanner')
-rw-r--r--tools/Scanner/Generator.lean267
-rw-r--r--tools/Scanner/Parser.lean3
-rw-r--r--tools/Scanner/Processor.lean39
-rw-r--r--tools/Scanner/Protocol.lean27
4 files changed, 318 insertions, 18 deletions
diff --git a/tools/Scanner/Generator.lean b/tools/Scanner/Generator.lean
new file mode 100644
index 0000000..1ac8139
--- /dev/null
+++ b/tools/Scanner/Generator.lean
@@ -0,0 +1,267 @@
+import Std.Data.TreeSet
+import Scanner.Protocol
+
+/-!
+# Generating Code from Protocol Descriptions
+
+This turns a `Client.ProtocolDesc` into the various Lean source files containing bindings for said protocol.
+-/
+
+namespace WaylandScanner
+
+open Client
+
+-- TODO: Maybe use Lean's `Syntax` API here instead of a custom formatter?
+
+private structure GeneratorState where
+ imports : Std.TreeSet String := .empty
+ code : Array String := #[]
+
+private structure GeneratorContext where
+ rootModule : String
+ currentModule : String
+
+private abbrev Generator := StateT GeneratorState (ReaderM GeneratorContext)
+
+private def emitImport (mod : String) : Generator Unit := do
+ let current := (← read).currentModule
+ if current != mod then
+ let oldState ← get
+ set { oldState with imports := oldState.imports.insert mod }
+ return ()
+
+private def emitLocalImport (protocolName : Identifier) (suffix : String := "") : Generator Unit := do
+ let root := (← read).rootModule
+ emitImport s!"{root}.{protocolName.pascalCase}{suffix}"
+
+private def emitLine (line : String) : Generator Unit := do
+ let oldState ← get
+ set { oldState with code := oldState.code ++ #[line] }
+
+private def emitNamespace {α : Type} (space : String) (gen : Generator α) : Generator α := do
+ emitLine s!"namespace {space}"
+ emitLine s!""
+ let res ← gen
+ emitLine s!""
+ emitLine s!"end {space}"
+ return res
+
+private def Generator.run (gen : Generator Unit) : ReaderM GeneratorContext String := do
+ let (_, res) ← StateT.run gen {}
+ let imports := res.imports
+ |>.toArray
+ |>.map fun m ↦ s!"import {m}"
+ let lines := imports ++ #[""] ++ res.code
+ return String.intercalate "\n" lines.toList
+
+private def Generator.runProtocol (rootModule : String) (protocol : ProtocolDesc) (suffix : String := "") (gen : Generator Unit) : String :=
+ gen.run.run { rootModule, currentModule := s!"{rootModule}.{protocol.name.pascalCase}{suffix}" }
+
+private def Generator.runIndex (rootModule : String) (gen : Generator Unit) : String :=
+ gen.run.run { rootModule, currentModule := rootModule }
+
+private def resolveInterface (iface : InterfaceRef) (suffix : String := ".Header") : Generator String := do
+ emitLocalImport iface.moduleName suffix
+ return iface.typeName.pascalCase
+
+private def resolveEnum (enum : EnumRef) : Generator String := do
+ let iface ← resolveInterface enum.toInterfaceRef
+ return s!"{iface}.{enum.enumName.pascalCase}"
+
+section Header
+
+private def emitNameDefinitions (protocol : ProtocolDesc) : Generator Unit := do
+ for iface in protocol.interfaces do
+ emitLine s!"abbrev {iface.name.pascalCase}.name : InterfaceName := {iface.name.quoted}"
+
+private def emitObjectDefinitions (protocol : ProtocolDesc) : Generator Unit := do
+ for iface in protocol.interfaces do
+ emitLine s!"def {iface.name.pascalCase} : Type := Object {iface.name.pascalCase}.name"
+
+private def emitEnumDefinitions (protocol : ProtocolDesc) : Generator Unit := do
+ for iface in protocol.interfaces do
+ for enum in iface.enums do
+ emitLine s!""
+ if enum.bitfield then
+ emitLine s!"structure {iface.name.pascalCase}.{enum.name.pascalCase} where"
+ for entry in enum.entries do
+ emitLine s!" {entry.name.camelCase} : Bool"
+ else
+ emitLine s!"inductive {iface.name.pascalCase}.{enum.name.pascalCase} where"
+ for entry in enum.entries do
+ emitLine s!" | {entry.name.camelCase}"
+
+def generateHeader (rootModule : String) (protocol : ProtocolDesc) : String :=
+ Generator.runProtocol rootModule protocol ".Header" do
+ emitNamespace rootModule do
+ emitImport "Wayland.Display"
+ emitNameDefinitions protocol
+ emitLine ""
+ emitObjectDefinitions protocol
+ emitEnumDefinitions protocol
+
+end Header
+
+section Interface
+
+private def emitEventDefinitions (protocol : ProtocolDesc) : Generator Unit := do
+ for iface in protocol.interfaces do
+ emitLine s!"inductive {iface.name.pascalCase}.Event where"
+ for event in iface.events do
+ emitLine s!" | {event.name.camelCase}"
+ for arg in event.arguments do
+ let argName := arg.name.camelCase
+ match arg.type with
+ | .int .none => emitLine s!" ({argName} : Int32)"
+ | .int (.some enum) => emitLine s!" ({argName} : {← resolveEnum enum})"
+ | .uInt .none => emitLine s!" ({argName} : UInt32)"
+ | .uInt (.some enum) => emitLine s!" ({argName} : {← resolveEnum enum})"
+ | .fixed => emitLine s!" ({argName} : Float)"
+ | .string .nullable => emitLine s!" ({argName} : Option String)"
+ | .string .notNull => emitLine s!" ({argName} : String)"
+ | .array => emitLine s!" ({argName} : ByteArray)"
+ | .fd => emitLine s!" ({argName} : Int32)"
+ | .object .nullable .none => emitLine s!" ({argName} : Option AnyObject)"
+ | .object .nullable (.some iface) => emitLine s!" ({argName} : Option {← resolveInterface iface})"
+ | .object .notNull .none => emitLine s!" ({argName} : AnyObject)"
+ | .object .notNull (.some iface) => emitLine s!" ({argName} : {← resolveInterface iface})"
+ emitLine s!""
+
+private def emitInterfaceInstances (protocol : ProtocolDesc) : Generator Unit := do
+ let emitMessageDesc (msg : MessageDesc) : Generator Unit := do
+ emitLine " {"
+ emitLine s!" name := {msg.name.quoted}"
+ let nullability (arg : Raw.ArgumentDesc) : String :=
+ if arg.allowNull then ".nullable" else ".notNull"
+ let interfaceName (arg : Raw.ArgumentDesc) : String :=
+ match arg.interface with
+ | .some iface => s!"(.some \"{iface}\")"
+ | .none => ".none"
+ let argumentDesc (arg : Raw.ArgumentDesc) : String :=
+ match arg.type with
+ | .int => ".int"
+ | .uInt => ".uint"
+ | .fixed => ".fixed"
+ | .string => s!".string {nullability arg}"
+ | .object => s!".object {nullability arg} {interfaceName arg}"
+ | .newID => s!".newID {interfaceName arg}"
+ | .array => ".array"
+ | .fd => ".fd"
+ let args := msg.rawArguments
+ |>.map argumentDesc
+ |>.toList
+ |> String.intercalate ", "
+ emitLine s!" args := #[{args}]"
+ emitLine s!" since := {msg.since}"
+ emitLine s!" isDestructor := {msg.isDestructor}"
+ emitLine " },"
+ for iface in protocol.interfaces do
+ emitLine s!""
+ emitLine s!"instance : Interface {iface.name.pascalCase}.name where"
+ emitLine s!" event := {iface.name.pascalCase}.Event"
+ emitLine s!" version := {iface.version}"
+ emitLine s!" requests := #["
+ for req in iface.requests do
+ emitMessageDesc req.toMessageDesc
+ emitLine s!" ]"
+ emitLine s!" events := #["
+ for ev in iface.events do
+ emitMessageDesc ev.toMessageDesc
+ emitLine s!" ]"
+ emitLine s!" demarshalEvent := sorry"
+ -- TODO
+
+def generateInterface (rootModule : String) (protocol : ProtocolDesc) : String :=
+ Generator.runProtocol rootModule protocol ".Interface" do
+ emitNamespace rootModule do
+ emitImport "Wayland.Display"
+ emitLocalImport protocol.name ".Header"
+ emitEventDefinitions protocol
+ emitInterfaceInstances protocol
+
+end Interface
+
+section Resolved
+
+private def emitResolvedInterfaces (protocol : ProtocolDesc) : Generator Unit := do
+ for iface in protocol.interfaces do
+ emitLine s!"instance : ResolvedInterface {iface.name.pascalCase}.name where"
+ emitLine s!" referencedInterfaces := #["
+ for ref in iface.referencedInterfaces do
+ let name ← resolveInterface ref (suffix := ".Interface")
+ emitLine s!" ⟨{name}.name, inferInstance⟩,"
+ emitLine s!" ]"
+ emitLine s!""
+
+def generateResolved (rootModule : String) (protocol : ProtocolDesc) : String :=
+ Generator.runProtocol rootModule protocol ".Resolved" do
+ emitNamespace rootModule do
+ emitImport "Wayland.Display"
+ emitLocalImport protocol.name ".Interface"
+ emitResolvedInterfaces protocol
+
+end Resolved
+
+section Requests
+
+private def emitRequests (protocol : ProtocolDesc) : Generator Unit := do
+ for iface in protocol.interfaces do
+ for req in iface.requests do
+ emitLine s!""
+ emitLine s!"def {iface.name.pascalCase}.{req.name.camelCase}"
+ emitLine s!" (ω : {iface.name.pascalCase})"
+ -- TODO: Special wl_callback handling
+ for arg in req.arguments do
+ let argName := arg.name.camelCase
+ match arg.type with
+ | .int .none => emitLine s!" ({argName} : Int32)"
+ | .int (.some enum) => emitLine s!" ({argName} : {← resolveEnum enum})"
+ | .uInt .none => emitLine s!" ({argName} : UInt32)"
+ | .uInt (.some enum) => emitLine s!" ({argName} : {← resolveEnum enum})"
+ | .fixed => emitLine s!" ({argName} : Float)"
+ | .string .nullable => emitLine s!" ({argName} : Option String)"
+ | .string .notNull => emitLine s!" ({argName} : String)"
+ | .array => emitLine s!" ({argName} : ByteArray)"
+ | .fd => emitLine s!" ({argName} : Int32)"
+ | .object .nullable .none => emitLine s!" ({argName} : Option AnyObject)"
+ | .object .nullable (.some iface) => emitLine s!" ({argName} : Option {← resolveInterface iface (suffix := ".Resolved")})"
+ | .object .notNull .none => emitLine s!" ({argName} : AnyObject)"
+ | .object .notNull (.some iface) => emitLine s!" ({argName} : {← resolveInterface iface (suffix := ".Resolved")})"
+ match req.returnType with
+ | .unit => emitLine s!" : DisplayM σ Unit :="
+ | .object .none => emitLine s!" : DisplayM σ AnyObject :="
+ | .object (.some iface) => emitLine s!" : DisplayM σ {← resolveInterface iface (suffix := ".Resolved")} :="
+ emitLine s!" sorry"
+ -- TODO
+
+def generateRequests (rootModule : String) (protocol : ProtocolDesc) : String :=
+ Generator.runProtocol rootModule protocol ".Requests" do
+ emitNamespace rootModule do
+ emitImport "Wayland.Display"
+ emitLocalImport protocol.name ".Resolved"
+ emitLine "variable {σ : Type}"
+ emitRequests protocol
+
+end Requests
+
+section Umbrella
+
+def generateUmbrella (rootModule : String) (protocol : ProtocolDesc) : String :=
+ Generator.runProtocol rootModule protocol "" do
+ emitLocalImport protocol.name ".Header"
+ emitLocalImport protocol.name ".Interface"
+ emitLocalImport protocol.name ".Resolved"
+ emitLocalImport protocol.name ".Requests"
+
+end Umbrella
+
+section Index
+
+def generateIndex (rootModule : String) (protocols : Array ProtocolDesc) : String :=
+ Generator.runIndex rootModule do
+ for protocol in protocols do
+ emitLocalImport protocol.name
+
+end Index
+
+end WaylandScanner
diff --git a/tools/Scanner/Parser.lean b/tools/Scanner/Parser.lean
index f89c239..5ee867b 100644
--- a/tools/Scanner/Parser.lean
+++ b/tools/Scanner/Parser.lean
@@ -93,9 +93,10 @@ private def ArgumentType.ofString : String → Except String ArgumentType
private def processDescription (el : Xml.Element) : Except String Description := do
el.ensureName "description"
+ let body := el.textContent
return {
summary := el.getAttribute "summary"
- body := el.textContent
+ body := if body.isEmpty then .none else .some body
}
private def processEnumEntry (el : Xml.Element) : Except String EnumEntryDesc := do
diff --git a/tools/Scanner/Processor.lean b/tools/Scanner/Processor.lean
index d591ee7..22148ed 100644
--- a/tools/Scanner/Processor.lean
+++ b/tools/Scanner/Processor.lean
@@ -21,9 +21,12 @@ private abbrev InterfaceMap := Std.TreeMap String InterfaceInfo
private structure Context where
interfaces : InterfaceMap
currentInterface : Client.InterfaceRef
+
+private structure TrackingState where
referencedInterfaces : Std.TreeSet Client.InterfaceRef
-private abbrev Processor : Type → Type := StateT Context (Except String)
+private abbrev Processor : Type → Type := ReaderT Context (Except String)
+private abbrev TrackingProcessor : Type → Type := StateT TrackingState Processor
private def processEnumEntry (raw : Raw.EnumEntryDesc) : Processor Client.EnumEntryDesc := do
return {
@@ -35,11 +38,11 @@ private def processEnumEntry (raw : Raw.EnumEntryDesc) : Processor Client.EnumEn
}
private def interfaceInfo (name : String) : Processor InterfaceInfo := do
- match (← get).interfaces.get? name with
+ match (← read).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
+private def resolveInterface (name : String) : TrackingProcessor Client.InterfaceRef := do
let info ← interfaceInfo name
let ref := {
moduleName := info.moduleName
@@ -52,7 +55,7 @@ private def resolveInterface (name : String) : Processor Client.InterfaceRef :=
private def resolveEnum (name : String) : Processor Client.EnumRef := do
let (interface, enum) ←
match (name.split ".").toArray with
- | #[enum] => pure ((← get).currentInterface.typeName, enum.toString)
+ | #[enum] => pure ((← read).currentInterface.typeName, enum.toString)
| #[interface, enum] => pure (interface.toString, enum.toString)
| _ => throw s!"Malformed enum reference {name}"
let info ← interfaceInfo interface
@@ -66,20 +69,20 @@ private def resolveEnum (name : String) : Processor Client.EnumRef := do
private def processEnum (raw : Raw.EnumDesc) : Processor Client.EnumDesc := do
return {
- name := raw.name
+ name := if raw.name != "event" then raw.name else "event'" -- We define an `Iface.Event` type, so avoid any possible conflicts.
description := raw.description
since := raw.since
bitfield := raw.bitfield
entries := ← raw.entries.mapM processEnumEntry
}
-private def processArgument (raw : Raw.ArgumentDesc) : Processor Client.ArgumentDesc := do
+private def processArgument (raw : Raw.ArgumentDesc) : TrackingProcessor 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
+ | .int => Client.ArgumentType.int <$> raw.enum.mapM (liftM ∘ resolveEnum)
+ | .uInt => Client.ArgumentType.uInt <$> raw.enum.mapM (liftM ∘ resolveEnum)
| .fixed => Client.ArgumentType.fixed |> pure
| .string => Client.ArgumentType.string (.ofAllowNull raw.allowNull) |> pure
| .array => Client.ArgumentType.array |> pure
@@ -89,7 +92,7 @@ private def processArgument (raw : Raw.ArgumentDesc) : Processor Client.Argument
description := raw.description
}
-private def processRequest (raw : Raw.MessageDesc) : Processor Client.RequestDesc := do
+private def processRequest (raw : Raw.MessageDesc) : TrackingProcessor 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 ←
@@ -104,11 +107,12 @@ private def processRequest (raw : Raw.MessageDesc) : Processor Client.RequestDes
isDestructor := raw.type == .destructor
since := raw.since
deprecatedSince := raw.deprecatedSince
+ rawArguments := raw.arguments
arguments := ← otherArgs.mapM processArgument
returnType := returnType
}
-private def processEvent (raw : Raw.MessageDesc) : Processor Client.EventDesc := do
+private def processEvent (raw : Raw.MessageDesc) : TrackingProcessor Client.EventDesc := do
return {
name := raw.name
opcode := raw.opcode
@@ -116,14 +120,16 @@ private def processEvent (raw : Raw.MessageDesc) : Processor Client.EventDesc :=
isDestructor := raw.type == .destructor
since := raw.since
deprecatedSince := raw.deprecatedSince
+ rawArguments := raw.arguments
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
+ let state : TrackingState := {
+ referencedInterfaces := { (← read).currentInterface }
+ }
+ let (requests, state) ← StateT.run (raw.requests.mapM processRequest) state
+ let (events, state) ← StateT.run (raw.events.mapM processEvent) state
return {
name := raw.name
version := raw.version
@@ -131,7 +137,7 @@ private def processInterface (raw : Raw.InterfaceDesc) : Processor Client.Interf
enums := ← raw.enums.mapM processEnum
requests := requests
events := events
- referencedInterfaces := referencedInterfaces
+ referencedInterfaces := state.referencedInterfaces
}
private def processProtocol (interfaces : InterfaceMap) (raw : Raw.ProtocolDesc) : Except String Client.ProtocolDesc := do
@@ -140,10 +146,9 @@ private def processProtocol (interfaces : InterfaceMap) (raw : Raw.ProtocolDesc)
copyright := raw.copyright
description := raw.description
interfaces := ← raw.interfaces.mapM
- fun iface ↦ (processInterface iface).run' {
+ fun iface ↦ (processInterface iface).run {
interfaces := interfaces
currentInterface := { moduleName := raw.name, typeName := iface.name }
- referencedInterfaces := .empty
}
}
diff --git a/tools/Scanner/Protocol.lean b/tools/Scanner/Protocol.lean
index 77908d9..6f74126 100644
--- a/tools/Scanner/Protocol.lean
+++ b/tools/Scanner/Protocol.lean
@@ -15,6 +15,32 @@ def Description.ofSummary (s : String) : Description :=
def Identifier := String
deriving Repr, BEq, Ord, Inhabited
+def Identifier.quoted (ident : Identifier) : String :=
+ let s : String := ident
+ s!"\"{s}\""
+
+private def Identifier.pascalCase' (parts : List String.Slice) : String :=
+ parts
+ |>.map (String.capitalize ∘ String.Slice.toString)
+ |> String.join
+
+private def sanitize (s : String) : String :=
+ let isInvalid :=
+ ((0 : String.Pos.Raw).get s).isDigit || s == "class"
+ if isInvalid then "_" ++ s else s
+
+def Identifier.pascalCase (ident : Identifier) : String :=
+ ident
+ |>.split "_"
+ |>.toList
+ |> pascalCase'
+ |> sanitize
+
+def Identifier.camelCase (ident : Identifier) : String :=
+ match (ident.split "_").toList with
+ | [] => ""
+ | x::xs => sanitize (x.toString ++ pascalCase' xs)
+
namespace Raw
structure EnumEntryDesc where
@@ -145,6 +171,7 @@ structure MessageDesc where
since : Nat
deprecatedSince : Option Nat
arguments : Array ArgumentDesc
+ rawArguments : Array Raw.ArgumentDesc
deriving Repr, BEq, Inhabited
inductive ReturnType where
generated by cgit v1.3.1 (git 2.54.0) at 2026-11-10 12:09:16 +0000