diff options
Diffstat (limited to 'kernel/memory/frame.sats')
-rw-r--r-- | kernel/memory/frame.sats | 50 |
1 files changed, 25 insertions, 25 deletions
diff --git a/kernel/memory/frame.sats b/kernel/memory/frame.sats index 0de5056..0926e6c 100644 --- a/kernel/memory/frame.sats +++ b/kernel/memory/frame.sats @@ -1,25 +1,25 @@ -#define PAGE_SIZE 4096 - -staload "kernel/bootinfo/multiboot.sats" - -typedef frame_t = @{ - num = size_t -} - -typedef frame_allocator_t = @{ - next_free_frame = frame_t, - current_area = memory_area_t, - kernel_start = frame_t, - kernel_end = frame_t, - multiboot_start = frame_t, - multiboot_end = frame_t -} - -vtypedef allocptr = [l : agz] (frame_allocator_t@l , frame_allocator_t@l -<lin,prf> void | ptr l) - -abst@ype frame_allocator = frame_allocator_t - -fn containing_address {l : addr} (address : ptr l) :<> frame_t -fn allocate_frame {l : agz}{k : agz} (bf : !boot_info_t @ k | b : ptr k) :<!ref,!wrt> frame_t -fn deallocate_frame (p : !allocptr) : void -fn frame_allocator_init(kernel_start: Ptr, kernel_end: Ptr, multiboot_start:Ptr, multiboot_end: Ptr, b : !bootptr) : void +(* #define PAGE_SIZE 4096 *) +(**) +(* staload "kernel/bootinfo/multiboot.sats" *) +(**) +(* typedef frame_t = @{ *) +(* num = size_t *) +(* } *) +(**) +(* typedef frame_allocator_t = @{ *) +(* next_free_frame = frame_t, *) +(* current_area = memory_area_t, *) +(* kernel_start = frame_t, *) +(* kernel_end = frame_t, *) +(* multiboot_start = frame_t, *) +(* multiboot_end = frame_t *) +(* } *) +(**) +(* vtypedef allocptr = [l : agz] (frame_allocator_t@l , frame_allocator_t@l -<lin,prf> void | ptr l) *) +(**) +(* abst@ype frame_allocator = frame_allocator_t *) +(**) +(* fn containing_address {l : addr} (address : ptr l) :<> frame_t *) +(* fn allocate_frame {l : agz}{k : agz} (bf : !boot_info_t @ k | b : ptr k) :<!ref,!wrt> frame_t *) +(* fn deallocate_frame (p : !allocptr) : void *) +(* (* fn frame_allocator_init(kernel_start: Ptr, kernel_end: Ptr, multiboot_start:Ptr, multiboot_end: Ptr, b : !bootptr) : void *) *) |