diff options
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 39 |
1 files changed, 16 insertions, 23 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index af6539b..ff0796c 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -15,20 +15,13 @@ data Term : (0 sig : Signature) -> (0 _ : sig.T -> Type) -> sig.T -> Type where Done : (i : x t) -> Term sig x t Call : (op : Op sig t) -> (ts : Term sig x ^ op.arity) -> Term sig x t -Environment : {a : Type} -> (x, y : a -> Type) -> Type -Environment {a} x y = (t : a) -> x t -> y t - -record SetoidEnvironment {a : Type} (x, y : ISetoid a) where - f : Environment {a} x.U y.U - cong : (t : a) -> {u, v : x.U t} -> x.relation t u v -> y.relation t (f t u) (f t v) - public export bindTerm : {auto a : RawAlgebra sig} - -> Environment x a.U -> {t : _} -> Term sig x t -> a.U t + -> IFunc x a.U -> {t : _} -> Term sig x t -> a.U t public export bindTerms : {auto a : RawAlgebra sig} - -> Environment x a.U -> {ts : _} -> Term sig x ^ ts -> a.U ^ ts + -> IFunc x a.U -> {ts : _} -> Term sig x ^ ts -> a.U ^ ts bindTerm env (Done i) = env _ i bindTerm {a = a} env (Call op ts) = a.sem op (bindTerms env ts) @@ -38,7 +31,7 @@ bindTerms env (t :: ts) = bindTerm env t :: bindTerms env ts public export bindTermsIsMap : {auto a : RawAlgebra sig} - -> (env : Environment x a.U) -> {ts : _} -> (tms : Term sig x ^ ts) + -> (env : IFunc x a.U) -> {ts : _} -> (tms : Term sig x ^ 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) @@ -117,14 +110,14 @@ FreeAlgebra : ISetoid sig.T -> Algebra sig FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v) public export -bindTermCong : {a : Algebra sig} -> (env : SetoidEnvironment x a.setoid) +bindTermCong : {a : Algebra sig} -> (env : IFunction 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') + -> a.rel t (bindTerm {a = a.raw} env.func tm) (bindTerm {a = a.raw} env.func tm') public export -bindTermsCong : {a : Algebra sig} -> (env : SetoidEnvironment x a.setoid) +bindTermsCong : {a : Algebra sig} -> (env : IFunction 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') + -> 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) @@ -134,33 +127,33 @@ bindTermsCong env {tms = (_ :: _)} {tms' = (_ :: _)} (t :: ts) = bindTermCong env t :: bindTermsCong env ts public export -bindHomo : (a : Algebra sig) -> (env : SetoidEnvironment v a.setoid) - -> IsHomomorphism (FreeAlgebra v) a (\t => bindTerm {a = a.raw} env.f) +bindHomo : (a : Algebra sig) -> (env : IFunction v a.setoid) + -> IsHomomorphism (FreeAlgebra v) a (\t => bindTerm {a = a.raw} env.func) bindHomo a env = MkIsHomomorphism (\t, eq => bindTermCong env eq) (\op, tms => a.algebra.semCong op $ map (\t => (a.algebra.equivalence t).equalImpliesEq) $ equalImpliesPwEq $ - bindTermsIsMap {a = a.raw} env.f tms) + bindTermsIsMap {a = a.raw} env.func tms) public export -bind : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) -> Homomorphism (FreeAlgebra v) a +bind : {a : Algebra sig} -> (env : IFunction v a.setoid) -> Homomorphism (FreeAlgebra v) a bind env = MkHomomorphism _ (bindHomo _ env) public export -bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) +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.f t i)) + -> ({t : sig.T} -> (i : v.U t) -> a.rel 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) ((Term.bind {a = a} env).f t tm) public export -bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) +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.f t i)) + -> ({t : sig.T} -> (i : v.U t) -> a.rel 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.f tms) + -> Pointwise a.rel (map f.f tms) (bindTerms {a = a.raw} env.func tms) bindUnique env f fDone (Done i) = fDone i bindUnique env f fDone (Call op ts) = (a.algebra.equivalence _).transitive |