refactor: reorder definitions.

1 files changed, 34 insertions, 25 deletions

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)
@@ -110,6 +89,10 @@ namespace Rel
   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
 
@@ -121,6 +104,20 @@ FreeAlgebra v = MkAlgebra
   }
 
 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)}
   -> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.relation t (env t x) (env' t y))
@@ -154,18 +151,30 @@ bindTermsCong : {a : Algebra sig} -> (env : v ~> a.setoid)
 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)