refactor: rename MakeRawAlgebra -> MkRawAlgebra.

5 files changed, 6 insertions, 14 deletions

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index b8cbc0c..f002dec 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -12,21 +12,13 @@ public export 0
 algebraOver : (sig : Signature) -> (U : sig.T -> Type) -> Type
 algebraOver sig x = {t : sig.T} -> (op : Op sig t) -> x ^ op.arity -> x t
 
-public export 0
-algebraOver' : (sig : Signature) -> (U : sig.T -> Type) -> Type
-algebraOver' sig x = {t : sig.T} -> (op : Op sig t) -> map x op.arity `ary` x t
-
 public export
 record RawAlgebra (0 sig : Signature) where
-  constructor MakeRawAlgebra
+  constructor MkRawAlgebra
   0 U : sig.T -> Type
   sem : sig `algebraOver` U
 
 public export
-MkRawAlgebra : (0 U : sig.T -> Type) -> (sem : sig `algebraOver'` U) -> RawAlgebra sig
-MkRawAlgebra u sem = MakeRawAlgebra u (\o => uncurry (sem o))
-
-public export
 record RawAlgebraWithRelation (0 sig : Signature) where
   constructor MkRawAlgebraWithRelation
   raw        : RawAlgebra sig
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index d0b1b14..84ac436 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -67,7 +67,7 @@ parameters {0 x, y : RawAlgebraWithRelation sig}
 
 public export
 Coproduct : (x, y : RawAlgebra sig) -> RawAlgebra sig
-Coproduct x y = MakeRawAlgebra
+Coproduct x y = MkRawAlgebra
   { U   = CoproductSet sig x.U y.U
   , sem = Call
   }
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 4a51f94..eaa2da2 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -127,7 +127,7 @@ namespace Rel
 
 public export
 Free : (0 V : sig.T -> Type) -> RawAlgebra sig
-Free v = MakeRawAlgebra (Term sig v) Call
+Free v = MkRawAlgebra (Term sig v) Call
 
 public export
 FreeIsAlgebra : (v : ISetoid sig.T) -> IsAlgebra sig (Free v.U) ((~=~) v.relation)
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 50877e9..664a5d7 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -24,7 +24,7 @@ algebraOver sig x = (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
 
 public export
 record RawAlgebra (0 sig : Signature) where
-  constructor MakeRawAlgebra
+  constructor MkRawAlgebra
   0 U    : (t : sig.T) -> (ctx : List sig.T) -> Type
   rename : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx') -> U t ctx -> U t ctx'
   sem    : sig `algebraOver` U
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index b08eb0e..5be7dd1 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -16,7 +16,7 @@ import Soat.SecondOrder.Signature.Lift
 public export
 project : SecondOrder.Algebra.RawAlgebra (lift sig) -> (ctx : List sig.T)
   -> FirstOrder.Algebra.RawAlgebra sig
-project a ctx = MakeRawAlgebra
+project a ctx = MkRawAlgebra
   (flip a.U ctx)
   (\op => a.sem ctx (MkOp (Op op.op)) . wrap (MkPair []))
 
@@ -133,7 +133,7 @@ indexFunc tms = MkIFunction
 
 public export
 Initial : (0 sig : _) -> SecondOrder.Algebra.RawAlgebra (lift sig)
-Initial sig = MakeRawAlgebra
+Initial sig = MkRawAlgebra
   (\t, ctx => Term sig (flip Elem ctx) t)
   (\t, f => bindTerm {a = Free _} (renameBodyFunc f).func)
   (\_, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair []))