From 272a40095e7c3f694f010d074ab54b326730009e Mon Sep 17 00:00:00 2001
From: Xander <xander@biltopia.org>
Date: Fri, 28 Jul 2023 22:30:45 +0200
Subject: Some work

---
 kernel/bootinfo/multiboot.dats | 30 ++++++++++++++----------------
 kernel/bootinfo/multiboot.sats |  2 +-
 lib/SATS/init.sats             |  1 -
 3 files changed, 15 insertions(+), 18 deletions(-)

diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats
index 0653184..9fe9103 100644
--- a/kernel/bootinfo/multiboot.dats
+++ b/kernel/bootinfo/multiboot.dats
@@ -26,10 +26,10 @@ in
   in
 
     implement init (p : Ptr1) = let
-      extern castfn unsafe_init(x : &boot_info_t? >> boot_info_t) :<> void
-      val total_size = $UN.ptr0_get<uint>(p)
+      val total_size = g1ofg0($UN.ptr0_get<uint>(p))
 
-      fun loop (boot_info : &boot_info_t? >> boot_info_t, p : ptr):<!wrt,!ntm> void = let
+      fun loop {n,i : nat | i < n} .<n-i>. (boot_info : &boot_info_t? >> boot_info_t, p : ptr, i: uint i, n: uint n):<!wrt> void = let
+        extern castfn unsafe_init(x : &boot_info_t? >> boot_info_t) :<> void
         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
@@ -45,23 +45,21 @@ in
                   )
           | _ => ();
 
-        if (type != 0u) then
-          loop(boot_info,ptr_add<uint8>(p, next))
+        if (i < n - 1u) then
+            loop(boot_info,ptr_add<uint8>(p, next),succ(i),n)
         else
           unsafe_init(boot_info)
       end
 
-      val (vbox pf | boot_p) = ref_get_viewptr(bootinfo_ref)
-    in
-      if (not boot_p->initialized) then 
-        let
-          prval ()  = opt_unnone boot_p->obj
-          val ()    = boot_p->obj.total_size := total_size
-          val ()    = loop(boot_p->obj, ptr_add<uint32>(p,2))
-          val ()    = boot_p->initialized := true
-          prval ()  = opt_some boot_p->obj
-        in end
-    end
+      implement initialize$fwork<boot_info_t>(v) = (
+        if (total_size > 0u) then (
+          v.total_size := total_size;
+          loop(v, ptr_add<uint32>(p,2),0u,total_size);
+          let prval () = opt_some v in true end)
+        else
+          let prval () = opt_none v in false end
+      )
+    in end
 
     implement get_memory_mappings_n() = let
       implement exec$fwork<boot_info_t><size_t>(v,_) = _get_memory_mappings_n(v)
diff --git a/kernel/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats
index cab885a..6be1e73 100644
--- a/kernel/bootinfo/multiboot.sats
+++ b/kernel/bootinfo/multiboot.sats
@@ -40,7 +40,7 @@ typedef elf64_shdr_t = @{
 }
 
 typedef boot_info_t = @{
-  total_size = uint,    // total size of boot information 
+  total_size = [n : int | n > 0] uint n,    // total size of boot information 
   memory_map = memory_areas_t,
   elf_tag = elf_tag_t
 }
diff --git a/lib/SATS/init.sats b/lib/SATS/init.sats
index 8219de1..9261ca9 100644
--- a/lib/SATS/init.sats
+++ b/lib/SATS/init.sats
@@ -11,4 +11,3 @@ fun {vt:viewt@ype} {a: t@ype} exec$fwork (v : &vt, default: a):<!wrt> a
 
 fun {vt:viewt@ype} initialize (r: ref(initializable vt)):<!ref,!wrt> void
 fun {vt:viewt@ype} initialize$fwork (v: &vt? >> opt(vt,success)):<!wrt> #[success : bool] bool success
-
-- 
cgit v1.2.3