28 | module Spidr.Data.Literal
30 | import Data.List.Elem
32 | import public Spidr.Shape
36 | data Literal : Shape -> Type -> Type where
37 | Scalar : a -> Literal [] a
38 | Nil : Literal (0 :: ds) a
39 | (::) : Literal ds a -> Literal (d :: ds) a -> Literal (S d :: ds) a
42 | fromInteger : Num a => Integer -> Literal [] a
43 | fromInteger = Scalar . fromInteger
46 | fromDouble : Double -> Literal [] Double
51 | True, False : Literal [] Bool
53 | False = Scalar False
56 | Functor (Literal shape) where
57 | map f (Scalar x) = Scalar (f x)
59 | map f (x :: xs) = map f x :: map f xs
61 | functorIdentity : (xs : Literal shape a) -> map Prelude.id xs = xs
62 | functorIdentity (Scalar _) = Refl
63 | functorIdentity [] = Refl
64 | functorIdentity (x :: xs) = cong2 (::) (functorIdentity x) (functorIdentity xs)
66 | functorComposition :
67 | (xs : Literal shape a) -> (f : a -> b) -> (g : b -> c) -> map (g . f) xs = map g (map f xs)
68 | functorComposition (Scalar _) _ _ = Refl
69 | functorComposition [] _ _ = Refl
70 | functorComposition (x :: xs) f g =
71 | cong2 (::) (functorComposition x f g) (functorComposition xs f g)
74 | {shape : _} -> Applicative (Literal shape) where
75 | pure x = case shape of
78 | (S d :: ds) => pure x :: assert_total (pure x)
80 | (Scalar f) <*> (Scalar x) = Scalar (f x)
82 | (f :: fs) <*> (x :: xs) = (f <*> x) :: (fs <*> xs)
84 | applicativeIdentity : (xs : Literal shape a) -> pure Prelude.id <*> xs = xs
85 | applicativeIdentity (Scalar _) = Refl
86 | applicativeIdentity [] = Refl
87 | applicativeIdentity (x :: xs) = cong2 (::) (applicativeIdentity x) (applicativeIdentity xs)
89 | applicativeHomomorphism :
90 | (shape : Shape) -> (f : a -> b) -> (x : a) -> pure f <*> pure x = pure {f = Literal shape} (f x)
91 | applicativeHomomorphism [] _ _ = Refl
92 | applicativeHomomorphism (d :: ds) f x = forCons d ds f x
99 | pure f <*> pure x = pure {f = Literal (d :: ds)} (f x)
100 | forCons 0 _ _ _ = Refl
101 | forCons (S d) ds f x = cong2 (::) (applicativeHomomorphism ds f x) (forCons d ds f x)
103 | applicativeInterchange :
104 | (fs : Literal shape (a -> b)) -> (x : a) -> fs <*> pure x = pure ($
x) <*> fs
105 | applicativeInterchange (Scalar _) _ = Refl
106 | applicativeInterchange [] _ = Refl
107 | applicativeInterchange (f :: fs) x =
108 | cong2 (::) (applicativeInterchange f x) (applicativeInterchange fs x)
110 | applicativeComposition :
111 | (xs : Literal shape a) ->
112 | (fs : Literal shape (a -> b)) ->
113 | (gs : Literal shape (b -> c)) ->
114 | pure (.) <*> gs <*> fs <*> xs = gs <*> (fs <*> xs)
115 | applicativeComposition (Scalar _) (Scalar _) (Scalar _) = Refl
116 | applicativeComposition [] [] [] = Refl
117 | applicativeComposition (x :: xs) (f :: fs) (g :: gs) =
118 | cong2 (::) (applicativeComposition x f g) (applicativeComposition xs fs gs)
121 | Foldable (Literal shape) where
122 | foldr f acc (Scalar x) = f x acc
123 | foldr _ acc [] = acc
124 | foldr f acc (x :: xs) = foldr f (foldr f acc xs) x
127 | Traversable (Literal shape) where
128 | traverse f (Scalar x) = [| Scalar (f x) |]
129 | traverse f [] = pure []
130 | traverse f (x :: xs) = [| traverse f x :: traverse f xs |]
133 | Zippable (Literal shape) where
134 | zipWith f (Scalar x) (Scalar y) = Scalar (f x y)
135 | zipWith _ [] [] = []
136 | zipWith f (x :: xs) (y :: ys) = zipWith f x y :: zipWith f xs ys
138 | zipWith3 f (Scalar x) (Scalar y) (Scalar z) = Scalar (f x y z)
139 | zipWith3 _ [] [] [] = []
140 | zipWith3 f (x :: xs) (y :: ys) (z :: zs) = zipWith3 f x y z :: zipWith3 f xs ys zs
142 | unzipWith f (Scalar x) = let (x, y) = f x in (Scalar x, Scalar y)
143 | unzipWith _ [] = ([], [])
144 | unzipWith f (x :: xs) =
145 | let (x, y) = unzipWith f x
146 | (xs, ys) = unzipWith f xs
147 | in (x :: xs, y :: ys)
149 | unzipWith3 f (Scalar x) = let (x, y, z) = f x in (Scalar x, Scalar y, Scalar z)
150 | unzipWith3 _ [] = ([], [], [])
151 | unzipWith3 f (x :: xs) =
152 | let (x, y, z) = unzipWith3 f x
153 | (xs, ys, zs) = unzipWith3 f xs
154 | in (x :: xs, y :: ys, z :: zs)
158 | all : Literal shape Bool -> Bool
159 | all xs = foldr (\x, y => x && y) True xs
162 | Num a => Num (Literal [] a) where
163 | x + y = [| x + y |]
164 | x * y = [| x * y |]
165 | fromInteger = Scalar . fromInteger
168 | negate : Neg a => Literal shape a -> Literal shape a
169 | negate = map negate
172 | Eq a => Eq (Literal shape a) where
173 | x == y = all (zipWith (==) x y)
175 | toVect : Literal (d :: ds) a -> Vect d (Literal ds a)
177 | toVect (x :: y) = x :: toVect y
181 | {shape : _} -> Show a => Show (Literal shape a) where
182 | show = showWithIndent "" where
183 | showWithIndent : {shape : _} -> String -> Literal shape a -> String
184 | showWithIndent _ (Scalar x) = show x
185 | showWithIndent _ [] = "[]"
186 | showWithIndent {shape = [S _]} _ x = show (toList x)
187 | showWithIndent {shape = (S d :: dd :: ddd)} indent (x :: xs) =
188 | let indent = " " ++ indent
189 | first = showWithIndent indent x
190 | rest = foldMap (\e => ",\n" ++ indent ++ showWithIndent indent e) (toVect xs)
191 | in "[" ++ first ++ rest ++ "]"
194 | {shape : _} -> Cast (Array shape a) (Literal shape a) where
195 | cast x with (shape)
196 | cast x | [] = Scalar x
197 | cast _ | (0 :: _) = []
198 | cast (x :: xs) | (S d :: ds) = cast x :: cast xs
201 | [toArray] Cast (Literal shape a) (Array shape a) where
202 | cast (Scalar x) = x
204 | cast (x :: y) = cast @{toArray} x :: cast @{toArray} y
211 | data All : (0 p : a -> Type) -> Literal shape a -> Type where
212 | Scalar : forall x . p x -> All p (Scalar x)
214 | (::) : All p x -> All p xs -> All p (x :: xs)
222 | data All2 : (p : a -> b -> Type) -> Literal shape a -> Literal shape b -> Type where
223 | Scalar : forall a, b . p a b -> All2 p (Scalar a) (Scalar b)
225 | (::) : All2 p a b -> All2 p as bs -> All2 p (a :: as) (b :: bs)