From 2a1507c44f138e975934e77a4c3ff6b0c79decf6 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 7 Dec 2022 11:40:30 +0000
Subject: refactor: reorder definitions.

---
 src/Soat/FirstOrder/Term.idr | 59 +++++++++++++++++++++++++-------------------
 1 file changed, 34 insertions(+), 25 deletions(-)

(limited to 'src/Soat/FirstOrder/Term.idr')

diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index a53e6b0..5713ae9 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -16,27 +16,6 @@ data Term : (0 sig : Signature) -> (0 _ : sig.T -> Type) -> sig.T -> Type where
   Done : (i : v t) -> Term sig v t
   Call : (op : Op sig t) -> (ts : Term sig v ^ op.arity) -> Term sig v t
 
-public export
-bindTerm : {auto a : RawAlgebra sig} -> ((t : sig.T) -> v t -> a.U t)
-  -> {t : _} -> Term sig v t -> a.U t
-
-public export
-bindTerms : {auto a : RawAlgebra sig} -> ((t : sig.T) -> v t -> a.U t)
-  -> {ts : _} -> Term sig v ^ 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 : (t : sig.T) -> v t -> a.U t) -> {ts : _} -> (tms : Term sig v ^ 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 v . (0 r : (t : sig.T) -> Rel (v t)) -> (t : sig.T) -> Rel (Term sig v t)
@@ -109,6 +88,10 @@ namespace Rel
   Term : (0 sig : Signature) -> (V : IndexedSetoid sig.T) -> IndexedSetoid sig.T
   Term sig v = MkIndexedSetoid (Term sig v.U) (tmRelEq v.equivalence)
 
+public export
+injectFunc : v ~> Term sig v
+injectFunc = MkIndexedSetoidHomomorphism (\_ => Done) (\_, _, _ => Done)
+
 public export
 Free : (0 V : sig.T -> Type) -> RawAlgebra sig
 Free v = MkRawAlgebra (Term sig v) Call
@@ -120,6 +103,20 @@ FreeAlgebra v = MkAlgebra
   , sem = \op => MkSetoidHomomorphism (Call op) (\_, _ => Call op)
   }
 
+public export
+bindTerm : {auto a : RawAlgebra sig} -> ((t : sig.T) -> v t -> a.U t)
+  -> {t : _} -> Term sig v t -> a.U t
+
+public export
+bindTerms : {auto a : RawAlgebra sig} -> ((t : sig.T) -> v t -> a.U t)
+  -> {ts : _} -> Term sig v ^ 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
 bindTermCong' : {a : Algebra sig} -> {env, env' : (t : sig.T) -> v t -> a.raw.U t}
   -> {0 rel : (t : sig.T) -> Rel (v t)}
@@ -153,19 +150,31 @@ bindTermsCong : {a : Algebra sig} -> (env : v ~> a.setoid)
   -> Pointwise a.relation (bindTerms {a = a.raw} env.H tms) (bindTerms {a = a.raw} env.H tms')
 bindTermsCong env = bindTermsCong' env.homomorphic
 
+public export
+bindTermsIsMap : {auto a : RawAlgebra sig}
+  -> (env : (t : sig.T) -> v t -> a.U t) -> {ts : _} -> (tms : Term sig v ^ 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)
+
+public export
+bindFunc : {a : Algebra sig} -> (env : v ~> a.setoid) -> Term sig v ~> a.setoid
+bindFunc env = MkIndexedSetoidHomomorphism
+  { H           = \_ => bindTerm {a = a.raw} env.H
+  , homomorphic = \_, _, _ => bindTermCong env
+  }
+
 public export
 bindHomo : {a : Algebra sig} -> (env : v ~> a.setoid) -> FreeAlgebra v ~> a
 bindHomo env = MkHomomorphism
-  { func    = MkIndexedSetoidHomomorphism
-    { H           = \_ => bindTerm {a = a.raw} env.H
-    , homomorphic = \_, _, _ => bindTermCong env
-    }
+  { func    = bindFunc env
   , semHomo = \op, tms =>
     a.algebra.semCong op $
     reflect (index (Product a.setoid) _) $
     bindTermsIsMap {a = a.raw} env.H tms
   }
 
+-- TODO: port to (_ ~~> _).equivalence.relation.
 public export
 bindUnique' : {v : IndexedSetoid sig.T} -> {a : Algebra sig}
   -> (f, g : FreeAlgebra v ~> a)
-- 
cgit v1.2.3