1structure armSyntax :> armSyntax =
2struct
3
4open Abbrev HolKernel arm_seq_monadTheory arm_decoderTheory;
5
6val ERR = Feedback.mk_HOL_ERR "armSyntax";
7
8fun dest_strip t =
9let val (l,r) = strip_comb t in
10  (fst (dest_const l), r)
11end;
12
13local
14  val arm_state_type = ``:arm_state``;
15  val err = ERR "dest_monad_type" "not an instance of 'a M"
16in
17  fun dest_monad_type ty =
18  let val (tya,tyb) = dom_rng ty in
19     if tya = arm_state_type then
20       case total dest_thy_type tyb of
21         SOME {Tyop = "error_option", Thy = "arm_seq_monad",
22               Args = [tyc, tyd]} =>
23           (if tyd = arm_state_type then tyc else raise err)
24       | _ => raise err
25     else
26       raise err
27  end handle HOL_ERR _ => raise err
28end;
29
30fun inst_word_alpha ty tm =
31  Term.inst [Type.alpha |->
32   (if wordsSyntax.is_word_type (Term.type_of tm) then
33      ty
34    else
35      wordsSyntax.mk_word_type ty)] tm;
36
37fun mk_monad_const s  = prim_mk_const{Name = s, Thy = "arm_seq_monad"}
38fun mk_core_const s   = prim_mk_const{Name = s, Thy = "arm_coretypes"}
39fun mk_decode_const s = prim_mk_const{Name = s, Thy = "arm_decoder"};
40
41val error_tm      = mk_monad_const "Error"
42val valuestate_tm = mk_monad_const "ValueState"
43
44val constT_tm = mk_monad_const "constT"
45val seqT_tm   = mk_monad_const "seqT"
46val parT_tm   = mk_monad_const "parT"
47val forT_tm   = mk_monad_const "forT"
48val readT_tm  = mk_monad_const "readT"
49val writeT_tm = mk_monad_const "writeT"
50
51val read__reg_tm  = mk_monad_const "read__reg"
52val write__reg_tm = mk_monad_const "write__reg"
53val read__psr_tm  = mk_monad_const "read__psr"
54val write__psr_tm = mk_monad_const "write__psr"
55
56val read_reg_mode_tm  = mk_monad_const "read_reg_mode"
57val write_reg_mode_tm = mk_monad_const "write_reg_mode"
58val read_reg_tm       = mk_monad_const "read_reg"
59val write_reg_tm      = mk_monad_const "write_reg"
60val read_cpsr_tm      = mk_monad_const "read_cpsr"
61val write_cpsr_tm     = mk_monad_const "write_cpsr"
62val read_spsr_tm      = mk_monad_const "read_spsr"
63val write_spsr_tm     = mk_monad_const "write_spsr"
64val read_memA_tm      = mk_monad_const "read_memA"
65val write_memA_tm     = mk_monad_const "write_memA"
66
67val clear_event_register_tm     = mk_monad_const "clear_event_register"
68val send_event_tm               = mk_monad_const "send_event"
69val wait_for_interrupt_tm       = mk_monad_const "wait_for_interrupt"
70val clear_wait_for_interrupt_tm = mk_monad_const "clear_wait_for_interrupt"
71
72val decode_psr_tm       = mk_core_const "decode_psr"
73val bytes_tm            = mk_core_const "bytes"
74val align_tm            = mk_core_const "align"
75val aligned_tm          = mk_core_const "aligned"
76val Encoding_ARM_tm     = mk_core_const "Encoding_ARM"
77val Encoding_Thumb_tm   = mk_core_const "Encoding_Thumb"
78val Encoding_Thumb2_tm  = mk_core_const "Encoding_Thumb2"
79val Encoding_ThumbEE_tm = mk_core_const "Encoding_ThumbEE"
80val ITAdvance_tm        = mk_core_const "ITAdvance"
81val NoInterrupt_tm      = mk_core_const "NoInterrupt"
82val HW_Reset_tm         = mk_core_const "HW_Reset"
83val HW_Fiq_tm           = mk_core_const "HW_Fiq"
84val HW_Irq_tm           = mk_core_const "HW_Irq"
85
86val arm_decode_tm       = mk_decode_const "arm_decode"
87val thumb_decode_tm     = mk_decode_const "thumb_decode"
88val thumbee_decode_tm   = mk_decode_const "thumbee_decode"
89val thumb2_decode_tm    = mk_decode_const "thumb2_decode";
90
91fun mk_error s =
92  HolKernel.mk_comb(error_tm,
93    Term.inst [Type.alpha |-> stringSyntax.string_ty] s)
94  handle HOL_ERR _ => raise ERR "mk_error" "";
95
96fun mk_valuestate (v,s) =
97  HolKernel.list_mk_comb(Term.inst
98    [Type.alpha |-> Term.type_of v,
99     Type.beta |-> Term.type_of s] valuestate_tm, [v,s])
100  handle HOL_ERR _ => raise ERR "mk_valuestate" "";
101
102fun mk_constT t =
103  HolKernel.mk_comb(Term.inst[Type.alpha |-> Term.type_of t] constT_tm,t)
104  handle HOL_ERR _ => raise ERR "mk_constT" "";
105
106fun mk_seqT (f,g) =
107  HolKernel.list_mk_comb(Term.inst
108    [Type.alpha |-> dest_monad_type (Term.type_of f),
109     Type.beta  |-> (dest_monad_type o snd o Type.dom_rng o Term.type_of) g]
110     seqT_tm, [f,g])
111  handle HOL_ERR _ => raise ERR "mk_seqT" "";
112
113fun mk_parT (f,g) =
114  HolKernel.list_mk_comb(Term.inst
115    [Type.alpha |-> dest_monad_type (Term.type_of f),
116     Type.beta  |-> dest_monad_type (Term.type_of g)] parT_tm,[f,g])
117  handle HOL_ERR _ => raise ERR "mk_parT" "";
118
119fun mk_forT (l,h,f) =
120  HolKernel.list_mk_comb(Term.inst
121    [Type.alpha |-> (dest_monad_type o snd o Type.dom_rng o Term.type_of) f]
122    forT_tm,[l,h,f])
123  handle HOL_ERR _ => raise ERR "mk_forT" "";
124
125fun mk_readT f =
126  HolKernel.mk_comb(Term.inst
127    [Type.alpha |-> snd (dom_rng (Term.type_of f))] readT_tm, f)
128  handle HOL_ERR _ => raise ERR "mk_readT" "";
129
130fun mk_writeT f =
131  HolKernel.mk_comb(writeT_tm, f)
132  handle HOL_ERR _ => raise ERR "mk_writeT" "";
133
134fun mk_read__reg (ii,r) =
135  HolKernel.list_mk_comb(read__reg_tm,
136    [Term.inst [Type.alpha |-> ``:iiid``] ii,
137     Term.inst [Type.alpha |-> ``:RName``] r])
138  handle HOL_ERR _ => raise ERR "mk_read__reg" "";
139
140fun mk_write__reg (ii,r,v) =
141  HolKernel.list_mk_comb(write__reg_tm,
142    [Term.inst [Type.alpha |-> ``:iiid``] ii,
143     Term.inst [Type.alpha |-> ``:RName``] r,
144     inst_word_alpha ``:32`` v])
145  handle HOL_ERR _ => raise ERR "mk_write__reg" "";
146
147fun mk_read__psr (ii,r) =
148  HolKernel.list_mk_comb(read__psr_tm,
149    [Term.inst [Type.alpha |-> ``:iiid``] ii,
150     Term.inst [Type.alpha |-> ``:PSRName``] r])
151  handle HOL_ERR _ => raise ERR "mk_read__psr" "";
152
153fun mk_write__psr (ii,r,v) =
154  HolKernel.list_mk_comb(write__psr_tm,
155    [Term.inst [Type.alpha |-> ``:iiid``] ii,
156     Term.inst [Type.alpha |-> ``:PSRName``] r,
157     Term.inst [Type.alpha |-> ``:ARMpsr``] v])
158  handle HOL_ERR _ => raise ERR "mk_write__psr" "";
159
160fun mk_read_reg (ii,n) =
161  HolKernel.list_mk_comb(read_reg_tm,
162    [Term.inst [Type.alpha |-> ``:iiid``] ii,
163     inst_word_alpha ``:4`` n])
164  handle HOL_ERR _ => raise ERR "mk_read_reg" "";
165
166fun mk_write_reg (ii,n,v) =
167  HolKernel.list_mk_comb(write_reg_tm,
168    [Term.inst [Type.alpha |-> ``:iiid``] ii,
169     inst_word_alpha ``:4`` n,
170     inst_word_alpha ``:32`` v])
171  handle HOL_ERR _ => raise ERR "mk_write_reg" "";
172
173fun mk_read_reg_mode (ii,n,m) =
174  HolKernel.list_mk_comb(read_reg_mode_tm,
175    [Term.inst [Type.alpha |-> ``:iiid``] ii,
176     pairSyntax.mk_pair
177       (inst_word_alpha ``:4`` n, inst_word_alpha ``:5`` m)])
178  handle HOL_ERR _ => raise ERR "mk_read_reg_mode" "";
179
180fun mk_write_reg_mode (ii,n,m,v) =
181  HolKernel.list_mk_comb(write_reg_mode_tm,
182    [Term.inst [Type.alpha |-> ``:iiid``] ii,
183     pairSyntax.mk_pair
184       (inst_word_alpha ``:4`` n, inst_word_alpha ``:5`` m),
185     inst_word_alpha ``:32`` v])
186  handle HOL_ERR _ => raise ERR "mk_write_reg_mode" "";
187
188fun mk_read_cpsr ii =
189  HolKernel.mk_comb(read_cpsr_tm, Term.inst [Type.alpha |-> ``:iiid``] ii)
190  handle HOL_ERR _ => raise ERR "mk_read_cpsr" "";
191
192fun mk_write_cpsr (ii,v) =
193  HolKernel.list_mk_comb(write_cpsr_tm,
194    [Term.inst [Type.alpha |-> ``:iiid``] ii,
195     Term.inst [Type.alpha |-> ``:ARMpsr``] v])
196  handle HOL_ERR _ => raise ERR "mk_write_cpsr" "";
197
198fun mk_read_spsr ii =
199  HolKernel.mk_comb(read_spsr_tm, Term.inst [Type.alpha |-> ``:iiid``] ii)
200  handle HOL_ERR _ => raise ERR "mk_read_spsr" "";
201
202fun mk_write_spsr (ii,v) =
203  HolKernel.list_mk_comb(write_spsr_tm,
204    [Term.inst [Type.alpha |-> ``:iiid``] ii,
205     Term.inst [Type.alpha |-> ``:ARMpsr``] v])
206  handle HOL_ERR _ => raise ERR "mk_write_spsr" "";
207
208fun mk_read_memA (ii,a,s) =
209  HolKernel.list_mk_comb(read_memA_tm,
210    [Term.inst [Type.alpha |-> ``:iiid``] ii,
211     pairSyntax.mk_pair
212       (inst_word_alpha ``:32`` a,
213        Term.inst [Type.alpha |-> ``:num``] s)])
214  handle HOL_ERR _ => raise ERR "mk_read_memA" "";
215
216fun mk_write_memA (ii,a,s,v) =
217  HolKernel.list_mk_comb(write_memA_tm,
218    [Term.inst [Type.alpha |-> ``:iiid``] ii,
219     pairSyntax.mk_pair
220       (inst_word_alpha ``:32`` a,
221        Term.inst [Type.alpha |-> ``:num``] s),
222     v])
223  handle HOL_ERR _ => raise ERR "mk_write_memA" "";
224
225fun mk_clear_event_register ii =
226  HolKernel.mk_comb(clear_event_register_tm,
227    Term.inst [Type.alpha |-> ``:iiid``] ii)
228  handle HOL_ERR _ => raise ERR "mk_clear_event_register" "";
229
230fun mk_send_event ii =
231  HolKernel.mk_comb(send_event_tm, Term.inst [Type.alpha |-> ``:iiid``] ii)
232  handle HOL_ERR _ => raise ERR "mk_send_event" "";
233
234fun mk_wait_for_interrupt ii =
235  HolKernel.mk_comb(wait_for_interrupt_tm,
236    Term.inst [Type.alpha |-> ``:iiid``] ii)
237  handle HOL_ERR _ => raise ERR "mk_wait_for_interrupt" "";
238
239fun mk_clear_wait_for_interrupt ii =
240  HolKernel.mk_comb(clear_wait_for_interrupt_tm,
241    Term.inst [Type.alpha |-> ``:iiid``] ii)
242  handle HOL_ERR _ => raise ERR "mk_clear_wait_for_interrupt" "";
243
244fun mk_decode_psr w =
245  HolKernel.mk_comb(decode_psr_tm, inst_word_alpha ``:32`` w)
246  handle HOL_ERR _ => raise ERR "mk_decode_psr" "";
247
248fun mk_bytes (w,n) =
249  HolKernel.mk_comb(bytes_tm, pairSyntax.mk_pair(inst_word_alpha ``:32`` w, n))
250  handle HOL_ERR _ => raise ERR "mk_bytes" "";
251
252fun mk_align (w,n) =
253  HolKernel.mk_comb(Term.inst
254    [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] align_tm,
255    pairSyntax.mk_pair(w, n))
256  handle HOL_ERR _ => raise ERR "mk_align" "";
257
258fun mk_aligned (w,n) =
259  HolKernel.mk_comb(Term.inst
260    [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] aligned_tm,
261    pairSyntax.mk_pair(w, n))
262  handle HOL_ERR _ => raise ERR "mk_aligned" "";
263
264fun mk_ITAdvance w =
265  HolKernel.mk_comb(Term.inst
266  [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] ITAdvance_tm, w)
267  handle HOL_ERR _ => raise ERR "mk_ITAdvance" "";
268
269fun mk_read_memA_1 (ii,a) = mk_read_memA (ii,a,``1n``);
270
271fun mk_write_memA_1 (ii,a,v) =
272   mk_write_memA (ii,a,``1n``,listSyntax.mk_list([v],``:word8``));
273
274fun mk_read_memA_2 (ii,a) = mk_read_memA (ii,a,``2n``);
275fun mk_write_memA_2 (ii,a,v) = mk_write_memA (ii,a,``2n``,mk_bytes(v,``2n``));
276fun mk_read_memA_4 (ii,a) = mk_read_memA (ii,a,``4n``);
277fun mk_write_memA_4 (ii,a,v) = mk_write_memA (ii,a,``4n``,mk_bytes(v,``4n``));
278
279fun mk_arm_decode(b,w) =
280  HolKernel.list_mk_comb(arm_decode_tm, [b,inst_word_alpha ``:32`` w])
281  handle HOL_ERR _ => raise ERR "mk_arm_decode" "";
282
283fun mk_thumb_decode(a,itstate,w) =
284  HolKernel.list_mk_comb(thumb_decode_tm,
285    [a,inst_word_alpha ``:8`` itstate, inst_word_alpha ``:16`` w])
286  handle HOL_ERR _ => raise ERR "mk_thumb_decode" "";
287
288fun mk_thumbee_decode(a,itstate,w) =
289  HolKernel.list_mk_comb(thumbee_decode_tm,
290    [a,inst_word_alpha ``:8`` itstate, inst_word_alpha ``:16`` w])
291  handle HOL_ERR _ => raise ERR "mk_thumbee_decode" "";
292
293fun mk_thumb2_decode(a,itstate,w1,w2) =
294  HolKernel.list_mk_comb(thumb2_decode_tm,
295    [a,inst_word_alpha ``:8`` itstate,
296     pairSyntax.mk_pair
297       (inst_word_alpha ``:16`` w1,
298        inst_word_alpha ``:16`` w2)])
299  handle HOL_ERR _ => raise ERR "mk_thumb2_decode" "";
300
301val dest_error = HolKernel.dest_monop error_tm (ERR "dest_error" "")
302
303val dest_valuestate =
304  HolKernel.dest_binop valuestate_tm (ERR "dest_valuestate" "")
305
306val dest_constT = HolKernel.dest_monop constT_tm (ERR "dest_constT" "")
307val dest_seqT   = HolKernel.dest_binop seqT_tm   (ERR "dest_seqT" "")
308val dest_parT   = HolKernel.dest_binop parT_tm   (ERR "dest_parT" "")
309val dest_forT   = HolKernel.dest_triop forT_tm   (ERR "dest_forT" "")
310val dest_readT  = HolKernel.dest_monop readT_tm  (ERR "dest_readT" "")
311val dest_writeT = HolKernel.dest_monop writeT_tm (ERR "dest_writeT" "")
312
313val dest_read__reg =
314  HolKernel.dest_binop read__reg_tm  (ERR "dest_read__reg" "")
315
316val dest_write__reg =
317  HolKernel.dest_triop write__reg_tm (ERR "dest_write__reg" "")
318
319val dest_read__psr =
320  HolKernel.dest_binop read__psr_tm  (ERR "dest_read__psr" "")
321
322val dest_write__psr =
323  HolKernel.dest_triop write__psr_tm (ERR "dest_write__psr" "")
324
325val dest_read_reg_mode =
326  HolKernel.dest_binop read_reg_mode_tm  (ERR "dest_read_reg_mode" "")
327
328val dest_write_reg_mode =
329  HolKernel.dest_triop write_reg_mode_tm (ERR "dest_write_reg_mode" "")
330
331val dest_read_reg   = dest_binop read_reg_tm   (ERR "dest_read_reg" "")
332val dest_write_reg  = dest_triop write_reg_tm  (ERR "dest_write_reg" "")
333val dest_read_cpsr  = dest_monop read_cpsr_tm  (ERR "dest_read_cpsr" "")
334val dest_write_cpsr = dest_binop write_cpsr_tm (ERR "dest_write_cpsr" "")
335val dest_read_spsr  = dest_monop read_spsr_tm  (ERR "dest_read_spsr" "")
336val dest_write_spsr = dest_binop write_spsr_tm (ERR "dest_write_spsr" "")
337val dest_read_memA  = dest_binop read_memA_tm  (ERR "dest_read_memA" "")
338val dest_write_memA = dest_triop write_memA_tm (ERR "dest_write_memA" "")
339val dest_decode_psr = dest_monop decode_psr_tm (ERR "dest_decode_psr" "")
340val dest_bytes      = dest_monop bytes_tm      (ERR "dest_bytes" "");
341val dest_align      = dest_monop align_tm      (ERR "dest_align" "");
342val dest_aligned    = dest_monop aligned_tm    (ERR "dest_align" "");
343val dest_ITAdvance  = dest_monop ITAdvance_tm  (ERR "dest_ITAdvance" "");
344
345val dest_clear_event_register =
346    HolKernel.dest_monop decode_psr_tm (ERR "dest_clear_event_register" "");
347
348val dest_send_event =
349    HolKernel.dest_monop send_event_tm (ERR "dest_send_event" "");
350
351val dest_wait_for_interrupt =
352    HolKernel.dest_monop wait_for_interrupt_tm
353    (ERR "dest_wait_for_interrupt" "");
354
355val dest_clear_wait_for_interrupt =
356    HolKernel.dest_monop clear_wait_for_interrupt_tm
357    (ERR "dest_clear_wait_for_interrupt" "");
358
359val dest_arm_decode =
360    HolKernel.dest_binop arm_decode_tm (ERR "dest_arm_decode" "");
361
362val dest_thumb_decode =
363    HolKernel.dest_triop thumb_decode_tm (ERR "dest_thumb_decode" "");
364
365val dest_thumbee_decode =
366    HolKernel.dest_triop thumbee_decode_tm (ERR "dest_thumbee_decode" "");
367
368val dest_thumb2_decode =
369    HolKernel.dest_triop thumb2_decode_tm (ERR "dest_thumb2_decode" "");
370
371val can = Lib.can
372
373val is_error      = can dest_error
374val is_valuestate = can dest_valuestate
375
376val is_constT = can dest_constT
377val is_seqT   = can dest_seqT
378val is_parT   = can dest_parT
379val is_forT   = can dest_forT
380val is_readT  = can dest_readT
381val is_writeT = can dest_writeT
382
383val is_read__reg      = can dest_read__reg
384val is_write__reg     = can dest_write__reg
385val is_read__psr      = can dest_read__psr
386val is_write__psr     = can dest_write__psr
387val is_read_reg_mode  = can dest_read_reg_mode
388val is_write_reg_mode = can dest_write_reg_mode
389val is_read_reg       = can dest_read_reg
390val is_write_reg      = can dest_write_reg
391val is_read_cpsr      = can dest_read_cpsr
392val is_write_cpsr     = can dest_write_cpsr
393val is_read_spsr      = can dest_read_spsr
394val is_write_spsr     = can dest_write_spsr
395val is_read_memA      = can dest_read_memA
396val is_write_memA     = can dest_write_memA
397val is_decode_psr     = can dest_decode_psr
398val is_bytes          = can dest_bytes
399val is_align          = can dest_align
400val is_aligned        = can dest_aligned
401val is_ITAdvance      = can dest_ITAdvance
402
403val is_clear_event_register     = can dest_clear_event_register
404val is_send_event               = can dest_send_event
405val is_wait_for_interrupt       = can dest_wait_for_interrupt
406val is_clear_wait_for_interrupt = can dest_clear_wait_for_interrupt;
407
408val is_arm_decode     = can dest_arm_decode
409val is_thumb_decode   = can dest_thumb_decode
410val is_thumbee_decode = can dest_thumbee_decode
411val is_thumb2_decode  = can dest_thumb2_decode;
412
413end
414