resolve types in protocols

1 files changed, 108 insertions, 9 deletions

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