diff options
Diffstat (limited to 'tools/Scanner')
| -rw-r--r-- | tools/Scanner/Generator.lean | 16 | ||||
| -rw-r--r-- | tools/Scanner/Parser.lean | 2 | ||||
| -rw-r--r-- | tools/Scanner/Processor.lean | 18 | ||||
| -rw-r--r-- | tools/Scanner/Protocol.lean | 58 |
4 files changed, 47 insertions, 47 deletions
diff --git a/tools/Scanner/Generator.lean b/tools/Scanner/Generator.lean index 1ac8139..5884a0d 100644 --- a/tools/Scanner/Generator.lean +++ b/tools/Scanner/Generator.lean @@ -61,12 +61,12 @@ private def Generator.runIndex (rootModule : String) (gen : Generator Unit) : St 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 + emitLocalImport iface.protocol suffix + return iface.interface.pascalCase private def resolveEnum (enum : EnumRef) : Generator String := do let iface ← resolveInterface enum.toInterfaceRef - return s!"{iface}.{enum.enumName.pascalCase}" + return s!"{iface}.{enum.enum.pascalCase}" section Header @@ -114,8 +114,8 @@ private def emitEventDefinitions (protocol : ProtocolDesc) : Generator Unit := d 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})" + | .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)" @@ -140,7 +140,7 @@ private def emitInterfaceInstances (protocol : ProtocolDesc) : Generator Unit := let argumentDesc (arg : Raw.ArgumentDesc) : String := match arg.type with | .int => ".int" - | .uInt => ".uint" + | .uint => ".uint" | .fixed => ".fixed" | .string => s!".string {nullability arg}" | .object => s!".object {nullability arg} {interfaceName arg}" @@ -216,8 +216,8 @@ private def emitRequests (protocol : ProtocolDesc) : Generator Unit := do 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})" + | .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)" diff --git a/tools/Scanner/Parser.lean b/tools/Scanner/Parser.lean index 5ee867b..5d4e837 100644 --- a/tools/Scanner/Parser.lean +++ b/tools/Scanner/Parser.lean @@ -82,7 +82,7 @@ private def MessageType.ofString : String → Except String MessageType private def ArgumentType.ofString : String → Except String ArgumentType | "int" => .ok .int -| "uint" => .ok .uInt +| "uint" => .ok .uint | "fixed" => .ok .fixed | "string" => .ok .string | "array" => .ok .array diff --git a/tools/Scanner/Processor.lean b/tools/Scanner/Processor.lean index 22148ed..513d89f 100644 --- a/tools/Scanner/Processor.lean +++ b/tools/Scanner/Processor.lean @@ -13,7 +13,7 @@ from other protocols. Thus, this needs to be done after parsing all protocols. namespace WaylandScanner private structure InterfaceInfo where - moduleName : Identifier + protocol : Identifier enums : Array Identifier private abbrev InterfaceMap := Std.TreeMap String InterfaceInfo @@ -45,8 +45,8 @@ private def interfaceInfo (name : String) : Processor InterfaceInfo := do private def resolveInterface (name : String) : TrackingProcessor Client.InterfaceRef := do let info ← interfaceInfo name let ref := { - moduleName := info.moduleName - typeName := name + protocol := info.protocol + interface := name } let old ← get set { old with referencedInterfaces := old.referencedInterfaces.insert ref } @@ -55,16 +55,16 @@ 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.typeName, enum.toString) + | #[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}" return { - moduleName := info.moduleName - typeName := interface - enumName := enum + protocol := info.protocol + interface + enum } private def processEnum (raw : Raw.EnumDesc) : Processor Client.EnumDesc := do @@ -82,7 +82,7 @@ private def processArgument (raw : Raw.ArgumentDesc) : TrackingProcessor Client. type := ← match raw.type with | .int => Client.ArgumentType.int <$> raw.enum.mapM (liftM ∘ resolveEnum) - | .uInt => Client.ArgumentType.uInt <$> 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 @@ -148,7 +148,7 @@ private def processProtocol (interfaces : InterfaceMap) (raw : Raw.ProtocolDesc) interfaces := ← raw.interfaces.mapM fun iface ↦ (processInterface iface).run { interfaces := interfaces - currentInterface := { moduleName := raw.name, typeName := iface.name } + currentInterface := { protocol := raw.name, interface := iface.name } } } diff --git a/tools/Scanner/Protocol.lean b/tools/Scanner/Protocol.lean index 6f74126..183ef6a 100644 --- a/tools/Scanner/Protocol.lean +++ b/tools/Scanner/Protocol.lean @@ -60,15 +60,15 @@ structure EnumDesc where deriving Repr, BEq, Inhabited inductive ArgumentType where -| int -| uInt -| fixed -| string -| array -| fd -| newID -| object -deriving Repr, BEq, Inhabited + | int + | uint + | fixed + | string + | array + | fd + | newID + | object + deriving Repr, BEq, Inhabited structure ArgumentDesc where name : String @@ -80,9 +80,9 @@ structure ArgumentDesc where deriving Repr, BEq, Inhabited inductive MessageType where -| normal -| destructor -deriving Repr, BEq, Inhabited + | normal + | destructor + deriving Repr, BEq, Inhabited structure MessageDesc where name : String @@ -115,12 +115,12 @@ end Raw namespace Client structure InterfaceRef where - moduleName : Identifier - typeName : Identifier + protocol : Identifier + interface : Identifier deriving Repr, BEq, Ord, Inhabited structure EnumRef extends InterfaceRef where - enumName : Identifier + enum : Identifier deriving Repr, BEq, Ord, Inhabited structure EnumEntryDesc where @@ -140,22 +140,22 @@ structure EnumDesc where deriving Repr, BEq, Inhabited inductive Nullability where -| nullable -| notNull -deriving Repr, BEq, Inhabited + | nullable + | notNull + deriving Repr, BEq, Inhabited 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, Inhabited + | int (enum : Option EnumRef) + | uint (enum : Option EnumRef) + | fixed + | string (nullability : Nullability) + | array + | fd + | object (nullability : Nullability) (interface : Option InterfaceRef) + deriving Repr, BEq, Inhabited structure ArgumentDesc where name : Identifier @@ -175,9 +175,9 @@ structure MessageDesc where deriving Repr, BEq, Inhabited inductive ReturnType where -| unit -| object (type : Option InterfaceRef) -deriving Repr, BEq, Inhabited + | unit + | object (type : Option InterfaceRef) + deriving Repr, BEq, Inhabited structure RequestDesc extends MessageDesc where returnType : ReturnType |