diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/Scanner.lean | 25 | ||||
| -rw-r--r-- | tools/Scanner/Generator.lean | 267 | ||||
| -rw-r--r-- | tools/Scanner/Parser.lean | 3 | ||||
| -rw-r--r-- | tools/Scanner/Processor.lean | 39 | ||||
| -rw-r--r-- | tools/Scanner/Protocol.lean | 27 |
5 files changed, 340 insertions, 21 deletions
diff --git a/tools/Scanner.lean b/tools/Scanner.lean index 81b4181..1daed2a 100644 --- a/tools/Scanner.lean +++ b/tools/Scanner.lean @@ -1,6 +1,7 @@ import Scanner.Protocol import Scanner.Parser import Scanner.Processor +import Scanner.Generator open WaylandScanner @@ -9,6 +10,24 @@ def parseRawProtocol (path : System.FilePath) : IO Raw.ProtocolDesc := do |>.mapError (fun ε ↦ s!"{path}: {ε}") |> IO.ofExcept +def writeProtocol (protocol : Client.ProtocolDesc) (rootModule : String) (rootModulePath : System.FilePath) : IO Unit := do + let protocolPath := rootModulePath / protocol.name.pascalCase + IO.FS.createDirAll protocolPath + let umbrellaPath := protocolPath.addExtension "lean" + IO.FS.writeFile umbrellaPath <| generateUmbrella rootModule protocol + let headerPath := protocolPath / "Header.lean" + IO.FS.writeFile headerPath <| generateHeader rootModule protocol + let interfacePath := protocolPath / "Interface.lean" + IO.FS.writeFile interfacePath <| generateInterface rootModule protocol + let resolvedPath := protocolPath / "Resolved.lean" + IO.FS.writeFile resolvedPath <| generateResolved rootModule protocol + let requestsPath := protocolPath / "Requests.lean" + IO.FS.writeFile requestsPath <| generateRequests rootModule protocol + +def writeIndex (protocols : Array Client.ProtocolDesc) (rootModule : String) (rootModulePath : System.FilePath) : IO Unit := do + let indexPath := rootModulePath.addExtension "lean" + IO.FS.writeFile indexPath <| generateIndex rootModule protocols + def process (rootModule : String) (outPath : System.FilePath) (srcPath : System.FilePath) : IO UInt32 := do let rawProtocols ← (← srcPath.readDir) |>.map IO.FS.DirEntry.path @@ -19,10 +38,10 @@ def process (rootModule : String) (outPath : System.FilePath) (srcPath : System. |>.map String.Slice.toString |>.toArray let rootModulePath := rootModuleComponents.foldl (· / ·) outPath - IO.println (reprStr clientProtocols) IO.FS.createDirAll rootModulePath - let indexPath := rootModulePath.addExtension "lean" - IO.FS.writeFile indexPath "" + for protocol in clientProtocols do + writeProtocol protocol rootModule rootModulePath + writeIndex clientProtocols rootModule rootModulePath return 0 def usage : IO UInt32 := do 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 |