module Soat.FirstOrder.Term

import Control.Relation

import Soat.Data.Product
import Soat.FirstOrder.Algebra
import Soat.FirstOrder.Signature
import Soat.Relation

%default total
%hide Control.Relation.Equivalence

public export
data Term : (0 sig : Signature) -> (0 _ : sig.T -> Type) -> sig.T -> Type where
  Done : (i : x t) -> Term sig x t
  Call : (op : Op sig t) -> (ts : Term sig x ^ op.arity) -> Term sig x t

Environment : {a : Type} -> (x, y : a -> Type) -> Type
Environment {a} x y = (t : a) -> x t -> y t

record SetoidEnvironment {a : Type} (x, y : ISetoid a) where
  f    : Environment {a} x.U y.U
  cong : (t : a) -> {u, v : x.U t} -> x.relation t u v -> y.relation t (f t u) (f t v)

public export
bindTerm : {auto a : RawAlgebra sig}
  -> Environment x a.U -> {t : _} -> Term sig x t -> a.U t

public export
bindTerms : {auto a : RawAlgebra sig}
  -> Environment x a.U -> {ts : _} -> Term sig x ^ ts -> a.U ^ ts

bindTerm         env (Done i)     = env _ i
bindTerm {a = a} env (Call op ts) = a.sem op (bindTerms env ts)

bindTerms env []        = []
bindTerms env (t :: ts) = bindTerm env t :: bindTerms env ts

public export
bindTermsIsMap : {auto a : RawAlgebra sig}
  -> (env : Environment x a.U) -> {ts : _} -> (tms : Term sig x ^ ts)
  -> bindTerms (\tm => env tm) tms = map (\t => bindTerm (\tm => env tm)) tms
bindTermsIsMap env []        = Refl
bindTermsIsMap env (t :: ts) = cong ((::) (bindTerm env t)) (bindTermsIsMap env ts)

