WIP half-peano SNatspeano-snat

1 files changed, 67 insertions, 62 deletions

diff --git a/src/Data/Array/Mixed/Internal/Arith.hs b/src/Data/Array/Mixed/Internal/Arith.hs
index a24efd6..dd4d8e7 100644
--- a/src/Data/Array/Mixed/Internal/Arith.hs
+++ b/src/Data/Array/Mixed/Internal/Arith.hs
@@ -24,14 +24,13 @@ import Foreign.C.Types
 import Foreign.Marshal.Alloc (alloca)
 import Foreign.Ptr
 import Foreign.Storable (Storable(sizeOf), peek, poke)
-import GHC.TypeLits
 import GHC.TypeNats qualified as TypeNats
 import Language.Haskell.TH
 import System.IO.Unsafe
 
+import Data.SNat.Peano
 import Data.Array.Mixed.Internal.Arith.Foreign
 import Data.Array.Mixed.Internal.Arith.Lists
-import Data.Array.Mixed.Types (fromSNat')
 
 
 -- TODO: need to sort strides for reduction-like functions so that the C inner-loop specialisation has some chance of working even after transposition
@@ -41,8 +40,8 @@ import Data.Array.Mixed.Types (fromSNat')
 liftVEltwise1 :: (Storable a, Storable b)
               => SNat n
               -> (VS.Vector a -> VS.Vector b)
-              -> RS.Array n a -> RS.Array n b
-liftVEltwise1 SNat f arr@(RS.A (RG.A sh (OI.T strides offset vec)))
+              -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) b
+liftVEltwise1 SNat' f arr@(RS.A (RG.A sh (OI.T strides offset vec)))
   | Just (blockOff, blockSz) <- stridesDense sh offset strides =
       let vec' = f (VS.slice blockOff blockSz vec)
       in RS.A (RG.A sh (OI.T strides (offset - blockOff) vec'))
@@ -52,8 +51,8 @@ liftVEltwise1 SNat f arr@(RS.A (RG.A sh (OI.T strides offset vec)))
 liftVEltwise2 :: (Storable a, Storable b, Storable c)
               => SNat n
               -> (Either a (VS.Vector a) -> Either b (VS.Vector b) -> VS.Vector c)
-              -> RS.Array n a -> RS.Array n b -> RS.Array n c
-liftVEltwise2 SNat f
+              -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) b -> RS.Array (GHCFromNat n) c
+liftVEltwise2 SNat' f
     arr1@(RS.A (RG.A sh1 (OI.T strides1 offset1 vec1)))
     arr2@(RS.A (RG.A sh2 (OI.T strides2 offset2 vec2)))
   | sh1 /= sh2 = error $ "liftVEltwise2: shapes unequal: " ++ show sh1 ++ " vs " ++ show sh2
@@ -172,8 +171,8 @@ vectorRedInnerOp :: forall a b n. (Num a, Storable a)
                  -> (Ptr a -> Ptr b)
                  -> (Int64 -> Ptr b -> b -> Ptr b -> IO ())  -- ^ scale by constant
                  -> (Int64 -> Ptr b -> Ptr Int64 -> Ptr Int64 -> Ptr b -> IO ())  -- ^ reduction kernel
-                 -> RS.Array (n + 1) a -> RS.Array n a
-vectorRedInnerOp sn@SNat valconv ptrconv fscale fred (RS.A (RG.A sh (OI.T strides offset vec)))
+                 -> RS.Array (GHCFromNat (S n)) a -> RS.Array (GHCFromNat n) a
+vectorRedInnerOp sn@SNat' valconv ptrconv fscale fred (RS.A (RG.A sh (OI.T strides offset vec)))
   | null sh = error "unreachable"
   | last sh <= 0 = RS.stretch (init sh) (RS.fromList (1 <$ init sh) [0])
   | any (<= 0) (init sh) = RS.A (RG.A (init sh) (OI.T (0 <$ init strides) 0 VS.empty))
@@ -210,7 +209,7 @@ vectorRedInnerOp sn@SNat valconv ptrconv fscale fred (RS.A (RG.A sh (OI.T stride
                VS.unsafeWith (VS.fromListN ndimsF (map fromIntegral stridesR)) $ \pstridesR ->
                  VS.unsafeWith (VS.slice offsetR (VS.length vec - offsetR) vec) $ \pvecR ->
                    fred (fromIntegral ndimsF) (ptrconv poutvR) pshF pstridesR (ptrconv pvecR)
-           TypeNats.withSomeSNat (fromIntegral (ndimsF - 1)) $ \(SNat :: SNat lenFm1) ->
+           TypeNats.withSomeSNat (fromIntegral (ndimsF - 1)) $ \(TypeNats.SNat :: TypeNats.SNat lenFm1) ->
              RS.stretch (init sh)  -- replicate to original shape
                . RS.reshape (init shOnes)  -- add 1-sized dimensions where the original was replicated
                . RS.rev (map fst (filter snd (zip [0..] revDims)))  -- re-reverse the correct dimensions
@@ -226,7 +225,7 @@ vectorRedFullOp :: forall a b n. (Num a, Storable a)
                 -> (b -> a)
                 -> (Ptr a -> Ptr b)
                 -> (Int64 -> Ptr Int64 -> Ptr Int64 -> Ptr b -> IO b)  -- ^ reduction kernel
-                -> RS.Array n a -> a
+                -> RS.Array (GHCFromNat n) a -> a
 vectorRedFullOp _ scaleval valbackconv ptrconv fred (RS.A (RG.A sh (OI.T strides offset vec)))
   | null sh = vec VS.! offset  -- 0D array has one element
   | any (<= 0) sh = 0
@@ -309,12 +308,12 @@ vectorDotprodInnerOp :: forall a b n. (Num a, Storable a)
                      => SNat n
                      -> (a -> b)
                      -> (Ptr a -> Ptr b)
-                     -> (SNat n -> RS.Array n a -> RS.Array n a -> RS.Array n a)  -- ^ elementwise multiplication
+                     -> (SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a)  -- ^ elementwise multiplication
                      -> (Int64 -> Ptr b -> b -> Ptr b -> IO ())  -- ^ scale by constant
                      -> (Int64 -> Ptr b -> Ptr Int64 -> Ptr Int64 -> Ptr b -> IO ())  -- ^ reduction kernel
                      -> (Int64 -> Ptr Int64 -> Ptr b -> Ptr Int64 -> Ptr b -> Ptr Int64 -> Ptr b -> IO ())  -- ^ dotprod kernel
-                     -> RS.Array (n + 1) a -> RS.Array (n + 1) a -> RS.Array n a
-vectorDotprodInnerOp sn@SNat valconv ptrconv fmul fscale fred fdotinner
+                     -> RS.Array (GHCFromNat (S n)) a -> RS.Array (GHCFromNat (S n)) a -> RS.Array (GHCFromNat n) a
+vectorDotprodInnerOp sn@SNat' valconv ptrconv fmul fscale fred fdotinner
     arr1@(RS.A (RG.A sh1 (OI.T strides1 offset1 vec1)))
     arr2@(RS.A (RG.A sh2 (OI.T strides2 offset2 vec2)))
   | null sh1 || null sh2 = error "unreachable"
@@ -344,7 +343,7 @@ vectorDotprodInnerOp sn@SNat valconv ptrconv fmul fscale fred fdotinner
           fdotinner (fromIntegral @Int @Int64 inrank) psh (ptrconv poutv)
                     pstrides1 (ptrconv pvec1 `plusPtr` (sizeOf (undefined :: a) * offset1))
                     pstrides2 (ptrconv pvec2 `plusPtr` (sizeOf (undefined :: a) * offset2))
-      RS.fromVector @_ @n (init sh1) <$> VS.unsafeFreeze outv
+      RS.fromVector @_ @(GHCFromNat n) (init sh1) <$> VS.unsafeFreeze outv
 
 {-# NOINLINE dotScalarVector #-}
 dotScalarVector :: forall a b. (Num a, Storable a)
@@ -398,7 +397,10 @@ $(fmap concat . forM typesList $ \arithtype -> do
           c_vs = varE (mkName (cnamebase ++ "_vs")) `appE` litE (integerL (fromIntegral (aboEnum arithop)))
           c_vv = varE (mkName (cnamebase ++ "_vv")) `appE` litE (integerL (fromIntegral (aboEnum arithop)))
       sequence [SigD name <$>
-                     [t| forall n. SNat n -> RS.Array n $ttyp -> RS.Array n $ttyp -> RS.Array n $ttyp |]
+                     [t| forall n. SNat n
+                                -> RS.Array (GHCFromNat n) $ttyp
+                                -> RS.Array (GHCFromNat n) $ttyp
+                                -> RS.Array (GHCFromNat n) $ttyp |]
                ,do body <- [| \sn -> liftVEltwise2 sn (vectorOp2 id id $c_ss $c_sv $c_vs $c_vv) |]
                    return $ FunD name [Clause [] (NormalB body) []]])
 
@@ -412,7 +414,10 @@ $(fmap concat . forM floatTypesList $ \arithtype -> do
           c_vs = varE (mkName (cnamebase ++ "_vs")) `appE` litE (integerL (fromIntegral (afboEnum arithop)))
           c_vv = varE (mkName (cnamebase ++ "_vv")) `appE` litE (integerL (fromIntegral (afboEnum arithop)))
       sequence [SigD name <$>
-                     [t| forall n. SNat n -> RS.Array n $ttyp -> RS.Array n $ttyp -> RS.Array n $ttyp |]
+                     [t| forall n. SNat n
+                                -> RS.Array (GHCFromNat n) $ttyp
+                                -> RS.Array (GHCFromNat n) $ttyp
+                                -> RS.Array (GHCFromNat n) $ttyp |]
                ,do body <- [| \sn -> liftVEltwise2 sn (vectorOp2 id id $c_ss $c_sv $c_vs $c_vv) |]
                    return $ FunD name [Clause [] (NormalB body) []]])
 
@@ -422,7 +427,7 @@ $(fmap concat . forM typesList $ \arithtype -> do
       let name = mkName (auoName arithop ++ "Vector" ++ nameBase (atType arithtype))
           c_op = varE (mkName ("c_unary_" ++ atCName arithtype)) `appE` litE (integerL (fromIntegral (auoEnum arithop)))
       sequence [SigD name <$>
-                     [t| forall n. SNat n -> RS.Array n $ttyp -> RS.Array n $ttyp |]
+                     [t| forall n. SNat n -> RS.Array (GHCFromNat n) $ttyp -> RS.Array (GHCFromNat n) $ttyp |]
                ,do body <- [| \sn -> liftVEltwise1 sn (vectorOp1 id $c_op) |]
                    return $ FunD name [Clause [] (NormalB body) []]])
 
@@ -432,7 +437,7 @@ $(fmap concat . forM floatTypesList $ \arithtype -> do
       let name = mkName (afuoName arithop ++ "Vector" ++ nameBase (atType arithtype))
           c_op = varE (mkName ("c_funary_" ++ atCName arithtype)) `appE` litE (integerL (fromIntegral (afuoEnum arithop)))
       sequence [SigD name <$>
-                     [t| forall n. SNat n -> RS.Array n $ttyp -> RS.Array n $ttyp |]
+                     [t| forall n. SNat n -> RS.Array (GHCFromNat n) $ttyp -> RS.Array (GHCFromNat n) $ttyp |]
                ,do body <- [| \sn -> liftVEltwise1 sn (vectorOp1 id $c_op) |]
                    return $ FunD name [Clause [] (NormalB body) []]])
 
@@ -451,11 +456,11 @@ $(fmap concat . forM typesList $ \arithtype -> do
           c_opfull = varE (mkName ("c_reducefull_" ++ atCName arithtype)) `appE` litE (integerL (fromIntegral (aroEnum arithop)))
           c_scale_op = varE (mkName ("c_binary_" ++ atCName arithtype ++ "_sv")) `appE` litE (integerL (fromIntegral (aboEnum BO_MUL)))
       sequence [SigD name1 <$>
-                     [t| forall n. SNat n -> RS.Array (n + 1) $ttyp -> RS.Array n $ttyp |]
+                     [t| forall n. SNat n -> RS.Array (GHCFromNat (S n)) $ttyp -> RS.Array (GHCFromNat n) $ttyp |]
                ,do body <- [| \sn -> vectorRedInnerOp sn id id $c_scale_op $c_op1 |]
                    return $ FunD name1 [Clause [] (NormalB body) []]
                ,SigD namefull <$>
-                     [t| forall n. SNat n -> RS.Array n $ttyp -> $ttyp |]
+                     [t| forall n. SNat n -> RS.Array (GHCFromNat n) $ttyp -> $ttyp |]
                ,do body <- [| \sn -> vectorRedFullOp sn $scaleVar id id $c_opfull |]
                    return $ FunD namefull [Clause [] (NormalB body) []]
                ])
@@ -478,7 +483,7 @@ $(fmap concat . forM typesList $ \arithtype -> do
         c_scale_op = varE (mkName ("c_binary_" ++ atCName arithtype ++ "_sv")) `appE` litE (integerL (fromIntegral (aboEnum BO_MUL)))
         c_red_op = varE (mkName ("c_reduce1_" ++ atCName arithtype)) `appE` litE (integerL (fromIntegral (aroEnum RO_SUM)))
     sequence [SigD name <$>
-                   [t| forall n. SNat n -> RS.Array (n + 1) $ttyp -> RS.Array (n + 1) $ttyp -> RS.Array n $ttyp |]
+                   [t| forall n. SNat n -> RS.Array (GHCFromNat (S n)) $ttyp -> RS.Array (GHCFromNat (S n)) $ttyp -> RS.Array (GHCFromNat n) $ttyp |]
              ,do body <- [| \sn -> vectorDotprodInnerOp sn id id $mul_op $c_scale_op $c_red_op $c_op |]
                  return $ FunD name [Clause [] (NormalB body) []]])
 
@@ -487,7 +492,7 @@ $(fmap concat . forM typesList $ \arithtype -> do
 intWidBranch1 :: forall i n. (FiniteBits i, Storable i)
               => (Int64 -> Ptr Int32 -> Ptr Int32 -> IO ())
               -> (Int64 -> Ptr Int64 -> Ptr Int64 -> IO ())
-              -> (SNat n -> RS.Array n i -> RS.Array n i)
+              -> (SNat n -> RS.Array (GHCFromNat n) i -> RS.Array (GHCFromNat n) i)
 intWidBranch1 f32 f64 sn
   | finiteBitSize (undefined :: i) == 32 = liftVEltwise1 sn (vectorOp1 @i @Int32 castPtr f32)
   | finiteBitSize (undefined :: i) == 64 = liftVEltwise1 sn (vectorOp1 @i @Int64 castPtr f64)
@@ -503,7 +508,7 @@ intWidBranch2 :: forall i n. (FiniteBits i, Storable i, Integral i)
               -> (Int64 -> Ptr Int64 -> Int64 -> Ptr Int64 -> IO ())  -- sv
               -> (Int64 -> Ptr Int64 -> Ptr Int64 -> Int64 -> IO ())  -- vs
               -> (Int64 -> Ptr Int64 -> Ptr Int64 -> Ptr Int64 -> IO ())  -- vv
-              -> (SNat n -> RS.Array n i -> RS.Array n i -> RS.Array n i)
+              -> (SNat n -> RS.Array (GHCFromNat n) i -> RS.Array (GHCFromNat n) i -> RS.Array (GHCFromNat n) i)
 intWidBranch2 ss sv32 vs32 vv32 sv64 vs64 vv64 sn
   | finiteBitSize (undefined :: i) == 32 = liftVEltwise2 sn (vectorOp2 @i @Int32 fromIntegral castPtr ss sv32 vs32 vv32)
   | finiteBitSize (undefined :: i) == 64 = liftVEltwise2 sn (vectorOp2 @i @Int64 fromIntegral castPtr ss sv64 vs64 vv64)
@@ -516,7 +521,7 @@ intWidBranchRed1 :: forall i n. (FiniteBits i, Storable i, Integral i)
                     -- int64
                  -> (Int64 -> Ptr Int64 -> Int64 -> Ptr Int64 -> IO ())  -- ^ scale by constant
                  -> (Int64 -> Ptr Int64 -> Ptr Int64 -> Ptr Int64 -> Ptr Int64 -> IO ())  -- ^ reduction kernel
-                 -> (SNat n -> RS.Array (n + 1) i -> RS.Array n i)
+                 -> (SNat n -> RS.Array (GHCFromNat (S n)) i -> RS.Array (GHCFromNat n) i)
 intWidBranchRed1 fsc32 fred32 fsc64 fred64 sn
   | finiteBitSize (undefined :: i) == 32 = vectorRedInnerOp @i @Int32 sn fromIntegral castPtr fsc32 fred32
   | finiteBitSize (undefined :: i) == 64 = vectorRedInnerOp @i @Int64 sn fromIntegral castPtr fsc64 fred64
@@ -528,7 +533,7 @@ intWidBranchRedFull :: forall i n. (FiniteBits i, Storable i, Integral i)
                     -> (Int64 -> Ptr Int64 -> Ptr Int64 -> Ptr Int32 -> IO Int32)  -- ^ reduction kernel
                        -- int64
                     -> (Int64 -> Ptr Int64 -> Ptr Int64 -> Ptr Int64 -> IO Int64)  -- ^ reduction kernel
-                    -> (SNat n -> RS.Array n i -> i)
+                    -> (SNat n -> RS.Array (GHCFromNat n) i -> i)
 intWidBranchRedFull fsc fred32 fred64 sn
   | finiteBitSize (undefined :: i) == 32 = vectorRedFullOp @i @Int32 sn fsc fromIntegral castPtr fred32
   | finiteBitSize (undefined :: i) == 64 = vectorRedFullOp @i @Int64 sn fsc fromIntegral castPtr fred64
@@ -554,26 +559,26 @@ intWidBranchDotprod :: forall i n. (FiniteBits i, Storable i, Integral i, NumElt
                     -> (Int64 -> Ptr Int64 -> Int64 -> Ptr Int64 -> IO ())  -- ^ scale by constant
                     -> (Int64 -> Ptr Int64 -> Ptr Int64 -> Ptr Int64 -> Ptr Int64 -> IO ())  -- ^ reduction kernel
                     -> (Int64 -> Ptr Int64 -> Ptr Int64 -> Ptr Int64 -> Ptr Int64 -> Ptr Int64 -> Ptr Int64 -> IO ())  -- ^ dotprod kernel
-                    -> (SNat n -> RS.Array (n + 1) i -> RS.Array (n + 1) i -> RS.Array n i)
+                    -> (SNat n -> RS.Array (GHCFromNat (S n)) i -> RS.Array (GHCFromNat (S n)) i -> RS.Array (GHCFromNat n) i)
 intWidBranchDotprod fsc32 fred32 fdot32 fsc64 fred64 fdot64 sn
   | finiteBitSize (undefined :: i) == 32 = vectorDotprodInnerOp @i @Int32 sn fromIntegral castPtr numEltMul fsc32 fred32 fdot32
   | finiteBitSize (undefined :: i) == 64 = vectorDotprodInnerOp @i @Int64 sn fromIntegral castPtr numEltMul fsc64 fred64 fdot64
   | otherwise = error "Unsupported Int width"
 
 class NumElt a where
-  numEltAdd :: SNat n -> RS.Array n a -> RS.Array n a -> RS.Array n a
-  numEltSub :: SNat n -> RS.Array n a -> RS.Array n a -> RS.Array n a
-  numEltMul :: SNat n -> RS.Array n a -> RS.Array n a -> RS.Array n a
-  numEltNeg :: SNat n -> RS.Array n a -> RS.Array n a
-  numEltAbs :: SNat n -> RS.Array n a -> RS.Array n a
-  numEltSignum :: SNat n -> RS.Array n a -> RS.Array n a
-  numEltSum1Inner :: SNat n -> RS.Array (n + 1) a -> RS.Array n a
-  numEltProduct1Inner :: SNat n -> RS.Array (n + 1) a -> RS.Array n a
-  numEltSumFull :: SNat n -> RS.Array n a -> a
-  numEltProductFull :: SNat n -> RS.Array n a -> a
-  numEltMinIndex :: SNat n -> RS.Array n a -> [Int]
-  numEltMaxIndex :: SNat n -> RS.Array n a -> [Int]
-  numEltDotprodInner :: SNat n -> RS.Array (n + 1) a -> RS.Array (n + 1) a -> RS.Array n a
+  numEltAdd :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  numEltSub :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  numEltMul :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  numEltNeg :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  numEltAbs :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  numEltSignum :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  numEltSum1Inner :: SNat n -> RS.Array (GHCFromNat (S n)) a -> RS.Array (GHCFromNat n) a
+  numEltProduct1Inner :: SNat n -> RS.Array (GHCFromNat (S n)) a -> RS.Array (GHCFromNat n) a
+  numEltSumFull :: SNat n -> RS.Array (GHCFromNat n) a -> a
+  numEltProductFull :: SNat n -> RS.Array (GHCFromNat n) a -> a
+  numEltMinIndex :: SNat n -> RS.Array (GHCFromNat n) a -> [Int]
+  numEltMaxIndex :: SNat n -> RS.Array (GHCFromNat n) a -> [Int]
+  numEltDotprodInner :: SNat n -> RS.Array (GHCFromNat (S n)) a -> RS.Array (GHCFromNat (S n)) a -> RS.Array (GHCFromNat n) a
 
 instance NumElt Int32 where
   numEltAdd = addVectorInt32
@@ -688,29 +693,29 @@ instance NumElt CInt where
                                                  (c_binary_i64_sv (aboEnum BO_MUL)) (c_reduce1_i64 (aroEnum RO_SUM)) c_dotprodinner_i64
 
 class FloatElt a where
-  floatEltDiv :: SNat n -> RS.Array n a -> RS.Array n a -> RS.Array n a
-  floatEltPow :: SNat n -> RS.Array n a -> RS.Array n a -> RS.Array n a
-  floatEltLogbase :: SNat n -> RS.Array n a -> RS.Array n a -> RS.Array n a
-  floatEltRecip :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltExp :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltLog :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltSqrt :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltSin :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltCos :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltTan :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltAsin :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltAcos :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltAtan :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltSinh :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltCosh :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltTanh :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltAsinh :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltAcosh :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltAtanh :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltLog1p :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltExpm1 :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltLog1pexp :: SNat n -> RS.Array n a -> RS.Array n a
-  floatEltLog1mexp :: SNat n -> RS.Array n a -> RS.Array n a
+  floatEltDiv :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltPow :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltLogbase :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltRecip :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltExp :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltLog :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltSqrt :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltSin :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltCos :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltTan :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltAsin :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltAcos :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltAtan :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltSinh :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltCosh :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltTanh :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltAsinh :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltAcosh :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltAtanh :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltLog1p :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltExpm1 :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltLog1pexp :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
+  floatEltLog1mexp :: SNat n -> RS.Array (GHCFromNat n) a -> RS.Array (GHCFromNat n) a
 
 instance FloatElt Float where
   floatEltDiv = divVectorFloat