module Soat.SecondOrder.Algebra.Lift

import Data.List.Elem

import Soat.Data.Product
import Soat.Data.Sublist
import Soat.FirstOrder.Algebra
import Soat.FirstOrder.Term
import Soat.Relation
import Soat.SecondOrder.Algebra
import Soat.SecondOrder.Signature.Lift

%default total

public export
project : SecondOrder.Algebra.RawAlgebra (lift sig) -> (ctx : List sig.T)
  -> FirstOrder.Algebra.RawAlgebra sig
project a ctx = MakeRawAlgebra
  (flip a.U ctx)
  (\op => a.sem ctx (MkOp (Op op.op)) . wrap (MkPair []))

public export
projectIsAlgebra : {a : _} -> forall rel . SecondOrder.Algebra.IsAlgebra (lift sig) a rel
  -> (ctx : List sig.T)
  -> FirstOrder.Algebra.IsAlgebra sig (project a ctx) (\t => rel (t, ctx))
projectIsAlgebra a ctx = MkIsAlgebra
  (\t => a.equivalence (t, ctx))
  (\op => a.semCong ctx _ . wrapIntro)

public export
projectAlgebra : SecondOrder.Algebra.Algebra (lift sig) -> (ctx : List sig.T)
  -> FirstOrder.Algebra.Algebra sig
projectAlgebra a ctx = MkAlgebra _ _ (projectIsAlgebra a.algebra ctx)

public export
projectIsHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> {f : _} -> IsHomomorphism a b f
  -> (ctx : _)
  -> IsHomomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra b ctx) (\t => f t ctx)
projectIsHomo {b = b} f ctx = MkIsHomomorphism
  (\t => f.cong t ctx)
  (\op, tms =>
    (b.algebra.equivalence _).transitive
      (f.semHomo ctx (MkOp (Op op.op)) (wrap (MkPair []) tms)) $
    b.algebra.semCong ctx (MkOp (Op op.op)) $
    map (\(_,_) => (b.algebra.equivalence _).equalImpliesEq) $
    equalImpliesPwEq $
    mapWrap (MkPair []) tms)

public export
projectHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> Homomorphism a b
  -> (ctx : _) -> Homomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra b ctx)
projectHomo f ctx = MkHomomorphism (\t => f.func t ctx) (projectIsHomo f.homo ctx)

