Generic.Examples

module Generic.Examples where

open import Generic.Core
open import Generic.Family
open import Generic.Certified
open import Generic.Macro
open import Generic.Macro.Family using
  ( deriveGenericFamilyIn1
  ; deriveGenericFamilyIn2
  ; deriveGenericReachableIn
  ; deriveGenericFamilyBundleIn1
  ; deriveCertifiedGenericFamilyBundleIn2
  ; deriveCertifiedGenericReachableIn
  )

data Color : Type₀ where
  red green blue : Color

data Direction : Type₀ where
  north east south west : Direction

data MaybeNat : Type₀ where
  none : MaybeNat
  some : ℕ → MaybeNat

data ListNat : Type₀ where
  nil  : ListNat
  cons : ℕ → ListNat → ListNat

data ExampleAtomCode : Type₀ where
  natA stringA boolA directionA unitA colorA maybeNatA listNatA : ExampleAtomCode

ExampleAtom : ExampleAtomCode → Type₀
ExampleAtom natA = ℕ
ExampleAtom stringA = String
ExampleAtom boolA = Bool
ExampleAtom directionA = Direction
ExampleAtom unitA = Unit
ExampleAtom colorA = Color
ExampleAtom maybeNatA = MaybeNat
ExampleAtom listNatA = ListNat

ExampleAtoms : AtomUniverse ℓ-zero
ExampleAtoms = atomUniverse ExampleAtomCode ExampleAtom

ColorDesc : Fin 1 → TyDesc ExampleAtoms 1
ColorDesc Fin.zero =
  dataD (con [] ∷ con [] ∷ con [] ∷ [])

encodeColor : Color → RootCodeIx ExampleAtoms ColorDesc (rootData Fin.zero)
encodeColor red   = rootDataIx (ν₀ ι₀)
encodeColor green = rootDataIx (ν₀ ι₁)
encodeColor blue  = rootDataIx (ν₀ ι₂)

decodeColor : RootCodeIx ExampleAtoms ColorDesc (rootData Fin.zero) → Color
decodeColor (rootDataIx (ν₀ ι₀)) = red
decodeColor (rootDataIx (ν₀ ι₁)) = green
decodeColor (rootDataIx (ν₀ ι₂)) = blue

decode-encodeColor : (x : Color) → decodeColor (encodeColor x) ≡ x
decode-encodeColor red = refl
decode-encodeColor green = refl
decode-encodeColor blue = refl

encode-decodeColor : (x : RootCodeIx ExampleAtoms ColorDesc (rootData Fin.zero)) → encodeColor (decodeColor x) ≡ x
encode-decodeColor (rootDataIx (ν₀ ι₀)) = refl
encode-decodeColor (rootDataIx (ν₀ ι₁)) = refl
encode-decodeColor (rootDataIx (ν₀ ι₂)) = refl

genericColor : Generic ExampleAtoms Color
genericColor =
  generic 1 ColorDesc (rootData Fin.zero)
    (λ { Fin.zero → "Color" })
    (λ { Fin.zero → "red" ∷ "green" ∷ "blue" ∷ [] })
    encodeColor decodeColor
    decode-encodeColor encode-decodeColor

certifiedGenericColor : CertifiedGeneric ExampleAtoms Color
certifiedGenericColor =
  certifiedGeneric genericColor
    (λ { Fin.zero → _∷ⁿ_ (_∷ⁿ_ (_∷ⁿ_ []ⁿ)) })

inferredDirection : InferredGeneric Direction
inferredDirection = deriveGenericEnum Direction

genericDirection : Generic (fst inferredDirection) Direction
genericDirection = snd inferredDirection

data AutoBuiltinLiterals : Type₀ where
  auto-lit-none : AutoBuiltinLiterals
  auto-lit-nat  : ℕ → AutoBuiltinLiterals
  auto-lit-mix  : String → Bool → Unit → AutoBuiltinLiterals

genericAutoBuiltinLiterals : Generic BuiltinAtoms AutoBuiltinLiterals
genericAutoBuiltinLiterals = deriveGenericIn BuiltinAtoms AutoBuiltinLiterals

data AutoMaybeNat : Type₀ where
  auto-none : AutoMaybeNat
  auto-some : ℕ → AutoMaybeNat

