module Generic.Default where

open import Generic.Core

open import Cubical.Data.Maybe.Base using (Maybe; just; nothing)

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

AtomDefaults : ∀ {ℓ} → AtomUniverse ℓ → Type ℓ
AtomDefaults U = (a : AtomCode U) → Atom U a

defaultMaybeMap : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} →
                  (A → B) → Maybe A → Maybe B
defaultMaybeMap f nothing = nothing
defaultMaybeMap f (just x) = just (f x)

Defaults : ∀ {ℓ n} (U : AtomUniverse ℓ) →
           (D : Fin n → TyDesc U n) → Type ℓ
Defaults {n = n} U D = (i : Fin n) → Maybe (CodeIx U D (D i))

prependConstructorDefault : ∀ {ℓ n} {U : AtomUniverse ℓ}
                            {D : Fin n → TyDesc U n}
                            {c : ConDesc U n} {cs : List (ConDesc U n)} →
                            Maybe (ArgsCodeIx U D c) →
                            Maybe (CodeIx U D (dataD cs)) →
                            Maybe (CodeIx U D (dataD (c ∷ cs)))
prependConstructorDefault (just args) rest = just (nodeIx here args)
prependConstructorDefault nothing nothing = nothing
prependConstructorDefault nothing (just (nodeIx i args)) =
  just (nodeIx (there i) args)

prependFieldDefault : ∀ {ℓ n} {U : AtomUniverse ℓ}
                      {D : Fin n → TyDesc U n}
                      {f : FieldDesc U n} {fs : List (FieldDesc U n)} →
                      Maybe (FieldCodeIx U D f) →
                      Maybe (ArgsCodeIx U D (con fs)) →
                      Maybe (ArgsCodeIx U D (con (f ∷ fs)))
prependFieldDefault nothing rest = nothing
prependFieldDefault (just x) nothing = nothing
prependFieldDefault (just x) (just xs) = just (x ∷ⁱ xs)

emptyDefaults : ∀ {ℓ n} {U : AtomUniverse ℓ}
                {D : Fin n → TyDesc U n} → Defaults U D
emptyDefaults i = nothing

mutual
  defaultCodeWith : ∀ {ℓ n} {U : AtomUniverse ℓ}
                    (atomDefaults : AtomDefaults U) →
                    (D : Fin n → TyDesc U n) →
                    Defaults U D →
                    (d : TyDesc U n) →
                    Maybe (CodeIx U D d)
  defaultCodeWith atomDefaults D previous (dataD cs) =
    defaultConstructorWith atomDefaults D previous cs

  defaultConstructorWith : ∀ {ℓ n} {U : AtomUniverse ℓ}
                           (atomDefaults : AtomDefaults U) →
                           (D : Fin n → TyDesc U n) →
                           Defaults U D →
                           (cs : List (ConDesc U n)) →
                           Maybe (CodeIx U D (dataD cs))
  defaultConstructorWith atomDefaults D previous [] = nothing
  defaultConstructorWith atomDefaults D previous (c ∷ cs) =
    prependConstructorDefault
      (defaultArgsWith atomDefaults D previous c)
      (defaultConstructorWith atomDefaults D previous cs)

  defaultFieldWith : ∀ {ℓ n} {U : AtomUniverse ℓ}
                     (atomDefaults : AtomDefaults U) →
                     (D : Fin n → TyDesc U n) →
                     Defaults U D →
                     (f : FieldDesc U n) →
                     Maybe (FieldCodeIx U D f)
  defaultFieldWith atomDefaults D previous (fieldRec i) =
    defaultMaybeMap recIx (previous i)
  defaultFieldWith atomDefaults D previous (fieldAtom a) =
    just (atomIx (atomDefaults a))

  defaultArgsWith : ∀ {ℓ n} {U : AtomUniverse ℓ}
                    (atomDefaults : AtomDefaults U) →
                    (D : Fin n → TyDesc U n) →
                    Defaults U D →
                    (c : ConDesc U n) →
                    Maybe (ArgsCodeIx U D c)
  defaultArgsWith atomDefaults D previous (con []) = just []ⁱ
  defaultArgsWith atomDefaults D previous (con (f ∷ fs)) =
    prependFieldDefault
      (defaultFieldWith atomDefaults D previous f)
      (defaultArgsWith atomDefaults D previous (con fs))

stepDefaults : ∀ {ℓ n} {U : AtomUniverse ℓ}
               (atomDefaults : AtomDefaults U) →
               (D : Fin n → TyDesc U n) →
               Defaults U D → Defaults U D
