4 files changed, 83 insertions, 3 deletions
diff --git a/kernel/interrupts/idt.dats b/kernel/interrupts/idt.dats
new file mode 100644
index 0000000..380260a
--- /dev/null
+++ b/kernel/interrupts/idt.dats
@@ -0,0 +1,52 @@
+#include "kernel/kernel_prelude.hats"
+
+#define ATS_DYNLOADFLAG 0
+
+staload "./idt.sats"
+
+extern castfn i2u8 {n: nat} (i: int n): uint8 n
+extern castfn i2u16 {n: nat} (i: int n): uint16 n
+extern castfn i2u32 {n: nat} (i: int n): uint32 n
+extern castfn i2u64 {n: nat} (i: int n): uint64 n
+extern castfn i2u {n: int} (i: uint8 n): int n
+
+%{
+  __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 : agz} {n : nat | n < 256} (vector: uint8 n, isr: ptr l, 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 t = @{
+    isr_low = i2u16(0), 
+    kernel_cs = i2u16(0) , 
+    ist = i2u8(0), 
+    attributes = i2u8(0) , 
+    isr_mid = i2u16(0), 
+    isr_high = i2u32(0), 
+    reserved = i2u32(0)
+  }
+in
+  idt[i2u(vector)] := t;
+  let prval () = fpf(pf) in end
+end
+
+implement idt_init() : void = let in end
diff --git a/kernel/interrupts/idt.sats b/kernel/interrupts/idt.sats
new file mode 100644
index 0000000..d8391aa
--- /dev/null
+++ b/kernel/interrupts/idt.sats
@@ -0,0 +1,29 @@
+
+#define 
+TRAP_GATE_FLAGS 0x8F // p=1, dpl=0b00, type=0b1111
+
+typedef idt_entry_t = @{
+  isr_low = uint16,   // The lower 16 bits of the ISR's address
+  kernel_cs = uint16, // The GDT segment selector that the CPU will load into CS before calling the ISR
+  ist = uint8,        // The IST in the TSS that the CPU will load into RSP; set to zero for now 
+  attributes = uint8, // Type and attributes; see the IDT page
+  isr_mid = uint16,   // The higher 16 bits of the lower 32 bits of the ISR's address
+  isr_high = uint32,  // The higher 32 bits of the ISR's address
+  reserved = uint32   // Set to zero
+}
+
+typedef idtr_t = @{
+  limit = uint16,
+  base = uint64
+}
+
+// Interrupt frame to pass to ISR
+typedef int_frame = @{
+  ip = uint64, // instruction pointer
+  cs = uint64, // code segment
+  rflags = uint64,
+  sp = uint64, // stack pointer
+  ss = uint64 // stack segment
+}
+
+fun idt_init() : void
diff --git a/kernel/kernel_prelude.hats b/kernel/kernel_prelude.hats
index 683b2d5..048cba1 100644
--- a/kernel/kernel_prelude.hats
+++ b/kernel/kernel_prelude.hats
@@ -8,7 +8,5 @@ val () = clear_screen()
 
 staload "kernel/output/print.dats"
 
-castfn i2u8 {n: nat} (i: int n): uint8 n
-
 #endif
 
diff --git a/kernel/output/writer.sats b/kernel/output/writer.sats
index 8f25313..65a2ea9 100644
--- a/kernel/output/writer.sats
+++ b/kernel/output/writer.sats
@@ -26,6 +26,7 @@ typedef screenChar = @{ ascii_character = char, color_code = uint8}
 vtypedef buffer = [l : agz] (@[screenChar][N] @ l | ptr l)
 typedef writer  = @{position = [a:int | a >= 0 && a < N] int (a), color_code = uint8}
 
+castfn i2u8 {n: nat} (i: int n): uint8 n
+
 fun put_string (str : string) : void
 fun clear_screen() : void
-