forked from idris-lang/Idris2
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[ lazy ] Weakly memoise lazy expressions on chez and racket
- Loading branch information
Showing
22 changed files
with
328 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
File renamed without changes.
File renamed without changes.
File renamed without changes.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,69 @@ | ||
-- This tests checks, whether lazy values constants are | ||
-- properly memoized. If they are not, this test | ||
-- will perform 10^20 additions and will therefore not | ||
-- finish in reasonable time. | ||
n0 : Lazy Nat | ||
n0 = 1 | ||
|
||
n1 : Lazy Nat | ||
n1 = n0 + n0 + n0 + n0 + n0 + n0 + n0 + n0 + n0 + n0 | ||
|
||
n2 : Lazy Nat | ||
n2 = n1 + n1 + n1 + n1 + n1 + n1 + n1 + n1 + n1 + n1 | ||
|
||
n3 : Lazy Nat | ||
n3 = n2 + n2 + n2 + n2 + n2 + n2 + n2 + n2 + n2 + n2 | ||
|
||
n4 : Lazy Nat | ||
n4 = n3 + n3 + n3 + n3 + n3 + n3 + n3 + n3 + n3 + n3 | ||
|
||
n5 : Lazy Nat | ||
n5 = n4 + n4 + n4 + n4 + n4 + n4 + n4 + n4 + n4 + n4 | ||
|
||
n6 : Lazy Nat | ||
n6 = n5 + n5 + n5 + n5 + n5 + n5 + n5 + n5 + n5 + n5 | ||
|
||
n7 : Lazy Nat | ||
n7 = n6 + n6 + n6 + n6 + n6 + n6 + n6 + n6 + n6 + n6 | ||
|
||
n8 : Lazy Nat | ||
n8 = n7 + n7 + n7 + n7 + n7 + n7 + n7 + n7 + n7 + n7 | ||
|
||
n9 : Lazy Nat | ||
n9 = n8 + n8 + n8 + n8 + n8 + n8 + n8 + n8 + n8 + n8 | ||
|
||
n10 : Lazy Nat | ||
n10 = n9 + n9 + n9 + n9 + n9 + n9 + n9 + n9 + n9 + n9 | ||
|
||
n11 : Lazy Nat | ||
n11 = n10 + n10 + n10 + n10 + n10 + n10 + n10 + n10 + n10 + n10 | ||
|
||
n12 : Lazy Nat | ||
n12 = n11 + n11 + n11 + n11 + n11 + n11 + n11 + n11 + n11 + n11 | ||
|
||
n13 : Lazy Nat | ||
n13 = n12 + n12 + n12 + n12 + n12 + n12 + n12 + n12 + n12 + n12 | ||
|
||
n14 : Lazy Nat | ||
n14 = n13 + n13 + n13 + n13 + n13 + n13 + n13 + n13 + n13 + n13 | ||
|
||
n15 : Lazy Nat | ||
n15 = n14 + n14 + n14 + n14 + n14 + n14 + n14 + n14 + n14 + n14 | ||
|
||
n16 : Lazy Nat | ||
n16 = n15 + n15 + n15 + n15 + n15 + n15 + n15 + n15 + n15 + n15 | ||
|
||
n17 : Lazy Nat | ||
n17 = n16 + n16 + n16 + n16 + n16 + n16 + n16 + n16 + n16 + n16 | ||
|
||
n18 : Lazy Nat | ||
n18 = n17 + n17 + n17 + n17 + n17 + n17 + n17 + n17 + n17 + n17 | ||
|
||
n19 : Lazy Nat | ||
n19 = n18 + n18 + n18 + n18 + n18 + n18 + n18 + n18 + n18 + n18 | ||
|
||
n20 : Lazy Nat | ||
n20 = n19 + n19 + n19 + n19 + n19 + n19 + n19 + n19 + n19 + n19 | ||
|
||
main : IO () | ||
main = do printLn n20 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
100000000000000000000 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
. ../../testutils.sh | ||
|
||
run Memo.idr |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,34 @@ | ||
-- This tests checks, whether lazy values constants are | ||
-- properly memoized. If they are not, this test | ||
-- will perform 10^20 additions and will therefore not | ||
-- finish in reasonable time. | ||
|
||
-- We return lazy values in a monad to avoid behaviour of common expression elimination | ||
|
||
nx : Lazy Nat -> IO $ Lazy Nat | ||
nx n = pure $ delay $ force n + force n + force n + force n + force n + force n + force n + force n + force n + force n | ||
|
||
main : IO () | ||
main = do | ||
n0 <- pure 1 | ||
n1 <- nx n0 | ||
n2 <- nx n1 | ||
n3 <- nx n2 | ||
n4 <- nx n3 | ||
n5 <- nx n4 | ||
n6 <- nx n5 | ||
n7 <- nx n6 | ||
n8 <- nx n7 | ||
n9 <- nx n8 | ||
n10 <- nx n9 | ||
n11 <- nx n10 | ||
n12 <- nx n11 | ||
n13 <- nx n12 | ||
n14 <- nx n13 | ||
n15 <- nx n14 | ||
n16 <- nx n15 | ||
n17 <- nx n16 | ||
n18 <- nx n17 | ||
n19 <- nx n18 | ||
n20 <- nx n19 | ||
printLn n20 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
100000000000000000000 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
. ../../testutils.sh | ||
|
||
run Memo.idr |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,45 @@ | ||
import Data.List.Lazy | ||
import Data.Stream | ||
|
||
import Debug.Trace | ||
|
||
S' : (pref : String) -> Nat -> Nat | ||
S' pref = S . traceValBy (\n => "\{pref} \{show n}") | ||
|
||
-- We return lazy values in a monad to avoid behaviour of common expression elimination | ||
|
||
natsS' : IO $ Stream Nat | ||
natsS' = pure $ iterate (S' "> s") Z | ||
|
||
natsL' : IO $ LazyList Nat | ||
natsL' = pure $ iterateN 200 (S' "> ll") Z | ||
|
||
main : IO () | ||
main = do | ||
natsS <- natsS' | ||
|
||
putStrLn "\n-----------------------" | ||
putStrLn "first take of stream (should be `s 0..9`)" | ||
printLn $ take 10 natsS | ||
|
||
putStrLn "\n-----------------------" | ||
putStrLn "second take of stream (should be no `s *`)" | ||
printLn $ take 10 natsS | ||
|
||
natsL <- natsL' | ||
|
||
putStrLn "\n-----------------------" | ||
putStrLn "first take of short lazy list (should be `ll 0..9`)" | ||
printLn $ take 10 natsL | ||
|
||
putStrLn "\n-----------------------" | ||
putStrLn "second take of short lazy list (should be no `ll *`)" | ||
printLn $ take 10 natsL | ||
|
||
putStrLn "\n-----------------------" | ||
putStrLn "first take of longer lazy list (should be `ll 10..14`)" | ||
printLn $ take 15 natsL | ||
|
||
putStrLn "\n-----------------------" | ||
putStrLn "second take of longer lazy list (should be no `ll *`)" | ||
printLn $ take 15 natsL |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,49 @@ | ||
|
||
----------------------- | ||
first take of stream (should be `s 0..9`) | ||
> s 0 | ||
> s 1 | ||
> s 2 | ||
> s 3 | ||
> s 4 | ||
> s 5 | ||
> s 6 | ||
> s 7 | ||
> s 8 | ||
> s 9 | ||
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9] | ||
|
||
----------------------- | ||
second take of stream (should be no `s *`) | ||
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9] | ||
|
||
----------------------- | ||
first take of short lazy list (should be `ll 0..9`) | ||
> ll 0 | ||
> ll 1 | ||
> ll 2 | ||
> ll 3 | ||
> ll 4 | ||
> ll 5 | ||
> ll 6 | ||
> ll 7 | ||
> ll 8 | ||
> ll 9 | ||
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9] | ||
|
||
----------------------- | ||
second take of short lazy list (should be no `ll *`) | ||
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9] | ||
|
||
----------------------- | ||
first take of longer lazy list (should be `ll 10..14`) | ||
> ll 10 | ||
> ll 11 | ||
> ll 12 | ||
> ll 13 | ||
> ll 14 | ||
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14] | ||
|
||
----------------------- | ||
second take of longer lazy list (should be no `ll *`) | ||
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
. ../../testutils.sh | ||
|
||
run --find-ipkg Memo.idr |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
package test | ||
|
||
main = Memo | ||
|
||
depends = contrib |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,36 @@ | ||
import Data.List.Lazy | ||
|
||
import Debug.Trace | ||
|
||
S' : (pref : String) -> Nat -> Nat | ||
S' pref = S . traceValBy (\n => "\{pref} \{show n}") | ||
|
||
-- We return lazy values in a monad to avoid behaviour of common expression elimination | ||
|
||
natsL' : IO $ LazyList Nat | ||
natsL' = pure $ iterateN 200 (S' "> ll") Z | ||
|
||
%foreign "scheme,chez:collect" | ||
"scheme,racket:collect-garbage" | ||
prim__gc : PrimIO () | ||
|
||
gc : IO () | ||
gc = primIO prim__gc | ||
|
||
main : IO () | ||
main = do | ||
natsL <- natsL' | ||
|
||
putStrLn "\n-----------------------" | ||
putStrLn "first take of lazy list (should be `ll 0..9`)" | ||
printLn $ take 10 natsL | ||
|
||
putStrLn "\n-----------------------" | ||
putStrLn "second take of lazy list (should be no `ll *`)" | ||
printLn $ take 10 natsL | ||
|
||
gc | ||
|
||
putStrLn "\n-----------------------" | ||
putStrLn "take of lazy list after gc (should be `ll 0..9`)" | ||
printLn $ take 10 natsL |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,32 @@ | ||
|
||
----------------------- | ||
first take of lazy list (should be `ll 0..9`) | ||
> ll 0 | ||
> ll 1 | ||
> ll 2 | ||
> ll 3 | ||
> ll 4 | ||
> ll 5 | ||
> ll 6 | ||
> ll 7 | ||
> ll 8 | ||
> ll 9 | ||
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9] | ||
|
||
----------------------- | ||
second take of lazy list (should be no `ll *`) | ||
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9] | ||
|
||
----------------------- | ||
take of lazy list after gc (should be `ll 0..9`) | ||
> ll 0 | ||
> ll 1 | ||
> ll 2 | ||
> ll 3 | ||
> ll 4 | ||
> ll 5 | ||
> ll 6 | ||
> ll 7 | ||
> ll 8 | ||
> ll 9 | ||
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
. ../../testutils.sh | ||
|
||
run --find-ipkg Memo.idr |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
package test | ||
|
||
main = Memo | ||
|
||
depends = contrib |