#include "kernel/prelude/kernel_prelude.hats"

#define ATS_DYNLOADFLAG 0

staload "./multiboot.sats"
staload UN = "prelude/SATS/unsafe.sats"

local

var boot_info : boot_info_t

in

implement boot_info_init (p : Ptr1) = let
  extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (boot_info_t@l) // takeout proof  UNSAFE:
  prval (pf, fpf) = __assert (addr@boot_info)
  val total_size = $UN.ptr0_get<uint>(p)

  fun loop {l : agz} (pf : !boot_info_t@l | boot_p : ptr l , p : ptr): void = let
    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
  in 
    case+ type of 
      | 6u => (
               boot_p->memory_map := $UN.ptr0_get<memory_map_t>(p); 
               boot_p->memory_map.entries := ptr_add<uint>(p,4)
              )
      | _ => ();

    if (type != 0u) then
      loop(pf | boot_p, ptr_add<uint8>(p, next))
  end

in
  boot_info.total_size := total_size;
  loop(pf | addr@boot_info, ptr_add<uint32>(p,2));

  (pf , fpf | addr@boot_info)
end

end

extern castfn ui2sz (n : uint) : [n : nat] size_t n

implement get_memory_mappings_n(p) = let
  val size = p.2->memory_map.tag.size 
  val n_entries = (if(size >= 16u) then (size - 16u) / p.2->memory_map.entry_size else 0u) : uint
in
  ui2sz n_entries
end

// TODO: here use optional datatype (fix runtime alloc)

implement get_memory_mapping(p,n) = let
  val size = p.2->memory_map.tag.size 
  val n_entries = ui2sz (if(size >= 16u) then (size - 16u) / p.2->memory_map.entry_size else 0u)
in
  assertloc(n < n_entries);
  $UN.ptr0_get<memory_entry_t>(ptr_add<memory_map_t>(p.2->memory_map.entries,n))
end

implement print_memory_mappings(p) = let
  val length = get_memory_mappings_n(p)
  fun loop {n,i : nat | i < n} .<n-i>. (p : !bootptr, i : size_t i, n : size_t n) : void = let 
    val entry = get_memory_mapping(p,i)
  in
    if (entry.type = 1) then (
      print("Start Address: ");
      print_hex(entry.base_addr);
      print(" Length: ");
      println_hex(entry.length);
    );
    if (i < n-1) then (
      loop (p,succ(i),n)
    )
  end
in
  if (length > 0) then
    loop(p,i2sz(0),length)
  else
    println!("No memory mappings")
end