import Scanner.Protocol
import Scanner.Xml.Basic
import Scanner.Xml.Parser

/-!
# Parsing of Protocol Description

This converts a protocol description XML into a `Raw.ProtocolDesc`.
-/

private def String.toNat (s : String) : Except String Nat :=
  match Lean.Syntax.decodeNatLitVal? s with
    | .some n => .ok n
    | .none => .error s!"Expected a natural number, but got {s}"

private def String.toBool : String → Except String Bool
  | "true" => .ok true
  | "false" => .ok false
  | s => .error s!"Expected a boolean value, but got {s}"

namespace Lean.Xml

private def Element.name : Xml.Element → String
  | .Element name _ _ => name

private def Element.attributes : Xml.Element → Xml.Attributes
  | .Element _ attrs _ => attrs

private def Element.content : Xml.Element → Array Xml.Content
  | .Element _ _ content => content

private def Element.ensureName (el : Xml.Element) (name : String) : Except String Unit :=
  if name == el.name
  then .ok ()
  else .error s!"Invalid tag: Expected {name}, but got {el.name}"

private def Element.textContent (el : Xml.Element) : String :=
  let reformat (str : String) : String :=
    str
    |>.split "\n"
    |>.map (String.Slice.trimAscii)
    |>.map (String.Slice.toString)
    |>.toList
    |> String.intercalate "\n"
    |>.trimAscii
    |>.toString
  reformat <| String.join <| Array.toList <| el.content.flatMap fun
    | .Element _ => #[]
    | .Comment _ => #[]
    | .Character s => #[s]

private def Element.getChildrenByName (el : Xml.Element) (name : String) : Array Xml.Element :=
  el.content.flatMap fun
    | .Element child => if child.name == name then #[child] else #[]
    | .Comment _ => #[]
    | .Character _ => #[]

private def Element.getChildByName (el : Xml.Element) (name : String) : Option Xml.Element :=
  match el.getChildrenByName name with
    | #[single] => .some single
    | _ => .none

private def Element.getAttribute (el : Xml.Element) (attr : String) : Option String :=
  el.attributes.get? attr

private def Element.getRequiredAttribute (el : Xml.Element) (attr : String) : Except String String :=
  el.getAttribute attr
    |>.map pure
    |>.getD (.error s!"Missing required attribute {attr}")

end Lean.Xml

open Lean

namespace WaylandScanner

open Raw

private def MessageType.ofString : String → Except String MessageType
  | "destructor" => .ok .destructor
  | s => .error s!"Expected \"destructor\", but got {s}"

private def ArgumentType.ofString : String → Except String ArgumentType
  | "int" => .ok .int
  | "uint" => .ok .uint
  | "fixed" => .ok .fixed
  | "string" => .ok .string
  | "array" => .ok .array
  | "fd" => .ok .fd
  | "new_id" => .ok .newID
  | "object" => .ok .object
  | s => .error s!"Expected an argument type, but got {s}"

private def processDescription (el : Xml.Element) : Except String Description := do
  el.ensureName "description"
  let body := el.textContent
  return {
    summary := el.getAttribute "summary"
    body := if body.isEmpty then .none else .some body
  }

private def processEnumEntry (el : Xml.Element) : Except String EnumEntryDesc := do
  el.ensureName "entry"
  let name ← el.getRequiredAttribute "name"
  let value ← (← el.getRequiredAttribute "value")
    |>.toNat
  let description ← el.getChildByName "description"
    |>.mapM processDescription
  let summary := el.getAttribute "summary"
  let since ← el.getAttribute "since"
    |>.mapM String.toNat
  let deprecatedSince ← el.getAttribute "deprecated-since"
    |>.mapM String.toNat
  return {
    name := name
    value := value
    description := description <|> summary.map Description.ofSummary
    since := since.getD 1
    deprecatedSince := deprecatedSince
  }

private def processEnum (el : Xml.Element) : Except String EnumDesc := do
  el.ensureName "enum"
  let name ← el.getRequiredAttribute "name"
  let description ← el.getChildByName "description"
    |>.mapM processDescription
  let since ← el.getAttribute "since"
    |>.mapM String.toNat
  let bitfield ← el.getAttribute "bitfield"
    |>.mapM String.toBool
  let entries ← el.getChildrenByName "entry"
    |>.mapM processEnumEntry
  return {
    name := name
    description := description
    since := since.getD 1
    bitfield := bitfield.getD false
    entries := entries
  }

private def processArgument (el : Xml.Element) : Except String ArgumentDesc := do
  el.ensureName "arg"
  let name ← el.getRequiredAttribute "name"
  let type ← (← el.getRequiredAttribute "type")
    |> ArgumentType.ofString
  let description ← el.getChildByName "description"
    |>.mapM processDescription
  let summary := el.getAttribute "summary"
  let interface := el.getAttribute "interface"
  let enum := el.getAttribute "enum"
  let allowNull ← el.getAttribute "allow-null"
    |>.mapM String.toBool
  return {
    name := name
    type := type
    description := description <|> summary.map Description.ofSummary
    interface := interface
    enum := enum
    allowNull := allowNull.getD false
  }

private def processMessage (opcode : Nat) (el : Xml.Element) : Except String MessageDesc := do
  let name ← el.getRequiredAttribute "name"
  let description ← el.getChildByName "description"
    |>.mapM processDescription
  let type ← el.getAttribute "type"
    |>.mapM MessageType.ofString
  let since ← el.getAttribute "since"
    |>.mapM String.toNat
  let deprecatedSince ← el.getAttribute "deprecated-since"
    |>.mapM String.toNat
  let args ← el.getChildrenByName "arg"
    |>.mapM processArgument
  return {
    name := name
    opcode := opcode
    description := description
    type := type.getD .normal
    since := since.getD 1
    deprecatedSince := deprecatedSince
    arguments := args
  }

private def processInterface (el : Xml.Element) : Except String InterfaceDesc := do
  el.ensureName "interface"
  let name ← el.getRequiredAttribute "name"
  let version ← (← el.getRequiredAttribute "version")
    |>.toNat
  let description ← el.getChildByName "description"
    |>.mapM processDescription
  let enums ← el.getChildrenByName "enum"
    |>.mapM processEnum
  let requests ← el.getChildrenByName "request"
    |>.mapIdxM processMessage
  let events ← el.getChildrenByName "event"
    |>.mapIdxM processMessage
  return {
    name := name
    version := version
    description := description
    enums := enums
    requests := requests
    events := events
  }

private def processProtocol (el : Xml.Element) : Except String ProtocolDesc := do
  el.ensureName "protocol"
  let name ← el.getRequiredAttribute "name"
  let copyright := el.getChildByName "copyright"
    |>.map Xml.Element.textContent
  let description ← el.getChildByName "description"
    |>.mapM processDescription
  let interfaces ← el.getChildrenByName "interface"
    |>.mapM processInterface
  return {
    name := name
    copyright := copyright
    description := description
    interfaces := interfaces
  }

def parse (text : String) : Except String ProtocolDesc :=
  Xml.parse text >>= processProtocol

end WaylandScanner