some cleanup

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