From ca4334e044926dcca5013125682e555a423f3bb8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= Date: Fri, 9 Aug 2024 19:06:07 +0200 Subject: [PATCH 1/3] Update integer list example * use `swarm format` * use `tydef` * use `format` * use accumulator functions --- example/list.sw | 305 +++++++++++++++++++++++------------------------- 1 file changed, 143 insertions(+), 162 deletions(-) diff --git a/example/list.sw b/example/list.sw index eb49f8521..62f35e1b8 100644 --- a/example/list.sw +++ b/example/list.sw @@ -1,3 +1,4 @@ + /*******************************************************************/ /* LIST ENCODING IN INT */ /* */ @@ -9,36 +10,31 @@ /* For examples of usage see the unit tests in testLIST function. */ /* */ /*******************************************************************/ - +// // Definitions: // - MAIN: nil (Haskell []), cons (Haskell (:)), head, tail // - BONUS: headTail, index, for, for_each, for_each_i // - ARITH: len, mod, shiftL, shiftR, shiftLH, shiftRH // - HELPERS: consP, getLenPart, setLenPart, to1numA, getLenA // - TESTS: assert, testLIST, testLIST_BIG, testLIST_ALL - +// /*******************************************************************/ /* TYPE */ /*******************************************************************/ - // Type of list of ints - the inner ints can themselves be lists, // so *any* type can be encoded inside. // // It is the callers responsibility to make sure a program using this // "type" is type safe. Notably 2 == [0] != [] == 0 but [] !! x == 0. -// -// TODO: once #153 is resolved, add types to definitions -// -// type ListI = Int +tydef ListI = Int end + /*******************************************************************/ /* LAYOUT */ /*******************************************************************/ - // The length of a number is kept in the header and split into 7bit // chunks each prefixed by 1bit that marks if the byte is last in // the header (0=YES). - /* EXAMPLE - [short_x,long_y] - concretly e.g. [42, 2^(2^7)] 0 < len short_x < 2^7 @@ -50,265 +46,250 @@ vvvvvvvvvvvv vvvvvvvvvvvvvvvvvvvvvvvvv vvv ^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ head tail */ - /*******************************************************************/ /* ARITH PRIMITIVES */ /*******************************************************************/ - // bitlength of a number (shifting by one) -def naive_len : Int -> Int = \i. - if (i == 0) {0} {1 + naive_len (i/2)} +def naive_len: Int -> Int -> Int + = \acc. \i. + if (i == 0) {acc} {naive_len (1 + acc) (i / 2)} end + // modulus function (%) -def mod : Int -> Int -> Int = \i.\m. - i - m * (i / m) -end +def mod: Int -> Int -> Int = \i. \m. i - m * (i / m) end + // f X Y = Y * 2^(-X) -def shiftL : Int -> Int -> Int = \s.\i. - i / 2^s -end +def shiftL: Int -> Int -> Int = \s. \i. i / 2 ^ s end + // f X Y = Y * 2^(X) -def shiftR : Int -> Int -> Int = \s.\i. - i * 2^s -end +def shiftR: Int -> Int -> Int = \s. \i. i * 2 ^ s end + // shift by (8bit) bytes -def shiftLH : Int -> Int -> Int = \s. shiftL (s*8) end -def shiftRH : Int -> Int -> Int = \s. shiftR (s*8) end +def shiftLH: Int -> Int -> Int = \s. shiftL (s * 8) end -// bitlength of a number (shifting by 64) -def len : Int -> Int = \i. - let next = i / 2^64 in - if (next == 0) {naive_len i} {64 + len next} +def shiftRH: Int -> Int -> Int = \s. shiftR (s * 8) end + + +// bitlength of a number using an accumulator (shifting by 64) +def len_accum: Int -> Int -> Int + = \acc. \i. + let next = i / 2 ^ 64 in + if (next == 0) {naive_len acc i} {len_accum (acc + 64) next} end + +// bitlength of a number (uses an accumulator and shifts by 64 bits) +def len: Int -> Int = len_accum 0 end + + /*******************************************************************/ /* helper functions */ /*******************************************************************/ +def getLenPart: Int -> Int = \i. mod (i / 2) (2 ^ 7) end + +def setLenPart: Int -> Int = \i. 2 * mod i (2 ^ 7) end -def getLenPart : Int -> Int = \i. mod (i/2) (2^7) end -def setLenPart : Int -> Int = \i. 2 * (mod i (2^7)) end // Split length into 7-bit parts and prefix all but last with 1 -def to1numA : Int -> Int * Int = \i. +def to1numA: Int -> (Int * Int) + = \i. let nextPart = shiftL 7 i in - if (nextPart == 0) - { ((2 * i), 1) } /* last part */ - { let p = to1numA nextPart in - ( 1 /* header isEnd bit */ + setLenPart i + shiftRH 1 (fst p) - , 1 + snd p - ) - } + if (nextPart == 0) {(2 * i, 1 /* last part */)} { + let p = to1numA nextPart in + (1 /* header isEnd bit */ + setLenPart i + shiftRH 1 (fst p), 1 + snd p) + } end + // Get bitlength of the first number in the list // and also the list starting at the number itself -// -// getLenA : ListI -> Int * Int -def getLenA = \xs. +def getLenA: ListI -> (Int * Int) + = \xs. let isEnd = 0 == mod xs 2 in let l = getLenPart xs in let nextPart = shiftLH 1 xs in - if isEnd - { (l, nextPart) } - { let p = getLenA nextPart in - (l + shiftR 7 (fst p), snd p) - } + if isEnd {(l, nextPart)} { + let p = getLenA nextPart in (l + shiftR 7 (fst p), snd p) + } end + /*******************************************************************/ /* LIST FUNCTIONS */ /*******************************************************************/ - -// headTail : ListI -> {Int} * {ListI} -def headTail = \xs. +def headTail: ListI -> (Int * ListI) + = \xs. let sign = mod xs 2 in let ns = xs / 2 in let p = getLenA ns in - ( { let x = mod (snd p) $ 2 ^ fst p in - if (sign == 0) {x} {-x} - } - , { shiftL (fst p) (snd p) } - ) + ( let x = mod (snd p) $ 2 ^ fst p in if (sign == 0) {x} {-x} + , shiftL (fst p) (snd p) ) end -// head : ListI -> Int -def head : Int -> Int = \xs. - force $ fst $ headTail xs +def head: ListI -> Int + = \xs. + let sign = mod xs 2 in + let ns = xs / 2 in + let p = getLenA ns in + let x = mod (snd p) $ 2 ^ fst p in if (sign == 0) {x} {-x} end -// tail : ListI -> ListI -def tail = \xs. - force $ snd $ headTail xs +def tail: ListI -> ListI + = \xs. + let sign = mod xs 2 in + let ns = xs / 2 in let p = getLenA ns in shiftL (fst p) (snd p) end -// nil : ListI -def nil = 0 end +def nil: ListI = 0 end + // Add non-negative number to beginning of list (cons adds the sign) -// consP : nat -> ListI -> Int -def consP = \x.\xs. - if (x == 0) - { 2 /* header says one bit length */ + shiftR (8+1) xs} - { let l = len x in - let pl = to1numA l in - (fst pl + shiftRH (snd pl) (x + shiftR l xs)) - } +def consP: Int -> ListI -> Int + = \x. \xs. + if (x == 0) {2 /* header says one bit length */ + shiftR (8 + 1) xs} { + let l = len x in + let pl = to1numA l in fst pl + shiftRH (snd pl) (x + shiftR l xs) + } end + // Add integer to the beginning of the list -// consP : Int -> ListI -> ListI -def cons = \x.\xs. - if (x >= 0) - { 2 * consP x xs } - { 1 + 2 * consP (-x) xs } +def cons: Int -> ListI -> ListI + = \x. \xs. + if (x >= 0) {2 * consP x xs} {1 + 2 * consP (-x) xs} end /*******************************************************************/ /* MORE LIST FUNCTIONS */ /*******************************************************************/ - -// index : Int -> ListI -> Int -def index = \i.\xs. - if (i <= 0) - {head xs} - {index (i-1) (tail xs)} +def index: Int -> ListI -> Int + = \i. \xs. + if (i <= 0) {head xs} {index (i - 1) (tail xs)} end -def for : Int -> Int -> (Int -> Cmd a) -> Cmd Unit = \s.\e.\act. - if (s == e) {} - {act s; for (s+1) e act} +def for: ∀ a. Int -> Int -> (Int -> Cmd a) -> Cmd Unit + = \s. \e. \act. + if (s == e) {} {act s; for (s + 1) e act} end -// for_each_i : Int -> ListI Int -> (Int * Int -> Cmd a) -> Cmd Unit -def for_each_i = \i.\xs.\act. - if (xs == nil) {} - { let ht = headTail xs - in act i (force $ fst ht); for_each_i (i+1) (force $ snd ht) act +def for_each_i: Int -> ListI -> (Int -> Int -> Cmd Unit) -> Cmd Unit + = \i. \xs. \act. + if (xs == nil) {} { + let ht = headTail xs in act i (fst ht); for_each_i (i + 1) (snd ht) act } end -// for_each : ListI Int -> (Int -> Cmd a) -> Cmd Unit -def for_each = \xs.\act. +def for_each: ListI -> (Int -> Cmd Unit) -> Cmd Unit + = \xs. \act. for_each_i 0 xs (\i. act) end + /*******************************************************************/ /* UNIT TESTS */ /*******************************************************************/ +def assert = \b. \m. if b {} {log "FAIL:"; fail m} end -// TODO: show values when #248 is implemented -def assert = \b.\m. - if b {} {log "FAIL:"; fail m} +def assert_eq + = \exp. \act. \m. + if (exp == act) {} { + log ("FAIL: expected " ++ format exp ++ " actual " ++ format act); + fail m + } end def testLIST = log "STARTING TESTS OF LIST:"; - log "check [0]"; let l0 = cons 0 nil in - assert (l0 == 4) "[0] ~ 4"; - assert (head l0 == 0) "head [0] == 0"; - assert (tail l0 == nil) "tail [0] == []"; - + assert_eq l0 4 "[0] ~ 4"; + assert_eq (head l0) 0 "head [0] == 0"; + assert_eq (tail l0) nil "tail [0] == []"; log "check [1]"; let l1 = cons 1 nil in - assert (l1 == 516) "[1] ~ 516"; - assert (head l1 == 1) "head [1] == 1"; - assert (tail l1 == nil) "tail [1] == []"; - + assert_eq l1 516 "[1] ~ 516"; + assert_eq (head l1) 1 "head [1] == 1"; + assert_eq (tail l1) nil "tail [1] == []"; log "check [-1]"; let ln1 = cons (-1) nil in - assert (ln1 == 517) "[-1] ~ 517"; - assert (head ln1 == -1) "head [-1] == -1"; - assert (tail ln1 == nil) "tail [-1] == []"; - + assert_eq ln1 517 "[-1] ~ 517"; + assert_eq (head ln1) (-1) "head [-1] == -1"; + assert_eq (tail ln1) nil "tail [-1] == []"; log "check [42]"; let l42 = cons 42 nil in - assert (l42 == 21528) "[42] ~ 21528"; - assert (head l42 == 42) "head [42] == 42"; - assert (tail l42 == nil) "tail [42] == []"; - + assert_eq l42 21528 "[42] ~ 21528"; + assert_eq (head l42) 42 "head [42] == 42"; + assert_eq (tail l42) nil "tail [42] == []"; log "check [499672]"; let l499672 = cons 499672 nil in - assert (l499672 == 255832140) "[499672] ~ 255832140"; - assert (head l499672 == 499672) "head [499672] == 499672"; - assert (tail l499672 == nil) "tail [499672] == []"; - + assert_eq l499672 255832140 "[499672] ~ 255832140"; + assert_eq (head l499672) 499672 "head [499672] == 499672"; + assert_eq (tail l499672) nil "tail [499672] == []"; log "check [1,0]"; let l1_0 = cons 1 l0 in - assert (l1_0 == 4612) "[1,0] ~ 4612"; - assert (head l1_0 == 1) "head [1,0] == 1"; - assert (tail l1_0 == l0) "tail [1,0] == [0]"; - + assert_eq l1_0 4612 "[1,0] ~ 4612"; + assert_eq (head l1_0) 1 "head [1,0] == 1"; + assert_eq (tail l1_0) l0 "tail [1,0] == [0]"; log "check [11,1,0]"; let l11_1_0 = cons 11 l1_0 in - assert (head l11_1_0 == 11) "head [11,1,0] == 11"; - assert (tail l11_1_0 == l1_0) "tail [11,1,0] == [1,0]"; - + assert_eq (head l11_1_0) 11 "head [11,1,0] == 11"; + assert_eq (tail l11_1_0) l1_0 "tail [11,1,0] == [1,0]"; log "check [0..9]"; - let l0__9 = cons 0 $ cons 1 $ cons 2 $ cons 3 $ cons 4 $ cons 5 $ cons 6 $ cons 7 $ cons 8 $ cons 9 nil in - assert (head l0__9 == 0) "head [0..9] == 0"; - - log "check indices"; - assert (index 0 l0__9 == 0) "[0..9] !! 0 == 0"; - assert (index 9 l0__9 == 9) "[0..9] !! 9 == 9"; - - // TODO: log the number of iteration once #248 is implemented - - log "check for"; - for 0 9 (\i. - assert (index i l0__9 == i) "[0..9] - every index I has value I" + let l0__9 = + cons 0 $ cons 1 $ cons 2 $ cons 3 $ cons 4 $ cons 5 $ cons 6 $ cons 7 $ cons 8 $ cons 9 nil in + assert_eq (head l0__9) 0 "head [0..9] == 0"; + log "- check indices"; + assert_eq (index 0 l0__9) 0 "[0..9] !! 0 == 0"; + assert_eq (index 9 l0__9) 9 "[0..9] !! 9 == 9"; + log "check for + index"; + for 0 9 ( + \i. log ("- at index " ++ format i); + assert_eq (index i l0__9) i "[0..9] - every index I has value I" ); - log "check for_each"; - for_each l0__9 (\x. - assert (x < 10) "[0..9] - every value X < 10" + for_each l0__9 ( + \x. log ("- at value " ++ format x); + assert (x < 10) "[0..9] - every value X < 10" ); - log "check for_each_i"; - for_each_i 0 l0__9 (\i.\x. - assert (i == x) "[0..9] - I == X for every value X at index I" + for_each_i 0 l0__9 ( + \i. \x. log ("- at index " ++ format i); + assert_eq i x "[0..9] - I == X for every value X at index I" ); - log "OK - ALL TEST PASSED\a" end + // This tests uses VERY LONG lists of size up to 2097332 bits. // TIP: increase the game speed (ticks/s) when you run this test. def testLIST_BIG = log "STARTING TESTS OF BIG LISTS:"; - log "check [2^(2^7)] aka [big]"; - let big = 2^2^7 in - assert (len big == 129) "len (2^2^7) == 2^7+1"; - assert (to1numA 129 == (515,2)) "to1numA: 129 == 1000_0001 --> 515 == [0000 001 0] [0000 001 1]"; - assert (getLenA 515 == (129,nil)) "getLenA: 515 --> 129"; + let big = 2 ^ 2 ^ 7 in + assert_eq (len big) 129 "len (2^2^7) == 2^7+1"; + assert_eq (to1numA 129) ( 515 + , 2 ) "to1numA: 129 == 1000_0001 --> 515 == [0000 001 0] [0000 001 1]"; + assert_eq (getLenA 515) (129, nil) "getLenA: 515 --> 129"; let ibig = 2 * (shiftR 16 big + 515) in let lbig = cons big nil in - assert (lbig == ibig) "[big] ~ 2 * ((big * 2^(2*8)) + 515)"; - assert (head lbig == big) "head [big] == big"; - assert (tail lbig == nil) "tail [big] == []"; - + assert_eq lbig ibig "[big] ~ 2 * ((big * 2^(2*8)) + 515)"; + assert_eq (head lbig) big "head [big] == big"; + assert_eq (tail lbig) nil "tail [big] == []"; log "check [2^(2^21)] aka [bigger]"; - let bigger = 2^(2^21) in + let bigger = 2 ^ 2 ^ 21 in let lbigger = cons bigger nil in - assert (head lbigger == bigger) "head [bigger] == bigger"; - assert (tail lbigger == nil) "tail [bigger] == []"; - + assert_eq (head lbigger) bigger "head [bigger] == bigger"; + assert_eq (tail lbigger) nil "tail [bigger] == []"; log "check [2^(2^21),2^(2^7)] aka [bigger,big]"; let lbiggest = cons bigger lbig in - assert (head lbiggest == bigger) "head [bigger,big] == bigger"; - assert (tail lbiggest == lbig) "tail [bigger,big] == [big]"; - - log "OK - ALL TEST PASSED"; + assert_eq (head lbiggest) bigger "head [bigger,big] == bigger"; + assert_eq (tail lbiggest) lbig "tail [bigger,big] == [big]"; + log "OK - ALL TEST PASSED" end -def testLIST_ALL = - testLIST; - testLIST_BIG; -end +def testLIST_ALL = testLIST; testLIST_BIG end \ No newline at end of file From e659ee9b3916a64d0e505c5ba00f077d8928f9eb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= Date: Fri, 9 Aug 2024 21:49:33 +0200 Subject: [PATCH 2/3] Add a note about new rec list --- example/list.sw | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/example/list.sw b/example/list.sw index 62f35e1b8..8824b2f25 100644 --- a/example/list.sw +++ b/example/list.sw @@ -9,6 +9,11 @@ /* */ /* For examples of usage see the unit tests in testLIST function. */ /* */ +/* NOTE THAT THIS IS NOT EFFICIENT OR ERGONIMIC!!! YOU SHOULD USE: */ +tydef NormalListType a = rec l. Unit + (a * l) end +/* */ +/* This code was written before swarm had 'format' or 'rec', but */ +/* it still serves as an example of pure swarm code with tests. */ /*******************************************************************/ // // Definitions: From d5c57b3213fded8a27e7d9d8f64358bef2b88c70 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ondr=CC=8Cej=20S=CC=8Cebek?= Date: Fri, 9 Aug 2024 21:52:12 +0200 Subject: [PATCH 3/3] Move comment --- example/list.sw | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/example/list.sw b/example/list.sw index 8824b2f25..8f5619611 100644 --- a/example/list.sw +++ b/example/list.sw @@ -10,7 +10,9 @@ /* For examples of usage see the unit tests in testLIST function. */ /* */ /* NOTE THAT THIS IS NOT EFFICIENT OR ERGONIMIC!!! YOU SHOULD USE: */ -tydef NormalListType a = rec l. Unit + (a * l) end +tydef NormalListType a = rec l. Unit + (a * l) end + + /* */ /* This code was written before swarm had 'format' or 'rec', but */ /* it still serves as an example of pure swarm code with tests. */ @@ -103,7 +105,11 @@ def setLenPart: Int -> Int = \i. 2 * mod i (2 ^ 7) end def to1numA: Int -> (Int * Int) = \i. let nextPart = shiftL 7 i in - if (nextPart == 0) {(2 * i, 1 /* last part */)} { + if (nextPart == 0) { + + // last part + (2 * i, 1) + } { let p = to1numA nextPart in (1 /* header isEnd bit */ + setLenPart i + shiftRH 1 (fst p), 1 + snd p) }