genericAutoMaybeNat : Generic BuiltinAtoms AutoMaybeNat
genericAutoMaybeNat = deriveGenericIn BuiltinAtoms AutoMaybeNat

data AutoRecordLike : Type₀ where
  auto-record-like : ℕ → Unit → AutoRecordLike

genericAutoRecordLike : Generic BuiltinAtoms AutoRecordLike
genericAutoRecordLike = deriveGenericIn BuiltinAtoms AutoRecordLike

record AutoBuiltinRecord : Type₀ where
  constructor auto-builtin-record
  field
    autoRecordNat : ℕ
    autoRecordBool : Bool
    autoRecordUnit : Unit

genericAutoBuiltinRecord : Generic BuiltinAtoms AutoBuiltinRecord
genericAutoBuiltinRecord = deriveGenericIn BuiltinAtoms AutoBuiltinRecord

record AutoInferredRecord : Type₀ where
  constructor auto-inferred-record
  field
    autoInferredColor : Color
    autoInferredDirection : Direction

inferredAutoInferredRecord : InferredGeneric AutoInferredRecord
inferredAutoInferredRecord = deriveGeneric AutoInferredRecord

genericAutoInferredRecord : Generic (fst inferredAutoInferredRecord) AutoInferredRecord
genericAutoInferredRecord = snd inferredAutoInferredRecord

data AutoShape : Type₀ where
  auto-point  : AutoShape
  auto-circle : ℕ → AutoShape
  auto-rect   : ℕ → ℕ → AutoShape
  auto-label  : Color → Direction → AutoShape

genericAutoShape : Generic ExampleAtoms AutoShape
genericAutoShape = deriveGenericIn ExampleAtoms AutoShape

certifiedGenericAutoShape : CertifiedGeneric ExampleAtoms AutoShape
certifiedGenericAutoShape = deriveCertifiedGenericIn ExampleAtoms AutoShape

data AutoRepeatedFields : Type₀ where
  auto-repeated : ℕ → ℕ → ℕ → AutoRepeatedFields

genericAutoRepeatedFields : Generic BuiltinAtoms AutoRepeatedFields
genericAutoRepeatedFields = deriveGenericIn BuiltinAtoms AutoRepeatedFields

MaybeNatDesc : Fin 1 → TyDesc ExampleAtoms 1
MaybeNatDesc Fin.zero = dataD (con [] ∷ con (fieldAtom natA ∷ []) ∷ [])

encodeMaybeNat : MaybeNat → RootCodeIx ExampleAtoms MaybeNatDesc (rootData Fin.zero)
encodeMaybeNat none = rootDataIx (ν₀ ι₀)
encodeMaybeNat (some n) =
  rootDataIx (ν₁ ι₁ (atomIx n))

decodeMaybeNat : RootCodeIx ExampleAtoms MaybeNatDesc (rootData Fin.zero) → MaybeNat
decodeMaybeNat (rootDataIx (ν₀ ι₀)) = none
decodeMaybeNat (rootDataIx (ν₁ ι₁ (atomIx n))) = some n

decode-encodeMaybeNat : (x : MaybeNat) → decodeMaybeNat (encodeMaybeNat x) ≡ x
decode-encodeMaybeNat none = refl
decode-encodeMaybeNat (some n) = refl

encode-decodeMaybeNat : (x : RootCodeIx ExampleAtoms MaybeNatDesc (rootData Fin.zero)) → encodeMaybeNat (decodeMaybeNat x) ≡ x
encode-decodeMaybeNat (rootDataIx (ν₀ ι₀)) = refl
encode-decodeMaybeNat (rootDataIx (ν₁ ι₁ (atomIx n))) = refl

genericMaybeNat : Generic ExampleAtoms MaybeNat
genericMaybeNat =
  generic 1 MaybeNatDesc (rootData Fin.zero)
    (λ { Fin.zero → "MaybeNat" })
    (λ { Fin.zero → "none" ∷ "some" ∷ [] })
    encodeMaybeNat decodeMaybeNat
    decode-encodeMaybeNat encode-decodeMaybeNat

certifiedGenericMaybeNat : CertifiedGeneric ExampleAtoms MaybeNat
certifiedGenericMaybeNat =
  certifiedGeneric genericMaybeNat
    (λ { Fin.zero → _∷ⁿ_ (_∷ⁿ_ []ⁿ) })

