namespace WaylandScanner

structure Description where
  summary : Option String
  body : Option String
  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, BEq

structure EnumDesc where
  name : String
  description : Option Description
  since : Nat
  bitfield : Bool
  entries: Array EnumEntryDesc
  deriving Repr, BEq

inductive ArgumentType where
| int
| uInt
| fixed
| string
| array
| fd
| newID
| object
deriving Repr, BEq

structure ArgumentDesc where
  name : String
  type : ArgumentType
  description : Option Description
  interface : Option String
  enum : Option String
  allowNull : Bool
  deriving Repr, BEq

inductive MessageType where
| normal
| destructor
deriving Repr, BEq

structure MessageDesc where
  name : String
  opcode : Nat
  description : Option Description
  type : MessageType
  since : Nat
  deprecatedSince : Option Nat
  arguments : Array ArgumentDesc
  deriving Repr, BEq

structure InterfaceDesc where
  name : String
  version : Nat
  description : Option Description
  enums : Array EnumDesc
  requests : Array MessageDesc
  events : Array MessageDesc
  deriving Repr, BEq

structure ProtocolDesc where
  name : String
  copyright : Option String
  description : Option Description
  interfaces : Array InterfaceDesc
  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
  referencedInterfaces : Array InterfaceRef
  deriving Repr, BEq

structure ProtocolDesc where
  name : Identifier
  copyright : Option String
  description : Option Description
  interfaces : Array InterfaceDesc
  deriving Repr, BEq

end Client

end WaylandScanner