1 files changed, 0 insertions, 62 deletions
diff --git a/kernel/multiboot.dats b/kernel/multiboot.dats
deleted file mode 100644
index bc3b552..0000000
--- a/kernel/multiboot.dats
+++ /dev/null
@@ -1,62 +0,0 @@
-#include "./prelude/kernel_prelude.hats"
-
-#define ATS_DYNLOADFLAG 0
-
-staload "./multiboot.sats"
-staload UN = "prelude/SATS/unsafe.sats"
-
-local
-
-var boot_info : boot_info_t
-
-in
-
-implement boot_info_init (p : Ptr1) = let
-  extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (boot_info_t@l) // takeout proof  UNSAFE:
-  prval (pf, fpf) = __assert (addr@boot_info)
-  val total_size = $UN.ptr0_get<uint>(p)
-
-  fun loop {l : agz} (pf : !boot_info_t@l | boot_p : ptr l , p : ptr): void = let
-    val type = $UN.ptr0_get<uint>(p)
-    val size = $UN.ptr0_get<uint>(ptr_succ<uint>(p))
-    val next = (if (size % 8u != 0) then size + 8u - (size % 8u) else size) : uint
-  in 
-    case+ type of 
-      | 6u => (
-               boot_p->memory_map := $UN.ptr0_get<memory_map_t>(p); 
-               boot_p->memory_map.entries := ptr_add<uint>(p,4)
-              )
-      | _ => ();
-
-    if (type != 0u) then
-      loop(pf | boot_p, ptr_add<uint8>(p, next))
-  end
-
-in
-  boot_info.total_size := total_size;
-  loop(pf | addr@boot_info, ptr_add<uint32>(p,2));
-
-  (pf , fpf | addr@boot_info)
-end
-
-end
-
-extern castfn ui2sz (n : uint) : size_t
-
-implement get_memory_mappings_n(p) = let
-  val size = p.2->memory_map.tag.size 
-  val n_entries = (if(size >= 16u) then (size - 16u) / p.2->memory_map.entry_size else 0u) : uint
-in
-  ui2sz n_entries
-end
-
-// TODO: here use optional datatype (fix runtime )
-
-implement get_memory_mapping(p,n) = let
-  val size = p.2->memory_map.tag.size 
-  val n_entries = ui2sz (if(size >= 16u) then (size - 16u) / p.2->memory_map.entry_size else 0u)
-in
-  assertloc(n < n_entries);
-  $UN.ptr0_get<memory_entry_t>(ptr_add<memory_map_t>(p.2->memory_map.entries,n))
-end
-