module Soat.SecondOrder.Algebra.Lift

import Data.List.Sublist
import Data.Setoid.Indexed
import Data.Setoid.Pair
import Data.Setoid.Product

import Soat.FirstOrder.Algebra
import Soat.SecondOrder.Algebra
import Soat.SecondOrder.Signature.Lift

import Syntax.PreorderReasoning.Setoid

%default total

public export
project : RawAlgebra (lift sig) -> (ctx : List sig.T) -> RawAlgebra sig
project a ctx = MkRawAlgebra
  (\t => a.U t ctx)
  (\op => a.sem ctx (MkOp (Op op.op)) . wrap (MkPair []))

public export
projectAlgebra : (0 sig : _) -> Algebra (lift sig) -> (ctx : List sig.T) -> Algebra sig
projectAlgebra sig a ctx = MkAlgebra
  { U   = a.setoidAt ctx
  , sem = \op =>
    a.semFunc ctx (MkOp (Op op.op)) .
    index (wrapFunc (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid) (MkPair [])) _
  }

public export
projectHomo : {a, b : Algebra (lift sig)} -> a ~> b
  -> (ctx : _) -> projectAlgebra sig a ctx ~> projectAlgebra sig b ctx
projectHomo f ctx = MkHomomorphism
  { func    = reindex (flip MkPair ctx) f.func
  , semHomo = \op, tms => CalcWith (index b.setoid _) $
    |~ f.func.H (_, ctx) (a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) tms))
    ~~ b.raw.sem ctx (MkOp (Op op.op)) (map (\ty => f.func.H (snd ty, fst ty ++ ctx)) (wrap (MkPair []) tms))
      ...(f.semHomo ctx (MkOp (Op op.op)) (wrap (MkPair []) tms))
    ~~ b.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => f.func.H (t, ctx)) tms))
      .=.(cong (b.raw.sem ctx (MkOp (Op op.op))) $
          mapWrap (MkPair []) {f = \ty => f.func.H (snd ty, fst ty ++ ctx)} tms)
  }

public export
(.renameHomo) : (a : Algebra (lift sig)) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx')
  -> projectAlgebra sig a ctx ~> projectAlgebra sig a ctx'
(.renameHomo) a f = MkHomomorphism
  { func    = a.renameFunc f
  , semHomo = \op, tms => CalcWith (index a.setoid _) $
    |~ a.raw.rename _ f (a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) tms))
    ~~ a.raw.sem _ (MkOp (Op op.op)) (map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms))
      ...(a.algebra.semNat f (MkOp (Op op.op)) (wrap (MkPair []) tms))
    ~~ a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => a.raw.rename t f) tms))
      ...(a.algebra.semCong _ (MkOp (Op op.op)) $
          CalcWith (index (Product (reindex (\ty => (snd ty, fst ty ++ _)) a.setoid)) _) $
          |~ map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms)
          ~~ wrap (MkPair []) (map (\t => a.raw.rename t (reflexive {x = []} ++ f)) tms)
            .=.(mapWrap (MkPair []) tms)
          ~~ wrap (MkPair []) (map (\t => a.raw.rename t f) tms)
            ...(wrapIntro $
                mapIntro'' (\t, tm, tm', eq =>
                  CalcWith (index a.setoid (t, _)) $
                  |~ a.raw.rename t (reflexive {x = []} ++ f) tm
                  ~~ a.raw.rename t f tm
                    .=.(cong (\f => a.raw.rename t f tm) $ uncurryCurry f)
                  ~~ a.raw.rename t f tm'
                    ...(a.algebra.renameCong t f eq)) $
                (Product (a.setoidAt ctx)).equivalence.reflexive _ tms))
  }

public export
(.substHomo1) : (a : Algebra (lift sig)) -> (ctx : List sig.T)
  -> {ctx' : List sig.T} -> (tms : (\t => a.raw.U t ctx) ^ ctx')
  -> projectAlgebra sig a ctx' ~> projectAlgebra sig a ctx
(.substHomo1) a ctx tms = MkHomomorphism
  { func    = bundle (\t =>
    a.substFunc t ctx ctx' .
    tuple
      (id (index a.setoid (t, ctx')))
      (const {b = index (Product (a.setoidAt ctx)) ctx'} tms))
  , semHomo = \op, tms' => CalcWith (index a.setoid _) $
    |~ a.raw.subst _ ctx (a.raw.sem ctx' (MkOp (Op op.op)) (wrap (MkPair []) tms')) tms
    ~~ a.raw.sem ctx (MkOp (Op op.op)) (map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms'))
      ...(a.algebra.substCompat ctx (MkOp (Op op.op)) (wrap (MkPair []) tms') tms)
    ~~ a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm tms) tms'))
      ...(a.algebra.semCong ctx (MkOp (Op op.op)) $
          CalcWith (index (Product (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid)) _) $
          |~ map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms')
          ~~ wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm (map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms)) tms')
            .=.(mapWrap (MkPair []) tms')
          ~~ wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm tms) tms')
            ...(wrapIntro $
                mapIntro' (\t, eq =>
                  a.algebra.substCong t ctx eq $
                  CalcWith (index (Product (a.setoidAt _)) _) $
                  |~ map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms
                  ~~ map (\t => id) tms
                    ...(mapIntro'' (\t, tm, tm', eq =>
                          CalcWith (index a.setoid (t, ctx)) $
                          |~ a.raw.rename t ([] {ys = []} ++ reflexive) tm
                          ~~ a.raw.rename t reflexive tm
                            .=.(cong (\f => a.raw.rename t f tm) $ uncurryCurry reflexive)
                          ~~ tm
                            ...(a.algebra.renameId t ctx tm)
                          ~~ tm'
                            ...(eq)) $
                        (Product (a.setoidAt _)).equivalence.reflexive _ _)
                  ~~ tms
                    .=.(mapId tms)) $
                (Product (a.setoidAt _)).equivalence.reflexive _ _))
  }