[fix] added missing foldable for trees

Author: bgavran

src/Data/Container/Base/InstanceInterfaces.idr

@@ -13,6 +13,7 @@ import Data.Container.Base.Extension.Instances
 import Data.Container.Base.Concrete.Instances
 
 import Data.Tree
+import Data.Container.Base.TreeUtils
 import Data.Algebra
 import Misc
 
@@ -129,6 +130,11 @@ namespace BinTreeLeafInstances
   Num a => Algebra BinTreeLeaf' a where
     reduce = reduce {f=BinTreeLeaf} . toBinTreeLeaf
 
+  ||| Requires making a choice on which subtree to process first
+  public export
+  Foldable BinTreeLeaf' where
+    foldr f z t = foldr {t=BinTreeLeaf} f z (toBinTreeLeaf t)
+
 
 namespace BinTreeNodeInstances
   ||| Is there a different way to convince Idris' totality checker?

src/Data/Tree.idr

@@ -120,17 +120,18 @@ namespace BinaryTrees
         pure x = Leaf x
         fs <*> xs = map {f=BinTreeLeaf} (uncurry ($)) $ liftA2BinTreeLeaf fs xs 
 
-    -- Is this even possible?
-    -- probably is, but foldable really means traversing in a linear order
-    -- with tree in principle we'd have to process each subtree in parallel
-    -- but we could implement foldable by first making a choice on how to traverse a tree and turn it into a list, and then performing the fold on the resulting list
+    ||| This requires us traversing a tree in a linear order
+    ||| This means we have to make a choice on which subtree to process first
+    ||| Another way is to first implement a traversal of the tree, and
+    ||| then use that
     public export
     Foldable BinTreeLeaf where
       foldr f z (Leaf leaf) = f leaf z
-      foldr f z (Node _ leftTree rightTree) = ?oo_1 where
-        leftTreeRes : acc
-        leftTreeRes = foldr {t=BinTreeLeaf} f z leftTree
-        rightTreeRes = foldr {t=BinTreeLeaf} f z rightTree
+      foldr f z (Node () leftTree rightTree) =
+        -- Process left first, i.e. fold right with z, then use that 
+        -- as accumulator for left
+        let rightResult = foldr {t=BinTreeLeaf} f z rightTree
+        in foldr {t=BinTreeLeaf} f rightResult leftTree
 
   namespace NodesOnly
     public export

tensortype.ipkg

@@ -44,6 +44,7 @@ modules = Data.Container.Base
         , Data.Container.Applicative.Extension.Instances
         , Data.Container.Applicative.Concrete.Instances
         , Data.Container.Applicative.Product.Interfaces
+        , Data.Container.Applicative.TreeUtils
 
         , Data.Container.SubTerm