From ded2e206c2b5d24a23d5d2d42a1250c8c3f4a473 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 22 Jul 2024 13:26:25 +0200
Subject: [PATCH] use for and rfor as primitive Foldable fields

---
 Stdlib/Trait/Foldable/Monomorphic.juvix | 40 +++++++++++++------------
 Stdlib/Trait/Foldable/Polymorphic.juvix | 28 +++++++++--------
 2 files changed, 36 insertions(+), 32 deletions(-)

diff --git a/Stdlib/Trait/Foldable/Monomorphic.juvix b/Stdlib/Trait/Foldable/Monomorphic.juvix
index f3e0a023..ae98167c 100644
--- a/Stdlib/Trait/Foldable/Monomorphic.juvix
+++ b/Stdlib/Trait/Foldable/Monomorphic.juvix
@@ -6,8 +6,16 @@ import Stdlib.Trait.Foldable.Polymorphic as Poly;
 --- A trait for combining elements into a single result, processing one element at a time.
 trait
 type Foldable (container elem : Type) :=
-  mkFoldable {-- Combine the elements of the type using the provided function starting with the element in the left-most position.
-  foldl : {B : Type} -> (B -> elem -> B) -> B -> container -> B};
+  mkFoldable {
+    -- Combine the elements of the type using the provided function starting with the element in the left-most position.
+    syntax iterator for {init := 1; range := 1};
+    {-# inline: 0 #-}
+    for : {B : Type} -> (B -> elem -> B) -> B -> container -> B;
+
+    syntax iterator rfor {init := 1; range := 1};
+    {-# inline: 0 #-}
+    rfor : {B : Type} -> (B -> elem -> B) -> B → container → B
+  };
 
 open Foldable;
 
@@ -16,9 +24,19 @@ open Foldable;
 fromPolymorphicFoldable
   {f : Type -> Type} {{foldable : Poly.Foldable f}} {elem} : Foldable (f elem) elem :=
   mkFoldable@{
-    foldl : {B : Type} -> (B -> elem -> B) -> B -> f elem -> B := Poly.foldl
+    for := Poly.for;
+    rfor := Poly.rfor
   };
 
+foldl
+  {container elem}
+  {{Foldable container elem}}
+  {B : Type}
+  (g : B -> elem -> B)
+  (ini : B)
+  (ls : container)
+  : B := for (acc := ini) (x in ls) {g acc x};
+
 --- Combine the elements of the type using the provided function starting with the element in the right-most position.
 foldr
   {container elem : Type}
@@ -26,19 +44,3 @@ foldr
   {B : Type}
   (g : elem -> B -> B)
   : B -> container -> B := foldl (flip g);
-
-syntax iterator for {init := 1; range := 1};
-
-{-# inline: 0 #-}
-for
-  {container elem : Type}
-  {B}
-  {{Foldable container elem}}
-  : (B -> elem -> B) -> B -> container -> B := foldl;
-
-syntax iterator rfor {init := 1; range := 1};
-
-{-# inline: 0 #-}
-rfor
-  {container elem : Type} {B} {{Foldable container elem}} (i : B → elem → B) : B → container → B :=
-  foldr (flip i);
diff --git a/Stdlib/Trait/Foldable/Polymorphic.juvix b/Stdlib/Trait/Foldable/Polymorphic.juvix
index acf66bfc..3078f7b4 100644
--- a/Stdlib/Trait/Foldable/Polymorphic.juvix
+++ b/Stdlib/Trait/Foldable/Polymorphic.juvix
@@ -5,21 +5,23 @@ import Stdlib.Function open;
 --- A trait for combining elements into a single result, processing one element at a time.
 trait
 type Foldable (f : Type -> Type) :=
-  mkFoldable {-- Combine the elements of the type using the provided function starting with the element in the left-most position.
-  foldl : {A B : Type} -> (B -> A -> B) -> B -> f A -> B};
+  mkFoldable {
+    -- Combine the elements of the type using the provided function starting with the element in the left-most position.
+    syntax iterator for {init := 1; range := 1};
+    {-# inline: 0 #-}
+    for : {A B : Type} -> (B -> A -> B) -> B -> f A -> B;
+
+    syntax iterator rfor {init := 1; range := 1};
+    {-# inline: 0 #-}
+    rfor : {A B : Type} -> (B → A → B) -> B → f A → B
+  };
 
 open Foldable public;
 
 --- Combine the elements of the type using the provided function starting with the element in the right-most position.
-foldr {f : Type -> Type} {{Foldable f}} {A B : Type} (g : A -> B -> B) : B -> f A -> B :=
-  foldl (flip g);
-
-syntax iterator for {init := 1; range := 1};
-
-{-# inline: 0 #-}
-for {f : Type -> Type} {A B} {{Foldable f}} : (B -> A -> B) -> B -> f A -> B := foldl;
+foldl {f : Type -> Type} {{Foldable f}} {A B : Type} (g : B -> A -> B) (ini : B) (ls : f A) : B :=
+  for (acc := ini) (x in ls) {g acc x};
 
-syntax iterator rfor {init := 1; range := 1};
-
-{-# inline: 0 #-}
-rfor {f : Type -> Type} {A B} {{Foldable f}} (i : B → A → B) : B → f A → B := foldr (flip i);
+--- Combine the elements of the type using the provided function starting with the element in the right-most position.
+foldr {f : Type -> Type} {{Foldable f}} {A B : Type} (g : A -> B -> B) (ini : B) (ls : f A) : B :=
+  rfor (acc := ini) (x in ls) {g x acc};