From 67245a7eebeb135427d50171fda7af58770afc6d Mon Sep 17 00:00:00 2001 From: Xander Date: Thu, 13 Jul 2023 00:52:37 +0200 Subject: Full restructure --- Makefile | 10 ++--- kernel/interrupts/idt.dats | 2 +- kernel/itoa.dats | 63 -------------------------- kernel/kernel_prelude.hats | 12 ----- kernel/main.dats | 2 +- kernel/output/print.dats | 21 --------- kernel/output/writer.dats | 91 -------------------------------------- kernel/output/writer.sats | 32 -------------- kernel/prelude/DATS/print.dats | 20 +++++++++ kernel/prelude/kernel_prelude.hats | 12 +++++ lib/DATS/itoa.dats | 63 ++++++++++++++++++++++++++ lib/DATS/writer.dats | 91 ++++++++++++++++++++++++++++++++++++++ lib/SATS/writer.sats | 32 ++++++++++++++ 13 files changed, 225 insertions(+), 226 deletions(-) delete mode 100644 kernel/itoa.dats delete mode 100644 kernel/kernel_prelude.hats delete mode 100644 kernel/output/print.dats delete mode 100644 kernel/output/writer.dats delete mode 100644 kernel/output/writer.sats create mode 100644 kernel/prelude/DATS/print.dats create mode 100644 kernel/prelude/kernel_prelude.hats create mode 100644 lib/DATS/itoa.dats create mode 100644 lib/DATS/writer.dats create mode 100644 lib/SATS/writer.sats diff --git a/Makefile b/Makefile index 1554030..19bca78 100644 --- a/Makefile +++ b/Makefile @@ -8,9 +8,9 @@ assembly_source_files := $(wildcard arch/$(arch)/boot/*.asm) assembly_object_files := $(patsubst arch/$(arch)/boot/%.asm, \ build/arch/$(arch)/%.o, $(assembly_source_files)) -dats_source_files := $(wildcard kernel/*.dats kernel/**/*.dats) -dats_object_files := $(patsubst kernel/%.dats, \ - build/kernel/%_dats.o, $(dats_source_files)) +dats_source_files := $(wildcard lib/**/*.dats kernel/*.dats kernel/**/*.dats kernel/**/**/*.dats) +dats_object_files := $(patsubst %.dats, \ + build/%_dats.o, $(dats_source_files)) PATSCC=acc pc @@ -51,11 +51,11 @@ build/arch/$(arch)/%.o: arch/$(arch)/boot/%.asm @mkdir -p $(shell dirname $@) @nasm -felf64 $< -o $@ -build/kernel/%_dats.c: kernel/%.dats +build/%_dats.c: %.dats @mkdir -p $(shell dirname $@) $(PATSCC) -ccats -o $@ $< @mv *_dats.c $@ -build/kernel/%.o: build/kernel/%.c +build/%.o: build/%.c @mkdir -p $(shell dirname $@) $(CC) $(INCLUDE_ATS) $(CFLAGS) $(CFLAGS_ATS) -O2 -c $< -o $@ diff --git a/kernel/interrupts/idt.dats b/kernel/interrupts/idt.dats index 851a2b0..ea25ced 100644 --- a/kernel/interrupts/idt.dats +++ b/kernel/interrupts/idt.dats @@ -1,4 +1,4 @@ -#include "kernel/kernel_prelude.hats" +#include "kernel/prelude/kernel_prelude.hats" #define ATS_DYNLOADFLAG 0 diff --git a/kernel/itoa.dats b/kernel/itoa.dats deleted file mode 100644 index 7557dac..0000000 --- a/kernel/itoa.dats +++ /dev/null @@ -1,63 +0,0 @@ -#include "share/atspre_staload.hats" - -#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 - val tmp = p->[i] - in - p->[i] := p->[j]; - p->[j] := tmp; - if (i+1 < j-1) then - loop(pf | p, i+1,j-1) - end -in - if (n > 0) then - loop(pf | p, 0, n) -end - -local - -#define BUFFER_SIZE 50 - -staload UN = "prelude/SATS/unsafe.sats" - -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 - -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 -implement itoa(value,base) = let - prval (pf , fpf) = __assert(addr@buffer) // Get proofs UNSAFE: - - 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 - val r = n % base - val k = n / base - in - if (r >= 10) then - p->[i] := $UN.cast{char}(65 + (r - 10)) - else - p->[i] := $UN.cast{char}(48 + r); - - if (i + 2 < BUFFER_SIZE) then - if (k > 0) then - loop(pf | p, k, succ(i)) - else ( - p->[succ(i)] := '\0'; - reverse(pf | p, sz2i(i))) - end - - // Run loop - val () = loop(pf | addr@buffer, value, i2sz(0)); - val str = char_arr2string(buffer); // Convert to string UNSAFE: -in - let prval () = fpf(pf) in end; - str // Return string -end - -end diff --git a/kernel/kernel_prelude.hats b/kernel/kernel_prelude.hats deleted file mode 100644 index 048cba1..0000000 --- a/kernel/kernel_prelude.hats +++ /dev/null @@ -1,12 +0,0 @@ -#ifndef PRELUDE -#define PRELUDE 1 - -#include "share/atspre_staload.hats" - -staload "kernel/output/writer.sats" -val () = clear_screen() - -staload "kernel/output/print.dats" - -#endif - diff --git a/kernel/main.dats b/kernel/main.dats index 26db859..d6e29f4 100644 --- a/kernel/main.dats +++ b/kernel/main.dats @@ -1,4 +1,4 @@ -#include "kernel/kernel_prelude.hats" +#include "./prelude/kernel_prelude.hats" staload "kernel/interrupts/idt.sats" diff --git a/kernel/output/print.dats b/kernel/output/print.dats deleted file mode 100644 index 9b5def0..0000000 --- a/kernel/output/print.dats +++ /dev/null @@ -1,21 +0,0 @@ -#include "share/atspre_staload.hats" - -#define ATS_DYNLOADFLAG 0 - - -staload "kernel/output/writer.sats" -staload "kernel/itoa.dats" - -extern fun print_newline() : void -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 -implement print_int(n) = put_string(itoa(n,10)) - -overload print with put_string of 1 -overload print with print_int of 1 - -macdef assertloc(tf) = assert_errmsg (,(tf), $mylocation) diff --git a/kernel/output/writer.dats b/kernel/output/writer.dats deleted file mode 100644 index c7731f6..0000000 --- a/kernel/output/writer.dats +++ /dev/null @@ -1,91 +0,0 @@ -#include "kernel/kernel_prelude.hats" - -staload "./writer.sats" - -#define ATS_DYNLOADFLAG 0 - -%{^ - #define get_buffer() ((void *) 0xB8000) -%} - -extern fun get_buffer():<> buffer = "mac#" -extern prfun eat_buffer (pf: buffer): void -extern fun getref (): [l:addr] vtakeoutptr (writer) - -fun color_value(c : color): uint8 = - case+ c of - | Black() => i2u8 0 - | Blue() => i2u8 1 - | Green() => i2u8 2 - | Cyan() => i2u8 3 - | Red() => i2u8 4 - | Magenta() => i2u8 5 - | Brown() => i2u8 6 - | LightGray() => i2u8 7 - | DarkGray() => i2u8 8 - | LightBlue() => i2u8 9 - | LightGreen() => i2u8 10 - | LightCyan() => i2u8 11 - | LightRed() => i2u8 12 - | Pink() => i2u8 13 - | Yellow() => i2u8 14 - | White() => i2u8 15 - -fun code_value(foreground: color, background:color): uint8 = - (color_value(background) << 4) lor color_value(foreground) - -local -var _val: writer - -in -implement getref () = let - extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (writer@l) - prval (pf, fpf) = __assert (addr@(_val)) -in - (pf, fpf | addr@(_val)) -end -end - -fun put_char (c : char, writer: &writer) : void = let - val buf = get_buffer() - val pos = writer.position -in - if (c = '\n') then - let - val new_pos = (pos / BUFFER_WIDTH + 1) * BUFFER_WIDTH - in - if (new_pos < N) then - writer.position := new_pos - else - clear_screen() - end - else ( - buf.1->[writer.position] := @{ ascii_character = c, color_code = writer.color_code}; - - if (pos < N - 1) then - writer.position := succ(pos) - else - clear_screen()); - - let prval() = eat_buffer buf in () end -end - - -implement put_string (str : string) : void = let - val (pf, fpf | p_val) = getref() - implement string_foreach$fwork (c,env) = put_char(c,env) - val _ = string_foreach_env (g1ofg0(str),!p_val) - prval() = fpf(pf) -in -end - -implement clear_screen() : void = let - val (pf, fpf | p_val) = getref() - fun loop {n : nat | n < N - 1} .. (i : int n, wr : &writer) : void = - (put_char('\0', wr); if (i < N - 2) then loop(i+1,wr)) - val () = !p_val := @{position = 0, color_code = code_value(White,Black)} -in - loop(0,!p_val); - !p_val.position := 0; - let prval() = fpf(pf) in () end -end diff --git a/kernel/output/writer.sats b/kernel/output/writer.sats deleted file mode 100644 index 65a2ea9..0000000 --- a/kernel/output/writer.sats +++ /dev/null @@ -1,32 +0,0 @@ -#define BUFFER_HEIGHT 23 -#define BUFFER_WIDTH 80 -#define N BUFFER_HEIGHT * BUFFER_WIDTH - -datatype color = - | Black - | Blue - | Green - | Cyan - | Red - | Magenta - | Brown - | LightGray - | DarkGray - | LightBlue - | LightGreen - | LightCyan - | LightRed - | Pink - | Yellow - | White - - -typedef screenChar = @{ ascii_character = char, color_code = uint8} - -vtypedef buffer = [l : agz] (@[screenChar][N] @ l | ptr l) -typedef writer = @{position = [a:int | a >= 0 && a < N] int (a), color_code = uint8} - -castfn i2u8 {n: nat} (i: int n): uint8 n - -fun put_string (str : string) : void -fun clear_screen() : void diff --git a/kernel/prelude/DATS/print.dats b/kernel/prelude/DATS/print.dats new file mode 100644 index 0000000..5049a98 --- /dev/null +++ b/kernel/prelude/DATS/print.dats @@ -0,0 +1,20 @@ +#include "share/atspre_staload.hats" + +#define ATS_DYNLOADFLAG 0 + +staload "lib/SATS/writer.sats" +staload "lib/DATS/itoa.dats" + +extern fun print_newline() : void +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 +implement print_int(n) = put_string(itoa(n,10)) + +overload print with put_string of 1 +overload print with print_int of 1 + +macdef assertloc(tf) = assert_errmsg (,(tf), $mylocation) diff --git a/kernel/prelude/kernel_prelude.hats b/kernel/prelude/kernel_prelude.hats new file mode 100644 index 0000000..eb1990d --- /dev/null +++ b/kernel/prelude/kernel_prelude.hats @@ -0,0 +1,12 @@ +#ifndef PRELUDE +#define PRELUDE 1 + +#include "share/atspre_staload.hats" + +staload "lib/SATS/writer.sats" +val () = clear_screen() + +staload "./DATS/print.dats" + +#endif + diff --git a/lib/DATS/itoa.dats b/lib/DATS/itoa.dats new file mode 100644 index 0000000..35b8c47 --- /dev/null +++ b/lib/DATS/itoa.dats @@ -0,0 +1,63 @@ +#include "share/atspre_staload.hats" + +#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 + val tmp = p->[i] + in + p->[i] := p->[j]; + p->[j] := tmp; + if (i+1 < j-1) then + loop(pf | p, i+1,j-1) + end +in + if (n > 0) then + loop(pf | p, 0, n) +end + +local + +#define BUFFER_SIZE 50 + +staload UN = "prelude/SATS/unsafe.sats" + +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 + +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 +implement itoa(value,base) = let + prval (pf , fpf) = __assert(addr@buffer) // Get proofs UNSAFE: + + 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 + val r = n % base + val k = n / base + in + if (r >= 10) then + p->[i] := $UN.cast{char}(65 + (r - 10)) + else + p->[i] := $UN.cast{char}(48 + r); + + if (i + 2 < BUFFER_SIZE) then + if (k > 0) then + loop(pf | p, k, succ(i)) + else ( + p->[succ(i)] := '\0'; + reverse(pf | p, sz2i(i))) + 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 +end + +end diff --git a/lib/DATS/writer.dats b/lib/DATS/writer.dats new file mode 100644 index 0000000..24246a1 --- /dev/null +++ b/lib/DATS/writer.dats @@ -0,0 +1,91 @@ +#include "share/atspre_staload.hats" + +staload "lib/SATS/writer.sats" + +#define ATS_DYNLOADFLAG 0 + +%{^ + #define get_buffer() ((void *) 0xB8000) +%} + +extern fun get_buffer():<> buffer = "mac#" +extern prfun eat_buffer (pf: buffer): void +extern fun getref (): [l:addr] vtakeoutptr (writer) + +fun color_value(c : color): uint8 = + case+ c of + | Black() => i2u8 0 + | Blue() => i2u8 1 + | Green() => i2u8 2 + | Cyan() => i2u8 3 + | Red() => i2u8 4 + | Magenta() => i2u8 5 + | Brown() => i2u8 6 + | LightGray() => i2u8 7 + | DarkGray() => i2u8 8 + | LightBlue() => i2u8 9 + | LightGreen() => i2u8 10 + | LightCyan() => i2u8 11 + | LightRed() => i2u8 12 + | Pink() => i2u8 13 + | Yellow() => i2u8 14 + | White() => i2u8 15 + +fun code_value(foreground: color, background:color): uint8 = + (color_value(background) << 4) lor color_value(foreground) + +local +var _val: writer + +in +implement getref () = let + extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (writer@l) + prval (pf, fpf) = __assert (addr@(_val)) +in + (pf, fpf | addr@(_val)) +end +end + +fun put_char (c : char, writer: &writer) : void = let + val buf = get_buffer() + val pos = writer.position +in + if (c = '\n') then + let + val new_pos = (pos / BUFFER_WIDTH + 1) * BUFFER_WIDTH + in + if (new_pos < N) then + writer.position := new_pos + else + clear_screen() + end + else ( + buf.1->[writer.position] := @{ ascii_character = c, color_code = writer.color_code}; + + if (pos < N - 1) then + writer.position := succ(pos) + else + clear_screen()); + + let prval() = eat_buffer buf in () end +end + + +implement put_string (str : string) : void = let + val (pf, fpf | p_val) = getref() + implement string_foreach$fwork (c,env) = put_char(c,env) + val _ = string_foreach_env (g1ofg0(str),!p_val) + prval() = fpf(pf) +in +end + +implement clear_screen() : void = let + val (pf, fpf | p_val) = getref() + fun loop {n : nat | n < N - 1} .. (i : int n, wr : &writer) : void = + (put_char('\0', wr); if (i < N - 2) then loop(i+1,wr)) + val () = !p_val := @{position = 0, color_code = code_value(White,Black)} +in + loop(0,!p_val); + !p_val.position := 0; + let prval() = fpf(pf) in () end +end diff --git a/lib/SATS/writer.sats b/lib/SATS/writer.sats new file mode 100644 index 0000000..65a2ea9 --- /dev/null +++ b/lib/SATS/writer.sats @@ -0,0 +1,32 @@ +#define BUFFER_HEIGHT 23 +#define BUFFER_WIDTH 80 +#define N BUFFER_HEIGHT * BUFFER_WIDTH + +datatype color = + | Black + | Blue + | Green + | Cyan + | Red + | Magenta + | Brown + | LightGray + | DarkGray + | LightBlue + | LightGreen + | LightCyan + | LightRed + | Pink + | Yellow + | White + + +typedef screenChar = @{ ascii_character = char, color_code = uint8} + +vtypedef buffer = [l : agz] (@[screenChar][N] @ l | ptr l) +typedef writer = @{position = [a:int | a >= 0 && a < N] int (a), color_code = uint8} + +castfn i2u8 {n: nat} (i: int n): uint8 n + +fun put_string (str : string) : void +fun clear_screen() : void -- cgit v1.2.3