#define ATS_DYNLOADFLAG 0

#include "kernel/prelude/kernel_prelude.hats"

staload "./table.sats"
staload "./entry.sats" 

staload "lib/SATS/valid.sats"
staload "lib/DATS/valid.dats"

// Calculate table address of next table based on current table and index: P4->P3->P2->P1
fn next_table_address{l:agz}(pf : !table_t@l | p : ptr(l), index : sizeLt(ENTRY_COUNT)) : Valid Ptr1 = let
  val entry = p->[index]
in
  if (contains_flag(entry,PRESENT) && ~contains_flag(entry,HUGE_PAGE)) then
    let 
      val next = g1ofg0((Ptr1_to_sz(p) << 9) lor (index << 12))
    in
      if next > i2sz(0) then
        create_valid(sz_to_Ptr1(next))
      else
        create_unvalid()
    end
  else
    create_unvalid()
end

implement set_zero(table) = let 
  implement array_foreach$fwork<entry_t><void>(entry,v) = set_unused(entry)
in
  assertloc(array_foreach<entry_t>(table,i2sz(ENTRY_COUNT)) = i2sz(ENTRY_COUNT))
end

// UNSAFE: unsafe block
local

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

in

  implement get_P4() = @{
    ptr = $UN.ptr_vtake(ulint_to_Ptr1(0xfffffffffffff000ul)),
    level = (0u | )
  }

  implement next_table(tp,index) = let
    val k = tp.ptr
    val next = next_table_address(k.0 | k.2,index)
    prval () = k.1 k.0
  in
    if is_valid(next) then 
      let
        val p = unwrap_valid(next)
      in
        create_valid(@{
          ptr = $UN.ptr_vtake(p),
          level = ( succ(tp.level.0) | )
        })
      end
    else
      let
        val () = destroy_unvalid(next)
      in
        create_unvalid()
      end
  end

end