From 1f5491a5af7bd0f1ec4046994d6344886465cba5 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sun, 5 Apr 2026 16:15:03 +0200 Subject: initial codegen --- tools/Scanner/Processor.lean | 39 ++++++++++++++++++++++----------------- 1 file changed, 22 insertions(+), 17 deletions(-) (limited to 'tools/Scanner/Processor.lean') 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 } } -- cgit v1.3.1