{-|
Module           : Data.Parameterized.Context
Copyright        : (c) Galois, Inc 2014-2019
Maintainer       : Joe Hendrix <jhendrix@galois.com>

This module reexports either "Data.Parameterized.Context.Safe"
or "Data.Parameterized.Context.Unsafe" depending on the
the unsafe-operations compile-time flag.

It also defines some utility typeclasses for transforming
between curried and uncurried versions of functions over contexts.

The 'Assignment' type is isomorphic to the 'Data.Parameterized.List'
type, except 'Assignment's construct lists from the right-hand side,
and instead of using type-level @'[]@-style lists, an 'Assignment' is
indexed by a type-level 'Data.Parameterized.Context.Ctx'. The
implementation of 'Assignment's is also more efficent than
'Data.Parameterized.List' for lists of many elements, as it uses a
balanced binary tree representation rather than a linear-time
list. For a motivating example, see 'Data.Parameterized.List'.

-}

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE ViewPatterns #-}
module Data.Parameterized.Context
 (
#ifdef UNSAFE_OPS
    module Data.Parameterized.Context.Unsafe
#else
    module Data.Parameterized.Context.Safe
#endif
  , singleton
  , toVector
  , pattern (:>)
  , pattern Empty
  , decompose
  , Data.Parameterized.Context.null
  , Data.Parameterized.Context.init
  , Data.Parameterized.Context.last
  , Data.Parameterized.Context.view
  , Data.Parameterized.Context.take
  , Data.Parameterized.Context.drop
  , forIndexM
  , generateSome
  , generateSomeM
  , fromList
  , traverseAndCollect
  , traverseWithIndex_
  , dropPrefix
  , unzip
  , flattenAssignment
  , flattenSize

    -- * Context extension and embedding utilities
  , CtxEmbedding(..)
  , ExtendContext(..)
  , ExtendContext'(..)
  , ApplyEmbedding(..)
  , ApplyEmbedding'(..)
  , identityEmbedding
  , extendEmbeddingRightDiff
  , extendEmbeddingRight
  , extendEmbeddingBoth
  , appendEmbedding
  , appendEmbeddingLeft
  , ctxeSize
  , ctxeAssignment

    -- * Static indexing and lenses for assignments
  , Idx
  , field
  , natIndex
  , natIndexProxy
    -- * Currying and uncurrying for assignments
  , CurryAssignment
  , CurryAssignmentClass(..)
    -- * Size and Index values
  , size1, size2, size3, size4, size5, size6
  , i1of2, i2of2
  , i1of3, i2of3, i3of3
  , i1of4, i2of4, i3of4, i4of4
  , i1of5, i2of5, i3of5, i4of5, i5of5
  , i1of6, i2of6, i3of6, i4of6, i5of6, i6of6
  ) where

import           Prelude hiding (unzip)

import           Control.Applicative (liftA2)
import           Control.Lens hiding (Index, (:>), Empty)
import           Data.Functor (void)
import           Data.Functor.Product (Product(Pair))
import           Data.Kind
import qualified Data.Vector as V
import qualified Data.Vector.Mutable as MV
import           GHC.TypeLits (Nat, type (-))

import           Data.Parameterized.Classes
import           Data.Parameterized.Some
import           Data.Parameterized.TraversableFC

#ifdef UNSAFE_OPS
import           Data.Parameterized.Context.Unsafe
#else
import           Data.Parameterized.Context.Safe
#endif


