module Soat.FirstOrder.Algebra

import Data.Product
import Data.Setoid.Indexed
import Data.Setoid.Product

import Soat.FirstOrder.Signature

import Syntax.PreorderReasoning.Setoid

%default total

infix 5 ~>

public export 0
algebraOver : (sig : Signature) -> (U : sig.T -> Type) -> Type
algebraOver sig x = {t : sig.T} -> (op : Op sig t) -> x ^ op.arity -> x t

public export
record RawAlgebra (0 sig : Signature) where
  constructor MkRawAlgebra
  0 U : sig.T -> Type
  sem : sig `algebraOver` U

public export
record RawSetoidAlgebra (0 sig : Signature) where
  constructor MkRawSetoidAlgebra
  raw        : RawAlgebra sig
  0 relation : (t : sig.T) -> Rel (raw.U t)

public export
record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where
  constructor MkIsAlgebra
  equivalence : IndexedEquivalence sig.T a.U
  semCong     : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity}
    -> Pointwise equivalence.relation tms tms'
    -> equivalence.relation t (a.sem op tms) (a.sem op tms')

public export
record Algebra (0 sig : Signature) where
  constructor MakeAlgebra
  raw        : RawAlgebra sig
  algebra    : IsAlgebra sig raw

public export
MkAlgebra : (U : IndexedSetoid sig.T)
  -> (sem : {t : sig.T} -> (op : Op sig t) -> index (Product U) op.arity ~> index U t)
  -> Algebra sig
MkAlgebra u sem = MakeAlgebra
  { raw     = MkRawAlgebra
    { U   = u.U
    , sem = \op => (sem op).H
    }
  , algebra = MkIsAlgebra
    { equivalence = u.equivalence
    , semCong     = \op => (sem op).homomorphic _ _
    }
  }

public export 0
(.relation) : (0 a : Algebra sig) -> (t : sig.T) -> Rel (a.raw.U t)
(.relation) a = a.algebra.equivalence.relation

public export
(.setoid) : Algebra sig -> IndexedSetoid sig.T
(.setoid) a = MkIndexedSetoid a.raw.U a.algebra.equivalence

public export
(.rawSetoid) : Algebra sig -> RawSetoidAlgebra sig
(.rawSetoid) a = MkRawSetoidAlgebra a.raw a.relation

public export
(.semFunc) : (a : Algebra sig) -> {t : sig.T} -> (op : Op sig t)
  -> index (Product a.setoid) op.arity ~> index a.setoid t
a .semFunc op = MkSetoidHomomorphism (a.raw.sem op) (\_, _ => a.algebra.semCong op)

public export
record (~>) {0 sig : Signature} (a, b : Algebra sig)
  where
  constructor MkHomomorphism
  func    : a.setoid ~> b.setoid
  semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
    -> b.relation t (func.H t (a.raw.sem op tms)) (b.raw.sem op (map func.H tms))

public export
id : {a : Algebra sig} -> a ~> a
id = MkHomomorphism
  { func    = id a.setoid
  , semHomo = \op, tms =>
    reflect (index a.setoid _) $
    sym $
    cong (a.raw.sem op) $
    mapId tms
  }

public export
(.) : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
(.) f g = MkHomomorphism
  { func    = f.func . g.func
  , semHomo = \op, tms =>
    CalcWith (index c.setoid _) $
    |~ f.func.H _ (g.func.H _ (a.raw.sem op tms))
    ~~ f.func.H _ (b.raw.sem op (map g.func.H tms))   ...(f.func.homomorphic _ _ _ $ g.semHomo op tms)
    ~~ c.raw.sem op (map f.func.H (map g.func.H tms)) ...(f.semHomo op $ map g.func.H tms)
    ~~ c.raw.sem op (map ((f.func . g.func).H) tms)   .=<(cong (c.raw.sem op) $ mapComp tms)
  }