#include "kernel/kernel_prelude.hats"

#define ATS_DYNLOADFLAG 0

staload "./idt.sats"

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

%{
  __attribute__ ((interrupt))
%}
// Default exception handler
fun default_exception_handler(frame: &int_frame) : void = let 
in
  println!("DEFAULT EXCEPTION HANDLER - NO ERROR CODE");
end

%{
  __attribute__ ((interrupt))
%}
// Default exception handler (with error code)
fun default_exception_handler_e(frame: &int_frame, error_code : uint64) : void = let 
in
  println!("DEFAULT EXCEPTION HANDLER - ERROR CODE")
end

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

fun idt_set_descriptor {l:addr} {n : nat | n < 256} (vector: int n, isr: (&int_frame) -> void, flags: uint8) : void = let
  extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (@[idt_entry_t][256]@l)
  prval (pf, fpf) = __assert (addr@(idt))
  val x = $UN.cast{uint64}(0xFFFF)
  val y = $UN.cast{uint64}(0xFFFFFFF)
  val entry = @{
    isr_low = $UN.cast($UN.cast{uint64}(isr) land x), 
    kernel_cs = $UN.cast(0x08), 
    ist = $UN.cast(0), 
    attributes = flags, 
    isr_mid = $UN.cast(($UN.cast{uint64}(isr) >> 16) land x), 
    isr_high = $UN.cast(($UN.cast{uint64}(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#"

implement idt_init() : void = let 
  extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (idtr_t@l)
  prval (pf, fpf) = __assert (addr@(idtr))
  fun loop {n : nat | n <= 32} (i : int n) : void = if (i < 32) then (idt_set_descriptor(i,default_exception_handler,$UN.cast(TRAP_GATE_FLAGS)); loop(i + 1))
in 
  idtr.base := addr@(idt);
  idtr.limit := $UN.cast{uint16}(8 * 256);
  loop(0);
  setup(idtr);
  let prval () = fpf(pf) in end
end