module Soat.FirstOrder.Algebra

import Data.Setoid.Indexed
import public Soat.Data.Product
import Soat.FirstOrder.Signature

import Syntax.PreorderReasoning.Setoid

%default total

public export
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
algebraOver' : (sig : Signature) -> (U : sig.T -> Type) -> Type
algebraOver' sig x = {t : sig.T} -> (op : Op sig t) -> map x op.arity `ary` x t

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

public export
MkRawAlgebra : (0 U : sig.T -> Type) -> (sem : sig `algebraOver'` U) -> RawAlgebra sig
MkRawAlgebra u sem = MakeRawAlgebra u (\o => uncurry (sem o))

public export
record RawAlgebraWithRelation (0 sig : Signature) where
  constructor MkRawAlgebraWithRelation
  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 MkAlgebra
  raw        : RawAlgebra sig
  algebra    : IsAlgebra sig raw

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

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

public export
(.rawWithRelation) : Algebra sig -> RawAlgebraWithRelation sig
(.rawWithRelation) a = MkRawAlgebraWithRelation a.raw a.relation

public export
record IsHomomorphism
  {0 sig : Signature} (a, b : Algebra sig)
  (f : (t : sig.T) -> a.raw.U t -> b.raw.U t)
  where
  constructor MkIsHomomorphism
  cong    : (t : sig.T) -> {tm, tm' : a.raw.U t}
    -> a.relation t tm tm' -> b.relation t (f t tm) (f t tm')
  semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
    -> b.relation t (f t (a.raw.sem op tms)) (b.raw.sem op (map f tms))

public export
record Homomorphism {0 sig : Signature} (a, b : Algebra sig)
  where
  constructor MkHomomorphism
  func : (t : sig.T) -> a.raw.U t -> b.raw.U t
  homo : IsHomomorphism a b func

public export
idIsHomo : {a : Algebra sig} -> IsHomomorphism a a (\_ => Basics.id)
idIsHomo = MkIsHomomorphism
  (\_ => id)
  (\op, tms =>
    reflect (index a.setoid _) $
    sym $
    cong (a.raw.sem op) $
    mapId tms)

public export
idHomo : {a : Algebra sig} -> Homomorphism a a
idHomo = MkHomomorphism _ idIsHomo

public export
compIsHomo : {a, b, c : Algebra sig}
  -> {f : (t : sig.T) -> b.raw.U t -> c.raw.U t} -> {g : (t : sig.T) -> a.raw.U t -> b.raw.U t}
  -> IsHomomorphism b c f -> IsHomomorphism a b g -> IsHomomorphism a c (\i => f i . g i)
compIsHomo fHomo gHomo = MkIsHomomorphism
  { cong = \t => fHomo.cong t . gHomo.cong t
  , semHomo = \op, tms => CalcWith (index c.setoid _) $
    |~ f _ (g _ (a.raw.sem op tms))
    ~~ f _ (b.raw.sem op (map g tms))           ...(fHomo.cong _ $ gHomo.semHomo op tms)
    ~~ c.raw.sem op (map f (map g tms))         ...(fHomo.semHomo op _)
    ~~ c.raw.sem op (map (\i => f i . g i) tms) .=<(cong (c.raw.sem op) $ mapComp tms)
  }

public export
compHomo : {a, b, c : Algebra sig} -> Homomorphism b c -> Homomorphism a b -> Homomorphism a c
compHomo f g = MkHomomorphism _ $ compIsHomo f.homo g.homo