]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_translation.ml
projects / helm.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
branch for universe
[helm.git] / matita / contribs / assembly / freescale / freescale_ocaml / matita_freescale_translation.ml
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 (file)
index 0000000..91c34be
--- /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)))))
+)
+;;
+
Unnamed repository; edit this file 'description' to name the repository.