From b78762c92afee705e618f29f89897db8b45df3dd Mon Sep 17 00:00:00 2001 From: Xander Date: Fri, 28 Jul 2023 21:38:35 +0200 Subject: optional implementation of multboot 1 --- lib/DATS/init.dats | 48 ++++++++++++++++++++++++++++++++++++++++++------ lib/DATS/itoa.dats | 10 +++++----- lib/DATS/writer.dats | 28 ++++++++++++---------------- lib/SATS/init.sats | 10 ++++++++-- lib/SATS/writer.sats | 4 ++-- 5 files changed, 69 insertions(+), 31 deletions(-) (limited to 'lib') 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) : 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 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) : [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} .. (pf : !(@[char][BUFFER_SIZE] @ l) | p : ptr l , n : int, i : int i): 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(v) = let + implement exec_void$fwork(v) = let implement string_foreach$fwork (c,env) = put_char(c,env) val _ = $effmask_all(string_foreach_env (g1ofg0(str),v)) in end in - init_exec(!p) + $effmask_ref(exec_void(writer_ref)) end implement clear_screen() : void = let - val (vbox pf | p) = ref_get_viewptr(writer_ref) - implement init_exec$fwork(v) = _clear_screen(v) + implement exec_void$fwork(v) = _clear_screen(v) + implement initialize$fwork(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 (!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_ref); + + exec_void(writer_ref) end end diff --git a/lib/SATS/init.sats b/lib/SATS/init.sats index 676657b..8219de1 100644 --- a/lib/SATS/init.sats +++ b/lib/SATS/init.sats @@ -3,6 +3,12 @@ viewtypedef initializable (vt:viewt@ype) = fun {vt:viewt@ype} uninitialized (v : opt(vt,false)): initializable vt -fun {vt:viewt@ype} init_exec (x : &(initializable vt)): void -fun {vt:viewt@ype} init_exec$fwork (v : &vt): void +fun {vt:viewt@ype} exec_void (r: ref(initializable vt)): void +fun {vt:viewt@ype} exec_void$fwork (v : &vt): void + +fun {vt:viewt@ype} {a: t@ype} exec (r: ref(initializable vt), default: a): a +fun {vt:viewt@ype} {a: t@ype} exec$fwork (v : &vt, default: a): a + +fun {vt:viewt@ype} initialize (r: ref(initializable vt)): void +fun {vt:viewt@ype} initialize$fwork (v: &vt? >> opt(vt,success)): #[success : bool] bool success diff --git a/lib/SATS/writer.sats b/lib/SATS/writer.sats index 14773ea..b23213f 100644 --- a/lib/SATS/writer.sats +++ b/lib/SATS/writer.sats @@ -22,5 +22,5 @@ datatype color = typedef screenChar = @{ ascii_character = char, color_code = uint8} -fun put_string (str : string) : void -fun clear_screen() : void +fn put_string (str : string) : void +fn clear_screen() : void -- cgit v1.2.3