From 4119fa8c0c59bb39f9aeba7f479067fd834c4e20 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Fri, 3 Apr 2026 23:38:07 +0200 Subject: resolve types in protocols --- tools/Scanner.lean | 11 ++-- tools/Scanner/Parser.lean | 2 + tools/Scanner/Processor.lean | 137 +++++++++++++++++++++++++++++++++++++++++++ tools/Scanner/Protocol.lean | 117 +++++++++++++++++++++++++++++++++--- 4 files changed, 254 insertions(+), 13 deletions(-) create mode 100644 tools/Scanner/Processor.lean (limited to 'tools') diff --git a/tools/Scanner.lean b/tools/Scanner.lean index d6962c7..81b4181 100644 --- a/tools/Scanner.lean +++ b/tools/Scanner.lean @@ -1,22 +1,25 @@ import Scanner.Protocol import Scanner.Parser +import Scanner.Processor open WaylandScanner -def parseProtocol (path : System.FilePath) : IO ProtocolDesc := do +def parseRawProtocol (path : System.FilePath) : IO Raw.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) + let rawProtocols ← (← srcPath.readDir) |>.map IO.FS.DirEntry.path - |>.mapM parseProtocol + |>.mapM parseRawProtocol + let clientProtocols ← processProtocols rawProtocols + |> IO.ofExcept let rootModuleComponents := rootModule.split "." |>.map String.Slice.toString |>.toArray let rootModulePath := rootModuleComponents.foldl (· / ·) outPath - IO.println (reprStr protocols) + IO.println (reprStr clientProtocols) IO.FS.createDirAll rootModulePath let indexPath := rootModulePath.addExtension "lean" IO.FS.writeFile indexPath "" diff --git a/tools/Scanner/Parser.lean b/tools/Scanner/Parser.lean index 3bdb7b6..630b3fc 100644 --- a/tools/Scanner/Parser.lean +++ b/tools/Scanner/Parser.lean @@ -68,6 +68,8 @@ open Lean namespace WaylandScanner +open Raw + private def MessageType.ofString : String → Except String MessageType | "destructor" => .ok .destructor | s => .error s!"Expected \"destructor\", but got {s}" diff --git a/tools/Scanner/Processor.lean b/tools/Scanner/Processor.lean new file mode 100644 index 0000000..fad25bc --- /dev/null +++ b/tools/Scanner/Processor.lean @@ -0,0 +1,137 @@ +import Scanner.Protocol +import Std.Data.TreeMap + +namespace WaylandScanner + +private structure InterfaceInfo where + moduleName : Identifier + enums : Array Identifier + +private abbrev InterfaceMap := Std.TreeMap String InterfaceInfo + +private structure Context where + interfaces : InterfaceMap + currentInterface : Identifier + +private abbrev Processor : Type → Type := ReaderT Context (Except String) + +private def processEnumEntry (raw : Raw.EnumEntryDesc) : Processor Client.EnumEntryDesc := do + return { + name := raw.name + value := raw.value + description := raw.description + since := raw.since + deprecatedSince := raw.deprecatedSince + } + +private def interfaceInfo (name : String) : Processor InterfaceInfo := do + 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 + let info ← interfaceInfo name + return { + moduleName := info.moduleName + typeName := name + } + +private def resolveEnum (name : String) : Processor Client.EnumRef := do + let (interface, enum) ← + match (name.split ".").toArray with + | #[enum] => pure ((← read).currentInterface, enum.toString) + | #[interface, enum] => pure (interface.toString, enum.toString) + | _ => throw s!"Malformed enum reference {name}" + let info ← interfaceInfo interface + if not (info.enums.contains enum) then + throw s!"Interface {repr interface} does not contain enum {repr enum}" + return { + moduleName := info.moduleName + typeName := interface + enumName := enum + } + +private def processEnum (raw : Raw.EnumDesc) : Processor Client.EnumDesc := do + return { + name := raw.name + description := raw.description + since := raw.since + bitfield := raw.bitfield + entries := ← raw.entries.mapM processEnumEntry + } + +private def processArgument (raw : Raw.ArgumentDesc) : Processor 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 + | .fixed => Client.ArgumentType.fixed |> pure + | .string => Client.ArgumentType.string (.ofAllowNull raw.allowNull) |> pure + | .array => Client.ArgumentType.array |> pure + | .fd => Client.ArgumentType.fd |> pure + | .newID => Client.ArgumentType.object .notNull <$> raw.interface.mapM resolveInterface + | .object => Client.ArgumentType.object (.ofAllowNull raw.allowNull) <$> raw.interface.mapM resolveInterface + description := raw.description + } + +private def processRequest (raw : Raw.MessageDesc) : Processor 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 ← + match newIDArgs with + | #[] => Client.ReturnType.unit |> pure + | #[arg] => Client.ReturnType.object <$> arg.interface.mapM resolveInterface + | _ => throw s!"Expected at most one new_id argument for request in {raw.name}" + return { + name := raw.name + opcode := raw.opcode + description := raw.description + isDestructor := raw.type == .destructor + since := raw.since + deprecatedSince := raw.deprecatedSince + arguments := ← otherArgs.mapM processArgument + returnType := returnType + } + +private def processEvent (raw : Raw.MessageDesc) : Processor Client.EventDesc := do + return { + name := raw.name + opcode := raw.opcode + description := raw.description + isDestructor := raw.type == .destructor + since := raw.since + deprecatedSince := raw.deprecatedSince + arguments := ← raw.arguments.mapM processArgument + } + +private def processInterface (raw : Raw.InterfaceDesc) : Processor Client.InterfaceDesc := do + return { + name := raw.name + version := raw.version + description := raw.description + enums := ← raw.enums.mapM processEnum + requests := ← raw.requests.mapM processRequest + events := ← raw.events.mapM processEvent + } + +private def processProtocol (interfaces : InterfaceMap) (raw : Raw.ProtocolDesc) : Except String Client.ProtocolDesc := do + return { + name := raw.name + copyright := raw.copyright + description := raw.description + interfaces := ← raw.interfaces.mapM + fun iface ↦ (processInterface iface).run { + interfaces := interfaces + currentInterface := iface.name + } + } + +def processProtocols (raw : Array Raw.ProtocolDesc) : Except String (Array Client.ProtocolDesc) := + let interfaces : InterfaceMap := .ofArray <| raw.flatMap + fun protocol ↦ protocol.interfaces.map + fun iface ↦ (iface.name, (⟨protocol.name, iface.enums.map Raw.EnumDesc.name⟩ : InterfaceInfo)) + raw.mapM (processProtocol interfaces) + +end WaylandScanner diff --git a/tools/Scanner/Protocol.lean b/tools/Scanner/Protocol.lean index 6c9a838..0ead630 100644 --- a/tools/Scanner/Protocol.lean +++ b/tools/Scanner/Protocol.lean @@ -3,19 +3,25 @@ namespace WaylandScanner structure Description where summary : Option String body : Option String - deriving Repr + deriving Repr, BEq def Description.ofSummary (s : String) : Description := { summary := s body := .none } +/-! Identifiers, stored in their original representation (i.e., camel case). -/ +def Identifier := String + deriving Repr, BEq + +namespace Raw + structure EnumEntryDesc where name : String value : Int description : Option Description since : Nat deprecatedSince : Option Nat - deriving Repr + deriving Repr, BEq structure EnumDesc where name : String @@ -23,7 +29,7 @@ structure EnumDesc where since : Nat bitfield : Bool entries: Array EnumEntryDesc - deriving Repr + deriving Repr, BEq inductive ArgumentType where | int @@ -34,7 +40,7 @@ inductive ArgumentType where | fd | newID | object -deriving Repr +deriving Repr, BEq structure ArgumentDesc where name : String @@ -43,12 +49,12 @@ structure ArgumentDesc where interface : Option String enum : Option String allowNull : Bool - deriving Repr + deriving Repr, BEq inductive MessageType where | normal | destructor -deriving Repr +deriving Repr, BEq structure MessageDesc where name : String @@ -58,7 +64,7 @@ structure MessageDesc where since : Nat deprecatedSince : Option Nat arguments : Array ArgumentDesc - deriving Repr + deriving Repr, BEq structure InterfaceDesc where name : String @@ -67,13 +73,106 @@ structure InterfaceDesc where enums : Array EnumDesc requests : Array MessageDesc events : Array MessageDesc - deriving Repr + deriving Repr, BEq structure ProtocolDesc where name : String copyright : Option String description : Option Description interfaces : Array InterfaceDesc - deriving Repr + deriving Repr, BEq + +end Raw + +namespace Client + +structure InterfaceRef where + moduleName : Identifier + typeName : Identifier + deriving Repr, BEq + +structure EnumRef extends InterfaceRef where + enumName : Identifier + deriving Repr, BEq + +structure EnumEntryDesc where + name : Identifier + value : Int + description : Option Description + since : Nat + deprecatedSince : Option Nat + deriving Repr, BEq + +structure EnumDesc where + name : Identifier + description : Option Description + since : Nat + bitfield : Bool + entries: Array EnumEntryDesc + deriving Repr, BEq + +inductive Nullability where +| nullable +| notNull +deriving Repr, BEq + +def Nullability.ofAllowNull (allowNull : Bool) : Nullability := + if allowNull then .nullable else .notNull + +inductive ArgumentType where +| int (enum : Option EnumRef) +| uInt (enum : Option EnumRef) +| fixed +| string (nullability : Nullability) +| array +| fd +| object (nullability : Nullability) (interface : Option InterfaceRef) +deriving Repr, BEq + +structure ArgumentDesc where + name : Identifier + type : ArgumentType + description : Option Description + deriving Repr, BEq + +structure MessageDesc where + name : Identifier + opcode : Nat + description : Option Description + isDestructor : Bool + since : Nat + deprecatedSince : Option Nat + arguments : Array ArgumentDesc + deriving Repr, BEq + +inductive ReturnType where +| unit +| object (type : Option InterfaceRef) +deriving Repr, BEq + +structure RequestDesc extends MessageDesc where + returnType : ReturnType + deriving Repr, BEq + +structure EventDesc extends MessageDesc + deriving Repr, BEq + +structure InterfaceDesc where + name : Identifier + version : Nat + description : Option Description + enums : Array EnumDesc + requests : Array RequestDesc + events : Array EventDesc + deriving Repr, BEq + +structure ProtocolDesc where + name : Identifier + copyright : Option String + description : Option Description + interfaces : Array InterfaceDesc + deriving Repr, BEq + +end Client end WaylandScanner -- cgit v1.3.1