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