[ TickERR s _ ⇒ None ?
(* azzeramento tutta RAM tranne dati *)
| TickSUSP s _ ⇒ None ?
- | TickOK s ⇒ Some ? (byte8_hexdump t (get_mem_desc HCS08 t s) dTest_HCS08_RAM (nat_of_word16 (byte8_strlen string)))
+ | TickOK s ⇒ Some ? (byte8_hexdump t (mem_desc HCS08 t s) dTest_HCS08_RAM (nat_of_word16 (byte8_strlen string)))
] =
Some ? (reverse_list ? string)).
[ TickERR s _ ⇒ None ?
(* azzeramento tutta RAM tranne dati *)
| TickSUSP s _ ⇒ None ?
- | TickOK s ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (get_mem_desc HCS08 t s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
+ | TickOK s ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (mem_desc HCS08 t s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
] =
Some ? (set_pc_reg HCS08 t
- (dTest_HCS08_sReverse_status t (fst ?? (shr_b8 (w16h (byte8_strlen string)))) (fst ?? (shr_w16 (byte8_strlen string))) (byte8_strlen string) (reverse_list ? string))
+ (dTest_HCS08_sReverse_status t (fst … (shr_b8 (w16h (byte8_strlen string)))) (fst … (shr_w16 (byte8_strlen string))) (byte8_strlen string) (reverse_list ? string))
(mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB)))).
(*
(42+79*(nat_of_word16 (byte8_strlen string))+5*((nat_of_word16 (byte8_strlen string))/512)) with
[ TickERR s _ ⇒ None ?
| TickSUSP s _ ⇒ None ?
- | TickOK s ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (get_mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
+ | TickOK s ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
].
ndefinition sReverseNoCalc ≝
λstring:list byte8.
Some ? (set_pc_reg HCS08 MEM_TREE
- (dTest_HCS08_sReverse_status MEM_TREE (fst ?? (shr_b8 (w16h (byte8_strlen string))))
- (fst ?? (shr_w16 (byte8_strlen string)))
+ (dTest_HCS08_sReverse_status MEM_TREE (fst … (shr_b8 (w16h (byte8_strlen string))))
+ (fst … (shr_w16 (byte8_strlen string)))
(byte8_strlen string) (reverse_list ? string))
(mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB))).
((nat_of_word16 〈〈x6,x4〉:〈x6,x4〉〉)+(nat_of_byte8 〈x9,x6〉)*(nat_of_word16 (byte8_strlen string))) with
[ TickERR s _ ⇒ None ?
(* azzeramento tutta RAM tranne dati *)
- | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (get_mem_desc HCS08 t s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
+ | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (mem_desc HCS08 t s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
| TickOK s ⇒ None ?
] =
Some ? (set_pc_reg HCS08 t
(TickOK ? (dTest_HCS08_cSort_status MEM_TREE true 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
((nat_of_word16 〈〈x6,x4〉:〈x6,x4〉〉)+(nat_of_byte8 〈x9,x6〉)*(nat_of_word16 (byte8_strlen string))) with
[ TickERR s _ ⇒ None ?
- | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (get_mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
+ | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
| TickOK s ⇒ None ?
].
(nat_of_word16 num) with
[ TickERR s _ ⇒ None ?
(* azzeramento tutta RAM tranne dati *)
- | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (get_mem_desc HCS08 t s) dTest_zeros3K 〈〈x0,x1〉:〈x2,x0〉〉))
+ | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (mem_desc HCS08 t s) dTest_zeros3K 〈〈x0,x1〉:〈x2,x0〉〉))
| TickOK s ⇒ None ?
] =
Some ? (dTest_HCS08_gNum_status t false 〈x0,x0〉 num 〈〈x1,x9〉:〈x5,x1〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num (dTest_HCS08_gNum_aurei num)).
(TickOK ? (dTest_HCS08_gNum_status MEM_TREE true 〈x0,x0〉 〈〈x1,xA〉:〈x0,x0〉〉 〈〈x1,x8〉:〈xB,xE〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num dTest_zeros))
(nat_of_word16 num) with
[ TickERR s _ ⇒ None ?
- | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (get_mem_desc HCS08 MEM_TREE s) dTest_zeros3K 〈〈x0,x1〉:〈x2,x0〉〉))
+ | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros3K 〈〈x0,x1〉:〈x2,x0〉〉))
| TickOK s ⇒ None ?
].