#include "kernel/prelude/kernel_prelude.hats"

#define ATS_DYNLOADFLAG 0

staload "./idt.sats"

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

extern typedef "int_frame" = int_frame

//----------------------------------No __attribute__ support in ats---------

%{
  __attribute__ ((interrupt))
  void default_exception_handler(int_frame *frame){
    default_exception_handler2(frame);
  }

  __attribute__ ((interrupt))
  void default_exception_handler_e(int_frame *frame, uint64_t error_code){
    default_exception_handler_e2(frame, error_code);
  }

  __attribute__ ((interrupt))
  void default_interrupt_handler(int_frame *frame, uint64_t error_code){
    default_interrupt_handler_e2(frame, error_code);
  }

  __attribute__ ((interrupt))
  void default_interrupt_handler_e(int_frame *frame, uint64_t error_code){
    default_interrupt_handler_e2(frame, error_code);
  }
%}

// DEFAULT HANDLERS,  --------------------------------------------------

extern fun default_exception_handler2(frame: &int_frame) : void = "mac#"
implement default_exception_handler2(frame) : void = let
in
  println!("DEFAULT EXCEPTION HANDLER - NO ERROR CODE");
end

extern fun default_exception_handler_e2(frame: &int_frame, error_code : uint64) : void = "mac#"
implement default_exception_handler_e2(frame,error_code) = let
in
  println!("DEFAULT EXCEPTION HANDLER - WIDTH ERROR CODE:", $UN.cast{int}(error_code));
end

extern fun default_interrupt_handler2(frame: &int_frame) : void = "mac#"
implement default_interrupt_handler2(frame) = let
in
  println!("DEFAULT INTERRUPT HANDLER - NO ERROR CODE");
end

extern fun default_interrupt_handler_e2 (frame: &int_frame, error_code : uint64) : void = "mac#"
implement default_interrupt_handler_e2(frame,error_code) = let
in
  println!("DEFAULT INTERRUPT HANDLER - WIDTH ERROR CODE:", $UN.cast{int}(error_code));
end

//-------------------------------------------------------

var idt : @[idt_entry_t][IDT_MAX_DESCRIPTORS] // The table
var idtr : idtr_t // interrupt descriptor table register instance

fun idt_set_descriptor  {n : nat | n < IDT_MAX_DESCRIPTORS} (vector: int n, isr: uint64, flags: uint8) : void = let
  extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (@[idt_entry_t][IDT_MAX_DESCRIPTORS]@l) // takeout proof  UNSAFE:
  prval (pf, fpf) = __assert (addr@(idt))
  val x = $UN.cast{uint64}(0xFFFF)
  val y = $UN.cast{uint64}(0xFFFFFFF)
  val entry = @{
    isr_low = $UN.cast(isr land x), 
    kernel_cs = $UN.cast(0x08), 
    ist = $UN.cast(0), 
    attributes = flags, 
    isr_mid = $UN.cast((isr >> 16) land x), 
    isr_high = $UN.cast((isr >> 32) land y), 
    reserved = $UN.cast(0)
  }
in
  idt[vector] := entry;
  let prval () = fpf(pf) in end
end

extern typedef "idtr_t" = idtr_t
%{$
  void setup(idtr_t idtr) {
    __asm__ volatile ("lidt %0" : : "m"(idtr)); // load the new IDT
  }
%}

extern fun setup(idtr : idtr_t) : void = "ext#"

// Setup exception handlers (vector 0-31)
fun setup_exceptions() = let
  fun loop {n : nat | n <= 32} (i : int n) : void = if (i < 32) then (
    idt_set_descriptor(i,$UN.cast(
      case+ i of
        | _ when i = 8 || i = 10 || i = 11 || i = 12 
                || i = 13 || i = 14 || i = 17 || i = 22 => default_exception_handler_e
        | _ => default_exception_handler
      ),$UN.cast(TRAP_GATE_FLAGS));
    loop(i + 1)
  )
in
loop(0)
end

// Setup trap interrupts (vector 32-255)
fun setup_interrupts() = let
  fun loop {n : nat | n <= IDT_MAX_DESCRIPTORS && n >= 32} (i : int n) : void = if (i < IDT_MAX_DESCRIPTORS - 1) then (
    idt_set_descriptor(i,$UN.cast(default_interrupt_handler),$UN.cast(INT_GATE_FLAGS));
    loop(i + 1)
  )
in
loop(32)
end

implement idt_init() : void = let 
  extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (idtr_t@l)
  prval (pf, fpf) = __assert (addr@(idtr)) // takeout proof  UNSAFE:
in 
  idtr.base := addr@(idt);
  idtr.limit := $UN.cast(8 * IDT_MAX_DESCRIPTORS);
  setup_exceptions();
  setup_interrupts();
  setup(idtr);
  let prval () = fpf(pf) in end
end