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.idr187
1 files changed, 85 insertions, 102 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index f9f0879..69bdcfc 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -1,11 +1,11 @@
module Soat.FirstOrder.Term
-import Data.Morphism.Indexed
import Data.Setoid.Indexed
import Soat.Data.Product
import Soat.FirstOrder.Algebra
import Soat.FirstOrder.Signature
+
import Syntax.PreorderReasoning.Setoid
%default total
@@ -16,10 +16,12 @@ data Term : (0 sig : Signature) -> (0 _ : sig.T -> Type) -> sig.T -> Type where
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
+bindTerm : {auto a : RawAlgebra sig} -> ((t : sig.T) -> v t -> a.U t)
+ -> {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
+bindTerms : {auto a : RawAlgebra sig} -> ((t : sig.T) -> v t -> a.U t)
+ -> {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)
@@ -29,197 +31,178 @@ 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)
+ -> (env : (t : sig.T) -> v t -> a.U t) -> {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
- data (~=~) : forall v . (0 r : IRel v) -> IRel (Term sig v)
+ data (~=~) : forall v . (0 r : (t : sig.T) -> Rel (v t)) -> (t : sig.T) -> Rel (Term sig v t)
where
- Done' : {0 v : sig.T -> Type} -> {0 r : IRel v}
+ Done : {0 v : sig.T -> Type} -> {0 r : (t : sig.T) -> Rel (v t)}
-> {t : sig.T} -> {i, j : v t}
-> r t i j
-> (~=~) {sig} {v} r t (Done i) (Done j)
- Call' : {0 v : sig.T -> Type} -> {0 r : IRel v}
+ Call : {0 v : sig.T -> Type} -> {0 r : (t : sig.T) -> Rel (v t)}
-> {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')
- public export
- tmRelEqualIsEqual : (~=~) (\_ => Equal) t tm tm' -> tm = tm'
-
- public export
- tmsRelEqualIsEqual : Pointwise ((~=~) (\_ => Equal)) tms tms' -> tms = tms'
-
- tmRelEqualIsEqual (Done' eq) = cong Done eq
- tmRelEqualIsEqual (Call' op eqs) = cong (Call op) $ tmsRelEqualIsEqual eqs
-
- tmsRelEqualIsEqual [] = Refl
- tmsRelEqualIsEqual (eq :: eqs) = cong2 (::) (tmRelEqualIsEqual eq) (tmsRelEqualIsEqual eqs)
-
- public export
- tmRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
+ tmRelRefl : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+ -> (refl : (t : sig.T) -> (x : V t) -> rel t x x)
-> {t : sig.T} -> (tm : Term sig V t) -> (~=~) rel t tm tm
- public export
- tmsRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
+ tmsRelRefl : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+ -> (refl : (t : sig.T) -> (x : V t) -> rel t x x)
-> {ts : List sig.T} -> (tms : Term sig V ^ ts) -> Pointwise ((~=~) rel) tms tms
- tmRelRefl refl (Done i) = Done' reflexive
- tmRelRefl refl (Call op ts) = Call' op (tmsRelRefl refl ts)
+ tmRelRefl refl (Done i) = Done (refl _ i)
+ tmRelRefl refl (Call op ts) = Call op (tmsRelRefl refl ts)
tmsRelRefl refl [] = []
tmsRelRefl refl (t :: ts) = tmRelRefl refl t :: tmsRelRefl refl ts
- public export
- tmRelReflexive : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
- -> {t : sig.T} -> {tm, tm' : Term sig V t} -> tm = tm' -> (~=~) rel t tm tm'
- tmRelReflexive refl Refl = tmRelRefl refl _
-
- public export
- tmsRelReflexive : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
- -> {ts : List sig.T} -> {tms, tms' : Term sig V ^ ts}
- -> tms = tms' -> Pointwise ((~=~) rel) tms tms'
- tmsRelReflexive refl Refl = tmsRelRefl refl _
-
- public export
- tmRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel)
+ tmRelSym : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+ -> (sym : (t : sig.T) -> (x, y : V t) -> rel t x y -> rel t y x)
-> {t : sig.T} -> {tm, tm' : Term sig V t} -> (~=~) rel t tm tm' -> (~=~) rel t tm' tm
- public export
- tmsRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel)
+ tmsRelSym : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+ -> (sym : (t : sig.T) -> (x, y : V t) -> rel t x y -> rel t y x)
-> {ts : List sig.T} -> {tms, tms' : Term sig V ^ ts}
-> Pointwise ((~=~) rel) tms tms' -> Pointwise ((~=~) rel) tms' tms
- tmRelSym sym (Done' i) = Done' (symmetric i)
- tmRelSym sym (Call' op ts) = Call' op (tmsRelSym sym ts)
+ tmRelSym sym (Done i) = Done (sym _ _ _ i)
+ tmRelSym sym (Call op ts) = Call op (tmsRelSym sym ts)
tmsRelSym sym [] = []
tmsRelSym sym (t :: ts) = tmRelSym sym t :: tmsRelSym sym ts
- public export
- tmRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel)
+ tmRelTrans : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+ -> (trans : (t : sig.T) -> (x, y, z : V t) -> rel t x y -> rel t y z -> rel t x z)
-> {t : sig.T} -> {tm, tm', tm'' : Term sig V t}
-> (~=~) rel t tm tm' -> (~=~) rel t tm' tm'' -> (~=~) rel t tm tm''
- public export
- tmsRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel)
+ tmsRelTrans : {0 V : sig.T -> Type} -> {0 rel : (t : sig.T) -> Rel (V t)}
+ -> (trans : (t : sig.T) -> (x, y, z : V t) -> rel t x y -> rel t y z -> rel t x z)
-> {ts : List sig.T} -> {tms, tms', tms'' : Term sig V ^ ts}
-> Pointwise ((~=~) rel) tms tms' -> Pointwise ((~=~) rel) tms' tms''
-> Pointwise ((~=~) rel) tms tms''
- tmRelTrans trans (Done' i) (Done' j) = Done' (transitive i j)
- tmRelTrans trans (Call' op ts) (Call' _ ts') = Call' op (tmsRelTrans trans ts ts')
+ tmRelTrans trans (Done i) (Done j) = Done (trans _ _ _ _ i j)
+ tmRelTrans trans (Call op ts) (Call _ ts') = Call op (tmsRelTrans trans ts ts')
tmsRelTrans trans [] [] = []
tmsRelTrans trans (t :: ts) (t' :: ts') = tmRelTrans trans t t' :: tmsRelTrans trans ts ts'
- export
- tmRelEq : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IEquivalence V rel
- -> IEquivalence _ ((~=~) {sig = sig} {v = V} rel)
- tmRelEq eq t = MkEquivalence
- (MkReflexive $ tmRelRefl (\t => (eq t).refl) _)
- (MkSymmetric $ tmRelSym (\t => (eq t).sym))
- (MkTransitive $ tmRelTrans (\t => (eq t).trans))
+ public export
+ tmRelEq : IndexedEquivalence sig.T v -> IndexedEquivalence sig.T (Term sig v)
+ tmRelEq eq = MkIndexedEquivalence
+ { relation = (~=~) eq.relation
+ , reflexive = \t => tmRelRefl eq.reflexive
+ , symmetric = \t, x, y => tmRelSym eq.symmetric
+ , transitive = \t, x, y, z => tmRelTrans eq.transitive
+ }
public export
Free : (0 V : sig.T -> Type) -> RawAlgebra sig
Free v = MkRawAlgebra (Term sig v) Call
public export
-FreeIsAlgebra : (v : ISetoid sig.T) -> IsAlgebra sig (Free v.U)
-FreeIsAlgebra v = MkIsAlgebra ((~=~) v.relation) (tmRelEq v.equivalence) Call'
+FreeIsAlgebra : (v : IndexedSetoid sig.T) -> IsAlgebra sig (Free v.U)
+FreeIsAlgebra v = MkIsAlgebra (tmRelEq v.equivalence) Call
public export
-FreeAlgebra : ISetoid sig.T -> Algebra sig
+FreeAlgebra : IndexedSetoid 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}
+bindTermCong' : {a : Algebra sig} -> {env, env' : (t : sig.T) -> v t -> a.raw.U t}
+ -> {0 rel : (t : sig.T) -> Rel (v t)}
-> (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'
+ -> {t : sig.T} -> {tm, tm' : Term sig v t} -> (eq : (~=~) rel t tm 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}
+bindTermsCong' : {a : Algebra sig} -> {env, env' : (t : sig.T) -> v t -> a.raw.U t}
+ -> {0 rel : (t : sig.T) -> Rel (v t)}
-> (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'
+ -> {ts : List sig.T} -> {tms, tms' : Term sig v ^ ts} -> (eqs : 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' {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.relation t (bindTerm {a = a.raw} env.func tm) (bindTerm {a = a.raw} env.func tm')
-bindTermCong env = bindTermCong' env.cong
+bindTermCong : {a : Algebra sig} -> (env : v ~> a.setoid)
+ -> {t : sig.T} -> {tm, tm' : Term sig v.U t} -> (eq : (~=~) v.equivalence.relation t tm tm')
+ -> a.relation t (bindTerm {a = a.raw} env.H tm) (bindTerm {a = a.raw} env.H tm')
+bindTermCong env = bindTermCong' env.homomorphic
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.relation
- (bindTerms {a = a.raw} env.func tms)
- (bindTerms {a = a.raw} env.func tms')
-bindTermsCong env = bindTermsCong' env.cong
+bindTermsCong : {a : Algebra sig} -> (env : v ~> a.setoid)
+ -> {ts : List sig.T} -> {tms, tms' : Term sig v.U ^ ts}
+ -> (eqs : Pointwise ((~=~) v.equivalence.relation) tms tms')
+ -> Pointwise a.relation (bindTerms {a = a.raw} env.H tms) (bindTerms {a = a.raw} env.H tms')
+bindTermsCong env = bindTermsCong' env.homomorphic
public export
-bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> FreeAlgebra v ~> a
+bindHomo : {a : Algebra sig} -> (env : v ~> a.setoid) -> FreeAlgebra v ~> a
bindHomo env = MkHomomorphism
- { func = \_ => bindTerm {a = a.raw} env.func
- , cong = \_ => bindTermCong env
+ { func = MkIndexedSetoidHomomorphism
+ { H = \_ => bindTerm {a = a.raw} env.H
+ , homomorphic = \_, _, _ => bindTermCong env
+ }
, semHomo = \op, tms =>
a.algebra.semCong op $
- map (\t => (a.algebra.equivalence t).equalImpliesEq) $
- equalImpliesPwEq $
- bindTermsIsMap {a = a.raw} env.func tms
+ reflect (index (pwSetoid a.setoid) _) $
+ bindTermsIsMap {a = a.raw} env.H tms
}
public export
-bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
+bindUnique' : {v : IndexedSetoid sig.T} -> {a : Algebra sig}
-> (f, g : FreeAlgebra v ~> a)
- -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i)))
+ -> (cong : {t : sig.T} -> (i : v.U t)
+ -> a.relation t (f.func.H t (Done i)) (g.func.H t (Done i)))
-> {t : sig.T} -> (tm : Term sig v.U t)
- -> a.relation t (f.func t tm) (g.func t tm)
+ -> a.relation t (f.func.H t tm) (g.func.H t tm)
public export
-bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
+bindsUnique' : {v : IndexedSetoid sig.T} -> {a : Algebra sig}
-> (f, g : FreeAlgebra v ~> a)
- -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i)))
+ -> (cong : {t : sig.T} -> (i : v.U t)
+ -> a.relation t (f.func.H t (Done i)) (g.func.H t (Done i)))
-> {ts : List sig.T} -> (tms : Term sig v.U ^ ts)
- -> Pointwise a.relation (map f.func tms) (map g.func tms)
+ -> Pointwise a.relation (map f.func.H tms) (map g.func.H tms)
bindUnique' f g cong (Done i) = cong i
-bindUnique' f g cong (Call op ts) = CalcWith (a.setoid.index _) $
- |~ f.func _ (Call op ts)
- ~~ a.raw.sem op (map f.func ts) ...( f.semHomo op ts )
- ~~ a.raw.sem op (map g.func ts) ...( a.algebra.semCong op $ bindsUnique' f g cong ts )
- ~~ g.func _ (Call op ts) ..<( g.semHomo op ts )
+bindUnique' f g cong (Call op ts) = CalcWith (index a.setoid _) $
+ |~ f.func.H _ (Call op ts)
+ ~~ a.raw.sem op (map f.func.H ts) ...( f.semHomo op ts )
+ ~~ a.raw.sem op (map g.func.H ts) ...( a.algebra.semCong op $ bindsUnique' f g cong ts )
+ ~~ g.func.H _ (Call op ts) ..<( g.semHomo op ts )
bindsUnique' f g cong [] = []
bindsUnique' f g cong (t :: ts) = bindUnique' f g cong t :: bindsUnique' f g cong ts
public export
-bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
+bindUnique : {v : IndexedSetoid sig.T} -> {a : Algebra sig} -> (env : v ~> a.setoid)
-> (f : FreeAlgebra v ~> a)
- -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i))
+ -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func.H t (Done i)) (env.H 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.H t tm) (bindTerm {a = a.raw} env.H tm)
bindUnique env f = bindUnique' f (bindHomo env)
public export
-bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid)
+bindsUnique : {v : IndexedSetoid sig.T} -> {a : Algebra sig} -> (env : v ~> a.setoid)
-> (f : FreeAlgebra v ~> a)
- -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i))
+ -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func.H t (Done i)) (env.H 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)
-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 )
+ -> Pointwise a.relation (map f.func.H tms) (bindTerms {a = a.raw} env.H tms)
+bindsUnique env f cong ts = CalcWith (index (pwSetoid a.setoid) _) $
+ |~ map f.func.H ts
+ ~~ map (\_ => bindTerm {a = a.raw} env.H) ts ...( bindsUnique' f (bindHomo env) cong ts )
+ ~~ bindTerms {a = a.raw} env.H ts .=<( bindTermsIsMap {a = a.raw} env.H ts )
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 21:55:38 +0000