]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_word16.ml
069774afcb7d922e0772647f1d73653f8fe88739
[helm.git] / helm / software / matita / contribs / assembly / freescale / freescale_ocaml / matita_freescale_word16.ml
1 type word16 =
2 Mk_word16 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
3 ;;
4
5 let word16_rec =
6 (function f -> (function w -> 
7 (match w with 
8    Mk_word16(b,b1) -> (f b b1))
9 ))
10 ;;
11
12 let word16_rect =
13 (function f -> (function w -> 
14 (match w with 
15    Mk_word16(b,b1) -> (f b b1))
16 ))
17 ;;
18
19 let w16h =
20 (function w -> 
21 (match w with 
22    Mk_word16(w16h,w16l) -> w16h)
23 )
24 ;;
25
26 let w16l =
27 (function w -> 
28 (match w with 
29    Mk_word16(w16h,w16l) -> w16l)
30 )
31 ;;
32
33 let eq_w16 =
34 (function w1 -> (function w2 -> (Matita_freescale_extra.and_bool (Matita_freescale_byte8.eq_b8 (w16h w1) (w16h w2)) (Matita_freescale_byte8.eq_b8 (w16l w1) (w16l w2)))))
35 ;;
36
37 let lt_w16 =
38 (function w1 -> (function w2 -> 
39 (match (Matita_freescale_byte8.lt_b8 (w16h w1) (w16h w2)) with 
40    Matita_datatypes_bool.True -> Matita_datatypes_bool.True
41  | Matita_datatypes_bool.False -> 
42 (match (Matita_freescale_byte8.gt_b8 (w16h w1) (w16h w2)) with 
43    Matita_datatypes_bool.True -> Matita_datatypes_bool.False
44  | Matita_datatypes_bool.False -> (Matita_freescale_byte8.lt_b8 (w16l w1) (w16l w2)))
45 )
46 ))
47 ;;
48
49 let le_w16 =
50 (function w1 -> (function w2 -> (Matita_freescale_extra.or_bool (eq_w16 w1 w2) (lt_w16 w1 w2))))
51 ;;
52
53 let gt_w16 =
54 (function w1 -> (function w2 -> (Matita_freescale_extra.not_bool (le_w16 w1 w2))))
55 ;;
56
57 let ge_w16 =
58 (function w1 -> (function w2 -> (Matita_freescale_extra.not_bool (lt_w16 w1 w2))))
59 ;;
60
61 let and_w16 =
62 (function w1 -> (function w2 -> (Mk_word16((Matita_freescale_byte8.and_b8 (w16h w1) (w16h w2)),(Matita_freescale_byte8.and_b8 (w16l w1) (w16l w2))))))
63 ;;
64
65 let or_w16 =
66 (function w1 -> (function w2 -> (Mk_word16((Matita_freescale_byte8.or_b8 (w16h w1) (w16h w2)),(Matita_freescale_byte8.or_b8 (w16l w1) (w16l w2))))))
67 ;;
68
69 let xor_w16 =
70 (function w1 -> (function w2 -> (Mk_word16((Matita_freescale_byte8.xor_b8 (w16h w1) (w16h w2)),(Matita_freescale_byte8.xor_b8 (w16l w1) (w16l w2))))))
71 ;;
72
73 let rcr_w16 =
74 (function w -> (function c -> 
75 (match (Matita_freescale_byte8.rcr_b8 (w16h w) c) with 
76    Matita_datatypes_constructors.Pair(wh',c') -> 
77 (match (Matita_freescale_byte8.rcr_b8 (w16l w) c') with 
78    Matita_datatypes_constructors.Pair(wl',c'') -> (Matita_datatypes_constructors.Pair((Mk_word16(wh',wl')),c'')))
79 )
80 ))
81 ;;
82
83 let shr_w16 =
84 (function w -> 
85 (match (Matita_freescale_byte8.rcr_b8 (w16h w) Matita_datatypes_bool.False) with 
86    Matita_datatypes_constructors.Pair(wh',c') -> 
87 (match (Matita_freescale_byte8.rcr_b8 (w16l w) c') with 
88    Matita_datatypes_constructors.Pair(wl',c'') -> (Matita_datatypes_constructors.Pair((Mk_word16(wh',wl')),c'')))
89 )
90 )
91 ;;
92
93 let ror_w16 =
94 (function w -> 
95 (match (Matita_freescale_byte8.rcr_b8 (w16h w) Matita_datatypes_bool.False) with 
96    Matita_datatypes_constructors.Pair(wh',c') -> 
97 (match (Matita_freescale_byte8.rcr_b8 (w16l w) c') with 
98    Matita_datatypes_constructors.Pair(wl',c'') -> 
99 (match c'' with 
100    Matita_datatypes_bool.True -> (Mk_word16((Matita_freescale_byte8.or_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)) wh'),wl'))
101  | Matita_datatypes_bool.False -> (Mk_word16(wh',wl')))
102 )
103 )
104 )
105 ;;
106
107 let ror_w16_n =
108 let rec ror_w16_n = 
109 (function w -> (function n -> 
110 (match n with 
111    Matita_nat_nat.O -> w
112  | Matita_nat_nat.S(n') -> (ror_w16_n (ror_w16 w) n'))
113 )) in ror_w16_n
114 ;;
115
116 let rcl_w16 =
117 (function w -> (function c -> 
118 (match (Matita_freescale_byte8.rcl_b8 (w16l w) c) with 
119    Matita_datatypes_constructors.Pair(wl',c') -> 
120 (match (Matita_freescale_byte8.rcl_b8 (w16h w) c') with 
121    Matita_datatypes_constructors.Pair(wh',c'') -> (Matita_datatypes_constructors.Pair((Mk_word16(wh',wl')),c'')))
122 )
123 ))
124 ;;
125
126 let shl_w16 =
127 (function w -> 
128 (match (Matita_freescale_byte8.rcl_b8 (w16l w) Matita_datatypes_bool.False) with 
129    Matita_datatypes_constructors.Pair(wl',c') -> 
130 (match (Matita_freescale_byte8.rcl_b8 (w16h w) c') with 
131    Matita_datatypes_constructors.Pair(wh',c'') -> (Matita_datatypes_constructors.Pair((Mk_word16(wh',wl')),c'')))
132 )
133 )
134 ;;
135
136 let rol_w16 =
137 (function w -> 
138 (match (Matita_freescale_byte8.rcl_b8 (w16l w) Matita_datatypes_bool.False) with 
139    Matita_datatypes_constructors.Pair(wl',c') -> 
140 (match (Matita_freescale_byte8.rcl_b8 (w16h w) c') with 
141    Matita_datatypes_constructors.Pair(wh',c'') -> 
142 (match c'' with 
143    Matita_datatypes_bool.True -> (Mk_word16(wh',(Matita_freescale_byte8.or_b8 (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X1)) wl')))
144  | Matita_datatypes_bool.False -> (Mk_word16(wh',wl')))
145 )
146 )
147 )
148 ;;
149
150 let rol_w16_n =
151 let rec rol_w16_n = 
152 (function w -> (function n -> 
153 (match n with 
154    Matita_nat_nat.O -> w
155  | Matita_nat_nat.S(n') -> (rol_w16_n (rol_w16 w) n'))
156 )) in rol_w16_n
157 ;;
158
159 let not_w16 =
160 (function w -> (Mk_word16((Matita_freescale_byte8.not_b8 (w16h w)),(Matita_freescale_byte8.not_b8 (w16l w)))))
161 ;;
162
163 let plus_w16 =
164 (function w1 -> (function w2 -> (function c -> 
165 (match (Matita_freescale_byte8.plus_b8 (w16l w1) (w16l w2) c) with 
166    Matita_datatypes_constructors.Pair(l,c') -> 
167 (match (Matita_freescale_byte8.plus_b8 (w16h w1) (w16h w2) c') with 
168    Matita_datatypes_constructors.Pair(h,c'') -> (Matita_datatypes_constructors.Pair((Mk_word16(h,l)),c'')))
169 )
170 )))
171 ;;
172
173 let plus_w16nc =
174 (function w1 -> (function w2 -> (Matita_datatypes_constructors.fst (plus_w16 w1 w2 Matita_datatypes_bool.False))))
175 ;;
176
177 let plus_w16c =
178 (function w1 -> (function w2 -> (Matita_datatypes_constructors.snd (plus_w16 w1 w2 Matita_datatypes_bool.False))))
179 ;;
180
181 let mSB_w16 =
182 (function w -> (Matita_freescale_exadecim.eq_ex Matita_freescale_exadecim.X8 (Matita_freescale_exadecim.and_ex Matita_freescale_exadecim.X8 (Matita_freescale_byte8.b8h (w16h w)))))
183 ;;
184
185 let nat_of_word16 =
186 (function w -> (Matita_nat_plus.plus (Matita_nat_times.times (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Matita_freescale_byte8.nat_of_byte8 (w16h w))) (Matita_freescale_byte8.nat_of_byte8 (w16l w))))
187 ;;
188
189 let word16_of_nat =
190 (function n -> (Mk_word16((Matita_freescale_byte8.byte8_of_nat (Matita_nat_div_and_mod.div n (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),(Matita_freescale_byte8.byte8_of_nat n))))
191 ;;
192
193 let pred_w16 =
194 (function w -> 
195 (match (Matita_freescale_byte8.eq_b8 (w16l w) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))) with 
196    Matita_datatypes_bool.True -> (Mk_word16((Matita_freescale_byte8.pred_b8 (w16h w)),(Matita_freescale_byte8.pred_b8 (w16l w))))
197  | Matita_datatypes_bool.False -> (Mk_word16((w16h w),(Matita_freescale_byte8.pred_b8 (w16l w)))))
198 )
199 ;;
200
201 let succ_w16 =
202 (function w -> 
203 (match (Matita_freescale_byte8.eq_b8 (w16l w) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF))) with 
204    Matita_datatypes_bool.True -> (Mk_word16((Matita_freescale_byte8.succ_b8 (w16h w)),(Matita_freescale_byte8.succ_b8 (w16l w))))
205  | Matita_datatypes_bool.False -> (Mk_word16((w16h w),(Matita_freescale_byte8.succ_b8 (w16l w)))))
206 )
207 ;;
208
209 let compl_w16 =
210 (function w -> 
211 (match (mSB_w16 w) with 
212    Matita_datatypes_bool.True -> (succ_w16 (not_w16 w))
213  | Matita_datatypes_bool.False -> (not_w16 (pred_w16 w)))
214 )
215 ;;
216
217 let mul_b8 =
218 (function b1 -> (function b2 -> 
219 (match b1 with 
220    Matita_freescale_byte8.Mk_byte8(b1h,b1l) -> 
221 (match b2 with 
222    Matita_freescale_byte8.Mk_byte8(b2h,b2l) -> 
223 (match (Matita_freescale_byte8.mul_ex b1l b2l) with 
224    Matita_freescale_byte8.Mk_byte8(t1_h,t1_l) -> 
225 (match (Matita_freescale_byte8.mul_ex b1h b2l) with 
226    Matita_freescale_byte8.Mk_byte8(t2_h,t2_l) -> 
227 (match (Matita_freescale_byte8.mul_ex b2h b1l) with 
228    Matita_freescale_byte8.Mk_byte8(t3_h,t3_l) -> 
229 (match (Matita_freescale_byte8.mul_ex b1h b2h) with 
230    Matita_freescale_byte8.Mk_byte8(t4_h,t4_l) -> (plus_w16nc (plus_w16nc (plus_w16nc (Mk_word16((Matita_freescale_byte8.Mk_byte8(t4_h,t4_l)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))) (Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,t3_h)),(Matita_freescale_byte8.Mk_byte8(t3_l,Matita_freescale_exadecim.X0))))) (Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,t2_h)),(Matita_freescale_byte8.Mk_byte8(t2_l,Matita_freescale_exadecim.X0))))) (Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(t1_h,t1_l))))))
231 )
232 )
233 )
234 )
235 )
236 ))
237 ;;
238
239 let div_b8 =
240 (function w -> (function b -> 
241 (match (Matita_freescale_byte8.eq_b8 b (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))) with 
242    Matita_datatypes_bool.True -> (Matita_freescale_extra.TripleT((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.XF,Matita_freescale_exadecim.XF)),(w16l w),Matita_datatypes_bool.True))
243  | Matita_datatypes_bool.False -> 
244 (match (eq_w16 w (Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))) with 
245    Matita_datatypes_bool.True -> (Matita_freescale_extra.TripleT((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),(Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),Matita_datatypes_bool.False))
246  | Matita_datatypes_bool.False -> (let rec aux = 
247 (function divd -> (function divs -> (function molt -> (function q -> (function c -> (let w' = (plus_w16nc divd (compl_w16 divs)) in 
248 (match c with 
249    Matita_nat_nat.O -> 
250 (match (le_w16 divs divd) with 
251    Matita_datatypes_bool.True -> (Matita_freescale_extra.TripleT((Matita_freescale_byte8.or_b8 molt q),(w16l w'),(Matita_freescale_extra.not_bool (Matita_freescale_byte8.eq_b8 (w16h w') (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0))))))
252  | Matita_datatypes_bool.False -> (Matita_freescale_extra.TripleT(q,(w16l divd),(Matita_freescale_extra.not_bool (Matita_freescale_byte8.eq_b8 (w16h divd) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)))))))
253
254  | Matita_nat_nat.S(c') -> 
255 (match (le_w16 divs divd) with 
256    Matita_datatypes_bool.True -> (aux w' (ror_w16 divs) (Matita_freescale_byte8.ror_b8 molt) (Matita_freescale_byte8.or_b8 molt q) c')
257  | Matita_datatypes_bool.False -> (aux divd (ror_w16 divs) (Matita_freescale_byte8.ror_b8 molt) q c'))
258 )
259 )))))) in aux w (rol_w16_n (Mk_word16((Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)),b)) (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X8,Matita_freescale_exadecim.X0)) (Matita_freescale_byte8.Mk_byte8(Matita_freescale_exadecim.X0,Matita_freescale_exadecim.X0)) (Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O))))))))))))))))
260 )
261 ))
262 ;;
263
264 let in_range =
265 (function x -> (function inf -> (function sup -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (le_w16 inf sup) (ge_w16 x inf)) (le_w16 x sup)))))
266 ;;
267
268 let forall_word16 =
269 (function p -> (Matita_freescale_byte8.forall_byte8 (function bh -> (Matita_freescale_byte8.forall_byte8 (function bl -> (p (Mk_word16(bh,bl))))))))
270 ;;
271