transitive closure of interface dependencies

3 files changed, 67 insertions, 33 deletions

diff --git a/tools/Scanner/Parser.lean b/tools/Scanner/Parser.lean
index 630b3fc..f89c239 100644
--- a/tools/Scanner/Parser.lean
+++ b/tools/Scanner/Parser.lean
@@ -2,6 +2,12 @@ import Scanner.Protocol
 import Lean.Data.Xml.Basic
 import Lean.Data.Xml.Parser
 
+/-!
+# Parsing of Protocol Description
+
+This converts a protocol description XML into a `Raw.ProtocolDesc`.
+-/
+
 private def String.toNat (s : String) : Except String Nat :=
   match Lean.Syntax.decodeNatLitVal? s with
   | .some n => .ok n
diff --git a/tools/Scanner/Processor.lean b/tools/Scanner/Processor.lean
index 88853a6..d591ee7 100644
--- a/tools/Scanner/Processor.lean
+++ b/tools/Scanner/Processor.lean
@@ -1,5 +1,14 @@
 import Scanner.Protocol
 import Std.Data.TreeMap
+import Std.Data.TreeSet
+
+/-!
+# Processing of Protocol Descriptions
+
+This is mainly used to resolve interface/enum references within protocols, converting a `Raw.ProtocolDesc` into a
+`Client.ProtocolDesc`. Note that this requires a global view of all protocols since interfaces can mention interfaces
+from other protocols. Thus, this needs to be done after parsing all protocols.
+-/
 
 namespace WaylandScanner
 
@@ -12,7 +21,7 @@ private abbrev InterfaceMap := Std.TreeMap String InterfaceInfo
 private structure Context where
   interfaces : InterfaceMap
   currentInterface : Client.InterfaceRef
-  referencedInterfaces : Array Client.InterfaceRef
+  referencedInterfaces : Std.TreeSet Client.InterfaceRef
 
 private abbrev Processor : Type → Type := StateT Context (Except String)
 
@@ -37,7 +46,7 @@ private def resolveInterface (name : String) : Processor Client.InterfaceRef :=
     typeName := name
   }
   let old ← get
-  set { old with referencedInterfaces := old.referencedInterfaces ++ #[ref] }
+  set { old with referencedInterfaces := old.referencedInterfaces.insert ref }
   return ref
 
 private def resolveEnum (name : String) : Processor Client.EnumRef := do
@@ -114,7 +123,7 @@ private def processInterface (raw : Raw.InterfaceDesc) : Processor Client.Interf
   let requests ← raw.requests.mapM processRequest
   let events ← raw.events.mapM processEvent
   let state ← get
-  let referencedInterfaces := state.referencedInterfaces ++ #[state.currentInterface]
+  let referencedInterfaces := state.referencedInterfaces.insert state.currentInterface
   return {
     name := raw.name
     version := raw.version
@@ -123,9 +132,6 @@ private def processInterface (raw : Raw.InterfaceDesc) : Processor Client.Interf
     requests := requests
     events := events
     referencedInterfaces := referencedInterfaces
-      |>.toList
-      |>.eraseDups
-      |>.toArray
   }
 
 private def processProtocol (interfaces : InterfaceMap) (raw : Raw.ProtocolDesc) : Except String Client.ProtocolDesc := do
@@ -137,14 +143,34 @@ private def processProtocol (interfaces : InterfaceMap) (raw : Raw.ProtocolDesc)
       fun iface ↦ (processInterface iface).run' {
         interfaces := interfaces
         currentInterface := { moduleName := raw.name, typeName := iface.name }
-        referencedInterfaces := #[]
+        referencedInterfaces := .empty
       }
   }
 
-def processProtocols (raw : Array Raw.ProtocolDesc) : Except String (Array Client.ProtocolDesc) :=
+/-! Compute the transitive closure w.r.t. `referencedInterfaces`. -/
+private partial def transitiveClosure (protocols : Array Client.ProtocolDesc) : Array Client.ProtocolDesc :=
+  let successors : Std.TreeMap Client.InterfaceRef (List Client.InterfaceRef) := .ofArray <| protocols.flatMap
+    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)
+  let interfaceClosure (iface : Client.InterfaceDesc) : Client.InterfaceDesc :=
+    { iface with referencedInterfaces := dfs .empty iface.referencedInterfaces.toList }
+  let protocolClosure (protocol : Client.ProtocolDesc) : Client.ProtocolDesc :=
+    { protocol with interfaces := protocol.interfaces.map interfaceClosure }
+  protocols.map protocolClosure
+
+-- TODO: Correctness proof for `transitiveClosure`
+
+def processProtocols (raw : Array Raw.ProtocolDesc) : Except String (Array Client.ProtocolDesc) := do
   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)
+  let res ← raw.mapM (processProtocol interfaces)
+  return transitiveClosure res
 
 end WaylandScanner
diff --git a/tools/Scanner/Protocol.lean b/tools/Scanner/Protocol.lean
index c90ab56..77908d9 100644
--- a/tools/Scanner/Protocol.lean
+++ b/tools/Scanner/Protocol.lean
@@ -1,9 +1,11 @@
+import Std.Data.TreeSet
+
 namespace WaylandScanner
 
 structure Description where
   summary : Option String
   body : Option String
