diff options
Diffstat (limited to 'src/Soat/FirstOrder/Term.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 30 |
1 files changed, 16 insertions, 14 deletions
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) $ |