ListNatDesc : Fin 1 → TyDesc ExampleAtoms 1
ListNatDesc Fin.zero =
  dataD (con [] ∷ con (fieldAtom natA ∷ fieldRec Fin.zero ∷ []) ∷ [])

encodeListNat : ListNat → CodeIx ExampleAtoms ListNatDesc (ListNatDesc Fin.zero)
encodeListNat nil = ν₀ ι₀
encodeListNat (cons n xs) =
  ν₂ ι₁ (atomIx n) (recIx (encodeListNat xs))

decodeListNat : CodeIx ExampleAtoms ListNatDesc (ListNatDesc Fin.zero) → ListNat
decodeListNat (ν₀ ι₀) = nil
decodeListNat (ν₂ ι₁ (atomIx n) (recIx xs)) =
  cons n (decodeListNat xs)

decode-encodeListNat : (x : ListNat) → decodeListNat (encodeListNat x) ≡ x
decode-encodeListNat nil = refl
decode-encodeListNat (cons n xs) = cong (cons n) (decode-encodeListNat xs)

encode-decodeListNat : (x : CodeIx ExampleAtoms ListNatDesc (ListNatDesc Fin.zero)) → encodeListNat (decodeListNat x) ≡ x
encode-decodeListNat (ν₀ ι₀) = refl
encode-decodeListNat (ν₂ ι₁ (atomIx n) (recIx xs)) =
  cong (λ ys → ν₂ ι₁ (atomIx n) (recIx ys))
    (encode-decodeListNat xs)

encodeListNatRoot : ListNat → RootCodeIx ExampleAtoms ListNatDesc (rootData Fin.zero)
encodeListNatRoot x = rootDataIx (encodeListNat x)

decodeListNatRoot : RootCodeIx ExampleAtoms ListNatDesc (rootData Fin.zero) → ListNat
decodeListNatRoot (rootDataIx x) = decodeListNat x

decode-encodeListNatRoot : (x : ListNat) → decodeListNatRoot (encodeListNatRoot x) ≡ x
decode-encodeListNatRoot = decode-encodeListNat

encode-decodeListNatRoot : (x : RootCodeIx ExampleAtoms ListNatDesc (rootData Fin.zero)) → encodeListNatRoot (decodeListNatRoot x) ≡ x
encode-decodeListNatRoot (rootDataIx x) =
  cong rootDataIx (encode-decodeListNat x)

genericListNat : Generic ExampleAtoms ListNat
genericListNat =
  generic 1 ListNatDesc (rootData Fin.zero)
    (λ { Fin.zero → "ListNat" })
    (λ { Fin.zero → "nil" ∷ "cons" ∷ [] })
    encodeListNatRoot decodeListNatRoot
    decode-encodeListNatRoot encode-decodeListNatRoot

certifiedGenericListNat : CertifiedGeneric ExampleAtoms ListNat
certifiedGenericListNat =
  certifiedGeneric genericListNat
    (λ { Fin.zero → _∷ⁿ_ (_∷ⁿ_ []ⁿ) })

data AutoNestedAtoms : Type₀ where
  auto-nested : MaybeNat → ListNat → AutoNestedAtoms

genericAutoNestedAtoms : Generic ExampleAtoms AutoNestedAtoms
genericAutoNestedAtoms = deriveGenericIn ExampleAtoms AutoNestedAtoms

data AutoLargeConstructor : Type₀ where
  auto-large : Unit → ℕ → Color → Direction → MaybeNat → AutoLargeConstructor

genericAutoLargeConstructor : Generic ExampleAtoms AutoLargeConstructor
genericAutoLargeConstructor = deriveGenericIn ExampleAtoms AutoLargeConstructor

data Even : Type₀
data Odd : Type₀

data Even where
  even-zero : Even
  even-suc  : Odd → Even

data Odd where
  odd-suc : Even → Odd

EvenOddDesc : Fin 2 → TyDesc ExampleAtoms 2
EvenOddDesc Fin.zero =
  dataD (con [] ∷ con (fieldRec (Fin.suc Fin.zero) ∷ []) ∷ [])
EvenOddDesc (Fin.suc Fin.zero) =
  dataD (con (fieldRec Fin.zero ∷ []) ∷ [])