namespace Rel
  public export
  data (~=~) : forall x . (0 r : IRel x) -> IRel (Term sig x)
    where
    Done' : {0 x : sig.T -> Type} -> {0 r : IRel x}
      -> {t : sig.T} -> {i, j : x t}
      -> r t i j
      -> (~=~) {sig = sig} {x = x} r t (Done i) (Done j)
    Call' : {0 x : sig.T -> Type} -> {0 r : IRel x}
      -> {t : sig.T} -> (op : Op sig t) -> {tms, tms' : Term sig x ^ op.arity}
      -> Pointwise ((~=~) {sig = sig} {x = x} r) tms tms'
      -> (~=~) {sig = sig} {x = x} r t (Call op tms) (Call op tms')

  tmRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
    -> {t : sig.T} -> (tm : Term sig V t) -> (~=~) rel t tm tm

  tmsRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
    -> {ts : List sig.T} -> (tms : Term sig V ^ ts) -> Pointwise ((~=~) rel) tms tms

  tmRelRefl refl (Done i)     = Done' reflexive
  tmRelRefl refl (Call op ts) = Call' op (tmsRelRefl refl ts)

  tmsRelRefl refl []        = []
  tmsRelRefl refl (t :: ts) = tmRelRefl refl t :: tmsRelRefl refl ts

  tmRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel)
    -> {t : sig.T} -> {tm, tm' : Term sig V t} -> (~=~) rel t tm tm' -> (~=~) rel t tm' tm

  tmsRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel)
    -> {ts : List sig.T} -> {tms, tms' : Term sig V ^ ts}
    -> Pointwise ((~=~) rel) tms tms' -> Pointwise ((~=~) rel) tms' tms

  tmRelSym sym (Done' i)     = Done' (symmetric i)
  tmRelSym sym (Call' op ts) = Call' op (tmsRelSym sym ts)

  tmsRelSym sym []        = []
  tmsRelSym sym (t :: ts) = tmRelSym sym t :: tmsRelSym sym ts

  tmRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel)
    -> {t : sig.T} -> {tm, tm', tm'' : Term sig V t}
    -> (~=~) rel t tm tm' -> (~=~) rel t tm' tm'' -> (~=~) rel t tm tm''

  tmsRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel)
    -> {ts : List sig.T} -> {tms, tms', tms'' : Term sig V ^ ts}
    -> Pointwise ((~=~) rel) tms tms' -> Pointwise ((~=~) rel) tms' tms''
    -> Pointwise ((~=~) rel) tms tms''

  tmRelTrans trans (Done' i)     (Done' j)     = Done' (transitive i j)
  tmRelTrans trans (Call' op ts) (Call' _ ts') = Call' op (tmsRelTrans trans ts ts')

  tmsRelTrans trans []        []          = []
  tmsRelTrans trans (t :: ts) (t' :: ts') = tmRelTrans trans t t' :: tmsRelTrans trans ts ts'

  export
  tmRelEq : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IEquivalence V rel
    -> IEquivalence _ ((~=~) {sig = sig} {x = V} rel)
  tmRelEq eq t = MkEquivalence
    (MkReflexive $ tmRelRefl (\t => (eq t).refl) _)
    (MkSymmetric $ tmRelSym (\t => (eq t).sym))
    (MkTransitive $ tmRelTrans (\t => (eq t).trans))

public export
Free : (0 V : sig.T -> Type) -> RawAlgebra sig
Free v = MakeRawAlgebra (Term sig v) Call

public export
FreeIsAlgebra : (v : ISetoid sig.T) -> IsAlgebra sig (Free v.U) ((~=~) v.relation)
FreeIsAlgebra v = MkIsAlgebra (tmRelEq v.equivalence) Call'

public export
FreeAlgebra : ISetoid sig.T -> Algebra sig
FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v)

public export
bindTermCong : {a : Algebra sig} -> (env : SetoidEnvironment x a.setoid)
  -> {t : sig.T} -> {tm, tm' : Term sig x.U t} -> (~=~) x.relation t tm tm'
  -> a.rel t (bindTerm {a = a.raw} env.f tm) (bindTerm {a = a.raw} env.f tm')

public export
bindTermsCong : {a : Algebra sig} -> (env : SetoidEnvironment x a.setoid)
  -> {ts : List sig.T} -> {tms, tms' : Term sig x.U ^ ts} -> Pointwise ((~=~) x.relation) tms tms'
  -> Pointwise a.rel (bindTerms {a = a.raw} env.f tms) (bindTerms {a = a.raw} env.f tms')

bindTermCong         env (Done' i)     = env.cong _ i
bindTermCong {a = a} env (Call' op ts) = a.algebra.semCong op (bindTermsCong env ts)

bindTermsCong env                                    []        = []
bindTermsCong env {tms = (_ :: _)} {tms' = (_ :: _)} (t :: ts) =
  bindTermCong env t :: bindTermsCong env ts

public export
bindHomo : (a : Algebra sig) -> (env : SetoidEnvironment v a.setoid)
  -> IsHomomorphism (FreeAlgebra v) a (\t => bindTerm {a = a.raw} env.f)
bindHomo a env = MkIsHomomorphism
  (\t, eq => bindTermCong env eq)
  (\op, tms =>
      a.algebra.semCong op $
      map (\t => (a.algebra.equivalence t).equalImpliesEq) $
      equalImpliesPwEq $
      bindTermsIsMap {a = a.raw} env.f tms)

public export
bind : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) -> Homomorphism (FreeAlgebra v) a
bind env = MkHomomorphism _ (bindHomo _ env)

public export
bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid)
  -> (f : Homomorphism (FreeAlgebra v) a)
  -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.f t i))
  -> {t : sig.T} -> (tm : Term sig v.U t)
  -> a.rel t (f.f t tm) ((Term.bind {a = a} env).f t tm)

public export
bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid)
  -> (f : Homomorphism (FreeAlgebra v) a)
  -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.f t i))
  -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
  -> Pointwise a.rel (map f.f tms) (bindTerms {a = a.raw} env.f tms)

bindUnique env f fDone (Done i)     = fDone i
bindUnique env f fDone (Call op ts) = (a.algebra.equivalence _).transitive
  (f.homo.semHomo op ts)
  (a.algebra.semCong op $ bindsUnique env f fDone ts)

bindsUnique env f fDone []        = []
bindsUnique env f fDone (t :: ts) = bindUnique env f fDone t :: bindsUnique env f fDone ts