X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_freescale_translation.ml;fp=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_freescale_translation.ml;h=91c34be529461ee5a03d1aafd37d7991f4266250;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_translation.ml b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_translation.ml new file mode 100644 index 000000000..91c34be52 --- /dev/null +++ b/matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_translation.ml @@ -0,0 +1,307 @@ +let opcode_table = +(function m -> +(match m with + Matita_freescale_opcode.HC05 -> Obj.magic (Matita_freescale_table_HC05.opcode_table_HC05) + | Matita_freescale_opcode.HC08 -> Obj.magic (Matita_freescale_table_HC08.opcode_table_HC08) + | Matita_freescale_opcode.HCS08 -> Obj.magic (Matita_freescale_table_HCS08.opcode_table_HCS08) + | Matita_freescale_opcode.RS08 -> Obj.magic (Matita_freescale_table_RS08.opcode_table_RS08)) +) +;; + +let full_info_of_word16 = +(function m -> (function borw -> (let rec aux = +(function param -> +(match param with + Matita_list_list.Nil -> (Matita_datatypes_constructors.None) + | Matita_list_list.Cons(hd,tl) -> +(match (Matita_freescale_extra.thd4T hd) with + Matita_freescale_opcode.Byte(b) -> +(match borw with + Matita_freescale_opcode.Byte(borw') -> +(match (Matita_freescale_byte8.eq_b8 borw' b) with + Matita_datatypes_bool.True -> (Matita_datatypes_constructors.Some(hd)) + | Matita_datatypes_bool.False -> (aux tl)) + + | Matita_freescale_opcode.Word(_) -> (aux tl)) + + | Matita_freescale_opcode.Word(w) -> +(match borw with + Matita_freescale_opcode.Byte(_) -> (aux tl) + | Matita_freescale_opcode.Word(borw') -> +(match (Matita_freescale_word16.eq_w16 borw' w) with + Matita_datatypes_bool.True -> (Matita_datatypes_constructors.Some(hd)) + | Matita_datatypes_bool.False -> (aux tl)) +) +) +) +) in aux (opcode_table m)))) +;; + +type t_byte8 = +TByte of Matita_freescale_byte8.byte8 +;; + +let t_byte8_rec = +(function m -> (function f -> (function t -> +(match t with + TByte(b) -> (f b)) +))) +;; + +let t_byte8_rect = +(function m -> (function f -> (function t -> +(match t with + TByte(b) -> (f b)) +))) +;; + +let t_byte8_OF_bitrigesim = +(function a -> (function m -> (TByte((Matita_freescale_aux_bases.byte8_of_bitrigesim a))))) +;; + +type mA_check = +MaINH + | MaINHA + | MaINHX + | MaINHH + | MaINHX0ADD + | MaINHX1ADD of Matita_freescale_byte8.byte8 + | MaINHX2ADD of Matita_freescale_word16.word16 + | MaIMM1 of Matita_freescale_byte8.byte8 + | MaIMM1EXT of Matita_freescale_byte8.byte8 + | MaIMM2 of Matita_freescale_word16.word16 + | MaDIR1 of Matita_freescale_byte8.byte8 + | MaDIR2 of Matita_freescale_word16.word16 + | MaIX0 + | MaIX1 of Matita_freescale_byte8.byte8 + | MaIX2 of Matita_freescale_word16.word16 + | MaSP1 of Matita_freescale_byte8.byte8 + | MaSP2 of Matita_freescale_word16.word16 + | MaDIR1_to_DIR1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 + | MaIMM1_to_DIR1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 + | MaIX0p_to_DIR1 of Matita_freescale_byte8.byte8 + | MaDIR1_to_IX0p of Matita_freescale_byte8.byte8 + | MaINHA_and_IMM1 of Matita_freescale_byte8.byte8 + | MaINHX_and_IMM1 of Matita_freescale_byte8.byte8 + | MaIMM1_and_IMM1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 + | MaDIR1_and_IMM1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 + | MaIX0_and_IMM1 of Matita_freescale_byte8.byte8 + | MaIX0p_and_IMM1 of Matita_freescale_byte8.byte8 + | MaIX1_and_IMM1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 + | MaIX1p_and_IMM1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 + | MaSP1_and_IMM1 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 + | MaDIRn of Matita_freescale_aux_bases.oct * Matita_freescale_byte8.byte8 + | MaDIRn_and_IMM1 of Matita_freescale_aux_bases.oct * Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 + | MaTNY of Matita_freescale_exadecim.exadecim + | MaSRT of Matita_freescale_aux_bases.bitrigesim +;; + +let mA_check_rec = +(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 -> +(match m with + MaINH -> p + | MaINHA -> p1 + | MaINHX -> p2 + | MaINHH -> p3 + | MaINHX0ADD -> p4 + | MaINHX1ADD(b) -> (f b) + | MaINHX2ADD(w) -> (f1 w) + | MaIMM1(b) -> (f2 b) + | MaIMM1EXT(b) -> (f3 b) + | MaIMM2(w) -> (f4 w) + | MaDIR1(b) -> (f5 b) + | MaDIR2(w) -> (f6 w) + | MaIX0 -> p5 + | MaIX1(b) -> (f7 b) + | MaIX2(w) -> (f8 w) + | MaSP1(b) -> (f9 b) + | MaSP2(w) -> (f10 w) + | MaDIR1_to_DIR1(b,b1) -> (f11 b b1) + | MaIMM1_to_DIR1(b,b1) -> (f12 b b1) + | MaIX0p_to_DIR1(b) -> (f13 b) + | MaDIR1_to_IX0p(b) -> (f14 b) + | MaINHA_and_IMM1(b) -> (f15 b) + | MaINHX_and_IMM1(b) -> (f16 b) + | MaIMM1_and_IMM1(b,b1) -> (f17 b b1) + | MaDIR1_and_IMM1(b,b1) -> (f18 b b1) + | MaIX0_and_IMM1(b) -> (f19 b) + | MaIX0p_and_IMM1(b) -> (f20 b) + | MaIX1_and_IMM1(b,b1) -> (f21 b b1) + | MaIX1p_and_IMM1(b,b1) -> (f22 b b1) + | MaSP1_and_IMM1(b,b1) -> (f23 b b1) + | MaDIRn(o,b) -> (f24 o b) + | MaDIRn_and_IMM1(o,b,b1) -> (f25 o b b1) + | MaTNY(e) -> (f26 e) + | MaSRT(b) -> (f27 b)) +)))))))))))))))))))))))))))))))))))) +;; + +let mA_check_rect = +(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 -> +(match m with + MaINH -> p + | MaINHA -> p1 + | MaINHX -> p2 + | MaINHH -> p3 + | MaINHX0ADD -> p4 + | MaINHX1ADD(b) -> (f b) + | MaINHX2ADD(w) -> (f1 w) + | MaIMM1(b) -> (f2 b) + | MaIMM1EXT(b) -> (f3 b) + | MaIMM2(w) -> (f4 w) + | MaDIR1(b) -> (f5 b) + | MaDIR2(w) -> (f6 w) + | MaIX0 -> p5 + | MaIX1(b) -> (f7 b) + | MaIX2(w) -> (f8 w) + | MaSP1(b) -> (f9 b) + | MaSP2(w) -> (f10 w) + | MaDIR1_to_DIR1(b,b1) -> (f11 b b1) + | MaIMM1_to_DIR1(b,b1) -> (f12 b b1) + | MaIX0p_to_DIR1(b) -> (f13 b) + | MaDIR1_to_IX0p(b) -> (f14 b) + | MaINHA_and_IMM1(b) -> (f15 b) + | MaINHX_and_IMM1(b) -> (f16 b) + | MaIMM1_and_IMM1(b,b1) -> (f17 b b1) + | MaDIR1_and_IMM1(b,b1) -> (f18 b b1) + | MaIX0_and_IMM1(b) -> (f19 b) + | MaIX0p_and_IMM1(b) -> (f20 b) + | MaIX1_and_IMM1(b,b1) -> (f21 b b1) + | MaIX1p_and_IMM1(b,b1) -> (f22 b b1) + | MaSP1_and_IMM1(b,b1) -> (f23 b b1) + | MaDIRn(o,b) -> (f24 o b) + | MaDIRn_and_IMM1(o,b,b1) -> (f25 o b b1) + | MaTNY(e) -> (f26 e) + | MaSRT(b) -> (f27 b)) +)))))))))))))))))))))))))))))))))))) +;; + +type instruction = +Instr of Matita_freescale_opcode.instr_mode * Matita_freescale_opcode.opcode * mA_check +;; + +let instruction_rec = +(function f -> (function i -> +(match i with + Instr(i1,o,m) -> (f i1 o m)) +)) +;; + +let instruction_rect = +(function f -> (function i -> +(match i with + Instr(i1,o,m) -> (f i1 o m)) +)) +;; + +let args_picker = +(function m -> (function i -> (function args -> +(match args with + MaINH -> Obj.magic ((Matita_list_list.Nil)) + | MaINHA -> Obj.magic ((Matita_list_list.Nil)) + | MaINHX -> Obj.magic ((Matita_list_list.Nil)) + | MaINHH -> Obj.magic ((Matita_list_list.Nil)) + | MaINHX0ADD -> Obj.magic ((Matita_list_list.Nil)) + | MaINHX1ADD(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil)))) + | 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)))))) + | MaIMM1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil)))) + | MaIMM1EXT(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil)))) + | 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)))))) + | MaDIR1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil)))) + | 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)))))) + | MaIX0 -> Obj.magic ((Matita_list_list.Nil)) + | MaIX1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil)))) + | 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)))))) + | MaSP1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil)))) + | 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)))))) + | MaDIR1_to_DIR1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil)))))) + | MaIMM1_to_DIR1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil)))))) + | MaIX0p_to_DIR1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil)))) + | MaDIR1_to_IX0p(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil)))) + | MaINHA_and_IMM1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil)))) + | MaINHX_and_IMM1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil)))) + | MaIMM1_and_IMM1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil)))))) + | MaDIR1_and_IMM1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil)))))) + | MaIX0_and_IMM1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil)))) + | MaIX0p_and_IMM1(b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil)))) + | MaIX1_and_IMM1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil)))))) + | MaIX1p_and_IMM1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil)))))) + | MaSP1_and_IMM1(b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil)))))) + | MaDIRn(_,b) -> Obj.magic ((Matita_list_list.Cons((TByte(b)),(Matita_list_list.Nil)))) + | MaDIRn_and_IMM1(_,b1,b2) -> Obj.magic ((Matita_list_list.Cons((TByte(b1)),(Matita_list_list.Cons((TByte(b2)),(Matita_list_list.Nil)))))) + | MaTNY(_) -> Obj.magic ((Matita_list_list.Nil)) + | MaSRT(_) -> Obj.magic ((Matita_list_list.Nil))) +))) +;; + +let bytes_of_pseudo_instr_mode_param = +(function m -> (function o -> (function i -> (function p -> (let rec aux = +(function param -> +(match param with + Matita_list_list.Nil -> (Matita_datatypes_constructors.None) + | Matita_list_list.Cons(hd,tl) -> +(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 + Matita_datatypes_bool.True -> +(match (Matita_freescale_extra.thd4T hd) with + 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)))) + | 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))))) + + | Matita_datatypes_bool.False -> (aux tl)) +) +) in aux (opcode_table m)))))) +;; + +let opcode_to_any = +(function m -> (function o -> (Matita_freescale_opcode.AnyOP(o)))) +;; + +let compile = +(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 = ( +(match res with + Matita_datatypes_constructors.None -> Obj.magic ((Matita_logic_connectives.false_rect)) + | Matita_datatypes_constructors.Some(v) -> Obj.magic (v)) +) in value)))))) +;; + +let source_to_byte8 = +(function mcu -> +(match mcu with + Matita_freescale_opcode.HC05 -> Obj.magic ((function l -> (let rec aux = +(function p1 -> (function p2 -> +(match p1 with + Matita_list_list.Nil -> p2 + | Matita_list_list.Cons(hd,tl) -> +(match hd with + TByte(b) -> (aux tl (Matita_list_list.append p2 (Matita_list_list.Cons(b,(Matita_list_list.Nil)))))) +) +)) in aux l (Matita_list_list.Nil)))) + | Matita_freescale_opcode.HC08 -> Obj.magic ((function l -> (let rec aux = +(function p1 -> (function p2 -> +(match p1 with + Matita_list_list.Nil -> p2 + | Matita_list_list.Cons(hd,tl) -> +(match hd with + TByte(b) -> (aux tl (Matita_list_list.append p2 (Matita_list_list.Cons(b,(Matita_list_list.Nil)))))) +) +)) in aux l (Matita_list_list.Nil)))) + | Matita_freescale_opcode.HCS08 -> Obj.magic ((function l -> (let rec aux = +(function p1 -> (function p2 -> +(match p1 with + Matita_list_list.Nil -> p2 + | Matita_list_list.Cons(hd,tl) -> +(match hd with + TByte(b) -> (aux tl (Matita_list_list.append p2 (Matita_list_list.Cons(b,(Matita_list_list.Nil)))))) +) +)) in aux l (Matita_list_list.Nil)))) + | Matita_freescale_opcode.RS08 -> Obj.magic ((function l -> (let rec aux = +(function p1 -> (function p2 -> +(match p1 with + Matita_list_list.Nil -> p2 + | Matita_list_list.Cons(hd,tl) -> +(match hd with + TByte(b) -> (aux tl (Matita_list_list.append p2 (Matita_list_list.Cons(b,(Matita_list_list.Nil)))))) +) +)) in aux l (Matita_list_list.Nil))))) +) +;; +