mutual
  encodeEven : Even → CodeIx ExampleAtoms EvenOddDesc (EvenOddDesc Fin.zero)
  encodeEven even-zero = ν₀ ι₀
  encodeEven (even-suc x) =
    ν₁ ι₁ (recIx (encodeOdd x))

  encodeOdd : Odd → CodeIx ExampleAtoms EvenOddDesc (EvenOddDesc (Fin.suc Fin.zero))
  encodeOdd (odd-suc x) =
    ν₁ ι₀ (recIx (encodeEven x))

mutual
  decodeEven : CodeIx ExampleAtoms EvenOddDesc (EvenOddDesc Fin.zero) → Even
  decodeEven (ν₀ ι₀) = even-zero
  decodeEven (ν₁ ι₁ (recIx x)) =
    even-suc (decodeOdd x)

  decodeOdd : CodeIx ExampleAtoms EvenOddDesc (EvenOddDesc (Fin.suc Fin.zero)) → Odd
  decodeOdd (ν₁ ι₀ (recIx x)) =
    odd-suc (decodeEven x)

mutual
  decode-encodeEven : (x : Even) → decodeEven (encodeEven x) ≡ x
  decode-encodeEven even-zero = refl
  decode-encodeEven (even-suc x) = cong even-suc (decode-encodeOdd x)

  decode-encodeOdd : (x : Odd) → decodeOdd (encodeOdd x) ≡ x
  decode-encodeOdd (odd-suc x) = cong odd-suc (decode-encodeEven x)

mutual
  encode-decodeEven : (x : CodeIx ExampleAtoms EvenOddDesc (EvenOddDesc Fin.zero)) → encodeEven (decodeEven x) ≡ x
  encode-decodeEven (ν₀ ι₀) = refl
  encode-decodeEven (ν₁ ι₁ (recIx x)) =
    cong (λ y → ν₁ ι₁ (recIx y))
      (encode-decodeOdd x)

  encode-decodeOdd : (x : CodeIx ExampleAtoms EvenOddDesc (EvenOddDesc (Fin.suc Fin.zero))) → encodeOdd (decodeOdd x) ≡ x
  encode-decodeOdd (ν₁ ι₀ (recIx x)) =
    cong (λ y → ν₁ ι₀ (recIx y))
      (encode-decodeEven x)

encodeEvenRoot : Even → RootCodeIx ExampleAtoms EvenOddDesc (rootData Fin.zero)
encodeEvenRoot x = rootDataIx (encodeEven x)

decodeEvenRoot : RootCodeIx ExampleAtoms EvenOddDesc (rootData Fin.zero) → Even
decodeEvenRoot (rootDataIx x) = decodeEven x

decode-encodeEvenRoot : (x : Even) → decodeEvenRoot (encodeEvenRoot x) ≡ x
decode-encodeEvenRoot = decode-encodeEven

encode-decodeEvenRoot : (x : RootCodeIx ExampleAtoms EvenOddDesc (rootData Fin.zero)) → encodeEvenRoot (decodeEvenRoot x) ≡ x
encode-decodeEvenRoot (rootDataIx x) =
  cong rootDataIx (encode-decodeEven x)

encodeOddRoot : Odd → RootCodeIx ExampleAtoms EvenOddDesc (rootData (Fin.suc Fin.zero))
encodeOddRoot x = rootDataIx (encodeOdd x)

decodeOddRoot : RootCodeIx ExampleAtoms EvenOddDesc (rootData (Fin.suc Fin.zero)) → Odd
decodeOddRoot (rootDataIx x) = decodeOdd x

decode-encodeOddRoot : (x : Odd) → decodeOddRoot (encodeOddRoot x) ≡ x
decode-encodeOddRoot = decode-encodeOdd

encode-decodeOddRoot : (x : RootCodeIx ExampleAtoms EvenOddDesc (rootData (Fin.suc Fin.zero))) → encodeOddRoot (decodeOddRoot x) ≡ x
encode-decodeOddRoot (rootDataIx x) =
  cong rootDataIx (encode-decodeOdd x)

