-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathoutput.tex
217 lines (203 loc) · 7.97 KB
/
output.tex
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
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
\chapter{Tog Generated Code}
\label{appendix:generatedTog}
\begin{togcode}
module Monoid where
record Monoid (A : Set) : Set where
constructor MonoidC
field
e : A
op : A -> A -> A
lunit_e : (x : A) -> op e x == x
runit_e : (x : A) -> op x e == x
associative_op : {x y z : A} -> op (op x y) z == op x (op y z)
\end{togcode}
\begin{togcode}
record Sig (AS : Set) : Set where
constructor SigSigC
field
eS : AS
opS : AS -> AS -> AS
record Product (A : Set) : Set where
constructor ProductC
field
eP : Prod A A
opP : Prod A A -> Prod A A -> Prod A A
lunit_eP : (xP : Prod A A) -> opP eP xP == xP
runit_eP : (xP : Prod A A) -> opP xP eP == xP
associative_opP : {xP yP zP : (Prod A A)} ->
opP (opP xP yP) zP == opP xP (opP yP zP)
\end{togcode}
\begin{togcode}
record Hom {A1 : Set} {A2 : Set}
(Mo1 : Monoid A1) (Mo2 : Monoid A2) : Set where
constructor HomC
field
hom : (A1 -> A2)
pres-e : (hom (e Mo1)) == e Mo2
pres-op : {x1 x2 : A1} ->
hom (op Mo1 x1 x2) == op Mo2 (hom x1) (hom x2)
record RelInterp {A1 : Set} {A2 : Set}
(Mo1 : (Monoid A1)) (Mo2 : (Monoid A2)) : Set where
constructor RelInterpC
field
interp : (A1 -> (A2 -> Set))
interp-e : (interp (e Mo1) (e Mo2))
interp-op : {x1 x2 : A1} {y1 y2 : A2} ->
((interp x1 y1) -> ((interp x2 y2) ->
(interp ((op Mo1) x1 x2) ((op Mo2) y1 y2))))
\end{togcode}
\begin{togcode}
data MonoidTerm : Set where
eL : MonoidTerm
opL : MonoidTerm -> MonoidTerm -> MonoidTerm
data ClMonoidTerm (A : Set) : Set where
sing : A -> ClMonoidTerm A
eCl : ClMonoidTerm A
opCl : ClMonoidTerm A -> ClMonoidTerm A -> ClMonoidTerm A
data OpMonoidTerm (n : Nat) : Set where
v : Fin n -> OpMonoidTerm n
eOL : OpMonoidTerm n
opOL : OpMonoidTerm n -> OpMonoidTerm n -> OpMonoidTerm n
data OpMonoidTerm2 (n : Nat) (A : Set) : Set where
v2 : Fin n -> OpMonoidTerm2 n A
sing2 : A -> OpMonoidTerm2 n A
eOL2 : OpMonoidTerm2 n A
opOL2 : OpMonoidTerm2 n A -> OpMonoidTerm2 n A -> OpMonoidTerm2 n A
\end{togcode}
\begin{togcode}
simplifyCl : {A : Set} -> ((ClMonoidTerm A) -> (ClMonoidTerm A))
simplifyCl (opCl eCl x) = x
simplifyCl (opCl x eCl) = x
simplifyCl (opCl x1 x2) = (opCl (simplifyCl x1) (simplifyCl x2))
simplifyCl eCl = eCl
simplifyCl (sing x1) = (sing x1)
simplifyOpB : {n : Nat} -> ((OpMonoidTerm n) -> (OpMonoidTerm n))
simplifyOpB (opOL eOL x) = x
simplifyOpB (opOL x eOL) = x
simplifyOpB (opOL x1 x2) = (opOL (simplifyOpB x1) (simplifyOpB x2))
simplifyOpB eOL = eOL
simplifyOpB (v x1) = (v x1)
simplifyOp : {n : Nat} {A : Set} ->
((OpMonoidTerm2 n A) -> (OpMonoidTerm2 n A))
simplifyOp (opOL2 eOL2 x) = x
simplifyOp (opOL2 x eOL2) = x
simplifyOp (opOL2 x1 x2) = (opOL2 (simplifyOp x1) (simplifyOp x2))
simplifyOp eOL2 = eOL2
simplifyOp (v2 x1) = (v2 x1)
simplifyOp (sing2 x1) = (sing2 x1)
\end{togcode}
\begin{togcode}
evalB : {A : Set} -> ((Monoid A) -> (MonoidTerm -> A))
evalB Mo (opL x1 x2) = ((op Mo) (evalB Mo x1) (evalB Mo x2))
evalB Mo eL = (e Mo)
evalCl : {A : Set} -> ((Monoid A) -> ((ClMonoidTerm A) -> A))
evalCl Mo (sing x1) = x1
evalCl Mo (opCl x1 x2) = ((op Mo) (evalCl Mo x1) (evalCl Mo x2))
evalCl Mo eCl = (e Mo)
evalOpB : {A : Set} {n : Nat} ->
((Monoid A) -> ((Vec A n) -> ((OpMonoidTerm n) -> A)))
evalOpB Mo vars (v x1) = (lookup _ x1 vars)
evalOpB Mo vars (opOL x1 x2) =
((op Mo) (evalOpB Mo vars x1) (evalOpB Mo vars x2))
evalOpB Mo vars eOL = (e Mo)
evalOp : {A : Set} {n : Nat} ->
((Monoid A) -> ((Vec A n) -> ((OpMonoidTerm2 n A) -> A)))
evalOp Mo vars (v2 x1) = (lookup _ x1 vars)
evalOp Mo vars (sing2 x1) = x1
evalOp Mo vars (opOL2 x1 x2) =
((op Mo) (evalOp Mo vars x1) (evalOp Mo vars x2))
evalOp Mo vars eOL2 = (e Mo)
\end{togcode}
\begin{togcode}
inductionB : {P : (MonoidTerm -> Set)} ->
(((x1 x2 : MonoidTerm) -> ((P x1) -> ((P x2) -> (P (opL x1 x2))))) ->
((P eL) -> ((x : MonoidTerm) -> (P x))))
inductionB {p} popl pel (opL x1 x2) =
(popl _ _ (inductionB {p} popl pel x1) (inductionB {p} popl pel x2))
inductionB {p} popl pel eL = pel
inductionCl : {A : Set} {P : ((ClMonoidTerm A) -> Set)} ->
(((x1 : A) -> (P (sing x1))) ->
(((x1 x2 : (ClMonoidTerm A)) ->
((P x1) -> ((P x2) -> (P (opCl x1 x2))))) ->
((P eCl) -> ((x : (ClMonoidTerm A)) -> (P x)))))
inductionCl {_} {p} psing popcl pecl (sing x1) = (psing x1)
inductionCl {_} {p} psing popcl pecl (opCl x1 x2) =
(popcl _ _ (inductionCl {_} {p} psing popcl pecl x1)
(inductionCl {_} {p} psing popcl pecl x2))
inductionCl {_} {p} psing popcl pecl eCl = pecl
\end{togcode}
\begin{togcode}
inductionOpB : {n : Nat} {P : ((OpMonoidTerm n) -> Set)} ->
(((fin : (Fin n)) -> (P (v fin))) ->
(((x1 x2 : (OpMonoidTerm n)) ->
((P x1) -> ((P x2) -> (P (opOL x1 x2))))) ->
((P eOL) -> ((x : (OpMonoidTerm n)) -> (P x)))))
inductionOpB {_} {p} pv popol peol (v x1) = (pv x1)
inductionOpB {_} {p} pv popol peol (opOL x1 x2) =
(popol _ _ (inductionOpB {_} {p} pv popol peol x1)
(inductionOpB {_} {p} pv popol peol x2))
inductionOpB {_} {p} pv popol peol eOL = peol
inductionOp : {n : Nat} {A : Set} {P : ((OpMonoidTerm2 n A) -> Set)} ->
(((fin : (Fin n)) -> (P (v2 fin))) ->
(((x1 : A) -> (P (sing2 x1))) ->
(((x1 x2 : (OpMonoidTerm2 n A)) ->
((P x1) -> ((P x2) -> (P (opOL2 x1 x2))))) ->
((P eOL2) -> ((x : (OpMonoidTerm2 n A)) -> (P x))))))
inductionOp {_} {_} {p} pv2 psing2 popol2 peol2 (v2 x1) = (pv2 x1)
inductionOp {_} {_} {p} pv2 psing2 popol2 peol2 (sing2 x1) = (psing2 x1)
inductionOp {_} {_} {p} pv2 psing2 popol2 peol2 (opOL2 x1 x2) =
(popol2 _ _ (inductionOp {_} {_} {p} pv2 psing2 popol2 peol2 x1)
(inductionOp {_} {_} {p} pv2 psing2 popol2 peol2 x2))
inductionOp {_} {_} {p} pv2 psing2 popol2 peol2 eOL2 = peol2
\end{togcode}
\begin{togcode}
opL' : (MonoidTerm -> (MonoidTerm -> MonoidTerm))
opL' x1 x2 = (opL x1 x2)
eL' : MonoidTerm
eL' = eL
stageB : (MonoidTerm -> (Staged MonoidTerm))
stageB (opL x1 x2) =
(stage2 opL' (codeLift2 opL') (stageB x1) (stageB x2))
stageB eL = (Now eL)
opCl' : {A : Set} ->
((ClMonoidTerm A) -> ((ClMonoidTerm A) -> (ClMonoidTerm A)))
opCl' x1 x2 = (opCl x1 x2)
eCl' : {A : Set} -> (ClMonoidTerm A)
eCl' = eCl
stageCl : {A : Set} -> ((ClMonoidTerm A) -> (Staged (ClMonoidTerm A)))
stageCl (sing x1) = (Now (sing x1))
stageCl (opCl x1 x2) =
(stage2 opCl' (codeLift2 opCl') (stageCl x1) (stageCl x2))
stageCl eCl = (Now eCl)
\end{togcode}
\begin{togcode}
opOL' : {n : Nat} ->
((OpMonoidTerm n) -> ((OpMonoidTerm n) -> (OpMonoidTerm n)))
opOL' x1 x2 = (opOL x1 x2)
eOL' : {n : Nat} -> (OpMonoidTerm n)
eOL' = eOL
stageOpB : {n : Nat} -> ((OpMonoidTerm n) -> (Staged (OpMonoidTerm n)))
stageOpB (v x1) = (const (code (v x1)))
stageOpB (opOL x1 x2) =
(stage2 opOL' (codeLift2 opOL') (stageOpB x1) (stageOpB x2))
stageOpB eOL = (Now eOL)
opOL2' : {n : Nat} {A : Set} ->
((OpMonoidTerm2 n A) -> ((OpMonoidTerm2 n A) -> (OpMonoidTerm2 n A)))
opOL2' x1 x2 = (opOL2 x1 x2)
eOL2' : {n : Nat} {A : Set} -> (OpMonoidTerm2 n A)
eOL2' = eOL2
stageOp : {n : Nat} {A : Set} ->
((OpMonoidTerm2 n A) -> (Staged (OpMonoidTerm2 n A)))
stageOp (sing2 x1) = (Now (sing2 x1))
stageOp (v2 x1) = (const (code (v2 x1)))
stageOp (opOL2 x1 x2) =
(stage2 opOL2' (codeLift2 opOL2') (stageOp x1) (stageOp x2))
stageOp eOL2 = (Now eOL2)
\end{togcode}
\begin{togcode}
record StagedRepr (A : Set) (Repr : (Set -> Set)) : Set where
constructor repr
field
opT : ((Repr A) -> ((Repr A) -> (Repr A)))
eT : (Repr A)
\end{togcode}