stepDefaults atomDefaults D previous i =
  defaultCodeWith atomDefaults D previous (D i)

iterateDefaults : ∀ {ℓ n} {U : AtomUniverse ℓ}
                  (atomDefaults : AtomDefaults U) →
                  (D : Fin n → TyDesc U n) →
                  ℕ → Defaults U D → Defaults U D
iterateDefaults atomDefaults D zero previous = previous
iterateDefaults atomDefaults D (suc fuel) previous =
  stepDefaults atomDefaults D
    (iterateDefaults atomDefaults D fuel previous)

defaultCodes : ∀ {ℓ n} {U : AtomUniverse ℓ} →
               AtomDefaults U →
               (D : Fin n → TyDesc U n) →
               Defaults U D
defaultCodes {n = n} atomDefaults D =
  iterateDefaults atomDefaults D n emptyDefaults

defaultRootCode : ∀ {ℓ n} {U : AtomUniverse ℓ} →
                  (atomDefaults : AtomDefaults U) →
                  (D : Fin n → TyDesc U n) →
                  (r : RootDesc U n) →
                  Maybe (RootCodeIx U D r)
defaultRootCode atomDefaults D (rootData i) with defaultCodes atomDefaults D i
... | just x = just (rootDataIx x)
... | nothing = nothing
defaultRootCode atomDefaults D (rootAtom a) =
  just (rootAtomIx (atomDefaults a))

-- `DefaultableWith previous d` is the precise local productivity condition
-- for one search pass: some constructor of `d` has defaults for all fields,
-- using `previous` for recursive references.
mutual
  data DefaultableWith {ℓ n} {U : AtomUniverse ℓ}
                       {D : Fin n → TyDesc U n}
                       (previous : Defaults U D) :
                       TyDesc U n → Type ℓ where
    defaultableData : ∀ {cs} →
                      DefaultableConstructorsWith previous cs →
                      DefaultableWith previous (dataD cs)

  data DefaultableConstructorsWith {ℓ n} {U : AtomUniverse ℓ}
                                   {D : Fin n → TyDesc U n}
                                   (previous : Defaults U D) :
                                   List (ConDesc U n) → Type ℓ where
    defaultableHere : ∀ {c cs} →
                      DefaultableArgsWith previous c →
                      DefaultableConstructorsWith previous (c ∷ cs)
    defaultableThere : ∀ {c cs} →
                       DefaultableConstructorsWith previous cs →
                       DefaultableConstructorsWith previous (c ∷ cs)

  data DefaultableFieldWith {ℓ n} {U : AtomUniverse ℓ}
                            {D : Fin n → TyDesc U n}
                            (previous : Defaults U D) :
                            FieldDesc U n → Type ℓ where
    defaultableRec : ∀ {i} (x : CodeIx U D (D i)) →
                     previous i ≡ just x →
                     DefaultableFieldWith previous (fieldRec i)
    defaultableAtom : ∀ {a} →
                      DefaultableFieldWith previous (fieldAtom a)

  data DefaultableArgsWith {ℓ n} {U : AtomUniverse ℓ}
                           {D : Fin n → TyDesc U n}
                           (previous : Defaults U D) :
                           ConDesc U n → Type ℓ where
    defaultable[] : DefaultableArgsWith previous (con [])
    defaultable∷ : ∀ {f fs} →
                   DefaultableFieldWith previous f →
                   DefaultableArgsWith previous (con fs) →
                   DefaultableArgsWith previous (con (f ∷ fs))

