summaryrefslogtreecommitdiff
path: root/src/Soat/FirstOrder/Term.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Soat/FirstOrder/Term.idr')
-rw-r--r--src/Soat/FirstOrder/Term.idr118
1 files changed, 78 insertions, 40 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 4a51f94..dc0c182 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -15,25 +15,6 @@ data Term : (0 sig : Signature) -> (0 _ : sig.T -> Type) -> sig.T -> Type where
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 v a.U -> {t : _} -> Term sig v t -> a.U t
-
-public export
-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)
-
-bindTerms env [] = []
-bindTerms env (t :: ts) = bindTerm env t :: bindTerms env ts
-
-public export
-bindTermsIsMap : {auto a : RawAlgebra sig}
- -> (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)
-
-- FIXME: these names shouldn't be public. Indication of bad API design
namespace Rel
public export
@@ -138,42 +119,85 @@ FreeAlgebra : ISetoid sig.T -> Algebra sig
FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v)
public export
+inject : IFunc v (Term sig v)
+inject _ = Done
+
+public export
+injectFunc : IFunction v (FreeAlgebra v).setoid
+injectFunc = MkIFunction (\_ => Done) (\_ => Done')
+
+public export
+bindTerm : {auto a : RawAlgebra sig} -> IFunc v a.U -> IFunc (Term sig v) a.U
+
+public export
+bindTerms : {auto a : RawAlgebra sig} -> IFunc v a.U -> IFunc ((^) (Term sig v)) ((^) a.U)
+
+bindTerm env _ (Done i) = env _ i
+bindTerm env _ (Call op ts) = a.sem op (bindTerms env _ ts)
+
+bindTerms env _ [] = []
+bindTerms env _ (t :: ts) = bindTerm env _ t :: bindTerms env _ ts
+
+public export
+free : IFunc v u -> IFunc (Term sig v) (Term sig u)
+free f = bindTerm {a = Free u} (\i => inject i . f i)
+
+public export
+bindTermsIsMap : {a : RawAlgebra sig}
+ -> (env : IFunc v a.U) -> {ts : _} -> (tms : Term sig v ^ ts)
+ -> bindTerms (\tm => env tm) _ tms = map (bindTerm (\tm => env tm)) tms
+bindTermsIsMap env [] = Refl
+bindTermsIsMap env (t :: ts) = cong ((::) (bindTerm env _ t)) (bindTermsIsMap env ts)
+
+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.relation t (env t x) (env' t y))
- -> {t : sig.T} -> {tm, tm' : Term sig v t} -> (~=~) rel t tm tm'
- -> a.relation t (bindTerm {a = a.raw} env tm) (bindTerm {a = a.raw} env' tm')
+ -> (t : sig.T) -> {tm, tm' : Term sig v t} -> (~=~) rel t tm tm'
+ -> a.relation t (bindTerm {a = a.raw} env t tm) (bindTerm {a = a.raw} env' t 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.relation t (env t x) (env' t y))
- -> {ts : List sig.T} -> {tms, tms' : Term sig v ^ ts} -> Pointwise ((~=~) rel) tms tms'
- -> Pointwise a.relation (bindTerms {a = a.raw} env tms) (bindTerms {a = a.raw} env' tms')
+ -> (ts : List sig.T) -> {tms, tms' : Term sig v ^ ts} -> Pointwise ((~=~) rel) tms 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)
+bindTermCong' cong _ (Done' i) = cong _ i
+bindTermCong' cong _ (Call' op ts) = a.algebra.semCong op (bindTermsCong' cong _ ts)
-bindTermsCong' cong [] = []
-bindTermsCong' cong (t :: ts) = bindTermCong' cong t :: bindTermsCong' cong ts
+bindTermsCong' cong _ [] = []
+bindTermsCong' cong _ (t :: ts) = bindTermCong' cong _ t :: bindTermsCong' cong _ ts
+
+public export
+freeCong' : {u : ISetoid sig.T} -> {f, g : IFunc v u.U} -> {0 rel : IRel v}
+ -> (cong : (t : sig.T) -> {i, j : v t} -> rel t i j -> u.relation t (f t i) (g t j))
+ -> (t : sig.T) -> {tm, tm' : Term sig v t}
+ -> (~=~) rel t tm tm' -> (~=~) u.relation t (free f t tm) (free g t tm')
+freeCong' cong = bindTermCong' {a = FreeAlgebra u} (\i => Done' . cong i)
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.relation t (bindTerm {a = a.raw} env.func tm) (bindTerm {a = a.raw} env.func tm')
+ -> (t : sig.T) -> {tm, tm' : Term sig v.U t} -> (~=~) v.relation t tm tm'
+ -> a.relation t (bindTerm {a = a.raw} env.func t tm) (bindTerm {a = a.raw} env.func t 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'
+ -> (ts : List sig.T) -> {tms, tms' : Term sig v.U ^ ts} -> Pointwise ((~=~) v.relation) tms tms'
-> Pointwise a.relation
- (bindTerms {a = a.raw} env.func tms)
- (bindTerms {a = a.raw} env.func tms')
+ (bindTerms {a = a.raw} env.func ts tms)
+ (bindTerms {a = a.raw} env.func ts tms')
bindTermsCong env = bindTermsCong' env.cong
public export
+freeCong : {u : ISetoid sig.T} -> (f : IFunction v u) -> (t : sig.T) -> {tm, tm' : Term sig v.U t}
+ -> (~=~) v.relation t tm tm' -> (~=~) u.relation t (free f.func t tm) (free f.func t tm')
+freeCong f = freeCong' f.cong
+
+public export
bindIsHomo : (a : Algebra sig) -> (env : IFunction v a.setoid)
- -> IsHomomorphism (FreeAlgebra v) a (\t => bindTerm {a = a.raw} env.func)
+ -> IsHomomorphism (FreeAlgebra v) a (bindTerm {a = a.raw} env.func)
bindIsHomo a env = MkIsHomomorphism
- (\t, eq => bindTermCong env eq)
+ (bindTermCong env)
(\op, tms =>
a.algebra.semCong op $
map (\t => (a.algebra.equivalence t).equalImpliesEq) $
@@ -185,14 +209,19 @@ bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> Homomorphism (Fr
bindHomo env = MkHomomorphism _ (bindIsHomo _ env)
public export
-bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
+freeHomo : {u : ISetoid sig.T} -> IFunction v u
+ -> Homomorphism {sig = sig} (FreeAlgebra v) (FreeAlgebra u)
+freeHomo f = bindHomo $ compFunc injectFunc f
+
+public export
+bindUnique' : {0 v : ISetoid sig.T} -> {a : Algebra sig}
-> (f, g : Homomorphism (FreeAlgebra v) a)
-> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i)))
-> {t : sig.T} -> (tm : Term sig v.U t)
-> a.relation t (f.func t tm) (g.func t tm)
public export
-bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
+bindsUnique' : {0 v : ISetoid sig.T} -> {a : Algebra sig}
-> (f, g : Homomorphism (FreeAlgebra v) a)
-> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i)))
-> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
@@ -213,7 +242,7 @@ bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.se
-> (f : Homomorphism (FreeAlgebra v) a)
-> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i))
-> {t : sig.T} -> (tm : Term sig v.U t)
- -> a.relation t (f.func t tm) (bindTerm {a = a.raw} env.func tm)
+ -> a.relation t (f.func t tm) (bindTerm {a = a.raw} env.func t tm)
bindUnique env f = bindUnique' f (bindHomo env)
public export
@@ -221,8 +250,17 @@ bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.s
-> (f : Homomorphism (FreeAlgebra v) a)
-> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i))
-> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
- -> Pointwise a.relation (map f.func tms) (bindTerms {a = a.raw} env.func tms)
+ -> Pointwise a.relation (map f.func tms) (bindTerms {a = a.raw} env.func ts tms)
bindsUnique env f cong ts = CalcWith (pwSetoid a.setoid _) $
|~ map f.func ts
- ~~ map (\_ => bindTerm {a = a.raw} env.func) ts ...( bindsUnique' f (bindHomo env) cong ts )
- ~~ bindTerms {a = a.raw} env.func ts .=<( bindTermsIsMap {a = a.raw} env.func ts )
+ ~~ map (bindTerm {a = a.raw} env.func) ts ...( bindsUnique' f (bindHomo env) cong ts )
+ ~~ bindTerms {a = a.raw} env.func _ ts .=<( bindTermsIsMap {a = a.raw} env.func ts )
+
+public export
+freeUnique : {v, u : ISetoid sig.T} -> (f : IFunction v u)
+ -> (g : Homomorphism (FreeAlgebra v) (FreeAlgebra u))
+ -> (cong : {t : sig.T} -> (i : v.U t)
+ -> (FreeAlgebra u).relation t (g.func t (Done i)) (Done (f.func t i)))
+ -> {t : sig.T} -> (tm : Term sig v.U t)
+ -> (FreeAlgebra u).relation t (g.func t tm) (free f.func t tm)
+freeUnique f = bindUnique $ compFunc injectFunc f
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 21:24:28 +0000