diff options
Diffstat (limited to 'kernel/bootinfo/multiboot.dats')
| -rw-r--r-- | kernel/bootinfo/multiboot.dats | 30 |
1 files changed, 14 insertions, 16 deletions
diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats index 0653184..9fe9103 100644 --- a/kernel/bootinfo/multiboot.dats +++ b/kernel/bootinfo/multiboot.dats @@ -26,10 +26,10 @@ in in implement init (p : Ptr1) = let - extern castfn unsafe_init(x : &boot_info_t? >> boot_info_t) :<> void - val total_size = $UN.ptr0_get<uint>(p) + val total_size = g1ofg0($UN.ptr0_get<uint>(p)) - fun loop (boot_info : &boot_info_t? >> boot_info_t, p : ptr):<!wrt,!ntm> void = let + fun loop {n,i : nat | i < n} .<n-i>. (boot_info : &boot_info_t? >> boot_info_t, p : ptr, i: uint i, n: uint n):<!wrt> void = let + extern castfn unsafe_init(x : &boot_info_t? >> boot_info_t) :<> void val type = $UN.ptr0_get<uint>(p) val size = $UN.ptr0_get<uint>(ptr_succ<uint>(p)) val next = (if (size % 8u != 0) then size + 8u - (size % 8u) else size) : uint @@ -45,23 +45,21 @@ in ) | _ => (); - if (type != 0u) then - loop(boot_info,ptr_add<uint8>(p, next)) + if (i < n - 1u) then + loop(boot_info,ptr_add<uint8>(p, next),succ(i),n) else unsafe_init(boot_info) end - val (vbox pf | boot_p) = ref_get_viewptr(bootinfo_ref) - in - if (not boot_p->initialized) then - let - prval () = opt_unnone boot_p->obj - val () = boot_p->obj.total_size := total_size - val () = loop(boot_p->obj, ptr_add<uint32>(p,2)) - val () = boot_p->initialized := true - prval () = opt_some boot_p->obj - in end - end + implement initialize$fwork<boot_info_t>(v) = ( + if (total_size > 0u) then ( + v.total_size := total_size; + loop(v, ptr_add<uint32>(p,2),0u,total_size); + let prval () = opt_some v in true end) + else + let prval () = opt_none v in false end + ) + in end implement get_memory_mappings_n() = let implement exec$fwork<boot_info_t><size_t>(v,_) = _get_memory_mappings_n(v) |