summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Soat/FirstOrder/Algebra.idr8
-rw-r--r--src/Soat/FirstOrder/Term.idr12
-rw-r--r--src/Soat/Relation.idr6
-rw-r--r--src/Soat/SecondOrder/Algebra.idr38
4 files changed, 32 insertions, 32 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index fef5871..5f166d5 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -30,8 +30,8 @@ MkRawAlgebra u sem = MakeRawAlgebra u (\o => uncurry (sem o))
public export
record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel a.U) where
constructor MkIsAlgebra
- 0 equivalence : IEquivalence a.U rel
- 0 semCong : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity}
+ equivalence : IEquivalence a.U rel
+ semCong : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity}
-> Pointwise rel tms tms' -> rel t (a.sem op tms) (a.sem op tms')
public export
@@ -51,8 +51,8 @@ record IsHomomorphism
(f : (t : sig.T) -> a.raw.U t -> b.raw.U t)
where
constructor MkIsHomomorphism
- 0 cong : (t : sig.T) -> {tm, tm' : a.raw.U t} -> a.rel t tm tm' -> b.rel t (f t tm) (f t tm')
- 0 semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
+ cong : (t : sig.T) -> {tm, tm' : a.raw.U t} -> a.rel t tm tm' -> b.rel 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))
public export
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 5f5e57b..af6539b 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -116,12 +116,12 @@ public export
FreeAlgebra : ISetoid sig.T -> Algebra sig
FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v)
-public export 0
+public export
bindTermCong : {a : Algebra sig} -> (env : SetoidEnvironment x a.setoid)
-> {t : sig.T} -> {tm, tm' : Term sig x.U t} -> (~=~) x.relation t tm tm'
-> a.rel t (bindTerm {a = a.raw} env.f tm) (bindTerm {a = a.raw} env.f tm')
-public export 0
+public export
bindTermsCong : {a : Algebra sig} -> (env : SetoidEnvironment x a.setoid)
-> {ts : List sig.T} -> {tms, tms' : Term sig x.U ^ ts} -> Pointwise ((~=~) x.relation) tms tms'
-> Pointwise a.rel (bindTerms {a = a.raw} env.f tms) (bindTerms {a = a.raw} env.f tms')
@@ -148,15 +148,15 @@ public export
bind : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) -> Homomorphism (FreeAlgebra v) a
bind env = MkHomomorphism _ (bindHomo _ env)
-public export 0
-bindUnique : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid)
+public export
+bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid)
-> (f : Homomorphism (FreeAlgebra v) a)
-> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.f t i))
-> {t : sig.T} -> (tm : Term sig v.U t)
-> a.rel t (f.f t tm) ((Term.bind {a = a} env).f t tm)
-public export 0
-bindsUnique : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid)
+public export
+bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid)
-> (f : Homomorphism (FreeAlgebra v) a)
-> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.f t i))
-> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
diff --git a/src/Soat/Relation.idr b/src/Soat/Relation.idr
index bf5a631..9a394c2 100644
--- a/src/Soat/Relation.idr
+++ b/src/Soat/Relation.idr
@@ -70,6 +70,6 @@ IEquivalence x rel = (i : a) -> Soat.Relation.Equivalence (x i) (rel i)
public export
record ISetoid (a : Type) where
constructor MkISetoid
- 0 U : a -> Type
- 0 relation : IRel U
- 0 equivalence : IEquivalence U relation
+ 0 U : a -> Type
+ 0 relation : IRel U
+ equivalence : IEquivalence U relation
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 3ce1726..bc3defb 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -34,28 +34,28 @@ record RawAlgebra (0 sig : Signature) where
public export
record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncurry a.U)) where
constructor MkIsAlgebra
- 0 equivalence : IEquivalence (uncurry a.U) rel
+ equivalence : IEquivalence (uncurry a.U) rel
-- Congruences
- 0 renameCong : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx')
+ renameCong : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx')
-> {tm, tm' : a.U t ctx} -> rel (t, ctx) tm tm'
-> rel (t, ctx') (a.rename t f tm) (a.rename t f tm')
- 0 semCong : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
+ 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} rel ctx) tms tms'
-> rel (t, ctx) (a.sem ctx op tms) (a.sem ctx op tms')
- 0 substCong : (t : sig.T) -> (ctx : List sig.T)
+ substCong : (t : sig.T) -> (ctx : List sig.T)
-> forall ctx' . {tm, tm' : a.U t ctx'} -> rel (t, ctx') tm tm'
-> {tms, tms' : flip a.U ctx ^ ctx'} -> Pointwise (\t => rel (t, ctx)) tms tms'
-> rel (t, ctx) (a.subst t ctx tm tms) (a.subst t ctx tm' tms')
-- rename is functorial
- 0 renameId : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx)
+ renameId : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx)
-> rel (t, ctx) (a.rename t {ctx = ctx} Relation.reflexive tm) tm
- 0 renameComp : (t : sig.T)
+ renameComp : (t : sig.T)
-> forall ctx, ctx', ctx'' . (f : ctx' `Sublist` ctx'') -> (g : ctx `Sublist` ctx')
-> (tm : a.U t ctx)
-> rel (t, ctx'') (a.rename t (transitive g f) tm) (a.rename t f $ a.rename t g tm)
-- sem are natural transformation
- 0 semNat : forall ctx, ctx' . (f : ctx `Sublist` ctx') -> {t : sig.T} -> (op : Op sig t)
+ semNat : forall ctx, ctx' . (f : ctx `Sublist` ctx') -> {t : sig.T} -> (op : Op sig t)
-> (tms : extend a.U ctx ^ op.arity)
-> rel (t, ctx')
(a.rename t f $ a.sem ctx op tms)
@@ -63,33 +63,33 @@ record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel (uncur
map (\ty => a.rename (snd ty) (Relation.reflexive {x = fst ty} ++ f)) $
tms)
-- var is natural transformation
- 0 varNat : forall t, ctx, ctx' . (f : ctx `Sublist` ctx') -> (i : Elem t ctx)
+ varNat : forall t, ctx, ctx' . (f : ctx `Sublist` ctx') -> (i : Elem t ctx)
-> rel (t, ctx') (a.rename t f $ a.var i) (a.var $ curry f i)
-- subst is natural transformation
- 0 substNat : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx')
+ substNat : (t : sig.T) -> forall ctx, ctx' . (f : ctx `Sublist` ctx')
-> forall ctx'' . (tm : a.U t ctx'') -> (tms : flip a.U ctx ^ ctx'')
-> rel (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
- 0 substExnat : (t : sig.T) -> (ctx : List sig.T)
+ substExnat : (t : sig.T) -> (ctx : List sig.T)
-> forall ctx', ctx'' . (f : ctx' `Sublist` ctx'')
-> (tm : a.U t ctx') -> (tms : flip a.U ctx ^ ctx'')
-> rel (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
- 0 substComm : (t : sig.T) -> (ctx : List sig.T)
+ substComm : (t : sig.T) -> (ctx : List sig.T)
-> forall ctx', ctx'' . (tm : a.U t ctx'')
-> (tms : flip a.U ctx' ^ ctx'') -> (tms' : flip a.U ctx ^ ctx')
-> rel (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)
- 0 substVarL : forall t . (ctx : List sig.T) -> forall ctx' . (i : Elem t ctx')
+ substVarL : forall t . (ctx : List sig.T) -> forall ctx' . (i : Elem t ctx')
-> (tms : flip a.U ctx ^ ctx')
-> rel (t, ctx) (a.subst t ctx (a.var i) tms) (index tms i)
- 0 substVarR : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx)
+ substVarR : (t : sig.T) -> (ctx : List sig.T) -> (tm : a.U t ctx)
-> rel (t, ctx) (a.subst t ctx {ctx' = ctx} tm $ tabulate a.var) tm
-- sem, var and subst are compatible
- 0 substCompat : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
+ substCompat : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
-> forall ctx' . (tms : extend a.U ctx' ^ op.arity) -> (tms' : flip a.U ctx ^ ctx')
-> rel (t, ctx)
(a.subst t ctx (a.sem ctx' op tms) tms')
@@ -117,18 +117,18 @@ record IsHomomorphism
(f : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx)
where
constructor MkIsHomomorphism
- 0 cong : (t : sig.T) -> (ctx : List sig.T) -> {tm, tm' : a.raw.U t ctx}
+ 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')
- 0 renameHomo : (t : sig.T) -> forall ctx, ctx' . (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx)
+ 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)
- 0 semHomo : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
+ semHomo : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
-> (tms : extend a.raw.U ctx ^ op.arity)
-> b.rel (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)
- 0 varHomo : forall t, ctx . (i : Elem t ctx)
+ varHomo : forall t, ctx . (i : Elem t ctx)
-> b.rel (t, ctx) (f t ctx $ a.raw.var i) (b.raw.var i)
- 0 substHomo : (t : sig.T) -> (ctx : List sig.T) -> forall ctx' . (tm : a.raw.U t ctx')
+ 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)
(f t ctx $ a.raw.subst t ctx tm tms)
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 14:45:00 +0000