genericEven : Generic ExampleAtoms Even
genericEven =
  generic 2 EvenOddDesc (rootData Fin.zero)
    (λ { Fin.zero → "Even" ; (Fin.suc Fin.zero) → "Odd" })
    (λ { Fin.zero → "even-zero" ∷ "even-suc" ∷ []
       ; (Fin.suc Fin.zero) → "odd-suc" ∷ [] })
    encodeEvenRoot decodeEvenRoot
    decode-encodeEvenRoot encode-decodeEvenRoot

genericOdd : Generic ExampleAtoms Odd
genericOdd =
  generic 2 EvenOddDesc (rootData (Fin.suc Fin.zero))
    (λ { Fin.zero → "Even" ; (Fin.suc Fin.zero) → "Odd" })
    (λ { Fin.zero → "even-zero" ∷ "even-suc" ∷ []
       ; (Fin.suc Fin.zero) → "odd-suc" ∷ [] })
    encodeOddRoot decodeOddRoot
    decode-encodeOddRoot encode-decodeOddRoot

certifiedGenericEven : CertifiedGeneric ExampleAtoms Even
certifiedGenericEven =
  certifiedGeneric genericEven λ
    { Fin.zero → _∷ⁿ_ (_∷ⁿ_ []ⁿ)
    ; (Fin.suc Fin.zero) → _∷ⁿ_ []ⁿ
    }

certifiedGenericOdd : CertifiedGeneric ExampleAtoms Odd
certifiedGenericOdd =
  certifiedGeneric genericOdd λ
    { Fin.zero → _∷ⁿ_ (_∷ⁿ_ []ⁿ)
    ; (Fin.suc Fin.zero) → _∷ⁿ_ []ⁿ
    }

data AutoEven : Type₀
data AutoOdd : Type₀

data AutoEven where
  auto-even-zero : AutoEven
  auto-even-suc  : AutoOdd → AutoEven

data AutoOdd where
  auto-odd-suc : AutoEven → AutoOdd

inferredAutoEven : InferredGeneric AutoEven
inferredAutoEven = deriveGeneric AutoEven

genericAutoEven : Generic (fst inferredAutoEven) AutoEven
genericAutoEven = snd inferredAutoEven

inferredAutoOdd : InferredGeneric AutoOdd
inferredAutoOdd = deriveGeneric AutoOdd

genericAutoOdd : Generic (fst inferredAutoOdd) AutoOdd
genericAutoOdd = snd inferredAutoOdd

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

genericMacroTree : Generic BuiltinAtoms MacroTree
genericMacroTree = deriveGenericFamilyIn1 BuiltinAtoms MacroTree

macroTreeFamily : GenericFamily BuiltinAtoms
macroTreeFamily = deriveGenericFamilyBundleIn1 BuiltinAtoms MacroTree

data MacroExpr : Type₀
data MacroBind : Type₀

data MacroExpr where
  macro-lit  : ℕ → MacroExpr
  macro-pair : MacroExpr → MacroExpr → MacroExpr
  macro-let  : MacroBind → MacroExpr → MacroExpr

data MacroBind where
  macro-bind  : String → MacroExpr → MacroBind
  macro-binds : MacroBind → MacroBind → MacroBind

genericMacroExpr : Generic BuiltinAtoms MacroExpr
genericMacroExpr = deriveGenericFamilyIn2 BuiltinAtoms MacroExpr MacroBind MacroExpr

genericMacroBind : Generic BuiltinAtoms MacroBind
genericMacroBind = deriveGenericFamilyIn2 BuiltinAtoms MacroExpr MacroBind MacroBind

certifiedMacroFamily : CertifiedFamily BuiltinAtoms
certifiedMacroFamily =
  deriveCertifiedGenericFamilyBundleIn2 BuiltinAtoms MacroExpr MacroBind

genericReachableMacroTree : Generic BuiltinAtoms MacroTree
genericReachableMacroTree = deriveGenericReachableIn BuiltinAtoms MacroTree

certifiedReachableMacroTree : CertifiedGeneric BuiltinAtoms MacroTree
certifiedReachableMacroTree =
  deriveCertifiedGenericReachableIn BuiltinAtoms MacroTree

genericReachableMacroExpr : Generic BuiltinAtoms MacroExpr
genericReachableMacroExpr = deriveGenericReachableIn BuiltinAtoms MacroExpr

genericReachableMacroBind : Generic BuiltinAtoms MacroBind
genericReachableMacroBind = deriveGenericReachableIn BuiltinAtoms MacroBind