summaryrefslogtreecommitdiff
path: root/src/Soat
diff options
context:
space:
mode:
Diffstat (limited to 'src/Soat')
-rw-r--r--src/Soat/FirstOrder/Algebra.idr13
-rw-r--r--src/Soat/FirstOrder/Term.idr30
-rw-r--r--src/Soat/SecondOrder/Algebra.idr18
3 files changed, 32 insertions, 29 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 5f166d5..bbc0430 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -37,13 +37,13 @@ record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel a.U) w
public export
record Algebra (0 sig : Signature) where
constructor MkAlgebra
- raw : RawAlgebra sig
- 0 rel : IRel raw.U
- algebra : IsAlgebra sig raw rel
+ raw : RawAlgebra sig
+ 0 relation : IRel raw.U
+ algebra : IsAlgebra sig raw relation
public export
(.setoid) : Algebra sig -> ISetoid sig.T
-(.setoid) a = MkISetoid a.raw.U a.rel a.algebra.equivalence
+(.setoid) a = MkISetoid a.raw.U a.relation a.algebra.equivalence
public export
record IsHomomorphism
@@ -51,9 +51,10 @@ record IsHomomorphism
(f : (t : sig.T) -> a.raw.U t -> b.raw.U t)
where
constructor MkIsHomomorphism
- cong : (t : sig.T) -> {tm, tm' : a.raw.U t} -> a.rel t tm tm' -> b.rel t (f t tm) (f t tm')
+ cong : (t : sig.T) -> {tm, tm' : a.raw.U t}
+ -> a.relation t tm tm' -> b.relation t (f t tm) (f t tm')
semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
- -> b.rel t (f t (a.raw.sem op tms)) (b.raw.sem op (map f tms))
+ -> b.relation t (f t (a.raw.sem op tms)) (b.raw.sem op (map f tms))
public export
record Homomorphism {0 sig : Signature} (a, b : Algebra sig)
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 701d3d6..92f35cc 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -109,15 +109,15 @@ FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v)
public export
bindTermCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v}
- -> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.rel t (env t x) (env' t y))
+ -> (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'
- -> a.rel t (bindTerm {a = a.raw} env tm) (bindTerm {a = a.raw} env' 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}
- -> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.rel t (env t x) (env' t y))
+ -> (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'
- -> Pointwise a.rel (bindTerms {a = a.raw} env tms) (bindTerms {a = a.raw} env' 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)
@@ -128,13 +128,15 @@ 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.rel t (bindTerm {a = a.raw} env.func tm) (bindTerm {a = a.raw} env.func tm')
+ -> a.relation t (bindTerm {a = a.raw} env.func tm) (bindTerm {a = a.raw} env.func tm')
bindTermCong env = bindTermCong' env.cong
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.rel (bindTerms {a = a.raw} env.func tms) (bindTerms {a = a.raw} env.func tms')
+ -> Pointwise a.relation
+ (bindTerms {a = a.raw} env.func tms)
+ (bindTerms {a = a.raw} env.func tms')
bindTermsCong env = bindTermsCong' env.cong
public export
@@ -155,16 +157,16 @@ bindHomo env = MkHomomorphism _ (bindIsHomo _ env)
public export
bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
-> (f, g : Homomorphism (FreeAlgebra v) a)
- -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (g.f t (Done i)))
+ -> ({t : sig.T} -> (i : v.U t) -> a.relation t (f.f t (Done i)) (g.f t (Done i)))
-> {t : sig.T} -> (tm : Term sig v.U t)
- -> a.rel t (f.f t tm) (g.f t tm)
+ -> a.relation t (f.f t tm) (g.f t tm)
public export
bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
-> (f, g : Homomorphism (FreeAlgebra v) a)
- -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (g.f t (Done i)))
+ -> ({t : sig.T} -> (i : v.U t) -> a.relation t (f.f t (Done i)) (g.f t (Done i)))
-> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
- -> Pointwise a.rel (map f.f tms) (map g.f tms)
+ -> Pointwise a.relation (map f.f tms) (map g.f tms)
bindUnique' f g cong (Done i) = cong i
bindUnique' f g cong (Call op ts) =
@@ -181,17 +183,17 @@ bindsUnique' f g cong (t :: ts) = bindUnique' f g cong t :: bindsUnique' f g con
public export
bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
-> (f : Homomorphism (FreeAlgebra v) a)
- -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.func t i))
+ -> ({t : sig.T} -> (i : v.U t) -> a.relation t (f.f t (Done i)) (env.func t i))
-> {t : sig.T} -> (tm : Term sig v.U t)
- -> a.rel t (f.f t tm) (bindTerm {a = a.raw} env.func tm)
+ -> a.relation t (f.f t tm) (bindTerm {a = a.raw} env.func tm)
bindUnique env f = bindUnique' f (bindHomo env)
public export
bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
-> (f : Homomorphism (FreeAlgebra v) a)
- -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.func t i))
+ -> ({t : sig.T} -> (i : v.U t) -> a.relation t (f.f t (Done i)) (env.func t i))
-> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
- -> Pointwise a.rel (map f.f tms) (bindTerms {a = a.raw} env.func tms)
+ -> Pointwise a.relation (map f.f tms) (bindTerms {a = a.raw} env.func tms)
bindsUnique env f cong ts =
pwTrans (\i => (a.algebra.equivalence i).trans)
(bindsUnique' f (bindHomo env) cong ts) $
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index bc3defb..57b8a51 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -103,13 +103,13 @@ record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncur
public export
record Algebra (0 sig : Signature) where
constructor MkAlgebra
- raw : RawAlgebra sig
- 0 rel : IRel (uncurry raw.U)
- algebra : IsAlgebra sig raw rel
+ raw : RawAlgebra sig
+ 0 relation : IRel (uncurry raw.U)
+ algebra : IsAlgebra sig raw relation
public export
(.setoid) : Algebra sig -> ISetoid (Pair sig.T (List sig.T))
-(.setoid) a = MkISetoid (uncurry a.raw.U) a.rel a.algebra.equivalence
+(.setoid) a = MkISetoid (uncurry a.raw.U) a.relation a.algebra.equivalence
public export
record IsHomomorphism
@@ -118,19 +118,19 @@ record IsHomomorphism
where
constructor MkIsHomomorphism
cong : (t : sig.T) -> (ctx : List sig.T) -> {tm, tm' : a.raw.U t ctx}
- -> a.rel (t, ctx) tm tm' -> b.rel (t, ctx) (f t ctx tm) (f t ctx tm')
+ -> a.relation (t, ctx) tm tm' -> b.relation (t, ctx) (f t ctx tm) (f t ctx tm')
renameHomo : (t : sig.T) -> forall ctx, ctx' . (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx)
- -> b.rel (t, ctx') (f t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ f t ctx tm)
+ -> b.relation (t, ctx') (f t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ f t ctx tm)
semHomo : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
-> (tms : extend a.raw.U ctx ^ op.arity)
- -> b.rel (t, ctx)
+ -> 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)
varHomo : forall t, ctx . (i : Elem t ctx)
- -> b.rel (t, ctx) (f t ctx $ a.raw.var i) (b.raw.var i)
+ -> b.relation (t, ctx) (f t ctx $ a.raw.var i) (b.raw.var i)
substHomo : (t : sig.T) -> (ctx : List sig.T) -> forall ctx' . (tm : a.raw.U t ctx')
-> (tms : flip a.raw.U ctx ^ ctx')
- -> b.rel (t, ctx)
+ -> b.relation (t, ctx)
(f t ctx $ a.raw.subst t ctx tm tms)
(b.raw.subst t ctx (f t ctx' tm) $ map (\t => f t ctx) tms)
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 23:47:43 +0000