module Generic.Unsafe.PrimAtom.ComplexExample where

open import Generic.Core hiding (natAtom; stringAtom; boolAtom)
open import Generic.PrimAtom
open import Generic.Unsafe.PrimAtom.Macro

data RichDocument : Type₀
data BlockList : Type₀
data RichBlock : Type₀

data RichDocument where
  document : String → BlockList → RichDocument

data BlockList where
  blocks-done : BlockList
  blocks-cons : RichBlock → BlockList → BlockList

data RichBlock where
  paragraph   : String → RichBlock
  titled-section : String → BlockList → RichBlock
  quote-block : BlockList → RichBlock

documentI : Fin 3
documentI = Fin.zero

blockListI : Fin 3
blockListI = Fin.suc Fin.zero

richBlockI : Fin 3
richBlockI = Fin.suc (Fin.suc Fin.zero)

RichDocumentDesc : Fin 3 → TyDesc PrimAtoms 3
RichDocumentDesc Fin.zero =
  dataD (κ₂ (α stringAtom) (μ blockListI) ∷ [])
RichDocumentDesc (Fin.suc Fin.zero) =
  dataD (κ₀ ∷ κ₂ (μ richBlockI) (μ blockListI) ∷ [])
RichDocumentDesc (Fin.suc (Fin.suc Fin.zero)) =
  dataD
    ( κ₁ (α stringAtom)
    ∷ κ₂ (α stringAtom) (μ blockListI)
    ∷ κ₁ (μ blockListI)
    ∷ [] )

mutual
  encodeRichDocument :
    RichDocument →
    CodeIx PrimAtoms RichDocumentDesc (RichDocumentDesc documentI)
  encodeRichDocument (document title blocks) =
    ν₂ ι₀ (atomIx title) (recIx (encodeBlockList blocks))

  encodeBlockList :
    BlockList →
    CodeIx PrimAtoms RichDocumentDesc (RichDocumentDesc blockListI)
  encodeBlockList blocks-done = ν₀ ι₀
  encodeBlockList (blocks-cons block rest) =
    ν₂ ι₁ (recIx (encodeRichBlock block)) (recIx (encodeBlockList rest))

  encodeRichBlock :
    RichBlock →
    CodeIx PrimAtoms RichDocumentDesc (RichDocumentDesc richBlockI)
  encodeRichBlock (paragraph text) =
    ν₁ ι₀ (atomIx text)
  encodeRichBlock (titled-section title blocks) =
    ν₂ ι₁ (atomIx title) (recIx (encodeBlockList blocks))
  encodeRichBlock (quote-block blocks) =
    ν₁ ι₂ (recIx (encodeBlockList blocks))

mutual
  decodeRichDocument :
    CodeIx PrimAtoms RichDocumentDesc (RichDocumentDesc documentI) →
    RichDocument
  decodeRichDocument (ν₂ ι₀ (atomIx title) (recIx blocks)) =
    document title (decodeBlockList blocks)

  decodeBlockList :
    CodeIx PrimAtoms RichDocumentDesc (RichDocumentDesc blockListI) →
    BlockList
  decodeBlockList (ν₀ ι₀) = blocks-done
  decodeBlockList (ν₂ ι₁ (recIx block) (recIx rest)) =
    blocks-cons (decodeRichBlock block) (decodeBlockList rest)

  decodeRichBlock :
    CodeIx PrimAtoms RichDocumentDesc (RichDocumentDesc richBlockI) →
    RichBlock
  decodeRichBlock (ν₁ ι₀ (atomIx text)) =
    paragraph text
  decodeRichBlock (ν₂ ι₁ (atomIx title) (recIx blocks)) =
    titled-section title (decodeBlockList blocks)
  decodeRichBlock (ν₁ ι₂ (recIx blocks)) =
    quote-block (decodeBlockList blocks)

mutual
  decode-encodeRichDocument :
    (x : RichDocument) →
    decodeRichDocument (encodeRichDocument x) ≡ x
  decode-encodeRichDocument (document title blocks) =
    cong (document title) (decode-encodeBlockList blocks)

  decode-encodeBlockList :
    (x : BlockList) →
    decodeBlockList (encodeBlockList x) ≡ x
  decode-encodeBlockList blocks-done = refl
  decode-encodeBlockList (blocks-cons block rest) =
    cong₂ blocks-cons
      (decode-encodeRichBlock block)
      (decode-encodeBlockList rest)

  decode-encodeRichBlock :
    (x : RichBlock) →
    decodeRichBlock (encodeRichBlock x) ≡ x
  decode-encodeRichBlock (paragraph text) = refl
  decode-encodeRichBlock (titled-section title blocks) =
    cong (titled-section title) (decode-encodeBlockList blocks)
  decode-encodeRichBlock (quote-block blocks) =
    cong quote-block (decode-encodeBlockList blocks)

