Generic.Tests

module Generic.Tests where

open import Generic.Core
open import Generic.Certified
open import Generic.Examples
open import Generic.ReflectionTerm
import Generic.ReflectionTermNativeJson as TermNativeJson
import Generic.NativeJson as NativeJson

import Agda.Builtin.Reflection as R

open Generic

atomic-roundtrip : (n : ℕ) → Generic.decode (atomicGeneric BuiltinAtoms natAtom) (Generic.encode (atomicGeneric BuiltinAtoms natAtom) n) ≡ n
atomic-roundtrip n = refl

color-red-roundtrip : Generic.decode genericColor (Generic.encode genericColor red) ≡ red
color-red-roundtrip = refl

color-code-roundtrip :
  Generic.encode genericColor (Generic.decode genericColor (rootDataIx (ν₀ ι₁)))
    ≡ rootDataIx (ν₀ ι₁)
color-code-roundtrip = refl

certified-color-constructor-name :
  CertifiedGeneric.constructorName certifiedGenericColor Fin.zero ι₁ ≡ "green"
certified-color-constructor-name = refl

macro-derived-enum-roundtrip :
  Generic.decode genericDirection (Generic.encode genericDirection south) ≡ south
macro-derived-enum-roundtrip = refl

macro-derived-builtin-nat :
  (n : ℕ) →
  Generic.decode genericAutoBuiltinLiterals
    (Generic.encode genericAutoBuiltinLiterals (auto-lit-nat n))
    ≡ auto-lit-nat n
macro-derived-builtin-nat n = refl

macro-derived-builtin-mix :
  Generic.decode genericAutoBuiltinLiterals
    (Generic.encode genericAutoBuiltinLiterals (auto-lit-mix "label" true tt))
    ≡ auto-lit-mix "label" true tt
macro-derived-builtin-mix = refl

macro-derived-field-roundtrip :
  (n : ℕ) →
  Generic.decode genericAutoMaybeNat (Generic.encode genericAutoMaybeNat (auto-some n))
    ≡ auto-some n
macro-derived-field-roundtrip n = refl

macro-derived-multi-field-roundtrip :
  (n : ℕ) →
  Generic.decode genericAutoRecordLike (Generic.encode genericAutoRecordLike (auto-record-like n tt))
    ≡ auto-record-like n tt
macro-derived-multi-field-roundtrip n = refl

macro-derived-builtin-record :
  (n : ℕ) →
  Generic.decode genericAutoBuiltinRecord
    (Generic.encode genericAutoBuiltinRecord (auto-builtin-record n false tt))
    ≡ auto-builtin-record n false tt
macro-derived-builtin-record n = refl

macro-derived-inferred-record :
  Generic.decode genericAutoInferredRecord
    (Generic.encode genericAutoInferredRecord (auto-inferred-record red east))
    ≡ auto-inferred-record red east
macro-derived-inferred-record = refl

macro-derived-mixed-nullary :
  Generic.decode genericAutoShape (Generic.encode genericAutoShape auto-point) ≡ auto-point
macro-derived-mixed-nullary = refl

macro-derived-mixed-unary :
  (n : ℕ) →
  Generic.decode genericAutoShape (Generic.encode genericAutoShape (auto-circle n))
    ≡ auto-circle n
macro-derived-mixed-unary n = refl

macro-derived-mixed-binary :
  (w h : ℕ) →
  Generic.decode genericAutoShape (Generic.encode genericAutoShape (auto-rect w h))
    ≡ auto-rect w h
macro-derived-mixed-binary w h = refl

macro-derived-mixed-custom-fields :
  Generic.decode genericAutoShape (Generic.encode genericAutoShape (auto-label green west))
    ≡ auto-label green west
macro-derived-mixed-custom-fields = refl

macro-derived-mixed-description :
  Generic.desc genericAutoShape Fin.zero
    ≡ dataD
        ( κ₀
        ∷ κ₁ (α natA)
        ∷ κ₂ (α natA) (α natA)
        ∷ κ₂ (α colorA) (α directionA)
        ∷ []
        )
macro-derived-mixed-description = refl

macro-derived-mixed-encoding :
  (w h : ℕ) →
  Generic.encode genericAutoShape (auto-rect w h)
    ≡ rootDataIx (ν₂ ι₂ (atomIx w) (atomIx h))
macro-derived-mixed-encoding w h = refl

macro-derived-nested-atomic-fields :
  (n : ℕ) →
  Generic.decode genericAutoNestedAtoms
    (Generic.encode genericAutoNestedAtoms (auto-nested (some n) (cons n nil)))
    ≡ auto-nested (some n) (cons n nil)
macro-derived-nested-atomic-fields n = refl

macro-derived-repeated-fields :
  (a b c : ℕ) →
  Generic.decode genericAutoRepeatedFields
    (Generic.encode genericAutoRepeatedFields (auto-repeated a b c))
    ≡ auto-repeated a b c
macro-derived-repeated-fields a b c = refl

macro-derived-large-constructor :
  (n : ℕ) →
  Generic.decode genericAutoLargeConstructor
    (Generic.encode genericAutoLargeConstructor (auto-large tt n blue north none))
    ≡ auto-large tt n blue north none
macro-derived-large-constructor n = refl

maybeNat-field-roundtrip : (n : ℕ) → Generic.decode genericMaybeNat (Generic.encode genericMaybeNat (some n)) ≡ some n
maybeNat-field-roundtrip n = refl

listNat-recursive-roundtrip :
  (n m : ℕ) →
  Generic.decode genericListNat (Generic.encode genericListNat (cons n (cons m nil)))
    ≡ cons n (cons m nil)
