Generalise bindUnique.

2 files changed, 40 insertions, 8 deletions

diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr
index cd69098..f92c23c 100644
--- a/src/Soat/Data/Product.idr
+++ b/src/Soat/Data/Product.idr
@@ -109,6 +109,13 @@ namespace Pointwise
   pwRefl f {xs = []}        = []
   pwRefl f {xs = (x :: xs)} = reflexive :: pwRefl f
 
+
+  public export
+  pwReflexive : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
+    -> ((i : a) -> Reflexive (x i) (rel i))
+    -> {is : List a} -> {xs, ys : x ^ is} -> xs = ys -> Pointwise rel xs ys
+  pwReflexive refl Refl = pwRefl refl
+
   public export
   pwSym : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
     -> ((i : a) -> Symmetric (x i) (rel i))
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 8f1b71a..701d3d6 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -153,11 +153,38 @@ bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> Homomorphism (Fr
 bindHomo env = MkHomomorphism _ (bindIsHomo _ env)
 
 public export
+bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
+  -> (f, g : Homomorphism (FreeAlgebra v) a)
+  -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (g.f t (Done i)))
+  -> {t : sig.T} -> (tm : Term sig v.U t)
+  -> a.rel t (f.f t tm) (g.f t tm)
+
+public export
+bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
+  -> (f, g : Homomorphism (FreeAlgebra v) a)
+  -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (g.f t (Done i)))
+  -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
+  -> Pointwise a.rel (map f.f tms) (map g.f tms)
+
+bindUnique' f g cong (Done i)     = cong i
+bindUnique' f g cong (Call op ts) =
+  (a.algebra.equivalence _).transitive (f.homo.semHomo op ts) $
+  (a.algebra.equivalence _).symmetric $
+  (a.algebra.equivalence _).transitive (g.homo.semHomo op ts) $
+  (a.algebra.equivalence _).symmetric $
+  a.algebra.semCong op $
+  bindsUnique' f g cong ts
+
+bindsUnique' f g cong []        = []
+bindsUnique' f g cong (t :: ts) = bindUnique' f g cong t :: bindsUnique' f g cong ts
+
+public export
 bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
   -> (f : Homomorphism (FreeAlgebra v) a)
   -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.func t i))
   -> {t : sig.T} -> (tm : Term sig v.U t)
   -> a.rel t (f.f t tm) (bindTerm {a = a.raw} env.func tm)
+bindUnique env f = bindUnique' f (bindHomo env)
 
 public export
 bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
@@ -165,11 +192,9 @@ bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.s
   -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.func t i))
   -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
   -> Pointwise a.rel (map f.f tms) (bindTerms {a = a.raw} env.func 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
+bindsUnique env f cong ts =
+  pwTrans (\i => (a.algebra.equivalence i).trans)
+    (bindsUnique' f (bindHomo env) cong ts) $
+  pwReflexive (\i => (a.algebra.equivalence i).refl) $
+  sym $
+  bindTermsIsMap {a = a.raw} env.func ts
\ No newline at end of file