-
Notifications
You must be signed in to change notification settings - Fork 483
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
PLT-1539: Use foldr
for Foldable
#5179
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
({cpu: 26593391908 | ||
| mem: 114092648}) | ||
({cpu: 26160853908 | ||
| mem: 112212048}) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
({cpu: 7596820298 | ||
| mem: 28604240}) | ||
({cpu: 7353687298 | ||
| mem: 27547140}) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
({cpu: 14229364305 | ||
| mem: 54977742}) | ||
({cpu: 14180259305 | ||
| mem: 54764242}) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
({cpu: 191619634648 | ||
| mem: 725849980}) | ||
({cpu: 191451412648 | ||
| mem: 725118580}) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
({cpu: 490859997 | ||
| mem: 1606369}) | ||
({cpu: 460200997 | ||
| mem: 1473069}) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
({cpu: 141343245 | ||
| mem: 464193}) | ||
({cpu: 133868245 | ||
| mem: 431693}) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
({cpu: 28136630 | ||
| mem: 110020}) | ||
({cpu: 16383630 | ||
| mem: 58920}) |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -2,66 +2,33 @@ letrec data (List :: * -> *) a | Nil_match where | |
Nil : List a | ||
Cons : a -> List a -> List a | ||
in | ||
let data (Monoid :: * -> *) a | Monoid_match where | ||
CConsMonoid : (\a -> a -> a -> a) a -> a -> Monoid a | ||
in | ||
letrec !fFoldableNil_cfoldMap | ||
: all m. all a. Monoid m -> (a -> m) -> List a -> m | ||
= /\m a -> | ||
\(dMonoid : Monoid m) (eta : a -> m) (eta : List a) -> | ||
Nil_match | ||
{a} eta {all dead. m} (/\dead -> | ||
Monoid_match | ||
{m} dMonoid {m} | ||
(\(v : (\a -> a -> a -> a) m) (v | ||
: m) -> | ||
v)) | ||
(\(x : a) (xs : List a) -> | ||
/\dead -> | ||
Monoid_match | ||
{m} dMonoid {(\a -> a -> a -> a) m} | ||
(\(v : (\a -> a -> a -> a) m) (v : m) -> v) (eta x) | ||
(fFoldableNil_cfoldMap {m} {a} dMonoid eta xs)) | ||
{all dead. dead} | ||
in | ||
let data Bool | Bool_match where | ||
True : Bool | ||
False : Bool | ||
data (MultiplicativeMonoid :: * -> *) a | MultiplicativeMonoid_match where | ||
CConsMultiplicativeMonoid | ||
: (\a -> a -> a -> a) a -> a -> MultiplicativeMonoid a | ||
in fFoldableNil_cfoldMap | ||
{(\a -> a) Bool} {integer} (let !v : MultiplicativeMonoid Bool | ||
= CConsMultiplicativeMonoid | ||
{Bool} (\(l : Bool) (r : Bool) -> | ||
Bool_match | ||
l {all dead. Bool} | ||
(/\dead -> r) (/\dead -> | ||
False) | ||
{all dead. dead}) True | ||
in CConsMonoid | ||
{(\a -> a) Bool} | ||
(\(eta : (\a -> a) Bool) (eta | ||
: (\a -> a) Bool) -> | ||
MultiplicativeMonoid_match | ||
{Bool} v {(\a -> a -> a -> a) Bool} | ||
(\(v : (\a -> a -> a -> a) Bool) (v | ||
: Bool) -> | ||
v) eta eta) | ||
(MultiplicativeMonoid_match | ||
{Bool} v {Bool} | ||
(\(v : (\a -> a -> a -> a) Bool) (v | ||
: Bool) -> | ||
v))) (\(v : integer) -> | ||
ifThenElse | ||
{Bool} | ||
(lessThanEqualsInteger | ||
1 v) False True) | ||
((let a = List integer in \(c : integer -> a -> a) (n : a) -> | ||
c | ||
1 (c | ||
2 (c | ||
3 (c | ||
in | ||
letrec !go : List integer -> Bool | ||
= \(ds : List integer) -> | ||
Nil_match | ||
{integer} ds {all dead. Bool} (/\dead -> True) | ||
(\(x : integer) (xs : List integer) -> | ||
/\dead -> | ||
let !acc : Bool = go xs in Bool_match | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. why didn't we break at the |
||
(ifThenElse | ||
{Bool} | ||
(lessThanEqualsInteger 1 x) | ||
False True) {all dead. Bool} | ||
(/\dead -> acc) (/\dead -> | ||
False) | ||
{all dead. dead}) | ||
{all dead. dead} | ||
Comment on lines
+15
to
+23
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. So everything works just fine except GHC makes a thunk for |
||
in | ||
let !eta : List integer | ||
= (let a = List integer in \(c : integer -> a -> a) (n : a) -> | ||
c | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. this is hilarious but I'm not sure what we could do better |
||
1 (c | ||
2 (c | ||
3 | ||
(c | ||
4 | ||
(c | ||
5 | ||
|
@@ -76,5 +43,6 @@ in fFoldableNil_cfoldMap | |
(c | ||
10 | ||
n)))))))))) | ||
(\(ds : integer) (ds : List integer) -> Cons {integer} ds ds) | ||
(Nil {integer})) | ||
(\(ds : integer) (ds : List integer) -> Cons {integer} ds ds) | ||
(Nil {integer}) | ||
in go eta |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
({cpu: 1748100 | ||
| mem: 7700}) | ||
({cpu: 736100 | ||
| mem: 3300}) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
({cpu: 28136630 | ||
| mem: 110020}) | ||
({cpu: 16383630 | ||
| mem: 58920}) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
({cpu: 28136630 | ||
| mem: 110020}) | ||
({cpu: 16383630 | ||
| mem: 58920}) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
prettyprinting improvement: always put the binding on the next line so we can indent it just 2 instead of 7 for
letrec