-  deriving Repr, BEq
+  deriving Repr, BEq, Inhabited
 
 def Description.ofSummary (s : String) : Description :=
   { summary := s
@@ -11,7 +13,7 @@ def Description.ofSummary (s : String) : Description :=
 
 /-! Identifiers, stored in their original representation (i.e., camel case). -/
 def Identifier := String
-  deriving Repr, BEq
+  deriving Repr, BEq, Ord, Inhabited
 
 namespace Raw
 
@@ -21,7 +23,7 @@ structure EnumEntryDesc where
   description : Option Description
   since : Nat
   deprecatedSince : Option Nat
-  deriving Repr, BEq
+  deriving Repr, BEq, Inhabited
 
 structure EnumDesc where
   name : String
@@ -29,7 +31,7 @@ structure EnumDesc where
   since : Nat
   bitfield : Bool
   entries: Array EnumEntryDesc
-  deriving Repr, BEq
+  deriving Repr, BEq, Inhabited
 
 inductive ArgumentType where
 | int
@@ -40,7 +42,7 @@ inductive ArgumentType where
 | fd
 | newID
 | object
-deriving Repr, BEq
+deriving Repr, BEq, Inhabited
 
 structure ArgumentDesc where
   name : String
@@ -49,12 +51,12 @@ structure ArgumentDesc where
   interface : Option String
   enum : Option String
   allowNull : Bool
-  deriving Repr, BEq
+  deriving Repr, BEq, Inhabited
 
 inductive MessageType where
 | normal
 | destructor
-deriving Repr, BEq
+deriving Repr, BEq, Inhabited
 
 structure MessageDesc where
   name : String
@@ -64,7 +66,7 @@ structure MessageDesc where
   since : Nat
   deprecatedSince : Option Nat
   arguments : Array ArgumentDesc
-  deriving Repr, BEq
+  deriving Repr, BEq, Inhabited
 
 structure InterfaceDesc where
   name : String
@@ -73,14 +75,14 @@ structure InterfaceDesc where
   enums : Array EnumDesc
   requests : Array MessageDesc
   events : Array MessageDesc
-  deriving Repr, BEq
+  deriving Repr, BEq, Inhabited
 
 structure ProtocolDesc where
   name : String
   copyright : Option String
   description : Option Description
   interfaces : Array InterfaceDesc
-  deriving Repr, BEq
+  deriving Repr, BEq, Inhabited
 
 end Raw
 
@@ -89,11 +91,11 @@ namespace Client
 structure InterfaceRef where
   moduleName : Identifier
   typeName : Identifier
-  deriving Repr, BEq
+  deriving Repr, BEq, Ord, Inhabited
 
 structure EnumRef extends InterfaceRef where
   enumName : Identifier
-  deriving Repr, BEq
+  deriving Repr, BEq, Ord, Inhabited
 
 structure EnumEntryDesc where
   name : Identifier
@@ -101,7 +103,7 @@ structure EnumEntryDesc where
   description : Option Description
   since : Nat
   deprecatedSince : Option Nat
-  deriving Repr, BEq
+  deriving Repr, BEq, Inhabited
 
 structure EnumDesc where
   name : Identifier
@@ -109,12 +111,12 @@ structure EnumDesc where
   since : Nat
   bitfield : Bool
   entries: Array EnumEntryDesc
-  deriving Repr, BEq
+  deriving Repr, BEq, Inhabited
 
 inductive Nullability where
 | nullable
 | notNull
-deriving Repr, BEq
+deriving Repr, BEq, Inhabited
 
 def Nullability.ofAllowNull (allowNull : Bool) : Nullability :=
   if allowNull then .nullable else .notNull
@@ -127,13 +129,13 @@ inductive ArgumentType where
 | array
 | fd
 | object (nullability : Nullability) (interface : Option InterfaceRef)
-deriving Repr, BEq
+deriving Repr, BEq, Inhabited
 
 structure ArgumentDesc where
   name : Identifier
   type : ArgumentType
   description : Option Description
-  deriving Repr, BEq
+  deriving Repr, BEq, Inhabited
 
 structure MessageDesc where
   name : Identifier
@@ -143,19 +145,19 @@ structure MessageDesc where
   since : Nat
   deprecatedSince : Option Nat
   arguments : Array ArgumentDesc
-  deriving Repr, BEq
+  deriving Repr, BEq, Inhabited
 
 inductive ReturnType where
 | unit
 | object (type : Option InterfaceRef)
-deriving Repr, BEq
+deriving Repr, BEq, Inhabited
 
 structure RequestDesc extends MessageDesc where
   returnType : ReturnType
-  deriving Repr, BEq
+  deriving Repr, BEq, Inhabited
 
 structure EventDesc extends MessageDesc
-  deriving Repr, BEq
+  deriving Repr, BEq, Inhabited
 
 structure InterfaceDesc where
   name : Identifier
@@ -164,15 +166,15 @@ structure InterfaceDesc where
   enums : Array EnumDesc
   requests : Array RequestDesc
   events : Array EventDesc
-  referencedInterfaces : Array InterfaceRef
-  deriving Repr, BEq
+  referencedInterfaces : Std.TreeSet InterfaceRef
+  deriving Repr, BEq, Inhabited
 
 structure ProtocolDesc where
   name : Identifier
   copyright : Option String
   description : Option Description
   interfaces : Array InterfaceDesc
-  deriving Repr, BEq
+  deriving Repr, BEq, Inhabited
 
 end Client