diff options
Diffstat (limited to 'src/Soat/SecondOrder/Algebra.idr')
| -rw-r--r-- | src/Soat/SecondOrder/Algebra.idr | 26 |
1 files changed, 18 insertions, 8 deletions
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 @@ -18,6 +18,11 @@ extendRel : {U : a -> List a -> Type} -> (rel : IRel (uncurry U)) 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) -> extend x ctx ^ op.arity -> x t ctx @@ -26,13 +31,23 @@ 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 equivalence : IEquivalence (uncurry a.U) rel @@ -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') |