1structure integer_wordSyntax :> integer_wordSyntax =
2struct
3
4open HolKernel boolLib
5open wordsSyntax integer_wordTheory
6
7val ERR = Feedback.mk_HOL_ERR "integer_wordSyntax"
8
9fun syntax_fns n d m =
10   HolKernel.syntax_fns {n = n, dest = d, make = m} "integer_word"
11
12(*------------------------------------------------------------------------- *)
13
14val s = HolKernel.syntax_fns1 "integer_word"
15
16val (toString_tm, mk_toString, dest_toString, is_toString) = s "toString"
17
18val (fromString_tm, mk_fromString, dest_fromString, is_fromString) =
19    s "fromString"
20
21val (w2i_tm, mk_w2i, dest_w2i, is_w2i) = s "w2i"
22
23(* - - - - - - - - - - - - - - - - - - - - - - - *)
24
25val s = syntax_fns 1
26   (fn tm1 => fn e => boolSyntax.dest_itself o HolKernel.dest_monop tm1 e)
27   (fn tm => fn ty =>
28      Term.mk_comb (Term.inst [Type.alpha |-> ty] tm, boolSyntax.mk_itself ty))
29
30val (int_min_tm, mk_int_min, dest_int_min, is_int_min) = s "INT_MIN"
31val (int_max_tm, mk_int_max, dest_int_max, is_int_max) = s "INT_MAX"
32val (uint_max_tm, mk_uint_max, dest_uint_max, is_uint_max) = s "UINT_MAX"
33
34(* - - - - - - - - - - - - - - - - - - - - - - - *)
35
36val s = syntax_fns 1
37   (fn tm1 => fn e => fn w => (HolKernel.dest_monop tm1 e w, dim_of w))
38   (fn tm => fn (w, ty) => Term.mk_comb (Term.inst [Type.alpha |-> ty] tm, w))
39
40val (i2w_tm, mk_i2w, dest_i2w, is_i2w) = s "i2w"
41
42val (saturate_i2sw_tm, mk_saturate_i2sw,
43     dest_saturate_i2sw, is_saturate_i2sw) = s "saturate_i2sw"
44
45val (saturate_i2w_tm, mk_saturate_i2w, dest_saturate_i2w, is_saturate_i2w) =
46    s "saturate_i2w"
47
48(* - - - - - - - - - - - - - - - - - - - - - - - *)
49
50val s = syntax_fns 1
51   (fn tm1 => fn e => fn w => (HolKernel.dest_monop tm1 e w, dim_of w))
52   (fn tm => fn (w, ty) =>
53       Term.mk_comb (Term.inst [Type.alpha |-> wordsSyntax.dim_of w,
54                                Type.beta |-> ty] tm, w))
55
56val (saturate_sw2sw_tm, mk_saturate_sw2sw,
57     dest_saturate_sw2sw, is_saturate_sw2sw) = s "saturate_sw2sw"
58
59val (saturate_sw2w_tm, mk_saturate_sw2w,
60     dest_saturate_sw2w, is_saturate_sw2w) = s "saturate_sw2w"
61
62val (saturate_w2sw_tm, mk_saturate_w2sw,
63     dest_saturate_w2sw, is_saturate_w2sw) = s "saturate_w2sw"
64
65(* - - - - - - - - - - - - - - - - - - - - - - - *)
66
67val s = HolKernel.syntax_fns2 "integer_word"
68
69val (signed_saturate_add_tm, mk_signed_saturate_add,
70     dest_signed_saturate_add, is_signed_saturate_add) = s "signed_saturate_add"
71
72val (signed_saturate_sub_tm, mk_signed_saturate_sub,
73     dest_signed_saturate_sub, is_signed_saturate_sub) = s "signed_saturate_sub"
74
75val (word_sdiv_tm, mk_word_sdiv, dest_word_sdiv, is_word_sdiv) = s "word_sdiv"
76val (word_smod_tm, mk_word_smod, dest_word_smod, is_word_smod) = s "word_smod"
77
78(*------------------------------------------------------------------------- *)
79
80end
81