{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_HADDOCK hide #-}

module Data.V.Linear.Internal
  ( V (..),
    empty,
    consume,
    map,
    pure,
    (<*>),
    uncons#,
    uncons,
    Elim,
    elim,
    cons,
    fromReplicator,
    dupV,
    theLength,
    Make,
    make,
    ArityV,
  )
where

import Data.Arity.Linear.Internal
import Data.Kind
import Data.Replicator.Linear.Internal (Replicator)
import qualified Data.Replicator.Linear.Internal as Replicator
import Data.Unrestricted.Linear.Internal.Dupable (Dupable (dupR))
import Data.Vector (Vector)
import qualified Data.Vector as Vector
import GHC.Exts (proxy#)
import GHC.TypeLits
import Prelude.Linear.Internal
import qualified Unsafe.Linear as Unsafe
import qualified Prelude

-- | @'V' n a@ represents an immutable sequence of @n@ elements of type @a@
-- (like a n-tuple), with a linear 'Data.Functor.Linear.Applicative' instance.
newtype V (n :: Nat) (a :: Type) = V (Vector a)
  deriving (V n a -> V n a -> Bool
forall (n :: Nat) a. Eq a => V n a -> V n a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: V n a -> V n a -> Bool
$c/= :: forall (n :: Nat) a. Eq a => V n a -> V n a -> Bool
== :: V n a -> V n a -> Bool
$c== :: forall (n :: Nat) a. Eq a => V n a -> V n a -> Bool
Prelude.Eq, V n a -> V n a -> Bool
V n a -> V n a -> Ordering
V n a -> V n a -> V n a
forall {n :: Nat} {a}. Ord a => Eq (V n a)
forall (n :: Nat) a. Ord a => V n a -> V n a -> Bool
forall (n :: Nat) a. Ord a => V n a -> V n a -> Ordering
forall (n :: Nat) a. Ord a => V n a -> V n a -> V n a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: V n a -> V n a -> V n a
$cmin :: forall (n :: Nat) a. Ord a => V n a -> V n a -> V n a
max :: V n a -> V n a -> V n a
$cmax :: forall (n :: Nat) a. Ord a => V n a -> V n a -> V n a
>= :: V n a -> V n a -> Bool
$c>= :: forall (n :: Nat) a. Ord a => V n a -> V n a -> Bool
> :: V n a -> V n a -> Bool
$c> :: forall (n :: Nat) a. Ord a => V n a -> V n a -> Bool
<= :: V n a -> V n a -> Bool
$c<= :: forall (n :: Nat) a. Ord a => V n a -> V n a -> Bool
< :: V n a -> V n a -> Bool
$c< :: forall (n :: Nat) a. Ord a => V n a -> V n a -> Bool
compare :: V n a -> V n a -> Ordering
$ccompare :: forall (n :: Nat) a. Ord a => V n a -> V n a -> Ordering
Prelude.Ord, Int -> V n a -> ShowS
forall (n :: Nat) a. Show a => Int -> V n a -> ShowS
forall (n :: Nat) a. Show a => [V n a] -> ShowS
forall (n :: Nat) a. Show a => V n a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [V n a] -> ShowS
$cshowList :: forall (n :: Nat) a. Show a => [V n a] -> ShowS
show :: V n a -> String
$cshow :: forall (n :: Nat) a. Show a => V n a -> String
showsPrec :: Int -> V n a -> ShowS
$cshowsPrec :: forall (n :: Nat) a. Show a => Int -> V n a -> ShowS
Prelude.Show, forall (n :: Nat) a. Eq a => a -> V n a -> Bool
forall (n :: Nat) a. Num a => V n a -> a
forall (n :: Nat) a. Ord a => V n a -> a
forall (n :: Nat) m. Monoid m => V n m -> m
forall (n :: Nat) a. V n a -> Bool
forall (n :: Nat) a. V n a -> Int
forall (n :: Nat) a. V n a -> [a]
forall (n :: Nat) a. (a -> a -> a) -> V n a -> a
forall (n :: Nat) m a. Monoid m => (a -> m) -> V n a -> m
forall (n :: Nat) b a. (b -> a -> b) -> b -> V n a -> b
forall (n :: Nat) a b. (a -> b -> b) -> b -> V n a -> b
forall a. Eq a => a -> V n a -> Bool
forall a. Num a => V n a -> a
forall a. Ord a => V n a -> a
forall m. Monoid m => V n m -> m
forall a. V n a -> Bool
forall a. V n a -> Int
forall a. V n a -> [a]
forall a. (a -> a -> a) -> V n a -> a
forall m a. Monoid m => (a -> m) -> V n a -> m
forall b a. (b -> a -> b) -> b -> V n a -> b
forall a b. (a -> b -> b) -> b -> V n a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => V n a -> a
$cproduct :: forall (n :: Nat) a. Num a => V n a -> a
sum :: forall a. Num a => V n a -> a
$csum :: forall (n :: Nat) a. Num a => V n a -> a
minimum :: forall a. Ord a => V n a -> a
$cminimum :: forall (n :: Nat) a. Ord a => V n a -> a
maximum :: forall a. Ord a => V n a -> a
$cmaximum :: forall (n :: Nat) a. Ord a => V n a -> a
elem :: forall a. Eq a => a -> V n a -> Bool
$celem :: forall (n :: Nat) a. Eq a => a -> V n a -> Bool
length :: forall a. V n a -> Int
$clength :: forall (n :: Nat) a. V n a -> Int
null :: forall a. V n a -> Bool
$cnull :: forall (n :: Nat) a. V n a -> Bool
toList :: forall a. V n a -> [a]
$ctoList :: forall (n :: Nat) a. V n a -> [a]
foldl1 :: forall a. (a -> a -> a) -> V n a -> a
$cfoldl1 :: forall (n :: Nat) a. (a -> a -> a) -> V n a -> a
foldr1 :: forall a. (a -> a -> a) -> V n a -> a
$cfoldr1 :: forall (n :: Nat) a. (a -> a -> a) -> V n a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> V n a -> b
$cfoldl' :: forall (n :: Nat) b a. (b -> a -> b) -> b -> V n a -> b
foldl :: forall b a. (b -> a -> b) -> b -> V n a -> b
$cfoldl :: forall (n :: Nat) b a. (b -> a -> b) -> b -> V n a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> V n a -> b
$cfoldr' :: forall (n :: Nat) a b. (a -> b -> b) -> b -> V n a -> b
foldr :: forall a b. (a -> b -> b) -> b -> V n a -> b
$cfoldr :: forall (n :: Nat) a b. (a -> b -> b) -> b -> V n a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> V n a -> m
$cfoldMap' :: forall (n :: Nat) m a. Monoid m => (a -> m) -> V n a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> V n a -> m
$cfoldMap :: forall (n :: Nat) m a. Monoid m => (a -> m) -> V n a -> m
fold :: forall m. Monoid m => V n m -> m
$cfold :: forall (n :: Nat) m. Monoid m => V n m -> m
Prelude.Foldable, forall (n :: Nat) a b. a -> V n b -> V n a
forall (n :: Nat) a b. (a -> b) -> V n a -> V n b
forall a b. a -> V n b -> V n a
forall a b. (a -> b) -> V n a -> V n b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> V n b -> V n a
$c<$ :: forall (n :: Nat) a b. a -> V n b -> V n a
fmap :: forall a b. (a -> b) -> V n a -> V n b
$cfmap :: forall (n :: Nat) a b. (a -> b) -> V n a -> V n b
Prelude.Functor, forall (n :: Nat). Functor (V n)
forall (n :: Nat). Foldable (V n)
forall (n :: Nat) (m :: * -> *) a.
Monad m =>
V n (m a) -> m (V n a)
forall (n :: Nat) (f :: * -> *) a.
Applicative f =>
V n (f a) -> f (V n a)
forall (n :: Nat) (m :: * -> *) a b.
Monad m =>
(a -> m b) -> V n a -> m (V n b)
forall (n :: Nat) (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> V n a -> f (V n b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> V n a -> f (V n b)
sequence :: forall (m :: * -> *) a. Monad m => V n (m a) -> m (V n a)
$csequence :: forall (n :: Nat) (m :: * -> *) a.
Monad m =>
V n (m a) -> m (V n a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> V n a -> m (V n b)
$cmapM :: forall (n :: Nat) (m :: * -> *) a b.
Monad m =>
(a -> m b) -> V n a -> m (V n b)
sequenceA :: forall (f :: * -> *) a. Applicative f => V n (f a) -> f (V n a)
$csequenceA :: forall (n :: Nat) (f :: * -> *) a.
Applicative f =>
V n (f a) -> f (V n a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> V n a -> f (V n b)
$ctraverse :: forall (n :: Nat) (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> V n a -> f (V n b)
Prelude.Traversable)

-- Using vector rather than, say, 'Array' (or directly 'Array#') because it
-- offers many convenience function. Since all these unsafeCoerces probably
-- kill the fusion rules, it may be worth it going lower level since I
-- probably have to write my own fusion anyway. Therefore, starting from
-- Vectors at the moment.

-- | Returns an empty 'V'.
empty :: forall a. V 0 a
empty :: forall a. V 0 a
empty = forall (n :: Nat) a. Vector a -> V n a
V forall a. Vector a
Vector.empty

consume :: V 0 a %1 -> ()
consume :: forall a. V 0 a %1 -> ()
consume = forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear (\V 0 a
_ -> ())
{-# INLINEABLE consume #-}

map :: (a %1 -> b) -> V n a %1 -> V n b
map :: forall a b (n :: Nat). (a %1 -> b) -> V n a %1 -> V n b
map a %1 -> b
f (V Vector a
xs) = forall (n :: Nat) a. Vector a -> V n a
V forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear (forall a b. (a -> b) -> Vector a -> Vector b
Vector.map (\a
x -> a %1 -> b
f a
x)) Vector a
xs

(<*>) :: V n (a %1 -> b) %1 -> V n a %1 -> V n b
(V Vector (a %1 -> b)
fs) <*> :: forall (n :: Nat) a b. V n (a %1 -> b) %1 -> V n a %1 -> V n b
<*> (V Vector a
xs) =
  forall (n :: Nat) a. Vector a -> V n a
V forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$
    forall a b c (p :: Multiplicity) (q :: Multiplicity)
       (x :: Multiplicity) (y :: Multiplicity).
(a %p -> b %q -> c) %1 -> a %x -> b %y -> c
Unsafe.toLinear2 (forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
Vector.zipWith (\a %1 -> b
f a
x -> a %1 -> b
f forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ a
x)) Vector (a %1 -> b)
fs Vector a
xs

infixl 4 <*> -- same fixity as base.<*>

-- | Splits the head and tail of the 'V', returning an unboxed tuple.
uncons# :: (1 <= n) => V n a %1 -> (# a, V (n - 1) a #)
uncons# :: forall (n :: Nat) a. (1 <= n) => V n a %1 -> (# a, V (n - 1) a #)
uncons# = forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear forall (n :: Nat) a. (1 <= n) => V n a -> (# a, V (n - 1) a #)
uncons'#
  where
    uncons'# :: (1 <= n) => V n a -> (# a, V (n - 1) a #)
    uncons'# :: forall (n :: Nat) a. (1 <= n) => V n a -> (# a, V (n - 1) a #)
uncons'# (V Vector a
xs) = (# forall a. Vector a -> a
Vector.head Vector a
xs, forall (n :: Nat) a. Vector a -> V n a
V (forall a. Vector a -> Vector a
Vector.tail Vector a
xs) #)
{-# INLINEABLE uncons# #-}

-- | Splits the head and tail of the 'V', returning a boxed tuple.
uncons :: (1 <= n) => V n a %1 -> (a, V (n - 1) a)
uncons :: forall (n :: Nat) a. (1 <= n) => V n a %1 -> (a, V (n - 1) a)
uncons = forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear forall (n :: Nat) a. (1 <= n) => V n a -> (a, V (n - 1) a)
uncons'
  where
    uncons' :: (1 <= n) => V n a -> (a, V (n - 1) a)
    uncons' :: forall (n :: Nat) a. (1 <= n) => V n a -> (a, V (n - 1) a)
uncons' (V Vector a
xs) = (forall a. Vector a -> a
Vector.head Vector a
xs, forall (n :: Nat) a. Vector a -> V n a
V (forall a. Vector a -> Vector a
Vector.tail Vector a
xs))
{-# INLINEABLE uncons #-}

-- | Takes a function of type @a %1 -> a %1 -> ... %1 -> a %1 -> b@, and
-- returns a @b@ . The @'V' n a@ is used to supply all the items of type @a@
-- required by the function.
--
-- For instance:
--
-- > elim @1 :: (a %1 -> b) %1 -> V 1 a %1 -> b
-- > elim @2 :: (a %1 -> a %1 -> b) %1 -> V 2 a %1 -> b
-- > elim @3 :: (a %1 -> a %1 -> a %1 -> b) %1 -> V 3 a %1 -> b
--
-- It is not always necessary to give the arity argument. It can be
-- inferred from the function argument.
--
-- About the constraints of this function (they won't get in your way):
--
-- * @n ~ 'PeanoToNat' ('NatToPeano' n)@ is just there to help GHC, and will always be proved
-- * @'Elim' ('NatToPeano' n) a b@ provides the actual implementation of 'elim'; there is an instance of this class for any @(n, a, b)@
-- * @'IsFunN' a b f, f ~ 'FunN' ('NatToPeano' n) a b, n ~ 'Arity' b f@ indicate the shape of @f@ to the typechecker (see documentation of 'IsFunN').
elim ::
  forall (n :: Nat) a b f.
  ( -- GHC cannot prove it for any @n@, but can prove it at call site when
    -- @n@ is known
    n ~ PeanoToNat (NatToPeano n),
    Elim (NatToPeano n) a b,
    IsFunN a b f,
    f ~ FunN (NatToPeano n) a b,
    n ~ Arity b f
  ) =>
  f %1 ->
  V n a %1 ->
  b
elim :: forall (n :: Nat) a b f.
(n ~ PeanoToNat (NatToPeano n), Elim (NatToPeano n) a b,
 IsFunN a b f, f ~ FunN (NatToPeano n) a b, n ~ Arity b f) =>
f %1 -> V n a %1 -> b
elim f
f V n a
v = forall (n :: Peano) a b.
Elim n a b =>
FunN n a b %1 -> V (PeanoToNat n) a %1 -> b
elim' @(NatToPeano n) f
f V n a
v

-- | @'Elim' n a b@ is used to implement 'elim' without recursion
-- so that we can guarantee that 'elim' will be inlined and unrolled.
--
-- 'Elim' is solely used in the signature of 'elim'.
type Elim :: Peano -> Type -> Type -> Constraint
class Elim n a b where
  -- Note that 'elim' is, in particular, used to force eta-expansion of
  -- 'elim\''. Otherwise, 'elim\'' might not get inlined (see
  -- https://github.com/tweag/linear-base/issues/369).
  elim' :: FunN n a b %1 -> V (PeanoToNat n) a %1 -> b

instance Elim 'Z a b where
  elim' :: FunN 'Z a b %1 -> V (PeanoToNat 'Z) a %1 -> b
elim' FunN 'Z a b
b V (PeanoToNat 'Z) a
v =
    forall a. V 0 a %1 -> ()
consume V (PeanoToNat 'Z) a
v forall a b (p :: Multiplicity) (q :: Multiplicity).
a %p -> (a %p -> b) %q -> b
& \case
      () -> FunN 'Z a b
b
  {-# INLINE elim' #-}

instance (1 <= 1 + PeanoToNat n, (1 + PeanoToNat n) - 1 ~ PeanoToNat n, Elim n a b) => Elim ('S n) a b where
  elim' :: FunN ('S n) a b %1 -> V (PeanoToNat ('S n)) a %1 -> b
elim' FunN ('S n) a b
g V (PeanoToNat ('S n)) a
v =
    forall (n :: Nat) a. (1 <= n) => V n a %1 -> (a, V (n - 1) a)
uncons V (PeanoToNat ('S n)) a
v forall a b (p :: Multiplicity) (q :: Multiplicity).
a %p -> (a %p -> b) %q -> b
& \case
      (a
a, V ((1 + PeanoToNat n) - 1) a
v') -> forall (n :: Peano) a b.
Elim n a b =>
FunN n a b %1 -> V (PeanoToNat n) a %1 -> b
elim' @n (FunN ('S n) a b
g a
a) V ((1 + PeanoToNat n) - 1) a
v'
  {-# INLINE elim' #-}

-- | Prepends the given element to the 'V'.
cons :: forall n a. a %1 -> V (n - 1) a %1 -> V n a
cons :: forall (n :: Nat) a. a %1 -> V (n - 1) a %1 -> V n a
cons = forall a b c (p :: Multiplicity) (q :: Multiplicity)
       (x :: Multiplicity) (y :: Multiplicity).
(a %p -> b %q -> c) %1 -> a %x -> b %y -> c
Unsafe.toLinear2 forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ \a
x (V Vector a
v) -> forall (n :: Nat) a. Vector a -> V n a
V (forall a. a -> Vector a -> Vector a
Vector.cons a
x Vector a
v)

-- | The 'ArityV' type family exists to help the type checker compute the arity
-- @n ~ 'Arity' b f@ when @b ~ 'V' n a@.
type family ArityV f where
  ArityV (V _ _) = 0
  ArityV (a %1 -> f) = 1 + ArityV f
  ArityV f =
    TypeError
      ( 'Text "Arity: "
          ':<>: 'ShowType f
          ':<>: 'Text " isn't a linear function with head (V _ _)"
      )

-- | Builds a n-ary constructor for @'V' n a@ (i.e. a function taking @n@ linear
-- arguments of type @a@ and returning a @'V' n a@).
--
-- > myV :: V 3 Int
-- > myV = make 1 2 3
--
-- About the constraints of this function (they won't get in your way):
--
-- * @n ~ 'PeanoToNat' ('NatToPeano' n)@ is just there to help GHC, and will always be proved
-- * @'Make' ('NatToPeano' n) ('NatToPeano' n) a@ provides the actual implementation of 'make'; there is an instance of this class for any @(n, a)@
-- * @'IsFunN' a ('V' n a) f, f ~ 'FunN' ('NatToPeano' n) a ('V' n a), n ~ 'ArityV' f@ indicate the shape to the typechecker of @f@ (see documentation of 'IsFunN').
make ::
  forall (n :: Nat) a f.
  ( -- GHC cannot prove it for any @n@, but can prove it at call site when
    -- @n@ is known
    n ~ PeanoToNat (NatToPeano n),
    Make (NatToPeano n) (NatToPeano n) a,
    IsFunN a (V n a) f,
    f ~ FunN (NatToPeano n) a (V n a),
    n ~ ArityV f
  ) =>
  f
make :: forall (n :: Nat) a f.
(n ~ PeanoToNat (NatToPeano n),
 Make (NatToPeano n) (NatToPeano n) a, IsFunN a (V n a) f,
 f ~ FunN (NatToPeano n) a (V n a), n ~ ArityV f) =>
f
make = forall (m :: Peano) (n :: Peano) a.
Make m n a =>
(V (PeanoToNat m) a %1 -> V (PeanoToNat n) a)
%1 -> FunN m a (V (PeanoToNat n) a)
make' @(NatToPeano n) @(NatToPeano n) @a forall a (q :: Multiplicity). a %q -> a
id
{-# INLINE make #-}

-- | @'Make' m n a@ is used to avoid recursion in the implementation of 'make'
-- so that 'make' can be inlined.
--
-- 'Make' is solely used in the signature of that function.
type Make :: Peano -> Peano -> Type -> Constraint
class Make m n a where
  -- The idea behind Make / make' / make is the following:
  --
  -- The function created by make' takes m values of type a, but returns a 'V n a' (with n ≥ m),
  -- so the n - m missing values must be supplied via the accumulator.
  --
  -- make' is initially called with m = n via make, and as m decreases,
  -- the number of lambda on the left increases and the captured values are put
  -- in the accumulator
  -- ('V[ ... ] <> ' represents the "extend" operation for 'V'):
  --
  -- >     make @n
  -- > --> make' @n @n (V[] <>)
  -- > --> λx. make' @(n - 1) @n (V[x] <>)
  -- > --> λx. λy. make' @(n - 2) @n (V[x, y] <>)
  -- > --> ...
  -- > --> λx. λy. ... λz. make' @0 @n (V[x, y, ... z] <>)    -- make' @0 @n f = f V[]
  -- > --> λx. λy. ... λz. V[x, y, ... z]
  make' :: (V (PeanoToNat m) a %1 -> V (PeanoToNat n) a) %1 -> FunN m a (V (PeanoToNat n) a)

instance Make 'Z n a where
  make' :: (V (PeanoToNat 'Z) a %1 -> V (PeanoToNat n) a)
%1 -> FunN 'Z a (V (PeanoToNat n) a)
make' V (PeanoToNat 'Z) a %1 -> V (PeanoToNat n) a
produceFrom = V (PeanoToNat 'Z) a %1 -> V (PeanoToNat n) a
produceFrom forall a. V 0 a
empty
  {-# INLINE make' #-}

instance ((1 + PeanoToNat m) - 1 ~ PeanoToNat m, Make m n a) => Make ('S m) n a where
  make' :: (V (PeanoToNat ('S m)) a %1 -> V (PeanoToNat n) a)
%1 -> FunN ('S m) a (V (PeanoToNat n) a)
make' V (PeanoToNat ('S m)) a %1 -> V (PeanoToNat n) a
produceFrom = \a
x -> forall (m :: Peano) (n :: Peano) a.
Make m n a =>
(V (PeanoToNat m) a %1 -> V (PeanoToNat n) a)
%1 -> FunN m a (V (PeanoToNat n) a)
make' @m @n @a (\V (PeanoToNat m) a
s -> V (PeanoToNat ('S m)) a %1 -> V (PeanoToNat n) a
produceFrom forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ forall (n :: Nat) a. a %1 -> V (n - 1) a %1 -> V n a
cons a
x V (PeanoToNat m) a
s)
  {-# INLINE make' #-}

-------------------------------------------------------------------------------
-- Functions below use AllowAmbiguousTypes
-------------------------------------------------------------------------------

-- | Returns the type-level 'Nat' of the context as a term-level integer.
theLength :: forall n. (KnownNat n) => Prelude.Int
theLength :: forall (n :: Nat). KnownNat n => Int
theLength = forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral (forall (n :: Nat). KnownNat n => Proxy# n -> Integer
natVal' @n (forall {k} (a :: k). Proxy# a
proxy# @_))

pure :: forall n a. (KnownNat n) => a -> V n a
pure :: forall (n :: Nat) a. KnownNat n => a -> V n a
pure a
a = forall (n :: Nat) a. Vector a -> V n a
V forall a b (p :: Multiplicity) (q :: Multiplicity).
(a %p -> b) %q -> a %p -> b
$ forall a. Int -> a -> Vector a
Vector.replicate (forall (n :: Nat). KnownNat n => Int
theLength @n) a
a

-- | Creates a 'V' of the specified size by consuming a 'Replicator'.
fromReplicator :: forall n a. (KnownNat n) => Replicator a %1 -> V n a
fromReplicator :: forall (n :: Nat) a. KnownNat n => Replicator a %1 -> V n a
fromReplicator = let n' :: Int
n' = forall (n :: Nat). KnownNat n => Int
theLength @n in forall (n :: Nat) a. Vector a -> V n a
V forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. forall a b (p :: Multiplicity) (x :: Multiplicity).
(a %p -> b) %1 -> a %x -> b
Unsafe.toLinear forall a. [a] -> Vector a
Vector.fromList forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. forall a. Int -> Replicator a %1 -> [a]
Replicator.take Int
n'

-- | Produces a @'V' n a@ from a 'Dupable' value @a@.
dupV :: forall n a. (KnownNat n, Dupable a) => a %1 -> V n a
dupV :: forall (n :: Nat) a. (KnownNat n, Dupable a) => a %1 -> V n a
dupV = forall (n :: Nat) a. KnownNat n => Replicator a %1 -> V n a
fromReplicator forall b c a (q :: Multiplicity) (m :: Multiplicity)
       (n :: Multiplicity).
(b %1 -> c) %q -> (a %1 -> b) %m -> a %n -> c
. forall a. Dupable a => a %1 -> Replicator a
dupR