module Generic.CanonicalJson where

open import Generic.Core
open import Generic.Json

open import Cubical.Data.Maybe.Base using (Maybe; just; nothing)
import Cubical.Data.Maybe.Properties as MaybeProperties
import Cubical.Data.Empty as Empty
import Cubical.Data.FinData.Base as FinData
import FF.Json as Json

record CanonicalFromToJSON' {ℓA ℓJ} (J : Json.AtomUniverse ℓJ)
                            (A : Type ℓA) : Type (ℓ-max ℓA ℓJ) where
  constructor canonicalFromToJSON'
  field
    codec : Json.FromToJSON' J A
    canonical : (j : Json.Json J) → (x : A) →
                fromJSONWith codec j ≡ just x →
                toJSONWith codec x ≡ j

open CanonicalFromToJSON' public

CanonicalAtomCodeCodec : ∀ {ℓ ℓJ} →
                         Json.AtomUniverse ℓJ → AtomUniverse ℓ →
                         Type (ℓ-max ℓJ ℓ-zero)
CanonicalAtomCodeCodec J U = CanonicalFromToJSON' J (AtomCode U)

CanonicalAtomValueCodecs : ∀ {ℓ ℓJ} →
                           Json.AtomUniverse ℓJ → AtomUniverse ℓ →
                           Type (ℓ-max ℓ ℓJ)
CanonicalAtomValueCodecs J U =
  (a : AtomCode U) → CanonicalFromToJSON' J (Atom U a)

canonicalAtomCodeCodec : ∀ {ℓ ℓJ} {J : Json.AtomUniverse ℓJ}
                         {U : AtomUniverse ℓ} →
                         CanonicalAtomCodeCodec J U → AtomCodeCodec J U
canonicalAtomCodeCodec c = codec c

canonicalAtomValueCodecs : ∀ {ℓ ℓJ} {J : Json.AtomUniverse ℓJ}
                           {U : AtomUniverse ℓ} →
                           CanonicalAtomValueCodecs J U → AtomValueCodecs J U
canonicalAtomValueCodecs codecs a = codec (codecs a)

nothing≡just-elim : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {x : A} →
                    nothing ≡ just x → B
nothing≡just-elim p = Empty.rec (MaybeProperties.¬nothing≡just p)

inspect : ∀ {ℓ} {A : Type ℓ} → (x : A) → Σ[ y ∈ A ] x ≡ y
inspect x = x , refl

natJSONCanonical : ∀ {ℓJ} {J : Json.AtomUniverse ℓJ} →
                   (j : Json.Json J) → (n : ℕ) →
                   fromNatJSON j ≡ just n → toNatJSON n ≡ j
natJSONCanonical (Json.atom c x) n p = nothing≡just-elim p
natJSONCanonical (Json.object xs) n p = nothing≡just-elim p
natJSONCanonical (Json.array []) n p =
  cong toNatJSON (sym (MaybeProperties.just-inj zero n p))
natJSONCanonical (Json.array (j ∷ [])) n p with inspect (fromNatJSON j)
... | nothing , eq =
  nothing≡just-elim (sym (cong (maybeMap suc) eq) ∙ p)
... | just k , eq =
  cong toNatJSON
    (sym (MaybeProperties.just-inj (suc k) n
      (sym (cong (maybeMap suc) eq) ∙ p)))
  ∙ cong (λ x → Json.array (x ∷ [])) (natJSONCanonical j k eq)
