From 83c85bf396949287365a694a89e0f49a58cab5a2 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 6 Dec 2022 15:33:27 +0000
Subject: Cast algebraic structure as setoid homomorphisms.

---
 src/Soat/FirstOrder/Algebra.idr  |  5 +++++
 src/Soat/SecondOrder/Algebra.idr | 27 +++++++++++++++++++++++++++
 2 files changed, 32 insertions(+)

(limited to 'src')

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 97b6adc..982e54e 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -54,6 +54,11 @@ 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
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index e7927ae..e52c945 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -4,6 +4,7 @@ import Data.List.Elem
 import Data.List.Sublist
 import Data.Product
 import Data.Setoid.Indexed
+import Data.Setoid.Pair
 import Data.Setoid.Product
 
 import Soat.SecondOrder.Signature
@@ -136,10 +137,36 @@ public export
 (.setoidAt) : Algebra sig -> (ctx : List sig.T) -> IndexedSetoid sig.T
 (.setoidAt) a ctx = reindex (flip MkPair ctx) a.setoid
 
+public export
+(.renameFunc) : (a : Algebra sig) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx')
+  -> a.setoidAt ctx ~> a.setoidAt ctx'
+(.renameFunc) a f = MkIndexedSetoidHomomorphism
+  { H           = \t => a.raw.rename t f
+  , homomorphic = \t, _, _ => a.algebra.renameCong t f
+  }
+
+public export
+(.semFunc) : (a : Algebra sig) -> (ctx : _) -> {t : _} -> (op : Op sig t)
+  -> index (Product (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid)) op.arity
+       ~> index a.setoid (t, ctx)
+(.semFunc) a ctx op = MkSetoidHomomorphism
+  { H           = a.raw.sem ctx op
+  , homomorphic = \_, _ => a.algebra.semCong ctx op
+  }
+
 public export
 (.varFunc) : (a : Algebra sig) -> (ctx : _) -> irrelevantCast (flip Elem ctx) ~> a.setoidAt ctx
 (.varFunc) a ctx = mate (\_ => a.raw.var)
 
+public export
+(.substFunc) : (a : Algebra sig) -> (t : _) -> (ctx, ctx' : _)
+  -> Pair (index a.setoid (t, ctx')) (index (Product (a.setoidAt ctx)) ctx')
+       ~> index a.setoid (t, ctx)
+(.substFunc) a t ctx ctx' = MkSetoidHomomorphism
+  { H           = \x => a.raw.subst t ctx (fst x) (snd x)
+  , homomorphic = \_, _, eq => a.algebra.substCong t ctx (fst eq) (snd eq)
+  }
+
 public export
 record (~>) {0 sig : Signature} (a, b : Algebra sig)
   where
-- 
cgit v1.2.3