0 | module Data.Container.Base.InstanceInterfaces
  1 |
  2 | import Data.Vect
  3 | import Decidable.Equality
  4 | import Data.Fin.Split
  5 | import Data.Finite
  6 |
  7 |
  8 | import Data.Container.Base.Object.Definition
  9 | import Data.Container.Base.Extension.Definition
 10 | import Data.Container.Base.Concrete.Definition
 11 | import Data.Container.Base.Object.Instances
 12 | import Data.Container.Base.Extension.Instances
 13 | import Data.Container.Base.Concrete.Instances
 14 |
 15 | import Data.Tree
 16 | import Data.Container.Base.TreeUtils
 17 | import Data.Functor.Algebra
 18 | import Misc
 19 |
 20 | %hide Prelude.toList
 21 |
 22 |
 23 | ||| Any finite container (i.e. whose each set of positions is finite) can be
 24 | ||| given an algebra instance simply by summing up all the concrete values
 25 | public export
 26 | algebraFinite : 
 27 |   (c : Cont) -> (isFinite : IsFinite c) =>
 28 |   (0 a : Type) -> Num a =>
 29 |   Algebra (Ext c) a
 30 | algebraFinite c {isFinite = MkI @{p}} _
 31 |   = MkAlgebra $ \(shp <| content) => reduce $ values @{p shp} <&> content
 32 |
 33 | namespace VectInstances
 34 |   public export
 35 |   {n : Nat} -> Eq x => Eq (Vect' n x) where
 36 |     v == v' = (toVect v) == (toVect v')
 37 |  
 38 |   public export
 39 |   {n : Nat} -> Show x => Show (Vect' n x) where
 40 |     show v = show (toVect v)
 41 |
 42 |   public export
 43 |   {n : Nat} -> Foldable (Vect' n) where
 44 |     foldr f z v = foldr f z (toVect v)
 45 |   
 46 |   public export
 47 |   {n : Nat} -> Num a => Algebra (Vect' n) a where
 48 |     reduce v = reduce (toVect v)
 49 |
 50 |   public export
 51 |   {n : Nat} -> Traversable (Vect' n) where
 52 |     traverse f v = fromVect <$> traverse f (toVect v)
 53 |
 54 |   -- Applicative and Naperian instance follow because the set of shapes is ()
 55 |
 56 |   -- analogus to Misc.takeFin, but for Vect'
 57 |   public export 
 58 |   take : {n : Nat} ->
 59 |     (s : Fin (S n)) -> Vect' n a -> Vect' (finToNat s) a
 60 |   take s = fromVect . takeFin s . toVect
 61 |
 62 |   public export
 63 |   (++) : {n : Nat} -> Vect' n a -> Vect' m a -> Vect' (n + m) a
 64 |   (++) v1 v2 = () <| \i => case splitSum i of
 65 |     Left i1 => index v1 i1
 66 |     Right i2 => index v2 i2
 67 |
 68 | {---
 69 | Ideally, all instances would be defined in terms of ConcreteTypes,
 70 | but there are totality checking issues with types whose size isn't known
 71 | at compile time
 72 | ---}
 73 | namespace ListInstances
 74 |   ||| Is there a different way to convince Idris' totality checker?
 75 |   public export
 76 |   Eq a => Eq (List' a) where
 77 |     l == l' = assert_total ((toList l) == (toList l'))
 78 |
 79 |   ||| Is there a different way to convince Idris' totality checker?
 80 |   public export
 81 |   Show a => Show (List' a) where
 82 |     show x = assert_total (show (toList x))
 83 |
 84 |   public export
 85 |   Foldable List' where
 86 |     foldr f z v = foldr f z (toList v)
 87 |
 88 |   public export
 89 |   Num a => Algebra List' a where
 90 |     reduce = reduce {f=List} . toList
 91 |
 92 |
 93 |   -- some attempts at fixing partiality below
 94 |   -- public export
 95 |   -- showListHelper : Show a => List' a -> String
 96 |   -- showListHelper (0 <| _) = ""
 97 |   -- showListHelper (1 <| index) = show $ index FZ
 98 |   -- showListHelper ((S k) <| index)
 99 |   --   = let (s, rest) = headTail index
100 |   --     in show s ++ ", " ++ showListHelper (k <| rest)
101 |
102 |   -- public export
103 |   -- showListHelper : Show a => List' a -> String
104 |   -- showListHelper x = show (toList x)
105 |
106 |
107 | namespace BinTreeInstances
108 |   ||| Is there a different way to convince Idris' totality checker?
109 |   public export
110 |   Eq a => Eq (BinTree' a) where
111 |     t == t' = assert_total (toBinTreeSame t == toBinTreeSame t')
112 |
113 |   ||| Is there a different way to convince Idris' totality checker?
114 |   public export
115 |   Show a => Show (BinTree' a) where
116 |     show = assert_total (show . toBinTreeSame)
117 |
118 |   ||| Summing up nodes and leaves of the tree given by the Num a structure
119 |   public export
120 |   Num a => Algebra BinTree' a where
121 |     reduce = reduce {f=BinTreeSame} . toBinTreeSame
122 |
123 |   -- public export
124 |   -- binTreePosInterface : InterfaceOnPositions BinTree DecEq
125 |   -- binTreePosInterface = MkI
126 |
127 |
128 | namespace BinTreeLeafInstances
129 |   ||| Is there a different way to convince Idris' totality checker?
130 |   public export
131 |   Eq a => Eq (BinTreeLeaf' a) where
132 |     t == t' = assert_total (toBinTreeLeaf t == toBinTreeLeaf t')
133 |
134 |   ||| Is there a different way to convince Idris' totality checker?
135 |   public export
136 |   Show a => Show (BinTreeLeaf' a) where
137 |     show = assert_total (show . toBinTreeLeaf)
138 |
139 |   ||| Summing up leaves of the tree given by the Num a structure
140 |   public export
141 |   Num a => Algebra BinTreeLeaf' a where
142 |     reduce = reduce {f=BinTreeLeaf} . toBinTreeLeaf
143 |
144 |   ||| Requires making a choice on which subtree to process first
145 |   public export
146 |   Foldable BinTreeLeaf' where
147 |     foldr f z t = foldr {t=BinTreeLeaf} f z (toBinTreeLeaf t)
148 |
149 |
150 | namespace BinTreeNodeInstances
151 |   ||| Is there a different way to convince Idris' totality checker?
152 |   public export
153 |   Eq a => Eq (BinTreeNode' a) where
154 |     t == t' = assert_total (toBinTreeNode t == toBinTreeNode t')
155 |
156 |   ||| Is there a different way to convince Idris' totality checker?
157 |   public export
158 |   Show a => Show (BinTreeNode' a) where
159 |     show = assert_total (show . toBinTreeNode)
160 |
161 |   ||| Summing up nodes of the tree given by the Num a structure
162 |   public export
163 |   Num a => Algebra BinTreeNode' a where
164 |     reduce = reduce {f=BinTreeNode} . toBinTreeNode
165 |
166 |