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 bit_count_tm        = mk_core_const "bit_count"
77val Encoding_ARM_tm     = mk_core_const "Encoding_ARM"
78val Encoding_Thumb_tm   = mk_core_const "Encoding_Thumb"
79val Encoding_Thumb2_tm  = mk_core_const "Encoding_Thumb2"
80val Encoding_ThumbEE_tm = mk_core_const "Encoding_ThumbEE"
81val ITAdvance_tm        = mk_core_const "ITAdvance"
82val NoInterrupt_tm      = mk_core_const "NoInterrupt"
83val HW_Reset_tm         = mk_core_const "HW_Reset"
84val HW_Fiq_tm           = mk_core_const "HW_Fiq"
85val HW_Irq_tm           = mk_core_const "HW_Irq"
86
87val arm_decode_tm       = mk_decode_const "arm_decode"
88val thumb_decode_tm     = mk_decode_const "thumb_decode"
89val thumbee_decode_tm   = mk_decode_const "thumbee_decode"
90val thumb2_decode_tm    = mk_decode_const "thumb2_decode";
91
92fun mk_error s =
93  HolKernel.mk_comb(error_tm,
94    Term.inst [Type.alpha |-> stringSyntax.string_ty] s)
95  handle HOL_ERR _ => raise ERR "mk_error" "";
96
97fun mk_valuestate (v,s) =
98  HolKernel.list_mk_comb(Term.inst
99    [Type.alpha |-> Term.type_of v,
100     Type.beta |-> Term.type_of s] valuestate_tm, [v,s])
101  handle HOL_ERR _ => raise ERR "mk_valuestate" "";
102
103fun mk_constT t =
104  HolKernel.mk_comb(Term.inst[Type.alpha |-> Term.type_of t] constT_tm,t)
105  handle HOL_ERR _ => raise ERR "mk_constT" "";
106
107fun mk_seqT (f,g) =
108  HolKernel.list_mk_comb(Term.inst
109    [Type.alpha |-> dest_monad_type (Term.type_of f),
110     Type.beta  |-> (dest_monad_type o snd o Type.dom_rng o Term.type_of) g]
111     seqT_tm, [f,g])
112  handle HOL_ERR _ => raise ERR "mk_seqT" "";
113
114fun mk_parT (f,g) =
115  HolKernel.list_mk_comb(Term.inst
116    [Type.alpha |-> dest_monad_type (Term.type_of f),
117     Type.beta  |-> dest_monad_type (Term.type_of g)] parT_tm,[f,g])
118  handle HOL_ERR _ => raise ERR "mk_parT" "";
119
120fun mk_forT (l,h,f) =
121  HolKernel.list_mk_comb(Term.inst
122    [Type.alpha |-> (dest_monad_type o snd o Type.dom_rng o Term.type_of) f]
123    forT_tm,[l,h,f])
124  handle HOL_ERR _ => raise ERR "mk_forT" "";
125
126fun mk_readT f =
127  HolKernel.mk_comb(Term.inst
128    [Type.alpha |-> snd (dom_rng (Term.type_of f))] readT_tm, f)
129  handle HOL_ERR _ => raise ERR "mk_readT" "";
130
131fun mk_writeT f =
132  HolKernel.mk_comb(writeT_tm, f)
133  handle HOL_ERR _ => raise ERR "mk_writeT" "";
134
135fun mk_read__reg (ii,r) =
136  HolKernel.list_mk_comb(read__reg_tm,
137    [Term.inst [Type.alpha |-> ``:iiid``] ii,
138     Term.inst [Type.alpha |-> ``:RName``] r])
139  handle HOL_ERR _ => raise ERR "mk_read__reg" "";
140
141fun mk_write__reg (ii,r,v) =
142  HolKernel.list_mk_comb(write__reg_tm,
143    [Term.inst [Type.alpha |-> ``:iiid``] ii,
144     Term.inst [Type.alpha |-> ``:RName``] r,
145     inst_word_alpha ``:32`` v])
146  handle HOL_ERR _ => raise ERR "mk_write__reg" "";
147
148fun mk_read__psr (ii,r) =
149  HolKernel.list_mk_comb(read__psr_tm,
150    [Term.inst [Type.alpha |-> ``:iiid``] ii,
151     Term.inst [Type.alpha |-> ``:PSRName``] r])
152  handle HOL_ERR _ => raise ERR "mk_read__psr" "";
153
154fun mk_write__psr (ii,r,v) =
155  HolKernel.list_mk_comb(write__psr_tm,
156    [Term.inst [Type.alpha |-> ``:iiid``] ii,
157     Term.inst [Type.alpha |-> ``:PSRName``] r,
158     Term.inst [Type.alpha |-> ``:ARMpsr``] v])
159  handle HOL_ERR _ => raise ERR "mk_write__psr" "";
160
161fun mk_read_reg (ii,n) =
162  HolKernel.list_mk_comb(read_reg_tm,
163    [Term.inst [Type.alpha |-> ``:iiid``] ii,
164     inst_word_alpha ``:4`` n])
165  handle HOL_ERR _ => raise ERR "mk_read_reg" "";
166
167fun mk_write_reg (ii,n,v) =
168  HolKernel.list_mk_comb(write_reg_tm,
169    [Term.inst [Type.alpha |-> ``:iiid``] ii,
170     inst_word_alpha ``:4`` n,
171     inst_word_alpha ``:32`` v])
172  handle HOL_ERR _ => raise ERR "mk_write_reg" "";
173
174fun mk_read_reg_mode (ii,n,m) =
175  HolKernel.list_mk_comb(read_reg_mode_tm,
176    [Term.inst [Type.alpha |-> ``:iiid``] ii,
177     pairSyntax.mk_pair
178       (inst_word_alpha ``:4`` n, inst_word_alpha ``:5`` m)])
179  handle HOL_ERR _ => raise ERR "mk_read_reg_mode" "";
180
181fun mk_write_reg_mode (ii,n,m,v) =
182  HolKernel.list_mk_comb(write_reg_mode_tm,
183    [Term.inst [Type.alpha |-> ``:iiid``] ii,
184     pairSyntax.mk_pair
185       (inst_word_alpha ``:4`` n, inst_word_alpha ``:5`` m),
186     inst_word_alpha ``:32`` v])
187  handle HOL_ERR _ => raise ERR "mk_write_reg_mode" "";
188
189fun mk_read_cpsr ii =
190  HolKernel.mk_comb(read_cpsr_tm, Term.inst [Type.alpha |-> ``:iiid``] ii)
191  handle HOL_ERR _ => raise ERR "mk_read_cpsr" "";
192
193fun mk_write_cpsr (ii,v) =
194  HolKernel.list_mk_comb(write_cpsr_tm,
195    [Term.inst [Type.alpha |-> ``:iiid``] ii,
196     Term.inst [Type.alpha |-> ``:ARMpsr``] v])
197  handle HOL_ERR _ => raise ERR "mk_write_cpsr" "";
198
199fun mk_read_spsr ii =
200  HolKernel.mk_comb(read_spsr_tm, Term.inst [Type.alpha |-> ``:iiid``] ii)
201  handle HOL_ERR _ => raise ERR "mk_read_spsr" "";
202
203fun mk_write_spsr (ii,v) =
204  HolKernel.list_mk_comb(write_spsr_tm,
205    [Term.inst [Type.alpha |-> ``:iiid``] ii,
206     Term.inst [Type.alpha |-> ``:ARMpsr``] v])
207  handle HOL_ERR _ => raise ERR "mk_write_spsr" "";
208
209fun mk_read_memA (ii,a,s) =
210  HolKernel.list_mk_comb(read_memA_tm,
211    [Term.inst [Type.alpha |-> ``:iiid``] ii,
212     pairSyntax.mk_pair
213       (inst_word_alpha ``:32`` a,
214        Term.inst [Type.alpha |-> ``:num``] s)])
215  handle HOL_ERR _ => raise ERR "mk_read_memA" "";
216
217fun mk_write_memA (ii,a,s,v) =
218  HolKernel.list_mk_comb(write_memA_tm,
219    [Term.inst [Type.alpha |-> ``:iiid``] ii,
220     pairSyntax.mk_pair
221       (inst_word_alpha ``:32`` a,
222        Term.inst [Type.alpha |-> ``:num``] s),
223     v])
224  handle HOL_ERR _ => raise ERR "mk_write_memA" "";
225
226fun mk_clear_event_register ii =
227  HolKernel.mk_comb(clear_event_register_tm,
228    Term.inst [Type.alpha |-> ``:iiid``] ii)
229  handle HOL_ERR _ => raise ERR "mk_clear_event_register" "";
230
231fun mk_send_event ii =
232  HolKernel.mk_comb(send_event_tm, Term.inst [Type.alpha |-> ``:iiid``] ii)
233  handle HOL_ERR _ => raise ERR "mk_send_event" "";
234
235fun mk_wait_for_interrupt ii =
236  HolKernel.mk_comb(wait_for_interrupt_tm,
237    Term.inst [Type.alpha |-> ``:iiid``] ii)
238  handle HOL_ERR _ => raise ERR "mk_wait_for_interrupt" "";
239
240fun mk_clear_wait_for_interrupt ii =
241  HolKernel.mk_comb(clear_wait_for_interrupt_tm,
242    Term.inst [Type.alpha |-> ``:iiid``] ii)
243  handle HOL_ERR _ => raise ERR "mk_clear_wait_for_interrupt" "";
244
245fun mk_decode_psr w =
246  HolKernel.mk_comb(decode_psr_tm, inst_word_alpha ``:32`` w)
247  handle HOL_ERR _ => raise ERR "mk_decode_psr" "";
248
249fun mk_bytes (w,n) =
250  HolKernel.mk_comb(bytes_tm, pairSyntax.mk_pair(inst_word_alpha ``:32`` w, n))
251  handle HOL_ERR _ => raise ERR "mk_bytes" "";
252
253fun mk_align (w,n) =
254  HolKernel.mk_comb(Term.inst
255    [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] align_tm,
256    pairSyntax.mk_pair(w, n))
257  handle HOL_ERR _ => raise ERR "mk_align" "";
258
259fun mk_aligned (w,n) =
260  HolKernel.mk_comb(Term.inst
261    [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] aligned_tm,
262    pairSyntax.mk_pair(w, n))
263  handle HOL_ERR _ => raise ERR "mk_aligned" "";
264
265fun mk_bit_count w =
266  HolKernel.mk_comb(Term.inst
267  [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] bit_count_tm, w)
268  handle HOL_ERR _ => raise ERR "mk_bit_count" "";
269
270fun mk_ITAdvance w =
271  HolKernel.mk_comb(Term.inst
272  [Type.alpha |-> wordsSyntax.dest_word_type (Term.type_of w)] ITAdvance_tm, w)
273  handle HOL_ERR _ => raise ERR "mk_ITAdvance" "";
274
275fun mk_read_memA_1 (ii,a) = mk_read_memA (ii,a,``1n``);
276
277fun mk_write_memA_1 (ii,a,v) =
278   mk_write_memA (ii,a,``1n``,listSyntax.mk_list([v],``:word8``));
279
280fun mk_read_memA_2 (ii,a) = mk_read_memA (ii,a,``2n``);
281fun mk_write_memA_2 (ii,a,v) = mk_write_memA (ii,a,``2n``,mk_bytes(v,``2n``));
282fun mk_read_memA_4 (ii,a) = mk_read_memA (ii,a,``4n``);
283fun mk_write_memA_4 (ii,a,v) = mk_write_memA (ii,a,``4n``,mk_bytes(v,``4n``));
284
285fun mk_arm_decode(b,w) =
286  HolKernel.list_mk_comb(arm_decode_tm, [b,inst_word_alpha ``:32`` w])
287  handle HOL_ERR _ => raise ERR "mk_arm_decode" "";
288
289fun mk_thumb_decode(a,itstate,w) =
290  HolKernel.list_mk_comb(thumb_decode_tm,
291    [a,inst_word_alpha ``:8`` itstate, inst_word_alpha ``:16`` w])
292  handle HOL_ERR _ => raise ERR "mk_thumb_decode" "";
293
294fun mk_thumbee_decode(a,itstate,w) =
295  HolKernel.list_mk_comb(thumbee_decode_tm,
296    [a,inst_word_alpha ``:8`` itstate, inst_word_alpha ``:16`` w])
297  handle HOL_ERR _ => raise ERR "mk_thumbee_decode" "";
298
299fun mk_thumb2_decode(a,itstate,w1,w2) =
300  HolKernel.list_mk_comb(thumb2_decode_tm,
301    [a,inst_word_alpha ``:8`` itstate,
302     pairSyntax.mk_pair
303       (inst_word_alpha ``:16`` w1,
304        inst_word_alpha ``:16`` w2)])
305  handle HOL_ERR _ => raise ERR "mk_thumb2_decode" "";
306
307val dest_error = HolKernel.dest_monop error_tm (ERR "dest_error" "")
308
309val dest_valuestate =
310  HolKernel.dest_binop valuestate_tm (ERR "dest_valuestate" "")
311
312val dest_constT = HolKernel.dest_monop constT_tm (ERR "dest_constT" "")
313val dest_seqT   = HolKernel.dest_binop seqT_tm   (ERR "dest_seqT" "")
314val dest_parT   = HolKernel.dest_binop parT_tm   (ERR "dest_parT" "")
315val dest_forT   = HolKernel.dest_triop forT_tm   (ERR "dest_forT" "")
316val dest_readT  = HolKernel.dest_monop readT_tm  (ERR "dest_readT" "")
317val dest_writeT = HolKernel.dest_monop writeT_tm (ERR "dest_writeT" "")
318
319val dest_read__reg =
320  HolKernel.dest_binop read__reg_tm  (ERR "dest_read__reg" "")
321
322val dest_write__reg =
323  HolKernel.dest_triop write__reg_tm (ERR "dest_write__reg" "")
324
325val dest_read__psr =
326  HolKernel.dest_binop read__psr_tm  (ERR "dest_read__psr" "")
327
328val dest_write__psr =
329  HolKernel.dest_triop write__psr_tm (ERR "dest_write__psr" "")
330
331val dest_read_reg_mode =
332  HolKernel.dest_binop read_reg_mode_tm  (ERR "dest_read_reg_mode" "")
333
334val dest_write_reg_mode =
335  HolKernel.dest_triop write_reg_mode_tm (ERR "dest_write_reg_mode" "")
336
337val dest_read_reg   = dest_binop read_reg_tm   (ERR "dest_read_reg" "")
338val dest_write_reg  = dest_triop write_reg_tm  (ERR "dest_write_reg" "")
339val dest_read_cpsr  = dest_monop read_cpsr_tm  (ERR "dest_read_cpsr" "")
340val dest_write_cpsr = dest_binop write_cpsr_tm (ERR "dest_write_cpsr" "")
341val dest_read_spsr  = dest_monop read_spsr_tm  (ERR "dest_read_spsr" "")
342val dest_write_spsr = dest_binop write_spsr_tm (ERR "dest_write_spsr" "")
343val dest_read_memA  = dest_binop read_memA_tm  (ERR "dest_read_memA" "")
344val dest_write_memA = dest_triop write_memA_tm (ERR "dest_write_memA" "")
345val dest_decode_psr = dest_monop decode_psr_tm (ERR "dest_decode_psr" "")
346val dest_bytes      = dest_monop bytes_tm      (ERR "dest_bytes" "");
347val dest_align      = dest_monop align_tm      (ERR "dest_align" "");
348val dest_aligned    = dest_monop aligned_tm    (ERR "dest_align" "");
349val dest_bit_count  = dest_monop bit_count_tm  (ERR "dest_bit_count" "");
350val dest_ITAdvance  = dest_monop ITAdvance_tm  (ERR "dest_ITAdvance" "");
351
352val dest_clear_event_register =
353    HolKernel.dest_monop decode_psr_tm (ERR "dest_clear_event_register" "");
354
355val dest_send_event =
356    HolKernel.dest_monop send_event_tm (ERR "dest_send_event" "");
357
358val dest_wait_for_interrupt =
359    HolKernel.dest_monop wait_for_interrupt_tm
360    (ERR "dest_wait_for_interrupt" "");
361
362val dest_clear_wait_for_interrupt =
363    HolKernel.dest_monop clear_wait_for_interrupt_tm
364    (ERR "dest_clear_wait_for_interrupt" "");
365
366val dest_arm_decode =
367    HolKernel.dest_binop arm_decode_tm (ERR "dest_arm_decode" "");
368
369val dest_thumb_decode =
370    HolKernel.dest_triop thumb_decode_tm (ERR "dest_thumb_decode" "");
371
372val dest_thumbee_decode =
373    HolKernel.dest_triop thumbee_decode_tm (ERR "dest_thumbee_decode" "");
374
375val dest_thumb2_decode =
376    HolKernel.dest_triop thumb2_decode_tm (ERR "dest_thumb2_decode" "");
377
378val can = Lib.can
379
380val is_error      = can dest_error
381val is_valuestate = can dest_valuestate
382
383val is_constT = can dest_constT
384val is_seqT   = can dest_seqT
385val is_parT   = can dest_parT
386val is_forT   = can dest_forT
387val is_readT  = can dest_readT
388val is_writeT = can dest_writeT
389
390val is_read__reg      = can dest_read__reg
391val is_write__reg     = can dest_write__reg
392val is_read__psr      = can dest_read__psr
393val is_write__psr     = can dest_write__psr
394val is_read_reg_mode  = can dest_read_reg_mode
395val is_write_reg_mode = can dest_write_reg_mode
396val is_read_reg       = can dest_read_reg
397val is_write_reg      = can dest_write_reg
398val is_read_cpsr      = can dest_read_cpsr
399val is_write_cpsr     = can dest_write_cpsr
400val is_read_spsr      = can dest_read_spsr
401val is_write_spsr     = can dest_write_spsr
402val is_read_memA      = can dest_read_memA
403val is_write_memA     = can dest_write_memA
404val is_decode_psr     = can dest_decode_psr
405val is_bytes          = can dest_bytes
406val is_align          = can dest_align
407val is_aligned        = can dest_aligned
408val is_bit_count      = can dest_bit_count
409val is_ITAdvance      = can dest_ITAdvance
410
411val is_clear_event_register     = can dest_clear_event_register
412val is_send_event               = can dest_send_event
413val is_wait_for_interrupt       = can dest_wait_for_interrupt
414val is_clear_wait_for_interrupt = can dest_clear_wait_for_interrupt;
415
416val is_arm_decode     = can dest_arm_decode
417val is_thumb_decode   = can dest_thumb_decode
418val is_thumbee_decode = can dest_thumbee_decode
419val is_thumb2_decode  = can dest_thumb2_decode;
420
421end
422