module Generic.Unsafe.PrimAtom.MacroComplexExample where

open import Generic.Core hiding (natAtom; stringAtom; boolAtom)
open import Generic.Macro
open import Generic.Macro.Family using (deriveGenericReachableIn)
open import Generic.PrimAtom
open import Generic.Unsafe.PrimAtom.FamilyMacro
open import Generic.Unsafe.PrimAtom.Macro

data WorkflowEvent : Type₀ where
  created        : String → String → WorkflowEvent
  assigned       : String → String → String → WorkflowEvent
  status-change  : String → String → String → String → WorkflowEvent
  comment-added  : String → String → String → WorkflowEvent
  attachment     : String → String → String → String → String → WorkflowEvent
  closed         : String → String → WorkflowEvent
  reopened       : String → String → String → WorkflowEvent
  heartbeat      : WorkflowEvent

genericWorkflowEvent : Generic PrimAtoms WorkflowEvent
genericWorkflowEvent = deriveGenericIn PrimAtoms WorkflowEvent

sampleWorkflowEvent : WorkflowEvent
sampleWorkflowEvent =
  status-change "ticket-17" "triage" "review" "Ada"

mockedWorkflowEvent : WorkflowEvent
mockedWorkflowEvent =
  choosePrimAtomValueMock
    genericWorkflowEvent
    "[[[[]]],[\"ticket-17\",\"triage\",\"review\",\"Ada\"]]"

mockedWorkflowEvent-ok :
  mockedWorkflowEvent ≡ sampleWorkflowEvent
mockedWorkflowEvent-ok = refl

record ReleaseCard : Type₀ where
  constructor release-card
  field
    releaseName : String
    owner       : String
    branch      : String
    summary     : String
    risk        : String
    rollback    : String

genericReleaseCard : Generic PrimAtoms ReleaseCard
genericReleaseCard = deriveGenericIn PrimAtoms ReleaseCard

sampleReleaseCard : ReleaseCard
sampleReleaseCard =
  release-card
    "v1.4.0"
    "Marcin"
    "main"
    "generic UI improvements"
    "medium"
    "revert commit"

mockedReleaseCard : ReleaseCard
mockedReleaseCard =
  choosePrimAtomValueMock
    genericReleaseCard
    "[[],[\"v1.4.0\",\"Marcin\",\"main\",\"generic UI improvements\",\"medium\",\"revert commit\"]]"

mockedReleaseCard-ok :
  mockedReleaseCard ≡ sampleReleaseCard
mockedReleaseCard-ok = refl

data MacroTree : Type₀ where
  macro-leaf   : String → MacroTree
  macro-branch : String → MacroTree → MacroTree → MacroTree

genericMacroTree : Generic PrimAtoms MacroTree
genericMacroTree = deriveStringFamily1 MacroTree

sampleMacroTree : MacroTree
sampleMacroTree =
  macro-branch "root" (macro-leaf "left") (macro-leaf "right")

mockedMacroTree : MacroTree
mockedMacroTree =
  choosePrimAtomValueMock
    genericMacroTree
    "[[[]],[\"root\",[[],[\"left\"]],[[],[\"right\"]]]]"

mockedMacroTree-ok :
  mockedMacroTree ≡ sampleMacroTree
mockedMacroTree-ok = refl

-- data MacroEven : Type₀
-- data MacroOdd : Type₀

-- data MacroEven where
--   macro-even-zero : MacroEven
--   macro-even-suc  : MacroOdd → MacroEven

-- data MacroOdd where
--   macro-odd-suc : String → MacroEven → MacroOdd

-- genericMacroEven : Generic PrimAtoms MacroEven
-- genericMacroEven =
--   deriveStringFamily2 MacroEven MacroOdd MacroEven

-- genericMacroOdd : Generic PrimAtoms MacroOdd
-- genericMacroOdd =
--   deriveStringFamily2 MacroEven MacroOdd MacroOdd

-- sampleMacroEven : MacroEven
-- sampleMacroEven =
--   macro-even-suc (macro-odd-suc "step" macro-even-zero)

-- mockedMacroEven : MacroEven
-- mockedMacroEven =
--   choosePrimAtomValueMock
--     genericMacroEven
--     "[[[]],[[[],[\"step\",[[],[]]]]]]"

-- mockedMacroEven-ok :
--   mockedMacroEven ≡ sampleMacroEven
-- mockedMacroEven-ok = refl

-- sampleMacroOdd : MacroOdd
-- sampleMacroOdd =
--   macro-odd-suc "outer"
--     (macro-even-suc (macro-odd-suc "inner" macro-even-zero))

-- mockedMacroOdd : MacroOdd
-- mockedMacroOdd =
--   choosePrimAtomValueMock
--     genericMacroOdd
--     "[[],[\"outer\",[[[]],[[[],[\"inner\",[[],[]]]]]]]]"

-- mockedMacroOdd-ok :
--   mockedMacroOdd ≡ sampleMacroOdd
-- mockedMacroOdd-ok = refl

-- data BindMacroExpr : Type₀
-- data BindMacro : Type₀

-- data BindMacroExpr where
--   bind-var   : String → BindMacroExpr
--   bind-text  : String → BindMacroExpr
--   bind-apply : BindMacroExpr → BindMacroExpr → BindMacroExpr
--   bind-let   : BindMacro → BindMacroExpr → BindMacroExpr

-- data BindMacro where
--   bind-one : String → BindMacroExpr → BindMacro
--   bind-seq : BindMacro → BindMacro → BindMacro

-- genericBindMacroExpr : Generic PrimAtoms BindMacroExpr
-- genericBindMacroExpr = deriveGenericReachableIn PrimAtoms BindMacroExpr

-- genericBindMacro : Generic PrimAtoms BindMacro
-- genericBindMacro = deriveGenericReachableIn PrimAtoms BindMacro

-- sampleBindMacro : BindMacro
-- sampleBindMacro =
--   bind-seq
--     (bind-one "x" (bind-text "hello"))
--     (bind-one "f" (bind-apply (bind-var "x") (bind-text "world")))

-- mockedBindMacro : BindMacro
-- mockedBindMacro =
--   choosePrimAtomValueMock
--     genericBindMacro
--     "[[[]],[[[],[\"x\",[[[]],[\"hello\"]]]],[[],[\"f\",[[[[]]],[[[],[\"x\"]],[[[]],[\"world\"]]]]]]]]"

-- mockedBindMacro-ok :
--   mockedBindMacro ≡ sampleBindMacro
-- mockedBindMacro-ok = refl

-- sampleBindMacroExpr : BindMacroExpr
-- sampleBindMacroExpr =
--   bind-let sampleBindMacro (bind-apply (bind-var "f") (bind-text "again"))

-- mockedBindMacroExpr : BindMacroExpr
-- mockedBindMacroExpr =
--   choosePrimAtomValueMock
--     genericBindMacroExpr
--     "[[[[[]]]],[[[[]],[[[],[\"x\",[[[]],[\"hello\"]]]],[[],[\"f\",[[[[]]],[[[],[\"x\"]],[[[]],[\"world\"]]]]]]]],[[[[]]],[[[],[\"f\"]],[[[]],[\"again\"]]]]]]"

-- mockedBindMacroExpr-ok :
--   mockedBindMacroExpr ≡ sampleBindMacroExpr
-- mockedBindMacroExpr-ok = refl