diff options
| -rw-r--r-- | kernel/interrupts/idt.dats | 6 | ||||
| -rw-r--r-- | kernel/prelude/DATS/print.dats | 2 | ||||
| -rw-r--r-- | lib/DATS/itoa.dats | 34 |
3 files changed, 29 insertions, 13 deletions
diff --git a/kernel/interrupts/idt.dats b/kernel/interrupts/idt.dats index ea25ced..0b91253 100644 --- a/kernel/interrupts/idt.dats +++ b/kernel/interrupts/idt.dats @@ -43,7 +43,7 @@ end extern fun default_exception_handler_e2(frame: &int_frame, error_code : uint64) : void = "mac#" implement default_exception_handler_e2(frame,error_code) = let in - println!("DEFAULT EXCEPTION HANDLER - WIDTH ERROR CODE"); + println!("DEFAULT EXCEPTION HANDLER - WIDTH ERROR CODE:", $UN.cast{int}(error_code)); end extern fun default_interrupt_handler2(frame: &int_frame) : void = "mac#" @@ -52,10 +52,10 @@ in println!("DEFAULT INTERRUPT HANDLER - NO ERROR CODE"); end -extern fun default_interrupt_handler_e2(frame: &int_frame, error_code : uint64) : void = "mac#" +extern fun default_interrupt_handler_e2 (frame: &int_frame, error_code : uint64) : void = "mac#" implement default_interrupt_handler_e2(frame,error_code) = let in - println!("DEFAULT INTERRUPT HANDLER - WIDTH ERROR CODE"); + println!("DEFAULT INTERRUPT HANDLER - WIDTH ERROR CODE:", $UN.cast{int}(error_code)); end //------------------------------------------------------- diff --git a/kernel/prelude/DATS/print.dats b/kernel/prelude/DATS/print.dats index 5049a98..6d378fa 100644 --- a/kernel/prelude/DATS/print.dats +++ b/kernel/prelude/DATS/print.dats @@ -11,7 +11,7 @@ implement print_newline() = put_string("\n") extern fun assert_errmsg(b: bool, msg: string) : void implement assert_errmsg(b,msg) = if (~b) then put_string(msg) -extern fun print_int {n : nat | n > 0} (n : int n) : void +extern fun print_int (n : int) : void implement print_int(n) = put_string(itoa(n,10)) overload print with put_string of 1 diff --git a/lib/DATS/itoa.dats b/lib/DATS/itoa.dats index 35b8c47..2fef14c 100644 --- a/lib/DATS/itoa.dats +++ b/lib/DATS/itoa.dats @@ -31,11 +31,12 @@ in //TODO: make function better by handling to large number for buffer -extern fun itoa {v,n:nat | n > 1 && n < 33 && v > 0} (value : int v, 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 {n,i : nat | n > 0 && i < BUFFER_SIZE} {l:addr} (pf : !(@[char][BUFFER_SIZE] @ l) | p : ptr l , n : int n, i : size_t 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 @@ -48,16 +49,31 @@ implement itoa(value,base) = let if (k > 0) then loop(pf | p, k, succ(i)) else ( - p->[succ(i)] := '\0'; - reverse(pf | p, sz2i(i))) + p->[i+1+offset] := '\0'; + reverse(pf | p, i+offset) + ) end - // Run loop - val () = loop(pf | addr@buffer, value, i2sz(0)); - val str = char_arr2string(buffer); // Convert arr to string UNSAFE: in - let prval () = fpf(pf) in end; - str // Return string + + if (value != 0) then + loop(pf | addr@buffer, abs(value), 0) + else ( + buffer[0] := '0'; + buffer[1] := '\0' + ); + + if (value < 0) then + buffer[0] := '-'; + + // Run loop + let + val str = char_arr2string(buffer) // Convert arr to string UNSAFE: + prval () = fpf(pf) + in + str // Return string + end + end end |