diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 27 |
1 files changed, 20 insertions, 7 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index 5935254..7c2fca1 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -108,21 +108,34 @@ FreeAlgebra : ISetoid 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} + -> (cong : (t : sig.T) -> {x, y : v t} -> rel t x y -> a.rel 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') + +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)) + -> {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') + +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.rel 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') - -bindTermCong env (Done' i) = env.cong _ i -bindTermCong {a = a} env (Call' op ts) = a.algebra.semCong op (bindTermsCong env ts) - -bindTermsCong env [] = [] -bindTermsCong env {tms = (_ :: _)} {tms' = (_ :: _)} (t :: ts) = - bindTermCong env t :: bindTermsCong env ts +bindTermsCong env = bindTermsCong' env.cong public export bindHomo : (a : Algebra sig) -> (env : IFunction v a.setoid) |