]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_translation.ml
91c34be529461ee5a03d1aafd37d7991f4266250
[helm.git] / helm / software / matita / contribs / assembly / freescale / freescale_ocaml / matita_freescale_translation.ml
1 let opcode_table =
2 (function m -> 
3 (match m with 
4    Matita_freescale_opcode.HC05 -> Obj.magic (Matita_freescale_table_HC05.opcode_table_HC05)
5  | Matita_freescale_opcode.HC08 -> Obj.magic (Matita_freescale_table_HC08.opcode_table_HC08)
6  | Matita_freescale_opcode.HCS08 -> Obj.magic (Matita_freescale_table_HCS08.opcode_table_HCS08)
7  | Matita_freescale_opcode.RS08 -> Obj.magic (Matita_freescale_table_RS08.opcode_table_RS08))
8 )
9 ;;
10
11 let full_info_of_word16 =
12 (function m -> (function borw -> (let rec aux = 
13 (function param -> 
14 (match param with 
15    Matita_list_list.Nil -> (Matita_datatypes_constructors.None)
16  | Matita_list_list.Cons(hd,tl) -> 
17 (match (Matita_freescale_extra.thd4T hd) with 
18    Matita_freescale_opcode.Byte(b) -> 
19 (match borw with 
20    Matita_freescale_opcode.Byte(borw') -> 
21 (match (Matita_freescale_byte8.eq_b8 borw' b) with 
22    Matita_datatypes_bool.True -> (Matita_datatypes_constructors.Some(hd))
23  | Matita_datatypes_bool.False -> (aux tl))
24
25  | Matita_freescale_opcode.Word(_) -> (aux tl))
26
27  | Matita_freescale_opcode.Word(w) -> 
28 (match borw with 
29    Matita_freescale_opcode.Byte(_) -> (aux tl)
30  | Matita_freescale_opcode.Word(borw') -> 
31 (match (Matita_freescale_word16.eq_w16 borw' w) with 
32    Matita_datatypes_bool.True -> (Matita_datatypes_constructors.Some(hd))
33  | Matita_datatypes_bool.False -> (aux tl))
34 )
35 )
36 )
37 ) in aux (opcode_table m))))
38 ;;
39
40 type t_byte8 =
41 TByte of Matita_freescale_byte8.byte8
42 ;;
43
44 let t_byte8_rec =
45 (function m -> (function f -> (function t -> 
46 (match t with 
47    TByte(b) -> (f b))
48 )))
49 ;;
50
51 let t_byte8_rect =
52 (function m -> (function f -> (function t -> 
53 (match t with 
54    TByte(b) -> (f b))
55 )))
56 ;;
57
58 let t_byte8_OF_bitrigesim =
59 (function a -> (function m -> (TByte((Matita_freescale_aux_bases.byte8_of_bitrigesim a)))))
60 ;;
61
62 type mA_check =
63 MaINH
64  | MaINHA
65  | MaINHX
66  | MaINHH
67  | MaINHX0ADD
68  | MaINHX1ADD of Matita_freescale_byte8.byte8
69  | MaINHX2ADD of Matita_freescale_word16.word16
70  | MaIMM1 of Matita_freescale_byte8.byte8
71  | MaIMM1EXT of Matita_freescale_byte8.byte8
72  | MaIMM2 of Matita_freescale_word16.word16
73  | MaDIR1 of Matita_freescale_byte8.byte8
74  | MaDIR2 of Matita_freescale_word16.word16
75  | MaIX0
76  | MaIX1 of Matita_freescale_byte8.byte8
77  | MaIX2 of Matita_freescale_word16.word16
78  | MaSP1 of Matita_freescale_byte8.byte8
79  | MaSP2 of Matita_freescale_word16.word16
80  | MaDIR1_to_DIR1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
81  | MaIMM1_to_DIR1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
82  | MaIX0p_to_DIR1 of Matita_freescale_byte8.byte8
83  | MaDIR1_to_IX0p of Matita_freescale_byte8.byte8
84  | MaINHA_and_IMM1 of Matita_freescale_byte8.byte8
85  | MaINHX_and_IMM1 of Matita_freescale_byte8.byte8
86  | MaIMM1_and_IMM1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
87  | MaDIR1_and_IMM1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
88  | MaIX0_and_IMM1 of Matita_freescale_byte8.byte8
89  | MaIX0p_and_IMM1 of Matita_freescale_byte8.byte8
90  | MaIX1_and_IMM1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
91  | MaIX1p_and_IMM1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
92  | MaSP1_and_IMM1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
93  | MaDIRn of Matita_freescale_aux_bases.oct * Matita_freescale_byte8.byte8
94  | MaDIRn_and_IMM1 of Matita_freescale_aux_bases.oct * Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8
95  | MaTNY of Matita_freescale_exadecim.exadecim
96  | MaSRT of Matita_freescale_aux_bases.bitrigesim
97 ;;
98
99 let mA_check_rec =
100 (function p -> (function p1 -> (function p2 -> (function p3 -> (function p4 -> (function f -> (function f1 -> (function f2 -> (function f3 -> (function f4 -> (function f5 -> (function f6 -> (function p5 -> (function f7 -> (function f8 -> (function f9 -> (function f10 -> (function f11 -> (function f12 -> (function f13 -> (function f14 -> (function f15 -> (function f16 -> (function f17 -> (function f18 -> (function f19 -> (function f20 -> (function f21 -> (function f22 -> (function f23 -> (function f24 -> (function f25 -> (function f26 -> (function f27 -> (function i -> (function m -> 
101 (match m with 
102    MaINH -> p
103  | MaINHA -> p1
104  | MaINHX -> p2
105  | MaINHH -> p3
106  | MaINHX0ADD -> p4
107  | MaINHX1ADD(b) -> (f b)
108  | MaINHX2ADD(w) -> (f1 w)
109  | MaIMM1(b) -> (f2 b)
110  | MaIMM1EXT(b) -> (f3 b)
111  | MaIMM2(w) -> (f4 w)
112  | MaDIR1(b) -> (f5 b)
113  | MaDIR2(w) -> (f6 w)
114  | MaIX0 -> p5
115  | MaIX1(b) -> (f7 b)
116  | MaIX2(w) -> (f8 w)
117  | MaSP1(b) -> (f9 b)
118  | MaSP2(w) -> (f10 w)
119  | MaDIR1_to_DIR1(b,b1) -> (f11 b b1)
120  | MaIMM1_to_DIR1(b,b1) -> (f12 b b1)
121  | MaIX0p_to_DIR1(b) -> (f13 b)
122  | MaDIR1_to_IX0p(b) -> (f14 b)
123  | MaINHA_and_IMM1(b) -> (f15 b)
124  | MaINHX_and_IMM1(b) -> (f16 b)
125  | MaIMM1_and_IMM1(b,b1) -> (f17 b b1)
126  | MaDIR1_and_IMM1(b,b1) -> (f18 b b1)
127  | MaIX0_and_IMM1(b) -> (f19 b)
128  | MaIX0p_and_IMM1(b) -> (f20 b)
129  | MaIX1_and_IMM1(b,b1) -> (f21 b b1)
130  | MaIX1p_and_IMM1(b,b1) -> (f22 b b1)
131  | MaSP1_and_IMM1(b,b1) -> (f23 b b1)
132  | MaDIRn(o,b) -> (f24 o b)
133  | MaDIRn_and_IMM1(o,b,b1) -> (f25 o b b1)
134  | MaTNY(e) -> (f26 e)
135  | MaSRT(b) -> (f27 b))
136 ))))))))))))))))))))))))))))))))))))
137 ;;
138
139 let mA_check_rect =
140 (function p -> (function p1 -> (function p2 -> (function p3 -> (function p4 -> (function f -> (function f1 -> (function f2 -> (function f3 -> (function f4 -> (function f5 -> (function f6 -> (function p5 -> (function f7 -> (function f8 -> (function f9 -> (function f10 -> (function f11 -> (function f12 -> (function f13 -> (function f14 -> (function f15 -> (function f16 -> (function f17 -> (function f18 -> (function f19 -> (function f20 -> (function f21 -> (function f22 -> (function f23 -> (function f24 -> (function f25 -> (function f26 -> (function f27 -> (function i -> (function m -> 
141 (match m with 
142    MaINH -> p
143  | MaINHA -> p1
144  | MaINHX -> p2
145  | MaINHH -> p3
146  | MaINHX0ADD -> p4
147  | MaINHX1ADD(b) -> (f b)
148  | MaINHX2ADD(w) -> (f1 w)
149  | MaIMM1(b) -> (f2 b)
150  | MaIMM1EXT(b) -> (f3 b)
151  | MaIMM2(w) -> (f4 w)
152  | MaDIR1(b) -> (f5 b)
153  | MaDIR2(w) -> (f6 w)
154  | MaIX0 -> p5
155  | MaIX1(b) -> (f7 b)
156  | MaIX2(w) -> (f8 w)
157  | MaSP1(b) -> (f9 b)
158  | MaSP2(w) -> (f10 w)
159  | MaDIR1_to_DIR1(b,b1) -> (f11 b b1)
160  | MaIMM1_to_DIR1(b,b1) -> (f12 b b1)
161  | MaIX0p_to_DIR1(b) -> (f13 b)
162  | MaDIR1_to_IX0p(b) -> (f14 b)
163  | MaINHA_and_IMM1(b) -> (f15 b)
164  | MaINHX_and_IMM1(b) -> (f16 b)
165  | MaIMM1_and_IMM1(b,b1) -> (f17 b b1)
166  | MaDIR1_and_IMM1(b,b1) -> (f18 b b1)
167  | MaIX0_and_IMM1(b) -> (f19 b)
168  | MaIX0p_and_IMM1(b) -> (f20 b)
169  | MaIX1_and_IMM1(b,b1) -> (f21 b b1)
170  | MaIX1p_and_IMM1(b,b1) -> (f22 b b1)
171  | MaSP1_and_IMM1(b,b1) -> (f23 b b1)
172  | MaDIRn(o,b) -> (f24 o b)
173  | MaDIRn_and_IMM1(o,b,b1) -> (f25 o b b1)
174  | MaTNY(e) -> (f26 e)
175  | MaSRT(b) -> (f27 b))
176 ))))))))))))))))))))))))))))))))))))
177 ;;
178
179 type instruction =
180 Instr of Matita_freescale_opcode.instr_mode * Matita_freescale_opcode.opcode * mA_check
181 ;;
182
183 let instruction_rec =
184 (function f -> (function i -> 
185 (match i with 
186    Instr(i1,o,m) -> (f i1 o m))
187 ))
188 ;;
189
190 let instruction_rect =
191 (function f -> (function i -> 
192 (match i with 
193    Instr(i1,o,m) -> (f i1 o m))
194 ))
195 ;;
196
197 let args_picker =
198 (function m -> (function i -> (function args -> 
199 (match args with 
200    MaINH -> Obj.magic ((Matita_list_list.Nil))
201  | MaINHA -> Obj.magic ((Matita_list_list.Nil))
202  | MaINHX -> Obj.magic ((Matita_list_list.Nil))
203  | MaINHH -> Obj.magic ((Matita_list_list.Nil))
204  | MaINHX0ADD -> Obj.magic ((Matita_list_list.Nil))
205  | MaINHX1ADD(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
206  | MaINHX2ADD(w) -> Obj.magic ((Matita_list_list.Cons((TByte((Matita_freescale_word16.w16h w))),(Matita_list_list.Cons((TByte((Matita_freescale_word16.w16l w))),(Matita_list_list.Nil))))))
207  | MaIMM1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
208  | MaIMM1EXT(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
209  | MaIMM2(w) -> Obj.magic ((Matita_list_list.Cons((TByte((Matita_freescale_word16.w16h w))),(Matita_list_list.Cons((TByte((Matita_freescale_word16.w16l w))),(Matita_list_list.Nil))))))
210  | MaDIR1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
211  | MaDIR2(w) -> Obj.magic ((Matita_list_list.Cons((TByte((Matita_freescale_word16.w16h w))),(Matita_list_list.Cons((TByte((Matita_freescale_word16.w16l w))),(Matita_list_list.Nil))))))
212  | MaIX0 -> Obj.magic ((Matita_list_list.Nil))
213  | MaIX1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
214  | MaIX2(w) -> Obj.magic ((Matita_list_list.Cons((TByte((Matita_freescale_word16.w16h w))),(Matita_list_list.Cons((TByte((Matita_freescale_word16.w16l w))),(Matita_list_list.Nil))))))
215  | MaSP1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
216  | MaSP2(w) -> Obj.magic ((Matita_list_list.Cons((TByte((Matita_freescale_word16.w16h w))),(Matita_list_list.Cons((TByte((Matita_freescale_word16.w16l w))),(Matita_list_list.Nil))))))
217  | MaDIR1_to_DIR1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil))))))
218  | MaIMM1_to_DIR1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil))))))
219  | MaIX0p_to_DIR1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
220  | MaDIR1_to_IX0p(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
221  | MaINHA_and_IMM1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
222  | MaINHX_and_IMM1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
223  | MaIMM1_and_IMM1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil))))))
224  | MaDIR1_and_IMM1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil))))))
225  | MaIX0_and_IMM1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
226  | MaIX0p_and_IMM1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
227  | MaIX1_and_IMM1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil))))))
228  | MaIX1p_and_IMM1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil))))))
229  | MaSP1_and_IMM1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil))))))
230  | MaDIRn(_,b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil))))
231  | MaDIRn_and_IMM1(_,b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil))))))
232  | MaTNY(_) -> Obj.magic ((Matita_list_list.Nil))
233  | MaSRT(_) -> Obj.magic ((Matita_list_list.Nil)))
234 )))
235 ;;
236
237 let bytes_of_pseudo_instr_mode_param =
238 (function m -> (function o -> (function i -> (function p -> (let rec aux = 
239 (function param -> 
240 (match param with 
241    Matita_list_list.Nil -> (Matita_datatypes_constructors.None)
242  | Matita_list_list.Cons(hd,tl) -> 
243 (match (Matita_freescale_extra.and_bool (Matita_freescale_opcode.eqop m o (Matita_freescale_extra.fst4T hd)) (Matita_freescale_opcode.eqim i (Matita_freescale_extra.snd4T hd))) with 
244    Matita_datatypes_bool.True -> 
245 (match (Matita_freescale_extra.thd4T hd) with 
246    Matita_freescale_opcode.Byte(isab) -> (Matita_datatypes_constructors.Some((Matita_list_list.append (Matita_list_list.Cons((TByte(isab)),(Matita_list_list.Nil))) (args_picker m i p))))
247  | Matita_freescale_opcode.Word(isaw) -> (Matita_datatypes_constructors.Some((Matita_list_list.append (Matita_list_list.Cons((TByte((Matita_freescale_word16.w16h isaw))),(Matita_list_list.Cons((TByte((Matita_freescale_word16.w16l isaw))),(Matita_list_list.Nil))))) (args_picker m i p)))))
248
249  | Matita_datatypes_bool.False -> (aux tl))
250 )
251 ) in aux (opcode_table m))))))
252 ;;
253
254 let opcode_to_any =
255 (function m -> (function o -> (Matita_freescale_opcode.AnyOP(o))))
256 ;;
257
258 let compile =
259 (function mcu -> (function i -> (function op -> (function arg -> (let res = (bytes_of_pseudo_instr_mode_param mcu (opcode_to_any mcu op) i arg) in (let value = (
260 (match res with 
261    Matita_datatypes_constructors.None -> Obj.magic ((Matita_logic_connectives.false_rect))
262  | Matita_datatypes_constructors.Some(v) -> Obj.magic (v))
263 ) in value))))))
264 ;;
265
266 let source_to_byte8 =
267 (function mcu -> 
268 (match mcu with 
269    Matita_freescale_opcode.HC05 -> Obj.magic ((function l -> (let rec aux = 
270 (function p1 -> (function p2 -> 
271 (match p1 with 
272    Matita_list_list.Nil -> p2
273  | Matita_list_list.Cons(hd,tl) -> 
274 (match hd with 
275    TByte(b) -> (aux tl (Matita_list_list.append p2 (Matita_list_list.Cons(b,(Matita_list_list.Nil))))))
276 )
277 )) in aux l (Matita_list_list.Nil))))
278  | Matita_freescale_opcode.HC08 -> Obj.magic ((function l -> (let rec aux = 
279 (function p1 -> (function p2 -> 
280 (match p1 with 
281    Matita_list_list.Nil -> p2
282  | Matita_list_list.Cons(hd,tl) -> 
283 (match hd with 
284    TByte(b) -> (aux tl (Matita_list_list.append p2 (Matita_list_list.Cons(b,(Matita_list_list.Nil))))))
285 )
286 )) in aux l (Matita_list_list.Nil))))
287  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function l -> (let rec aux = 
288 (function p1 -> (function p2 -> 
289 (match p1 with 
290    Matita_list_list.Nil -> p2
291  | Matita_list_list.Cons(hd,tl) -> 
292 (match hd with 
293    TByte(b) -> (aux tl (Matita_list_list.append p2 (Matita_list_list.Cons(b,(Matita_list_list.Nil))))))
294 )
295 )) in aux l (Matita_list_list.Nil))))
296  | Matita_freescale_opcode.RS08 -> Obj.magic ((function l -> (let rec aux = 
297 (function p1 -> (function p2 -> 
298 (match p1 with 
299    Matita_list_list.Nil -> p2
300  | Matita_list_list.Cons(hd,tl) -> 
301 (match hd with 
302    TByte(b) -> (aux tl (Matita_list_list.append p2 (Matita_list_list.Cons(b,(Matita_list_list.Nil))))))
303 )
304 )) in aux l (Matita_list_list.Nil)))))
305 )
306 ;;
307