import Std.Data.TreeSet

namespace WaylandScanner

structure Description where
  summary : Option String
  body : Option String
  deriving Repr, BEq, Inhabited

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, Ord, Inhabited

def Identifier.quoted (ident : Identifier) : String :=
  let s : String := ident
  s!"\"{s}\""

private def Identifier.pascalCase' (parts : List String.Slice) : String :=
  parts
    |>.map (String.capitalize ∘ String.Slice.toString)
    |> String.join

private def sanitize (s : String) : String :=
  let isInvalid :=
    ((0 : String.Pos.Raw).get s).isDigit || s == "class"
  if isInvalid then "_" ++ s else s

def Identifier.pascalCase (ident : Identifier) : String :=
  ident
    |>.split "_"
    |>.toList
    |> pascalCase'
    |> sanitize

def Identifier.camelCase (ident : Identifier) : String :=
  match (ident.split "_").toList with
  | [] => ""
  | x::xs => sanitize (x.toString ++ pascalCase' xs)

namespace Raw

structure EnumEntryDesc where
  name : String
  value : Int
  description : Option Description
  since : Nat
  deprecatedSince : Option Nat
  deriving Repr, BEq, Inhabited

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

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

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

inductive MessageType where
  | normal
  | destructor
  deriving Repr, BEq, Inhabited

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

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

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

end Raw

namespace Client

structure InterfaceRef where
  protocol : Identifier
  interface : Identifier
  deriving Repr, BEq, Ord, Inhabited

structure EnumRef extends InterfaceRef where
  enum : Identifier
  deriving Repr, BEq, Ord, Inhabited

structure EnumEntryDesc where
  name : Identifier
  value : Int
  description : Option Description
  since : Nat
  deprecatedSince : Option Nat
  deriving Repr, BEq, Inhabited

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

inductive Nullability where
  | nullable
  | notNull
  deriving Repr, BEq, Inhabited

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, Inhabited

structure ArgumentDesc where
  name : Identifier
  type : ArgumentType
  description : Option Description
  deriving Repr, BEq, Inhabited

structure MessageDesc where
  name : Identifier
  opcode : Nat
  description : Option Description
  isDestructor : Bool
  since : Nat
  deprecatedSince : Option Nat
  arguments : Array ArgumentDesc
  rawArguments : Array Raw.ArgumentDesc
  deriving Repr, BEq, Inhabited

inductive ReturnType where
  | unit
  | object (type : Option InterfaceRef)
  deriving Repr, BEq, Inhabited

structure RequestDesc extends MessageDesc where
  returnType : ReturnType
  deriving Repr, BEq, Inhabited

structure EventDesc extends MessageDesc
  deriving Repr, BEq, Inhabited

structure InterfaceDesc where
  name : Identifier
  version : Nat
  description : Option Description
  enums : Array EnumDesc
  requests : Array RequestDesc
  events : Array EventDesc
  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, Inhabited

end Client

end WaylandScanner