transitive closure of interface dependencies

1 files changed, 26 insertions, 24 deletions

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