Rewrite table

1 files changed, 16 insertions, 8 deletions

diff --git a/kernel/memory/paging/table.sats b/kernel/memory/paging/table.sats
index 9a103f4..491b77e 100644
--- a/kernel/memory/paging/table.sats
+++ b/kernel/memory/paging/table.sats
@@ -4,16 +4,24 @@ staload "./entry.sats"
 staload "lib/SATS/valid.sats"
 staload "lib/DATS/valid.dats"
 
-typedef table_t = @[entry_t][ENTRY_COUNT]
+vtypedef tablePtr1(level : int)  = [l : agz] (@[entry_t][ENTRY_COUNT]@l , @[entry_t][ENTRY_COUNT]@l -<lin,prf> void, uint level | ptr l)
 
-vtypedef tablePtr1(c : int)  = @{
-    ptr = [l : agz] (table_t@l , table_t@l -<lin,prf> void | ptr l),
-    level = (uint c | )
-  }
+absvt@ype table_t(level:int) = tablePtr1 level
+
+vtypedef Table_t = [level:nat | level < 4] table_t(level)
+
+fun table_get_at{n:int}(table: !table_t(n), i: sizeLt(ENTRY_COUNT)):<> entry_t
+
+fun table_set_at{n:int}(table: !table_t(n), i: sizeLt(ENTRY_COUNT), x: entry_t):<!wrt> void
+
+overload [] with table_get_at
+overload [] with table_set_at
 
 // Set all the entries in the table to unused (zero)
-fn set_zero(&table_t): void
+fn set_zero(&Table_t):<!wrt> void
+
+castfn consume(Table_t): void
 
-fun get_P4() : tablePtr1(0)
+fun get_P4() : table_t 0
 
-fun next_table{n : nat | n < 3}(tablePtr1(n), sizeLt(ENTRY_COUNT)) : Valid (tablePtr1(n+1))
+fun next_table{n : nat | n < 3}(table_t n, sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1))