0 | module Generics.SOP
  1 |
  2 | import Decidable.Equality
  3 |
  4 | import public Data.List.Elem
  5 | import public Data.SOP
  6 |
  7 | %default total
  8 |
  9 | ||| Interface for converting a data type from and to
 10 | ||| its generic representation as a sum of products.
 11 | |||
 12 | ||| Additional Idris coolness: This comes with proofs
 13 | ||| that `from . to = id` and `to . from = id` and
 14 | ||| thus, that `t` and `SOP code` are indeed isomorphic.
 15 | public export
 16 | interface Generic (0 t : Type) (0 code : List $ List Type) | t where
 17 |   constructor MkGeneric
 18 |   ||| Converts the data type to its generic representation.
 19 |   from : (v : t) -> SOP I code
 20 |
 21 |   ||| Converts the generic representation back to the original
 22 |   ||| value.
 23 |   to   : (v : SOP I code) -> t
 24 |
 25 |   ||| Proof that `to . from = id`.
 26 |   fromToId : (v : t) -> to (from v) = v
 27 |
 28 |   ||| Proof that `from . to = id`.
 29 |   toFromId : (v : SOP I code) -> from (to v) = v
 30 |
 31 | export
 32 | fromInjective :
 33 |      {auto _ : Generic t code}
 34 |   -> (0 x : t)
 35 |   -> (0 y : t)
 36 |   -> (from x = from y)
 37 |   -> x = y
 38 | fromInjective x y prf = rewrite sym $ fromToId y in lemma2
 39 |
 40 |   where
 41 |     lemma1 : to {t = t} (from x) = to {t = t} (from y)
 42 |     lemma1 = cong to prf
 43 |
 44 |     lemma2 : x = to {t = t} (from y)
 45 |     lemma2 = rewrite sym $ fromToId x in lemma1
 46 |
 47 | public export
 48 | 0 Code : (t : Type) -> Generic t code => List $ List Type
 49 | Code _ = code
 50 |
 51 | ||| Tries to extract the arguments of a single constructor
 52 | ||| from a value's generic representation.
 53 | public export
 54 | genExtract :
 55 |      (0 ts : List Type)
 56 |   -> (v : t)
 57 |   -> {auto _ : Generic t code}
 58 |   -> {auto prf : Elem ts code}
 59 |   -> Maybe (NP I ts)
 60 | genExtract ts v = extractSOP ts $ from v
 61 |
 62 | ||| Tries to extract the value of a single one argument
 63 | ||| constructor from a value's generic representation.
 64 | public export
 65 | genExtract1 :
 66 |      (0 t' : Type)
 67 |   -> (v : t)
 68 |   -> {auto _   : Generic t code}
 69 |   -> {auto prf : Elem [t'] code}
 70 |   -> Maybe t'
 71 | genExtract1 t' v = hd <$> genExtract [t'] v
 72 |
 73 | ||| Returns all value from a generic enum type
 74 | ||| (all nullary constructors) wrapped in homogeneous n-ary product.
 75 | public export
 76 | valuesNP : Generic t code => (et : EnumType code) =>
 77 |            NP_ (List Type) (K t) code
 78 | valuesNP = hmap (to . MkSOP) (run et)
 79 |
 80 |   where
 81 |     run :  EnumType kss -> NP_ (List k) (K (NS_ (List k) (NP f) kss)) kss
 82 |     run EZ     = []
 83 |     run (ES x) = Z [] :: mapNP (\ns => S ns) (run x)
 84 |
 85 | ||| Returns all value from a generic enum type
 86 | ||| (all nullary constructors) wrapped in a list.
 87 | public export %inline
 88 | values : Generic t code => (et : EnumType code) => List t
 89 | values = collapseNP valuesNP
 90 |
 91 | ||| Like `valuesNP` but takes the erased value type as an
 92 | ||| explicit argument to help with type inference.
 93 | public export %inline
 94 | valuesForNP :
 95 |      (0 t: Type)
 96 |   -> {auto _ : Generic t code}
 97 |   -> {auto et : EnumType code}
 98 |   -> NP_ (List Type) (K t) code
 99 | valuesForNP _ = valuesNP
100 |
101 | ||| Like `values` but takes the erased value type as an
102 | ||| explicit argument to help with type inference.
103 | public export %inline
104 | valuesFor : (0 t : Type) -> Generic t code => (et : EnumType code) => List t
105 | valuesFor _ = values
106 |
107 | --------------------------------------------------------------------------------
108 | --          Generic Implementation Functions
109 | --------------------------------------------------------------------------------
110 |
111 | ||| Default `(==)` implementation for data types with a `Generic`
112 | ||| instance.
113 | public export
114 | genEq : Generic t code => POP Eq code => t -> t -> Bool
115 | genEq x y = from x == from y
116 |
117 | ||| Default `compare` implementation for data types with a `Generic`
118 | ||| instance.
119 | public export
120 | genCompare : Generic t code => POP Ord code => t -> t -> Ordering
121 | genCompare x y = compare (from x) (from y)
122 |
123 | ||| Default `decEq` implementation for data types with a `Generic`
124 | ||| instance.
125 | public export
126 | genDecEq :
127 |      {auto _ : Generic t code}
128 |   -> {auto _ : POP DecEq code}
129 |   -> (x : t)
130 |   -> (y : t)
131 |   -> Dec (x = y)
132 | genDecEq x y =
133 |   case decEq (from x) (from y) of
134 |     (Yes prf)   => Yes $ fromInjective x y prf
135 |     (No contra) => No $ \h => contra (cong from h)
136 |
137 | ||| Default `(<+>)` implementation for data types with a `Generic`
138 | ||| instance.
139 | public export
140 | genAppend :
141 |      {auto _ : Generic t [ts]}
142 |   -> {auto _ : POP Semigroup [ts]}
143 |   -> t -> t -> t
144 | genAppend x y = to $ from x <+> from y
145 |
146 | ||| Default `neutral` implementation for data types with a `Generic`
147 | ||| instance.
148 | public export
149 | genNeutral :  Generic t [ts] => POP Monoid [ts] => t
150 | genNeutral = to neutral
151 |
152 | --------------------------------------------------------------------------------
153 | --          Prelude Implementations
154 | --------------------------------------------------------------------------------
155 |
156 | -- I wrote the implementations below manually to get a feel for
157 | -- their general structure before starting with deriving
158 | -- them via elaborator reflection.
159 |
160 | public export
161 | Generic () [[]] where
162 |   from () = MkSOP $ Z []
163 |
164 |   to (MkSOP $ Z []) = ()
165 |   to (MkSOP $ S _) impossible
166 |
167 |   fromToId () = Refl
168 |
169 |   toFromId (MkSOP $ Z []) = Refl
170 |
171 | public export
172 | Generic (a,b) [[a,b]] where
173 |   from (a,b) = MkSOP $ Z [a,b]
174 |
175 |   to (MkSOP $ Z [a,b]) = (a,b)
176 |   to (MkSOP $ S _) impossible
177 |
178 |   fromToId (a,b) = Refl
179 |
180 |   toFromId (MkSOP $ Z [a,b]) = Refl
181 |
182 | public export
183 | Generic (LPair a b) [[a,b]] where
184 |   from (a # b) = MkSOP $ Z [a,b]
185 |
186 |   to (MkSOP $ Z [a,b]) = (a # b)
187 |   to (MkSOP $ S _) impossible
188 |
189 |   fromToId (a # b) = Refl
190 |
191 |   toFromId (MkSOP $ Z [a, b]) = Refl
192 |
193 | public export
194 | Generic Void [] where
195 |   from v impossible
196 |
197 |   to (MkSOP v) impossible
198 |
199 |   fromToId v impossible
200 |
201 |   toFromId (MkSOP v) impossible
202 |
203 | public export
204 | Generic (Stream a) [[a, Inf (Stream a)]] where
205 |   from (h :: t) = MkSOP $ Z [h,t]
206 |
207 |   to (MkSOP $ Z [h,t])  = h :: t
208 |
209 |   fromToId (h :: t) = Refl
210 |
211 |   toFromId (MkSOP $ Z [h,t]) = Refl
212 |