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