#define ATS_DYNLOADFLAG 0

#include "kernel/prelude/kernel_prelude.hats"

staload "./page.sats"
staload FR = "kernel/memory/frame.sats"
staload "./table.sats"

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

datatype table_level = 
  | Level4
  | Level3
  | Level2
  | Level1

fn start_address(page : page_t) : size_t = page.num * $FR.PAGE_SIZE

fn get_index(page: page_t,n : intLte(3)) = g1ofg0((page.num >> (27 - 9 * n)) land i2sz(511))

//NOTE: huge page handler not implemented
fn translate_page(page: page_t) : Valid $FR.frame_t = let
  fun loop{n : nat | n < 3}.<3-n>.(table : table_t n, count : int n) : Valid $FR.frame_t = let
    staload "./entry.sats"
    val index = get_index(page,count)
  in
    if index < ENTRY_COUNT then let
        val v = next_table(table,index)
      in
        if is_valid(v) then let
            val table_next = unwrap_valid(v)
          in
            if count < 2 then
              loop(table_next,succ(count))
            else(
              consume(table_next);
              frame
            ) where {
                val index = get_index(page,count+1)
                val frame = (if index < ENTRY_COUNT then pointed_frame(table_next[index]) else create_unvalid()) : Valid $FR.frame_t
              }
          end
        else (
          destroy_unvalid(v);
          println!("Unvalid table pointer encountered: ", count); 
          create_unvalid())
      end
    else (
      consume(table);
      println!("Table index too big");
      create_unvalid())
  end
in
  loop(get_P4(),0)
end

implement translate(virtual_addr) = let
  val offset = Ptr0_to_sz(virtual_addr) % i2sz($FR.PAGE_SIZE)
  val vframe = translate_page(containing_address(virtual_addr))
in
  if is_valid(vframe) then let
      val frame = unwrap_valid(vframe)
    in
      create_valid (sz_to_Ptr0(frame.num * $FR.PAGE_SIZE + offset))
    end
  else (
    destroy_unvalid(vframe);
    create_unvalid();
  )
end

implement containing_address(address) = (
  assertloc(address < ulint_to_Ptr0(0x0000800000000000ul) ||
            address >= ulint_to_Ptr0(0xFFFF800000000000ul));
  @{num = Ptr0_to_sz(address) / i2sz($FR.PAGE_SIZE)}
)

// TODO: implement and_then and or_else for valid (like in rust)
implement map_to{s}(page,frame,flags,size) = let
  staload "./entry.sats"
  fun loop{n : nat | n < 3}.<3-n>.(table : table_t n, count : int n, flags: &(@[entry_flag][s])) : void = let
    staload "lib/SATS/panic.sats"
    val index = get_index(page,count)
    val () = println!(index)
  in
    if index < ENTRY_COUNT then let
        val v = next_table_create(table,index)
      in
        if is_valid(v) then let
            val table_next = unwrap_valid(v)
          in
            if count < 2 then
              loop(table_next,succ(count),flags)
            else let
                val index = get_index(page,count+1)
              in
                if index < ENTRY_COUNT then (
                  assertloc(is_unused(table_next[index]));
                  table_next[index] := add_flag(create_entry(frame, flags,size),PRESENT);
                );
                consume(table_next);
              end
          end
        else (
          destroy_unvalid(v);
          panic("Could not create table"))
      end
    else (
      consume(table);
      println!("Table index too big"))
  end
in
  loop(get_P4(),0,flags)
end

implement map(page,flags,size) = map_to(page,$FR.allocate_frame(),flags,size)