mutual
  defaultCodeWith-complete : ∀ {ℓ n} {U : AtomUniverse ℓ}
                             {D : Fin n → TyDesc U n}
                             (atomDefaults : AtomDefaults U) →
                             (previous : Defaults U D) →
                             {d : TyDesc U n} →
                             DefaultableWith previous d →
                             Σ[ x ∈ CodeIx U D d ]
                               defaultCodeWith atomDefaults D previous d ≡ just x
  defaultCodeWith-complete atomDefaults previous (defaultableData witness) =
    defaultConstructorsWith-complete atomDefaults previous witness

  defaultConstructorsWith-complete : ∀ {ℓ n} {U : AtomUniverse ℓ}
                                     {D : Fin n → TyDesc U n}
                                     (atomDefaults : AtomDefaults U) →
                                     (previous : Defaults U D) →
                                     {cs : List (ConDesc U n)} →
                                     DefaultableConstructorsWith previous cs →
                                     Σ[ x ∈ CodeIx U D (dataD cs) ]
                                       defaultConstructorWith atomDefaults D previous cs ≡ just x
  defaultConstructorsWith-complete atomDefaults previous
    (defaultableHere {c = c} {cs = cs} args) with
      defaultArgsWith-complete atomDefaults previous args
  ... | xs , argsEq =
    nodeIx here xs ,
    cong
      (λ result → prependConstructorDefault result
        (defaultConstructorWith atomDefaults _ previous cs))
      argsEq
  defaultConstructorsWith-complete {D = D} atomDefaults previous
    (defaultableThere {c = c} {cs = cs} witness) with
      inspectDefault (defaultArgsWith atomDefaults D previous c)
  ... | just xs , headEq =
    nodeIx here xs ,
    cong
      (λ result → prependConstructorDefault result
        (defaultConstructorWith atomDefaults D previous cs))
      headEq
  ... | nothing , headEq with
      defaultConstructorsWith-complete atomDefaults previous witness
  ...   | nodeIx i xs , restEq =
    nodeIx (there i) xs ,
    cong
      (λ result → prependConstructorDefault result
        (defaultConstructorWith atomDefaults D previous cs))
      headEq
    ∙ cong (prependConstructorDefault nothing) restEq

  defaultFieldWith-complete : ∀ {ℓ n} {U : AtomUniverse ℓ}
                              {D : Fin n → TyDesc U n}
                              (atomDefaults : AtomDefaults U) →
                              (previous : Defaults U D) →
                              {f : FieldDesc U n} →
                              DefaultableFieldWith previous f →
                              Σ[ x ∈ FieldCodeIx U D f ]
                                defaultFieldWith atomDefaults D previous f ≡ just x
  defaultFieldWith-complete {D = D} atomDefaults previous
    (defaultableRec {i = i} x eq) =
    recIx x , cong (defaultMaybeMap recIx) eq
  defaultFieldWith-complete atomDefaults previous defaultableAtom =
    atomIx (atomDefaults _) , refl

  defaultArgsWith-complete : ∀ {ℓ n} {U : AtomUniverse ℓ}
                             {D : Fin n → TyDesc U n}
                             (atomDefaults : AtomDefaults U) →
                             (previous : Defaults U D) →
                             {c : ConDesc U n} →
                             DefaultableArgsWith previous c →
                             Σ[ xs ∈ ArgsCodeIx U D c ]
                               defaultArgsWith atomDefaults D previous c ≡ just xs
  defaultArgsWith-complete atomDefaults previous defaultable[] = []ⁱ , refl
  defaultArgsWith-complete {D = D} atomDefaults previous
    (defaultable∷ {f = f} {fs = fs} fieldWitness fieldsWitness) with
      defaultFieldWith-complete atomDefaults previous fieldWitness
    | defaultArgsWith-complete atomDefaults previous fieldsWitness
  ... | x , fieldEq | xs , fieldsEq =
    x ∷ⁱ xs ,
    cong
      (λ result → prependFieldDefault result
        (defaultArgsWith atomDefaults D previous (con fs)))
      fieldEq
    ∙ cong (prependFieldDefault (just x)) fieldsEq

previousDefaults : ∀ {ℓ n} {U : AtomUniverse ℓ} →
                   AtomDefaults U →
                   (D : Fin n → TyDesc U n) →
                   Defaults U D
previousDefaults {n = zero} atomDefaults D = emptyDefaults
previousDefaults {n = suc n} atomDefaults D =
  iterateDefaults atomDefaults D n emptyDefaults

ProductiveAtBound : ∀ {ℓ n} {U : AtomUniverse ℓ} →
                    (atomDefaults : AtomDefaults U) →
                    (D : Fin n → TyDesc U n) →
                    Fin n → Type ℓ
ProductiveAtBound atomDefaults D i =
  DefaultableWith (previousDefaults atomDefaults D) (D i)

defaultCodes-complete : ∀ {ℓ n} {U : AtomUniverse ℓ} →
                        (atomDefaults : AtomDefaults U) →
                        (D : Fin n → TyDesc U n) →
                        (i : Fin n) →
                        ProductiveAtBound atomDefaults D i →
                        Σ[ x ∈ CodeIx U D (D i) ]
                          defaultCodes atomDefaults D i ≡ just x
defaultCodes-complete {n = zero} atomDefaults D ()
defaultCodes-complete {n = suc n} atomDefaults D i witness =
  defaultCodeWith-complete atomDefaults
    (iterateDefaults atomDefaults D n emptyDefaults)
    witness