(* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
nlet rec mb_load_from_source_at (old_mem:Array16T (Array16T (Array16T (Array16T (Array8T bool)))))
- (source:list byte8) (addr:word16) on source ≝
-match source with
- (* fine di source: carica da old_mem *)
- [ nil ⇒ old_mem
- | cons hd tl ⇒ match lt_w16 addr 〈〈xF,xF〉:〈xF,xF〉〉 with
- (* non supera 0xFFFF, ricorsione *)
- [ true ⇒ mb_load_from_source_at (mt_update ? old_mem addr (bits_of_byte8 hd)) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)
- (* supera 0xFFFF, niente ricorsione *)
- | false ⇒ mt_update ? old_mem addr (bits_of_byte8 hd)
- ]].
+ (src:list byte8) (addr:word16) on src ≝
+ match src with
+ (* fine di source: carica da old_mem *)
+ [ nil ⇒ old_mem
+ | cons hd tl ⇒ mb_load_from_source_at (mt_update ? old_mem addr (bits_of_byte8 hd)) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)
+ ].