summaryrefslogtreecommitdiff
path: root/tools/Scanner/Processor.lean
diff options
context:
space:
mode:
authorHannes Schulze <haschu0103@outlook.de>2026-04-05 16:20:10 +0200
committerHannes Schulze <haschu0103@outlook.de>2026-04-05 16:20:10 +0200
commitd47eacf3939411aff7ca0badbed1d1f2f5494969 (patch)
tree59b3dcc6f420d01be1463ea5971ad4e795586a5c /tools/Scanner/Processor.lean
parent1a59b19a615483ade6284e554c53f17afabb7287 (diff)
further cleanup
Diffstat (limited to 'tools/Scanner/Processor.lean')
-rw-r--r--tools/Scanner/Processor.lean42
1 files changed, 21 insertions, 21 deletions
diff --git a/tools/Scanner/Processor.lean b/tools/Scanner/Processor.lean
index 513d89f..a50767f 100644
--- a/tools/Scanner/Processor.lean
+++ b/tools/Scanner/Processor.lean
@@ -39,8 +39,8 @@ private def processEnumEntry (raw : Raw.EnumEntryDesc) : Processor Client.EnumEn
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}"
+ | .some info => pure info
+ | .none => .error s!"Unable to find referenced interface {name}"
private def resolveInterface (name : String) : TrackingProcessor Client.InterfaceRef := do
let info ← interfaceInfo name
@@ -55,9 +55,9 @@ private def resolveInterface (name : String) : TrackingProcessor Client.Interfac
private def resolveEnum (name : String) : Processor Client.EnumRef := do
let (interface, enum) ←
match (name.split ".").toArray with
- | #[enum] => pure ((← read).currentInterface.interface, enum.toString)
- | #[interface, enum] => pure (interface.toString, enum.toString)
- | _ => throw s!"Malformed enum reference {name}"
+ | #[enum] => pure ((← read).currentInterface.interface, 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}"
@@ -81,14 +81,14 @@ private def processArgument (raw : Raw.ArgumentDesc) : TrackingProcessor Client.
name := raw.name
type :=
← match raw.type with
- | .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
- | .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
+ | .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
+ | .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
}
@@ -97,9 +97,9 @@ private def processRequest (raw : Raw.MessageDesc) : TrackingProcessor Client.Re
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}"
+ | #[] => 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
@@ -158,11 +158,11 @@ private partial def transitiveClosure (protocols : Array Client.ProtocolDesc) :
fun protocol ↦ protocol.interfaces.map
fun iface ↦ ((⟨protocol.name, iface.name⟩ : Client.InterfaceRef), iface.referencedInterfaces.toList)
let rec dfs : Std.TreeSet Client.InterfaceRef → List Client.InterfaceRef → Std.TreeSet Client.InterfaceRef
- | visited, [] => visited
- | visited, (x::xs) =>
- if visited.contains x
- then dfs visited xs
- else dfs (visited.insert x) (successors.get! x ++ xs)
+ | visited, [] => visited
+ | visited, (x::xs) =>
+ if visited.contains x
+ then dfs visited xs
+ else dfs (visited.insert x) (successors.get! x ++ xs)
let interfaceClosure (iface : Client.InterfaceDesc) : Client.InterfaceDesc :=
{ iface with referencedInterfaces := dfs .empty iface.referencedInterfaces.toList }
let protocolClosure (protocol : Client.ProtocolDesc) : Client.ProtocolDesc :=