module Generic.Json where
open import Generic.Core
import Cubical.Data.FinData.Base as FinData
open import Cubical.Data.Maybe.Base using (Maybe; just; nothing)
import FF.Json as Json
infixr 5 _∷ᵈ_ _∷ᵛ_
maybeMap : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (A → B) → Maybe A → Maybe B
maybeMap f (just x) = just (f x)
maybeMap f nothing = nothing
maybeBind : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → Maybe A → (A → Maybe B) → Maybe B
maybeBind (just x) f = f x
maybeBind nothing f = nothing
toJSONWith : ∀ {ℓA ℓJ} {J : Json.AtomUniverse ℓJ} {A : Type ℓA} →
Json.FromToJSON' J A → A → Json.Json J
toJSONWith codec = Json.toJSON (Json.FromToJSON'.to codec)
fromJSONWith : ∀ {ℓA ℓJ} {J : Json.AtomUniverse ℓJ} {A : Type ℓA} →
Json.FromToJSON' J A → Json.Json J → Maybe A
fromJSONWith codec = Json.fromJSON (Json.FromToJSON'.from codec)
roundtripWith : ∀ {ℓA ℓJ} {J : Json.AtomUniverse ℓJ} {A : Type ℓA}
(codec : Json.FromToJSON' J A) →
(x : A) → fromJSONWith codec (toJSONWith codec x) ≡ just x
roundtripWith codec = Json.FromToJSON'.roundtrip codec
tag₀ : ∀ {ℓJ} {J : Json.AtomUniverse ℓJ} → Json.Json J
tag₀ = Json.array []
tag₁ : ∀ {ℓJ} {J : Json.AtomUniverse ℓJ} → Json.Json J
tag₁ = Json.array (tag₀ ∷ [])
toNatJSON : ∀ {ℓJ} {J : Json.AtomUniverse ℓJ} → ℕ → Json.Json J
toNatJSON zero = Json.array []
toNatJSON (suc n) = Json.array (toNatJSON n ∷ [])
fromNatJSON : ∀ {ℓJ} {J : Json.AtomUniverse ℓJ} → Json.Json J → Maybe ℕ
fromNatJSON (Json.array []) = just zero
fromNatJSON (Json.array (x ∷ [])) = maybeMap suc (fromNatJSON x)
fromNatJSON _ = nothing
natJSONRoundtrip : ∀ {ℓJ} {J : Json.AtomUniverse ℓJ} →
(n : ℕ) → fromNatJSON {J = J} (toNatJSON n) ≡ just n
natJSONRoundtrip zero = refl
natJSONRoundtrip {J = J} (suc n) =
cong (maybeMap suc) (natJSONRoundtrip {J = J} n)
fromFin : (n : ℕ) → ℕ → Maybe (Fin n)
fromFin zero _ = nothing
fromFin (suc n) zero = just FinData.zero
fromFin (suc n) (suc k) = maybeMap FinData.suc (fromFin n k)
fromFin-toℕ : ∀ {n} (i : Fin n) → fromFin n (FinData.toℕ i) ≡ just i
fromFin-toℕ FinData.zero = refl
fromFin-toℕ (FinData.suc i) =
cong (maybeMap FinData.suc) (fromFin-toℕ i)
toFinJSON : ∀ {ℓJ n} {J : Json.AtomUniverse ℓJ} → Fin n → Json.Json J
toFinJSON i = toNatJSON (FinData.toℕ i)
fromFinJSON : ∀ {ℓJ} {J : Json.AtomUniverse ℓJ} →
(n : ℕ) → Json.Json J → Maybe (Fin n)
fromFinJSON n j = maybeBind (fromNatJSON j) (fromFin n)
finJSONRoundtrip : ∀ {ℓJ n} {J : Json.AtomUniverse ℓJ} →
(i : Fin n) → fromFinJSON n (toFinJSON {J = J} i) ≡ just i
finJSONRoundtrip {n = n} {J = J} i =
cong (λ m → maybeBind m (fromFin n))
(natJSONRoundtrip {J = J} (FinData.toℕ i))
∙ fromFin-toℕ i
data DescVec {ℓ} (U : AtomUniverse ℓ) (count : ℕ) : ℕ → Type₀ where
[]ᵈ : DescVec U count zero
_∷ᵈ_ : ∀ {len} → TyDesc U count → DescVec U count len → DescVec U count (suc len)
data Vec₀ (A : Type₀) : ℕ → Type₀ where
[]ᵛ : Vec₀ A zero
_∷ᵛ_ : ∀ {len} → A → Vec₀ A len → Vec₀ A (suc len)
lookupDescVec : ∀ {ℓ count len} {U : AtomUniverse ℓ} →
DescVec U count len → Fin len → TyDesc U count
lookupDescVec (d ∷ᵈ ds) FinData.zero = d
lookupDescVec (d ∷ᵈ ds) (FinData.suc i) = lookupDescVec ds i
lookupVec₀ : ∀ {A len} → Vec₀ A len → Fin len → A
lookupVec₀ (x ∷ᵛ xs) FinData.zero = x
lookupVec₀ (x ∷ᵛ xs) (FinData.suc i) = lookupVec₀ xs i
tabulateDescFrom : ∀ {ℓ} {U : AtomUniverse ℓ} →
(count len : ℕ) →
(Fin len → Fin count) →
(Fin count → TyDesc U count) →
DescVec U count len
tabulateDescFrom count zero shift desc = []ᵈ
tabulateDescFrom count (suc len) shift desc =
desc (shift FinData.zero) ∷ᵈ
tabulateDescFrom count len (λ i → shift (FinData.suc i)) desc
tabulateDesc : ∀ {ℓ} {U : AtomUniverse ℓ} →
(count : ℕ) →
(Fin count → TyDesc U count) →
DescVec U count count
tabulateDesc count = tabulateDescFrom count count (λ i → i)
lookupDescVec-tabulateDescFrom : ∀ {ℓ} {U : AtomUniverse ℓ} →
(count len : ℕ) →
(shift : Fin len → Fin count) →
(desc : Fin count → TyDesc U count) →
(i : Fin len) →
lookupDescVec (tabulateDescFrom count len shift desc) i ≡ desc (shift i)
lookupDescVec-tabulateDescFrom count (suc len) shift desc FinData.zero = refl
lookupDescVec-tabulateDescFrom count (suc len) shift desc (FinData.suc i) =
lookupDescVec-tabulateDescFrom count len (λ j → shift (FinData.suc j)) desc i
lookupDescVec-tabulateDesc : ∀ {ℓ} {U : AtomUniverse ℓ} →
(count : ℕ) →
(desc : Fin count → TyDesc U count) →
(i : Fin count) →
lookupDescVec (tabulateDesc count desc) i ≡ desc i
lookupDescVec-tabulateDesc count desc i =
lookupDescVec-tabulateDescFrom count count (λ j → j) desc i
tabulateVecFrom : ∀ {A} →
(count len : ℕ) →
(Fin len → Fin count) →
(Fin count → A) →
Vec₀ A len
tabulateVecFrom count zero shift f = []ᵛ
tabulateVecFrom count (suc len) shift f =
f (shift FinData.zero) ∷ᵛ
tabulateVecFrom count len (λ i → shift (FinData.suc i)) f
tabulateVec : ∀ {A} →
(count : ℕ) →
(Fin count → A) →
Vec₀ A count
tabulateVec count = tabulateVecFrom count count (λ i → i)
lookupVec₀-tabulateVecFrom : ∀ {A} →
(count len : ℕ) →
(shift : Fin len → Fin count) →
(f : Fin count → A) →
(i : Fin len) →
lookupVec₀ (tabulateVecFrom count len shift f) i ≡ f (shift i)
lookupVec₀-tabulateVecFrom count (suc len) shift f FinData.zero = refl
lookupVec₀-tabulateVecFrom count (suc len) shift f (FinData.suc i) =
lookupVec₀-tabulateVecFrom count len (λ j → shift (FinData.suc j)) f i
lookupVec₀-tabulateVec : ∀ {A} →
(count : ℕ) →
(f : Fin count → A) →
(i : Fin count) →
lookupVec₀ (tabulateVec count f) i ≡ f i
lookupVec₀-tabulateVec count f i =
lookupVec₀-tabulateVecFrom count count (λ j → j) f i
record GenericSpecification {ℓ} (U : AtomUniverse ℓ) : Type₀ where
constructor genericSpecification
field
typeCount : ℕ
typeNamesV : Vec₀ String typeCount
constructorNamesV : Vec₀ (List String) typeCount
descs : DescVec U typeCount typeCount
root : RootDesc U typeCount
open GenericSpecification public
specificationOf : ∀ {ℓ} {U : AtomUniverse ℓ} {A : Type ℓ} →
Generic U A → GenericSpecification U
specificationOf g =
genericSpecification
(Generic.typeCount g)
(tabulateVec (Generic.typeCount g) (Generic.typeNames g))
(tabulateVec (Generic.typeCount g) (Generic.constructorNames g))
(tabulateDesc (Generic.typeCount g) (Generic.desc g))
(Generic.root g)
descOfSpecification : ∀ {ℓ} {U : AtomUniverse ℓ} →
(s : GenericSpecification U) →
Fin (typeCount s) → TyDesc U (typeCount s)
descOfSpecification s = lookupDescVec (descs s)
typeNameOfSpecification : ∀ {ℓ} {U : AtomUniverse ℓ} →
(s : GenericSpecification U) →
Fin (typeCount s) → String
typeNameOfSpecification s = lookupVec₀ (typeNamesV s)
constructorNamesOfSpecification : ∀ {ℓ} {U : AtomUniverse ℓ} →
(s : GenericSpecification U) →
Fin (typeCount s) → List String
constructorNamesOfSpecification s = lookupVec₀ (constructorNamesV s)
typeCount-specificationOf : ∀ {ℓ} {U : AtomUniverse ℓ} {A : Type ℓ} →
(g : Generic U A) →
typeCount (specificationOf g) ≡ Generic.typeCount g
typeCount-specificationOf g = refl
descOfSpecification-specificationOf : ∀ {ℓ} {U : AtomUniverse ℓ} {A : Type ℓ} →
(g : Generic U A) →
(i : Fin (Generic.typeCount g)) →
descOfSpecification (specificationOf g) i ≡ Generic.desc g i
descOfSpecification-specificationOf g i =
lookupDescVec-tabulateDesc (Generic.typeCount g) (Generic.desc g) i
typeNameOfSpecification-specificationOf : ∀ {ℓ} {U : AtomUniverse ℓ} {A : Type ℓ} →
(g : Generic U A) →
(i : Fin (Generic.typeCount g)) →
typeNameOfSpecification (specificationOf g) i ≡ Generic.typeNames g i
typeNameOfSpecification-specificationOf g i =
lookupVec₀-tabulateVec (Generic.typeCount g) (Generic.typeNames g) i
constructorNamesOfSpecification-specificationOf : ∀ {ℓ} {U : AtomUniverse ℓ} {A : Type ℓ} →
(g : Generic U A) →
(i : Fin (Generic.typeCount g)) →
constructorNamesOfSpecification (specificationOf g) i
≡ Generic.constructorNames g i
constructorNamesOfSpecification-specificationOf g i =
lookupVec₀-tabulateVec (Generic.typeCount g) (Generic.constructorNames g) i
root-specificationOf : ∀ {ℓ} {U : AtomUniverse ℓ} {A : Type ℓ} →
(g : Generic U A) →
root (specificationOf g) ≡ Generic.root g
root-specificationOf g = refl
AtomCodeCodec : ∀ {ℓ ℓJ} → Json.AtomUniverse ℓJ → AtomUniverse ℓ →
Type (ℓ-max ℓJ ℓ-zero)
AtomCodeCodec J U = Json.FromToJSON' J (AtomCode U)
AtomValueCodecs : ∀ {ℓ ℓJ} → Json.AtomUniverse ℓJ → AtomUniverse ℓ →
Type (ℓ-max ℓ ℓJ)
AtomValueCodecs J U = (a : AtomCode U) → Json.FromToJSON' J (Atom U a)
AtomValueToCodecs : ∀ {ℓ ℓJ} → Json.AtomUniverse ℓJ → AtomUniverse ℓ →
Type (ℓ-max ℓ ℓJ)
AtomValueToCodecs J U = (a : AtomCode U) → Json.ToJSON' J (Atom U a)
fromToAtomValueToCodecs : ∀ {ℓ ℓJ} {J : Json.AtomUniverse ℓJ} {U : AtomUniverse ℓ} →
AtomValueCodecs J U → AtomValueToCodecs J U
fromToAtomValueToCodecs atomCodecs a = Json.FromToJSON'.to (atomCodecs a)
fromFieldDescTag : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → (n : ℕ) → Json.Json J →
ℕ → Maybe (FieldDesc U n)
fromFieldDescTag atomCodeCodec n j zero =
maybeMap fieldRec (fromFinJSON n j)
fromFieldDescTag atomCodeCodec n j (suc zero) =
maybeMap fieldAtom (fromJSONWith atomCodeCodec j)
fromFieldDescTag atomCodeCodec n j (suc (suc _)) = nothing
mutual
toFieldDescJSON : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → FieldDesc U n → Json.Json J
toFieldDescJSON atomCodeCodec (fieldRec i) =
Json.array (tag₀ ∷ toFinJSON i ∷ [])
toFieldDescJSON atomCodeCodec (fieldAtom a) =
Json.array (tag₁ ∷ toJSONWith atomCodeCodec a ∷ [])
fromFieldDescJSON : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → (n : ℕ) → Json.Json J → Maybe (FieldDesc U n)
fromFieldDescJSON atomCodeCodec n (Json.array (tag ∷ j ∷ [])) =
maybeBind (fromNatJSON tag) (fromFieldDescTag atomCodeCodec n j)
fromFieldDescJSON atomCodeCodec n _ = nothing
toFieldDescListJSON : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → List (FieldDesc U n) → List (Json.Json J)
toFieldDescListJSON atomCodeCodec [] = []
toFieldDescListJSON atomCodeCodec (f ∷ fs) =
toFieldDescJSON atomCodeCodec f ∷ toFieldDescListJSON atomCodeCodec fs
fromFieldDescListJSON : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → (n : ℕ) → List (Json.Json J) →
Maybe (List (FieldDesc U n))
fromFieldDescListJSON atomCodeCodec n [] = just []
fromFieldDescListJSON atomCodeCodec n (j ∷ js) =
maybeBind (fromFieldDescJSON atomCodeCodec n j) λ f →
maybeMap (f ∷_) (fromFieldDescListJSON atomCodeCodec n js)
toConDescJSON : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → ConDesc U n → Json.Json J
toConDescJSON atomCodeCodec (con fs) =
Json.array (toFieldDescListJSON atomCodeCodec fs)
fromConDescJSON : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → (n : ℕ) → Json.Json J → Maybe (ConDesc U n)
fromConDescJSON atomCodeCodec n (Json.array js) =
maybeMap con (fromFieldDescListJSON atomCodeCodec n js)
fromConDescJSON atomCodeCodec n _ = nothing
toConDescListJSON : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → List (ConDesc U n) → List (Json.Json J)
toConDescListJSON atomCodeCodec [] = []
toConDescListJSON atomCodeCodec (c ∷ cs) =
toConDescJSON atomCodeCodec c ∷ toConDescListJSON atomCodeCodec cs
fromConDescListJSON : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → (n : ℕ) → List (Json.Json J) →
Maybe (List (ConDesc U n))
fromConDescListJSON atomCodeCodec n [] = just []
fromConDescListJSON atomCodeCodec n (j ∷ js) =
maybeBind (fromConDescJSON atomCodeCodec n j) λ c →
maybeMap (c ∷_) (fromConDescListJSON atomCodeCodec n js)
toTyDescJSON : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → TyDesc U n → Json.Json J
toTyDescJSON atomCodeCodec (dataD cs) =
Json.array (toConDescListJSON atomCodeCodec cs)
fromTyDescJSON : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → (n : ℕ) → Json.Json J → Maybe (TyDesc U n)
fromTyDescJSON atomCodeCodec n (Json.array js) =
maybeMap dataD (fromConDescListJSON atomCodeCodec n js)
fromTyDescJSON atomCodeCodec n _ = nothing
mutual
fieldDescJSONRoundtrip : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodeCodec : AtomCodeCodec J U) →
(f : FieldDesc U n) →
fromFieldDescJSON atomCodeCodec n (toFieldDescJSON atomCodeCodec f) ≡ just f
fieldDescJSONRoundtrip atomCodeCodec (fieldRec i) =
cong (maybeMap fieldRec) (finJSONRoundtrip i)
fieldDescJSONRoundtrip atomCodeCodec (fieldAtom a) =
cong (maybeMap fieldAtom) (roundtripWith atomCodeCodec a)
fieldDescListJSONRoundtrip : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodeCodec : AtomCodeCodec J U) →
(fs : List (FieldDesc U n)) →
fromFieldDescListJSON atomCodeCodec n (toFieldDescListJSON atomCodeCodec fs) ≡ just fs
fieldDescListJSONRoundtrip atomCodeCodec [] = refl
fieldDescListJSONRoundtrip atomCodeCodec (f ∷ fs) =
cong
(λ m →
maybeBind m λ f' →
maybeMap (f' ∷_) (fromFieldDescListJSON atomCodeCodec _ (toFieldDescListJSON atomCodeCodec fs)))
(fieldDescJSONRoundtrip atomCodeCodec f)
∙ cong (maybeMap (f ∷_)) (fieldDescListJSONRoundtrip atomCodeCodec fs)
conDescJSONRoundtrip : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodeCodec : AtomCodeCodec J U) →
(c : ConDesc U n) →
fromConDescJSON atomCodeCodec n (toConDescJSON atomCodeCodec c) ≡ just c
conDescJSONRoundtrip atomCodeCodec (con fs) =
cong (maybeMap con) (fieldDescListJSONRoundtrip atomCodeCodec fs)
conDescListJSONRoundtrip : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodeCodec : AtomCodeCodec J U) →
(cs : List (ConDesc U n)) →
fromConDescListJSON atomCodeCodec n (toConDescListJSON atomCodeCodec cs) ≡ just cs
conDescListJSONRoundtrip atomCodeCodec [] = refl
conDescListJSONRoundtrip atomCodeCodec (c ∷ cs) =
cong
(λ m →
maybeBind m λ c' →
maybeMap (c' ∷_) (fromConDescListJSON atomCodeCodec _ (toConDescListJSON atomCodeCodec cs)))
(conDescJSONRoundtrip atomCodeCodec c)
∙ cong (maybeMap (c ∷_)) (conDescListJSONRoundtrip atomCodeCodec cs)
tyDescJSONRoundtrip : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodeCodec : AtomCodeCodec J U) →
(d : TyDesc U n) →
fromTyDescJSON atomCodeCodec n (toTyDescJSON atomCodeCodec d) ≡ just d
tyDescJSONRoundtrip atomCodeCodec (dataD cs) =
cong (maybeMap dataD) (conDescListJSONRoundtrip atomCodeCodec cs)
toDescVecListJSON : ∀ {ℓ ℓJ count len} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → DescVec U count len → List (Json.Json J)
toDescVecListJSON atomCodeCodec []ᵈ = []
toDescVecListJSON atomCodeCodec (d ∷ᵈ ds) =
toTyDescJSON atomCodeCodec d ∷ toDescVecListJSON atomCodeCodec ds
toDescVecJSON : ∀ {ℓ ℓJ count len} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → DescVec U count len → Json.Json J
toDescVecJSON atomCodeCodec ds = Json.array (toDescVecListJSON atomCodeCodec ds)
fromDescVecJSON : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → (count len : ℕ) →
Json.Json J → Maybe (DescVec U count len)
fromDescVecJSON atomCodeCodec count zero (Json.array []) = just []ᵈ
fromDescVecJSON atomCodeCodec count zero _ = nothing
fromDescVecJSON atomCodeCodec count (suc len) (Json.array (j ∷ js)) =
maybeBind (fromTyDescJSON atomCodeCodec count j) λ d →
maybeMap (d ∷ᵈ_) (fromDescVecJSON atomCodeCodec count len (Json.array js))
fromDescVecJSON atomCodeCodec count (suc len) _ = nothing
descVecJSONRoundtrip : ∀ {ℓ ℓJ count len} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodeCodec : AtomCodeCodec J U) →
(ds : DescVec U count len) →
fromDescVecJSON atomCodeCodec count len (toDescVecJSON atomCodeCodec ds) ≡ just ds
descVecJSONRoundtrip atomCodeCodec []ᵈ = refl
descVecJSONRoundtrip atomCodeCodec (d ∷ᵈ ds) =
cong
(λ m →
maybeBind m λ d' →
maybeMap (d' ∷ᵈ_) (fromDescVecJSON atomCodeCodec _ _ (Json.array (toDescVecListJSON atomCodeCodec ds))))
(tyDescJSONRoundtrip atomCodeCodec d)
∙ cong (maybeMap (d ∷ᵈ_)) (descVecJSONRoundtrip atomCodeCodec ds)
toListJSON : ∀ {ℓJ} {A : Type₀} {J : Json.AtomUniverse ℓJ} →
(A → Json.Json J) → List A → List (Json.Json J)
toListJSON to [] = []
toListJSON to (x ∷ xs) = to x ∷ toListJSON to xs
fromListJSON : ∀ {ℓJ} {A : Type₀} {J : Json.AtomUniverse ℓJ} →
(Json.Json J → Maybe A) → List (Json.Json J) → Maybe (List A)
fromListJSON from [] = just []
fromListJSON from (j ∷ js) =
maybeBind (from j) λ x →
maybeMap (x ∷_) (fromListJSON from js)
listJSONRoundtrip : ∀ {ℓJ} {A : Type₀} {J : Json.AtomUniverse ℓJ}
(to : A → Json.Json J)
(from : Json.Json J → Maybe A)
(round : (x : A) → from (to x) ≡ just x)
(xs : List A) →
fromListJSON from (toListJSON to xs) ≡ just xs
listJSONRoundtrip to from round [] = refl
listJSONRoundtrip to from round (x ∷ xs) =
cong
(λ m →
maybeBind m λ x' →
maybeMap (x' ∷_) (fromListJSON from (toListJSON to xs)))
(round x)
∙ cong (maybeMap (x ∷_)) (listJSONRoundtrip to from round xs)
toVecListJSON : ∀ {ℓJ len} {A : Type₀} {J : Json.AtomUniverse ℓJ} →
(A → Json.Json J) → Vec₀ A len → List (Json.Json J)
toVecListJSON to []ᵛ = []
toVecListJSON to (x ∷ᵛ xs) = to x ∷ toVecListJSON to xs
toVecJSON : ∀ {ℓJ len} {A : Type₀} {J : Json.AtomUniverse ℓJ} →
(A → Json.Json J) → Vec₀ A len → Json.Json J
toVecJSON to xs = Json.array (toVecListJSON to xs)
fromVecJSON : ∀ {ℓJ} {A : Type₀} {J : Json.AtomUniverse ℓJ} →
(Json.Json J → Maybe A) → (len : ℕ) → Json.Json J → Maybe (Vec₀ A len)
fromVecJSON from zero (Json.array []) = just []ᵛ
fromVecJSON from zero _ = nothing
fromVecJSON from (suc len) (Json.array (j ∷ js)) =
maybeBind (from j) λ x →
maybeMap (x ∷ᵛ_) (fromVecJSON from len (Json.array js))
fromVecJSON from (suc len) _ = nothing
vecJSONRoundtrip : ∀ {ℓJ len} {A : Type₀} {J : Json.AtomUniverse ℓJ}
(to : A → Json.Json J)
(from : Json.Json J → Maybe A)
(round : (x : A) → from (to x) ≡ just x)
(xs : Vec₀ A len) →
fromVecJSON from len (toVecJSON to xs) ≡ just xs
vecJSONRoundtrip to from round []ᵛ = refl
vecJSONRoundtrip to from round (x ∷ᵛ xs) =
cong
(λ m →
maybeBind m λ x' →
maybeMap (x' ∷ᵛ_) (fromVecJSON from _ (Json.array (toVecListJSON to xs))))
(round x)
∙ cong (maybeMap (x ∷ᵛ_)) (vecJSONRoundtrip to from round xs)
toStringListJSON : ∀ {ℓJ} {J : Json.AtomUniverse ℓJ} →
Json.FromToJSON' J String → List String → Json.Json J
toStringListJSON stringCodec xs =
Json.array (toListJSON (toJSONWith stringCodec) xs)
fromStringListJSON : ∀ {ℓJ} {J : Json.AtomUniverse ℓJ} →
Json.FromToJSON' J String → Json.Json J → Maybe (List String)
fromStringListJSON stringCodec (Json.array js) =
fromListJSON (fromJSONWith stringCodec) js
fromStringListJSON stringCodec _ = nothing
stringListJSONRoundtrip : ∀ {ℓJ} {J : Json.AtomUniverse ℓJ}
(stringCodec : Json.FromToJSON' J String) →
(xs : List String) →
fromStringListJSON stringCodec (toStringListJSON stringCodec xs) ≡ just xs
stringListJSONRoundtrip stringCodec =
listJSONRoundtrip
(toJSONWith stringCodec)
(fromJSONWith stringCodec)
(roundtripWith stringCodec)
toRootDescJSON : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → RootDesc U n → Json.Json J
toRootDescJSON atomCodeCodec (rootData i) =
Json.array (tag₀ ∷ toFinJSON i ∷ [])
toRootDescJSON atomCodeCodec (rootAtom a) =
Json.array (tag₁ ∷ toJSONWith atomCodeCodec a ∷ [])
fromRootDescTag : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → (n : ℕ) → Json.Json J →
ℕ → Maybe (RootDesc U n)
fromRootDescTag atomCodeCodec n j zero =
maybeMap rootData (fromFinJSON n j)
fromRootDescTag atomCodeCodec n j (suc zero) =
maybeMap rootAtom (fromJSONWith atomCodeCodec j)
fromRootDescTag atomCodeCodec n j (suc (suc _)) = nothing
fromRootDescJSON : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
AtomCodeCodec J U → (n : ℕ) → Json.Json J → Maybe (RootDesc U n)
fromRootDescJSON atomCodeCodec n (Json.array (tag ∷ j ∷ [])) =
maybeBind (fromNatJSON tag) (fromRootDescTag atomCodeCodec n j)
fromRootDescJSON atomCodeCodec n _ = nothing
rootDescJSONRoundtrip : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodeCodec : AtomCodeCodec J U) →
(r : RootDesc U n) →
fromRootDescJSON atomCodeCodec n (toRootDescJSON atomCodeCodec r) ≡ just r
rootDescJSONRoundtrip atomCodeCodec (rootData i) =
cong (maybeMap rootData) (finJSONRoundtrip i)
rootDescJSONRoundtrip atomCodeCodec (rootAtom a) =
cong (maybeMap rootAtom) (roundtripWith atomCodeCodec a)
toSpecificationJSON : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
Json.FromToJSON' J String →
AtomCodeCodec J U → GenericSpecification U → Json.Json J
toSpecificationJSON stringCodec atomCodeCodec (genericSpecification count typeNames constructorNames descs root) =
Json.array
( toNatJSON count
∷ toVecJSON (toJSONWith stringCodec) typeNames
∷ toVecJSON (toStringListJSON stringCodec) constructorNames
∷ toDescVecJSON atomCodeCodec descs
∷ toRootDescJSON atomCodeCodec root
∷ [] )
fromSpecificationRoot : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
(count : ℕ) →
Vec₀ String count →
Vec₀ (List String) count →
AtomCodeCodec J U → Json.Json J →
DescVec U count count →
Maybe (GenericSpecification U)
fromSpecificationRoot count typeNames constructorNames atomCodeCodec jr descs =
maybeMap
(genericSpecification count typeNames constructorNames descs)
(fromRootDescJSON atomCodeCodec count jr)
fromSpecificationDescs : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
(count : ℕ) →
Vec₀ String count →
AtomCodeCodec J U → Json.Json J → Json.Json J →
Vec₀ (List String) count →
Maybe (GenericSpecification U)
fromSpecificationDescs count typeNames atomCodeCodec jd jr constructorNames =
maybeBind
(fromDescVecJSON atomCodeCodec count count jd)
(fromSpecificationRoot count typeNames constructorNames atomCodeCodec jr)
fromSpecificationConstructorNames :
∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
(count : ℕ) →
Json.FromToJSON' J String → AtomCodeCodec J U →
Json.Json J → Json.Json J → Json.Json J →
Vec₀ String count →
Maybe (GenericSpecification U)
fromSpecificationConstructorNames count stringCodec atomCodeCodec jcn jd jr typeNames =
maybeBind
(fromVecJSON (fromStringListJSON stringCodec) count jcn)
(fromSpecificationDescs count typeNames atomCodeCodec jd jr)
fromSpecificationTypeNames :
∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
Json.FromToJSON' J String → AtomCodeCodec J U →
Json.Json J → Json.Json J → Json.Json J → Json.Json J →
(count : ℕ) →
Maybe (GenericSpecification U)
fromSpecificationTypeNames stringCodec atomCodeCodec jtn jcn jd jr count =
maybeBind
(fromVecJSON (fromJSONWith stringCodec) count jtn)
(fromSpecificationConstructorNames
count stringCodec atomCodeCodec jcn jd jr)
fromSpecificationCount :
∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
Json.FromToJSON' J String → AtomCodeCodec J U →
Json.Json J → Json.Json J → Json.Json J → Json.Json J →
ℕ → Maybe (GenericSpecification U)
fromSpecificationCount stringCodec atomCodeCodec jtn jcn jd jr count =
fromSpecificationTypeNames stringCodec atomCodeCodec jtn jcn jd jr count
fromSpecificationJSON : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ} →
Json.FromToJSON' J String →
AtomCodeCodec J U → Json.Json J → Maybe (GenericSpecification U)
fromSpecificationJSON stringCodec atomCodeCodec (Json.array (jn ∷ jtn ∷ jcn ∷ jd ∷ jr ∷ [])) =
maybeBind (fromNatJSON jn)
(fromSpecificationCount stringCodec atomCodeCodec jtn jcn jd jr)
fromSpecificationJSON stringCodec atomCodeCodec _ = nothing
specificationJSONRoundtrip : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(stringCodec : Json.FromToJSON' J String) →
(atomCodeCodec : AtomCodeCodec J U) →
(s : GenericSpecification U) →
fromSpecificationJSON stringCodec atomCodeCodec (toSpecificationJSON stringCodec atomCodeCodec s) ≡ just s
specificationJSONRoundtrip stringCodec atomCodeCodec (genericSpecification count typeNames constructorNames descs root) =
cong
(λ m →
maybeBind m λ count' →
maybeBind (fromVecJSON (fromJSONWith stringCodec) count' (toVecJSON (toJSONWith stringCodec) typeNames)) λ typeNames' →
maybeBind (fromVecJSON (fromStringListJSON stringCodec) count' (toVecJSON (toStringListJSON stringCodec) constructorNames)) λ constructorNames' →
maybeBind (fromDescVecJSON atomCodeCodec count' count' (toDescVecJSON atomCodeCodec descs)) λ descs' →
maybeMap (genericSpecification count' typeNames' constructorNames' descs') (fromRootDescJSON atomCodeCodec count' (toRootDescJSON atomCodeCodec root)))
(natJSONRoundtrip count)
∙ cong
(λ m →
maybeBind m λ typeNames' →
maybeBind (fromVecJSON (fromStringListJSON stringCodec) count (toVecJSON (toStringListJSON stringCodec) constructorNames)) λ constructorNames' →
maybeBind (fromDescVecJSON atomCodeCodec count count (toDescVecJSON atomCodeCodec descs)) λ descs' →
maybeMap (genericSpecification count typeNames' constructorNames' descs') (fromRootDescJSON atomCodeCodec count (toRootDescJSON atomCodeCodec root)))
(vecJSONRoundtrip
(toJSONWith stringCodec)
(fromJSONWith stringCodec)
(roundtripWith stringCodec)
typeNames)
∙ cong
(λ m →
maybeBind m λ constructorNames' →
maybeBind (fromDescVecJSON atomCodeCodec count count (toDescVecJSON atomCodeCodec descs)) λ descs' →
maybeMap (genericSpecification count typeNames constructorNames' descs') (fromRootDescJSON atomCodeCodec count (toRootDescJSON atomCodeCodec root)))
(vecJSONRoundtrip
(toStringListJSON stringCodec)
(fromStringListJSON stringCodec)
(stringListJSONRoundtrip stringCodec)
constructorNames)
∙ cong
(λ m →
maybeBind m λ descs' →
maybeMap (genericSpecification count typeNames constructorNames descs') (fromRootDescJSON atomCodeCodec count (toRootDescJSON atomCodeCodec root)))
(descVecJSONRoundtrip atomCodeCodec descs)
∙ cong (maybeMap (genericSpecification count typeNames constructorNames descs)) (rootDescJSONRoundtrip atomCodeCodec root)
genericSpecificationFromToJSON : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ}
(J : Json.AtomUniverse ℓJ) →
Json.FromToJSON' J String →
AtomCodeCodec J U →
Json.FromToJSON' J (GenericSpecification U)
genericSpecificationFromToJSON J stringCodec atomCodeCodec =
Json.mkFromToJSON'
(Json.mkToJSON' (toSpecificationJSON stringCodec atomCodeCodec))
(Json.mkFromJSON' (fromSpecificationJSON stringCodec atomCodeCodec))
(specificationJSONRoundtrip stringCodec atomCodeCodec)
listIxToNat : ∀ {ℓ} {A : Type ℓ} {xs : List A} → ListIx xs → ℕ
listIxToNat here = zero
listIxToNat (there i) = suc (listIxToNat i)
toListIxJSON' : ∀ {ℓ ℓJ} {A : Type ℓ} {xs : List A} {J : Json.AtomUniverse ℓJ} →
ListIx xs → Json.Json J
toListIxJSON' i = toNatJSON (listIxToNat i)
fromListIx : ∀ {ℓ} {A : Type ℓ} (xs : List A) → ℕ → Maybe (ListIx xs)
fromListIx [] n = nothing
fromListIx (x ∷ xs) zero = just here
fromListIx (x ∷ xs) (suc n) = maybeMap there (fromListIx xs n)
fromListIx-toNat : ∀ {ℓ} {A : Type ℓ} {xs : List A} →
(i : ListIx xs) → fromListIx xs (listIxToNat i) ≡ just i
fromListIx-toNat here = refl
fromListIx-toNat (there i) =
cong (maybeMap there) (fromListIx-toNat i)
fromListIxJSON : ∀ {ℓ ℓJ} {A : Type ℓ} {J : Json.AtomUniverse ℓJ} →
(xs : List A) → Json.Json J → Maybe (ListIx xs)
fromListIxJSON xs j = maybeBind (fromNatJSON j) (fromListIx xs)
listIxJSONRoundtrip : ∀ {ℓ ℓJ} {A : Type ℓ} {xs : List A} {J : Json.AtomUniverse ℓJ} →
(i : ListIx xs) →
fromListIxJSON xs (toListIxJSON' {J = J} i) ≡ just i
listIxJSONRoundtrip {xs = xs} {J = J} i =
cong (λ m → maybeBind m (fromListIx xs))
(natJSONRoundtrip {J = J} (listIxToNat i))
∙ fromListIx-toNat i
mutual
toCodeJSONWith : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueToCodecs J U) →
(D : Fin n → TyDesc U n) →
{d : TyDesc U n} →
CodeIx U D d → Json.Json J
toCodeJSONWith atomCodecs D (nodeIx c args) =
Json.array (toListIxJSON' c ∷ toArgsCodeJSONWith atomCodecs D args ∷ [])
toFieldCodeJSONWith : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueToCodecs J U) →
(D : Fin n → TyDesc U n) →
{f : FieldDesc U n} →
FieldCodeIx U D f → Json.Json J
toFieldCodeJSONWith atomCodecs D (recIx x) = toCodeJSONWith atomCodecs D x
toFieldCodeJSONWith atomCodecs D (atomIx {a = a} x) = Json.toJSON (atomCodecs a) x
toArgsCodeListJSONWith : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueToCodecs J U) →
(D : Fin n → TyDesc U n) →
{c : ConDesc U n} →
ArgsCodeIx U D c → List (Json.Json J)
toArgsCodeListJSONWith atomCodecs D []ⁱ = []
toArgsCodeListJSONWith atomCodecs D (x ∷ⁱ xs) =
toFieldCodeJSONWith atomCodecs D x ∷ toArgsCodeListJSONWith atomCodecs D xs
toArgsCodeJSONWith : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueToCodecs J U) →
(D : Fin n → TyDesc U n) →
{c : ConDesc U n} →
ArgsCodeIx U D c → Json.Json J
toArgsCodeJSONWith atomCodecs D xs = Json.array (toArgsCodeListJSONWith atomCodecs D xs)
toRootCodeJSONWith : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueToCodecs J U) →
(D : Fin n → TyDesc U n) →
(r : RootDesc U n) →
RootCodeIx U D r → Json.Json J
toRootCodeJSONWith atomCodecs D (rootData i) (rootDataIx x) = toCodeJSONWith atomCodecs D x
toRootCodeJSONWith atomCodecs D (rootAtom a) (rootAtomIx x) = Json.toJSON (atomCodecs a) x
genericToJSON : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {A : Type ℓ}
(J : Json.AtomUniverse ℓJ) →
(atomCodecs : AtomValueToCodecs J U) →
(g : Generic U A) →
Json.ToJSON' J A
genericToJSON J atomCodecs g =
Json.mkToJSON' λ x →
toRootCodeJSONWith atomCodecs (Generic.desc g) (Generic.root g) (Generic.encode g x)
mutual
toCodeJSON : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueCodecs J U) →
(D : Fin n → TyDesc U n) →
{d : TyDesc U n} →
CodeIx U D d → Json.Json J
toCodeJSON atomCodecs D (nodeIx c args) =
Json.array (toListIxJSON' c ∷ toArgsCodeJSON atomCodecs D args ∷ [])
toFieldCodeJSON : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueCodecs J U) →
(D : Fin n → TyDesc U n) →
{f : FieldDesc U n} →
FieldCodeIx U D f → Json.Json J
toFieldCodeJSON atomCodecs D (recIx x) = toCodeJSON atomCodecs D x
toFieldCodeJSON atomCodecs D (atomIx {a = a} x) = toJSONWith (atomCodecs a) x
toArgsCodeListJSON : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueCodecs J U) →
(D : Fin n → TyDesc U n) →
{c : ConDesc U n} →
ArgsCodeIx U D c → List (Json.Json J)
toArgsCodeListJSON atomCodecs D []ⁱ = []
toArgsCodeListJSON atomCodecs D (x ∷ⁱ xs) =
toFieldCodeJSON atomCodecs D x ∷ toArgsCodeListJSON atomCodecs D xs
toArgsCodeJSON : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueCodecs J U) →
(D : Fin n → TyDesc U n) →
{c : ConDesc U n} →
ArgsCodeIx U D c → Json.Json J
toArgsCodeJSON atomCodecs D xs = Json.array (toArgsCodeListJSON atomCodecs D xs)
fromCodeJSON : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueCodecs J U) →
(D : Fin n → TyDesc U n) →
(d : TyDesc U n) →
Json.Json J → Maybe (CodeIx U D d)
fromCodeJSON atomCodecs D (dataD cs) (Json.array (jc ∷ ja ∷ [])) =
maybeBind (fromListIxJSON cs jc) λ c →
maybeMap (nodeIx c) (fromArgsCodeJSON atomCodecs D (lookup c) ja)
fromCodeJSON atomCodecs D d _ = nothing
fromFieldCodeJSON : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueCodecs J U) →
(D : Fin n → TyDesc U n) →
(f : FieldDesc U n) →
Json.Json J → Maybe (FieldCodeIx U D f)
fromFieldCodeJSON atomCodecs D (fieldRec i) j =
maybeMap recIx (fromCodeJSON atomCodecs D (D i) j)
fromFieldCodeJSON atomCodecs D (fieldAtom a) j =
maybeMap atomIx (fromJSONWith (atomCodecs a) j)
fromArgsCodeJSON : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueCodecs J U) →
(D : Fin n → TyDesc U n) →
(c : ConDesc U n) →
Json.Json J → Maybe (ArgsCodeIx U D c)
fromArgsCodeJSON atomCodecs D (con []) (Json.array []) = just []ⁱ
fromArgsCodeJSON atomCodecs D (con []) _ = nothing
fromArgsCodeJSON atomCodecs D (con (f ∷ fs)) (Json.array (j ∷ js)) =
maybeBind (fromFieldCodeJSON atomCodecs D f j) λ x →
maybeMap (x ∷ⁱ_) (fromArgsCodeJSON atomCodecs D (con fs) (Json.array js))
fromArgsCodeJSON atomCodecs D (con (f ∷ fs)) _ = nothing
mutual
codeJSONRoundtrip : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueCodecs J U) →
(D : Fin n → TyDesc U n) →
{d : TyDesc U n} →
(x : CodeIx U D d) →
fromCodeJSON atomCodecs D d (toCodeJSON atomCodecs D x) ≡ just x
codeJSONRoundtrip atomCodecs D (nodeIx c args) =
cong
(λ m →
maybeBind m λ c' →
maybeMap (nodeIx c') (fromArgsCodeJSON atomCodecs D (lookup c') (toArgsCodeJSON atomCodecs D args)))
(listIxJSONRoundtrip c)
∙ cong (maybeMap (nodeIx c)) (argsCodeJSONRoundtrip atomCodecs D args)
fieldCodeJSONRoundtrip : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueCodecs J U) →
(D : Fin n → TyDesc U n) →
{f : FieldDesc U n} →
(x : FieldCodeIx U D f) →
fromFieldCodeJSON atomCodecs D f (toFieldCodeJSON atomCodecs D x) ≡ just x
fieldCodeJSONRoundtrip atomCodecs D (recIx x) =
cong (maybeMap recIx) (codeJSONRoundtrip atomCodecs D x)
fieldCodeJSONRoundtrip atomCodecs D (atomIx {a = a} x) =
cong (maybeMap atomIx) (roundtripWith (atomCodecs a) x)
argsCodeJSONRoundtrip : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueCodecs J U) →
(D : Fin n → TyDesc U n) →
{c : ConDesc U n} →
(xs : ArgsCodeIx U D c) →
fromArgsCodeJSON atomCodecs D c (toArgsCodeJSON atomCodecs D xs) ≡ just xs
argsCodeJSONRoundtrip atomCodecs D []ⁱ = refl
argsCodeJSONRoundtrip atomCodecs D (x ∷ⁱ xs) =
cong
(λ m →
maybeBind m λ x' →
maybeMap (x' ∷ⁱ_) (fromArgsCodeJSON atomCodecs D _ (Json.array (toArgsCodeListJSON atomCodecs D xs))))
(fieldCodeJSONRoundtrip atomCodecs D x)
∙ cong (maybeMap (x ∷ⁱ_)) (argsCodeJSONRoundtrip atomCodecs D xs)
toRootCodeJSON : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueCodecs J U) →
(D : Fin n → TyDesc U n) →
(r : RootDesc U n) →
RootCodeIx U D r → Json.Json J
toRootCodeJSON atomCodecs D (rootData i) (rootDataIx x) = toCodeJSON atomCodecs D x
toRootCodeJSON atomCodecs D (rootAtom a) (rootAtomIx x) = toJSONWith (atomCodecs a) x
fromRootCodeJSON : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueCodecs J U) →
(D : Fin n → TyDesc U n) →
(r : RootDesc U n) →
Json.Json J → Maybe (RootCodeIx U D r)
fromRootCodeJSON atomCodecs D (rootData i) j =
maybeMap rootDataIx (fromCodeJSON atomCodecs D (D i) j)
fromRootCodeJSON atomCodecs D (rootAtom a) j =
maybeMap rootAtomIx (fromJSONWith (atomCodecs a) j)
rootCodeJSONRoundtrip : ∀ {ℓ ℓJ n} {U : AtomUniverse ℓ} {J : Json.AtomUniverse ℓJ}
(atomCodecs : AtomValueCodecs J U) →
(D : Fin n → TyDesc U n) →
(r : RootDesc U n) →
(x : RootCodeIx U D r) →
fromRootCodeJSON atomCodecs D r (toRootCodeJSON atomCodecs D r x) ≡ just x
rootCodeJSONRoundtrip atomCodecs D (rootData i) (rootDataIx x) =
cong (maybeMap rootDataIx) (codeJSONRoundtrip atomCodecs D x)
rootCodeJSONRoundtrip atomCodecs D (rootAtom a) (rootAtomIx x) =
cong (maybeMap rootAtomIx) (roundtripWith (atomCodecs a) x)
genericFromToJSON : ∀ {ℓ ℓJ} {U : AtomUniverse ℓ} {A : Type ℓ}
(J : Json.AtomUniverse ℓJ) →
(atomCodecs : AtomValueCodecs J U) →
(g : Generic U A) →
Json.FromToJSON' J A
genericFromToJSON J atomCodecs g =
Json.mkFromToJSON' to from round
where
D = Generic.desc g
r = Generic.root g
to : Json.ToJSON' J _
to = Json.mkToJSON' λ x →
toRootCodeJSON atomCodecs D r (Generic.encode g x)
from : Json.FromJSON' J _
from = Json.mkFromJSON' λ j →
maybeMap (Generic.decode g) (fromRootCodeJSON atomCodecs D r j)
round : (x : _) → Json.fromJSON from (Json.toJSON to x) ≡ just x
round x =
cong (maybeMap (Generic.decode g))
(rootCodeJSONRoundtrip atomCodecs D r (Generic.encode g x))
∙ cong just (Generic.decode-encode g x)