diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 38 |
1 files changed, 18 insertions, 20 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index ff0796c..5935254 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -12,16 +12,14 @@ import Soat.Relation public export 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 + Done : (i : v t) -> Term sig v t + Call : (op : Op sig t) -> (ts : Term sig v ^ op.arity) -> Term sig v t public export -bindTerm : {auto a : RawAlgebra sig} - -> IFunc x a.U -> {t : _} -> Term sig x t -> a.U t +bindTerm : {auto a : RawAlgebra sig} -> IFunc v a.U -> {t : _} -> Term sig v t -> a.U t public export -bindTerms : {auto a : RawAlgebra sig} - -> IFunc x a.U -> {ts : _} -> Term sig x ^ ts -> a.U ^ ts +bindTerms : {auto a : RawAlgebra sig} -> IFunc v a.U -> {ts : _} -> Term sig v ^ ts -> a.U ^ ts bindTerm env (Done i) = env _ i bindTerm {a = a} env (Call op ts) = a.sem op (bindTerms env ts) @@ -31,23 +29,23 @@ bindTerms env (t :: ts) = bindTerm env t :: bindTerms env ts public export bindTermsIsMap : {auto a : RawAlgebra sig} - -> (env : IFunc x a.U) -> {ts : _} -> (tms : Term sig x ^ ts) + -> (env : IFunc v a.U) -> {ts : _} -> (tms : Term sig v ^ 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) namespace Rel public export - data (~=~) : forall x . (0 r : IRel x) -> IRel (Term sig x) + data (~=~) : forall v . (0 r : IRel v) -> IRel (Term sig v) where - Done' : {0 x : sig.T -> Type} -> {0 r : IRel x} - -> {t : sig.T} -> {i, j : x t} + Done' : {0 v : sig.T -> Type} -> {0 r : IRel v} + -> {t : sig.T} -> {i, j : v t} -> r t i j - -> (~=~) {sig = sig} {x = x} r t (Done i) (Done j) - Call' : {0 x : sig.T -> Type} -> {0 r : IRel x} - -> {t : sig.T} -> (op : Op sig t) -> {tms, tms' : Term sig x ^ op.arity} - -> Pointwise ((~=~) {sig = sig} {x = x} r) tms tms' - -> (~=~) {sig = sig} {x = x} r t (Call op tms) (Call op tms') + -> (~=~) {sig} {v} r t (Done i) (Done j) + Call' : {0 v : sig.T -> Type} -> {0 r : IRel v} + -> {t : sig.T} -> (op : Op sig t) -> {tms, tms' : Term sig v ^ op.arity} + -> Pointwise ((~=~) {sig} {v} r) tms tms' + -> (~=~) {sig} {v} r t (Call op tms) (Call op tms') tmRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel -> {t : sig.T} -> (tm : Term sig V t) -> (~=~) rel t tm tm @@ -91,7 +89,7 @@ namespace Rel export tmRelEq : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IEquivalence V rel - -> IEquivalence _ ((~=~) {sig = sig} {x = V} rel) + -> IEquivalence _ ((~=~) {sig = sig} {v = V} rel) tmRelEq eq t = MkEquivalence (MkReflexive $ tmRelRefl (\t => (eq t).refl) _) (MkSymmetric $ tmRelSym (\t => (eq t).sym)) @@ -110,13 +108,13 @@ FreeAlgebra : ISetoid sig.T -> Algebra sig FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v) public export -bindTermCong : {a : Algebra sig} -> (env : IFunction x a.setoid) - -> {t : sig.T} -> {tm, tm' : Term sig x.U t} -> (~=~) x.relation t tm tm' +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') public export -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' +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 |