summaryrefslogtreecommitdiff
path: root/src/Soat/FirstOrder
diff options
context:
space:
mode:
Diffstat (limited to 'src/Soat/FirstOrder')
-rw-r--r--src/Soat/FirstOrder/Algebra.idr47
-rw-r--r--src/Soat/FirstOrder/Algebra/Coproduct.idr150
-rw-r--r--src/Soat/FirstOrder/Term.idr187
3 files changed, 178 insertions, 206 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 6e39612..31b25b4 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -1,12 +1,12 @@
module Soat.FirstOrder.Algebra
-import Data.Morphism.Indexed
import Data.Setoid.Indexed
import public Soat.Data.Product
import Soat.FirstOrder.Signature
+import Syntax.PreorderReasoning.Setoid
+
%default total
-%hide Control.Relation.Equivalence
infix 5 ~>
@@ -24,15 +24,15 @@ public export
record RawSetoidAlgebra (0 sig : Signature) where
constructor MkRawSetoidAlgebra
raw : RawAlgebra sig
- 0 relation : IRel raw.U
+ 0 relation : (t : sig.T) -> Rel (raw.U t)
public export
record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where
constructor MkIsAlgebra
- 0 relation : IRel a.U
- equivalence : IEquivalence a.U relation
+ equivalence : IndexedEquivalence sig.T a.U
semCong : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity}
- -> Pointwise relation tms tms' -> relation t (a.sem op tms) (a.sem op tms')
+ -> Pointwise equivalence.relation tms tms'
+ -> equivalence.relation t (a.sem op tms) (a.sem op tms')
public export
record Algebra (0 sig : Signature) where
@@ -41,12 +41,12 @@ record Algebra (0 sig : Signature) where
algebra : IsAlgebra sig raw
public export 0
-(.relation) : (0 a : Algebra sig) -> IRel a.raw.U
-(.relation) a = a.algebra.relation
+(.relation) : (0 a : Algebra sig) -> (t : sig.T) -> Rel (a.raw.U t)
+(.relation) a = a.algebra.equivalence.relation
public export
-(.setoid) : Algebra sig -> ISetoid sig.T
-(.setoid) a = MkISetoid a.raw.U a.relation a.algebra.equivalence
+(.setoid) : Algebra sig -> IndexedSetoid sig.T
+(.setoid) a = MkIndexedSetoid a.raw.U a.algebra.equivalence
public export
(.rawSetoid) : Algebra sig -> RawSetoidAlgebra sig
@@ -56,19 +56,16 @@ public export
record (~>) {0 sig : Signature} (a, b : Algebra sig)
where
constructor MkHomomorphism
- func : (t : sig.T) -> a.raw.U t -> b.raw.U t
- cong : (t : sig.T) -> {tm, tm' : a.raw.U t}
- -> a.relation t tm tm' -> b.relation t (func t tm) (func t tm')
+ func : a.setoid ~> b.setoid
semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
- -> b.relation t (func t (a.raw.sem op tms)) (b.raw.sem op (map func tms))
+ -> b.relation t (func.H t (a.raw.sem op tms)) (b.raw.sem op (map func.H tms))
public export
id : {a : Algebra sig} -> a ~> a
id = MkHomomorphism
- { func = \_ => id
- , cong = \_ => id
+ { func = id a.setoid
, semHomo = \op, tms =>
- (a.algebra.equivalence _).equalImpliesEq $
+ reflect (index a.setoid _) $
sym $
cong (a.raw.sem op) $
mapId tms
@@ -77,15 +74,11 @@ id = MkHomomorphism
public export
(.) : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
(.) f g = MkHomomorphism
- { func = \t => f.func t . g.func t
- , cong = \t => f.cong t . g.cong t
+ { func = f.func . g.func
, semHomo = \op, tms =>
- (c.algebra.equivalence _).transitive
- (f.cong _ $ g.semHomo op tms) $
- (c.algebra.equivalence _).transitive
- (f.semHomo op (map g.func tms)) $
- (c.algebra.equivalence _).equalImpliesEq $
- sym $
- cong (c.raw.sem op) $
- mapComp tms
+ CalcWith (index c.setoid _) $
+ |~ f.func.H _ (g.func.H _ (a.raw.sem op tms))
+ ~~ f.func.H _ (b.raw.sem op (map g.func.H tms)) ...(f.func.homomorphic _ _ _ $ g.semHomo op tms)
+ ~~ c.raw.sem op (map f.func.H (map g.func.H tms)) ...(f.semHomo op $ map g.func.H tms)
+ ~~ c.raw.sem op (map ((f.func . g.func).H) tms) .=<(cong (c.raw.sem op) $ mapComp tms)
}
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index 5cb4c45..a8e4c0e 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -1,6 +1,5 @@
module Soat.FirstOrder.Algebra.Coproduct
-import Data.Morphism.Indexed
import Data.Setoid.Indexed
import Data.Setoid.Either
@@ -17,7 +16,9 @@ CoproductSet : (0 sig : Signature) -> (0 x, y : sig.T -> Type) -> sig.T -> Type
CoproductSet sig x y = Term sig (\i => Either (x i) (y i))
public export
-data (~=~) : (0 x, y : RawSetoidAlgebra sig) -> IRel (CoproductSet sig x.raw.U y.raw.U) where
+data (~=~) : (0 x, y : RawSetoidAlgebra sig) -> (t : sig.T)
+ -> Rel (CoproductSet sig x.raw.U y.raw.U t)
+ where
DoneL : {0 x, y : RawSetoidAlgebra sig}
-> {t : sig.T} -> {i, j : x.raw.U t} -> x.relation t i j
-> (~=~) x y t (Done $ Left i) (Done $ Left j)
@@ -36,31 +37,29 @@ data (~=~) : (0 x, y : RawSetoidAlgebra sig) -> IRel (CoproductSet sig x.raw.U y
-> (~=~) x y t tm tm' -> (~=~) x y t tm' tm'' -> (~=~) x y t tm tm''
parameters {0 x, y : RawSetoidAlgebra sig}
- coprodRelRefl : IReflexive x.raw.U x.relation -> IReflexive y.raw.U y.relation
+ coprodRelRefl : (xRefl : (t : sig.T) -> (a : x.raw.U t) -> x.relation t a a)
+ -> (yRefl : (t : sig.T) -> (a : y.raw.U t) -> y.relation t a a)
-> {t : _} -> (tm : _) -> (~=~) x y t tm tm
- coprodsRelRefl : IReflexive x.raw.U x.relation -> IReflexive y.raw.U y.relation
+ coprodsRelRefl : (xRefl : (t : sig.T) -> (a : x.raw.U t) -> x.relation t a a)
+ -> (yRefl : (t : sig.T) -> (a : y.raw.U t) -> y.relation t a a)
-> {ts : _} -> (tms : _ ^ ts) -> Pointwise ((~=~) x y) tms tms
- coprodRelRefl x y (Done (Left i)) = DoneL $ reflexive @{x _}
- coprodRelRefl x y (Done (Right i)) = DoneR $ reflexive @{y _}
+ coprodRelRefl x y (Done (Left i)) = DoneL $ x _ i
+ coprodRelRefl x y (Done (Right i)) = DoneR $ y _ i
coprodRelRefl x y (Call op ts) = Call op $ coprodsRelRefl x y ts
coprodsRelRefl x y [] = []
coprodsRelRefl x y (t :: ts) = coprodRelRefl x y t :: coprodsRelRefl x y ts
- coprodsRelReflexive : IReflexive x.raw.U x.relation -> IReflexive y.raw.U y.relation
- -> {ts : _} -> {tms, tms' : _ ^ ts} -> tms = tms' -> Pointwise ((~=~) x y) tms tms'
- coprodsRelReflexive x y Refl = coprodsRelRefl x y _
-
- tmRelImpliesCoprodRel : Term.Rel.(~=~) (\i => Either (x.relation i) (y.relation i)) t tm tm'
+ tmRelImpliesCoprodRel : Term.Rel.(~=~) (\i => x.relation i `Or` y.relation i) t tm tm'
-> (~=~) x y t tm tm'
tmRelsImpliesCoprodRels : {0 tms, tms' : _ ^ ts}
- -> Pointwise (Term.Rel.(~=~) (\i => Either (x.relation i) (y.relation i))) tms tms'
+ -> Pointwise (Term.Rel.(~=~) (\i => x.relation i `Or` y.relation i)) tms tms'
-> Pointwise ((~=~) x y) tms tms'
- tmRelImpliesCoprodRel (Done' (Left eq)) = DoneL eq
- tmRelImpliesCoprodRel (Done' (Right eq)) = DoneR eq
- tmRelImpliesCoprodRel (Call' op eqs) = Call op $ tmRelsImpliesCoprodRels eqs
+ tmRelImpliesCoprodRel (Done (Left eq)) = DoneL eq
+ tmRelImpliesCoprodRel (Done (Right eq)) = DoneR eq
+ tmRelImpliesCoprodRel (Call op eqs) = Call op $ tmRelsImpliesCoprodRels eqs
tmRelsImpliesCoprodRels [] = []
tmRelsImpliesCoprodRels (eq :: eqs) = tmRelImpliesCoprodRel eq :: tmRelsImpliesCoprodRels eqs
@@ -76,17 +75,17 @@ public export
CoproductIsAlgebra : IsAlgebra sig x -> IsAlgebra sig y
-> IsAlgebra sig (Coproduct x y)
CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra
- { relation =
- (~=~)
- (MkRawSetoidAlgebra x xIsAlgebra.relation)
- (MkRawSetoidAlgebra y yIsAlgebra.relation)
- , equivalence = \t => MkEquivalence
- { refl = MkReflexive $ coprodRelRefl
- (\t => (xIsAlgebra.equivalence t).refl)
- (\t => (yIsAlgebra.equivalence t).refl)
- _
- , sym = MkSymmetric $ Sym
- , trans = MkTransitive $ Trans
+ { equivalence = MkIndexedEquivalence
+ { relation =
+ (~=~)
+ (MkRawSetoidAlgebra x xIsAlgebra.equivalence.relation)
+ (MkRawSetoidAlgebra y yIsAlgebra.equivalence.relation)
+ , reflexive = \_ =>
+ coprodRelRefl
+ xIsAlgebra.equivalence.reflexive
+ yIsAlgebra.equivalence.reflexive
+ , symmetric = \_, _, _ => Sym
+ , transitive = \_, _, _, _ => Trans
}
, semCong = Call
}
@@ -98,87 +97,84 @@ CoproductAlgebra x y = MkAlgebra (Coproduct x.raw y.raw) $ CoproductIsAlgebra x.
public export
injectLHomo : x ~> CoproductAlgebra x y
injectLHomo = MkHomomorphism
- { func = \_ => Done . Left
- , cong = \_ => DoneL
+ { func = MkIndexedSetoidHomomorphism (\_ => Done . Left) (\_, _, _ => DoneL)
, semHomo = InjectL
}
public export
injectRHomo : y ~> CoproductAlgebra x y
injectRHomo = MkHomomorphism
- { func = \_ => Done . Right
- , cong = \_ => DoneR
+ { func = MkIndexedSetoidHomomorphism (\_ => Done . Right) (\_, _, _ => DoneR)
, semHomo = InjectR
}
public export
-coproduct : {z : RawAlgebra sig} -> IFunc x z.U -> IFunc y z.U -> IFunc (CoproductSet sig x y) z.U
+coproduct : {z : RawAlgebra sig}
+ -> (f : (t : sig.T) -> x t -> z.U t) -> (g : (t : sig.T) -> y t -> z.U t)
+ -> (t : sig.T) -> CoproductSet sig x y t -> z.U t
coproduct f g _ = bindTerm (\i => either (f i) (g i))
public export
-coproducts : {z : RawAlgebra sig} -> IFunc x z.U -> IFunc y z.U -> (ts : _)
- -> CoproductSet sig x y ^ ts -> z.U ^ ts
+coproducts : {z : RawAlgebra sig}
+ -> (f : (t : sig.T) -> x t -> z.U t) -> (g : (t : sig.T) -> y t -> z.U t)
+ -> (ts : List sig.T) -> CoproductSet sig x y ^ ts -> z.U ^ ts
coproducts f g _ = bindTerms (\i => either (f i) (g i))
public export
coproductCong : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
- -> (t : sig.T) -> {tm, tm' : _} -> (~=~) x.rawSetoid y.rawSetoid t tm tm'
- -> (z.relation t `on` coproduct {z = z.raw} f.func g.func t) tm tm'
+ -> {t : sig.T} -> {tm, tm' : _} -> (~=~) x.rawSetoid y.rawSetoid t tm tm'
+ -> (z.relation t `on` coproduct {z = z.raw} f.func.H g.func.H t) tm tm'
public export
coproductsCong : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
- -> (ts : List sig.T) -> {tms, tms' : _ ^ ts}
+ -> {ts : List sig.T} -> {tms, tms' : _ ^ ts}
-> Pointwise ((~=~) x.rawSetoid y.rawSetoid) tms tms'
- -> (Pointwise z.relation `on` (coproducts {z = z.raw} f.func g.func ts)) tms tms'
-
-coproductCong f g _ (DoneL eq) = f.cong _ eq
-coproductCong f g _ (DoneR eq) = g.cong _ eq
-coproductCong f g _ (Call op eqs) =
- z.algebra.semCong op $
- coproductsCong f g _ eqs
-coproductCong f g _ (InjectL op ts) = CalcWith (z.setoid.index _) $
- |~ f.func _ (x.raw.sem op ts)
- ~~ z.raw.sem op (map f.func ts) ...(f.semHomo op ts)
- ~~ z.raw.sem op (map (coproduct f.func g.func) (map (\_ => Done . Left) ts)) .=.(cong (z.raw.sem op) $ mapComp ts)
- ~~ z.raw.sem op (coproducts f.func g.func _ (map (\_ => Done . Left) ts)) .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _)
-coproductCong f g _ (InjectR op ts) = CalcWith (z.setoid.index _) $
- |~ g.func _ (y.raw.sem op ts)
- ~~ z.raw.sem op (map g.func ts) ...(g.semHomo op ts)
- ~~ z.raw.sem op (map (coproduct f.func g.func) (map (\_ => Done . Right) ts)) .=.(cong (z.raw.sem op) $ mapComp ts)
- ~~ z.raw.sem op (coproducts f.func g.func _ (map (\_ => Done . Right) ts)) .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _)
-coproductCong f g _ (Sym eq) = (z.algebra.equivalence _).symmetric $ coproductCong f g _ eq
-coproductCong f g _ (Trans eq eq') = (z.algebra.equivalence _).transitive
- (coproductCong f g _ eq)
- (coproductCong f g _ eq')
-
-coproductsCong f g _ [] = []
-coproductsCong f g _ (eq :: eqs) =
- coproductCong f g _ eq :: coproductsCong f g _ eqs
+ -> (Pointwise z.relation `on` (coproducts {z = z.raw} f.func.H g.func.H ts)) tms tms'
+
+coproductCong f g (DoneL eq) = f.func.homomorphic _ _ _ eq
+coproductCong f g (DoneR eq) = g.func.homomorphic _ _ _ eq
+coproductCong f g (Call op eqs) = z.algebra.semCong op $ coproductsCong f g eqs
+coproductCong f g (InjectL op ts) = CalcWith (index z.setoid _) $
+ |~ f.func.H _ (x.raw.sem op ts)
+ ~~ z.raw.sem op (map f.func.H ts) ...(f.semHomo op ts)
+ ~~ z.raw.sem op (map (coproduct f.func.H g.func.H) (map (\_ => Done . Left) ts)) .=.(cong (z.raw.sem op) $ mapComp ts)
+ ~~ z.raw.sem op (coproducts f.func.H g.func.H _ (map (\_ => Done . Left) ts)) .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _)
+coproductCong f g (InjectR op ts) = CalcWith (index z.setoid _) $
+ |~ g.func.H _ (y.raw.sem op ts)
+ ~~ z.raw.sem op (map g.func.H ts) ...(g.semHomo op ts)
+ ~~ z.raw.sem op (map (coproduct f.func.H g.func.H) (map (\_ => Done . Right) ts)) .=.(cong (z.raw.sem op) $ mapComp ts)
+ ~~ z.raw.sem op (coproducts f.func.H g.func.H _ (map (\_ => Done . Right) ts)) .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _)
+coproductCong f g (Sym eq) = z.algebra.equivalence.symmetric _ _ _ $ coproductCong f g eq
+coproductCong f g (Trans eq eq') = z.algebra.equivalence.transitive _ _ _ _
+ (coproductCong f g eq)
+ (coproductCong f g eq')
+
+coproductsCong f g [] = []
+coproductsCong f g (eq :: eqs) = coproductCong f g eq :: coproductsCong f g eqs
public export
coproductHomo : {x, y, z : Algebra sig} -> x ~> z -> y ~> z
-> CoproductAlgebra x y ~> z
coproductHomo f g = MkHomomorphism
- { func = coproduct {z = z.raw} f.func g.func
- , cong = coproductCong f g
+ { func = MkIndexedSetoidHomomorphism
+ { H = coproduct {z = z.raw} f.func.H g.func.H
+ , homomorphic = \_, _, _ => coproductCong f g
+ }
, semHomo = \op, tms =>
- (z.algebra.equivalence _).equalImpliesEq $
+ reflect (index z.setoid _) $
cong (z.raw.sem op) $
bindTermsIsMap {a = z.raw} _ tms
}
public export
termToCoproduct : (x, y : Algebra sig)
- -> FreeAlgebra (fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i))) ~>
+ -> FreeAlgebra (bundle (\t => Either (index x.setoid t) (index y.setoid t))) ~>
CoproductAlgebra x y
termToCoproduct x y = MkHomomorphism
- { func = \_ => id
- , cong = \t => tmRelImpliesCoprodRel
+ { func = MkIndexedSetoidHomomorphism (\_ => id) (\t, _, _ => tmRelImpliesCoprodRel)
, semHomo = \op, tms =>
Call op $
- coprodsRelReflexive
- (\i => (x.algebra.equivalence i).refl)
- (\i => (y.algebra.equivalence i).refl) $
+ reflect (index (pwSetoid (CoproductAlgebra x y).setoid) _) $
sym $
mapId tms
}
@@ -188,13 +184,13 @@ coproductUnique' : {x, y, z : Algebra sig}
-> (f : CoproductAlgebra x y ~> z)
-> (g : CoproductAlgebra x y ~> z)
-> (congL : {t : sig.T} -> (i : x.raw.U t)
- -> z.relation t (f.func t (Done (Left i))) (g.func t (Done (Left i))))
+ -> z.relation t (f.func.H t (Done (Left i))) (g.func.H t (Done (Left i))))
-> (congR : {t : sig.T} -> (i : y.raw.U t)
- -> z.relation t (f.func t (Done (Right i))) (g.func t (Done (Right i))))
+ -> z.relation t (f.func.H t (Done (Right i))) (g.func.H t (Done (Right i))))
-> {t : sig.T} -> (tm : _)
- -> z.relation t (f.func t tm) (g.func t tm)
+ -> z.relation t (f.func.H t tm) (g.func.H t tm)
coproductUnique' f g congL congR tm = bindUnique'
- { v = fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i))
+ { v = bundle (\t => Either (index x.setoid t) (index y.setoid t))
, f = f . termToCoproduct x y
, g = g . termToCoproduct x y
, cong = \x => case x of
@@ -207,9 +203,9 @@ public export
coproductUnique : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
-> (h : CoproductAlgebra x y ~> z)
-> (congL : {t : sig.T} -> (i : x.raw.U t)
- -> z.relation t (h.func t (Done (Left i))) (f.func t i))
+ -> z.relation t (h.func.H t (Done (Left i))) (f.func.H t i))
-> (congR : {t : sig.T} -> (i : y.raw.U t)
- -> z.relation t (h.func t (Done (Right i))) (g.func t i))
+ -> z.relation t (h.func.H t (Done (Right i))) (g.func.H t i))
-> {t : sig.T} -> (tm : _)
- -> z.relation t (h.func t tm) (coproduct {z = z.raw} f.func g.func t tm)
+ -> z.relation t (h.func.H t tm) (coproduct {z = z.raw} f.func.H g.func.H t tm)
coproductUnique f g h = coproductUnique' h (coproductHomo f g)
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index f9f0879..69bdcfc 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -1,11 +1,11 @@
module Soat.FirstOrder.Term
-import Data.Morphism.Indexed
import Data.Setoid.Indexed
import Soat.Data.Product
import Soat.FirstOrder.Algebra
import Soat.FirstOrder.Signature
+
import Syntax.PreorderReasoning.Setoid
%default total
@@ -16,10 +16,12 @@ data Term : (0 sig : Signature) -> (0 _ : sig.T -> Type) -> sig.T -> Type where
Call : (op : Op sig t) -> (ts : Term sig v ^ op.arity) -> Term sig v t
public export
-bindTerm : {auto a : RawAlgebra sig} -> IFunc v a.U -> {t : _} -> Term sig v t -> a.U t
+bindTerm : {auto a : RawAlgebra sig} -> ((t : sig.T) -> v t -> a.U t)
+ -> {t : _} -> Term sig v t -> a.U t
public export
-bindTerms : {auto a : RawAlgebra sig} -> IFunc v a.U -> {ts : _} -> Term sig v ^ ts -> a.U ^ ts
+bindTerms : {auto a : RawAlgebra sig} -> ((t : sig.T) -> v t -> a.U t)
+ -> {ts : _} -> Term sig v ^ ts -> a.U ^ ts
bindTerm env (Done i) = env _ i
bindTerm {a = a} env (Call op ts) = a.sem op (bindTerms env ts)
@@ -29,197 +31,178 @@ bindTerms env (t :: ts) = bindTerm env t :: bindTerms env ts
public export
bindTermsIsMap : {auto a : RawAlgebra sig}
- -> (env : IFunc v a.U) -> {ts : _} -> (tms : Term sig v ^ ts)
+ -> (env : (t : sig.T) -> v t -> a.U t) -> {ts : _} -> (tms : Term sig v ^ ts)
-> bindTerms (\tm => env tm) tms = map (\t => bindTerm (\tm => env tm)) tms
bindTermsIsMap env [] = Refl
bindTermsIsMap env (t :: ts) = cong ((::) (bindTerm env t)) (bindTermsIsMap env ts)
--- FIXME: these names shouldn't be public. Indication of bad API design
namespace Rel
public export
- data (~=~) : forall v . (0 r : IRel v) -> IRel (Term sig v)
+ data (~=~) : forall v . (0 r : (t : sig.T) -> Rel (v t)) -> (t : sig.T) -> Rel (Term sig v t)
where
- Done' : {0 v : sig.T -> Type} -> {0 r : IRel v}
+ Done : {0 v : sig.T -> Type} -> {0 r : (t : sig.T) -> Rel (v t)}
-> {t : sig.T} -> {i, j : v t}
-> r t i j
-> (~=~) {sig} {v} r t (Done i) (Done j)
- Call' : {0 v : sig.T -> Type} -> {0 r : IRel v}
+ Call : {0 v : sig.T -> Type} -> {0 r : (t : sig.T) -> Rel (v t)}
-> {t : sig.T} -> (op : Op sig t) -> {tms, tms' : Term sig v ^ op.arity}
-> Pointwise ((~=~) {sig} {v} r) tms tms'
-> (~=~) {sig} {v} r t (Call op tms) (Call op tms')
- public export
- tmRelEqualIsEqual : (~=~) (\_ => Equal) t tm tm' -> tm = tm'
-
- public export
- tmsRelEqualIsEqual : Pointwise ((~=~) (\_ => Equal)) tms tms' -> tms = tms'
-
- tmRelEqualIsEqual (Done' eq) = cong Done eq
- tmRelEqualIsEqual (Call' op eqs) = cong (Call op) $ tmsRelEqualIsEqual eqs
-
- tmsRelEqualIsEqual [] = Refl
- tmsRelEqualIsEqual (eq :: eqs) = cong2 (::) (tmRelEqualIsEqual eq) (tmsRelEqualIsEqual eqs)
-
- public export
- tmRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
+ tmRelRefl : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+ -> (refl : (t : sig.T) -> (x : V t) -> rel t x x)
-> {t : sig.T} -> (tm : Term sig V t) -> (~=~) rel t tm tm
- public export
- tmsRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
+ tmsRelRefl : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+ -> (refl : (t : sig.T) -> (x : V t) -> rel t x x)
-> {ts : List sig.T} -> (tms : Term sig V ^ ts) -> Pointwise ((~=~) rel) tms tms
- tmRelRefl refl (Done i) = Done' reflexive
- tmRelRefl refl (Call op ts) = Call' op (tmsRelRefl refl ts)
+ tmRelRefl refl (Done i) = Done (refl _ i)
+ tmRelRefl refl (Call op ts) = Call op (tmsRelRefl refl ts)
tmsRelRefl refl [] = []
tmsRelRefl refl (t :: ts) = tmRelRefl refl t :: tmsRelRefl refl ts
- public export
- tmRelReflexive : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
- -> {t : sig.T} -> {tm, tm' : Term sig V t} -> tm = tm' -> (~=~) rel t tm tm'
- tmRelReflexive refl Refl = tmRelRefl refl _
-
- public export
- tmsRelReflexive : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
- -> {ts : List sig.T} -> {tms, tms' : Term sig V ^ ts}
- -> tms = tms' -> Pointwise ((~=~) rel) tms tms'
- tmsRelReflexive refl Refl = tmsRelRefl refl _
-
- public export
- tmRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel)
+ tmRelSym : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+ -> (sym : (t : sig.T) -> (x, y : V t) -> rel t x y -> rel t y x)
-> {t : sig.T} -> {tm, tm' : Term sig V t} -> (~=~) rel t tm tm' -> (~=~) rel t tm' tm
- public export
- tmsRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel)
+ tmsRelSym : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+ -> (sym : (t : sig.T) -> (x, y : V t) -> rel t x y -> rel t y x)
-> {ts : List sig.T} -> {tms, tms' : Term sig V ^ ts}
-> Pointwise ((~=~) rel) tms tms' -> Pointwise ((~=~) rel) tms' tms
- tmRelSym sym (Done' i) = Done' (symmetric i)
- tmRelSym sym (Call' op ts) = Call' op (tmsRelSym sym ts)
+ tmRelSym sym (Done i) = Done (sym _ _ _ i)
+ tmRelSym sym (Call op ts) = Call op (tmsRelSym sym ts)
tmsRelSym sym [] = []
tmsRelSym sym (t :: ts) = tmRelSym sym t :: tmsRelSym sym ts
- public export
- tmRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel)
+ tmRelTrans : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+ -> (trans : (t : sig.T) -> (x, y, z : V t) -> rel t x y -> rel t y z -> rel t x z)
-> {t : sig.T} -> {tm, tm', tm'' : Term sig V t}
-> (~=~) rel t tm tm' -> (~=~) rel t tm' tm'' -> (~=~) rel t tm tm''
- public export
- tmsRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel)
+ tmsRelTrans : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+ -> (trans : (t : sig.T) -> (x, y, z : V t) -> rel t x y -> rel t y z -> rel t x z)
-> {ts : List sig.T} -> {tms, tms', tms'' : Term sig V ^ ts}
-> Pointwise ((~=~) rel) tms tms' -> Pointwise ((~=~) rel) tms' tms''
-> Pointwise ((~=~) rel) tms tms''
- tmRelTrans trans (Done' i) (Done' j) = Done' (transitive i j)
- tmRelTrans trans (Call' op ts) (Call' _ ts') = Call' op (tmsRelTrans trans ts ts')
+ tmRelTrans trans (Done i) (Done j) = Done (trans _ _ _ _ i j)
+ tmRelTrans trans (Call op ts) (Call _ ts') = Call op (tmsRelTrans trans ts ts')
tmsRelTrans trans [] [] = []
tmsRelTrans trans (t :: ts) (t' :: ts') = tmRelTrans trans t t' :: tmsRelTrans trans ts ts'
- export
- tmRelEq : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IEquivalence V rel
- -> IEquivalence _ ((~=~) {sig = sig} {v = V} rel)
- tmRelEq eq t = MkEquivalence
- (MkReflexive $ tmRelRefl (\t => (eq t).refl) _)
- (MkSymmetric $ tmRelSym (\t => (eq t).sym))
- (MkTransitive $ tmRelTrans (\t => (eq t).trans))
+ public export
+ tmRelEq : IndexedEquivalence sig.T v -> IndexedEquivalence sig.T (Term sig v)
+ tmRelEq eq = MkIndexedEquivalence
+ { relation = (~=~) eq.relation
+ , reflexive = \t => tmRelRefl eq.reflexive
+ , symmetric = \t, x, y => tmRelSym eq.symmetric
+ , transitive = \t, x, y, z => tmRelTrans eq.transitive
+ }
public export
Free : (0 V : sig.T -> Type) -> RawAlgebra sig
Free v = MkRawAlgebra (Term sig v) Call
public export
-FreeIsAlgebra : (v : ISetoid sig.T) -> IsAlgebra sig (Free v.U)
-FreeIsAlgebra v = MkIsAlgebra ((~=~) v.relation) (tmRelEq v.equivalence) Call'
+FreeIsAlgebra : (v : IndexedSetoid sig.T) -> IsAlgebra sig (Free v.U)
+FreeIsAlgebra v = MkIsAlgebra (tmRelEq v.equivalence) Call
public export
-FreeAlgebra : ISetoid sig.T -> Algebra sig
+FreeAlgebra : IndexedSetoid sig.T -> Algebra sig
FreeAlgebra v = MkAlgebra _ (FreeIsAlgebra v)
public export
-bindTermCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v}
+bindTermCong' : {a : Algebra sig} -> {env, env' : (t : sig.T) -> v t -> a.raw.U t}
+ -> {0 rel : (t : sig.T) -> Rel (v t)}
-> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.relation t (env t x) (env' t y))
- -> {t : sig.T} -> {tm, tm' : Term sig v t} -> (~=~) rel t tm tm'
+ -> {t : sig.T} -> {tm, tm' : Term sig v t} -> (eq : (~=~) rel t tm tm')
-> a.relation t (bindTerm {a = a.raw} env tm) (bindTerm {a = a.raw} env' tm')
public export
-bindTermsCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v}
+bindTermsCong' : {a : Algebra sig} -> {env, env' : (t : sig.T) -> v t -> a.raw.U t}
+ -> {0 rel : (t : sig.T) -> Rel (v t)}
-> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.relation t (env t x) (env' t y))
- -> {ts : List sig.T} -> {tms, tms' : Term sig v ^ ts} -> Pointwise ((~=~) rel) tms tms'
+ -> {ts : List sig.T} -> {tms, tms' : Term sig v ^ ts} -> (eqs : Pointwise ((~=~) rel) tms tms')
-> Pointwise a.relation (bindTerms {a = a.raw} env tms) (bindTerms {a = a.raw} env' tms')
-bindTermCong' cong (Done' i) = cong _ i
-bindTermCong' {a = a} cong (Call' op ts) = a.algebra.semCong op (bindTermsCong' cong ts)
+bindTermCong' cong (Done i) = cong _ i
+bindTermCong' {a = a} cong (Call op ts) = a.algebra.semCong op (bindTermsCong' cong ts)
bindTermsCong' cong [] = []
bindTermsCong' cong (t :: ts) = bindTermCong' cong t :: bindTermsCong' cong ts
public export
-bindTermCong : {a : Algebra sig} -> (env : IFunction v a.setoid)
- -> {t : sig.T} -> {tm, tm' : Term sig v.U t} -> (~=~) v.relation t tm tm'
- -> a.relation t (bindTerm {a = a.raw} env.func tm) (bindTerm {a = a.raw} env.func tm')
-bindTermCong env = bindTermCong' env.cong
+bindTermCong : {a : Algebra sig} -> (env : v ~> a.setoid)
+ -> {t : sig.T} -> {tm, tm' : Term sig v.U t} -> (eq : (~=~) v.equivalence.relation t tm tm')
+ -> a.relation t (bindTerm {a = a.raw} env.H tm) (bindTerm {a = a.raw} env.H tm')
+bindTermCong env = bindTermCong' env.homomorphic
public export
-bindTermsCong : {a : Algebra sig} -> (env : IFunction v a.setoid)
- -> {ts : List sig.T} -> {tms, tms' : Term sig v.U ^ ts} -> Pointwise ((~=~) v.relation) tms tms'
- -> Pointwise a.relation
- (bindTerms {a = a.raw} env.func tms)
- (bindTerms {a = a.raw} env.func tms')
-bindTermsCong env = bindTermsCong' env.cong
+bindTermsCong : {a : Algebra sig} -> (env : v ~> a.setoid)
+ -> {ts : List sig.T} -> {tms, tms' : Term sig v.U ^ ts}
+ -> (eqs : Pointwise ((~=~) v.equivalence.relation) tms tms')
+ -> Pointwise a.relation (bindTerms {a = a.raw} env.H tms) (bindTerms {a = a.raw} env.H tms')
+bindTermsCong env = bindTermsCong' env.homomorphic
public export
-bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> FreeAlgebra v ~> a
+bindHomo : {a : Algebra sig} -> (env : v ~> a.setoid) -> FreeAlgebra v ~> a
bindHomo env = MkHomomorphism
- { func = \_ => bindTerm {a = a.raw} env.func
- , cong = \_ => bindTermCong env
+ { func = MkIndexedSetoidHomomorphism
+ { H = \_ => bindTerm {a = a.raw} env.H
+ , homomorphic = \_, _, _ => bindTermCong env
+ }
, semHomo = \op, tms =>
a.algebra.semCong op $
- map (\t => (a.algebra.equivalence t).equalImpliesEq) $
- equalImpliesPwEq $
- bindTermsIsMap {a = a.raw} env.func tms
+ reflect (index (pwSetoid a.setoid) _) $
+ bindTermsIsMap {a = a.raw} env.H tms
}
public export
-bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
+bindUnique' : {v : IndexedSetoid sig.T} -> {a : Algebra sig}
-> (f, g : FreeAlgebra v ~> a)
- -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i)))
+ -> (cong : {t : sig.T} -> (i : v.U t)
+ -> a.relation t (f.func.H t (Done i)) (g.func.H t (Done i)))
-> {t : sig.T} -> (tm : Term sig v.U t)
- -> a.relation t (f.func t tm) (g.func t tm)
+ -> a.relation t (f.func.H t tm) (g.func.H t tm)
public export
-bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
+bindsUnique' : {v : IndexedSetoid sig.T} -> {a : Algebra sig}
-> (f, g : FreeAlgebra v ~> a)
- -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i)))
+ -> (cong : {t : sig.T} -> (i : v.U t)
+ -> a.relation t (f.func.H t (Done i)) (g.func.H t (Done i)))
-> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
- -> Pointwise a.relation (map f.func tms) (map g.func tms)
+ -> Pointwise a.relation (map f.func.H tms) (map g.func.H tms)
bindUnique' f g cong (Done i) = cong i
-bindUnique' f g cong (Call op ts) = CalcWith (a.setoid.index _) $
- |~ f.func _ (Call op ts)
- ~~ a.raw.sem op (map f.func ts) ...( f.semHomo op ts )
- ~~ a.raw.sem op (map g.func ts) ...( a.algebra.semCong op $ bindsUnique' f g cong ts )
- ~~ g.func _ (Call op ts) ..<( g.semHomo op ts )
+bindUnique' f g cong (Call op ts) = CalcWith (index a.setoid _) $
+ |~ f.func.H _ (Call op ts)
+ ~~ a.raw.sem op (map f.func.H ts) ...( f.semHomo op ts )
+ ~~ a.raw.sem op (map g.func.H ts) ...( a.algebra.semCong op $ bindsUnique' f g cong ts )
+ ~~ g.func.H _ (Call op ts) ..<( g.semHomo op ts )
bindsUnique' f g cong [] = []
bindsUnique' f g cong (t :: ts) = bindUnique' f g cong t :: bindsUnique' f g cong ts
public export
-bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
+bindUnique : {v : IndexedSetoid sig.T} -> {a : Algebra sig} -> (env : v ~> a.setoid)
-> (f : FreeAlgebra v ~> a)
- -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i))
+ -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func.H t (Done i)) (env.H t i))
-> {t : sig.T} -> (tm : Term sig v.U t)
- -> a.relation t (f.func t tm) (bindTerm {a = a.raw} env.func tm)
+ -> a.relation t (f.func.H t tm) (bindTerm {a = a.raw} env.H tm)
bindUnique env f = bindUnique' f (bindHomo env)
public export
-bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
+bindsUnique : {v : IndexedSetoid sig.T} -> {a : Algebra sig} -> (env : v ~> a.setoid)
-> (f : FreeAlgebra v ~> a)
- -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i))
+ -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func.H t (Done i)) (env.H t i))
-> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
- -> Pointwise a.relation (map f.func tms) (bindTerms {a = a.raw} env.func tms)
-bindsUnique env f cong ts = CalcWith (pwSetoid a.setoid _) $
- |~ map f.func ts
- ~~ map (\_ => bindTerm {a = a.raw} env.func) ts ...( bindsUnique' f (bindHomo env) cong ts )
- ~~ bindTerms {a = a.raw} env.func ts .=<( bindTermsIsMap {a = a.raw} env.func ts )
+ -> Pointwise a.relation (map f.func.H tms) (bindTerms {a = a.raw} env.H tms)
+bindsUnique env f cong ts = CalcWith (index (pwSetoid a.setoid) _) $
+ |~ map f.func.H ts
+ ~~ map (\_ => bindTerm {a = a.raw} env.H) ts ...( bindsUnique' f (bindHomo env) cong ts )
+ ~~ bindTerms {a = a.raw} env.H ts .=<( bindTermsIsMap {a = a.raw} env.H ts )
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 12:27:52 +0000