mutual
  encode-decodeRichDocument :
    (x : CodeIx PrimAtoms RichDocumentDesc (RichDocumentDesc documentI)) →
    encodeRichDocument (decodeRichDocument x) ≡ x
  encode-decodeRichDocument (ν₂ ι₀ (atomIx title) (recIx blocks)) =
    cong (λ ys → ν₂ ι₀ (atomIx title) (recIx ys))
      (encode-decodeBlockList blocks)

  encode-decodeBlockList :
    (x : CodeIx PrimAtoms RichDocumentDesc (RichDocumentDesc blockListI)) →
    encodeBlockList (decodeBlockList x) ≡ x
  encode-decodeBlockList (ν₀ ι₀) = refl
  encode-decodeBlockList (ν₂ ι₁ (recIx block) (recIx rest)) =
    cong₂ (λ b r → ν₂ ι₁ (recIx b) (recIx r))
      (encode-decodeRichBlock block)
      (encode-decodeBlockList rest)

  encode-decodeRichBlock :
    (x : CodeIx PrimAtoms RichDocumentDesc (RichDocumentDesc richBlockI)) →
    encodeRichBlock (decodeRichBlock x) ≡ x
  encode-decodeRichBlock (ν₁ ι₀ (atomIx text)) = refl
  encode-decodeRichBlock (ν₂ ι₁ (atomIx title) (recIx blocks)) =
    cong (λ ys → ν₂ ι₁ (atomIx title) (recIx ys))
      (encode-decodeBlockList blocks)
  encode-decodeRichBlock (ν₁ ι₂ (recIx blocks)) =
    cong (λ ys → ν₁ ι₂ (recIx ys))
      (encode-decodeBlockList blocks)

encodeRichDocumentRoot :
  RichDocument →
  RootCodeIx PrimAtoms RichDocumentDesc (rootData documentI)
encodeRichDocumentRoot x = rootDataIx (encodeRichDocument x)

decodeRichDocumentRoot :
  RootCodeIx PrimAtoms RichDocumentDesc (rootData documentI) →
  RichDocument
decodeRichDocumentRoot (rootDataIx x) = decodeRichDocument x

decode-encodeRichDocumentRoot :
  (x : RichDocument) →
  decodeRichDocumentRoot (encodeRichDocumentRoot x) ≡ x
decode-encodeRichDocumentRoot = decode-encodeRichDocument

encode-decodeRichDocumentRoot :
  (x : RootCodeIx PrimAtoms RichDocumentDesc (rootData documentI)) →
  encodeRichDocumentRoot (decodeRichDocumentRoot x) ≡ x
encode-decodeRichDocumentRoot (rootDataIx x) =
  cong rootDataIx (encode-decodeRichDocument x)

richDocumentTypeNames : Fin 3 → String
richDocumentTypeNames Fin.zero = "RichDocument"
richDocumentTypeNames (Fin.suc Fin.zero) = "BlockList"
richDocumentTypeNames (Fin.suc (Fin.suc Fin.zero)) = "RichBlock"

richDocumentConstructorNames : Fin 3 → List String
richDocumentConstructorNames Fin.zero =
  "document" ∷ []
richDocumentConstructorNames (Fin.suc Fin.zero) =
  "blocks-done" ∷ "blocks-cons" ∷ []
richDocumentConstructorNames (Fin.suc (Fin.suc Fin.zero)) =
  "paragraph" ∷ "titled-section" ∷ "quote-block" ∷ []

genericRichDocument : Generic PrimAtoms RichDocument
genericRichDocument =
  generic 3 RichDocumentDesc (rootData documentI)
    richDocumentTypeNames
    richDocumentConstructorNames
    encodeRichDocumentRoot decodeRichDocumentRoot
    decode-encodeRichDocumentRoot encode-decodeRichDocumentRoot

sampleRichDocument : RichDocument
sampleRichDocument =
  document "Manual"
    (blocks-cons
      (titled-section "Intro"
        (blocks-cons (paragraph "hello") blocks-done))
      (blocks-cons
        (quote-block
          (blocks-cons (paragraph "quote") blocks-done))
        blocks-done))

mockedRichDocument : RichDocument
mockedRichDocument =
  choosePrimAtomValueMock
    genericRichDocument
    "[[],[\"Manual\",[[[]],[[[[]],[\"Intro\",[[[]],[[[],[\"hello\"]],[[],[]]]]]],[[[]],[[[[[]]],[[[[]],[[[],[\"quote\"]],[[],[]]]]]],[[],[]]]]]]]]"

mockedRichDocument-ok : mockedRichDocument ≡ sampleRichDocument
mockedRichDocument-ok = refl