{-|
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 :: forall {k} (f :: k -> *) (tp :: k).
f tp -> Assignment f (EmptyCtx ::> tp)
singleton = (forall {k} (f :: k -> *). Assignment f EmptyCtx
empty 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 :: forall {k} (ctx :: Ctx k) (m :: * -> *).
Applicative m =>
Size ctx -> (forall (tp :: k). Index ctx tp -> m ()) -> m ()
forIndexM Size ctx
sz forall (tp :: k). Index ctx tp -> m ()
f = 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 -> forall (tp :: k). Index ctx tp -> m ()
f Index ctx tp
i forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> m ()
r) (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 :: forall {k} (f :: k -> *).
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 = forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall {k} (f :: k -> *). Assignment f EmptyCtx
empty
        go Int
i = (\(Some Assignment f x
a) (Some f x
e) -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some (Assignment f x
a 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
iforall a. Num a => a -> a -> a
-Int
1)) (Int -> Some f
f (Int
iforall 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 :: forall {k} (m :: * -> *) (f :: k -> *).
Applicative m =>
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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall {k} (f :: k -> *). Assignment f EmptyCtx
empty)
        go Int
i = (\(Some Assignment f x
a) (Some f x
e) -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some (Assignment f x
a forall {k} (f :: k -> *) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
`extend` f x
e)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m (Some (Assignment f))
go (Int
iforall a. Num a => a -> a -> a
-Int
1) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> m (Some f)
f (Int
iforall 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 :: forall {k} (f :: k -> *) (tps :: Ctx k) e.
Assignment f tps -> (forall (tp :: k). f tp -> e) -> Vector e
toVector Assignment f tps
a forall (tp :: k). f tp -> e
f = forall a. (forall s. ST s (MVector s a)) -> Vector a
V.create forall a b. (a -> b) -> a -> b
$ do
  MVector s e
vm <- forall (m :: * -> *) a.
PrimMonad m =>
Int -> m (MVector (PrimState m) a)
MV.new (forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt (forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size Assignment f tps
a))
  forall {k} (ctx :: Ctx k) (m :: * -> *).
Applicative m =>
Size ctx -> (forall (tp :: k). Index ctx tp -> m ()) -> m ()
forIndexM (forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size Assignment f tps
a) forall a b. (a -> b) -> a -> b
$ \Index tps tp
i -> do
    forall (m :: * -> *) a.
PrimMonad m =>
MVector (PrimState m) a -> Int -> a -> m ()
MV.write MVector s e
vm (forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
indexVal Index tps tp
i) (forall (tp :: k). f tp -> e
f (Assignment f tps
a forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Index tps tp
i))
  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 :: forall {k} (f :: k -> *) (xs :: Ctx k) (prefix :: Ctx k) a.
TestEquality f =>
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 = 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 (forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt (forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size Assignment f xs
xs0))
  where
  sz_prefix :: Int
sz_prefix = forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt (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 :: 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' :> f tp
z) Int
sz_x forall (addl :: Ctx k).
(ys ~ (prefix <+> addl)) =>
Assignment f addl -> a
success | Int
sz_x forall a. Ord a => a -> a -> Bool
> Int
sz_prefix =
    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_xforall a. Num a => a -> a -> a
-Int
1) (\Assignment f addl
zs -> forall (addl :: Ctx k).
(ys ~ (prefix <+> addl)) =>
Assignment f addl -> a
success (Assignment f addl
zs 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 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 -> forall (addl :: Ctx k).
(ys ~ (prefix <+> addl)) =>
Assignment f addl -> a
success 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 :: 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
fgs =
  case 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 -> (forall {k} (f :: k -> *). Assignment f EmptyCtx
empty, 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) = 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 (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, 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 :: forall {a} (f :: a -> *) (ctxs :: Ctx (Ctx a)).
Assignment (Assignment f) ctxs -> Assignment f (CtxFlatten ctxs)
flattenAssignment Assignment (Assignment f) ctxs
ctxs =
  case 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 -> forall {k} (f :: k -> *). Assignment f EmptyCtx
empty
    AssignExtend Assignment (Assignment f) ctx
ctxs' Assignment f tp
ctx -> forall {a} (f :: a -> *) (ctxs :: Ctx (Ctx a)).
Assignment (Assignment f) ctxs -> Assignment f (CtxFlatten ctxs)
flattenAssignment Assignment (Assignment f) ctx
ctxs' 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 :: forall {k} (ctxs :: Ctx (Ctx k)).
Assignment Size ctxs -> Size (CtxFlatten ctxs)
flattenSize Assignment Size ctxs
a =
  case forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
viewAssign Assignment Size ctxs
a of
    AssignView Size ctxs
AssignEmpty -> forall {k}. Size 'EmptyCtx
zeroSize
    AssignExtend Assignment Size ctx
b Size tp
s -> forall {k} (x :: Ctx k) (y :: Ctx k).
Size x -> Size y -> Size (x <+> y)
addSize (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 :: forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
$mEmpty :: forall {r} {k} {ctx :: Ctx k} {f :: k -> *}.
Assignment f ctx -> ((ctx ~ EmptyCtx) => r) -> ((# #) -> r) -> r
Empty <- (viewAssign -> AssignEmpty)
  where Empty = 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:> :: forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
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)
-> ((# #) -> r)
-> r
(:>) a v <- (viewAssign -> AssignExtend a v)
  where Assignment f ctx
a :> f tp
v = 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 :: forall {k} (f :: k -> *) (ctx :: Ctx k). Assignment f ctx -> Bool
null Assignment f ctx
a =
  case 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 :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f (ctx ::> tp) -> (Assignment f ctx, f tp)
decompose Assignment f (ctx ::> tp)
x = (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, 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 :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f (ctx '::> tp) -> Assignment f ctx
init Assignment f (ctx '::> tp)
x =
  case 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
t

-- | Return the last element in the assignment.
last :: Assignment f (ctx '::> tp) -> f tp
last :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f (ctx '::> tp) -> f tp
last Assignment f (ctx '::> tp)
x =
  case 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
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 :: forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
view = 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 :: forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k).
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 = forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
appendDiff Size ctx'
sz' in
  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 forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f 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 :: forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k).
Size ctx
-> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx'
drop Size ctx
sz Size ctx'
sz' Assignment f (ctx <+> ctx')
asgn = 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 forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f 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 { forall k (ctx :: Ctx k) (ctx' :: Ctx k).
CtxEmbedding ctx ctx' -> Size ctx'
_ctxeSize       :: Size ctx'
                 , forall k (ctx :: Ctx k) (ctx' :: Ctx k).
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 :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k).
Simple Lens (CtxEmbedding ctx ctx') (Size ctx')
ctxeSize = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens 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 :: 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 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens 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' :: forall (ctx :: Ctx k') (ctx' :: Ctx k') (v :: k').
CtxEmbedding ctx ctx' -> Index ctx v -> Index ctx' v
applyEmbedding' CtxEmbedding ctx ctx'
ctxe Index ctx v
idx = (CtxEmbedding ctx ctx'
ctxe forall s a. s -> Getting a s a -> a
^. 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) 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' :: forall (ctx :: Ctx k') (ctx' :: Ctx k') (v :: k').
Diff ctx ctx' -> Index ctx v -> Index ctx' v
extendContext' = 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 :: forall {k} (ctx :: Ctx k). Size ctx -> CtxEmbedding ctx ctx
identityEmbedding Size ctx
sz = forall k (ctx :: Ctx k) (ctx' :: Ctx k).
Size ctx' -> Assignment (Index ctx') ctx -> CtxEmbedding ctx ctx'
CtxEmbedding Size ctx
sz (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 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 :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (ctx'' :: Ctx k).
Diff ctx' ctx'' -> CtxEmbedding ctx ctx' -> CtxEmbedding ctx ctx''
extendEmbeddingRightDiff Diff ctx' ctx''
diff (CtxEmbedding Size ctx'
sz' Assignment (Index ctx') ctx
assgn) = forall k (ctx :: Ctx k) (ctx' :: Ctx k).
Size ctx' -> Assignment (Index ctx') ctx -> CtxEmbedding ctx ctx'
CtxEmbedding (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 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 (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 :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k).
CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
extendEmbeddingRight = forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (ctx'' :: Ctx k).
Diff ctx' ctx'' -> CtxEmbedding ctx ctx' -> CtxEmbedding ctx ctx''
extendEmbeddingRightDiff 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 :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k).
Size ctx -> Size ctx' -> CtxEmbedding ctx (ctx <+> ctx')
appendEmbedding Size ctx
sz Size ctx'
sz' = forall k (ctx :: Ctx k) (ctx' :: Ctx k).
Size ctx' -> Assignment (Index ctx') ctx -> CtxEmbedding ctx ctx'
CtxEmbedding (forall {k} (x :: Ctx k) (y :: Ctx k).
Size x -> Size y -> Size (x <+> y)
addSize Size ctx
sz Size ctx'
sz') (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 {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 = 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 :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k).
Size ctx -> Size ctx' -> CtxEmbedding ctx' (ctx <+> ctx')
appendEmbeddingLeft Size ctx
sz Size ctx'
sz' = forall k (ctx :: Ctx k) (ctx' :: Ctx k).
Size ctx' -> Assignment (Index ctx') ctx -> CtxEmbedding ctx ctx'
CtxEmbedding (forall {k} (x :: Ctx k) (y :: Ctx k).
Size x -> Size y -> Size (x <+> y)
addSize Size ctx
sz Size ctx'
sz') (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 {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 :: forall {k} (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k).
CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
extendEmbeddingBoth CtxEmbedding ctx ctx'
ctxe = CtxEmbedding ctx (ctx' ::> tp)
updated forall a b. a -> (a -> b) -> b
& 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 forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall {k} (f :: k -> *) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
extend (forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex (CtxEmbedding ctx ctx'
ctxe forall s a. s -> Getting a s a -> a
^. 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 = 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 :: forall {k} (n :: Nat) (ctx :: Ctx k) (f :: k -> *) (r :: k).
Idx n ctx r =>
Lens' (Assignment f ctx) (f r)
field = 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
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 :: forall {k} (n :: Nat) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
natIndex = forall k (n :: Nat) (ctx :: Ctx k) (r :: k).
Idx' 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 :: forall {k} (n :: Nat) (ctx :: Ctx k) (r :: k) (proxy :: Nat -> *).
Idx n ctx r =>
proxy n -> Index ctx r
natIndexProxy proxy n
_ = forall {k} (n :: Nat) (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' = forall {k} (ctx :: Ctx k) (tp :: k).
Size (ctx ::> tp) -> Index (ctx ::> tp) tp
lastIndex 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' = 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
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 :: forall (f :: k -> *) x.
(Assignment f EmptyCtx -> x) -> CurryAssignment EmptyCtx f x
curryAssignment Assignment f EmptyCtx -> x
k = Assignment f EmptyCtx -> x
k forall {k} (f :: k -> *). Assignment f EmptyCtx
empty
  uncurryAssignment :: forall (f :: k -> *) x.
CurryAssignment EmptyCtx f x -> Assignment f EmptyCtx -> x
uncurryAssignment CurryAssignment EmptyCtx f x
k Assignment f EmptyCtx
_ = CurryAssignment EmptyCtx f x
k

instance CurryAssignmentClass ctx => CurryAssignmentClass (ctx ::> a) where
  curryAssignment :: forall (f :: k -> *) x.
(Assignment f (ctx ::> a) -> x) -> CurryAssignment (ctx ::> a) f x
curryAssignment Assignment f (ctx ::> a) -> x
k = 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 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 :: forall (f :: k -> *) x.
CurryAssignment (ctx ::> a) f x -> Assignment f (ctx ::> a) -> x
uncurryAssignment CurryAssignment (ctx ::> a) f x
k Assignment f (ctx ::> a)
asgn =
    case 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 -> forall k (ctx :: Ctx k) (f :: k -> *) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
uncurryAssignment 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 :: forall {k} (f :: k -> *). [Some f] -> Some (Assignment f)
fromList = forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> [Some f] -> Some (Assignment f)
go forall {k} (f :: k -> *). Assignment f EmptyCtx
empty
  where go :: Assignment f ctx -> [Some f] -> Some (Assignment f)
        go :: forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> [Some f] -> Some (Assignment f)
go Assignment f ctx
prev [] = 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) = (forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> [Some f] -> Some (Assignment f)
go forall a b. (a -> b) -> a -> b
$! Assignment f ctx
prev 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 { forall {k} {k} (m :: k -> *) (w :: k) (a :: k).
Collector m w a -> m w
runCollector :: m w }
instance Functor (Collector m w) where
  fmap :: forall a b. (a -> b) -> Collector m w a -> Collector m w b
fmap a -> b
_ (Collector m w
x) = 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 :: forall a. a -> Collector m w a
pure a
_ = forall {k} {k} (m :: k -> *) (w :: k) (a :: k).
m w -> Collector m w a
Collector (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty)
  Collector m w
x <*> :: forall a b.
Collector m w (a -> b) -> Collector m w a -> Collector m w b
<*> Collector m w
y = forall {k} {k} (m :: k -> *) (w :: k) (a :: k).
m w -> Collector m w a
Collector (forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 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 {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 w
f =
  forall {k} {k} (m :: k -> *) (w :: k) (a :: k).
Collector m w a -> m w
runCollector forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> forall {k} {k} (m :: k -> *) (w :: k) (a :: k).
m w -> Collector m w a
Collector (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 {k} (m :: * -> *) (ctx :: Ctx k) (f :: k -> *).
Applicative m =>
(forall (tp :: k). Index ctx tp -> f tp -> m ())
-> Assignment f ctx -> m ()
traverseWithIndex_ forall (tp :: k). Index ctx tp -> f tp -> m ()
f = forall (f :: * -> *) a. Functor f => f a -> f ()
void forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall {k} (a :: k). Size (EmptyCtx ::> a)
size1 = forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize forall {k}. Size 'EmptyCtx
zeroSize

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

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

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

size5 :: Size (EmptyCtx ::> a ::> b ::> c ::> d ::> e)
size5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
size5 = forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize 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 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k).
Size ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f)
size6 = forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize 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 :: forall {k} (a :: k) (b :: k). Index ((EmptyCtx ::> a) ::> b) a
i1of2 = forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex forall {k} (tp :: k). Index ('EmptyCtx '::> tp) tp
baseIndex

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

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

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

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

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

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

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

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

i1of5 :: Index (EmptyCtx ::> a ::> b ::> c ::> d ::> e) a
i1of5 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) a
i1of5 = forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex 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 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) b
i2of5 = forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex 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 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) c
i3of5 = forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex 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 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) d
i4of5 = forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex 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 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
Index (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) e
i5of5 = forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex 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 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k).
Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) a
i1of6 = forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex 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 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k).
Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) b
i2of6 = forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex 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 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k).
Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) c
i3of6 = forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex 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 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k).
Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) d
i4of6 = forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex 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 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k).
Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) e
i5of6 = forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex 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 :: forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k) (f :: k).
Index ((((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e) ::> f) f
i6of6 = forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex forall {k} (a :: k) (b :: k) (c :: k) (d :: k) (e :: k).
Size (((((EmptyCtx ::> a) ::> b) ::> c) ::> d) ::> e)
size5