1 files changed, 79 insertions, 0 deletions
diff --git a/tools/Scanner/Protocol.lean b/tools/Scanner/Protocol.lean
new file mode 100644
index 0000000..6c9a838
--- /dev/null
+++ b/tools/Scanner/Protocol.lean
@@ -0,0 +1,79 @@
+namespace WaylandScanner
+
+structure Description where
+  summary : Option String
+  body : Option String
+  deriving Repr
+
+def Description.ofSummary (s : String) : Description :=
+  { summary := s
+    body := .none }
+
+structure EnumEntryDesc where
+  name : String
+  value : Int
+  description : Option Description
+  since : Nat
+  deprecatedSince : Option Nat
+  deriving Repr
+
+structure EnumDesc where
+  name : String
+  description : Option Description
+  since : Nat
+  bitfield : Bool
+  entries: Array EnumEntryDesc
+  deriving Repr
+
+inductive ArgumentType where
+| int
+| uInt
+| fixed
+| string
+| array
+| fd
+| newID
+| object
+deriving Repr
+
+structure ArgumentDesc where
+  name : String
+  type : ArgumentType
+  description : Option Description
+  interface : Option String
+  enum : Option String
+  allowNull : Bool
+  deriving Repr
+
+inductive MessageType where
+| normal
+| destructor
+deriving Repr
+
+structure MessageDesc where
+  name : String
+  opcode : Nat
+  description : Option Description
+  type : MessageType
+  since : Nat
+  deprecatedSince : Option Nat
+  arguments : Array ArgumentDesc
+  deriving Repr
+
+structure InterfaceDesc where
+  name : String
+  version : Nat
+  description : Option Description
+  enums : Array EnumDesc
+  requests : Array MessageDesc
+  events : Array MessageDesc
+  deriving Repr
+
+structure ProtocolDesc where
+  name : String
+  copyright : Option String
+  description : Option Description
+  interfaces : Array InterfaceDesc
+  deriving Repr
+
+end WaylandScanner