
   0 | ||| Union types (= sum types) in the FFI.
   1 | module JS.Union
   2 | 
   3 | import Data.List.Quantifiers.Extra
   4 | import JS.Inheritance
   5 | import JS.Marshall
   6 | 
   7 | %default total
   8 | 
   9 | public export
  10 | data NPP :  (f : Type -> Type -> Type)
  11 |          -> (ps1 : List Type)
  12 |          -> (ps2 : List Type)
  13 |          -> Type where
  14 |   Nil  : NPP f Nil Nil
  15 |   (::) : f a b -> NPP f ps1 ps2 -> NPP f (a :: ps1) (b :: ps2)
  16 | 
  17 | appToFFI : NPP ToFFI ps1 ps2 -> HSum ps1 -> HSum ps2
  18 | appToFFI (_ :: _) (Here v)  = Here $ toFFI v
  19 | appToFFI (_ :: t) (There y) = There $ appToFFI t y
  20 | appToFFI [] x = absurd x
  21 | 
  22 | appFromFFI : NPP FromFFI ps1 ps2 -> HSum ps2 -> Maybe $ HSum ps1
  23 | appFromFFI (_ :: _) (Here v)  = Here <$> fromFFI v
  24 | appFromFFI (_ :: t) (There y) = There <$> appFromFFI t y
  25 | appFromFFI []       x         = absurd x
  26 | 
  27 | --------------------------------------------------------------------------------
  28 | --          Union2
  29 | --------------------------------------------------------------------------------
  30 | 
  31 | export
  32 | data Union2 : Type -> Type -> Type where [external]
  33 | 
  34 | export
  35 | toUnion2 : HSum [a,b] -> Union2 a b
  36 | toUnion2 = collapse' . hmap believe_me
  37 | 
  38 | export
  39 | fromUnion2 : All SafeCast [a,b] => Union2 a b -> Maybe $ HSum [a,b]
  40 | fromUnion2 = safeCastAny
  41 | 
  42 | export
  43 | (npp : NPP ToFFI [a,b] [m,n]) =>
  44 |   ToFFI (HSum [a,b]) (Union2 m n) where
  45 |     toFFI ns = toUnion2 $ appToFFI npp ns
  46 | 
  47 | export
  48 | (npp : NPP FromFFI [a,b] [m,n]) => All SafeCast [m,n] =>
  49 |   FromFFI (HSum [a,b]) (Union2 m n) where
  50 |     fromFFI ns = fromUnion2 ns >>= appFromFFI npp
  51 | 
  52 | export
  53 | FromFFI (Union2 a b) (Union2 a b) where
  54 |   fromFFI = Just
  55 | 
  56 | export
  57 | ToFFI (Union2 a b) (Union2 a b) where
  58 |   toFFI = id
  59 | 
  60 | --------------------------------------------------------------------------------
  61 | --          Union3
  62 | --------------------------------------------------------------------------------
  63 | 
  64 | export
  65 | data Union3 : Type -> Type -> Type -> Type where [external]
  66 | 
  67 | export
  68 | toUnion3 : HSum [a,b,c] -> Union3 a b c
  69 | toUnion3 = collapse' . hmap believe_me
  70 | 
  71 | export
  72 | fromUnion3 : All SafeCast [a,b,c] => Union3 a b c -> Maybe $ HSum [a,b,c]
  73 | fromUnion3 = safeCastAny
  74 | 
  75 | export
  76 | (npp : NPP ToFFI [a,b,c] [m,n,o]) =>
  77 |   ToFFI (HSum [a,b,c]) (Union3 m n o) where
  78 |     toFFI ns = toUnion3 $ appToFFI npp ns
  79 | 
  80 | export
  81 | (npp : NPP FromFFI [a,b,c] [m,n,o]) => All SafeCast [m,n,o] =>
  82 |   FromFFI (HSum [a,b,c]) (Union3 m n o) where
  83 |     fromFFI ns = fromUnion3 ns >>= appFromFFI npp
  84 | 
  85 | export
  86 | FromFFI (Union3 a b c) (Union3 a b c) where
  87 |   fromFFI = Just
  88 | 
  89 | export
  90 | ToFFI (Union3 a b c) (Union3 a b c) where
  91 |   toFFI = id
  92 | 
  93 | --------------------------------------------------------------------------------
  94 | --          Union4
  95 | --------------------------------------------------------------------------------
  96 | 
  97 | export
  98 | data Union4 : Type -> Type -> Type -> Type -> Type where [external]
  99 | 
 100 | export
 101 | toUnion4 : HSum [a,b,c,d] -> Union4 a b c d
 102 | toUnion4 = collapse' . hmap believe_me
 103 | 
 104 | export
 105 | fromUnion4 : All SafeCast [a,b,c,d] => Union4 a b c d -> Maybe $ HSum [a,b,c,d]
 106 | fromUnion4 = safeCastAny
 107 | 
 108 | export
 109 | (npp : NPP ToFFI [a,b,c,d] [m,n,o,p]) =>
 110 |   ToFFI (HSum [a,b,c,d]) (Union4 m n o p) where
 111 |     toFFI ns = toUnion4 $ appToFFI npp ns
 112 | 
 113 | export
 114 | (npp : NPP FromFFI [a,b,c,d] [m,n,o,p]) => All SafeCast [m,n,o,p] =>
 115 |   FromFFI (HSum [a,b,c,d]) (Union4 m n o p) where
 116 |     fromFFI ns = fromUnion4 ns >>= appFromFFI npp
 117 | 
 118 | export
 119 | FromFFI (Union4 a b c d) (Union4 a b c d) where
 120 |   fromFFI = Just
 121 | 
 122 | export
 123 | ToFFI (Union4 a b c d) (Union4 a b c d) where
 124 |   toFFI = id
 125 | 
 126 | --------------------------------------------------------------------------------
 127 | --          Union5
 128 | --------------------------------------------------------------------------------
 129 | 
 130 | export
 131 | data Union5 : Type -> Type -> Type -> Type -> Type -> Type where [external]
 132 | 
 133 | export
 134 | toUnion5 : HSum [a,b,c,d,e] -> Union5 a b c d e
 135 | toUnion5 = collapse' . hmap believe_me
 136 | 
 137 | export
 138 | fromUnion5 : All SafeCast [a,b,c,d,e] =>
 139 |              Union5 a b c d e -> Maybe $ HSum [a,b,c,d,e]
 140 | fromUnion5 = safeCastAny
 141 | 
 142 | export
 143 | (npp : NPP ToFFI [a,b,c,d,e] [m,n,o,p,q]) =>
 144 |   ToFFI (HSum [a,b,c,d,e]) (Union5 m n o p q) where
 145 |     toFFI ns = toUnion5 $ appToFFI npp ns
 146 | 
 147 | export
 148 | (npp : NPP FromFFI [a,b,c,d,e] [m,n,o,p,r]) => All SafeCast [m,n,o,p,r] =>
 149 |   FromFFI (HSum [a,b,c,d,e]) (Union5 m n o p r) where
 150 |     fromFFI ns = fromUnion5 ns >>= appFromFFI npp
 151 | 
 152 | export
 153 | FromFFI (Union5 a b c d e) (Union5 a b c d e) where
 154 |   fromFFI = Just
 155 | 
 156 | export
 157 | ToFFI (Union5 a b c d e) (Union5 a b c d e) where
 158 |   toFFI = id
 159 | 
 160 | --------------------------------------------------------------------------------
 161 | --          Union6
 162 | --------------------------------------------------------------------------------
 163 | 
 164 | export
 165 | data Union6 : Type -> Type -> Type -> Type -> Type -> Type -> Type where [external]
 166 | 
 167 | export
 168 | toUnion6 : HSum [a,b,c,d,e,f] -> Union6 a b c d e f
 169 | toUnion6 = collapse' . hmap believe_me
 170 | 
 171 | export
 172 | fromUnion6 : All SafeCast [a,b,c,d,e,f] =>
 173 |              Union6 a b c d e f -> Maybe $ HSum [a,b,c,d,e,f]
 174 | fromUnion6 = safeCastAny
 175 | 
 176 | export
 177 | (npp : NPP ToFFI [a,b,c,d,e,f] [m,n,o,p,q,r]) =>
 178 |   ToFFI (HSum [a,b,c,d,e,f]) (Union6 m n o p q r) where
 179 |     toFFI ns = toUnion6 $ appToFFI npp ns
 180 | 
 181 | export
 182 | (npp : NPP FromFFI [a,b,c,d,e,f] [m,n,o,p,r,s]) =>
 183 | All SafeCast [m,n,o,p,r,s] =>
 184 |   FromFFI (HSum [a,b,c,d,e,f]) (Union6 m n o p r s) where
 185 |     fromFFI ns = fromUnion6 ns >>= appFromFFI npp
 186 | 
 187 | export
 188 | FromFFI (Union6 a b c d e f) (Union6 a b c d e f) where
 189 |   fromFFI = Just
 190 | 
 191 | export
 192 | ToFFI (Union6 a b c d e f) (Union6 a b c d e f) where
 193 |   toFFI = id
 194 | 
 195 | --------------------------------------------------------------------------------
 196 | --          Union7
 197 | --------------------------------------------------------------------------------
 198 | 
 199 | export
 200 | data Union7 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where [external]
 201 | 
 202 | export
 203 | toUnion7 : HSum [a,b,c,d,e,f,g] -> Union7 a b c d e f g
 204 | toUnion7 = collapse' . hmap believe_me
 205 | 
 206 | export
 207 | fromUnion7 : All SafeCast [a,b,c,d,e,f,g] =>
 208 |              Union7 a b c d e f g -> Maybe $ HSum [a,b,c,d,e,f,g]
 209 | fromUnion7 = safeCastAny
 210 | 
 211 | export
 212 | (npp : NPP ToFFI [a,b,c,d,e,f,g] [m,n,o,p,q,r,s]) =>
 213 |   ToFFI (HSum [a,b,c,d,e,f,g]) (Union7 m n o p q r s) where
 214 |     toFFI ns = toUnion7 $ appToFFI npp ns
 215 | 
 216 | export
 217 | (npp : NPP FromFFI [a,b,c,d,e,f,g] [m,n,o,p,r,s,t]) =>
 218 | All SafeCast [m,n,o,p,r,s,t] =>
 219 |   FromFFI (HSum [a,b,c,d,e,f,g]) (Union7 m n o p r s t) where
 220 |     fromFFI ns = fromUnion7 ns >>= appFromFFI npp
 221 | 
 222 | export
 223 | FromFFI (Union7 a b c d e f g) (Union7 a b c d e f g) where
 224 |   fromFFI = Just
 225 | 
 226 | export
 227 | ToFFI (Union7 a b c d e f g) (Union7 a b c d e f g) where
 228 |   toFFI = id
 229 | 
 230 | --------------------------------------------------------------------------------
 231 | --          Union8
 232 | --------------------------------------------------------------------------------
 233 | 
 234 | export
 235 | data Union8 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where [external]
 236 | 
 237 | export
 238 | toUnion8 : HSum [a,b,c,d,e,f,g,h] -> Union8 a b c d e f g h
 239 | toUnion8 = collapse' . hmap believe_me
 240 | 
 241 | export
 242 | fromUnion8 : All SafeCast [a,b,c,d,e,f,g,h] =>
 243 |              Union8 a b c d e f g h -> Maybe $ HSum [a,b,c,d,e,f,g,h]
 244 | fromUnion8 = safeCastAny
 245 | 
 246 | export
 247 | (npp : NPP ToFFI [a,b,c,d,e,f,g,h] [m,n,o,p,q,r,s,t]) =>
 248 |   ToFFI (HSum [a,b,c,d,e,f,g,h]) (Union8 m n o p q r s t) where
 249 |     toFFI ns = toUnion8 $ appToFFI npp ns
 250 | 
 251 | export
 252 | (npp : NPP FromFFI [a,b,c,d,e,f,g,h] [m,n,o,p,r,s,t,u]) =>
 253 | All SafeCast [m,n,o,p,r,s,t,u] =>
 254 |   FromFFI (HSum [a,b,c,d,e,f,g,h]) (Union8 m n o p r s t u) where
 255 |     fromFFI ns = fromUnion8 ns >>= appFromFFI npp
 256 | 
 257 | export
 258 | FromFFI (Union8 a b c d e f g h) (Union8 a b c d e f g h) where
 259 |   fromFFI = Just
 260 | 
 261 | export
 262 | ToFFI (Union8 a b c d e f g h) (Union8 a b c d e f g h) where
 263 |   toFFI = id
 264 | 
 265 | --------------------------------------------------------------------------------
 266 | --          Union9
 267 | --------------------------------------------------------------------------------
 268 | 
 269 | export
 270 | data Union9 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where [external]
 271 | 
 272 | export
 273 | toUnion9 : HSum [a,b,c,d,e,f,g,h,i] -> Union9 a b c d e f g h i
 274 | toUnion9 = collapse' . hmap believe_me
 275 | 
 276 | export
 277 | fromUnion9 : All SafeCast [a,b,c,d,e,f,g,h,i] =>
 278 |              Union9 a b c d e f g h i -> Maybe $ HSum [a,b,c,d,e,f,g,h,i]
 279 | fromUnion9 = safeCastAny
 280 | 
 281 | export
 282 | (npp : NPP ToFFI [a,b,c,d,e,f,g,h,i] [m,n,o,p,q,r,s,t,u]) =>
 283 |   ToFFI (HSum [a,b,c,d,e,f,g,h,i]) (Union9 m n o p q r s t u) where
 284 |     toFFI ns = toUnion9 $ appToFFI npp ns
 285 | 
 286 | export
 287 | (npp : NPP FromFFI [a,b,c,d,e,f,g,h,i] [m,n,o,p,r,s,t,u,v]) =>
 288 | All SafeCast [m,n,o,p,r,s,t,u,v] =>
 289 |   FromFFI (HSum [a,b,c,d,e,f,g,h,i]) (Union9 m n o p r s t u v) where
 290 |     fromFFI ns = fromUnion9 ns >>= appFromFFI npp
 291 | 
 292 | export
 293 | FromFFI (Union9 a b c d e f g h i) (Union9 a b c d e f g h i) where
 294 |   fromFFI = Just
 295 | 
 296 | export
 297 | ToFFI (Union9 a b c d e f g h i) (Union9 a b c d e f g h i) where
 298 |   toFFI = id
 299 | 
 300 | --------------------------------------------------------------------------------
 301 | --          Union10
 302 | --------------------------------------------------------------------------------
 303 | 
 304 | export
 305 | data Union10 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where [external]
 306 | 
 307 | export
 308 | toUnion10 : HSum [a,b,c,d,e,f,g,h,i,j] -> Union10 a b c d e f g h i j
 309 | toUnion10 = collapse' . hmap believe_me
 310 | 
 311 | export
 312 | fromUnion10 : All SafeCast [a,b,c,d,e,f,g,h,i,j] =>
 313 |              Union10 a b c d e f g h i j -> Maybe $ HSum [a,b,c,d,e,f,g,h,i,j]
 314 | fromUnion10 = safeCastAny
 315 | 
 316 | export
 317 | (npp : NPP ToFFI [a,b,c,d,e,f,g,h,i,j] [m,n,o,p,q,r,s,t,u,v]) =>
 318 |   ToFFI (HSum [a,b,c,d,e,f,g,h,i,j]) (Union10 m n o p q r s t u v) where
 319 |     toFFI ns = toUnion10 $ appToFFI npp ns
 320 | 
 321 | export
 322 | (npp : NPP FromFFI [a,b,c,d,e,f,g,h,i,j] [m,n,o,p,r,s,t,u,v,w]) =>
 323 | All SafeCast [m,n,o,p,r,s,t,u,v,w] =>
 324 |   FromFFI (HSum [a,b,c,d,e,f,g,h,i,j]) (Union10 m n o p r s t u v w) where
 325 |     fromFFI ns = fromUnion10 ns >>= appFromFFI npp
 326 | 
 327 | export
 328 | FromFFI (Union10 a b c d e f g h i j) (Union10 a b c d e f g h i j) where
 329 |   fromFFI = Just
 330 | 
 331 | export
 332 | ToFFI (Union10 a b c d e f g h i j) (Union10 a b c d e f g h i j) where
 333 |   toFFI = id
 334 | 
 335 | --------------------------------------------------------------------------------
 336 | --          Union11
 337 | --------------------------------------------------------------------------------
 338 | 
 339 | export
 340 | data Union11 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where [external]
 341 | 
 342 | export
 343 | toUnion11 : HSum [a,b,c,d,e,f,g,h,i,j,k] -> Union11 a b c d e f g h i j k
 344 | toUnion11 = collapse' . hmap believe_me
 345 | 
 346 | export
 347 | fromUnion11 : All SafeCast [a,b,c,d,e,f,g,h,i,j,k] =>
 348 |              Union11 a b c d e f g h i j k -> Maybe $ HSum [a,b,c,d,e,f,g,h,i,j,k]
 349 | fromUnion11 = safeCastAny
 350 | 
 351 | export
 352 | (npp : NPP ToFFI [a,b,c,d,e,f,g,h,i,j,k] [m,n,o,p,q,r,s,t,u,v,w]) =>
 353 |   ToFFI (HSum [a,b,c,d,e,f,g,h,i,j,k]) (Union11 m n o p q r s t u v w) where
 354 |     toFFI ns = toUnion11 $ appToFFI npp ns
 355 | 
 356 | export
 357 | (npp : NPP FromFFI [a,b,c,d,e,f,g,h,i,j,k] [m,n,o,p,q,r,s,t,u,v,w]) =>
 358 | All SafeCast [m,n,o,p,q,r,s,t,u,v,w] =>
 359 |   FromFFI (HSum [a,b,c,d,e,f,g,h,i,j,k]) (Union11 m n o p q r s t u v w) where
 360 |     fromFFI ns = fromUnion11 ns >>= appFromFFI npp
 361 | 
 362 | export
 363 | FromFFI (Union11 a b c d e f g h i j k) (Union11 a b c d e f g h i j k) where
 364 |   fromFFI = Just
 365 | 
 366 | export
 367 | ToFFI (Union11 a b c d e f g h i j k) (Union11 a b c d e f g h i j k) where
 368 |   toFFI = id
 369 | 
 370 | --------------------------------------------------------------------------------
 371 | --          Union12
 372 | --------------------------------------------------------------------------------
 373 | 
 374 | export
 375 | data Union12 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where [external]
 376 | 
 377 | export
 378 | toUnion12 : HSum [a,b,c,d,e,f,g,h,i,j,k,l] -> Union12 a b c d e f g h i j k l
 379 | toUnion12 = collapse' . hmap believe_me
 380 | 
 381 | export
 382 | fromUnion12 : All SafeCast [a,b,c,d,e,f,g,h,i,j,k,l] =>
 383 |              Union12 a b c d e f g h i j k l -> Maybe $ HSum [a,b,c,d,e,f,g,h,i,j,k,l]
 384 | fromUnion12 = safeCastAny
 385 | 
 386 | export
 387 | (npp : NPP ToFFI [a,b,c,d,e,f,g,h,i,j,k,l] [m,n,o,p,q,r,s,t,u,v,w,x]) =>
 388 |   ToFFI (HSum [a,b,c,d,e,f,g,h,i,j,k,l]) (Union12 m n o p q r s t u v w x) where
 389 |     toFFI ns = toUnion12 $ appToFFI npp ns
 390 | 
 391 | export
 392 | (npp : NPP FromFFI [a,b,c,d,e,f,g,h,i,j,k,l] [m,n,o,p,q,r,s,t,u,v,w,x]) =>
 393 | All SafeCast [m,n,o,p,q,r,s,t,u,v,w,x] =>
 394 |   FromFFI (HSum [a,b,c,d,e,f,g,h,i,j,k,l]) (Union12 m n o p q r s t u v w x) where
 395 |     fromFFI ns = fromUnion12 ns >>= appFromFFI npp
 396 | 
 397 | export
 398 | FromFFI (Union12 a b c d e f g h i j k l) (Union12 a b c d e f g h i j k l) where
 399 |   fromFFI = Just
 400 | 
 401 | export
 402 | ToFFI (Union12 a b c d e f g h i j k l) (Union12 a b c d e f g h i j k l) where
 403 |   toFFI = id
 404 | 
 405 | --------------------------------------------------------------------------------
 406 | --          Union13
 407 | --------------------------------------------------------------------------------
 408 | 
 409 | export
 410 | data Union13 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where [external]
 411 | 
 412 | export
 413 | toUnion13 : HSum [a,b,c,d,e,f,g,h,i,j,k,l,a1] -> Union13 a b c d e f g h i j k l a1
 414 | toUnion13 = collapse' . hmap believe_me
 415 | 
 416 | export
 417 | fromUnion13 : All SafeCast [a,b,c,d,e,f,g,h,i,j,k,l,a1] =>
 418 |              Union13 a b c d e f g h i j k l a1 -> Maybe $ HSum [a,b,c,d,e,f,g,h,i,j,k,l,a1]
 419 | fromUnion13 = safeCastAny
 420 | 
 421 | export
 422 | (npp : NPP ToFFI [a,b,c,d,e,f,g,h,i,j,k,l,a1] [m,n,o,p,q,r,s,t,u,v,w,x,y]) =>
 423 |   ToFFI (HSum [a,b,c,d,e,f,g,h,i,j,k,l,a1]) (Union13 m n o p q r s t u v w x y) where
 424 |     toFFI ns = toUnion13 $ appToFFI npp ns
 425 | 
 426 | export
 427 | (npp : NPP FromFFI [a,b,c,d,e,f,g,h,i,j,k,l,a1] [m,n,o,p,q,r,s,t,u,v,w,x,y]) =>
 428 | All SafeCast [m,n,o,p,q,r,s,t,u,v,w,x,y] =>
 429 |   FromFFI (HSum [a,b,c,d,e,f,g,h,i,j,k,l,a1]) (Union13 m n o p q r s t u v w x y) where
 430 |     fromFFI ns = fromUnion13 ns >>= appFromFFI npp
 431 | 
 432 | export
 433 | FromFFI (Union13 a b c d e f g h i j k l m) (Union13 a b c d e f g h i j k l m) where
 434 |   fromFFI = Just
 435 | 
 436 | export
 437 | ToFFI (Union13 a b c d e f g h i j k l m) (Union13 a b c d e f g h i j k l m) where
 438 |   toFFI = id
 439 | 
 440 | --------------------------------------------------------------------------------
 441 | --          Union14
 442 | --------------------------------------------------------------------------------
 443 | 
 444 | export
 445 | data Union14 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where [external]
 446 | 
 447 | export
 448 | toUnion14 : HSum [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2] -> Union14 a b c d e f g h i j k l a1 a2
 449 | toUnion14 = collapse' . hmap believe_me
 450 | 
 451 | export
 452 | fromUnion14 : All SafeCast [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2] =>
 453 |              Union14 a b c d e f g h i j k l a1 a2 -> Maybe $ HSum [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2]
 454 | fromUnion14 = safeCastAny
 455 | 
 456 | export
 457 | (npp : NPP ToFFI [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2] [m,n,o,p,q,r,s,t,u,v,w,x,y,z]) =>
 458 |   ToFFI (HSum [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2]) (Union14 m n o p q r s t u v w x y z) where
 459 |     toFFI ns = toUnion14 $ appToFFI npp ns
 460 | 
 461 | export
 462 | (npp : NPP FromFFI [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2] [m,n,o,p,q,r,s,t,u,v,w,x,y,z]) =>
 463 | All SafeCast [m,n,o,p,q,r,s,t,u,v,w,x,y,z] =>
 464 |   FromFFI (HSum [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2]) (Union14 m n o p q r s t u v w x y z) where
 465 |     fromFFI ns = fromUnion14 ns >>= appFromFFI npp
 466 | 
 467 | export
 468 | FromFFI (Union14 a b c d e f g h i j k l m n) (Union14 a b c d e f g h i j k l m n) where
 469 |   fromFFI = Just
 470 | 
 471 | export
 472 | ToFFI (Union14 a b c d e f g h i j k l m n) (Union14 a b c d e f g h i j k l m n) where
 473 |   toFFI = id
 474 | 
 475 | --------------------------------------------------------------------------------
 476 | --          Union15
 477 | --------------------------------------------------------------------------------
 478 | 
 479 | export
 480 | data Union15 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where [external]
 481 | 
 482 | export
 483 | toUnion15 : HSum [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3] -> Union15 a b c d e f g h i j k l a1 a2 a3
 484 | toUnion15 = collapse' . hmap believe_me
 485 | 
 486 | export
 487 | fromUnion15 : All SafeCast [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3] =>
 488 |              Union15 a b c d e f g h i j k l a1 a2 a3 -> Maybe $ HSum [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3]
 489 | fromUnion15 = safeCastAny
 490 | 
 491 | export
 492 | (npp : NPP ToFFI [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3] [m,n,o,p,q,r,s,t,u,v,w,x,y,z,z1]) =>
 493 |   ToFFI (HSum [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3]) (Union15 m n o p q r s t u v w x y z z1) where
 494 |     toFFI ns = toUnion15 $ appToFFI npp ns
 495 | 
 496 | export
 497 | (npp : NPP FromFFI [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3] [m,n,o,p,q,r,s,t,u,v,w,x,y,z,z1]) =>
 498 | All SafeCast [m,n,o,p,q,r,s,t,u,v,w,x,y,z,z1] =>
 499 |   FromFFI (HSum [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3]) (Union15 m n o p q r s t u v w x y z z1) where
 500 |     fromFFI ns = fromUnion15 ns >>= appFromFFI npp
 501 | 
 502 | export
 503 | FromFFI (Union15 a b c d e f g h i j k l m n o) (Union15 a b c d e f g h i j k l m n o) where
 504 |   fromFFI = Just
 505 | 
 506 | export
 507 | ToFFI (Union15 a b c d e f g h i j k l m n o) (Union15 a b c d e f g h i j k l m n o) where
 508 |   toFFI = id
 509 | 
 510 | --------------------------------------------------------------------------------
 511 | --          Union16
 512 | --------------------------------------------------------------------------------
 513 | 
 514 | export
 515 | data Union16 : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type where [external]
 516 | 
 517 | export
 518 | toUnion16 : HSum [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3,a4] -> Union16 a b c d e f g h i j k l a1 a2 a3 a4
 519 | toUnion16 = collapse' . hmap believe_me
 520 | 
 521 | export
 522 | fromUnion16 : All SafeCast [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3,a4] =>
 523 |              Union16 a b c d e f g h i j k l a1 a2 a3 a4 -> Maybe $ HSum [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3,a4]
 524 | fromUnion16 = safeCastAny
 525 | 
 526 | export
 527 | (npp : NPP ToFFI [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3,a4] [m,n,o,p,q,r,s,t,u,v,w,x,y,z,z1,z2]) =>
 528 |   ToFFI (HSum [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3,a4]) (Union16 m n o p q r s t u v w x y z z1 z2) where
 529 |     toFFI ns = toUnion16 $ appToFFI npp ns
 530 | 
 531 | export
 532 | (npp : NPP FromFFI [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3,a4] [m,n,o,p,q,r,s,t,u,v,w,x,y,z,z1,z2]) =>
 533 | All SafeCast [m,n,o,p,q,r,s,t,u,v,w,x,y,z,z1,z2] =>
 534 |   FromFFI (HSum [a,b,c,d,e,f,g,h,i,j,k,l,a1,a2,a3,a4]) (Union16 m n o p q r s t u v w x y z z1 z2) where
 535 |     fromFFI ns = fromUnion16 ns >>= appFromFFI npp
 536 | 
 537 | export
 538 | FromFFI (Union16 a b c d e f g h i j k l m n o p) (Union16 a b c d e f g h i j k l m n o p) where
 539 |   fromFFI = Just
 540 | 
 541 | export
 542 | ToFFI (Union16 a b c d e f g h i j k l m n o p) (Union16 a b c d e f g h i j k l m n o p) where
 543 |   toFFI = id
 544 |