From f77aeb6c4b25b381e897a4ab59c1008e34005404 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 5 Dec 2022 14:43:50 +0000 Subject: refactor: rename MakeRawAlgebra -> MkRawAlgebra. --- src/Soat/FirstOrder/Algebra.idr | 10 +--------- src/Soat/FirstOrder/Algebra/Coproduct.idr | 2 +- src/Soat/FirstOrder/Term.idr | 2 +- src/Soat/SecondOrder/Algebra.idr | 2 +- src/Soat/SecondOrder/Algebra/Lift.idr | 4 ++-- 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,20 +12,12 @@ 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 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 [])) -- cgit v1.2.3