From 522eb40ab39800f75daa704ae56c18953c4885e7 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 6 Dec 2022 13:22:10 +0000 Subject: Migrate to use idris-setoid library. --- src/Soat/SecondOrder/Algebra.idr | 93 +++++----- src/Soat/SecondOrder/Algebra/Lift.idr | 319 ++++++++++++++++++---------------- 2 files changed, 217 insertions(+), 195 deletions(-) (limited to 'src/Soat/SecondOrder') diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr index 6f7cb4a..06d8674 100644 --- a/src/Soat/SecondOrder/Algebra.idr +++ b/src/Soat/SecondOrder/Algebra.idr @@ -1,6 +1,5 @@ module Soat.SecondOrder.Algebra -import Data.Morphism.Indexed import Data.Setoid.Indexed import Data.List.Elem @@ -15,15 +14,10 @@ extend : (U : a -> List a -> Type) -> (ctx : List a) -> Pair (List a) a -> Type extend x ctx ty = x (snd ty) (fst ty ++ ctx) public export -extendRel : {U : a -> List a -> Type} -> (rel : IRel (uncurry U)) - -> (ctx : List a) -> IRel (extend U ctx) +extendRel : {U : a -> List a -> Type} -> (rel : (ty : _) -> Rel (uncurry U ty)) + -> (ctx : List a) -> (ty : _) -> Rel (extend U ctx ty) 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 0 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) @@ -41,7 +35,7 @@ record RawAlgebra (0 sig : Signature) where public export (.extendSubst) : (a : RawAlgebra sig) -> (ctx : List sig.T) -> {ctx' : List sig.T} - -> (tms : (\t => a.U t ctx) ^ ctx') -> IFunc (extend a.U ctx') (extend a.U ctx) + -> (tms : (\t => a.U t ctx) ^ ctx') -> (ty : _) -> extend a.U ctx' ty -> extend a.U ctx ty a .extendSubst ctx tms ty tm = a.subst (snd ty) (fst ty ++ ctx) @@ -52,65 +46,69 @@ a .extendSubst ctx tms ty tm = a.subst public export record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where constructor MkIsAlgebra - 0 relation : IRel (uncurry a.U) - equivalence : IEquivalence (uncurry a.U) relation + equivalence : IndexedEquivalence _ (uncurry a.U) -- Congruences renameCong : (t : sig.T) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx') - -> {tm, tm' : a.U t ctx} -> relation (t, ctx) tm tm' - -> relation (t, ctx') (a.rename t f tm) (a.rename t f tm') + -> {tm, tm' : a.U t ctx} -> equivalence.relation (t, ctx) tm tm' + -> equivalence.relation (t, ctx') (a.rename t f tm) (a.rename t f tm') semCong : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t) -> {tms, tms' : extend a.U ctx ^ op.arity} - -> Pointwise (extendRel {U = a.U} relation ctx) tms tms' - -> relation (t, ctx) (a.sem ctx op tms) (a.sem ctx op tms') + -> Pointwise (extendRel {U = a.U} equivalence.relation ctx) tms tms' + -> equivalence.relation (t, ctx) (a.sem ctx op tms) (a.sem ctx op tms') substCong : (t : sig.T) -> (ctx : List sig.T) - -> {ctx' : _} -> {tm, tm' : a.U t ctx'} -> relation (t, ctx') tm tm' - -> {tms, tms' : (\t => a.U t ctx) ^ ctx'} -> Pointwise (\t => relation (t, ctx)) tms tms' - -> relation (t, ctx) (a.subst t ctx tm tms) (a.subst t ctx tm' tms') + -> {ctx' : _} -> {tm, tm' : a.U t ctx'} -> equivalence.relation (t, ctx') tm tm' + -> {tms, tms' : (\t => a.U t ctx) ^ ctx'} + -> Pointwise (\t => equivalence.relation (t, ctx)) tms tms' + -> equivalence.relation (t, ctx) (a.subst t ctx tm tms) (a.subst t ctx tm' tms') -- rename is functorial renameId : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx) - -> relation (t, ctx) (a.rename t {ctx = ctx} Relation.reflexive tm) tm + -> equivalence.relation (t, ctx) (a.rename t {ctx = ctx} Relation.reflexive tm) tm renameComp : (t : sig.T) -> {ctx, ctx', ctx'' : _} -> (f : ctx' `Sublist` ctx'') -> (g : ctx `Sublist` ctx') -> (tm : a.U t ctx) - -> relation (t, ctx'') (a.rename t (transitive g f) tm) (a.rename t f $ a.rename t g tm) + -> equivalence.relation (t, ctx'') + (a.rename t (transitive g f) tm) + (a.rename t f $ a.rename t g tm) -- sem are natural transformation semNat : {ctx, ctx' : _} -> (f : ctx `Sublist` ctx') -> {t : sig.T} -> (op : Op sig t) -> (tms : extend a.U ctx ^ op.arity) - -> relation (t, ctx') + -> equivalence.relation (t, ctx') (a.rename t f $ a.sem ctx op tms) (a.sem ctx' op $ map (\ty => a.rename (snd ty) (Relation.reflexive {x = fst ty} ++ f)) $ tms) -- var is natural transformation varNat : {t : _} -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx') -> (i : Elem t ctx) - -> relation (t, ctx') (a.rename t f $ a.var i) (a.var $ curry f i) + -> equivalence.relation (t, ctx') (a.rename t f $ a.var i) (a.var $ curry f i) -- subst is natural transformation substNat : (t : sig.T) -> {ctx, ctx' : _} -> (f : ctx `Sublist` ctx') -> {ctx'' : _} -> (tm : a.U t ctx'') -> (tms : (\t => a.U t ctx) ^ ctx'') - -> relation (t, ctx') + -> equivalence.relation (t, ctx') (a.rename t f $ a.subst t ctx tm tms) (a.subst t ctx' tm $ map (\t => a.rename t f) tms) -- subst is extranatural transformation substExnat : (t : sig.T) -> (ctx : List sig.T) -> {ctx', ctx'' : _} -> (f : ctx' `Sublist` ctx'') -> (tm : a.U t ctx') -> (tms : (\t => a.U t ctx) ^ ctx'') - -> relation (t, ctx) (a.subst t ctx (a.rename t f tm) tms) (a.subst t ctx tm (shuffle f tms)) + -> equivalence.relation (t, ctx) + (a.subst t ctx (a.rename t f tm) tms) + (a.subst t ctx tm (shuffle f tms)) -- var, subst is a monoid substComm : (t : sig.T) -> (ctx : List sig.T) -> {ctx', ctx'' : _} -> (tm : a.U t ctx'') -> (tms : (\t => a.U t ctx') ^ ctx'') -> (tms' : (\t => a.U t ctx) ^ ctx') - -> relation (t, ctx) + -> equivalence.relation (t, ctx) (a.subst t ctx (a.subst t ctx' tm tms) tms') (a.subst t ctx tm $ map (\t, tm => a.subst t ctx tm tms') tms) substVarL : {t : _} -> (ctx : List sig.T) -> {ctx' : _} -> (i : Elem t ctx') -> (tms : (\t => a.U t ctx) ^ ctx') - -> relation (t, ctx) (a.subst t ctx (a.var i) tms) (index tms i) + -> equivalence.relation (t, ctx) (a.subst t ctx (a.var i) tms) (index tms i) substVarR : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx) - -> relation (t, ctx) (a.subst t ctx {ctx' = ctx} tm $ tabulate a.var) tm + -> equivalence.relation (t, ctx) (a.subst t ctx {ctx' = ctx} tm $ tabulate a.var) tm -- sem, var and subst are compatible substCompat : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t) -> {ctx' : _} -> (tms : extend a.U ctx' ^ op.arity) -> (tms' : (\t => a.U t ctx) ^ ctx') - -> relation (t, ctx) + -> equivalence.relation (t, ctx) (a.subst t ctx (a.sem ctx' op tms) tms') (a.sem ctx op $ map (\ty, tm => @@ -126,44 +124,39 @@ record Algebra (0 sig : Signature) where algebra : IsAlgebra sig raw public export 0 -(.relation) : (0 a : Algebra sig) -> IRel (uncurry a.raw.U) -(.relation) a = a.algebra.relation +(.relation) : (0 a : Algebra sig) -> (ty : _) -> Rel (uncurry a.raw.U ty) +(.relation) a = a.algebra.equivalence.relation public export -(.setoid) : Algebra sig -> ISetoid (Pair sig.T (List sig.T)) -(.setoid) a = MkISetoid (uncurry a.raw.U) a.relation a.algebra.equivalence +(.setoid) : Algebra sig -> IndexedSetoid (Pair sig.T (List sig.T)) +(.setoid) a = MkIndexedSetoid (uncurry a.raw.U) a.algebra.equivalence public export -(.setoidAt) : Algebra sig -> (ctx : List sig.T) -> ISetoid sig.T -(.setoidAt) a ctx = MkISetoid - (flip a.raw.U ctx) - (\t => a.relation (t, ctx)) - (\_ => a.algebra.equivalence _) +(.setoidAt) : Algebra sig -> (ctx : List sig.T) -> IndexedSetoid sig.T +(.setoidAt) a ctx = reindex (flip MkPair ctx) a.setoid public export -(.varFunc) : (a : Algebra sig) -> (ctx : _) -> IFunction (isetoid (flip Elem ctx)) (a.setoidAt ctx) -(.varFunc) a ctx = MkIFunction - (\_ => a.raw.var) - (\_ => (a.algebra.equivalence _).equalImpliesEq . cong a.raw.var) +(.varFunc) : (a : Algebra sig) -> (ctx : _) -> irrelevantCast (flip Elem ctx) ~> a.setoidAt ctx +(.varFunc) a ctx = mate (\_ => a.raw.var) public export record (~>) {0 sig : Signature} (a, b : Algebra sig) where constructor MkHomomorphism - func : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx - cong : (t : sig.T) -> (ctx : List sig.T) -> {tm, tm' : a.raw.U t ctx} - -> a.relation (t, ctx) tm tm' -> b.relation (t, ctx) (func t ctx tm) (func t ctx tm') + func : a.setoid ~> b.setoid renameHomo : (t : sig.T) -> {ctx, ctx' : _} -> (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx) - -> b.relation (t, ctx') (func t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ func t ctx tm) + -> b.relation (t, ctx') + (func.H (t, ctx') $ a.raw.rename t g tm) + (b.raw.rename t g $ func.H (t, ctx) tm) semHomo : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t) -> (tms : extend a.raw.U ctx ^ op.arity) -> b.relation (t, ctx) - (func t ctx $ a.raw.sem ctx op tms) - (b.raw.sem ctx op $ map (\ty => func (snd ty) (fst ty ++ ctx)) tms) + (func.H (t, ctx) $ a.raw.sem ctx op tms) + (b.raw.sem ctx op $ map (\ty => func.H (snd ty, fst ty ++ ctx)) tms) varHomo : {t : _} -> {ctx : _} -> (i : Elem t ctx) - -> b.relation (t, ctx) (func t ctx $ a.raw.var i) (b.raw.var i) + -> b.relation (t, ctx) (func.H (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') -> (tms : (\t => a.raw.U t ctx) ^ ctx') -> b.relation (t, ctx) - (func t ctx $ a.raw.subst t ctx tm tms) - (b.raw.subst t ctx (func t ctx' tm) $ map (\t => func t ctx) tms) + (func.H (t, ctx) $ a.raw.subst t ctx tm tms) + (b.raw.subst t ctx (func.H (t, ctx') tm) $ map (\t => func.H (t, ctx)) tms) diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr index 30bcd91..bb3d24b 100644 --- a/src/Soat/SecondOrder/Algebra/Lift.idr +++ b/src/Soat/SecondOrder/Algebra/Lift.idr @@ -1,7 +1,6 @@ module Soat.SecondOrder.Algebra.Lift import Data.List.Elem -import Data.Morphism.Indexed import Data.Setoid.Indexed import Soat.Data.Product @@ -14,37 +13,40 @@ import Soat.SecondOrder.Signature.Lift import Syntax.PreorderReasoning.Setoid %default total +%ambiguity_depth 4 public export project : SecondOrder.Algebra.RawAlgebra (lift sig) -> (ctx : List sig.T) -> FirstOrder.Algebra.RawAlgebra sig project a ctx = MkRawAlgebra - (flip a.U ctx) + (\t => a.U t ctx) (\op => a.sem ctx (MkOp (Op op.op)) . wrap (MkPair [])) -public export -projectIsAlgebra : IsAlgebra (lift sig) a -> (ctx : List sig.T) -> IsAlgebra sig (project a ctx) -projectIsAlgebra a ctx = MkIsAlgebra - (\t => a.relation (t, ctx)) - (\t => a.equivalence (t, ctx)) - (\op => a.semCong ctx _ . wrapIntro) - public export projectAlgebra : (0 sig : _) -> Algebra (lift sig) -> (ctx : List sig.T) -> Algebra sig -projectAlgebra sig a ctx = MkAlgebra _ (projectIsAlgebra a.algebra ctx) +projectAlgebra sig a ctx = MkAlgebra + { raw = project a.raw ctx + , algebra = MkIsAlgebra + { equivalence = (reindex (flip MkPair ctx) a.setoid).equivalence + , semCong = \op => a.algebra.semCong ctx (MkOp (Op op.op)) . wrapIntro + } + } public export projectHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> a ~> b -> (ctx : _) -> projectAlgebra sig a ctx ~> projectAlgebra sig b ctx projectHomo f ctx = MkHomomorphism - { func = \t => f.func t ctx - , cong = \t => f.cong t ctx - , semHomo = \op, tms => CalcWith (b.setoid.index _) $ - |~ f.func _ ctx (a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) tms)) - ~~ b.raw.sem ctx (MkOp (Op op.op)) (map (extendFunc f.func ctx) (wrap (MkPair []) tms)) + { func = MkIndexedSetoidHomomorphism + { H = \t => f.func.H (t, ctx) + , homomorphic = \t => f.func.homomorphic (t, ctx) + } + , semHomo = \op, tms => CalcWith (index b.setoid _) $ + |~ f.func.H (_, ctx) (a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) tms)) + ~~ b.raw.sem ctx (MkOp (Op op.op)) (map (\ty => f.func.H (snd ty, fst ty ++ ctx)) (wrap (MkPair []) tms)) ...(f.semHomo ctx (MkOp (Op op.op)) (wrap (MkPair []) tms)) - ~~ b.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => f.func t ctx) tms)) - .=.(cong (b.raw.sem ctx (MkOp (Op op.op))) $ mapWrap (MkPair []) {f = extendFunc f.func ctx} tms) + ~~ b.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => f.func.H (t, ctx)) tms)) + .=.(cong (b.raw.sem ctx (MkOp (Op op.op))) $ + mapWrap (MkPair []) {f = \ty => f.func.H (snd ty, fst ty ++ ctx)} tms) } public export @@ -52,23 +54,30 @@ public export -> (f : ctx `Sublist` ctx') -> projectAlgebra sig a ctx ~> projectAlgebra sig a ctx' (.renameHomo) a f = MkHomomorphism - { func = \t => a.raw.rename t f - , cong = \t => a.algebra.renameCong t f - , semHomo = \op, tms => CalcWith (a.setoid.index _) $ + { func = MkIndexedSetoidHomomorphism + { H = \t => a.raw.rename t f + , homomorphic = \t, _, _ => a.algebra.renameCong t f + } + , semHomo = \op, tms => CalcWith (index a.setoid _) $ |~ a.raw.rename _ f (a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) tms)) ~~ a.raw.sem _ (MkOp (Op op.op)) (map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms)) ...(a.algebra.semNat f (MkOp (Op op.op)) (wrap (MkPair []) tms)) ~~ a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => a.raw.rename t f) tms)) ...(a.algebra.semCong _ (MkOp (Op op.op)) $ - CalcWith (pwSetoid (reindex (\ty => (snd ty, fst ty ++ _)) a.setoid) _) $ + CalcWith (index (pwSetoid (reindex (\ty => (snd ty, fst ty ++ _)) a.setoid)) _) $ |~ map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms) ~~ wrap (MkPair []) (map (\t => a.raw.rename t (reflexive {x = []} ++ f)) tms) .=.(mapWrap (MkPair []) tms) ~~ wrap (MkPair []) (map (\t => a.raw.rename t f) tms) - .=.(cong (wrap (MkPair [])) $ - pwEqImpliesEqual $ - mapIntro'' (\t, tm, _, Refl => cong (\f => a.raw.rename t f tm) $ uncurryCurry f) $ - equalImpliesPwEq Refl)) + ...(wrapIntro $ + mapIntro'' (\t, tm, tm', eq => + CalcWith (index a.setoid (t, _)) $ + |~ a.raw.rename t (reflexive {x = []} ++ f) tm + ~~ a.raw.rename t f tm + .=.(cong (\f => a.raw.rename t f tm) $ uncurryCurry f) + ~~ a.raw.rename t f tm' + ...(a.algebra.renameCong t f eq)) $ + (pwSetoid (a.setoidAt ctx)).equivalence.reflexive _ tms)) } public export @@ -76,17 +85,19 @@ public export -> {ctx' : List sig.T} -> (tms : (\t => a.raw.U t ctx) ^ ctx') -> projectAlgebra sig a ctx' ~> projectAlgebra sig a ctx (.substHomo1) a ctx tms = MkHomomorphism - { func = \t, tm => a.raw.subst t ctx tm tms - , cong = \t, eq => - a.algebra.substCong t ctx eq $ - pwRefl (\_ => (a.algebra.equivalence _).refl) - , semHomo = \op, tms' => CalcWith (a.setoid.index _) $ + { func = MkIndexedSetoidHomomorphism + { H = \t, tm => a.raw.subst t ctx tm tms + , homomorphic = \t, _, _, eq => + a.algebra.substCong t ctx eq $ + (pwSetoid (a.setoidAt _)).equivalence.reflexive _ tms + } + , semHomo = \op, tms' => CalcWith (index a.setoid _) $ |~ a.raw.subst _ ctx (a.raw.sem ctx' (MkOp (Op op.op)) (wrap (MkPair []) tms')) tms ~~ a.raw.sem ctx (MkOp (Op op.op)) (map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms')) ...(a.algebra.substCompat ctx (MkOp (Op op.op)) (wrap (MkPair []) tms') tms) ~~ a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm tms) tms')) ...(a.algebra.semCong ctx (MkOp (Op op.op)) $ - CalcWith (pwSetoid (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid) _) $ + CalcWith (index (pwSetoid (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid)) _) $ |~ map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms') ~~ wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm (map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms)) tms') .=.(mapWrap (MkPair []) tms') @@ -94,39 +105,42 @@ public export ...(wrapIntro $ mapIntro' (\t, eq => a.algebra.substCong t ctx eq $ - CalcWith (pwSetoid (a.setoidAt _) _) $ + CalcWith (index (pwSetoid (a.setoidAt _)) _) $ |~ map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms - ~~ map (\t => a.raw.rename t reflexive) tms - .=.(pwEqImpliesEqual $ - mapIntro' (\t => cong2 (a.raw.rename t) $ uncurryCurry reflexive) $ - equalImpliesPwEq Refl) ~~ map (\t => id) tms - ...(mapIntro' (\t, Refl => a.algebra.renameId t ctx _) $ - equalImpliesPwEq Refl) + ...(mapIntro'' (\t, tm, tm', eq => + CalcWith (index a.setoid (t, ctx)) $ + |~ a.raw.rename t ([] {ys = []} ++ reflexive) tm + ~~ a.raw.rename t reflexive tm + .=.(cong (\f => a.raw.rename t f tm) $ uncurryCurry reflexive) + ~~ tm + ...(a.algebra.renameId t ctx tm) + ~~ tm' + ...(eq)) $ + (pwSetoid (a.setoidAt _)).equivalence.reflexive _ _) ~~ tms .=.(mapId tms)) $ - pwRefl (\t => (a.algebra.equivalence _).refl))) + (pwSetoid (a.setoidAt _)).equivalence.reflexive _ _)) } -renameBodyFunc : (f : ctx `Sublist` ctx') - -> IFunction - (isetoid (flip Elem ctx)) - (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx'))).setoid -renameBodyFunc f = MkIFunction (\_ => Done . curry f) (\_ => Done' . cong (curry f)) +-- renameBodyFunc : (f : ctx `Sublist` ctx') +-- -> irrelevantCast (flip Elem ctx) ~> +-- (FreeAlgebra {sig = sig} (irrelevantCast (flip Elem ctx'))).setoid +-- renameBodyFunc f = mate (\_ => Done . curry f) -indexFunc : {ctx : List sig.T} -> (tms : Term sig (flip Elem ctx) ^ ts) - -> IFunction - (isetoid (flip Elem ts)) - (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx))).setoid -indexFunc tms = MkIFunction - (\_ => index tms) - (\_ => ((FreeIsAlgebra (isetoid (flip Elem _))).equivalence _).equalImpliesEq . cong (index tms)) +-- indexFunc : {ctx : List sig.T} -> (tms : Term sig (flip Elem ctx) ^ ts) +-- -> irrelevantCast (flip Elem ts) ~> +-- (FreeAlgebra {sig = sig} (irrelevantCast (flip Elem ctx))).setoid +-- indexFunc tms = mate (\_ => index tms) + +freeAlg : List sig.T -> FirstOrder.Algebra.Algebra sig +freeAlg ctx = FreeAlgebra (irrelevantCast (flip Elem ctx)) public export Initial : (0 sig : _) -> SecondOrder.Algebra.RawAlgebra (lift sig) Initial sig = MkRawAlgebra - (\t, ctx => Term sig (flip Elem ctx) t) - (\t, f => bindTerm {a = Free _} (renameBodyFunc f).func) + (\t, ctx => (freeAlg ctx).raw.U t) + (\t, f => bindTerm {a = Free _} (\_ => Done . curry f)) (\_, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair [])) Done (\_, _, t, ts => bindTerm {a = Free _} (\_ => index ts) t) @@ -134,29 +148,37 @@ Initial sig = MkRawAlgebra public export InitialIsAlgebra : (0 sig : _) -> SecondOrder.Algebra.IsAlgebra (lift sig) (Initial sig) InitialIsAlgebra sig = MkIsAlgebra - { relation = \(t, ctx) => (~=~) {sig = sig} {v = flip Elem ctx} (\_ => Equal) t - , equivalence = \(t, ctx) => tmRelEq (\_ => equiv) t - , renameCong = \t, f => bindTermCong {a = FreeAlgebra (isetoid (flip Elem _))} (renameBodyFunc f) - , semCong = \_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro + { equivalence = MkIndexedEquivalence + { relation = \(t, ctx) => (freeAlg ctx).relation t + , reflexive = \(t, ctx) => (freeAlg ctx).algebra.equivalence.reflexive t + , symmetric = \(t, ctx) => (freeAlg ctx).algebra.equivalence.symmetric t + , transitive = \(t, ctx) => (freeAlg ctx).algebra.equivalence.transitive t + } + , renameCong = \t, f => bindTermCong + { a = freeAlg _ + , env = mate (\_ => Done . curry f) + } + , semCong = \_ , (MkOp (Op op)) => Call (MkOp op) . unwrapIntro , substCong = \_, _, eq, eqs => bindTermCong' - {a = FreeAlgebra (isetoid (flip Elem _))} - (\t, Refl => index eqs _) - eq + { a = freeAlg _ + , cong = \_, Refl => index eqs _ + , eq + } , renameId = \t, ctx, tm => - tmRelSym (\_ => MkSymmetric symmetric) $ - bindUnique (renameBodyFunc reflexive) id (\i => Done' $ sym $ curryUncurry id i) $ - tm + (freeAlg _).setoid.equivalence.symmetric t _ _ $ + bindUnique (mate (\_ => Done . curry reflexive)) id (\i => Done $ sym $ curryUncurry id i) tm , renameComp = \t, f, g, tm => - tmRelSym (\_ => MkSymmetric symmetric) $ + (freeAlg _).setoid.equivalence.symmetric t _ _ $ bindUnique - {a = FreeAlgebra (isetoid (flip Elem _))} - (renameBodyFunc (transitive g f)) - (bindHomo (renameBodyFunc f) . bindHomo (renameBodyFunc g)) - (\i => Done' $ sym $ curryUncurry (curry f . curry g) i) $ - tm + { a = freeAlg _ + , env = mate (\_ => Done . curry (transitive g f)) + , f = bindHomo (mate (\_ => Done . curry f)) . bindHomo (mate (\_ => Done . curry g)) + , cong = \i => Done $ sym $ curryUncurry (curry f . curry g) i + , tm + } , semNat = \f, (MkOp (Op op)), tms => - Call' (MkOp op) $ - CalcWith (pwSetoid (FreeAlgebra (isetoid (flip Elem _))).setoid _) $ + Call (MkOp op) $ + CalcWith (index (pwSetoid (freeAlg _).setoid) _) $ |~ bindTerms {a = Free _} (\_ => Done . curry f) (unwrap (MkPair []) tms) ~~ map (\_ => bindTerm {a = Free _} (\_ => Done . curry f)) (unwrap (MkPair []) tms) .=.(bindTermsIsMap {a = Free _} _ _) @@ -164,76 +186,78 @@ InitialIsAlgebra sig = MkIsAlgebra ..<(mapIntro' (\t => bindTermCong' {rel = \_ => Equal} - {a = FreeAlgebra (isetoid (flip Elem _))} - (\_, Refl => Done' $ curryUncurry (curry f) _)) $ - tmsRelRefl (\_ => MkReflexive reflexive) (unwrap (MkPair []) tms)) + {a = freeAlg _} + (\_, Refl => Done $ curryUncurry (curry f) _)) $ + (pwSetoid (freeAlg _).setoid).equivalence.reflexive _ (unwrap (MkPair []) tms)) ~~ unwrap (MkPair []) (map (\ty => bindTerm {a = Free _} (\_ => Done . curry (reflexive {x = fst ty} ++ f))) tms) .=.(mapUnwrap (MkPair []) tms) - , varNat = \_, _ => Done' Refl - , substNat = \t, f, tm, tms => - bindUnique - {a = FreeAlgebra (isetoid (flip Elem _))} - (indexFunc _) - (bindHomo (renameBodyFunc f) . bindHomo (indexFunc tms)) - (\i => - tmRelReflexive (\_ => MkReflexive reflexive) $ - sym $ - indexMap tms i) - tm - , substExnat = \t, ctx, f, tm, tms => - bindUnique - {a = FreeAlgebra (isetoid (flip Elem _))} - (indexFunc _) - (bindHomo (indexFunc tms) . bindHomo (renameBodyFunc f)) - (\i => - tmRelReflexive (\_ => MkReflexive reflexive) $ - sym $ - indexShuffle f i) - tm - , substComm = \t, ctx, tm, tms, tms' => - bindUnique - {a = FreeAlgebra (isetoid (flip Elem _))} - (indexFunc _) - (bindHomo (indexFunc tms') . bindHomo (indexFunc tms)) - (\i => - tmRelReflexive (\_ => MkReflexive reflexive) $ - sym $ - indexMap tms i) - tm - , substVarL = \_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _ + , varNat = \_, _ => Done Refl + , substNat = \t, f, tm, tms => bindUnique + { a = freeAlg _ + , env = mate (\_ => index $ map (\_ => bindTerm {a = Free _} (\_ => Done . curry f)) tms) + , f = bindHomo (mate (\_ => Done . curry f)) . bindHomo (mate (\_ => index tms)) + , cong = \i => + reflect (index (freeAlg _).setoid _) $ + sym $ + indexMap tms i + , tm + } + , substExnat = \t, ctx, f, tm, tms => bindUnique + { a = freeAlg _ + , env = mate (\_ => index $ shuffle f tms) + , f = bindHomo (mate (\_ => index tms)) . bindHomo (mate (\_ => Done . curry f)) + , cong = \i => + reflect (index (freeAlg _).setoid _) $ + sym $ + indexShuffle f i + , tm + } + , substComm = \t, ctx, tm, tms, tms' => bindUnique + { a = freeAlg _ + , env = mate (\_ => index $ map (\_ => bindTerm {a = Free _} (\_ => index tms')) tms) + , f = bindHomo (mate (\_ => index tms')) . bindHomo (mate (\_ => index tms)) + , cong = \i => + reflect (index (freeAlg _).setoid _) $ + sym $ + indexMap tms i + , tm + } + , substVarL = \_, _, _ => (freeAlg _).setoid.equivalence.reflexive _ _ , substVarR = \t, ctx, tm => - tmRelSym (\_ => MkSymmetric symmetric) $ + (freeAlg _).setoid.equivalence.symmetric t _ _ $ bindUnique - {a = FreeAlgebra (isetoid (flip Elem _))} - (indexFunc _) - id - (\i => - tmRelReflexive (\_ => MkReflexive reflexive) $ + { v = irrelevantCast (flip Elem ctx) + , a = freeAlg ctx + , env = mate (\_ => index $ tabulate (Done {sig = sig, v = flip Elem ctx})) + , f = id + , cong = \i => + reflect (index (freeAlg ctx).setoid _) $ sym $ - indexTabulate Done i) - tm + indexTabulate Done i + , tm + } , substCompat = \ctx, (MkOp (Op op)), tms, tms' => - Call' (MkOp op) $ - CalcWith (pwSetoid (FreeAlgebra (isetoid (flip Elem _))).setoid _) $ + Call (MkOp op) $ + CalcWith (index (pwSetoid (freeAlg _).setoid) _) $ |~ bindTerms {a = Free _} (\_ => index tms') (unwrap (MkPair []) tms) ~~ map (\_ => bindTerm {a = Free _} (\_ => index tms')) (unwrap (MkPair []) tms) .=.(bindTermsIsMap {a = Free _} _ _) ~~ map (\t => (Initial sig).extendSubst ctx tms' ([], t)) (unwrap (MkPair []) tms) ..<(mapIntro' (\t => bindTermCong' {rel = \_ => Equal} - {a = FreeAlgebra (isetoid (flip Elem _))} - (\t, Refl => CalcWith ((FreeAlgebra (isetoid (flip Elem _))).setoid.index _) $ + {a = freeAlg _} + (\t, Refl => CalcWith (index (freeAlg _).setoid _) $ |~ index (map (\_ => bindTerm {a = Free _} (\_ => Done . curry ([] {ys = []} ++ reflexive))) tms') _ ~~ bindTerm {a = Free _} (\_ => Done . curry ([] {ys = []} ++ reflexive)) (index tms' _) .=.(indexMap tms' _) ~~ index tms' _ ..<(bindUnique - (renameBodyFunc ([] {ys = []} ++ reflexive)) - id - (\i => Done' $ sym $ trans (curryUncurry _ i) (curryUncurry id i)) - (index tms' _)))) $ - tmsRelRefl (\_ => MkReflexive reflexive) $ - unwrap (MkPair []) tms) + { env = mate (\_ => Done . curry ([] {ys = []} ++ reflexive)) + , f = id + , cong = \i => Done $ sym $ trans (curryUncurry _ i) (curryUncurry id i) + , tm = index tms' _ + }))) $ + (pwSetoid (freeAlg _).setoid).equivalence.reflexive _ (unwrap (MkPair []) tms)) ~~ unwrap (MkPair []) (map ((Initial sig).extendSubst ctx tms') tms) .=.(mapUnwrap (MkPair []) tms) } @@ -244,15 +268,18 @@ InitialAlgebra sig = MkAlgebra (Initial sig) (InitialIsAlgebra sig) public export freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T) - -> FreeAlgebra (isetoid (flip Elem ctx)) ~> projectAlgebra sig (InitialAlgebra sig) ctx + -> FreeAlgebra (irrelevantCast (flip Elem ctx)) ~> + projectAlgebra sig (InitialAlgebra sig) ctx freeToInitialHomo sig ctx = MkHomomorphism - { func = \_ => id - , cong = \_ => id + { func = MkIndexedSetoidHomomorphism + { H = \_ => id + , homomorphic = \_, _, _ => id + } , semHomo = \(MkOp op), tms => - Call' (MkOp op) $ - tmsRelSym (\_ => MkSymmetric symmetric) $ - tmsRelReflexive (\_ => MkReflexive reflexive) $ - transitive (unwrapWrap _ _) (mapId tms) + Call (MkOp op) $ + reflect (index (pwSetoid ((InitialAlgebra sig).setoidAt ctx)) _) $ + sym $ + trans (unwrapWrap (extend (Initial sig).U ctx) _) (mapId tms) } public export @@ -263,31 +290,33 @@ fromInitial a t ctx = bindTerm {a = project a ctx} (\_ => a.var) public export fromInitialHomo : (a : Algebra (lift sig)) -> InitialAlgebra sig ~> a fromInitialHomo a = MkHomomorphism - { func = fromInitial a.raw - , cong = \t , ctx => bindTermCong {a = projectAlgebra sig a ctx} (a.varFunc ctx) + { func = MkIndexedSetoidHomomorphism + { H = \(t, ctx) => fromInitial a.raw t ctx + , homomorphic = \(t, ctx), _, _ => bindTermCong {a = projectAlgebra sig a ctx} (a.varFunc ctx) + } , renameHomo = \t, f => bindUnique' - {v = isetoid (flip Elem _)} + {v = irrelevantCast (flip Elem _)} {a = projectAlgebra sig a _} - (bindHomo (a.varFunc _) . bindHomo (renameBodyFunc f)) + (bindHomo (a.varFunc _) . bindHomo (mate (\_ => Done . curry f))) (a.renameHomo f . bindHomo (a.varFunc _)) - (\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i) + (\i => a.algebra.equivalence.symmetric _ _ _ $ a.algebra.varNat f i) , semHomo = \ctx, (MkOp (Op op)), tms => a.algebra.semCong ctx (MkOp (Op op)) $ - CalcWith (pwSetoid (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid) _) $ + CalcWith (index (pwSetoid (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid)) _) $ |~ wrap (MkPair []) (bindTerms {a = project a.raw ctx} (\_ => a.raw.var) (unwrap (MkPair []) tms)) ~~ wrap (MkPair []) (map (\t => fromInitial a.raw t ctx) (unwrap (MkPair []) tms)) .=.(cong (wrap _) $ bindTermsIsMap {a = project a.raw ctx} _ _) - ~~ wrap (MkPair []) (unwrap (MkPair []) (map (extendFunc (fromInitial a.raw) ctx) tms)) + ~~ wrap (MkPair []) (unwrap (MkPair []) (map (\ty => fromInitial a.raw (snd ty) (fst ty ++ ctx)) tms)) .=.(cong (wrap _) $ mapUnwrap (MkPair []) tms) - ~~ map (extendFunc (fromInitial a.raw) ctx) tms + ~~ map (\ty => fromInitial a.raw (snd ty) (fst ty ++ ctx)) tms .=.(wrapUnwrap _) - , varHomo = \_ => (a.algebra.equivalence _).reflexive + , varHomo = \i => a.algebra.equivalence.reflexive _ $ a.raw.var i , substHomo = \t, ctx, tm, tms => bindUnique' - {v = isetoid (flip Elem _)} + {v = irrelevantCast (flip Elem _)} {a = projectAlgebra sig a _} - (bindHomo (a.varFunc _) . bindHomo (indexFunc tms)) + (bindHomo (a.varFunc _) . bindHomo (mate (\_ => index tms))) (a.substHomo1 ctx _ . bindHomo (a.varFunc _)) - (\i => CalcWith (a.setoid.index _) $ + (\i => CalcWith (index a.setoid _) $ |~ bindTerm {a = project a.raw _} (\_ => a.raw.var) (index tms i) ~~ index (map (\_ => bindTerm {a = project a.raw _} (\_ => a.raw.var)) tms) i .=<(indexMap {f = \_ => bindTerm {a = project a.raw _} (\_ => a.raw.var)} tms i) @@ -300,9 +329,9 @@ public export fromInitialUnique : {a : SecondOrder.Algebra.Algebra (lift sig)} -> (f : InitialAlgebra sig ~> a) -> (t : sig.T) -> (ctx : List sig.T) -> (tm : Term sig (flip Elem ctx) t) - -> a.relation (t, ctx) (f.func t ctx tm) (fromInitial a.raw t ctx tm) + -> a.relation (t, ctx) (f.func.H (t, ctx) tm) (fromInitial a.raw t ctx tm) fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique - {v = isetoid (flip Elem _)} + {v = irrelevantCast (flip Elem _)} {a = projectAlgebra sig a ctx} (a.varFunc ctx) (projectHomo f ctx . freeToInitialHomo sig ctx) -- cgit v1.2.3