1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
|
module Soat.FirstOrder.Term
import Control.Relation
import Soat.Data.Product
import Soat.FirstOrder.Algebra
import Soat.FirstOrder.Signature
import Soat.Relation
%default total
%hide Control.Relation.Equivalence
public export
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)
namespace Rel
public export
data (~=~) : forall v . (0 r : IRel v) -> IRel (Term sig v)
where
Done' : {0 v : sig.T -> Type} -> {0 r : IRel v}
-> {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}
-> {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
tmsRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
-> {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)
tmsRelRefl refl [] = []
tmsRelRefl refl (t :: ts) = tmRelRefl refl t :: tmsRelRefl refl ts
tmRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel)
-> {t : sig.T} -> {tm, tm' : Term sig V t} -> (~=~) rel t tm tm' -> (~=~) rel t tm' tm
tmsRelSym : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ISymmetric V rel)
-> {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)
tmsRelSym sym [] = []
tmsRelSym sym (t :: ts) = tmRelSym sym t :: tmsRelSym sym ts
tmRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel)
-> {t : sig.T} -> {tm, tm', tm'' : Term sig V t}
-> (~=~) rel t tm tm' -> (~=~) rel t tm' tm'' -> (~=~) rel t tm tm''
tmsRelTrans : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> (ITransitive V rel)
-> {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')
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
Free : (0 V : sig.T -> Type) -> RawAlgebra sig
Free v = MakeRawAlgebra (Term sig v) Call
public export
FreeIsAlgebra : (v : ISetoid sig.T) -> IsAlgebra sig (Free v.U) ((~=~) v.relation)
FreeIsAlgebra v = MkIsAlgebra (tmRelEq v.equivalence) Call'
public export
FreeAlgebra : ISetoid sig.T -> Algebra sig
FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v)
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.rel t (bindTerm {a = a.raw} env.func tm) (bindTerm {a = a.raw} env.func tm')
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.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)
bindTermsCong env [] = []
bindTermsCong env {tms = (_ :: _)} {tms' = (_ :: _)} (t :: ts) =
bindTermCong env t :: bindTermsCong env ts
public export
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.func tms)
public export
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 : 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.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 : 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.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.func tms)
bindUnique env f fDone (Done i) = fDone i
bindUnique env f fDone (Call op ts) = (a.algebra.equivalence _).transitive
(f.homo.semHomo op ts)
(a.algebra.semCong op $ bindsUnique env f fDone ts)
bindsUnique env f fDone [] = []
bindsUnique env f fDone (t :: ts) = bindUnique env f fDone t :: bindsUnique env f fDone ts
|
