Dim & Dims

readme.org

@@ -744,21 +744,8 @@ import Data.Vector qualified as V
 #+end_src
 
 #+RESULTS:
-#+begin_example
-Build profile: -w ghc-9.8.2 -O1
-In order, the following will be built (use -v for more details):
- - numhask-array-0.12 (lib) (file src/NumHask/Array/Fixed.hs changed)
-Preprocessing library for numhask-array-0.12..
-GHCi, version 9.8.2: https://www.haskell.org/ghc/  :? for help
-Loaded GHCi configuration from /Users/tonyday567/haskell/numhask-array/.ghci
-[1 of 5] Compiling NumHask.Array.Shape ( src/NumHask/Array/Shape.hs, interpreted )
-[2 of 5] Compiling NumHask.Array.Sort ( src/NumHask/Array/Sort.hs, interpreted )
-[3 of 5] Compiling NumHask.Array.Dynamic ( src/NumHask/Array/Dynamic.hs, interpreted )
-[4 of 5] Compiling NumHask.Array.Fixed ( src/NumHask/Array/Fixed.hs, interpreted )
-[5 of 5] Compiling NumHask.Array    ( src/NumHask/Array.hs, interpreted )
-Ok, five modules loaded.
-Ok, five modules loaded.
-#+end_example
+: [4 of 5] Compiling NumHask.Array.Fixed ( src/NumHask/Array/Fixed.hs, interpreted ) [Source file changed]
+: Ok, five modules loaded.
 
 #+begin_src haskell-ng
 a = range @[2,3,4]
@@ -1505,27 +1492,40 @@ https://github.com/goldfirere/singletons/blob/master/README.md
 ** dependent type examples
 
 #+begin_src haskell-ng :results output
+:{
 example_inserta :: (Show a, FromInteger a) => SomeArray a -> String
-example_inserta (SomeArray (SNats :: SNats ns) a) = show (insert (SNat @0) 0 a (toScalar 0))
--- Could not deduce ‘KnownNats
+example_inserta (SomeArray (SNats :: SNats ns) a) = show (insert (SNat @0) (SNat @0) a (toScalar 0))
+:}
 -- (If (s Data.Type.Equality.== '[]) '[1] s)’
 --    arising from a use of ‘insert’
 #+end_src
 
 segfaults as SNats is somehow SNat @'[]
 
 #+begin_src haskell-ng :results output
+:{
+import Fcf (Eval)
+someTakeDim :: forall d t s. (KnownNats s, KnownNat d, KnownNat t) => SNats (Eval (TakeDim d t s))
+someTakeDim = withSomeSNats (fromIntegral <$> takeDim (int (SNat :: SNat d)) (int (SNat :: SNat t)) (ints (SNats :: SNats s))) unsafeCoerce
+
 example_take :: forall a s. (KnownNats s, Show a) => Nat -> Nat -> Array s a -> String
 example_take d t a =
   withSomeSNat d
   (\(SNat :: SNat d) ->
     withSomeSNat t
     (\(SNat :: SNat t) ->
       case someTakeDim @d @t @s of
-        SNats -> show $ take (SNat @d) (SNat @t) a))
+        SNats -> show $ F.take (SNat @d) (SNat @t) a))
+:}
 #+end_src
 
+but this is ok
+
 #+begin_src haskell-ng :results output
+:{
+someTakeDim2 :: forall d t s. (KnownNats s, KnownNat d, KnownNat t) => SNats (Eval (TakeDim d t s))
+someTakeDim2 = UnsafeSNats (fromIntegral <$> takeDim (int @d) (int @t) (ints @s))
+
 example_take' :: forall a s. (KnownNats s, Show a) => Nat -> Nat -> Array s a -> String
 example_take' d t a =
   withSomeSNat d
@@ -1534,64 +1534,6 @@ example_take' d t a =
     (\(SNat :: SNat t) ->
       case someTakeDim2 @d' @t @s of
         x -> show x <> " " <> show (someTakeDim2 @d' @t @s) <> " : take " <> show (SNat @d') <> " " <> show (SNat @t) <> " " <> show a))
-#+end_src
-
-example_take' 0 1 (range @[2,3,4])
-"SNats @[1, 3, 4] SNats @[1, 3, 4] : take SNat @0 SNat @1 [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23]"
-
-vector examples
-
-#+begin_src haskell-ng :results output
-data SomeVector a where
-  SomeVector :: KnownNat n => Vector n a -> SomeVector a
-
-deriving instance (Show a) => Show (SomeVector a)
-
-withLength :: forall n a r. Vector n a -> (KnownNat n => r) -> r
-withLength v r = case someNatVal (fromIntegral $ V.length (asVector v)) of
-  SomeNat (Proxy :: Proxy n') -> case unsafeCoerce Refl of
-    (Refl :: n :~: n') -> r
-
-aVector :: FromVector t a => t -> SomeVector a
-aVector (Array . asVector -> v) = withLength v (SomeVector v)
 
-example_append :: (Show a, Num a, FromInteger a) => SomeVector a -> String
-example_append (SomeVector a) = show (append (SNat @0) a (toScalar 0))
-
-example_insert :: (Show a, FromInteger a) => SomeVector a -> String
-example_insert (SomeVector a) = show (insert (SNat @0) 0 a (toScalar 0))
-
-data SomeVector' a = forall n. SomeVector' (SNat n) (Vector n a)
-
-deriving instance (Show a) => Show (SomeVector' a)
-
-someVector' :: FromVector t a => KnownNat n => SNat n -> t -> SomeVector' a
-someVector' n t = SomeVector' n (vector' n t)
-
-aVector' :: forall a t. FromVector t a => t -> SomeVector' a
-aVector' t = withSomeSNat (fromIntegral $ V.length (asVector t)) $ \(SNat :: SNat n) -> SomeVector' SNat (vector' (SNat @n) (asVector t))
-
-example_insert' :: (Show a, FromInteger a) => SomeVector' a -> String
-example_insert' (SomeVector' (SNat :: SNat n) a) = show (insert (SNat @0) 0 a (toScalar 0))
-
-example_append' :: (Show a, Num a, FromInteger a) => SomeVector' a -> String
-example_append' (SomeVector' (SNat :: SNat n) a) = show (append (SNat @0) a (toScalar 0))
-
-instance (Arbitrary a) => Arbitrary (SomeVector' a) where
-  arbitrary = do
-    n <- arbitrary
-    v <- V.replicateM (Prelude.fromIntegral n) arbitrary
-    withSomeNat n $ \sn -> pure (someVector' sn v)
-#+end_src
-
-
-#+begin_src haskell-ng :results output
-someTakeDim :: forall d t s. (KnownNats s, KnownNat d, KnownNat t) => SNats (Eval (TakeDim d t s))
-someTakeDim = withSomeSNats (fromIntegral <$> takeDim (int (SNat :: SNat d)) (int (SNat :: SNat t)) (ints (SNats :: SNats s))) unsafeCoerce
-
-someTakeDim2 :: forall d t s. (KnownNats s, KnownNat d, KnownNat t) => SNats (Eval (TakeDim d t s))
-someTakeDim2 = UnsafeSNats (fromIntegral <$> takeDim (int (SNat :: SNat d)) (int (SNat :: SNat t)) (ints (SNats :: SNats s)))
-
-someUnsafeGetIndex :: forall d s. (KnownNats s, KnownNat d) => SNat (Eval (UnsafeGetIndex d s))
-someUnsafeGetIndex = withSomeSNat (fromIntegral $ getDim (int (SNat :: SNat d)) (ints (SNats :: SNats s))) unsafeCoerce
+:}
 #+end_src