optional implementation of multboot 1

3 files changed, 59 insertions, 27 deletions

diff --git a/lib/DATS/init.dats b/lib/DATS/init.dats
index a4c84b3..cfdc12e 100644
--- a/lib/DATS/init.dats
+++ b/lib/DATS/init.dats
@@ -1,3 +1,4 @@
+#include "share/atspre_staload.hats"
 staload "lib/SATS/init.sats"
 
 #define ATS_DYNLOADFLAG 0
@@ -9,15 +10,50 @@ in
 end
 
 
-implement{vt} init_exec (x) = 
-  if x.initialized then
+implement{vt} exec_void (r) = let
+  val (vbox pf | p) = ref_get_viewptr{initializable vt}(r)
+in
+  if p->initialized then
     let
-      prval () = opt_unsome x.obj
-      val () = init_exec$fwork (x.obj)
-      prval () = opt_some  x.obj
+      prval () = opt_unsome p->obj
+      val () = exec_void$fwork (p->obj)
+      prval () = opt_some  p->obj
     in
     end
+end
 
-implement{vt} init_exec$fwork (v) = ()
+implement{vt} exec_void$fwork (v) = ()
+
+implement{vt} {a} exec  (r,default) = let
+  val (vbox pf | p) = ref_get_viewptr{initializable vt}(r)
+in
+  if p->initialized then
+    let
+      prval () = opt_unsome p->obj
+      val a = exec$fwork (p->obj,default)
+      prval () = opt_some  p->obj
+    in
+      a
+    end
+  else
+    default
+end
 
+implement{vt} {a} exec$fwork (v,default) = default
+
+implement{vt} initialize (r) = let
+  val (vbox pf | p) = ref_get_viewptr{initializable vt}(r)
+in
+  if (not p->initialized) then
+    let
+      prval () = opt_unnone p->obj
+      val () = p->initialized := initialize$fwork(p->obj)
+    in end
+end
+
+implement{vt} initialize$fwork (v) = let
+  prval () = opt_none v
+in
+  false
+end
 
diff --git a/lib/DATS/itoa.dats b/lib/DATS/itoa.dats
index 2fef14c..29697b5 100644
--- a/lib/DATS/itoa.dats
+++ b/lib/DATS/itoa.dats
@@ -3,8 +3,8 @@
 #define ATS_DYNLOADFLAG 0
 
 
-fun reverse {l : addr} {n,m:nat | n < m} (pf : !(@[char][m] @ l) | p : ptr l, n : int n) : void = let
-  fun loop {i,j,n:nat | i < j && j < n} (pf : !(@[char][n] @ l) | p : ptr l , i : int i, j : int j) : void = let
+fn reverse {l : addr} {n,m:nat | n < m} (pf : !(@[char][m] @ l) | p : ptr l, n : int n) :<!wrt> void = let
+  fun loop {i,j,n:nat | i < j && j < n} .<j-i>. (pf : !(@[char][n] @ l) | p : ptr l , i : int i, j : int j) :<!wrt> void = let
     val tmp = p->[i]
   in
     p->[i] := p->[j];
@@ -23,7 +23,7 @@ local
 
 staload UN = "prelude/SATS/unsafe.sats"
 
-extern castfn char_arr2string (arr : &(@[char][BUFFER_SIZE])) : [n : nat | n < BUFFER_SIZE] string n
+extern castfn char_arr2string (arr : &(@[char][BUFFER_SIZE])) :<> [n : nat | n < BUFFER_SIZE] string n
 extern praxi __assert {l:addr} (ptr: ptr (l)):  vtakeout0 (@[char][BUFFER_SIZE]@l)
 var buffer : @[char][BUFFER_SIZE] // Size should be BUFFER_SIZE
 
@@ -31,12 +31,12 @@ in
 
 //TODO: make function better by handling to large number for buffer
 
-extern fun itoa  {n:nat | n > 1 && n < 33} (value : int, base : int n) : [k : nat | k < BUFFER_SIZE] string k
+extern fun itoa  {n:nat | n > 1 && n < 33} (value : int, base : int n) :<!wrt> [k : nat | k < BUFFER_SIZE] string k
 implement itoa(value,base) = let
   prval (pf , fpf) = __assert(addr@buffer) // Get proofs  UNSAFE:
   val offset = (if(value < 0) then 1 else 0) : [n: nat | n == 0 || n == 1] int n
 
-  fun loop {i : nat | i < BUFFER_SIZE} {l:addr} (pf : !(@[char][BUFFER_SIZE] @ l) | p : ptr l , n : int, i : int i): void = let
+  fun loop {i : nat | i < BUFFER_SIZE} {l:addr} .<BUFFER_SIZE - i>. (pf : !(@[char][BUFFER_SIZE] @ l) | p : ptr l , n : int, i : int i):<!wrt> void = let
     val r = n % base
     val k = n / base
   in
diff --git a/lib/DATS/writer.dats b/lib/DATS/writer.dats
index 9b2fd78..b8625f4 100644
--- a/lib/DATS/writer.dats
+++ b/lib/DATS/writer.dats
@@ -97,31 +97,27 @@ in
   in
 
     implement put_string (str : string) : void = let
-      val (vbox pf | p) = ref_get_viewptr(writer_ref)
-      implement init_exec$fwork<writer_t>(v) = let 
+      implement exec_void$fwork<writer_t>(v) = let 
         implement string_foreach$fwork<writer_t> (c,env) = put_char(c,env)
         val _ = $effmask_all(string_foreach_env<writer_t> (g1ofg0(str),v))
       in 
       end
     in  
-      init_exec<writer_t>(!p)
+      $effmask_ref(exec_void<writer_t>(writer_ref))
     end
 
     implement clear_screen() : void = let
-      val (vbox pf | p) = ref_get_viewptr(writer_ref)
-      implement init_exec$fwork<writer_t>(v) = _clear_screen(v)
+      implement exec_void$fwork<writer_t>(v) = _clear_screen(v)
+      implement initialize$fwork<writer_t>(v) =
+        (
+          v := @{position = 0, color_code = code_value(White,Black)}; 
+          let prval() = opt_some v in true end
+        )
     in
-      if p->initialized then
-        init_exec<writer_t> (!p)
-      else
-        let
-          prval () = opt_unnone p->obj
-          val () = p->obj := @{position = 0, color_code = code_value(White,Black)}
-          val () = p->initialized := true
-          val () = _clear_screen(p->obj)
-          prval () = opt_some p->obj
-        in
-        end
+      if not writer_ref->initialized then
+        initialize<writer_t>(writer_ref);
+      
+      exec_void<writer_t>(writer_ref)
     end
 
   end