-- | Create a single element context.
singleton :: f tp -> Assignment f (EmptyCtx ::> tp)
singleton :: f tp -> Assignment f (EmptyCtx ::> tp)
singleton = (Assignment f EmptyCtx
forall k (f :: k -> *). Assignment f EmptyCtx
empty Assignment f EmptyCtx -> f tp -> Assignment f (EmptyCtx ::> tp)
forall k (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>)

-- |'forIndexM sz f' calls 'f' on indices '[0..sz-1]'.
forIndexM :: forall ctx m
           . Applicative m
          => Size ctx
          -> (forall tp . Index ctx tp -> m ())
          -> m ()
forIndexM :: Size ctx -> (forall (tp :: k). Index ctx tp -> m ()) -> m ()
forIndexM Size ctx
sz forall (tp :: k). Index ctx tp -> m ()
f = Int
-> Size ctx
-> (forall (tp :: k). Index ctx tp -> m () -> m ())
-> m ()
-> m ()
forall k (ctx :: Ctx k) r.
Int
-> Size ctx -> (forall (tp :: k). Index ctx tp -> r -> r) -> r -> r
forIndexRange Int
0 Size ctx
sz (\Index ctx tp
i m ()
r -> Index ctx tp -> m ()
forall (tp :: k). Index ctx tp -> m ()
f Index ctx tp
i m () -> m () -> m ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m ()
r) (() -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())

-- | Generate an assignment with some context type that is not known.
generateSome :: forall f
              . Int
             -> (Int -> Some f)
             -> Some (Assignment f)
generateSome :: Int -> (Int -> Some f) -> Some (Assignment f)
generateSome Int
n Int -> Some f
f = Int -> Some (Assignment f)
go Int
n
  where go :: Int -> Some (Assignment f)
        go :: Int -> Some (Assignment f)
go Int
0 = Assignment f EmptyCtx -> Some (Assignment f)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some Assignment f EmptyCtx
forall k (f :: k -> *). Assignment f EmptyCtx
empty
        go Int
i = (\(Some Assignment f x
a) (Some e) -> Assignment f (x ::> x) -> Some (Assignment f)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (Assignment f x
a Assignment f x -> f x -> Assignment f (x ::> x)
forall k (f :: k -> *) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
`extend` f x
e)) (Int -> Some (Assignment f)
go (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) (Int -> Some f
f (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))

-- | Generate an assignment with some context type that is not known.
generateSomeM :: forall m f
              .  Applicative m
              => Int
              -> (Int -> m (Some f))
              -> m (Some (Assignment f))
generateSomeM :: Int -> (Int -> m (Some f)) -> m (Some (Assignment f))
generateSomeM Int
n Int -> m (Some f)
f = Int -> m (Some (Assignment f))
go Int
n
  where go :: Int -> m (Some (Assignment f))
        go :: Int -> m (Some (Assignment f))
go Int
0 = Some (Assignment f) -> m (Some (Assignment f))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Assignment f EmptyCtx -> Some (Assignment f)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some Assignment f EmptyCtx
forall k (f :: k -> *). Assignment f EmptyCtx
empty)
        go Int
i = (\(Some Assignment f x
a) (Some e) -> Assignment f (x ::> x) -> Some (Assignment f)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (Assignment f x
a Assignment f x -> f x -> Assignment f (x ::> x)
forall k (f :: k -> *) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
`extend` f x
e)) (Some (Assignment f) -> Some f -> Some (Assignment f))
-> m (Some (Assignment f)) -> m (Some f -> Some (Assignment f))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m (Some (Assignment f))
go (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) m (Some f -> Some (Assignment f))
-> m (Some f) -> m (Some (Assignment f))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> m (Some f)
f (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)

-- | Convert the assignment to a vector.
toVector :: Assignment f tps -> (forall tp . f tp -> e) -> V.Vector e
toVector :: Assignment f tps -> (forall (tp :: k). f tp -> e) -> Vector e
toVector Assignment f tps
a forall (tp :: k). f tp -> e
f = (forall s. ST s (MVector s e)) -> Vector e
forall a. (forall s. ST s (MVector s a)) -> Vector a
V.create ((forall s. ST s (MVector s e)) -> Vector e)
-> (forall s. ST s (MVector s e)) -> Vector e
forall a b. (a -> b) -> a -> b
$ do
  MVector s e
vm <- Int -> ST s (MVector (PrimState (ST s)) e)
forall (m :: * -> *) a.
PrimMonad m =>
Int -> m (MVector (PrimState m) a)
MV.new (Size tps -> Int
forall k (ctx :: Ctx k). Size ctx -> Int
sizeInt (Assignment f tps -> Size tps
forall k (f :: k -> *) (ctx :: Ctx k). Assignment f ctx -> Size ctx
size Assignment f tps
a))
  Size tps -> (forall (tp :: k). Index tps tp -> ST s ()) -> ST s ()
forall k (ctx :: Ctx k) (m :: * -> *).
Applicative m =>
Size ctx -> (forall (tp :: k). Index ctx tp -> m ()) -> m ()
forIndexM (Assignment f tps -> Size tps
forall k (f :: k -> *) (ctx :: Ctx k). Assignment f ctx -> Size ctx
size Assignment f tps
a) ((forall (tp :: k). Index tps tp -> ST s ()) -> ST s ())
-> (forall (tp :: k). Index tps tp -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \Index tps tp
i -> do
    MVector (PrimState (ST s)) e -> Int -> e -> ST s ()
forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector s e
MVector (PrimState (ST s)) e
vm (Index tps tp -> Int
forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
indexVal Index tps tp
i) (f tp -> e
forall (tp :: k). f tp -> e
f (Assignment f tps
a Assignment f tps -> Index tps tp -> f tp
forall k (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Index tps tp
i))
  MVector s e -> ST s (MVector s e)
forall (m :: * -> *) a. Monad m => a -> m a
return MVector s e
vm
{-# INLINABLE toVector #-}

-- | Utility function for testing if @xs@ is an assignment with
--   `prefix` as a prefix, and computing the tail of xs
--   not in the prefix, if so.
dropPrefix :: forall f xs prefix a.
  TestEquality f =>
  Assignment f xs     {- ^ Assignment to split -} ->
  Assignment f prefix {- ^ Expected prefix -} ->
  a {- ^ error continuation -} ->
  (forall addl. (xs ~ (prefix <+> addl)) => Assignment f addl -> a)
    {- ^ success continuation -} ->
  a
dropPrefix :: Assignment f xs
-> Assignment f prefix
-> a
-> (forall (addl :: Ctx k).
    (xs ~ (prefix <+> addl)) =>
    Assignment f addl -> a)
-> a
dropPrefix Assignment f xs
xs0 Assignment f prefix
prefix a
err = Assignment f xs
-> Int
-> (forall (addl :: Ctx k).
    (xs ~ (prefix <+> addl)) =>
    Assignment f addl -> a)
-> a
forall (ys :: Ctx k).
Assignment f ys
-> Int
-> (forall (addl :: Ctx k).
    (ys ~ (prefix <+> addl)) =>
    Assignment f addl -> a)
-> a
go Assignment f xs
xs0 (Size xs -> Int
forall k (ctx :: Ctx k). Size ctx -> Int
sizeInt (Assignment f xs -> Size xs
forall k (f :: k -> *) (ctx :: Ctx k). Assignment f ctx -> Size ctx
size Assignment f xs
xs0))
  where
  sz_prefix :: Int
sz_prefix = Size prefix -> Int
forall k (ctx :: Ctx k). Size ctx -> Int
sizeInt (Assignment f prefix -> Size prefix
forall k (f :: k -> *) (ctx :: Ctx k). Assignment f ctx -> Size ctx
size Assignment f prefix
prefix)

  go :: forall ys.
   Assignment f ys ->
   Int ->
   (forall addl. (ys ~ (prefix <+> addl)) => Assignment f addl -> a) ->
   a

  go :: Assignment f ys
-> Int
-> (forall (addl :: Ctx k).
    (ys ~ (prefix <+> addl)) =>
    Assignment f addl -> a)
-> a
go (Assignment f ctx
xs' :> f tp
z) Int
sz_x forall (addl :: Ctx k).
(ys ~ (prefix <+> addl)) =>
Assignment f addl -> a
success | Int
sz_x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
sz_prefix =
    Assignment f ctx
-> Int
-> (forall (addl :: Ctx k).
    (ctx ~ (prefix <+> addl)) =>
    Assignment f addl -> a)
-> a
forall (ys :: Ctx k).
Assignment f ys
-> Int
-> (forall (addl :: Ctx k).
    (ys ~ (prefix <+> addl)) =>
    Assignment f addl -> a)
-> a
go Assignment f ctx
xs' (Int
sz_xInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (\Assignment f addl
zs -> Assignment f (addl ::> tp) -> a
forall (addl :: Ctx k).
(ys ~ (prefix <+> addl)) =>
Assignment f addl -> a
success (Assignment f addl
zs Assignment f addl -> f tp -> Assignment f (addl ::> tp)
forall k (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> f tp
z))

  go Assignment f ys
xs Int
_ forall (addl :: Ctx k).
(ys ~ (prefix <+> addl)) =>
Assignment f addl -> a
success =
    case Assignment f ys -> Assignment f prefix -> Maybe (ys :~: prefix)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Assignment f ys
xs Assignment f prefix
prefix of
      Just ys :~: prefix
Refl -> Assignment f EmptyCtx -> a
forall (addl :: Ctx k).
(ys ~ (prefix <+> addl)) =>
Assignment f addl -> a
success Assignment f EmptyCtx
forall k (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty
      Maybe (ys :~: prefix)
Nothing   -> a
err

-- | Unzip an assignment of pairs into a pair of assignments.
--
-- This is the inverse of @'zipWith' 'Pair'@.
unzip :: Assignment (Product f g) ctx -> (Assignment f ctx, Assignment g ctx)
unzip :: Assignment (Product f g) ctx
-> (Assignment f ctx, Assignment g ctx)
unzip Assignment (Product f g) ctx
fgs =
  case Assignment (Product f g) ctx -> AssignView (Product f g) ctx
forall k (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
viewAssign Assignment (Product f g) ctx
fgs of
    AssignView (Product f g) ctx
AssignEmpty -> (Assignment f ctx
forall k (f :: k -> *). Assignment f EmptyCtx
empty, Assignment g ctx
forall k (f :: k -> *). Assignment f EmptyCtx
empty)
    AssignExtend Assignment (Product f g) ctx
rest (Pair f tp
f g tp
g) ->
      let (Assignment f ctx
fs, Assignment g ctx
gs) = Assignment (Product f g) ctx
-> (Assignment f ctx, Assignment g ctx)
forall k (f :: k -> *) (g :: k -> *) (ctx :: Ctx k).
Assignment (Product f g) ctx
-> (Assignment f ctx, Assignment g ctx)
unzip Assignment (Product f g) ctx
rest
      in (Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)
forall k (f :: k -> *) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
extend Assignment f ctx
fs f tp
f, Assignment g ctx -> g tp -> Assignment g (ctx ::> tp)
forall k (f :: k -> *) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
extend Assignment g ctx
gs g tp
g)

-- | Flattens a nested assignment over a context of contexts @ctxs :: Ctx (Ctx
-- a)@ into a flat assignment over the flattened context @CtxFlatten ctxs@.
flattenAssignment ::
  Assignment (Assignment f) ctxs ->
  Assignment f (CtxFlatten ctxs)
flattenAssignment :: Assignment (Assignment f) ctxs -> Assignment f (CtxFlatten ctxs)
flattenAssignment Assignment (Assignment f) ctxs
ctxs =
  case Assignment (Assignment f) ctxs -> AssignView (Assignment f) ctxs
forall k (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
viewAssign Assignment (Assignment f) ctxs
ctxs of
    AssignView (Assignment f) ctxs
AssignEmpty -> Assignment f (CtxFlatten ctxs)
forall k (f :: k -> *). Assignment f EmptyCtx
empty
    AssignExtend Assignment (Assignment f) ctx
ctxs' Assignment f tp
ctx -> Assignment (Assignment f) ctx -> Assignment f (CtxFlatten ctx)
forall a (f :: a -> *) (ctxs :: Ctx (Ctx a)).
Assignment (Assignment f) ctxs -> Assignment f (CtxFlatten ctxs)
flattenAssignment Assignment (Assignment f) ctx
ctxs' Assignment f (CtxFlatten ctx)
-> Assignment f tp -> Assignment f (CtxFlatten ctx <+> tp)
forall k (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
Assignment f x -> Assignment f y -> Assignment f (x <+> y)
<++> Assignment f tp
ctx

-- | Given the size of each context in @ctxs@, returns the size of @CtxFlatten
-- ctxs@.  You can obtain the former from any nested assignment @Assignment
-- (Assignment f) ctxs@, by calling @fmapFC size@.
flattenSize ::
  Assignment Size ctxs ->
  Size (CtxFlatten ctxs)
flattenSize :: Assignment Size ctxs -> Size (CtxFlatten ctxs)
flattenSize Assignment Size ctxs
a =
  case Assignment Size ctxs -> AssignView Size ctxs
forall k (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
viewAssign Assignment Size ctxs
a of
    AssignView Size ctxs
AssignEmpty -> Size (CtxFlatten ctxs)
forall k. Size 'EmptyCtx
zeroSize
    AssignExtend Assignment Size ctx
b Size tp
s -> Size (CtxFlatten ctx) -> Size tp -> Size (CtxFlatten ctx <+> tp)
forall k (x :: Ctx k) (y :: Ctx k).
Size x -> Size y -> Size (x <+> y)
addSize (Assignment Size ctx -> Size (CtxFlatten ctx)
forall k (ctxs :: Ctx (Ctx k)).
Assignment Size ctxs -> Size (CtxFlatten ctxs)
flattenSize Assignment Size ctx
b) Size tp
s


--------------------------------------------------------------------------------
-- Patterns

-- | Pattern synonym for the empty assignment
pattern Empty :: () => ctx ~ EmptyCtx => Assignment f ctx
pattern $bEmpty :: Assignment f ctx
$mEmpty :: forall r k (ctx :: Ctx k) (f :: k -> *).
Assignment f ctx -> ((ctx ~ EmptyCtx) => r) -> (Void# -> r) -> r
Empty <- (viewAssign -> AssignEmpty)
  where Empty = Assignment f ctx
forall k (f :: k -> *). Assignment f EmptyCtx
empty

infixl :>

-- | Pattern synonym for extending an assignment on the right
pattern (:>) :: () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx'
pattern $b:> :: Assignment f ctx -> f tp -> Assignment f ctx'
$m:> :: forall r k (ctx' :: Ctx k) (f :: k -> *).
Assignment f ctx'
-> (forall (ctx :: Ctx k) (tp :: k).
    (ctx' ~ (ctx ::> tp)) =>
    Assignment f ctx -> f tp -> r)
-> (Void# -> r)
-> r
(:>) a v <- (viewAssign -> AssignExtend a v)
  where Assignment f ctx
a :> f tp
v = Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)
forall k (f :: k -> *) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
extend Assignment f ctx
a f tp
v

{-# COMPLETE (:>), Empty :: Assignment  #-}

--------------------------------------------------------------------------------
-- Views

-- | Return true if assignment is empty.
null :: Assignment f ctx -> Bool
null :: Assignment f ctx -> Bool
null Assignment f ctx
a =
  case Assignment f ctx -> AssignView f ctx
forall k (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
viewAssign Assignment f ctx
a of
    AssignView f ctx
AssignEmpty -> Bool
True
    AssignExtend{} -> Bool
False

decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)
decompose :: Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)
decompose Assignment f (ctx ::> tp)
x = (Assignment f (ctx ::> tp) -> Assignment f ctx
forall k (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f (ctx '::> tp) -> Assignment f ctx
Data.Parameterized.Context.init Assignment f (ctx ::> tp)
x, Assignment f (ctx ::> tp) -> f tp
forall k (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f (ctx '::> tp) -> f tp
Data.Parameterized.Context.last Assignment f (ctx ::> tp)
x)

-- | Return assignment with all but the last block.
init :: Assignment f (ctx '::> tp) -> Assignment f ctx
init :: Assignment f (ctx '::> tp) -> Assignment f ctx
init Assignment f (ctx '::> tp)
x =
  case Assignment f (ctx '::> tp) -> AssignView f (ctx '::> tp)
forall k (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
viewAssign Assignment f (ctx '::> tp)
x of
    AssignExtend Assignment f ctx
t f tp
_ -> Assignment f ctx
Assignment f ctx
t

-- | Return the last element in the assignment.
last :: Assignment f (ctx '::> tp) -> f tp
last :: Assignment f (ctx '::> tp) -> f tp
last Assignment f (ctx '::> tp)
x =
  case Assignment f (ctx '::> tp) -> AssignView f (ctx '::> tp)
forall k (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
viewAssign Assignment f (ctx '::> tp)
x of
    AssignExtend Assignment f ctx
_ f tp
e -> f tp
f tp
e

{-# DEPRECATED view "Use viewAssign or the Empty and :> patterns instead." #-}
-- | View an assignment as either empty or an assignment with one appended.
view :: forall f ctx . Assignment f ctx -> AssignView f ctx
view :: Assignment f ctx -> AssignView f ctx
view = Assignment f ctx -> AssignView f ctx
forall k (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
viewAssign

-- | Return the prefix of an appended 'Assignment'
take :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx
take :: Size ctx
-> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx
take Size ctx
sz Size ctx'
sz' Assignment f (ctx <+> ctx')
asgn =
  let diff :: Diff ctx (ctx <+> ctx')
diff = Size ctx' -> Diff ctx (ctx <+> ctx')
forall k (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
appendDiff Size ctx'
sz' in
  Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
forall k (ctx :: Ctx k) (f :: k -> *).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
generate Size ctx
sz (\Index ctx tp
i -> Assignment f (ctx <+> ctx')
asgn Assignment f (ctx <+> ctx') -> Index (ctx <+> ctx') tp -> f tp
forall k (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Diff ctx (ctx <+> ctx') -> Index ctx tp -> Index (ctx <+> ctx') tp
forall k (l :: Ctx k) (r :: Ctx k) (tp :: k).
Diff l r -> Index l tp -> Index r tp
extendIndex' Diff ctx (ctx <+> ctx')
diff Index ctx tp
i)

-- | Return the suffix of an appended 'Assignment'
drop :: forall f ctx ctx'. Size ctx -> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx'
drop :: Size ctx
-> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx'
drop Size ctx
sz Size ctx'
sz' Assignment f (ctx <+> ctx')
asgn = Size ctx'
-> (forall (tp :: k). Index ctx' tp -> f tp) -> Assignment f ctx'
forall k (ctx :: Ctx k) (f :: k -> *).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
generate Size ctx'
sz' (\Index ctx' tp
i -> Assignment f (ctx <+> ctx')
asgn Assignment f (ctx <+> ctx') -> Index (ctx <+> ctx') tp -> f tp
forall k (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Size ctx -> Size ctx' -> Index ctx' tp -> Index (ctx <+> ctx') tp
forall k (l :: Ctx k) (r :: Ctx k) (tp :: k).
Size l -> Size r -> Index r tp -> Index (l <+> r) tp
extendIndexAppendLeft Size ctx
sz Size ctx'
sz' Index ctx' tp
i)

--------------------------------------------------------------------------------
-- Context embedding.

-- | This datastructure contains a proof that the first context is
-- embeddable in the second.  This is useful if we want to add extend
-- an existing term under a larger context.

data CtxEmbedding (ctx :: Ctx k) (ctx' :: Ctx k)
  = CtxEmbedding { CtxEmbedding ctx ctx' -> Size ctx'
_ctxeSize       :: Size ctx'
                 , CtxEmbedding ctx ctx' -> Assignment (Index ctx') ctx
_ctxeAssignment :: Assignment (Index ctx') ctx
                 }

-- Alternate encoding?
-- data CtxEmbedding ctx ctx' where
--   EIdentity  :: CtxEmbedding ctx ctx
--   ExtendBoth :: CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
--   ExtendOne  :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)

ctxeSize :: Simple Lens (CtxEmbedding ctx ctx') (Size ctx')
ctxeSize :: (Size ctx' -> f (Size ctx'))
-> CtxEmbedding ctx ctx' -> f (CtxEmbedding ctx ctx')
ctxeSize = (CtxEmbedding ctx ctx' -> Size ctx')
-> (CtxEmbedding ctx ctx' -> Size ctx' -> CtxEmbedding ctx ctx')
-> Lens
     (CtxEmbedding ctx ctx')
     (CtxEmbedding ctx ctx')
     (Size ctx')
     (Size ctx')
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens CtxEmbedding ctx ctx' -> Size ctx'
forall k (ctx :: Ctx k) (ctx' :: Ctx k).
CtxEmbedding ctx ctx' -> Size ctx'
_ctxeSize (\CtxEmbedding ctx ctx'
s Size ctx'
v -> CtxEmbedding ctx ctx'
s { _ctxeSize :: Size ctx'
_ctxeSize = Size ctx'
v })

ctxeAssignment :: Lens (CtxEmbedding ctx1 ctx') (CtxEmbedding ctx2 ctx')
                       (Assignment (Index ctx') ctx1) (Assignment (Index ctx') ctx2)
ctxeAssignment :: (Assignment (Index ctx') ctx1 -> f (Assignment (Index ctx') ctx2))
-> CtxEmbedding ctx1 ctx' -> f (CtxEmbedding ctx2 ctx')
ctxeAssignment = (CtxEmbedding ctx1 ctx' -> Assignment (Index ctx') ctx1)
-> (CtxEmbedding ctx1 ctx'
    -> Assignment (Index ctx') ctx2 -> CtxEmbedding ctx2 ctx')
-> Lens
     (CtxEmbedding ctx1 ctx')
     (CtxEmbedding ctx2 ctx')
     (Assignment (Index ctx') ctx1)
     (Assignment (Index ctx') ctx2)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens CtxEmbedding ctx1 ctx' -> Assignment (Index ctx') ctx1
forall k (ctx :: Ctx k) (ctx' :: Ctx k).
CtxEmbedding ctx ctx' -> Assignment (Index ctx') ctx
_ctxeAssignment (\CtxEmbedding ctx1 ctx'
s Assignment (Index ctx') ctx2
v -> CtxEmbedding ctx1 ctx'
s { _ctxeAssignment :: Assignment (Index ctx') ctx2
_ctxeAssignment = Assignment (Index ctx') ctx2
v })

class ApplyEmbedding (f :: Ctx k -> Type) where
  applyEmbedding :: CtxEmbedding ctx ctx' -> f ctx -> f ctx'

class ApplyEmbedding' (f :: Ctx k -> k' -> Type) where
  applyEmbedding' :: CtxEmbedding ctx ctx' -> f ctx v -> f ctx' v

class ExtendContext (f :: Ctx k -> Type) where
  extendContext :: Diff ctx ctx' -> f ctx -> f ctx'

class ExtendContext' (f :: Ctx k -> k' -> Type) where
  extendContext' :: Diff ctx ctx' -> f ctx v -> f ctx' v

instance ApplyEmbedding' Index where
  applyEmbedding' :: CtxEmbedding ctx ctx' -> Index ctx v -> Index ctx' v
applyEmbedding' CtxEmbedding ctx ctx'
ctxe Index ctx v
idx = (CtxEmbedding ctx ctx'
ctxe CtxEmbedding ctx ctx'
-> Getting
     (Assignment (Index ctx') ctx)
     (CtxEmbedding ctx ctx')
     (Assignment (Index ctx') ctx)
-> Assignment (Index ctx') ctx
forall s a. s -> Getting a s a -> a
^. Getting
  (Assignment (Index ctx') ctx)
  (CtxEmbedding ctx ctx')
  (Assignment (Index ctx') ctx)
forall k (ctx1 :: Ctx k) (ctx' :: Ctx k) (ctx2 :: Ctx k).
Lens
  (CtxEmbedding ctx1 ctx')
  (CtxEmbedding ctx2 ctx')
  (Assignment (Index ctx') ctx1)
  (Assignment (Index ctx') ctx2)
ctxeAssignment) Assignment (Index ctx') ctx -> Index ctx v -> Index ctx' v
forall k (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Index ctx v
idx

instance ExtendContext' Index where
  extendContext' :: Diff ctx ctx' -> Index ctx v -> Index ctx' v
extendContext' = Diff ctx ctx' -> Index ctx v -> Index ctx' v
forall k (l :: Ctx k) (r :: Ctx k) (tp :: k).
Diff l r -> Index l tp -> Index r tp
extendIndex'

-- -- This is the inefficient way of doing things.  A better way is to
-- -- just have a map between indices.
-- applyEmbedding :: CtxEmbedding ctx ctx'
--                -> Index ctx tp -> Index ctx' tp
-- applyEmbedding ctxe idx = (ctxe ^. ctxeAssignment) ! idx

identityEmbedding :: Size ctx -> CtxEmbedding ctx ctx
identityEmbedding :: Size ctx -> CtxEmbedding ctx ctx
identityEmbedding Size ctx
sz = Size ctx -> Assignment (Index ctx) ctx -> CtxEmbedding ctx ctx
forall k (ctx :: Ctx k) (ctx' :: Ctx k).
Size ctx' -> Assignment (Index ctx') ctx -> CtxEmbedding ctx ctx'
CtxEmbedding Size ctx
sz (Size ctx
-> (forall (tp :: k). Index ctx tp -> Index ctx tp)
-> Assignment (Index ctx) ctx
forall k (ctx :: Ctx k) (f :: k -> *).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
generate Size ctx
sz forall (tp :: k). Index ctx tp -> Index ctx tp
forall a. a -> a
id)

-- emptyEmbedding :: CtxEmbedding EmptyCtx EmptyCtx
-- emptyEmbedding = identityEmbedding knownSize

extendEmbeddingRightDiff :: forall ctx ctx' ctx''.
                            Diff ctx' ctx''
                            -> CtxEmbedding ctx ctx'
                            -> CtxEmbedding ctx ctx''
extendEmbeddingRightDiff :: Diff ctx' ctx'' -> CtxEmbedding ctx ctx' -> CtxEmbedding ctx ctx''
extendEmbeddingRightDiff Diff ctx' ctx''
diff (CtxEmbedding Size ctx'
sz' Assignment (Index ctx') ctx
assgn) = Size ctx''
-> Assignment (Index ctx'') ctx -> CtxEmbedding ctx ctx''
forall k (ctx :: Ctx k) (ctx' :: Ctx k).
Size ctx' -> Assignment (Index ctx') ctx -> CtxEmbedding ctx ctx'
CtxEmbedding (Size ctx' -> Diff ctx' ctx'' -> Size ctx''
forall k (l :: Ctx k) (r :: Ctx k). Size l -> Diff l r -> Size r
extSize Size ctx'
sz' Diff ctx' ctx''
diff) Assignment (Index ctx'') ctx
updated
  where
    updated :: Assignment (Index ctx'') ctx
    updated :: Assignment (Index ctx'') ctx
updated = (forall (x :: k). Index ctx' x -> Index ctx'' x)
-> Assignment (Index ctx') ctx -> Assignment (Index ctx'') ctx
forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
fmapFC (Diff ctx' ctx'' -> Index ctx' x -> Index ctx'' x
forall k (l :: Ctx k) (r :: Ctx k) (tp :: k).
Diff l r -> Index l tp -> Index r tp
extendIndex' Diff ctx' ctx''
diff) Assignment (Index ctx') ctx
assgn

extendEmbeddingRight :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
extendEmbeddingRight :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
extendEmbeddingRight = Diff ctx' (ctx' ::> tp)
-> CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
forall k (ctx :: Ctx k) (ctx' :: Ctx k) (ctx'' :: Ctx k).
Diff ctx' ctx'' -> CtxEmbedding ctx ctx' -> CtxEmbedding ctx ctx''
extendEmbeddingRightDiff Diff ctx' (ctx' ::> tp)
forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
knownDiff

-- | Prove that the prefix of an appended context is embeddable in it
appendEmbedding :: Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx')
appendEmbedding :: Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx')
appendEmbedding Size ctx
sz Size ctx'
sz' = Size (ctx <+> ctx')
-> Assignment (Index (ctx <+> ctx')) ctx
-> CtxEmbedding ctx (ctx <+> ctx')
forall k (ctx :: Ctx k) (ctx' :: Ctx k).
Size ctx' -> Assignment (Index ctx') ctx -> CtxEmbedding ctx ctx'
CtxEmbedding (Size ctx -> Size ctx' -> Size (ctx <+> ctx')
forall k (x :: Ctx k) (y :: Ctx k).
Size x -> Size y -> Size (x <+> y)
addSize Size ctx
sz Size ctx'
sz') (Size ctx
-> (forall (tp :: k). Index ctx tp -> Index (ctx <+> ctx') tp)
-> Assignment (Index (ctx <+> ctx')) ctx
forall k (ctx :: Ctx k) (f :: k -> *).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
generate Size ctx
sz (Diff ctx (ctx <+> ctx') -> Index ctx tp -> Index (ctx <+> ctx') tp
forall k (l :: Ctx k) (r :: Ctx k) (tp :: k).
Diff l r -> Index l tp -> Index r tp
extendIndex' Diff ctx (ctx <+> ctx')
diff))
  where
  diff :: Diff ctx (ctx <+> ctx')
diff = Size ctx' -> Diff ctx (ctx <+> ctx')
forall k (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
appendDiff Size ctx'
sz'

-- | Prove that the suffix of an appended context is embeddable in it
appendEmbeddingLeft :: Size ctx -> Size ctx' -> CtxEmbedding ctx' (ctx <+> ctx')
appendEmbeddingLeft :: Size ctx -> Size ctx' -> CtxEmbedding ctx' (ctx <+> ctx')
appendEmbeddingLeft Size ctx
sz Size ctx'
sz' = Size (ctx <+> ctx')
-> Assignment (Index (ctx <+> ctx')) ctx'
-> CtxEmbedding ctx' (ctx <+> ctx')
forall k (ctx :: Ctx k) (ctx' :: Ctx k).
Size ctx' -> Assignment (Index ctx') ctx -> CtxEmbedding ctx ctx'
CtxEmbedding (Size ctx -> Size ctx' -> Size (ctx <+> ctx')
forall k (x :: Ctx k) (y :: Ctx k).
Size x -> Size y -> Size (x <+> y)
addSize Size ctx
sz Size ctx'
sz') (Size ctx'
-> (forall (tp :: k). Index ctx' tp -> Index (ctx <+> ctx') tp)
-> Assignment (Index (ctx <+> ctx')) ctx'
forall k (ctx :: Ctx k) (f :: k -> *).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
generate Size ctx'
sz' (Size ctx -> Size ctx' -> Index ctx' tp -> Index (ctx <+> ctx') tp
forall k (l :: Ctx k) (r :: Ctx k) (tp :: k).
Size l -> Size r -> Index r tp -> Index (l <+> r) tp
extendIndexAppendLeft Size ctx
sz Size ctx'
sz'))

extendEmbeddingBoth :: forall ctx ctx' tp. CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
extendEmbeddingBoth :: CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
extendEmbeddingBoth CtxEmbedding ctx ctx'
ctxe = CtxEmbedding ctx (ctx' ::> tp)
updated CtxEmbedding ctx (ctx' ::> tp)
-> (CtxEmbedding ctx (ctx' ::> tp)
    -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp))
-> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
forall a b. a -> (a -> b) -> b
& (Assignment (Index (ctx' ::> tp)) ctx
 -> Identity (Assignment (Index (ctx' ::> tp)) (ctx ::> tp)))
-> CtxEmbedding ctx (ctx' ::> tp)
-> Identity (CtxEmbedding (ctx ::> tp) (ctx' ::> tp))
forall k (ctx1 :: Ctx k) (ctx' :: Ctx k) (ctx2 :: Ctx k).
Lens
  (CtxEmbedding ctx1 ctx')
  (CtxEmbedding ctx2 ctx')
  (Assignment (Index ctx') ctx1)
  (Assignment (Index ctx') ctx2)
ctxeAssignment ((Assignment (Index (ctx' ::> tp)) ctx
  -> Identity (Assignment (Index (ctx' ::> tp)) (ctx ::> tp)))
 -> CtxEmbedding ctx (ctx' ::> tp)
 -> Identity (CtxEmbedding (ctx ::> tp) (ctx' ::> tp)))
-> (Assignment (Index (ctx' ::> tp)) ctx
    -> Assignment (Index (ctx' ::> tp)) (ctx ::> tp))
-> CtxEmbedding ctx (ctx' ::> tp)
-> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Assignment (Index (ctx' ::> tp)) ctx
 -> Index (ctx' ::> tp) tp
 -> Assignment (Index (ctx' ::> tp)) (ctx ::> tp))
-> Index (ctx' ::> tp) tp
-> Assignment (Index (ctx' ::> tp)) ctx
-> Assignment (Index (ctx' ::> tp)) (ctx ::> tp)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Assignment (Index (ctx' ::> tp)) ctx
-> Index (ctx' ::> tp) tp
-> Assignment (Index (ctx' ::> tp)) (ctx ::> tp)
forall k (f :: k -> *) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
extend (Size ctx' -> Index (ctx' ::> tp) tp
forall k (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex (CtxEmbedding ctx ctx'
ctxe CtxEmbedding ctx ctx'
-> Getting (Size ctx') (CtxEmbedding ctx ctx') (Size ctx')
-> Size ctx'
forall s a. s -> Getting a s a -> a
^. Getting (Size ctx') (CtxEmbedding ctx ctx') (Size ctx')
forall k (ctx :: Ctx k) (ctx' :: Ctx k).
Simple Lens (CtxEmbedding ctx ctx') (Size ctx')
ctxeSize))
  where
    updated :: CtxEmbedding ctx (ctx' ::> tp)
    updated :: CtxEmbedding ctx (ctx' ::> tp)
updated = CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
forall k (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k).
CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
extendEmbeddingRight CtxEmbedding ctx ctx'
ctxe

--------------------------------------------------------------------------------
-- Static indexing based on type-level naturals

-- | Get a lens for an position in an 'Assignment' by zero-based, left-to-right position.
-- The position must be specified using @TypeApplications@ for the @n@ parameter.
field :: forall n ctx f r. Idx n ctx r => Lens' (Assignment f ctx) (f r)
field :: Lens' (Assignment f ctx) (f r)
field = IndexF (Assignment f ctx) r
-> Lens' (Assignment f ctx) (IxValueF (Assignment f ctx) r)
forall k m (x :: k).
IxedF' k m =>
IndexF m x -> Lens' m (IxValueF m x)
ixF' (forall k (n :: Nat) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
forall (ctx :: Ctx k) (r :: k). Idx n ctx r => Index ctx r
natIndex @n)

-- | Constraint synonym used for getting an 'Index' into a 'Ctx'.
-- @n@ is the zero-based, left-counted index into the list of types
-- @ctx@ which has the type @r@.
type Idx n ctx r = (ValidIx n ctx, Idx' (FromLeft ctx n) ctx r)

-- | Compute an 'Index' value for a particular position in a 'Ctx'. The
-- @TypeApplications@ extension will be needed to disambiguate the choice
-- of the type @n@.
natIndex :: forall n ctx r. Idx n ctx r => Index ctx r
natIndex :: Index ctx r
natIndex = forall k (n :: Nat) (ctx :: Ctx k) (r :: k).
Idx' n ctx r =>
Index ctx r
forall (ctx :: Ctx k) (r :: k).
Idx' (FromLeft ctx n) ctx r =>
Index ctx r
natIndex' @_ @(FromLeft ctx n)

-- | This version of 'natIndex' is suitable for use without the @TypeApplications@
-- extension.
natIndexProxy :: forall n ctx r proxy. Idx n ctx r => proxy n -> Index ctx r
natIndexProxy :: proxy n -> Index ctx r
natIndexProxy proxy n
_ = forall k (n :: Nat) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
forall (ctx :: Ctx k) (r :: k). Idx n ctx r => Index ctx r
natIndex @n

------------------------------------------------------------------------
-- Implementation
------------------------------------------------------------------------

-- | Class for computing 'Index' values for positions in a 'Ctx'.
class KnownContext ctx => Idx' (n :: Nat) (ctx :: Ctx k) (r :: k) | n ctx -> r where
  natIndex' :: Index ctx r

-- | Base-case
instance KnownContext xs => Idx' 0 (xs '::> x) x where
  natIndex' :: Index (xs '::> x) x
natIndex' = Size (xs '::> x) -> Index (xs '::> x) x
forall k (ctx :: Ctx k) (tp :: k).
Size (ctx ::> tp) -> Index (ctx ::> tp) tp
lastIndex Size (xs '::> x)
forall k (ctx :: Ctx k). KnownContext ctx => Size ctx
knownSize

-- | Inductive-step
instance {-# Overlaps #-} (KnownContext xs, Idx' (n-1) xs r) =>
  Idx' n (xs '::> x) r where

  natIndex' :: Index (xs '::> x) r
natIndex' = Index xs r -> Index (xs '::> x) r
forall k (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex (forall k (n :: Nat) (ctx :: Ctx k) (r :: k).
Idx' n ctx r =>
Index ctx r
forall (ctx :: Ctx k) (r :: k). Idx' (n - 1) ctx r => Index ctx r
natIndex' @_ @(n-1))


--------------------------------------------------------------------------------
-- * CurryAssignment

-- | This type family is used to define currying\/uncurrying operations
-- on assignments.  It is best understood by seeing its evaluation on
-- several examples:
--
-- > CurryAssignment EmptyCtx f x = x
-- > CurryAssignment (EmptyCtx ::> a) f x = f a -> x
-- > CurryAssignment (EmptyCtx ::> a ::> b) f x = f a -> f b -> x
-- > CurryAssignment (EmptyCtx ::> a ::> b ::> c) f x = f a -> f b -> f c -> x
type family CurryAssignment (ctx :: Ctx k) (f :: k -> Type) (x :: Type) :: Type where
   CurryAssignment EmptyCtx    f x = x
   CurryAssignment (ctx ::> a) f x = CurryAssignment ctx f (f a -> x)

-- | This class implements two methods that witness the isomorphism between
--   curried and uncurried functions.
class CurryAssignmentClass (ctx :: Ctx k) where

  -- | Transform a function that accepts an assignment into one with a separate
  --   variable for each element of the assignment.
  curryAssignment   :: (Assignment f ctx -> x) -> CurryAssignment ctx f x

  -- | Transform a curried function into one that accepts an assignment value.
  uncurryAssignment :: CurryAssignment ctx f x -> (Assignment f ctx -> x)

instance CurryAssignmentClass EmptyCtx where
  curryAssignment :: (Assignment f EmptyCtx -> x) -> CurryAssignment EmptyCtx f x
curryAssignment Assignment f EmptyCtx -> x
k = Assignment f EmptyCtx -> x
k Assignment f EmptyCtx
forall k (f :: k -> *). Assignment f EmptyCtx
empty
  uncurryAssignment :: CurryAssignment EmptyCtx f x -> Assignment f EmptyCtx -> x
uncurryAssignment CurryAssignment EmptyCtx f x
k Assignment f EmptyCtx
_ = x
CurryAssignment EmptyCtx f x
k

instance CurryAssignmentClass ctx => CurryAssignmentClass (ctx ::> a) where
  curryAssignment :: (Assignment f (ctx ::> a) -> x) -> CurryAssignment (ctx ::> a) f x
curryAssignment Assignment f (ctx ::> a) -> x
k = (Assignment f ctx -> f a -> x) -> CurryAssignment ctx f (f a -> x)
forall k (ctx :: Ctx k) (f :: k -> *) x.
CurryAssignmentClass ctx =>
(Assignment f ctx -> x) -> CurryAssignment ctx f x
curryAssignment (\Assignment f ctx
asgn f a
a -> Assignment f (ctx ::> a) -> x
k (Assignment f ctx
asgn Assignment f ctx -> f a -> Assignment f (ctx ::> a)
forall k (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> f a
a))
  uncurryAssignment :: CurryAssignment (ctx ::> a) f x -> Assignment f (ctx ::> a) -> x
uncurryAssignment CurryAssignment (ctx ::> a) f x
k Assignment f (ctx ::> a)
asgn =
    case Assignment f (ctx ::> a) -> AssignView f (ctx ::> a)
forall k (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
viewAssign Assignment f (ctx ::> a)
asgn of
      AssignExtend Assignment f ctx
asgn' f tp
x -> CurryAssignment ctx f (f tp -> x) -> Assignment f ctx -> f tp -> x
forall k (ctx :: Ctx k) (f :: k -> *) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment CurryAssignment ctx f (f tp -> x)
CurryAssignment (ctx ::> a) f x
k Assignment f ctx
asgn' f tp
x

-- | Create an assignment from a list of values.
fromList :: [Some f] -> Some (Assignment f)
fromList :: [Some f] -> Some (Assignment f)
fromList = Assignment f EmptyCtx -> [Some f] -> Some (Assignment f)
forall k (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> [Some f] -> Some (Assignment f)
go Assignment f EmptyCtx
forall k (f :: k -> *). Assignment f EmptyCtx
empty
  where go :: Assignment f ctx -> [Some f] -> Some (Assignment f)
        go :: Assignment f ctx -> [Some f] -> Some (Assignment f)
go Assignment f ctx
prev [] = Assignment f ctx -> Some (Assignment f)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some Assignment f ctx
prev
        go Assignment f ctx
prev (Some f x
g:[Some f]
next) = (Assignment f (ctx ::> x) -> [Some f] -> Some (Assignment f)
forall k (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> [Some f] -> Some (Assignment f)
go (Assignment f (ctx ::> x) -> [Some f] -> Some (Assignment f))
-> Assignment f (ctx ::> x) -> [Some f] -> Some (Assignment f)
forall a b. (a -> b) -> a -> b
$! Assignment f ctx
prev Assignment f ctx -> f x -> Assignment f (ctx ::> x)
forall k (f :: k -> *) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
`extend` f x
g) [Some f]
next


newtype Collector m w a = Collector { Collector m w a -> m w
runCollector :: m w }
instance Functor (Collector m w) where
  fmap :: (a -> b) -> Collector m w a -> Collector m w b
fmap a -> b
_ (Collector m w
x) = m w -> Collector m w b
forall k k (m :: k -> *) (w :: k) (a :: k). m w -> Collector m w a
Collector m w
x
instance (Applicative m, Monoid w) => Applicative (Collector m w) where
  pure :: a -> Collector m w a
pure a
_ = m w -> Collector m w a
forall k k (m :: k -> *) (w :: k) (a :: k). m w -> Collector m w a
Collector (w -> m w
forall (f :: * -> *) a. Applicative f => a -> f a
pure w
forall a. Monoid a => a
mempty)
  Collector m w
x <*> :: Collector m w (a -> b) -> Collector m w a -> Collector m w b
<*> Collector m w
y = m w -> Collector m w b
forall k k (m :: k -> *) (w :: k) (a :: k). m w -> Collector m w a
Collector ((w -> w -> w) -> m w -> m w -> m w
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 w -> w -> w
forall a. Semigroup a => a -> a -> a
(<>) m w
x m w
y)

-- | Visit each of the elements in an @Assignment@ in order
--   from left to right and collect the results using the provided @Monoid@.
traverseAndCollect ::
  (Monoid w, Applicative m) =>
  (forall tp. Index ctx tp -> f tp -> m w) ->
  Assignment f ctx ->
  m w
traverseAndCollect :: (forall (tp :: k). Index ctx tp -> f tp -> m w)
-> Assignment f ctx -> m w
traverseAndCollect forall (tp :: k). Index ctx tp -> f tp -> m w
f =
  Collector m w (Assignment Any ctx) -> m w
forall k (m :: k -> *) (w :: k) k (a :: k). Collector m w a -> m w
runCollector (Collector m w (Assignment Any ctx) -> m w)
-> (Assignment f ctx -> Collector m w (Assignment Any ctx))
-> Assignment f ctx
-> m w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (tp :: k). Index ctx tp -> f tp -> Collector m w (Any tp))
-> Assignment f ctx -> Collector m w (Assignment Any ctx)
forall k (m :: * -> *) (ctx :: Ctx k) (f :: k -> *) (g :: k -> *).
Applicative m =>
(forall (tp :: k). Index ctx tp -> f tp -> m (g tp))
-> Assignment f ctx -> m (Assignment g ctx)
traverseWithIndex (\Index ctx tp
i f tp
x -> m w -> Collector m w (Any tp)
forall k k (m :: k -> *) (w :: k) (a :: k). m w -> Collector m w a
Collector (Index ctx tp -> f tp -> m w
forall (tp :: k). Index ctx tp -> f tp -> m w
f Index ctx tp
i f tp
x))

-- | Visit each of the elements in an @Assignment@ in order
--   from left to right, executing an action with each.
traverseWithIndex_ :: Applicative m
                   => (forall tp . Index ctx tp -> f tp -> m ())
                   -> Assignment f ctx
                   -> m ()
traverseWithIndex_ :: (forall (tp :: k). Index ctx tp -> f tp -> m ())
-> Assignment f ctx -> m ()
traverseWithIndex_ forall (tp :: k). Index ctx tp -> f tp -> m ()
f = m () -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m () -> m ())
-> (Assignment f ctx -> m ()) -> Assignment f ctx -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (tp :: k). Index ctx tp -> f tp -> m ())
-> Assignment f ctx -> m ()
forall k w (m :: * -> *) (ctx :: Ctx k) (f :: k -> *).
(Monoid w, Applicative m) =>
(forall (tp :: k). Index ctx tp -> f tp -> m w)
-> Assignment f ctx -> m w
traverseAndCollect forall (tp :: k). Index ctx tp -> f tp -> m ()
f

--------------------------------------------------------------------------------
-- Size and Index values

size1 :: Size (EmptyCtx ::> a)
size1 :: Size (EmptyCtx ::> a)
size1 = Size EmptyCtx -> Size (EmptyCtx ::> a)
forall k (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size EmptyCtx
forall k. Size 'EmptyCtx
zeroSize

size2 :: Size (EmptyCtx ::> a ::> b)
size2 :: Size ((EmptyCtx ::> a) ::> b)
size2 = Size (EmptyCtx ::> a) -> Size ((EmptyCtx ::> a) ::> b)
forall k (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size (EmptyCtx ::> a)
forall k (a :: k). Size (EmptyCtx ::> a)
size1

size3 :: Size (EmptyCtx ::> a ::> b ::> c)
size3 :: Size (((EmptyCtx ::> a) ::> b) ::> c)
size3 = Size ((EmptyCtx ::> a) ::> b)
-> Size (((EmptyCtx ::> a) ::> b) ::> c)
forall k (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ((EmptyCtx ::> a) ::> b)
forall k (a :: k) (b :: k). Size ((EmptyCtx ::> a) ::> b)
size2

size4 :: Size (EmptyCtx ::> a ::> b ::> c ::> d)
size4 :: Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
size4 = Size (((EmptyCtx ::> a) ::> b) ::> c)
-> Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
forall k (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size (((EmptyCtx ::> a) ::> b) ::> c)
forall k (a :: k) (b :: k) (c :: k).
Size (((EmptyCtx ::> a) ::> b) ::> c)
size3

size5 :: Size (EmptyCtx ::> a ::> b ::> c ::> d ::> e)
size5 :: Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
size5 = Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
-> Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
forall k (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
size4

size6 :: Size (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f)
size6 :: Size ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f)
size6 = Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
-> Size ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f)
forall k (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
forall k (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
size5

i1of2 :: Index (EmptyCtx ::> a ::> b) a
i1of2 :: Index ((EmptyCtx ::> a) ::> b) a
i1of2 = Index (EmptyCtx ::> a) a -> Index ((EmptyCtx ::> a) ::> b) a
forall k (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index (EmptyCtx ::> a) a
forall k (tp :: k). Index ('EmptyCtx '::> tp) tp
baseIndex

i2of2 :: Index (EmptyCtx ::> a ::> b) b
i2of2 :: Index ((EmptyCtx ::> a) ::> b) b
i2of2 = Size (EmptyCtx ::> a) -> Index ((EmptyCtx ::> a) ::> b) b
forall k (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size (EmptyCtx ::> a)
forall k (a :: k). Size (EmptyCtx ::> a)
size1

i1of3 :: Index (EmptyCtx ::> a ::> b ::> c) a
i1of3 :: Index (((EmptyCtx ::> a) ::> b) ::> c) a
i1of3 = Index ((EmptyCtx ::> a) ::> b) a
-> Index (((EmptyCtx ::> a) ::> b) ::> c) a
forall k (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index ((EmptyCtx ::> a) ::> b) a
forall k (a :: k) (b :: k). Index ((EmptyCtx ::> a) ::> b) a
i1of2

i2of3 :: Index (EmptyCtx ::> a ::> b ::> c) b
i2of3 :: Index (((EmptyCtx ::> a) ::> b) ::> c) b
i2of3 = Index ((EmptyCtx ::> a) ::> b) b
-> Index (((EmptyCtx ::> a) ::> b) ::> c) b
forall k (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index ((EmptyCtx ::> a) ::> b) b
forall k (a :: k) (b :: k). Index ((EmptyCtx ::> a) ::> b) b
i2of2

i3of3 :: Index (EmptyCtx ::> a ::> b ::> c) c
i3of3 :: Index (((EmptyCtx ::> a) ::> b) ::> c) c
i3of3 = Size ((EmptyCtx ::> a) ::> b)
-> Index (((EmptyCtx ::> a) ::> b) ::> c) c
forall k (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size ((EmptyCtx ::> a) ::> b)
forall k (a :: k) (b :: k). Size ((EmptyCtx ::> a) ::> b)
size2

i1of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) a
i1of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) a
i1of4 = Index (((EmptyCtx ::> a) ::> b) ::> c) a
-> Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) a
forall k (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index (((EmptyCtx ::> a) ::> b) ::> c) a
forall k (a :: k) (b :: k) (c :: k).
Index (((EmptyCtx ::> a) ::> b) ::> c) a
i1of3

i2of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) b
i2of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) b
i2of4 = Index (((EmptyCtx ::> a) ::> b) ::> c) b
-> Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) b
forall k (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index (((EmptyCtx ::> a) ::> b) ::> c) b
forall k (a :: k) (b :: k) (c :: k).
Index (((EmptyCtx ::> a) ::> b) ::> c) b
i2of3

i3of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) c
i3of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) c
i3of4 = Index (((EmptyCtx ::> a) ::> b) ::> c) c
-> Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) c
forall k (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index (((EmptyCtx ::> a) ::> b) ::> c) c
forall k (a :: k) (b :: k) (c :: k).
Index (((EmptyCtx ::> a) ::> b) ::> c) c
i3of3

i4of4 :: Index (EmptyCtx ::> a ::> b ::> c ::> d) d
i4of4 :: Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) d
i4of4 = Size (((EmptyCtx ::> a) ::> b) ::> c)
-> Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) d
forall k (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size (((EmptyCtx ::> a) ::> b) ::> c)
forall k (a :: k) (b :: k) (c :: k).
Size (((EmptyCtx ::> a) ::> b) ::> c)
size3

i1of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) a
i1of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) a
i1of5 = Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) a
-> Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) a
forall k (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) a
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) a
i1of4

i2of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) b
i2of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) b
i2of5 = Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) b
-> Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) b
forall k (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) b
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) b
i2of4

i3of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) c
i3of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) c
i3of5 = Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) c
-> Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) c
forall k (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) c
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) c
i3of4

i4of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) d
i4of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) d
i4of5 = Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) d
-> Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) d
forall k (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) d
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Index ((((EmptyCtx ::> a) ::> b) ::> c) ::> d) d
i4of4

i5of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) e
i5of5 :: Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) e
i5of5 = Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
-> Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) e
forall k (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
forall k (a :: k) (b :: k) (c :: k) (d :: k).
Size ((((EmptyCtx ::> a) ::> b) ::> c) ::> d)
size4

i1of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) a
i1of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) a
i1of6 = Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) a
-> Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) a
forall k (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) a
forall k (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) a
i1of5

i2of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) b
i2of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) b
i2of6 = Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) b
-> Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) b
forall k (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) b
forall k (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) b
i2of5

i3of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) c
i3of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) c
i3of6 = Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) c
-> Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) c
forall k (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) c
forall k (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) c
i3of5

i4of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) d
i4of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) d
i4of6 = Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) d
-> Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) d
forall k (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) d
forall k (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) d
i4of5

i5of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) e
i5of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) e
i5of6 = Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) e
-> Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) e
forall k (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) e
forall k (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) e
i5of5

i6of6 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e ::> f) f
i6of6 :: Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) f
i6of6 = Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
-> Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) f
forall k (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
forall k (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
size5