listNat-recursive-roundtrip n m = refl

mutual-even-roundtrip :
  Generic.decode genericEven (Generic.encode genericEven (even-suc (odd-suc even-zero)))
    ≡ even-suc (odd-suc even-zero)
mutual-even-roundtrip = refl

mutual-odd-roundtrip :
  Generic.decode genericOdd (Generic.encode genericOdd (odd-suc (even-suc (odd-suc even-zero))))
    ≡ odd-suc (even-suc (odd-suc even-zero))
mutual-odd-roundtrip = refl

macro-mutual-even-as-atomic-field :
  Generic.decode genericAutoEven
    (Generic.encode genericAutoEven (auto-even-suc (auto-odd-suc auto-even-zero)))
    ≡ auto-even-suc (auto-odd-suc auto-even-zero)
macro-mutual-even-as-atomic-field = refl

macro-mutual-odd-as-atomic-field :
  Generic.decode genericAutoOdd
    (Generic.encode genericAutoOdd (auto-odd-suc (auto-even-suc (auto-odd-suc auto-even-zero))))
    ≡ auto-odd-suc (auto-even-suc (auto-odd-suc auto-even-zero))
macro-mutual-odd-as-atomic-field = refl

macro-family-tree-roundtrip :
  Generic.decode genericMacroTree
    (Generic.encode genericMacroTree
      (macro-node "root" (macro-leaf "left") (macro-node "right" (macro-leaf "a") (macro-leaf "b"))))
    ≡ macro-node "root" (macro-leaf "left") (macro-node "right" (macro-leaf "a") (macro-leaf "b"))
macro-family-tree-roundtrip = refl

macro-family-tree-encoding :
  Generic.encode genericMacroTree
    (macro-node "root" (macro-leaf "left") (macro-leaf "right"))
    ≡ rootDataIx
        (ν₃ ι₁
          (atomIx "root")
          (recIx (ν₁ ι₀ (atomIx "left")))
          (recIx (ν₁ ι₀ (atomIx "right"))))
macro-family-tree-encoding = refl

macro-family-expr-roundtrip :
  Generic.decode genericMacroExpr
    (Generic.encode genericMacroExpr
      (macro-let
        (macro-binds
          (macro-bind "x" (macro-lit 1))
          (macro-bind "y" (macro-pair (macro-lit 2) (macro-lit 3))))
        (macro-pair (macro-lit 4) (macro-lit 5))))
    ≡ macro-let
        (macro-binds
          (macro-bind "x" (macro-lit 1))
          (macro-bind "y" (macro-pair (macro-lit 2) (macro-lit 3))))
        (macro-pair (macro-lit 4) (macro-lit 5))
macro-family-expr-roundtrip = refl

macro-family-bind-roundtrip :
  Generic.decode genericMacroBind
    (Generic.encode genericMacroBind
      (macro-binds
        (macro-bind "first" (macro-lit 0))
        (macro-bind "second" (macro-let (macro-bind "inner" (macro-lit 1)) (macro-lit 2)))))
    ≡ macro-binds
        (macro-bind "first" (macro-lit 0))
        (macro-bind "second" (macro-let (macro-bind "inner" (macro-lit 1)) (macro-lit 2)))
macro-family-bind-roundtrip = refl

macro-reachable-tree-roundtrip :
  Generic.decode genericReachableMacroTree
    (Generic.encode genericReachableMacroTree
      (macro-node "root" (macro-leaf "left") (macro-leaf "right")))
    ≡ macro-node "root" (macro-leaf "left") (macro-leaf "right")
macro-reachable-tree-roundtrip = refl

macro-reachable-expr-roundtrip :
  Generic.decode genericReachableMacroExpr
    (Generic.encode genericReachableMacroExpr
      (macro-let
        (macro-bind "x" (macro-pair (macro-lit 1) (macro-lit 2)))
        (macro-lit 3)))
    ≡ macro-let
        (macro-bind "x" (macro-pair (macro-lit 1) (macro-lit 2)))
        (macro-lit 3)
macro-reachable-expr-roundtrip = refl

macro-reachable-bind-roundtrip :
  Generic.decode genericReachableMacroBind
    (Generic.encode genericReachableMacroBind
      (macro-binds
        (macro-bind "left" (macro-lit 4))
        (macro-bind "right" (macro-pair (macro-lit 5) (macro-lit 6)))))
    ≡ macro-binds
        (macro-bind "left" (macro-lit 4))
        (macro-bind "right" (macro-pair (macro-lit 5) (macro-lit 6)))
macro-reachable-bind-roundtrip = refl

empty-atomic-code :
  RootCodeIx
    BuiltinAtoms
    (Generic.desc (atomicGeneric BuiltinAtoms unitAtom))
    (Generic.root (atomicGeneric BuiltinAtoms unitAtom))
empty-atomic-code = Generic.encode (atomicGeneric BuiltinAtoms unitAtom) tt

reflection-term-var-roundtrip :
  Generic.decode genericTerm (Generic.encode genericTerm (R.var 0 [])) ≡ R.var 0 []
reflection-term-var-roundtrip = refl

reflection-term-unknown-roundtrip :
  Generic.decode genericTerm (Generic.encode genericTerm R.unknown) ≡ R.unknown
reflection-term-unknown-roundtrip = refl

certified-reflection-term-constructor-name :
  CertifiedGeneric.constructorName certifiedGenericTerm termI ι₀ ≡ "var"
certified-reflection-term-constructor-name = refl

reflection-term-native-json-smoke : NativeJson.JsonValue
reflection-term-native-json-smoke =
  TermNativeJson.termToNativeJSON (R.var 0 [])