resolve types in protocols

4 files changed, 254 insertions, 13 deletions

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