From 2bd69bf893b7e1ebe4186639526451caf2083b12 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 2 Dec 2022 14:14:44 +0000
Subject: WIP: Frex is free

---
 src/Soat/SecondOrder/Algebra.idr | 26 ++++++++++++++++++--------
 1 file changed, 18 insertions(+), 8 deletions(-)

(limited to 'src/Soat/SecondOrder/Algebra.idr')

diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index c506c85..f28d4bc 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -17,6 +17,11 @@ extendRel : {U : a -> List a -> Type} -> (rel : IRel (uncurry U))
   -> (ctx : List a) -> IRel (extend U ctx)
 extendRel rel ctx ty = rel (snd ty, fst ty ++ ctx)
 
+public export
+extendFunc : {0 U, V : a -> List a -> Type} -> (f : (t : a) -> IFunc (U t) (V t)) -> (ctx : List a)
+  -> IFunc (extend U ctx) (extend V ctx)
+extendFunc f ctx ty = f (snd ty) (fst ty ++ ctx)
+
 public export
 algebraOver : (sig : Signature) -> (U : sig.T -> List sig.T -> Type) -> Type
 algebraOver sig x = (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
@@ -26,12 +31,22 @@ public export
 record RawAlgebra (0 sig : Signature) where
   constructor MakeRawAlgebra
   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'
+  rename : (t : sig.T) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx') -> U t ctx -> U t ctx'
   sem    : sig `algebraOver` U
   var    : forall t, ctx . (i : Elem t ctx) -> U t ctx
   subst  : (t : sig.T) -> (ctx : List sig.T)
     -> forall ctx' . U t ctx' -> (\t => U t ctx) ^ ctx' -> U t ctx
 
+public export
+(.extendSubst) : (a : RawAlgebra sig) -> (ctx : _) -> {ctx' : _}
+  -> (tms : (\t => a.U t ctx) ^ ctx') -> IFunc (extend a.U ctx') (extend a.U ctx)
+(.extendSubst) a ctx tms ty tm = a.subst
+  (snd ty)
+  (fst ty ++ ctx)
+  tm
+  (tabulate {is = fst ty} (a.var . Sublist.elemJoinL {ys = ctx}) ++
+   map (\t => a.rename t ([] {ys = fst ty} ++ Relation.reflexive {x = ctx})) tms)
+
 public export
 record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncurry a.U)) where
   constructor MkIsAlgebra
@@ -94,12 +109,7 @@ record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncur
     -> {ctx' : _} -> (tms : extend a.U ctx' ^ op.arity) -> (tms' : (\t => a.U t ctx) ^ ctx')
     -> rel (t, ctx)
          (a.subst t ctx (a.sem ctx' op tms) tms')
-         (a.sem ctx op $
-          map (\ty, tm =>
-            a.subst (snd ty) (fst ty ++ ctx) tm
-              (tabulate {is = fst ty} (a.var . Sublist.elemJoinL {ys = ctx}) ++
-               map (\t => a.rename t ([] {ys = fst ty} ++ Relation.reflexive {x = ctx})) tms')) $
-          tms)
+         (a.sem ctx op $ map (a.extendSubst ctx tms') $ tms)
 
 public export
 record Algebra (0 sig : Signature) where
@@ -139,7 +149,7 @@ record IsHomomorphism
     -> (tms : extend a.raw.U ctx ^ op.arity)
     -> b.relation (t, ctx)
          (f t ctx $ a.raw.sem ctx op tms)
-         (b.raw.sem ctx op $ map (\ty => f (snd ty) (fst ty ++ ctx)) tms)
+         (b.raw.sem ctx op $ map (extendFunc f ctx) tms)
   varHomo    : {t : _} -> {ctx : _} -> (i : Elem t ctx)
     -> b.relation (t, ctx) (f t ctx $ a.raw.var i) (b.raw.var i)
   substHomo  : (t : sig.T) -> (ctx : List sig.T) -> {ctx' : _} -> (tm : a.raw.U t ctx')
-- 
cgit v1.2.3