natJSONCanonical (Json.array (j ∷ j' ∷ js)) n p = nothing≡just-elim p

fromFin-index : ∀ {n k} {i : Fin n} →
                fromFin n k ≡ just i → FinData.toℕ i ≡ k
fromFin-index {n = zero} p = nothing≡just-elim p
fromFin-index {n = suc n} {k = zero} {i} p =
  cong FinData.toℕ (sym (MaybeProperties.just-inj FinData.zero i p))
fromFin-index {n = suc n} {k = suc k} {i} p with inspect (fromFin n k)
... | nothing , eq =
  nothing≡just-elim (sym (cong (maybeMap FinData.suc) eq) ∙ p)
... | just i' , eq =
  cong FinData.toℕ
    (sym (MaybeProperties.just-inj (FinData.suc i') i
      (sym (cong (maybeMap FinData.suc) eq) ∙ p)))
  ∙ cong suc (fromFin-index {n = n} {k = k} {i = i'} eq)

finJSONCanonical : ∀ {ℓJ n} {J : Json.AtomUniverse ℓJ} →
                   (j : Json.Json J) → (i : Fin n) →
                   fromFinJSON n j ≡ just i → toFinJSON i ≡ j
finJSONCanonical {n = n} j i p with inspect (fromNatJSON j)
... | nothing , natEq =
  nothing≡just-elim
    (sym (cong (λ m → maybeBind m (fromFin n)) natEq) ∙ p)
... | just k , natEq with inspect (fromFin n k)
...   | nothing , finEq =
  nothing≡just-elim
    (sym (cong (λ m → maybeBind m (fromFin n)) natEq ∙ finEq) ∙ p)
...   | just i' , finEq =
  cong toNatJSON
    ( cong FinData.toℕ
        (sym (MaybeProperties.just-inj i' i
          (sym (cong (λ m → maybeBind m (fromFin n)) natEq ∙ finEq) ∙ p)))
    ∙ fromFin-index {n = n} {k = k} {i = i'} finEq )
  ∙ natJSONCanonical j k natEq

fromListIx-index : ∀ {ℓ} {A : Type ℓ} {xs : List A} {k}
                   {i : ListIx xs} →
                   fromListIx xs k ≡ just i → listIxToNat i ≡ k
fromListIx-index {xs = []} p = nothing≡just-elim p
fromListIx-index {xs = x ∷ xs} {k = zero} {i} p =
  cong listIxToNat (sym (MaybeProperties.just-inj here i p))
fromListIx-index {xs = x ∷ xs} {k = suc k} {i} p with
  inspect (fromListIx xs k)
... | nothing , eq =
  nothing≡just-elim (sym (cong (maybeMap there) eq) ∙ p)
... | just i' , eq =
  cong listIxToNat
    (sym (MaybeProperties.just-inj (there i') i
      (sym (cong (maybeMap there) eq) ∙ p)))
  ∙ cong suc (fromListIx-index {xs = xs} {k = k} {i = i'} eq)

listIxJSONCanonical : ∀ {ℓ ℓJ} {A : Type ℓ} {xs : List A}
                      {J : Json.AtomUniverse ℓJ} →
                      (j : Json.Json J) → (i : ListIx xs) →
                      fromListIxJSON xs j ≡ just i →
                      toListIxJSON' i ≡ j
listIxJSONCanonical {xs = xs} j i p with inspect (fromNatJSON j)
... | nothing , natEq =
  nothing≡just-elim
    (sym (cong (λ m → maybeBind m (fromListIx xs)) natEq) ∙ p)
... | just k , natEq with inspect (fromListIx xs k)
...   | nothing , ixEq =
  nothing≡just-elim
    (sym (cong (λ m → maybeBind m (fromListIx xs)) natEq ∙ ixEq) ∙ p)
...   | just i' , ixEq =
  cong toNatJSON
    ( cong listIxToNat
        (sym (MaybeProperties.just-inj i' i
          (sym (cong (λ m → maybeBind m (fromListIx xs)) natEq ∙ ixEq) ∙ p)))
    ∙ fromListIx-index {xs = xs} {k = k} {i = i'} ixEq )
  ∙ natJSONCanonical j k natEq

mutual
  codeJSONCanonical : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ}
                      {J : Json.AtomUniverse ℓJ} →
                      (atomCodecs : CanonicalAtomValueCodecs J U) →
                      (D : Fin n → TyDesc U n) →
                      (d : TyDesc U n) →
                      (j : Json.Json J) →
                      (x : CodeIx U D d) →
                      fromCodeJSON (canonicalAtomValueCodecs atomCodecs) D d j ≡ just x →
                      toCodeJSON (canonicalAtomValueCodecs atomCodecs) D x ≡ j
  codeJSONCanonical atomCodecs D (dataD cs) (Json.atom c a) x p = nothing≡just-elim p
  codeJSONCanonical atomCodecs D (dataD cs) (Json.object fields) x p = nothing≡just-elim p
  codeJSONCanonical atomCodecs D (dataD cs) (Json.array []) x p = nothing≡just-elim p
  codeJSONCanonical atomCodecs D (dataD cs) (Json.array (j ∷ [])) x p = nothing≡just-elim p
  codeJSONCanonical atomCodecs D (dataD cs) (Json.array (jc ∷ ja ∷ [])) x p with
    inspect (fromListIxJSON cs jc)
  ... | nothing , cEq =
    nothing≡just-elim
      (sym (cong
        (λ m → maybeBind m λ c →
          maybeMap (nodeIx c)
            (fromArgsCodeJSON (canonicalAtomValueCodecs atomCodecs) D (lookup c) ja))
        cEq) ∙ p)
  ... | just c , cEq with
    inspect (fromArgsCodeJSON (canonicalAtomValueCodecs atomCodecs) D (lookup c) ja)
  ...   | nothing , argsEq =
    nothing≡just-elim
      (sym
        ( cong
            (λ m → maybeBind m λ c' →
              maybeMap (nodeIx c')
                (fromArgsCodeJSON (canonicalAtomValueCodecs atomCodecs) D (lookup c') ja))
            cEq
        ∙ cong (maybeMap (nodeIx c)) argsEq )
      ∙ p)
  ...   | just args , argsEq =
    cong (toCodeJSON (canonicalAtomValueCodecs atomCodecs) D)
      (sym (MaybeProperties.just-inj (nodeIx c args) x
        ( sym
            ( cong
                (λ m → maybeBind m λ c' →
                  maybeMap (nodeIx c')
                    (fromArgsCodeJSON (canonicalAtomValueCodecs atomCodecs) D (lookup c') ja))
                cEq
            ∙ cong (maybeMap (nodeIx c)) argsEq )
        ∙ p )))
    ∙ (λ i → Json.array
        ( listIxJSONCanonical jc c cEq i
        ∷ argsCodeJSONCanonical atomCodecs D (lookup c) ja args argsEq i
        ∷ [] ))
  codeJSONCanonical atomCodecs D (dataD cs) (Json.array (j ∷ j' ∷ j'' ∷ js)) x p =
    nothing≡just-elim p

  fieldCodeJSONCanonical : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ}
                           {J : Json.AtomUniverse ℓJ} →
                           (atomCodecs : CanonicalAtomValueCodecs J U) →
                           (D : Fin n → TyDesc U n) →
                           (f : FieldDesc U n) →
                           (j : Json.Json J) →
                           (x : FieldCodeIx U D f) →
                           fromFieldCodeJSON (canonicalAtomValueCodecs atomCodecs) D f j ≡ just x →
                           toFieldCodeJSON (canonicalAtomValueCodecs atomCodecs) D x ≡ j
  fieldCodeJSONCanonical atomCodecs D (fieldRec i) j x p with
    inspect (fromCodeJSON (canonicalAtomValueCodecs atomCodecs) D (D i) j)
  ... | nothing , eq =
    nothing≡just-elim (sym (cong (maybeMap recIx) eq) ∙ p)
  ... | just y , eq =
    cong (toFieldCodeJSON (canonicalAtomValueCodecs atomCodecs) D)
      (sym (MaybeProperties.just-inj (recIx y) x
        (sym (cong (maybeMap recIx) eq) ∙ p)))
    ∙ codeJSONCanonical atomCodecs D (D i) j y eq
  fieldCodeJSONCanonical atomCodecs D (fieldAtom a) j x p with
    inspect (fromJSONWith (codec (atomCodecs a)) j)
  ... | nothing , eq =
    nothing≡just-elim (sym (cong (maybeMap atomIx) eq) ∙ p)
  ... | just y , eq =
    cong (toFieldCodeJSON (canonicalAtomValueCodecs atomCodecs) D)
      (sym (MaybeProperties.just-inj (atomIx y) x
        (sym (cong (maybeMap atomIx) eq) ∙ p)))
    ∙ canonical (atomCodecs a) j y eq

  argsCodeListJSONCanonical : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ}
                              {J : Json.AtomUniverse ℓJ} →
                              (atomCodecs : CanonicalAtomValueCodecs J U) →
                              (D : Fin n → TyDesc U n) →
                              (c : ConDesc U n) →
                              (js : List (Json.Json J)) →
                              (xs : ArgsCodeIx U D c) →
                              fromArgsCodeJSON (canonicalAtomValueCodecs atomCodecs) D c (Json.array js)
                                ≡ just xs →
                              toArgsCodeListJSON (canonicalAtomValueCodecs atomCodecs) D xs ≡ js
  argsCodeListJSONCanonical atomCodecs D (con []) [] xs p =
    cong (toArgsCodeListJSON (canonicalAtomValueCodecs atomCodecs) D)
      (sym (MaybeProperties.just-inj []ⁱ xs p))
  argsCodeListJSONCanonical atomCodecs D (con []) (j ∷ js) xs p =
    nothing≡just-elim p
  argsCodeListJSONCanonical atomCodecs D (con (f ∷ fs)) [] xs p =
    nothing≡just-elim p
  argsCodeListJSONCanonical atomCodecs D (con (f ∷ fs)) (j ∷ js) xs p with
    inspect (fromFieldCodeJSON (canonicalAtomValueCodecs atomCodecs) D f j)
  ... | nothing , xEq =
    nothing≡just-elim
      (sym
        (cong
          (λ m → maybeBind m λ x →
            maybeMap (x ∷ⁱ_)
              (fromArgsCodeJSON (canonicalAtomValueCodecs atomCodecs) D (con fs) (Json.array js)))
          xEq)
      ∙ p)
  ... | just x , xEq with
    inspect (fromArgsCodeJSON (canonicalAtomValueCodecs atomCodecs) D (con fs) (Json.array js))
  ...   | nothing , xsEq =
    nothing≡just-elim
      (sym
        ( cong
            (λ m → maybeBind m λ x' →
              maybeMap (x' ∷ⁱ_)
                (fromArgsCodeJSON (canonicalAtomValueCodecs atomCodecs) D (con fs) (Json.array js)))
            xEq
        ∙ cong (maybeMap (x ∷ⁱ_)) xsEq )
      ∙ p)
  ...   | just xs' , xsEq =
    cong (toArgsCodeListJSON (canonicalAtomValueCodecs atomCodecs) D)
      (sym (MaybeProperties.just-inj (x ∷ⁱ xs') xs
        ( sym
            ( cong
                (λ m → maybeBind m λ x' →
                  maybeMap (x' ∷ⁱ_)
                    (fromArgsCodeJSON (canonicalAtomValueCodecs atomCodecs) D (con fs) (Json.array js)))
                xEq
            ∙ cong (maybeMap (x ∷ⁱ_)) xsEq )
        ∙ p )))
    ∙ (λ i →
        fieldCodeJSONCanonical atomCodecs D f j x xEq i
        ∷ argsCodeListJSONCanonical atomCodecs D (con fs) js xs' xsEq i)

  argsCodeJSONCanonical : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ}
                          {J : Json.AtomUniverse ℓJ} →
                          (atomCodecs : CanonicalAtomValueCodecs J U) →
                          (D : Fin n → TyDesc U n) →
                          (c : ConDesc U n) →
                          (j : Json.Json J) →
                          (xs : ArgsCodeIx U D c) →
                          fromArgsCodeJSON (canonicalAtomValueCodecs atomCodecs) D c j ≡ just xs →
                          toArgsCodeJSON (canonicalAtomValueCodecs atomCodecs) D xs ≡ j
  argsCodeJSONCanonical atomCodecs D (con []) (Json.atom a x) xs p = nothing≡just-elim p
  argsCodeJSONCanonical atomCodecs D (con (f ∷ fs)) (Json.atom a x) xs p = nothing≡just-elim p
  argsCodeJSONCanonical atomCodecs D (con []) (Json.object fields) xs p = nothing≡just-elim p
  argsCodeJSONCanonical atomCodecs D (con (f ∷ fs)) (Json.object fields) xs p = nothing≡just-elim p
  argsCodeJSONCanonical atomCodecs D c (Json.array js) xs p =
    cong Json.array (argsCodeListJSONCanonical atomCodecs D c js xs p)

rootCodeJSONCanonical : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ}
                        {J : Json.AtomUniverse ℓJ} →
                        (atomCodecs : CanonicalAtomValueCodecs J U) →
                        (D : Fin n → TyDesc U n) →
                        (r : RootDesc U n) →
                        (j : Json.Json J) →
                        (x : RootCodeIx U D r) →
                        fromRootCodeJSON (canonicalAtomValueCodecs atomCodecs) D r j ≡ just x →
                        toRootCodeJSON (canonicalAtomValueCodecs atomCodecs) D r x ≡ j
rootCodeJSONCanonical atomCodecs D (rootData i) j x p with
  inspect (fromCodeJSON (canonicalAtomValueCodecs atomCodecs) D (D i) j)
... | nothing , eq =
  nothing≡just-elim (sym (cong (maybeMap rootDataIx) eq) ∙ p)
... | just y , eq =
  cong (toRootCodeJSON (canonicalAtomValueCodecs atomCodecs) D (rootData i))
    (sym (MaybeProperties.just-inj (rootDataIx y) x
      (sym (cong (maybeMap rootDataIx) eq) ∙ p)))
  ∙ codeJSONCanonical atomCodecs D (D i) j y eq
rootCodeJSONCanonical atomCodecs D (rootAtom a) j x p with
  inspect (fromJSONWith (codec (atomCodecs a)) j)
... | nothing , eq =
  nothing≡just-elim (sym (cong (maybeMap rootAtomIx) eq) ∙ p)
... | just y , eq =
  cong (toRootCodeJSON (canonicalAtomValueCodecs atomCodecs) D (rootAtom a))
    (sym (MaybeProperties.just-inj (rootAtomIx y) x
      (sym (cong (maybeMap rootAtomIx) eq) ∙ p)))
  ∙ canonical (atomCodecs a) j y eq

genericCanonicalFromToJSON : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ}
                             {A : Type ℓ} →
                             (J : Json.AtomUniverse ℓJ) →
                             CanonicalAtomValueCodecs J U →
                             (g : Generic U A) →
                             CanonicalFromToJSON' J A
genericCanonicalFromToJSON J atomCodecs g =
  canonicalFromToJSON' baseCodec canonicalGeneric
  where
  baseCodec = genericFromToJSON J (canonicalAtomValueCodecs atomCodecs) g

  canonicalGeneric : (j : Json.Json J) → (x : _) →
                     fromJSONWith baseCodec j ≡ just x →
                     toJSONWith baseCodec x ≡ j
  canonicalGeneric j x p with
    inspect
      (fromRootCodeJSON
        (canonicalAtomValueCodecs atomCodecs)
        (Generic.desc g) (Generic.root g) j)
  ... | nothing , eq =
    nothing≡just-elim
      (sym (cong (maybeMap (Generic.decode g)) eq) ∙ p)
  ... | just code , eq =
    cong
      (λ y →
        toRootCodeJSON
          (canonicalAtomValueCodecs atomCodecs)
          (Generic.desc g) (Generic.root g)
          (Generic.encode g y))
      (sym (MaybeProperties.just-inj (Generic.decode g code) x
        (sym (cong (maybeMap (Generic.decode g)) eq) ∙ p)))
    ∙ cong
        (toRootCodeJSON
          (canonicalAtomValueCodecs atomCodecs)
          (Generic.desc g) (Generic.root g))
        (Generic.encode-decode g code)
    ∙ rootCodeJSONCanonical atomCodecs
        (Generic.desc g) (Generic.root g) j code eq

listJSONCanonical : ∀ {ℓJ} {A : Type₀} {J : Json.AtomUniverse ℓJ} →
                    (to : A → Json.Json J) →
                    (from : Json.Json J → Maybe A) →
                    ((j : Json.Json J) → (x : A) → from j ≡ just x → to x ≡ j) →
                    (js : List (Json.Json J)) → (xs : List A) →
                    fromListJSON from js ≡ just xs →
                    toListJSON to xs ≡ js
listJSONCanonical to from elementCanonical [] xs p =
  cong (toListJSON to) (sym (MaybeProperties.just-inj [] xs p))
listJSONCanonical to from elementCanonical (j ∷ js) xs p with inspect (from j)
... | nothing , xEq =
  nothing≡just-elim
    (sym
      (cong
        (λ m → maybeBind m λ x → maybeMap (x ∷_) (fromListJSON from js))
        xEq)
    ∙ p)
... | just x , xEq with inspect (fromListJSON from js)
...   | nothing , xsEq =
  nothing≡just-elim
    (sym
      ( cong
          (λ m → maybeBind m λ x' → maybeMap (x' ∷_) (fromListJSON from js))
          xEq
      ∙ cong (maybeMap (x ∷_)) xsEq )
    ∙ p)
...   | just xs' , xsEq =
  cong (toListJSON to)
    (sym (MaybeProperties.just-inj (x ∷ xs') xs
      ( sym
          ( cong
              (λ m → maybeBind m λ x' → maybeMap (x' ∷_) (fromListJSON from js))
              xEq
          ∙ cong (maybeMap (x ∷_)) xsEq )
      ∙ p )))
  ∙ (λ i →
      elementCanonical j x xEq i
      ∷ listJSONCanonical to from elementCanonical js xs' xsEq i)

vecJSONCanonical : ∀ {ℓJ len} {A : Type₀} {J : Json.AtomUniverse ℓJ} →
                   (to : A → Json.Json J) →
                   (from : Json.Json J → Maybe A) →
                   ((j : Json.Json J) → (x : A) → from j ≡ just x → to x ≡ j) →
                   (js : List (Json.Json J)) → (xs : Vec₀ A len) →
                   fromVecJSON from len (Json.array js) ≡ just xs →
                   toVecListJSON to xs ≡ js
vecJSONCanonical to from elementCanonical [] []ᵛ p = refl
vecJSONCanonical to from elementCanonical (j ∷ js) []ᵛ p = nothing≡just-elim p
vecJSONCanonical to from elementCanonical [] (x ∷ᵛ xs) p = nothing≡just-elim p
vecJSONCanonical to from elementCanonical (j ∷ js) (x ∷ᵛ xs) p with inspect (from j)
... | nothing , xEq =
  nothing≡just-elim
    (sym
      (cong
        (λ m → maybeBind m λ x → maybeMap (x ∷ᵛ_) (fromVecJSON from _ (Json.array js)))
        xEq)
    ∙ p)
... | just x' , xEq with inspect (fromVecJSON from _ (Json.array js))
...   | nothing , xsEq =
  nothing≡just-elim
    (sym
      ( cong
          (λ m → maybeBind m λ y → maybeMap (y ∷ᵛ_) (fromVecJSON from _ (Json.array js)))
          xEq
      ∙ cong (maybeMap (x' ∷ᵛ_)) xsEq )
    ∙ p)
...   | just xs' , xsEq =
  let pairEq = MaybeProperties.just-inj (x' ∷ᵛ xs') (x ∷ᵛ xs)
        ( sym
            ( cong
                (λ m → maybeBind m λ y → maybeMap (y ∷ᵛ_) (fromVecJSON from _ (Json.array js)))
                xEq
            ∙ cong (maybeMap (x' ∷ᵛ_)) xsEq )
        ∙ p )
  in
  cong (toVecListJSON to) (sym pairEq)
  ∙ (λ i →
      elementCanonical j x' xEq i
      ∷ vecJSONCanonical to from elementCanonical js xs' xsEq i)

vecJSONValueCanonical : ∀ {ℓJ len} {A : Type₀} {J : Json.AtomUniverse ℓJ} →
                        (to : A → Json.Json J) →
                        (from : Json.Json J → Maybe A) →
                        ((j : Json.Json J) → (x : A) → from j ≡ just x → to x ≡ j) →
                        (j : Json.Json J) → (xs : Vec₀ A len) →
                        fromVecJSON from len j ≡ just xs →
                        toVecJSON to xs ≡ j
vecJSONValueCanonical to from elementCanonical (Json.atom a x) []ᵛ p =
  nothing≡just-elim p
vecJSONValueCanonical to from elementCanonical (Json.object fields) []ᵛ p =
  nothing≡just-elim p
vecJSONValueCanonical to from elementCanonical (Json.array js) []ᵛ p =
  cong Json.array (vecJSONCanonical to from elementCanonical js []ᵛ p)
vecJSONValueCanonical to from elementCanonical (Json.atom a x) (y ∷ᵛ ys) p =
  nothing≡just-elim p
vecJSONValueCanonical to from elementCanonical (Json.object fields) (y ∷ᵛ ys) p =
  nothing≡just-elim p
vecJSONValueCanonical to from elementCanonical (Json.array js) (y ∷ᵛ ys) p =
  cong Json.array (vecJSONCanonical to from elementCanonical js (y ∷ᵛ ys) p)

fieldDescTagJSONCanonical : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ}
                            {J : Json.AtomUniverse ℓJ} →
                            (atomCodeCodec : CanonicalAtomCodeCodec J U) →
                            (tag j : Json.Json J) → (k : ℕ) →
                            fromNatJSON tag ≡ just k →
                            (f : FieldDesc U n) →
                            fromFieldDescTag (codec atomCodeCodec) n j k ≡ just f →
                            toFieldDescJSON (codec atomCodeCodec) f
                              ≡ Json.array (tag ∷ j ∷ [])
fieldDescTagJSONCanonical {n = n} atomCodeCodec tag j zero tagEq f p with
  inspect (fromFinJSON n j)
... | nothing , valueEq =
  nothing≡just-elim (sym (cong (maybeMap fieldRec) valueEq) ∙ p)
... | just i , valueEq =
  cong (toFieldDescJSON (codec atomCodeCodec))
    (sym (MaybeProperties.just-inj (fieldRec i) f
      (sym (cong (maybeMap fieldRec) valueEq) ∙ p)))
  ∙ (λ q → Json.array
      (natJSONCanonical tag zero tagEq q ∷ finJSONCanonical j i valueEq q ∷ []))
fieldDescTagJSONCanonical atomCodeCodec tag j (suc zero) tagEq f p with
  inspect (fromJSONWith (codec atomCodeCodec) j)
... | nothing , valueEq =
  nothing≡just-elim (sym (cong (maybeMap fieldAtom) valueEq) ∙ p)
... | just a , valueEq =
  cong (toFieldDescJSON (codec atomCodeCodec))
    (sym (MaybeProperties.just-inj (fieldAtom a) f
      (sym (cong (maybeMap fieldAtom) valueEq) ∙ p)))
  ∙ (λ q → Json.array
      ( natJSONCanonical tag (suc zero) tagEq q
      ∷ canonical atomCodeCodec j a valueEq q
      ∷ [] ))
fieldDescTagJSONCanonical atomCodeCodec tag j (suc (suc k)) tagEq f p =
  nothing≡just-elim p

fieldDescJSONCanonical : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ}
                         {J : Json.AtomUniverse ℓJ} →
                         (atomCodeCodec : CanonicalAtomCodeCodec J U) →
                         (j : Json.Json J) → (f : FieldDesc U n) →
                         fromFieldDescJSON (codec atomCodeCodec) n j ≡ just f →
                         toFieldDescJSON (codec atomCodeCodec) f ≡ j
fieldDescJSONCanonical atomCodeCodec (Json.atom c x) f p = nothing≡just-elim p
fieldDescJSONCanonical atomCodeCodec (Json.object xs) f p = nothing≡just-elim p
fieldDescJSONCanonical atomCodeCodec (Json.array []) f p = nothing≡just-elim p
fieldDescJSONCanonical atomCodeCodec (Json.array (tag ∷ [])) f p = nothing≡just-elim p
fieldDescJSONCanonical {n = n} atomCodeCodec (Json.array (tag ∷ j ∷ [])) f p with
  inspect (fromNatJSON tag)
... | nothing , tagEq =
  nothing≡just-elim
    (sym
      (cong
        (λ m → maybeBind m (fromFieldDescTag (codec atomCodeCodec) n j))
        tagEq)
    ∙ p)
... | just k , tagEq =
  fieldDescTagJSONCanonical atomCodeCodec tag j k tagEq f
    (sym
      (cong
        (λ m → maybeBind m (fromFieldDescTag (codec atomCodeCodec) n j))
        tagEq)
    ∙ p)
fieldDescJSONCanonical atomCodeCodec (Json.array (j ∷ j' ∷ j'' ∷ js)) f p =
  nothing≡just-elim p

fieldDescListJSONCanonical : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ}
                             {J : Json.AtomUniverse ℓJ} →
                             (atomCodeCodec : CanonicalAtomCodeCodec J U) →
                             (js : List (Json.Json J)) →
                             (fs : List (FieldDesc U n)) →
                             fromFieldDescListJSON (codec atomCodeCodec) n js ≡ just fs →
                             toFieldDescListJSON (codec atomCodeCodec) fs ≡ js
fieldDescListJSONCanonical {n = n} {U = U} {J = J} atomCodeCodec js fs p =
  toFieldDescList-agrees atomCodeCodec fs
  ∙ listJSONCanonical
      (toFieldDescJSON (codec atomCodeCodec))
      (fromFieldDescJSON (codec atomCodeCodec) n)
      (fieldDescJSONCanonical atomCodeCodec)
      js fs
      (sym (fromFieldDescList-agrees atomCodeCodec js) ∙ p)
  where
  toFieldDescList-agrees :
    (atomCodeCodec : CanonicalAtomCodeCodec J U) →
    (fs : List (FieldDesc U n)) →
    toFieldDescListJSON (codec atomCodeCodec) fs
      ≡ toListJSON (toFieldDescJSON (codec atomCodeCodec)) fs
  toFieldDescList-agrees atomCodeCodec [] = refl
  toFieldDescList-agrees atomCodeCodec (f ∷ fs) =
    cong (toFieldDescJSON (codec atomCodeCodec) f ∷_)
      (toFieldDescList-agrees atomCodeCodec fs)

  fromFieldDescList-agrees :
    (atomCodeCodec : CanonicalAtomCodeCodec J U) →
    (js : List (Json.Json J)) →
    fromFieldDescListJSON (codec atomCodeCodec) n js
      ≡ fromListJSON (fromFieldDescJSON (codec atomCodeCodec) n) js
  fromFieldDescList-agrees atomCodeCodec [] = refl
  fromFieldDescList-agrees atomCodeCodec (j ∷ js) =
    cong
      (λ tail →
        maybeBind (fromFieldDescJSON (codec atomCodeCodec) n j) λ f →
        maybeMap (f ∷_) tail)
      (fromFieldDescList-agrees atomCodeCodec js)

conDescJSONCanonical : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ}
                       {J : Json.AtomUniverse ℓJ} →
                       (atomCodeCodec : CanonicalAtomCodeCodec J U) →
                       (j : Json.Json J) → (c : ConDesc U n) →
                       fromConDescJSON (codec atomCodeCodec) n j ≡ just c →
                       toConDescJSON (codec atomCodeCodec) c ≡ j
conDescJSONCanonical atomCodeCodec (Json.atom a x) c p = nothing≡just-elim p
conDescJSONCanonical atomCodeCodec (Json.object fields) c p = nothing≡just-elim p
conDescJSONCanonical {n = n} atomCodeCodec (Json.array js) c p with
  inspect (fromFieldDescListJSON (codec atomCodeCodec) n js)
... | nothing , eq =
  nothing≡just-elim (sym (cong (maybeMap con) eq) ∙ p)
... | just fs , eq =
  cong (toConDescJSON (codec atomCodeCodec))
    (sym (MaybeProperties.just-inj (con fs) c
      (sym (cong (maybeMap con) eq) ∙ p)))
  ∙ cong Json.array (fieldDescListJSONCanonical atomCodeCodec js fs eq)

conDescListJSONCanonical : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ}
                           {J : Json.AtomUniverse ℓJ} →
                           (atomCodeCodec : CanonicalAtomCodeCodec J U) →
                           (js : List (Json.Json J)) →
                           (cs : List (ConDesc U n)) →
                           fromConDescListJSON (codec atomCodeCodec) n js ≡ just cs →
                           toConDescListJSON (codec atomCodeCodec) cs ≡ js
conDescListJSONCanonical {n = n} {U = U} {J = J} atomCodeCodec js cs p =
  toConDescList-agrees atomCodeCodec cs
  ∙ listJSONCanonical
      (toConDescJSON (codec atomCodeCodec))
      (fromConDescJSON (codec atomCodeCodec) n)
      (conDescJSONCanonical atomCodeCodec)
      js cs
      (sym (fromConDescList-agrees atomCodeCodec js) ∙ p)
  where
  toConDescList-agrees :
    (atomCodeCodec : CanonicalAtomCodeCodec J U) →
    (cs : List (ConDesc U n)) →
    toConDescListJSON (codec atomCodeCodec) cs
      ≡ toListJSON (toConDescJSON (codec atomCodeCodec)) cs
  toConDescList-agrees atomCodeCodec [] = refl
  toConDescList-agrees atomCodeCodec (c ∷ cs) =
    cong (toConDescJSON (codec atomCodeCodec) c ∷_)
      (toConDescList-agrees atomCodeCodec cs)

  fromConDescList-agrees :
    (atomCodeCodec : CanonicalAtomCodeCodec J U) →
    (js : List (Json.Json J)) →
    fromConDescListJSON (codec atomCodeCodec) n js
      ≡ fromListJSON (fromConDescJSON (codec atomCodeCodec) n) js
  fromConDescList-agrees atomCodeCodec [] = refl
  fromConDescList-agrees atomCodeCodec (j ∷ js) =
    cong
      (λ tail →
        maybeBind (fromConDescJSON (codec atomCodeCodec) n j) λ c →
        maybeMap (c ∷_) tail)
      (fromConDescList-agrees atomCodeCodec js)

tyDescJSONCanonical : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ}
                      {J : Json.AtomUniverse ℓJ} →
                      (atomCodeCodec : CanonicalAtomCodeCodec J U) →
                      (j : Json.Json J) → (d : TyDesc U n) →
                      fromTyDescJSON (codec atomCodeCodec) n j ≡ just d →
                      toTyDescJSON (codec atomCodeCodec) d ≡ j
tyDescJSONCanonical atomCodeCodec (Json.atom a x) d p = nothing≡just-elim p
tyDescJSONCanonical atomCodeCodec (Json.object fields) d p = nothing≡just-elim p
tyDescJSONCanonical {n = n} atomCodeCodec (Json.array js) d p with
  inspect (fromConDescListJSON (codec atomCodeCodec) n js)
... | nothing , eq =
  nothing≡just-elim (sym (cong (maybeMap dataD) eq) ∙ p)
... | just cs , eq =
  cong (toTyDescJSON (codec atomCodeCodec))
    (sym (MaybeProperties.just-inj (dataD cs) d
      (sym (cong (maybeMap dataD) eq) ∙ p)))
  ∙ cong Json.array (conDescListJSONCanonical atomCodeCodec js cs eq)

descVecListJSONCanonical : ∀ {ℓ ℓJ count len} {U : AtomUniverse ℓ}
                           {J : Json.AtomUniverse ℓJ} →
                           (atomCodeCodec : CanonicalAtomCodeCodec J U) →
                           (js : List (Json.Json J)) →
                           (ds : DescVec U count len) →
                           fromDescVecJSON (codec atomCodeCodec) count len (Json.array js)
                             ≡ just ds →
                           toDescVecListJSON (codec atomCodeCodec) ds ≡ js
descVecListJSONCanonical atomCodeCodec [] []ᵈ p = refl
descVecListJSONCanonical atomCodeCodec (j ∷ js) []ᵈ p = nothing≡just-elim p
descVecListJSONCanonical atomCodeCodec [] (d ∷ᵈ ds) p = nothing≡just-elim p
descVecListJSONCanonical {count = count} atomCodeCodec (j ∷ js) (d ∷ᵈ ds) p with
  inspect (fromTyDescJSON (codec atomCodeCodec) count j)
... | nothing , dEq =
  nothing≡just-elim
    (sym
      (cong
        (λ m → maybeBind m λ d →
          maybeMap (d ∷ᵈ_)
            (fromDescVecJSON (codec atomCodeCodec) count _ (Json.array js)))
        dEq)
    ∙ p)
... | just d' , dEq with
  inspect (fromDescVecJSON (codec atomCodeCodec) count _ (Json.array js))
...   | nothing , dsEq =
  nothing≡just-elim
    (sym
      ( cong
          (λ m → maybeBind m λ d'' →
            maybeMap (d'' ∷ᵈ_)
              (fromDescVecJSON (codec atomCodeCodec) count _ (Json.array js)))
          dEq
      ∙ cong (maybeMap (d' ∷ᵈ_)) dsEq )
    ∙ p)
...   | just ds' , dsEq =
  let parsedEq = MaybeProperties.just-inj (d' ∷ᵈ ds') (d ∷ᵈ ds)
        ( sym
            ( cong
                (λ m → maybeBind m λ d'' →
                  maybeMap (d'' ∷ᵈ_)
                    (fromDescVecJSON (codec atomCodeCodec) count _ (Json.array js)))
                dEq
            ∙ cong (maybeMap (d' ∷ᵈ_)) dsEq )
        ∙ p )
  in
  cong (toDescVecListJSON (codec atomCodeCodec)) (sym parsedEq)
  ∙ (λ i →
      tyDescJSONCanonical atomCodeCodec j d' dEq i
      ∷ descVecListJSONCanonical atomCodeCodec js ds' dsEq i)

descVecJSONCanonical : ∀ {ℓ ℓJ count len} {U : AtomUniverse ℓ}
                       {J : Json.AtomUniverse ℓJ} →
                       (atomCodeCodec : CanonicalAtomCodeCodec J U) →
                       (j : Json.Json J) → (ds : DescVec U count len) →
                       fromDescVecJSON (codec atomCodeCodec) count len j ≡ just ds →
                       toDescVecJSON (codec atomCodeCodec) ds ≡ j
descVecJSONCanonical atomCodeCodec (Json.atom a x) []ᵈ p = nothing≡just-elim p
descVecJSONCanonical atomCodeCodec (Json.object fields) []ᵈ p = nothing≡just-elim p
descVecJSONCanonical atomCodeCodec (Json.array js) []ᵈ p =
  cong Json.array (descVecListJSONCanonical atomCodeCodec js []ᵈ p)
descVecJSONCanonical atomCodeCodec (Json.atom a x) (d ∷ᵈ ds) p = nothing≡just-elim p
descVecJSONCanonical atomCodeCodec (Json.object fields) (d ∷ᵈ ds) p = nothing≡just-elim p
descVecJSONCanonical atomCodeCodec (Json.array js) (d ∷ᵈ ds) p =
  cong Json.array (descVecListJSONCanonical atomCodeCodec js (d ∷ᵈ ds) p)

stringListJSONCanonical : ∀ {ℓJ} {J : Json.AtomUniverse ℓJ} →
                          (stringCodec : CanonicalFromToJSON' J String) →
                          (j : Json.Json J) → (xs : List String) →
                          fromStringListJSON (codec stringCodec) j ≡ just xs →
                          toStringListJSON (codec stringCodec) xs ≡ j
stringListJSONCanonical stringCodec (Json.atom a x) xs p = nothing≡just-elim p
stringListJSONCanonical stringCodec (Json.object fields) xs p = nothing≡just-elim p
stringListJSONCanonical stringCodec (Json.array js) xs p =
  cong Json.array
    (listJSONCanonical
      (toJSONWith (codec stringCodec))
      (fromJSONWith (codec stringCodec))
      (canonical stringCodec)
      js xs p)

rootDescTagJSONCanonical : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ}
                           {J : Json.AtomUniverse ℓJ} →
                           (atomCodeCodec : CanonicalAtomCodeCodec J U) →
                           (tag j : Json.Json J) → (k : ℕ) →
                           fromNatJSON tag ≡ just k →
                           (r : RootDesc U n) →
                           fromRootDescTag (codec atomCodeCodec) n j k ≡ just r →
                           toRootDescJSON (codec atomCodeCodec) r
                             ≡ Json.array (tag ∷ j ∷ [])
rootDescTagJSONCanonical {n = n} atomCodeCodec tag j zero tagEq r p with
  inspect (fromFinJSON n j)
... | nothing , valueEq =
  nothing≡just-elim (sym (cong (maybeMap rootData) valueEq) ∙ p)
... | just i , valueEq =
  cong (toRootDescJSON (codec atomCodeCodec))
    (sym (MaybeProperties.just-inj (rootData i) r
      (sym (cong (maybeMap rootData) valueEq) ∙ p)))
  ∙ (λ q → Json.array
      (natJSONCanonical tag zero tagEq q ∷ finJSONCanonical j i valueEq q ∷ []))
rootDescTagJSONCanonical atomCodeCodec tag j (suc zero) tagEq r p with
  inspect (fromJSONWith (codec atomCodeCodec) j)
... | nothing , valueEq =
  nothing≡just-elim (sym (cong (maybeMap rootAtom) valueEq) ∙ p)
... | just a , valueEq =
  cong (toRootDescJSON (codec atomCodeCodec))
    (sym (MaybeProperties.just-inj (rootAtom a) r
      (sym (cong (maybeMap rootAtom) valueEq) ∙ p)))
  ∙ (λ q → Json.array
      ( natJSONCanonical tag (suc zero) tagEq q
      ∷ canonical atomCodeCodec j a valueEq q
      ∷ [] ))
rootDescTagJSONCanonical atomCodeCodec tag j (suc (suc k)) tagEq r p =
  nothing≡just-elim p

rootDescJSONCanonical : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ}
                        {J : Json.AtomUniverse ℓJ} →
                        (atomCodeCodec : CanonicalAtomCodeCodec J U) →
                        (j : Json.Json J) → (r : RootDesc U n) →
                        fromRootDescJSON (codec atomCodeCodec) n j ≡ just r →
                        toRootDescJSON (codec atomCodeCodec) r ≡ j
rootDescJSONCanonical atomCodeCodec (Json.atom c x) r p = nothing≡just-elim p
rootDescJSONCanonical atomCodeCodec (Json.object xs) r p = nothing≡just-elim p
rootDescJSONCanonical atomCodeCodec (Json.array []) r p = nothing≡just-elim p
rootDescJSONCanonical atomCodeCodec (Json.array (tag ∷ [])) r p = nothing≡just-elim p
rootDescJSONCanonical {n = n} atomCodeCodec (Json.array (tag ∷ j ∷ [])) r p with
  inspect (fromNatJSON tag)
... | nothing , tagEq =
  nothing≡just-elim
    (sym
      (cong
        (λ m → maybeBind m (fromRootDescTag (codec atomCodeCodec) n j))
        tagEq)
    ∙ p)
... | just k , tagEq =
  rootDescTagJSONCanonical atomCodeCodec tag j k tagEq r
    (sym
      (cong
        (λ m → maybeBind m (fromRootDescTag (codec atomCodeCodec) n j))
        tagEq)
    ∙ p)
rootDescJSONCanonical atomCodeCodec (Json.array (j ∷ j' ∷ j'' ∷ js)) r p =
  nothing≡just-elim p

module SpecificationCanonicalProof
  {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
  (stringCodec : CanonicalFromToJSON' J String)
  (atomCodeCodec : CanonicalAtomCodeCodec J U)
  (jn jtn jcn jd jr : Json.Json J)
  (target : GenericSpecification U)
  where

  stringBase = codec stringCodec
  atomBase = codec atomCodeCodec

  Result : Type ℓJ
  Result =
    toSpecificationJSON stringBase atomBase target
      ≡ Json.array (jn ∷ jtn ∷ jcn ∷ jd ∷ jr ∷ [])

  rootStage :
    (count : ℕ) → fromNatJSON jn ≡ just count →
    (typeNames : Vec₀ String count) →
    fromVecJSON (fromJSONWith stringBase) count jtn ≡ just typeNames →
    (constructorNames : Vec₀ (List String) count) →
    fromVecJSON (fromStringListJSON stringBase) count jcn ≡ just constructorNames →
    (descs : DescVec U count count) →
    fromDescVecJSON atomBase count count jd ≡ just descs →
    fromSpecificationRoot count typeNames constructorNames atomBase jr descs
      ≡ just target →
    Result
  rootStage count countEq typeNames typeNamesEq constructorNames constructorNamesEq
    descs descsEq p with inspect (fromRootDescJSON atomBase count jr)
  ... | nothing , rootEq =
    nothing≡just-elim
      (sym
        (cong
          (maybeMap (genericSpecification count typeNames constructorNames descs))
          rootEq)
      ∙ p)
  ... | just root , rootEq =
    cong (toSpecificationJSON stringBase atomBase)
      (sym (MaybeProperties.just-inj
        (genericSpecification count typeNames constructorNames descs root)
        target
        ( sym
            (cong
              (maybeMap (genericSpecification count typeNames constructorNames descs))
              rootEq)
        ∙ p )))
    ∙ (λ i → Json.array
        ( natJSONCanonical jn count countEq i
        ∷ vecJSONValueCanonical
            (toJSONWith stringBase)
            (fromJSONWith stringBase)
            (canonical stringCodec)
            jtn typeNames typeNamesEq i
        ∷ vecJSONValueCanonical
            (toStringListJSON stringBase)
            (fromStringListJSON stringBase)
            (stringListJSONCanonical stringCodec)
            jcn constructorNames constructorNamesEq i
        ∷ descVecJSONCanonical atomCodeCodec jd descs descsEq i
        ∷ rootDescJSONCanonical atomCodeCodec jr root rootEq i
        ∷ [] ))

  descsStage :
    (count : ℕ) → fromNatJSON jn ≡ just count →
    (typeNames : Vec₀ String count) →
    fromVecJSON (fromJSONWith stringBase) count jtn ≡ just typeNames →
    (constructorNames : Vec₀ (List String) count) →
    fromVecJSON (fromStringListJSON stringBase) count jcn ≡ just constructorNames →
    fromSpecificationDescs count typeNames atomBase jd jr constructorNames
      ≡ just target →
    Result
  descsStage count countEq typeNames typeNamesEq constructorNames constructorNamesEq p with
    inspect (fromDescVecJSON atomBase count count jd)
  ... | nothing , descsEq =
    nothing≡just-elim
      (sym
        (cong
          (λ m → maybeBind m
            (fromSpecificationRoot count typeNames constructorNames atomBase jr))
          descsEq)
      ∙ p)
  ... | just descs , descsEq =
    rootStage count countEq typeNames typeNamesEq constructorNames constructorNamesEq
      descs descsEq
      (sym
        (cong
          (λ m → maybeBind m
            (fromSpecificationRoot count typeNames constructorNames atomBase jr))
          descsEq)
      ∙ p)

  constructorNamesStage :
    (count : ℕ) → fromNatJSON jn ≡ just count →
    (typeNames : Vec₀ String count) →
    fromVecJSON (fromJSONWith stringBase) count jtn ≡ just typeNames →
    fromSpecificationConstructorNames
      count stringBase atomBase jcn jd jr typeNames ≡ just target →
    Result
  constructorNamesStage count countEq typeNames typeNamesEq p with
    inspect (fromVecJSON (fromStringListJSON stringBase) count jcn)
  ... | nothing , constructorNamesEq =
    nothing≡just-elim
      (sym
        (cong
          (λ m → maybeBind m
            (fromSpecificationDescs count typeNames atomBase jd jr))
          constructorNamesEq)
      ∙ p)
  ... | just constructorNames , constructorNamesEq =
    descsStage count countEq typeNames typeNamesEq constructorNames constructorNamesEq
      (sym
        (cong
          (λ m → maybeBind m
            (fromSpecificationDescs count typeNames atomBase jd jr))
          constructorNamesEq)
      ∙ p)

  typeNamesStage :
    (count : ℕ) → fromNatJSON jn ≡ just count →
    fromSpecificationTypeNames stringBase atomBase jtn jcn jd jr count
      ≡ just target →
    Result
  typeNamesStage count countEq p with
    inspect (fromVecJSON (fromJSONWith stringBase) count jtn)
  ... | nothing , typeNamesEq =
    nothing≡just-elim
      (sym
        (cong
          (λ m → maybeBind m
            (fromSpecificationConstructorNames
              count stringBase atomBase jcn jd jr))
          typeNamesEq)
      ∙ p)
  ... | just typeNames , typeNamesEq =
    constructorNamesStage count countEq typeNames typeNamesEq
      (sym
        (cong
          (λ m → maybeBind m
            (fromSpecificationConstructorNames
              count stringBase atomBase jcn jd jr))
          typeNamesEq)
      ∙ p)

  countStage :
    fromSpecificationJSON stringBase atomBase
      (Json.array (jn ∷ jtn ∷ jcn ∷ jd ∷ jr ∷ []))
      ≡ just target →
    Result
  countStage p with inspect (fromNatJSON jn)
  ... | nothing , countEq =
    nothing≡just-elim
      (sym
        (cong
          (λ m → maybeBind m
            (fromSpecificationCount stringBase atomBase jtn jcn jd jr))
          countEq)
      ∙ p)
  ... | just count , countEq =
    typeNamesStage count countEq
      (sym
        (cong
          (λ m → maybeBind m
            (fromSpecificationCount stringBase atomBase jtn jcn jd jr))
          countEq)
      ∙ p)

specificationJSONCanonical : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ}
                             {J : Json.AtomUniverse ℓJ} →
                             (stringCodec : CanonicalFromToJSON' J String) →
                             (atomCodeCodec : CanonicalAtomCodeCodec J U) →
                             (j : Json.Json J) →
                             (s : GenericSpecification U) →
                             fromSpecificationJSON (codec stringCodec) (codec atomCodeCodec) j
                               ≡ just s →
                             toSpecificationJSON (codec stringCodec) (codec atomCodeCodec) s ≡ j
specificationJSONCanonical stringCodec atomCodeCodec (Json.atom a x) s p =
  nothing≡just-elim p
specificationJSONCanonical stringCodec atomCodeCodec (Json.object fields) s p =
  nothing≡just-elim p
specificationJSONCanonical stringCodec atomCodeCodec (Json.array []) s p =
  nothing≡just-elim p
specificationJSONCanonical stringCodec atomCodeCodec (Json.array (j₀ ∷ [])) s p =
  nothing≡just-elim p
specificationJSONCanonical stringCodec atomCodeCodec (Json.array (j₀ ∷ j₁ ∷ [])) s p =
  nothing≡just-elim p
specificationJSONCanonical stringCodec atomCodeCodec (Json.array (j₀ ∷ j₁ ∷ j₂ ∷ [])) s p =
  nothing≡just-elim p
specificationJSONCanonical stringCodec atomCodeCodec
  (Json.array (j₀ ∷ j₁ ∷ j₂ ∷ j₃ ∷ [])) s p =
  nothing≡just-elim p
specificationJSONCanonical stringCodec atomCodeCodec
  (Json.array (jn ∷ jtn ∷ jcn ∷ jd ∷ jr ∷ [])) s p =
  SpecificationCanonicalProof.countStage
    stringCodec atomCodeCodec jn jtn jcn jd jr s p
specificationJSONCanonical stringCodec atomCodeCodec
  (Json.array (j₀ ∷ j₁ ∷ j₂ ∷ j₃ ∷ j₄ ∷ j₅ ∷ js)) s p =
  nothing≡just-elim p

canonicalGenericSpecificationFromToJSON :
  ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} →
  (J : Json.AtomUniverse ℓJ) →
  CanonicalFromToJSON' J String →
  CanonicalAtomCodeCodec J U →
  CanonicalFromToJSON' J (GenericSpecification U)
canonicalGenericSpecificationFromToJSON J stringCodec atomCodeCodec =
  canonicalFromToJSON'
    (genericSpecificationFromToJSON J (codec stringCodec) (codec atomCodeCodec))
    (specificationJSONCanonical stringCodec atomCodeCodec)