module Generic.Unsafe.PrimAtom.MockTest where

open import Agda.Builtin.Nat using (Nat)

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

mockedString : String
mockedString =
  choosePrimAtomValueMock (atomicGeneric PrimAtoms stringAtom) "\"hello\""

mockedString-ok : mockedString ≡ "hello"
mockedString-ok = refl

mockedStringSource : String
mockedStringSource =
  choosePrimAtomValueSourceMock
    (atomicGeneric PrimAtoms stringAtom)
    "\"legacy source\""

mockedStringSource-ok : mockedStringSource ≡ "legacy source"
mockedStringSource-ok = refl

data MockAction : Type₀ where
  mock-note    : String → MockAction
  mock-rename  : String → String → MockAction
  mock-publish : String → String → String → MockAction
  mock-archive : String → MockAction
  mock-no-op   : MockAction

genericMockAction : Generic PrimAtoms MockAction
genericMockAction = deriveGenericIn PrimAtoms MockAction

mockedPublish : MockAction
mockedPublish =
  choosePrimAtomValueMock
    genericMockAction
    "[[[[]]],[\"draft\",\"owner\",\"body\"]]"

mockedPublish-ok :
  mockedPublish ≡ mock-publish "draft" "owner" "body"
mockedPublish-ok = refl

record MockTicket : Type₀ where
  constructor mock-ticket
  field
    title : String
    owner : String
    body  : String

genericMockTicket : Generic PrimAtoms MockTicket
genericMockTicket = deriveGenericIn PrimAtoms MockTicket

certifiedMockTicket : CertifiedGeneric PrimAtoms MockTicket
certifiedMockTicket = deriveCertifiedGenericIn PrimAtoms MockTicket

mockedTicket : MockTicket
mockedTicket =
  choosePrimAtomValueMock
    genericMockTicket
    "[[],[\"A title\",\"Ada\",\"Details\"]]"

mockedTicket-ok :
  mockedTicket ≡ mock-ticket "A title" "Ada" "Details"
mockedTicket-ok = refl

mockedTicketSource : MockTicket
mockedTicketSource =
  choosePrimAtomValueSourceMock
    genericMockTicket
    "[[],[\"Source title\",\"Grace\",\"Escape path\"]]"

mockedTicketSource-ok :
  mockedTicketSource ≡ mock-ticket "Source title" "Grace" "Escape path"
mockedTicketSource-ok = refl

mockedCertifiedTicket : MockTicket
mockedCertifiedTicket =
  chooseCertifiedPrimAtomValueMock
    certifiedMockTicket
    "[[],[\"Certified\",\"Ada\",\"Structured renderer\"]]"

mockedCertifiedTicket-ok :
  mockedCertifiedTicket ≡ mock-ticket "Certified" "Ada" "Structured renderer"
mockedCertifiedTicket-ok = refl

record MockAtomForm : Type₀ where
  constructor mock-atom-form
  field
    label   : String
    count   : Nat
    offset  : Int
    enabled : Bool

genericMockAtomForm : Generic PrimAtoms MockAtomForm
genericMockAtomForm = deriveGenericIn PrimAtoms MockAtomForm

mockedAtomForm : MockAtomForm
mockedAtomForm =
  choosePrimAtomValueMock
    genericMockAtomForm
    "[[],[\"alpha\",3,[\"negsuc\",1],true]]"

mockedAtomForm-ok :
  mockedAtomForm ≡
    mock-atom-form "alpha" (suc (suc (suc zero))) (negsuc (suc zero)) true
mockedAtomForm-ok = refl