diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-05 15:48:09 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-05 15:48:09 +0000 |
| commit | 2301a52aaad73e2f70aba46682ec69686f35aa6c (patch) | |
| tree | 8cd61f69f4e249a5a7306e11520affe84a961599 /src/Soat/FirstOrder/Term.idr | |
| parent | 8e103a340a6c7d2751c0297ad4f01cd5c5a7da47 (diff) | |
Inline definition of IsHomomorphism.
Diffstat (limited to 'src/Soat/FirstOrder/Term.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 25 |
1 files changed, 11 insertions, 14 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index bedfe3f..f9f0879 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -170,19 +170,16 @@ bindTermsCong : {a : Algebra sig} -> (env : IFunction v a.setoid) bindTermsCong env = bindTermsCong' env.cong public export -bindIsHomo : (a : Algebra sig) -> (env : IFunction v a.setoid) - -> IsHomomorphism (FreeAlgebra v) a (\t => bindTerm {a = a.raw} env.func) -bindIsHomo 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.func tms) - -public export bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> FreeAlgebra v ~> a -bindHomo env = MkHomomorphism _ (bindIsHomo _ env) +bindHomo env = MkHomomorphism + { func = \_ => bindTerm {a = a.raw} env.func + , cong = \_ => bindTermCong env + , semHomo = \op, tms => + a.algebra.semCong op $ + map (\t => (a.algebra.equivalence t).equalImpliesEq) $ + equalImpliesPwEq $ + bindTermsIsMap {a = a.raw} env.func tms + } public export bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig} @@ -201,9 +198,9 @@ bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig} 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.homo.semHomo 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.homo.semHomo op ts ) + ~~ g.func _ (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 |