|
407
|
1 {-# OPTIONS --cubical-compatible --safe #-}
|
|
|
2
|
|
139
|
3 module utm where
|
|
|
4
|
|
|
5 open import turing
|
|
|
6 open import Data.Product
|
|
319
|
7 -- open import Data.Bool
|
|
139
|
8 open import Data.List
|
|
|
9 open import Data.Nat
|
|
319
|
10 open import logic
|
|
139
|
11
|
|
|
12 data utmStates : Set where
|
|
140
|
13 reads : utmStates
|
|
139
|
14 read0 : utmStates
|
|
|
15 read1 : utmStates
|
|
|
16 read2 : utmStates
|
|
|
17 read3 : utmStates
|
|
|
18 read4 : utmStates
|
|
|
19 read5 : utmStates
|
|
|
20 read6 : utmStates
|
|
|
21
|
|
|
22 loc0 : utmStates
|
|
|
23 loc1 : utmStates
|
|
|
24 loc2 : utmStates
|
|
|
25 loc3 : utmStates
|
|
|
26 loc4 : utmStates
|
|
|
27 loc5 : utmStates
|
|
|
28 loc6 : utmStates
|
|
|
29
|
|
|
30 fetch0 : utmStates
|
|
|
31 fetch1 : utmStates
|
|
|
32 fetch2 : utmStates
|
|
|
33 fetch3 : utmStates
|
|
|
34 fetch4 : utmStates
|
|
|
35 fetch5 : utmStates
|
|
|
36 fetch6 : utmStates
|
|
|
37 fetch7 : utmStates
|
|
|
38
|
|
|
39 print0 : utmStates
|
|
|
40 print1 : utmStates
|
|
|
41 print2 : utmStates
|
|
|
42 print3 : utmStates
|
|
|
43 print4 : utmStates
|
|
|
44 print5 : utmStates
|
|
|
45 print6 : utmStates
|
|
|
46 print7 : utmStates
|
|
|
47
|
|
|
48 mov0 : utmStates
|
|
|
49 mov1 : utmStates
|
|
|
50 mov2 : utmStates
|
|
|
51 mov3 : utmStates
|
|
|
52 mov4 : utmStates
|
|
|
53 mov5 : utmStates
|
|
|
54 mov6 : utmStates
|
|
|
55
|
|
|
56 tidy0 : utmStates
|
|
|
57 tidy1 : utmStates
|
|
|
58 halt : utmStates
|
|
|
59
|
|
|
60 data utmΣ : Set where
|
|
|
61 ０ : utmΣ
|
|
|
62 １ : utmΣ
|
|
|
63 B : utmΣ
|
|
|
64 * : utmΣ
|
|
|
65 $ : utmΣ
|
|
|
66 ^ : utmΣ
|
|
|
67 X : utmΣ
|
|
|
68 Y : utmΣ
|
|
|
69 Z : utmΣ
|
|
|
70 ＠ : utmΣ
|
|
|
71 b : utmΣ
|
|
|
72
|
|
|
73 utmδ : utmStates → utmΣ → utmStates × (Write utmΣ) × Move
|
|
140
|
74 utmδ reads x = read0 , wnone , mnone
|
|
139
|
75 utmδ read0 * = read1 , write * , left
|
|
|
76 utmδ read0 x = read0 , write x , right
|
|
|
77 utmδ read1 x = read2 , write ＠ , right
|
|
|
78 utmδ read2 ^ = read3 , write ^ , right
|
|
|
79 utmδ read2 x = read2 , write x , right
|
|
|
80 utmδ read3 ０ = read4 , write ０ , left
|
|
|
81 utmδ read3 １ = read5 , write １ , left
|
|
|
82 utmδ read3 b = read6 , write b , left
|
|
|
83 utmδ read4 ＠ = loc0 , write ０ , right
|
|
|
84 utmδ read4 x = read4 , write x , left
|
|
|
85 utmδ read5 ＠ = loc0 , write １ , right
|
|
|
86 utmδ read5 x = read5 , write x , left
|
|
|
87 utmδ read6 ＠ = loc0 , write B , right
|
|
|
88 utmδ read6 x = read6 , write x , left
|
|
|
89 utmδ loc0 ０ = loc0 , write X , left
|
|
|
90 utmδ loc0 １ = loc0 , write Y , left
|
|
|
91 utmδ loc0 B = loc0 , write Z , left
|
|
|
92 utmδ loc0 $ = loc1 , write $ , right
|
|
|
93 utmδ loc0 x = loc0 , write x , left
|
|
|
94 utmδ loc1 X = loc2 , write ０ , right
|
|
|
95 utmδ loc1 Y = loc3 , write １ , right
|
|
|
96 utmδ loc1 Z = loc4 , write B , right
|
|
|
97 utmδ loc1 * = fetch0 , write * , right
|
|
|
98 utmδ loc1 x = loc1 , write x , right
|
|
|
99 utmδ loc2 ０ = loc5 , write X , right
|
|
|
100 utmδ loc2 １ = loc6 , write Y , right
|
|
|
101 utmδ loc2 B = loc6 , write Z , right
|
|
|
102 utmδ loc2 x = loc2 , write x , right
|
|
|
103 utmδ loc3 １ = loc5 , write Y , right
|
|
|
104 utmδ loc3 ０ = loc6 , write X , right
|
|
|
105 utmδ loc3 B = loc6 , write Z , right
|
|
|
106 utmδ loc3 x = loc3 , write x , right
|
|
|
107 utmδ loc4 B = loc5 , write Z , right
|
|
|
108 utmδ loc4 ０ = loc6 , write X , right
|
|
|
109 utmδ loc4 １ = loc6 , write Y , right
|
|
|
110 utmδ loc4 x = loc4 , write x , right
|
|
|
111 utmδ loc5 $ = loc1 , write $ , right
|
|
|
112 utmδ loc5 x = loc5 , write x , left
|
|
|
113 utmδ loc6 $ = halt , write $ , right
|
|
|
114 utmδ loc6 * = loc0 , write * , left
|
|
|
115 utmδ loc6 x = loc6 , write x , right
|
|
|
116 utmδ fetch0 ０ = fetch1 , write X , left
|
|
|
117 utmδ fetch0 １ = fetch2 , write Y , left
|
|
|
118 utmδ fetch0 B = fetch3 , write Z , left
|
|
|
119 utmδ fetch0 x = fetch0 , write x , right
|
|
|
120 utmδ fetch1 $ = fetch4 , write $ , right
|
|
|
121 utmδ fetch1 x = fetch1 , write x , left
|
|
|
122 utmδ fetch2 $ = fetch5 , write $ , right
|
|
|
123 utmδ fetch2 x = fetch2 , write x , left
|
|
|
124 utmδ fetch3 $ = fetch6 , write $ , right
|
|
|
125 utmδ fetch3 x = fetch3 , write x , left
|
|
|
126 utmδ fetch4 ０ = fetch7 , write X , right
|
|
|
127 utmδ fetch4 １ = fetch7 , write X , right
|
|
|
128 utmδ fetch4 B = fetch7 , write X , right
|
|
|
129 utmδ fetch4 * = print0 , write * , left
|
|
|
130 utmδ fetch4 x = fetch4 , write x , right
|
|
|
131 utmδ fetch5 ０ = fetch7 , write Y , right
|
|
|
132 utmδ fetch5 １ = fetch7 , write Y , right
|
|
|
133 utmδ fetch5 B = fetch7 , write Y , right
|
|
|
134 utmδ fetch5 * = print0 , write * , left
|
|
|
135 utmδ fetch5 x = fetch5 , write x , right
|
|
|
136 utmδ fetch6 ０ = fetch7 , write Z , right
|
|
|
137 utmδ fetch6 １ = fetch7 , write Z , right
|
|
|
138 utmδ fetch6 B = fetch7 , write Z , right
|
|
|
139 utmδ fetch6 * = print0 , write * , left
|
|
|
140 utmδ fetch6 x = fetch6 , write x , right
|
|
|
141 utmδ fetch7 * = fetch0 , write * , right
|
|
|
142 utmδ fetch7 x = fetch7 , write x , right
|
|
|
143 utmδ print0 X = print1 , write X , right
|
|
|
144 utmδ print0 Y = print2 , write Y , right
|
|
|
145 utmδ print0 Z = print3 , write Z , right
|
|
|
146 utmδ print1 ^ = print4 , write ^ , right
|
|
|
147 utmδ print1 x = print1 , write x , right
|
|
|
148 utmδ print2 ^ = print5 , write ^ , right
|
|
|
149 utmδ print2 x = print2 , write x , right
|
|
|
150 utmδ print3 ^ = print6 , write ^ , right
|
|
|
151 utmδ print3 x = print3 , write x , right
|
|
|
152 utmδ print4 x = print7 , write ０ , left
|
|
|
153 utmδ print5 x = print7 , write １ , left
|
|
|
154 utmδ print6 x = print7 , write B , left
|
|
|
155 utmδ print7 X = mov0 , write X , right
|
|
|
156 utmδ print7 Y = mov1 , write Y , right
|
|
|
157 utmδ print7 x = print7 , write x , left
|
|
|
158 utmδ mov0 ^ = mov2 , write ^ , left
|
|
|
159 utmδ mov0 x = mov0 , write x , right
|
|
|
160 utmδ mov1 ^ = mov3 , write ^ , right
|
|
|
161 utmδ mov1 x = mov1 , write x , right
|
|
|
162 utmδ mov2 ０ = mov4 , write ^ , right
|
|
|
163 utmδ mov2 １ = mov5 , write ^ , right
|
|
|
164 utmδ mov2 B = mov6 , write ^ , right
|
|
|
165 utmδ mov3 ０ = mov4 , write ^ , left
|
|
|
166 utmδ mov3 １ = mov5 , write ^ , left
|
|
|
167 utmδ mov3 B = mov6 , write ^ , left
|
|
|
168 utmδ mov4 ^ = tidy0 , write ０ , left
|
|
|
169 utmδ mov5 ^ = tidy0 , write １ , left
|
|
|
170 utmδ mov6 ^ = tidy0 , write B , left
|
|
|
171 utmδ tidy0 $ = tidy1 , write $ , left
|
|
|
172 utmδ tidy0 x = tidy0 , write x , left
|
|
|
173 utmδ tidy1 X = tidy1 , write ０ , left
|
|
|
174 utmδ tidy1 Y = tidy1 , write １ , left
|
|
|
175 utmδ tidy1 Z = tidy1 , write B , left
|
|
141
|
176 utmδ tidy1 $ = reads , write $ , right
|
|
139
|
177 utmδ tidy1 x = tidy1 , write x , left
|
|
|
178 utmδ _ x = halt , write x , mnone
|
|
|
179
|
|
|
180 U-TM : Turing utmStates utmΣ
|
|
|
181 U-TM = record {
|
|
|
182 tδ = utmδ
|
|
|
183 ; tstart = read0
|
|
|
184 ; tend = tend
|
|
|
185 ; tnone = b
|
|
|
186 } where
|
|
|
187 tend : utmStates → Bool
|
|
|
188 tend halt = true
|
|
|
189 tend _ = false
|
|
|
190
|
|
|
191 -- Copyδ : CopyStates → ℕ → CopyStates × ( Write ℕ ) × Move
|
|
|
192 -- Copyδ s1 0 = H , wnone , mnone
|
|
|
193 -- Copyδ s1 1 = s2 , write 0 , right
|
|
|
194 -- Copyδ s2 0 = s3 , write 0 , right
|
|
|
195 -- Copyδ s2 1 = s2 , write 1 , right
|
|
|
196 -- Copyδ s3 0 = s4 , write 1 , left
|
|
|
197 -- Copyδ s3 1 = s3 , write 1 , right
|
|
|
198 -- Copyδ s4 0 = s5 , write 0 , left
|
|
|
199 -- Copyδ s4 1 = s4 , write 1 , left
|
|
|
200 -- Copyδ s5 0 = s1 , write 1 , right
|
|
|
201 -- Copyδ s5 1 = s5 , write 1 , left
|
|
|
202 -- Copyδ H _ = H , wnone , mnone
|
|
|
203 -- Copyδ _ (suc (suc _)) = H , wnone , mnone
|
|
|
204
|
|
|
205 Copyδ-encode : List utmΣ
|
|
|
206 Copyδ-encode =
|
|
|
207 ０ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ ０ ∷ -- s1 0 = H , wnone , mnone
|
|
332
|
208 * ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ -- s0 1 = s2 , write 0 , right
|
|
139
|
209 * ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷ １ ∷ -- s2 0 = s3 , write 0 , right
|
|
|
210 * ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ -- s2 1 = s2 , write 1 , right
|
|
|
211 * ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ -- s3 0 = s4 , write 1 , left
|
|
|
212 * ∷ ０ ∷ １ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ -- s3 1 = s3 , write 1 , right
|
|
|
213 * ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ -- s4 0 = s5 , write 0 , left
|
|
|
214 * ∷ １ ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ -- s4 1 = s4 , write 1 , left
|
|
|
215 * ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ -- s5 0 = s1 , write 1 , right
|
|
|
216 * ∷ １ ∷ ０ ∷ １ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷ -- s5 1 = s5 , write 1 , left
|
|
|
217 []
|
|
|
218
|
|
|
219
|
|
|
220 input-encode : List utmΣ
|
|
|
221 input-encode = １ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ []
|
|
|
222
|
|
|
223 input+Copyδ : List utmΣ
|
|
|
224 input+Copyδ = ( $ ∷ ０ ∷ ０ ∷ ０ ∷ ０ ∷ * ∷ [] ) -- start state
|
|
|
225 ++ Copyδ-encode
|
|
|
226 ++ ( $ ∷ ^ ∷ input-encode )
|
|
|
227
|
|
140
|
228 short-input : List utmΣ
|
|
|
229 short-input = $ ∷ ０ ∷ ０ ∷ ０ ∷ * ∷
|
|
|
230 ０ ∷ ０ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ １ ∷ * ∷
|
|
|
231 ０ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ １ ∷ １ ∷ * ∷
|
|
|
232 ０ ∷ １ ∷ B ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ * ∷
|
|
|
233 １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ １ ∷ $ ∷
|
|
|
234 ^ ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ []
|
|
139
|
235
|
|
140
|
236 utm-test1 : List utmΣ → utmStates × ( List utmΣ ) × ( List utmΣ )
|
|
407
|
237 utm-test1 inp = Turing.taccept U-TM 10 inp
|
|
140
|
238
|
|
|
239 utm-test2 : ℕ → List utmΣ → utmStates × ( List utmΣ ) × ( List utmΣ )
|
|
|
240 utm-test2 n inp = loop n (Turing.tstart U-TM) inp []
|
|
139
|
241 where
|
|
|
242 loop : ℕ → utmStates → ( List utmΣ ) → ( List utmΣ ) → utmStates × ( List utmΣ ) × ( List utmΣ )
|
|
|
243 loop zero q L R = ( q , L , R )
|
|
140
|
244 loop (suc n) q L R with move {utmStates} {utmΣ} {０} {utmδ} q L R | q
|
|
|
245 ... | nq , nL , nR | reads = loop n nq nL nR
|
|
407
|
246 ... | nq , nL , nR | _ = loop n nq nL nR
|
|
139
|
247
|
|
332
|
248 t1 = utm-test2 3 short-input
|
|
140
|
249
|
|
|
250 t : (n : ℕ) → utmStates × ( List utmΣ ) × ( List utmΣ )
|
|
141
|
251 -- t n = utm-test2 n input+Copyδ
|
|
|
252 t n = utm-test2 n short-input
|