public export
(.renameHomo) : (a : SecondOrder.Algebra.Algebra (lift sig)) -> {ctx, ctx' : _}
  -> (f : ctx `Sublist` ctx')
  -> FirstOrder.Algebra.Homomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra a ctx')
(.renameHomo) a f = MkHomomorphism
  (\t => a.raw.rename t f)
  (MkIsHomomorphism
    (\t => a.algebra.renameCong t f)
    (\op, tms => (a.algebra.equivalence _).transitive
      (a.algebra.semNat f (MkOp (Op op.op)) (wrap (MkPair []) tms))
      (a.algebra.semCong _ (MkOp (Op op.op)) $
       map (\(_,_) => (a.algebra.equivalence _).equalImpliesEq) $
       pwSym (\_ => MkSymmetric symmetric) $
       pwTrans (\_ => MkTransitive transitive)
         (wrapIntro $
          mapIntro'' (\t, tm, _, Refl =>
            cong (\f => a.raw.rename t f tm) $
            sym $
            uncurryCurry f) $
          equalImpliesPwEq Refl) $
       equalImpliesPwEq $
       sym $
       mapWrap (MkPair []) tms)))

public export
(.substHomo1) : (a : SecondOrder.Algebra.Algebra (lift sig)) -> (ctx : List sig.T)
  -> {ctx' : List sig.T} -> (tms : (\t => a.raw.U t ctx) ^ ctx')
  -> FirstOrder.Algebra.Homomorphism {sig = sig} (projectAlgebra a ctx') (projectAlgebra a ctx)
(.substHomo1) a ctx tms = MkHomomorphism
  (\t, tm => a.raw.subst t ctx tm tms)
  (MkIsHomomorphism
     (\t, eq => a.algebra.substCong t ctx eq $ pwRefl (\_ => (a.algebra.equivalence _).refl))
     (\op, tms' => (a.algebra.equivalence _).transitive
       (a.algebra.substCompat ctx (MkOp (Op op.op)) (wrap (MkPair []) tms') tms)
       (a.algebra.semCong ctx (MkOp (Op op.op)) $
        pwSym (\(_,_) => (a.algebra.equivalence _).sym) $
        pwTrans (\(_,_) => (a.algebra.equivalence _).trans)
          (pwSym (\(_,_) => (a.algebra.equivalence _).sym) $
           wrapIntro $
           mapIntro'' (\t, tm, _, Refl =>
             a.algebra.substCong t ctx (a.algebra.equivalence _).reflexive $
             pwTrans (\_ => (a.algebra.equivalence _).trans)
               (mapIntro'' (\t, tm, _, Refl => (a.algebra.equivalence _).transitive
                 ((a.algebra.equivalence _).equalImpliesEq $
                  cong (\f => a.raw.rename t f tm) $
                  uncurryCurry reflexive)
                 (a.algebra.renameId _ _ tm)) $
                equalImpliesPwEq Refl) $
             map (\_ => (a.algebra.equivalence _).equalImpliesEq) $
             equalImpliesPwEq $
             mapId tms) $
           equalImpliesPwEq Refl) $
        map (\(_,_) => (a.algebra.equivalence _).equalImpliesEq) $
        equalImpliesPwEq $
        sym $
        mapWrap (MkPair []) tms')))

renameBodyFunc : (f : ctx `Sublist` ctx')
  -> IFunction
       (isetoid (flip Elem ctx))
       (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx'))).setoid
renameBodyFunc f = MkIFunction (\_ => Done . curry f) (\_ => Done' . cong (curry f))

indexFunc : {ctx : List sig.T} -> (tms : Term sig (flip Elem ctx) ^ ts)
  -> IFunction
       (isetoid (flip Elem ts))
       (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx))).setoid
indexFunc tms = MkIFunction
  (\_ => index tms)
  (\_ => ((FreeIsAlgebra (isetoid (flip Elem _))).equivalence _).equalImpliesEq . cong (index tms))

-- renameFunc : (f : ctx `Sublist` ctx')
--   -> IFunction
--        (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx))).setoid
--        (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx'))).setoid
-- renameFunc f = MkIFunction
--   (\_ => bindTerm {a = Free _} (renameBodyFunc f).func)
--   (\t => bindTermCong {a = FreeAlgebra (isetoid (flip Elem _))} (renameBodyFunc f))

public export
Initial : (0 sig : _) -> SecondOrder.Algebra.RawAlgebra (lift sig)
Initial sig = MakeRawAlgebra
  (\t, ctx => Term sig (flip Elem ctx) t)
  (\t, f => bindTerm {a = Free _} (renameBodyFunc f).func)
  (\_, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair []))
  Done
  (\_, _, t, ts => bindTerm {a = Free _} (\_ => index ts) t)

public export
InitialIsAlgebra : (0 sig : _)
  -> SecondOrder.Algebra.IsAlgebra
       (lift sig)
       (Initial sig)
       (\(t, ctx) => (~=~) {sig = sig} {v = flip Elem ctx} (\_ => Equal) t)
InitialIsAlgebra sig = MkIsAlgebra
  (\(t, ctx) => tmRelEq (\_ => equiv) t)
  (\t, f => bindTermCong {a = FreeAlgebra (isetoid (flip Elem _))} (renameBodyFunc f))
  (\_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro)
  (\_, _, eq, eqs => bindTermCong'
    {a = FreeAlgebra (isetoid (flip Elem _))}
    (\t, Refl => index eqs _)
    eq)
  (\t, ctx, tm =>
    tmRelSym (\_ => MkSymmetric symmetric) $
    bindUnique (renameBodyFunc reflexive) idHomo (\i => Done' $ sym $ curryUncurry id i) $
    tm)
  (\t, f, g, tm =>
    tmRelSym (\_ => MkSymmetric symmetric) $
    bindUnique
      {a = FreeAlgebra (isetoid (flip Elem _))}
      (renameBodyFunc (transitive g f))
      (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (renameBodyFunc g)))
      (\i => Done' $ sym $ curryUncurry (curry f . curry g) i) $
    tm)
  (\f, (MkOp (Op op)), tms =>
    Call' (MkOp op) $
    Pointwise.map (\_ => tmRelReflexive (\_ => MkReflexive reflexive)) $
    pwTrans (\_ => MkTransitive transitive) (equalImpliesPwEq $ bindTermsIsMap {a = Free _} _ _) $
    pwTrans (\_ => MkTransitive transitive)
      (mapIntro' (\t, eq =>
        tmRelEqualIsEqual $
        bindTermCong'
          {rel = \_ => Equal}
          {a = FreeAlgebra (isetoid (flip Elem _))}
          (\_, Refl => Done' $ sym $ curryUncurry (curry f) _) $
        tmRelReflexive (\_ => MkReflexive reflexive) $
        eq) $
       equalImpliesPwEq Refl) $
    equalImpliesPwEq $
    mapUnwrap _ _)
    -- Pointwise.map (\_ => tmRelReflexive (\_ => MkReflexive reflexive)) $
    -- transitive (equalImpliesPwEq $ bindTermsIsMap {a = Free _} _ (unwrap (MkPair []) tms)) $
    -- transitive
    --   (mapIntro
    --      (\t, eq =>
    --        bindTermCong'
    --          {v = isetoid (flip Elem _)}
    --          {a = FreeAlgebra (isetoid (flip Elem _))}
    --          (\_, Refl => Done' $ sym $ curryUncurry (curry f) _) $
    --        tmRelReflexive (\_ => MkReflexive reflexive) $
    --        eq) $
    --    equalImpliesPwEq Refl) $
    -- equalImpliesPwEq $
    -- mapUnwrap
    --   (MkPair [])
    --   (\ty => (renameFunc (reflexive ++ f)).func (snd ty))
    --   tms)
  (\_, _ => Done' Refl)
  (\t, f, tm, tms =>
    bindUnique
      {a = FreeAlgebra (isetoid (flip Elem _))}
      (indexFunc _)
      (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (indexFunc tms)))
      (\i =>
        tmRelReflexive (\_ => MkReflexive reflexive) $
        sym $
        indexMap tms i)
      tm)
  (\t, ctx, f, tm, tms =>
    bindUnique
      {a = FreeAlgebra (isetoid (flip Elem _))}
      (indexFunc _)
      (compHomo (bindHomo (indexFunc tms)) (bindHomo (renameBodyFunc f)))
      (\i =>
        tmRelReflexive (\_ => MkReflexive reflexive) $
        sym $
        indexShuffle f i)
      tm)
  (\t, ctx, tm, tms, tms' =>
    bindUnique
      {a = FreeAlgebra (isetoid (flip Elem _))}
      (indexFunc _)
      (compHomo (bindHomo (indexFunc tms')) (bindHomo (indexFunc tms)))
      (\i =>
        tmRelReflexive (\_ => MkReflexive reflexive) $
        sym $
        indexMap tms i)
      tm)
  (\_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _)
  (\t, ctx, tm =>
    tmRelSym (\_ => MkSymmetric symmetric) $
    bindUnique
      {a = FreeAlgebra (isetoid (flip Elem _))}
      (indexFunc _)
      idHomo
      (\i =>
        tmRelReflexive (\_ => MkReflexive reflexive) $
        sym $
        indexTabulate Done i)
      tm)
  (\ctx, (MkOp (Op op)), tms, tms' =>
    Call' (MkOp op) $
    tmsRelTrans (\_ => MkTransitive transitive)
      (tmsRelSym (\_ => MkSymmetric symmetric) $
       bindsUnique
         {a = FreeAlgebra (isetoid (flip Elem _))}
         (indexFunc tms')
         (bindHomo (indexFunc _))
         (\i =>
           (tmRelTrans (\_ => MkTransitive transitive)
              (tmRelReflexive (\_ => MkReflexive reflexive) $
               indexMap
                 {f = (\_ => bindTerm {a = Free _} (\_ => Done . curry (uncurry (curry reflexive))))}
                 tms'
                 i) $
            tmRelSym (\_ => MkSymmetric symmetric) $
            (bindUnique
               {a = FreeAlgebra (isetoid (flip Elem _))}
               (renameBodyFunc _)
               idHomo
               (\i =>
                 Done' $
                 sym $
                 transitive (curryUncurry (curry reflexive) i) (curryUncurry id i))
               (index tms' i))))
         (unwrap (MkPair []) tms)) $
    tmsRelReflexive (\_ => MkReflexive reflexive) $
    mapUnwrap _ _)

public export
InitialAlgebra : (0 sig : _) -> SecondOrder.Algebra.Algebra (lift sig)
InitialAlgebra sig = MkAlgebra (Initial sig) _ (InitialIsAlgebra sig)

public export
freeToInitialIsHomo : (0 sig : _) -> (ctx : List sig.T)
  -> IsHomomorphism {sig = sig}
       (FreeAlgebra (isetoid (flip Elem ctx)))
       (projectAlgebra (InitialAlgebra sig) ctx)
       (\_ => Basics.id)
freeToInitialIsHomo sig ctx = MkIsHomomorphism
  (\_ => id)
  (\(MkOp op), tms =>
    Call' (MkOp op) $
    tmsRelSym (\_ => MkSymmetric symmetric) $
    tmsRelReflexive (\_ => MkReflexive reflexive) $
    transitive (unwrapWrap _ _) (mapId tms))

public export
freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T)
  -> Homomorphism {sig = sig}
       (FreeAlgebra (isetoid (flip Elem ctx)))
       (projectAlgebra (InitialAlgebra sig) ctx)
freeToInitialHomo sig ctx = MkHomomorphism (\_ => id) (freeToInitialIsHomo sig ctx)

public export
fromInitial : (a : SecondOrder.Algebra.RawAlgebra (lift sig)) -> (t : sig.T) -> (ctx : List sig.T)
  -> (Initial sig).U t ctx -> a.U t ctx
fromInitial a t ctx = bindTerm {a = project a ctx} (\_ => a.var)

public export
fromInitialIsHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
  -> IsHomomorphism (InitialAlgebra sig) a (fromInitial a.raw)
fromInitialIsHomo a = MkIsHomomorphism
  (\t , ctx => bindTermCong {a = projectAlgebra a ctx} (a.varFunc ctx))
  (\t, f => bindUnique'
    {v = isetoid (flip Elem _)}
    {a = projectAlgebra a _}
    (compHomo (bindHomo (a.varFunc _)) (bindHomo (renameBodyFunc f)))
    (compHomo (a.renameHomo f) (bindHomo (a.varFunc _)))
    (\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i))
  (\ctx, (MkOp (Op op)), tms =>
    a.algebra.semCong ctx (MkOp (Op op)) $
    map (\_ => (a.algebra.equivalence _).equalImpliesEq) $
    equalImpliesPwEq $
    transitive
      (cong (wrap _) $ bindTermsIsMap {a = project a.raw _} (\_ => a.raw.var) $ unwrap _ tms) $
    transitive
      (sym $ mapWrap (MkPair []) {f = \_ => fromInitial a.raw _ _} $ unwrap _ tms) $
    cong (map _) $
    wrapUnwrap tms)
  (\_ => (a.algebra.equivalence _).reflexive)
  (\t, ctx, tm, tms => bindUnique'
    {v = isetoid (flip Elem _)}
    {a = projectAlgebra a _}
    (compHomo (bindHomo (a.varFunc _)) (bindHomo (indexFunc tms)))
    (compHomo (a.substHomo1 ctx _) (bindHomo (a.varFunc _)))
    (\i =>
      (a.algebra.equivalence _).transitive
        (bindUnique
          {v = isetoid (flip Elem _)}
          {a = projectAlgebra a _}
          (a.varFunc _)
          (bindHomo (a.varFunc _))
          (\i => (a.algebra.equivalence _).reflexive)
          (index tms i)) $
      (a.algebra.equivalence _).symmetric $
      (a.algebra.equivalence _).transitive
        (a.algebra.substVarL ctx i _) $
      (a.algebra.equivalence _).equalImpliesEq $
      indexMap {f = \t => bindTerm {a = project a.raw ctx} (\_ => a.raw.var)} tms i)
    tm)

public export
fromInitialHomo : (a : SecondOrder.Algebra.Algebra (lift sig))
  -> Homomorphism (InitialAlgebra sig) a
fromInitialHomo a = MkHomomorphism (fromInitial a.raw) (fromInitialIsHomo a)

public export
fromInitialUnique : {a : SecondOrder.Algebra.Algebra (lift sig)}
  -> (f : Homomorphism (InitialAlgebra sig) a)
  -> (t : sig.T) -> (ctx : List sig.T) -> (tm : Term sig (flip Elem ctx) t)
  -> a.relation (t, ctx) (f.func t ctx tm) (fromInitial a.raw t ctx tm)
fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique
  {v = isetoid (flip Elem _)}
  {a = projectAlgebra a ctx}
  (a.varFunc ctx)
  (compHomo (projectHomo f ctx) (freeToInitialHomo sig ctx))
  f.homo.varHomo