------------------------------------------------------------------------
-- |
-- Module           : Data.Parameterized.Context.Safe
-- Copyright        : (c) Galois, Inc 2014-2015
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
--
-- This module defines type contexts as a data-kind that consists of
-- a list of types.  Indexes are defined with respect to these contexts.
-- In addition, finite dependent products (Assignments) are defined over
-- type contexts.  The elements of an assignment can be accessed using
-- appropriately-typed indexes.
--
-- This module is intended to export exactly the same API as module
-- "Data.Parameterized.Context.Unsafe", so that they can be used
-- interchangeably.
--
-- This implementation is entirely typesafe, and provides a proof that
-- the signature implemented by this module is consistent.  Contexts,
-- indexes, and assignments are represented naively by linear sequences.
--
-- Compared to the implementation in "Data.Parameterized.Context.Unsafe",
-- this one suffers from the fact that the operation of extending an
-- the context of an index is /not/ a no-op. We therefore cannot use
-- 'Data.Coerce.coerce' to understand indexes in a new context without
-- actually breaking things.
--------------------------------------------------------------------------
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_HADDOCK hide #-}
module Data.Parameterized.Context.Safe
  ( module Data.Parameterized.Ctx
    -- * Size
  , Size
  , sizeInt
  , zeroSize
  , incSize
  , decSize
  , extSize
  , addSize
  , SizeView(..)
  , viewSize
  , sizeToNatRepr
  , KnownContext(..)
    -- * Diff
  , Diff
  , noDiff
  , addDiff
  , extendRight
  , appendDiff
  , DiffView(..)
  , viewDiff
  , KnownDiff(..)
  , IsAppend(..)
  , diffIsAppend
    -- * Indexing
  , Index
  , indexVal
  , baseIndex
  , skipIndex
  , lastIndex
  , nextIndex
  , leftIndex
  , rightIndex
  , extendIndex
  , extendIndex'
  , extendIndexAppendLeft
  , forIndex
  , forIndexRange
  , intIndex
  , IndexView(..)
  , viewIndex
    -- * Assignments
  , Assignment
  , size
  , Data.Parameterized.Context.Safe.replicate
  , generate
  , generateM
  , empty
  , extend
  , adjust
  , update
  , adjustM
  , AssignView(..)
  , viewAssign
  , (!)
  , (!^)
  , zipWith
  , zipWithM
  , (<++>)
  , traverseWithIndex
  ) where

import qualified Control.Category as Cat
import Control.DeepSeq
import qualified Control.Lens as Lens
import Control.Monad.Identity (Identity(..))
import Data.Hashable
import Data.List (intercalate)
import Data.Maybe (listToMaybe)
import Data.Type.Equality
import Prelude hiding (init, map, null, replicate, succ, zipWith)
import Data.Kind(Type)

import Data.Parameterized.Classes
import Data.Parameterized.Ctx
import Data.Parameterized.NatRepr
import Data.Parameterized.Some
import Data.Parameterized.TraversableFC
import Data.Parameterized.TraversableFC.WithIndex

------------------------------------------------------------------------
-- Size

-- | An indexed singleton type representing the size of a context.
data Size (ctx :: Ctx k) where
  SizeZero :: Size 'EmptyCtx
  SizeSucc :: !(Size ctx) -> Size (ctx '::> tp)

-- | Renders as integer literal
instance Show (Size ctx) where
  show :: Size ctx -> String
show = forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt

instance ShowF Size

-- | Convert a context size to an 'Int'.
sizeInt :: Size ctx -> Int
sizeInt :: forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt Size ctx
SizeZero = Int
0
sizeInt (SizeSucc Size ctx
sz) = (forall a. Num a => a -> a -> a
+Int
1) forall a b. (a -> b) -> a -> b
$! forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt Size ctx
sz

-- | The size of an empty context.
zeroSize :: Size 'EmptyCtx
zeroSize :: forall {k}. Size 'EmptyCtx
zeroSize = forall {k}. Size 'EmptyCtx
SizeZero

-- | Increment the size to the next value.
incSize :: Size ctx -> Size (ctx '::> tp)
incSize :: forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
sz = forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
SizeSucc Size ctx
sz

decSize :: Size (ctx '::> tp) -> Size ctx
decSize :: forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx '::> tp) -> Size ctx
decSize (SizeSucc Size ctx
sz) = Size ctx
sz

-- | The total size of two concatenated contexts.
addSize :: Size x -> Size y -> Size (x <+> y)
addSize :: forall {k} (x :: Ctx k) (y :: Ctx k).
Size x -> Size y -> Size (x <+> y)
addSize Size x
sx Size y
SizeZero = Size x
sx
addSize Size x
sx (SizeSucc Size ctx
sy) = forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
SizeSucc (forall {k} (x :: Ctx k) (y :: Ctx k).
Size x -> Size y -> Size (x <+> y)
addSize Size x
sx Size ctx
sy)

-- | Allows interpreting a size.
data SizeView (ctx :: Ctx k) where
  ZeroSize :: SizeView 'EmptyCtx
  IncSize :: !(Size ctx) -> SizeView (ctx '::> tp)

-- | View a size as either zero or a smaller size plus one.
viewSize :: Size ctx -> SizeView ctx
viewSize :: forall {k} (ctx :: Ctx k). Size ctx -> SizeView ctx
viewSize Size ctx
SizeZero = forall {k}. SizeView 'EmptyCtx
ZeroSize
viewSize (SizeSucc Size ctx
s) = forall {k} (n :: Ctx k) (tp :: k). Size n -> SizeView (n '::> tp)
IncSize Size ctx
s

-- | Convert a 'Size' into a 'NatRepr'.
sizeToNatRepr :: Size items -> NatRepr (CtxSize items)
sizeToNatRepr :: forall {k} (items :: Ctx k). Size items -> NatRepr (CtxSize items)
sizeToNatRepr Size items
sz =
  case forall {k} (ctx :: Ctx k). Size ctx -> SizeView ctx
viewSize Size items
sz of
    SizeView items
ZeroSize -> forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr
    IncSize Size ctx
sz' ->
      let oldRep :: NatRepr (CtxSize ctx)
oldRep = forall {k} (items :: Ctx k). Size items -> NatRepr (CtxSize items)
sizeToNatRepr Size ctx
sz'
      in case forall (f :: Nat -> *) (m :: Nat) (g :: Nat -> *) (n :: Nat).
f m -> g n -> (m + n) :~: (n + m)
plusComm (forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr :: NatRepr 1) NatRepr (CtxSize ctx)
oldRep of
           (1 + CtxSize ctx) :~: (CtxSize ctx + 1)
Refl -> forall (n :: Nat). NatRepr n -> NatRepr (n + 1)
incNat NatRepr (CtxSize ctx)
oldRep

------------------------------------------------------------------------
-- Size

-- | A context that can be determined statically at compiler time.
class KnownContext (ctx :: Ctx k) where
  knownSize :: Size ctx

instance KnownContext 'EmptyCtx where
  knownSize :: Size 'EmptyCtx
knownSize = forall {k}. Size 'EmptyCtx
zeroSize

instance KnownContext ctx => KnownContext (ctx '::> tp) where
  knownSize :: Size (ctx '::> tp)
knownSize = forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize forall k (ctx :: Ctx k). KnownContext ctx => Size ctx
knownSize

------------------------------------------------------------------------
-- Diff

-- | Difference in number of elements between two contexts.
-- The first context must be a sub-context of the other.
data Diff (l :: Ctx k) (r :: Ctx k) where
  DiffHere :: Diff ctx ctx
  DiffThere :: Diff ctx1 ctx2 -> Diff ctx1 (ctx2 '::> tp)

-- | The identity difference. Identity element of 'Category' instance.
noDiff :: Diff l l
noDiff :: forall {k} (l :: Ctx k). Diff l l
noDiff = forall {k} (l :: Ctx k). Diff l l
DiffHere

-- | The addition of differences. Flipped binary operation
-- of 'Category' instance.
addDiff :: Diff a b -> Diff b c -> Diff a c
addDiff :: forall {k} (a :: Ctx k) (b :: Ctx k) (c :: Ctx k).
Diff a b -> Diff b c -> Diff a c
addDiff Diff a b
x Diff b c
DiffHere = Diff a b
x
addDiff Diff a b
x (DiffThere Diff b ctx2
y) = forall {k} (ctx1 :: Ctx k) (n :: Ctx k) (tp :: k).
Diff ctx1 n -> Diff ctx1 (n '::> tp)
DiffThere (forall {k} (a :: Ctx k) (b :: Ctx k) (c :: Ctx k).
Diff a b -> Diff b c -> Diff a c
addDiff Diff a b
x Diff b ctx2
y)

-- | Extend the difference to a sub-context of the right side.
extendRight :: Diff l r -> Diff l (r '::> tp)
extendRight :: forall {k} (ctx1 :: Ctx k) (n :: Ctx k) (tp :: k).
Diff ctx1 n -> Diff ctx1 (n '::> tp)
extendRight Diff l r
diff = forall {k} (ctx1 :: Ctx k) (n :: Ctx k) (tp :: k).
Diff ctx1 n -> Diff ctx1 (n '::> tp)
DiffThere Diff l r
diff

appendDiff :: Size r -> Diff l (l <+> r)
appendDiff :: forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
appendDiff Size r
SizeZero = forall {k} (l :: Ctx k). Diff l l
DiffHere
appendDiff (SizeSucc Size ctx
sz) = forall {k} (ctx1 :: Ctx k) (n :: Ctx k) (tp :: k).
Diff ctx1 n -> Diff ctx1 (n '::> tp)
DiffThere (forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
appendDiff Size ctx
sz)

-- | Implemented with 'noDiff' and 'addDiff'
instance Cat.Category Diff where
  id :: forall (a :: Ctx k). Diff a a
id = forall {k} (l :: Ctx k). Diff l l
DiffHere
  Diff b c
d1 . :: forall (b :: Ctx k) (c :: Ctx k) (a :: Ctx k).
Diff b c -> Diff a b -> Diff a c
. Diff a b
d2 = forall {k} (a :: Ctx k) (b :: Ctx k) (c :: Ctx k).
Diff a b -> Diff b c -> Diff a c
addDiff Diff a b
d2 Diff b c
d1

-- | Extend the size by a given difference.
extSize :: Size l -> Diff l r -> Size r
extSize :: forall {k} (l :: Ctx k) (r :: Ctx k). Size l -> Diff l r -> Size r
extSize Size l
sz Diff l r
DiffHere = Size l
sz
extSize Size l
sz (DiffThere Diff l ctx2
diff) = forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize (forall {k} (l :: Ctx k) (r :: Ctx k). Size l -> Diff l r -> Size r
extSize Size l
sz Diff l ctx2
diff)

-- | Proof that @r = l <+> app@ for some @app@
data IsAppend l r where
  IsAppend :: Size app -> IsAppend l (l <+> app)

-- | If @l@ is a sub-context of @r@ then extract out their "contextual
-- difference", i.e., the @app@ such that @r = l <+> app@
diffIsAppend :: Diff l r -> IsAppend l r
diffIsAppend :: forall {k} (l :: Ctx k) (r :: Ctx k). Diff l r -> IsAppend l r
diffIsAppend Diff l r
DiffHere = forall {k} (n :: Ctx k) (l :: Ctx k).
Size n -> IsAppend l (l <+> n)
IsAppend forall {k}. Size 'EmptyCtx
zeroSize
diffIsAppend (DiffThere Diff l ctx2
diff) =
  case forall {k} (l :: Ctx k) (r :: Ctx k). Diff l r -> IsAppend l r
diffIsAppend Diff l ctx2
diff of
    IsAppend Size app
sz -> forall {k} (n :: Ctx k) (l :: Ctx k).
Size n -> IsAppend l (l <+> n)
IsAppend (forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size app
sz)

data DiffView a b where
  NoDiff :: DiffView a a
  ExtendRightDiff :: Diff a b -> DiffView a (b ::> r)

viewDiff :: Diff a b -> DiffView a b
viewDiff :: forall {k} (a :: Ctx k) (b :: Ctx k). Diff a b -> DiffView a b
viewDiff Diff a b
DiffHere = forall {k} (a :: Ctx k). DiffView a a
NoDiff
viewDiff (DiffThere Diff a ctx2
diff) = forall {k} (a :: Ctx k) (n :: Ctx k) (tp :: k).
Diff a n -> DiffView a (n ::> tp)
ExtendRightDiff Diff a ctx2
diff

------------------------------------------------------------------------
-- KnownDiff

-- | A difference that can be automatically inferred at compile time.
class KnownDiff (l :: Ctx k) (r :: Ctx k) where
  knownDiff :: Diff l r

instance KnownDiff l l where
  knownDiff :: Diff l l
knownDiff = forall {k} (l :: Ctx k). Diff l l
noDiff

instance KnownDiff l r => KnownDiff l (r '::> tp) where
  knownDiff :: Diff l (r '::> tp)
knownDiff = forall {k} (ctx1 :: Ctx k) (n :: Ctx k) (tp :: k).
Diff ctx1 n -> Diff ctx1 (n '::> tp)
extendRight forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
knownDiff

------------------------------------------------------------------------
-- Index

-- | An index is a reference to a position with a particular type in a
-- context.
data Index (ctx :: Ctx k) (tp :: k) where
  IndexHere :: Size ctx -> Index (ctx '::> tp) tp
  IndexThere :: !(Index ctx tp) -> Index (ctx '::> tp') tp

-- | Convert an index to an 'Int', where the index of the left-most type in the context is 0.
indexVal :: Index ctx tp -> Int
indexVal :: forall {k} (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
indexVal (IndexHere Size ctx
sz) = forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt Size ctx
sz
indexVal (IndexThere Index ctx tp
idx) = forall {k} (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
indexVal Index ctx tp
idx

instance Eq (Index ctx tp) where
  Index ctx tp
idx1 == :: Index ctx tp -> Index ctx tp -> Bool
== Index ctx tp
idx2 = forall a. Maybe a -> Bool
isJust (forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Index ctx tp
idx1 Index ctx tp
idx2)

instance TestEquality (Index ctx) where
  testEquality :: forall (a :: k) (b :: k).
Index ctx a -> Index ctx b -> Maybe (a :~: b)
testEquality (IndexHere Size ctx
_) (IndexHere Size ctx
_) = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEquality (IndexHere Size ctx
_) (IndexThere Index ctx b
_) = forall a. Maybe a
Nothing
  testEquality (IndexThere Index ctx a
_) (IndexHere Size ctx
_) = forall a. Maybe a
Nothing
  testEquality (IndexThere Index ctx a
idx1) (IndexThere Index ctx b
idx2) =
     case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Index ctx a
idx1 Index ctx b
idx2 of
         Just a :~: b
Refl -> forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
         Maybe (a :~: b)
Nothing -> forall a. Maybe a
Nothing

instance Ord (Index ctx tp) where
  compare :: Index ctx tp -> Index ctx tp -> Ordering
compare Index ctx tp
i Index ctx tp
j = forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF Index ctx tp
i Index ctx tp
j)

instance OrdF (Index ctx) where
  compareF :: forall (x :: k) (y :: k).
Index ctx x -> Index ctx y -> OrderingF x y
compareF (IndexHere Size ctx
_) (IndexHere Size ctx
_) = forall {k} (x :: k). OrderingF x x
EQF
  compareF (IndexThere Index ctx x
_) (IndexHere Size ctx
_) = forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareF (IndexHere Size ctx
_) (IndexThere Index ctx y
_) = forall {k} (x :: k) (y :: k). OrderingF x y
GTF
  compareF (IndexThere Index ctx x
idx1) (IndexThere Index ctx y
idx2) = forall j k (f :: j -> *) (a :: j) (b :: j) (c :: k) (d :: k).
OrdF f =>
f a -> f b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
lexCompareF Index ctx x
idx1 Index ctx y
idx2 forall a b. (a -> b) -> a -> b
$ forall {k} (x :: k). OrderingF x x
EQF

-- | Index for first element in context.
baseIndex :: Index ('EmptyCtx '::> tp) tp
baseIndex :: forall {k} (tp :: k). Index ('EmptyCtx '::> tp) tp
baseIndex = forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
IndexHere forall {k}. Size 'EmptyCtx
SizeZero

-- | Increase context while staying at same index.
skipIndex :: Index ctx x -> Index (ctx '::> y) x
skipIndex :: forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex Index ctx x
idx = forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
IndexThere Index ctx x
idx

-- | Return the index of an element one past the size.
nextIndex :: Size ctx -> Index (ctx '::> tp) tp
nextIndex :: forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
nextIndex Size ctx
sz = forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
IndexHere Size ctx
sz

-- | Return the last index of a element.
lastIndex :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp
lastIndex :: forall {k} (ctx :: Ctx k) (tp :: k).
Size (ctx ::> tp) -> Index (ctx ::> tp) tp
lastIndex (SizeSucc Size ctx
s) = forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
IndexHere Size ctx
s

-- | Adapts an index in the left hand context of an append operation.
leftIndex :: Size r -> Index l tp -> Index (l <+> r) tp
leftIndex :: forall {k} (r :: Ctx k) (l :: Ctx k) (tp :: k).
Size r -> Index l tp -> Index (l <+> r) tp
leftIndex Size r
sr Index l tp
il = forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Diff l r -> Index l tp -> Index r tp
extendIndex' (forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
appendDiff Size r
sr) Index l tp
il

-- | Adapts an index in the right hand context of an append operation.
rightIndex :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp
rightIndex :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Size l -> Size r -> Index r tp -> Index (l <+> r) tp
rightIndex Size l
sl Size r
sr Index r tp
ir =
  case forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index ctx tp -> IndexView ctx tp
viewIndex Size r
sr Index r tp
ir of
    IndexViewInit Index ctx tp
i -> forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex (forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Size l -> Size r -> Index r tp -> Index (l <+> r) tp
rightIndex Size l
sl (forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx '::> tp) -> Size ctx
decSize Size r
sr) Index ctx tp
i)
    IndexViewLast Size ctx
s -> forall {k} (ctx :: Ctx k) (tp :: k).
Size (ctx ::> tp) -> Index (ctx ::> tp) tp
lastIndex (forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize (forall {k} (x :: Ctx k) (y :: Ctx k).
Size x -> Size y -> Size (x <+> y)
addSize Size l
sl Size ctx
s))

{-# INLINE extendIndex #-}
extendIndex :: KnownDiff l r => Index l tp -> Index r tp
extendIndex :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
KnownDiff l r =>
Index l tp -> Index r tp
extendIndex = forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Diff l r -> Index l tp -> Index r tp
extendIndex' forall k (l :: Ctx k) (r :: Ctx k). KnownDiff l r => Diff l r
knownDiff

{-# INLINE extendIndex' #-}
-- | Compute an 'Index' into a context @r@ from an 'Index' into
-- a sub-context @l@ of @r@.
extendIndex' :: Diff l r -> Index l tp -> Index r tp
extendIndex' :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Diff l r -> Index l tp -> Index r tp
extendIndex' Diff l r
DiffHere Index l tp
idx = Index l tp
idx
extendIndex' (DiffThere Diff l ctx2
diff) Index l tp
idx = forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
IndexThere (forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Diff l r -> Index l tp -> Index r tp
extendIndex' Diff l ctx2
diff Index l tp
idx)

{-# INLINE extendIndexAppendLeft #-}
-- | Compute an 'Index' into an appended context from an 'Index' into
-- its suffix.
extendIndexAppendLeft :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp
extendIndexAppendLeft :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Size l -> Size r -> Index r tp -> Index (l <+> r) tp
extendIndexAppendLeft Size l
sz Size r
sz' Index r tp
idx = case forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index ctx tp -> IndexView ctx tp
viewIndex Size r
sz' Index r tp
idx of
  IndexViewLast Size ctx
_ -> forall {k} (ctx :: Ctx k) (tp :: k).
Size (ctx ::> tp) -> Index (ctx ::> tp) tp
lastIndex (forall {k} (x :: Ctx k) (y :: Ctx k).
Size x -> Size y -> Size (x <+> y)
addSize Size l
sz Size r
sz')
  IndexViewInit Index ctx tp
idx' -> forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
skipIndex (forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Size l -> Size r -> Index r tp -> Index (l <+> r) tp
extendIndexAppendLeft Size l
sz (forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx '::> tp) -> Size ctx
decSize Size r
sz') Index ctx tp
idx')

-- | Given a size @n@, a function @f@, and an initial value @v0@, the
-- expression @forIndex n f v0@ calls @f@ on each index less than @n@
-- starting from @0@ and @v0@, with the value @v@ obtained from the
-- last call.
forIndex :: forall ctx r
          . Size ctx
         -> (forall tp . r -> Index ctx tp -> r)
         -> r
         -> r
forIndex :: forall {k} (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
forIndex Size ctx
sz_top forall (tp :: k). r -> Index ctx tp -> r
f = forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> r -> r
go forall a. a -> a
id Size ctx
sz_top
 where go :: forall ctx'. (forall tp. Index ctx' tp -> Index ctx tp) -> Size ctx' -> r -> r
       go :: forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> r -> r
go forall (tp :: k). Index ctx' tp -> Index ctx tp
_ Size ctx'
SizeZero = forall a. a -> a
id
       go forall (tp :: k). Index ctx' tp -> Index ctx tp
g (SizeSucc Size ctx
sz) = \r
r -> forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> r -> r
go (\Index ctx tp
i -> forall (tp :: k). Index ctx' tp -> Index ctx tp
g (forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
IndexThere Index ctx tp
i)) Size ctx
sz  forall a b. (a -> b) -> a -> b
$ forall (tp :: k). r -> Index ctx tp -> r
f r
r (forall (tp :: k). Index ctx' tp -> Index ctx tp
g (forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
IndexHere Size ctx
sz))

data LDiff (l :: Ctx k) (r :: Ctx k) where
 LDiffHere :: LDiff a a
 LDiffThere :: !(LDiff (a::>x) b) -> LDiff a b

ldiffIndex :: Index a tp -> LDiff a b -> Index b tp
ldiffIndex :: forall {k} (a :: Ctx k) (tp :: k) (b :: Ctx k).
Index a tp -> LDiff a b -> Index b tp
ldiffIndex Index a tp
i LDiff a b
LDiffHere = Index a tp
i
ldiffIndex Index a tp
i (LDiffThere LDiff (a ::> x) b
d) = forall {k} (a :: Ctx k) (tp :: k) (b :: Ctx k).
Index a tp -> LDiff a b -> Index b tp
ldiffIndex (forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
IndexThere Index a tp
i) LDiff (a ::> x) b
d

forIndexLDiff :: Size a
              -> LDiff a b
              -> (forall tp . Index b tp -> r -> r)
              -> r
              -> r
forIndexLDiff :: forall {k} (a :: Ctx k) (b :: Ctx k) r.
Size a
-> LDiff a b -> (forall (tp :: k). Index b tp -> r -> r) -> r -> r
forIndexLDiff Size a
_ LDiff a b
LDiffHere forall (tp :: k). Index b tp -> r -> r
_ r
r = r
r
forIndexLDiff Size a
sz (LDiffThere LDiff (a ::> x) b
d) forall (tp :: k). Index b tp -> r -> r
f r
r =
  forall {k} (a :: Ctx k) (b :: Ctx k) r.
Size a
-> LDiff a b -> (forall (tp :: k). Index b tp -> r -> r) -> r -> r
forIndexLDiff (forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
SizeSucc Size a
sz) LDiff (a ::> x) b
d forall (tp :: k). Index b tp -> r -> r
f (forall (tp :: k). Index b tp -> r -> r
f (forall {k} (a :: Ctx k) (tp :: k) (b :: Ctx k).
Index a tp -> LDiff a b -> Index b tp
ldiffIndex (forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
IndexHere Size a
sz) LDiff (a ::> x) b
d) r
r)

forIndexRangeImpl :: Int
                  -> Size a
                  -> LDiff a b
                  -> (forall tp . Index b tp -> r -> r)
                  -> r
                  -> r
forIndexRangeImpl :: forall {k} (a :: Ctx k) (b :: Ctx k) r.
Int
-> Size a
-> LDiff a b
-> (forall (tp :: k). Index b tp -> r -> r)
-> r
-> r
forIndexRangeImpl Int
0 Size a
sz LDiff a b
d forall (tp :: k). Index b tp -> r -> r
f r
r = forall {k} (a :: Ctx k) (b :: Ctx k) r.
Size a
-> LDiff a b -> (forall (tp :: k). Index b tp -> r -> r) -> r -> r
forIndexLDiff Size a
sz LDiff a b
d forall (tp :: k). Index b tp -> r -> r
f r
r
forIndexRangeImpl Int
_ Size a
SizeZero LDiff a b
_ forall (tp :: k). Index b tp -> r -> r
_ r
r = r
r
forIndexRangeImpl Int
i (SizeSucc Size ctx
sz) LDiff a b
d forall (tp :: k). Index b tp -> r -> r
f r
r =
  forall {k} (a :: Ctx k) (b :: Ctx k) r.
Int
-> Size a
-> LDiff a b
-> (forall (tp :: k). Index b tp -> r -> r)
-> r
-> r
forIndexRangeImpl (Int
iforall a. Num a => a -> a -> a
-Int
1) Size ctx
sz (forall {k} (a :: Ctx k) (n :: k) (b :: Ctx k).
LDiff (a ::> n) b -> LDiff a b
LDiffThere LDiff a b
d) forall (tp :: k). Index b tp -> r -> r
f r
r

-- | Given an index @i@, size @n@, a function @f@, and a value @v@,
-- the expression @forIndexRange i n f v@ is equivalent
-- to @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n f v)@
-- otherwise.
forIndexRange :: Int
              -> Size ctx
              -> (forall tp . Index ctx tp -> r -> r)
              -> r
              -> r
forIndexRange :: forall {k} (ctx :: Ctx k) r.
Int
-> Size ctx -> (forall (tp :: k). Index ctx tp -> r -> r) -> r -> r
forIndexRange Int
i Size ctx
sz forall (tp :: k). Index ctx tp -> r -> r
f r
r = forall {k} (a :: Ctx k) (b :: Ctx k) r.
Int
-> Size a
-> LDiff a b
-> (forall (tp :: k). Index b tp -> r -> r)
-> r
-> r
forIndexRangeImpl Int
i Size ctx
sz forall {k} (a :: Ctx k). LDiff a a
LDiffHere forall (tp :: k). Index ctx tp -> r -> r
f r
r

indexList :: forall ctx. Size ctx -> [Some (Index ctx)]
indexList :: forall {k} (ctx :: Ctx k). Size ctx -> [Some (Index ctx)]
indexList Size ctx
sz_top = forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> [Some (Index ctx)] -> Size ctx' -> [Some (Index ctx)]
go forall a. a -> a
id [] Size ctx
sz_top
 where go :: (forall tp. Index ctx' tp -> Index ctx tp)
          -> [Some (Index ctx)]
          -> Size ctx'
          -> [Some (Index ctx)]
       go :: forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> [Some (Index ctx)] -> Size ctx' -> [Some (Index ctx)]
go forall (tp :: k). Index ctx' tp -> Index ctx tp
_ [Some (Index ctx)]
ls Size ctx'
SizeZero       = [Some (Index ctx)]
ls
       go forall (tp :: k). Index ctx' tp -> Index ctx tp
g [Some (Index ctx)]
ls (SizeSucc Size ctx
sz)  = forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> [Some (Index ctx)] -> Size ctx' -> [Some (Index ctx)]
go (\Index ctx tp
i -> forall (tp :: k). Index ctx' tp -> Index ctx tp
g (forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
IndexThere Index ctx tp
i)) (forall k (f :: k -> *) (x :: k). f x -> Some f
Some (forall (tp :: k). Index ctx' tp -> Index ctx tp
g (forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
IndexHere Size ctx
sz)) forall a. a -> [a] -> [a]
: [Some (Index ctx)]
ls) Size ctx
sz

-- | Return index at given integer or nothing if integer is out of bounds.
intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx))
intIndex :: forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
intIndex Int
n Size ctx
sz = forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
n forall a b. (a -> b) -> a -> b
$ forall {k} (ctx :: Ctx k). Size ctx -> [Some (Index ctx)]
indexList Size ctx
sz

-- | Renders as integer literal
instance Show (Index ctx tp) where
   show :: Index ctx tp -> String
show = forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
indexVal

instance ShowF (Index ctx)

-- | View of indexes as pointing to the last element in the
-- index range or pointing to an earlier element in a smaller
-- range.
data IndexView ctx tp where
  IndexViewLast :: Size  ctx   -> IndexView (ctx '::> t) t
  IndexViewInit :: Index ctx t -> IndexView (ctx '::> u) t

instance ShowF (IndexView ctx)
deriving instance Show (IndexView ctx tp)

-- | Project an index
viewIndex :: Size ctx -> Index ctx tp -> IndexView ctx tp
viewIndex :: forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index ctx tp -> IndexView ctx tp
viewIndex Size ctx
_ (IndexHere Size ctx
sz) = forall {k} (n :: Ctx k) (t :: k). Size n -> IndexView (n '::> t) t
IndexViewLast Size ctx
sz
viewIndex Size ctx
_ (IndexThere Index ctx tp
i) = forall {k} (n :: Ctx k) (t :: k) (tp :: k).
Index n t -> IndexView (n '::> tp) t
IndexViewInit Index ctx tp
i
-- NB: the unused size parameter is needed in the Unsafe module

------------------------------------------------------------------------
-- Assignment

-- | An assignment is a sequence that maps each index with type 'tp' to
-- a value of type 'f tp'.
data Assignment (f :: k -> Type) (ctx :: Ctx k) where
  AssignmentEmpty :: Assignment f EmptyCtx
  AssignmentExtend :: Assignment f ctx -> f tp -> Assignment f (ctx ::> tp)

-- | View an assignment as either empty or an assignment with one appended.
data AssignView (f :: k -> Type) (ctx :: Ctx k) where
  AssignEmpty :: AssignView f EmptyCtx
  AssignExtend :: Assignment f ctx -> f tp -> AssignView f (ctx::>tp)

viewAssign :: forall f ctx . Assignment f ctx -> AssignView f ctx
viewAssign :: forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
viewAssign Assignment f ctx
AssignmentEmpty = forall {k} (f :: k -> *). AssignView f EmptyCtx
AssignEmpty
viewAssign (AssignmentExtend Assignment f ctx
asgn f tp
x) = forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> AssignView f (n ::> tp)
AssignExtend Assignment f ctx
asgn f tp
x

instance NFData (Assignment f ctx) where
  rnf :: Assignment f ctx -> ()
rnf Assignment f ctx
AssignmentEmpty = ()
  rnf (AssignmentExtend Assignment f ctx
asgn f tp
x) = forall a. NFData a => a -> ()
rnf Assignment f ctx
asgn seq :: forall a b. a -> b -> b
`seq` f tp
x seq :: forall a b. a -> b -> b
`seq` ()

-- | Return number of elements in assignment.
size :: Assignment f ctx -> Size ctx
size :: forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size Assignment f ctx
AssignmentEmpty = forall {k}. Size 'EmptyCtx
SizeZero
size (AssignmentExtend Assignment f ctx
asgn f tp
_) = forall {k} (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
SizeSucc (forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size Assignment f ctx
asgn)

-- | Generate an assignment
generate :: forall ctx f
          . Size ctx
         -> (forall tp . Index ctx tp -> f tp)
         -> Assignment f ctx
generate :: forall {k} (ctx :: Ctx k) (f :: k -> *).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
generate Size ctx
sz_top forall (tp :: k). Index ctx tp -> f tp
f = forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> Assignment f ctx'
go forall a. a -> a
id Size ctx
sz_top
 where go :: forall ctx'
           . (forall tp. Index ctx' tp -> Index ctx tp)
          -> Size ctx'
          -> Assignment f ctx'
       go :: forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> Assignment f ctx'
go forall (tp :: k). Index ctx' tp -> Index ctx tp
_ Size ctx'
SizeZero = forall {k} (f :: k -> *). Assignment f EmptyCtx
AssignmentEmpty
       go forall (tp :: k). Index ctx' tp -> Index ctx tp
g (SizeSucc Size ctx
sz) =
            let ctx :: Assignment f ctx
ctx = forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> Assignment f ctx'
go (\Index ctx tp
i -> forall (tp :: k). Index ctx' tp -> Index ctx tp
g (forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
IndexThere Index ctx tp
i)) Size ctx
sz
                x :: f tp
x = forall (tp :: k). Index ctx tp -> f tp
f (forall (tp :: k). Index ctx' tp -> Index ctx tp
g (forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
IndexHere Size ctx
sz))
             in forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend Assignment f ctx
ctx f tp
x

-- | Generate an assignment
generateM :: forall ctx m f
           . Applicative m
          => Size ctx
          -> (forall tp . Index ctx tp -> m (f tp))
          -> m (Assignment f ctx)
generateM :: forall {k} (ctx :: Ctx k) (m :: * -> *) (f :: k -> *).
Applicative m =>
Size ctx
-> (forall (tp :: k). Index ctx tp -> m (f tp))
-> m (Assignment f ctx)
generateM Size ctx
sz_top forall (tp :: k). Index ctx tp -> m (f tp)
f = forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> m (Assignment f ctx')
go forall a. a -> a
id Size ctx
sz_top
 where go :: forall ctx'. (forall tp. Index ctx' tp -> Index ctx tp) -> Size ctx' -> m (Assignment f ctx')
       go :: forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> m (Assignment f ctx')
go forall (tp :: k). Index ctx' tp -> Index ctx tp
_ Size ctx'
SizeZero = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (f :: k -> *). Assignment f EmptyCtx
AssignmentEmpty
       go forall (tp :: k). Index ctx' tp -> Index ctx tp
g (SizeSucc Size ctx
sz) =
             forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (ctx' :: Ctx k).
(forall (tp :: k). Index ctx' tp -> Index ctx tp)
-> Size ctx' -> m (Assignment f ctx')
go (\Index ctx tp
i -> forall (tp :: k). Index ctx' tp -> Index ctx tp
g (forall {k} (ctx :: Ctx k) (x :: k) (y :: k).
Index ctx x -> Index (ctx '::> y) x
IndexThere Index ctx tp
i)) Size ctx
sz) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (tp :: k). Index ctx tp -> m (f tp)
f (forall (tp :: k). Index ctx' tp -> Index ctx tp
g (forall {k} (n :: Ctx k) (tp :: k). Size n -> Index (n '::> tp) tp
IndexHere Size ctx
sz))

-- | @replicate n@ make a context with different copies of the same
-- polymorphic value.
replicate :: Size ctx -> (forall tp . f tp) -> Assignment f ctx
replicate :: forall {k} (ctx :: Ctx k) (f :: k -> *).
Size ctx -> (forall (tp :: k). f tp) -> Assignment f ctx
replicate Size ctx
n forall (tp :: k). f tp
c = forall {k} (ctx :: Ctx k) (f :: k -> *).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
generate Size ctx
n (\Index ctx tp
_ -> forall (tp :: k). f tp
c)

-- | Create empty indexed vector.
empty :: Assignment f 'EmptyCtx
empty :: forall {k} (f :: k -> *). Assignment f EmptyCtx
empty = forall {k} (f :: k -> *). Assignment f EmptyCtx
AssignmentEmpty

-- n.b. see 'singleton' in Data/Parameterized/Context.hs

-- | Extend an indexed vector with a new entry.
extend :: Assignment f ctx -> f tp -> Assignment f (ctx '::> tp)
extend :: forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
extend Assignment f ctx
asgn f tp
e = forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend Assignment f ctx
asgn f tp
e

{-# DEPRECATED adjust "Replace 'adjust f i asgn' with 'Lens.over (ixF i) f asgn' instead." #-}
adjust :: forall f ctx tp. (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx
adjust :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(f tp -> f tp)
-> Index ctx tp -> Assignment f ctx -> Assignment f ctx
adjust f tp -> f tp
f Index ctx tp
idx Assignment f ctx
asgn = forall a. Identity a -> a
runIdentity (forall {k} (m :: * -> *) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Functor m =>
(f tp -> m (f tp))
-> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
adjustM (forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. f tp -> f tp
f) Index ctx tp
idx Assignment f ctx
asgn)

{-# DEPRECATED update "Replace 'update idx val asgn' with 'Lens.set (ixF idx) val asgn' instead." #-}
update :: forall f ctx tp. Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx
update :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx
update Index ctx tp
i f tp
v Assignment f ctx
a = forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(f tp -> f tp)
-> Index ctx tp -> Assignment f ctx -> Assignment f ctx
adjust (\f tp
_ -> f tp
v) Index ctx tp
i Assignment f ctx
a

adjustM :: forall m f ctx tp. Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
adjustM :: forall {k} (m :: * -> *) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Functor m =>
(f tp -> m (f tp))
-> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
adjustM f tp -> m (f tp)
f = forall (g :: k -> *) (ctx' :: Ctx k).
(forall (tp' :: k). g tp' -> f tp')
-> Index ctx' tp -> Assignment g ctx' -> m (Assignment f ctx')
go (\f tp'
x -> f tp'
x)
 where
  go :: (forall tp'. g tp' -> f tp') -> Index ctx' tp -> Assignment g ctx' -> m (Assignment f ctx')
  go :: forall (g :: k -> *) (ctx' :: Ctx k).
(forall (tp' :: k). g tp' -> f tp')
-> Index ctx' tp -> Assignment g ctx' -> m (Assignment f ctx')
go forall (tp' :: k). g tp' -> f tp'
g (IndexHere Size ctx
_)     (AssignmentExtend Assignment g ctx
asgn g tp
x) = forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend (forall {k} (f :: k -> *) (g :: k -> *) (c :: Ctx k).
(forall (tp :: k). f tp -> g tp)
-> Assignment f c -> Assignment g c
map forall (tp' :: k). g tp' -> f tp'
g Assignment g ctx
asgn) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f tp -> m (f tp)
f (forall (tp' :: k). g tp' -> f tp'
g g tp
x)
  go forall (tp' :: k). g tp' -> f tp'
g (IndexThere Index ctx tp
idx)  (AssignmentExtend Assignment g ctx
asgn g tp
x) = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend (forall (tp' :: k). g tp' -> f tp'
g g tp
x)   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (g :: k -> *) (ctx' :: Ctx k).
(forall (tp' :: k). g tp' -> f tp')
-> Index ctx' tp -> Assignment g ctx' -> m (Assignment f ctx')
go forall (tp' :: k). g tp' -> f tp'
g Index ctx tp
idx Assignment g ctx
asgn

type instance IndexF   (Assignment (f :: k -> Type) ctx) = Index ctx
type instance IxValueF (Assignment (f :: k -> Type) ctx) = f

instance forall k (f :: k -> Type) ctx. IxedF k (Assignment f ctx) where
  ixF :: Index ctx x -> Lens.Traversal' (Assignment f ctx) (f x)
  ixF :: forall (x :: k). Index ctx x -> Traversal' (Assignment f ctx) (f x)
ixF Index ctx x
idx f x -> f (f x)
f = forall {k} (m :: * -> *) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Functor m =>
(f tp -> m (f tp))
-> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
adjustM f x -> f (f x)
f Index ctx x
idx

instance forall k (f :: k -> Type) ctx. IxedF' k (Assignment f ctx) where
  ixF' :: Index ctx x -> Lens.Lens' (Assignment f ctx) (f x)
  ixF' :: forall (x :: k). Index ctx x -> Lens' (Assignment f ctx) (f x)
ixF' Index ctx x
idx f x -> f (f x)
f = forall {k} (m :: * -> *) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Functor m =>
(f tp -> m (f tp))
-> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
adjustM f x -> f (f x)
f Index ctx x
idx

idxlookup :: (forall tp. a tp -> b tp) -> Assignment a ctx -> forall tp. Index ctx tp -> b tp
idxlookup :: forall {k} (a :: k -> *) (b :: k -> *) (ctx :: Ctx k).
(forall (tp :: k). a tp -> b tp)
-> Assignment a ctx -> forall (tp :: k). Index ctx tp -> b tp
idxlookup forall (tp :: k). a tp -> b tp
f (AssignmentExtend Assignment a ctx
_   a tp
x) (IndexHere Size ctx
_) = forall (tp :: k). a tp -> b tp
f a tp
x
idxlookup forall (tp :: k). a tp -> b tp
f (AssignmentExtend Assignment a ctx
ctx a tp
_) (IndexThere Index ctx tp
idx) = forall {k} (a :: k -> *) (b :: k -> *) (ctx :: Ctx k).
(forall (tp :: k). a tp -> b tp)
-> Assignment a ctx -> forall (tp :: k). Index ctx tp -> b tp
idxlookup forall (tp :: k). a tp -> b tp
f Assignment a ctx
ctx Index ctx tp
idx
idxlookup forall (tp :: k). a tp -> b tp
_ Assignment a ctx
AssignmentEmpty Index ctx tp
idx = case Index ctx tp
idx of {}

-- | Return value of assignment.
(!) :: Assignment f ctx -> Index ctx tp -> f tp
! :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
(!) Assignment f ctx
asgn Index ctx tp
idx = forall {k} (a :: k -> *) (b :: k -> *) (ctx :: Ctx k).
(forall (tp :: k). a tp -> b tp)
-> Assignment a ctx -> forall (tp :: k). Index ctx tp -> b tp
idxlookup forall a. a -> a
id Assignment f ctx
asgn Index ctx tp
idx

-- | Return value of assignment, where the index is into an
--   initial sequence of the assignment.
(!^) :: KnownDiff l r => Assignment f r -> Index l tp -> f tp
Assignment f r
a !^ :: forall {k} (l :: Ctx k) (r :: Ctx k) (f :: k -> *) (tp :: k).
KnownDiff l r =>
Assignment f r -> Index l tp -> f tp
!^ Index l tp
i = Assignment f r
a 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).
KnownDiff l r =>
Index l tp -> Index r tp
extendIndex Index l tp
i

instance TestEquality f => Eq (Assignment f ctx) where
  Assignment f ctx
x == :: Assignment f ctx -> Assignment f ctx -> Bool
== Assignment f ctx
y = forall a. Maybe a -> Bool
isJust (forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Assignment f ctx
x Assignment f ctx
y)

testEq :: (forall x y. f x -> f y -> Maybe (x :~: y))
       -> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)
testEq :: forall {k} (f :: k -> *) (cxt1 :: Ctx k) (cxt2 :: Ctx k).
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)
testEq forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
_ Assignment f cxt1
AssignmentEmpty Assignment f cxt2
AssignmentEmpty = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
testEq forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test (AssignmentExtend Assignment f ctx
ctx1 f tp
x1) (AssignmentExtend Assignment f ctx
ctx2 f tp
x2) =
     case forall {k} (f :: k -> *) (cxt1 :: Ctx k) (cxt2 :: Ctx k).
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)
testEq forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test Assignment f ctx
ctx1 Assignment f ctx
ctx2 of
       Maybe (ctx :~: ctx)
Nothing -> forall a. Maybe a
Nothing
       Just ctx :~: ctx
Refl ->
          case forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test f tp
x1 f tp
x2 of
             Maybe (tp :~: tp)
Nothing -> forall a. Maybe a
Nothing
             Just tp :~: tp
Refl -> forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
testEq forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
_ Assignment f cxt1
AssignmentEmpty AssignmentExtend{} = forall a. Maybe a
Nothing
testEq forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
_ AssignmentExtend{} Assignment f cxt2
AssignmentEmpty = forall a. Maybe a
Nothing

instance TestEqualityFC Assignment where
   testEqualityFC :: forall (f :: k -> *).
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> forall (x :: Ctx k) (y :: Ctx k).
   Assignment f x -> Assignment f y -> Maybe (x :~: y)
testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
f = forall {k} (f :: k -> *) (cxt1 :: Ctx k) (cxt2 :: Ctx k).
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)
testEq forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
f
instance TestEquality f => TestEquality (Assignment f) where
   testEquality :: forall (a :: Ctx k) (b :: Ctx k).
Assignment f a -> Assignment f b -> Maybe (a :~: b)
testEquality Assignment f a
x Assignment f b
y = forall {k} (f :: k -> *) (cxt1 :: Ctx k) (cxt2 :: Ctx k).
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> Assignment f cxt1 -> Assignment f cxt2 -> Maybe (cxt1 :~: cxt2)
testEq forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Assignment f a
x Assignment f b
y
instance TestEquality f => PolyEq (Assignment f x) (Assignment f y) where
  polyEqF :: Assignment f x
-> Assignment f y -> Maybe (Assignment f x :~: Assignment f y)
polyEqF Assignment f x
x Assignment f y
y = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\x :~: y
Refl -> forall {k} (a :: k). a :~: a
Refl) forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Assignment f x
x Assignment f y
y

compareAsgn :: (forall x y. f x -> f y -> OrderingF x y)
            -> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2
compareAsgn :: forall {k} (f :: k -> *) (ctx1 :: Ctx k) (ctx2 :: Ctx k).
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2
compareAsgn forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
_ Assignment f ctx1
AssignmentEmpty Assignment f ctx2
AssignmentEmpty = forall {k} (x :: k). OrderingF x x
EQF
compareAsgn forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
_ Assignment f ctx1
AssignmentEmpty Assignment f ctx2
_ = forall {k} (x :: k) (y :: k). OrderingF x y
GTF
compareAsgn forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
_ Assignment f ctx1
_ Assignment f ctx2
AssignmentEmpty = forall {k} (x :: k) (y :: k). OrderingF x y
LTF
compareAsgn forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test (AssignmentExtend Assignment f ctx
ctx1 f tp
x) (AssignmentExtend Assignment f ctx
ctx2 f tp
y) =
  case forall {k} (f :: k -> *) (ctx1 :: Ctx k) (ctx2 :: Ctx k).
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2
compareAsgn forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test Assignment f ctx
ctx1 Assignment f ctx
ctx2 of
    OrderingF ctx ctx
LTF -> forall {k} (x :: k) (y :: k). OrderingF x y
LTF
    OrderingF ctx ctx
GTF -> forall {k} (x :: k) (y :: k). OrderingF x y
GTF
    OrderingF ctx ctx
EQF -> case forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test f tp
x f tp
y of
              OrderingF tp tp
LTF -> forall {k} (x :: k) (y :: k). OrderingF x y
LTF
              OrderingF tp tp
GTF -> forall {k} (x :: k) (y :: k). OrderingF x y
GTF
              OrderingF tp tp
EQF -> forall {k} (x :: k). OrderingF x x
EQF

instance OrdFC Assignment where
  compareFC :: forall (f :: k -> *).
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> forall (x :: Ctx k) (y :: Ctx k).
   Assignment f x -> Assignment f y -> OrderingF x y
compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
f = forall {k} (f :: k -> *) (ctx1 :: Ctx k) (ctx2 :: Ctx k).
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2
compareAsgn forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
f

instance OrdF f => OrdF (Assignment f) where
  compareF :: forall (x :: Ctx k) (y :: Ctx k).
Assignment f x -> Assignment f y -> OrderingF x y
compareF = forall {k} (f :: k -> *) (ctx1 :: Ctx k) (ctx2 :: Ctx k).
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> Assignment f ctx1 -> Assignment f ctx2 -> OrderingF ctx1 ctx2
compareAsgn forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF

instance OrdF f => Ord (Assignment f ctx) where
  compare :: Assignment f ctx -> Assignment f ctx -> Ordering
compare Assignment f ctx
x Assignment f ctx
y = forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
compareF Assignment f ctx
x Assignment f ctx
y)


instance Hashable (Index ctx tp) where
  hashWithSalt :: Int -> Index ctx tp -> Int
hashWithSalt = forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
hashWithSaltF
instance HashableF (Index ctx) where
  hashWithSaltF :: forall (tp :: k). Int -> Index ctx tp -> Int
hashWithSaltF Int
s Index ctx tp
i = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (forall {k} (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
indexVal Index ctx tp
i)

instance (HashableF f, TestEquality f) => HashableF (Assignment f) where
  hashWithSaltF :: forall (tp :: Ctx k). Int -> Assignment f tp -> Int
hashWithSaltF = forall a. Hashable a => Int -> a -> Int
hashWithSalt

instance (HashableF f, TestEquality f) => Hashable (Assignment f ctx) where
  hashWithSalt :: Int -> Assignment f ctx -> Int
hashWithSalt Int
s Assignment f ctx
AssignmentEmpty = Int
s
  hashWithSalt Int
s (AssignmentExtend Assignment f ctx
asgn f tp
x) = (Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Assignment f ctx
asgn) forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
`hashWithSaltF` f tp
x

instance ShowF f => Show (Assignment f ctx) where
  show :: Assignment f ctx -> String
show Assignment f ctx
a = String
"[" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall {k} (f :: k -> *) a (c :: Ctx k).
(forall (tp :: k). f tp -> a) -> Assignment f c -> [a]
toList forall k (f :: k -> *) (tp :: k). ShowF f => f tp -> String
showF Assignment f ctx
a) forall a. [a] -> [a] -> [a]
++ String
"]"

instance ShowF f => ShowF (Assignment f)

instance FunctorFC Assignment where
  fmapFC :: forall (f :: k -> *) (g :: k -> *).
(forall (x :: k). f x -> g x)
-> forall (x :: Ctx k). Assignment f x -> Assignment g x
fmapFC = forall {k} {l} (t :: (k -> *) -> l -> *) (f :: k -> *)
       (g :: k -> *).
TraversableFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
fmapFCDefault

instance FoldableFC Assignment where
  foldMapFC :: forall (f :: k -> *) m.
Monoid m =>
(forall (x :: k). f x -> m)
-> forall (x :: Ctx k). Assignment f x -> m
foldMapFC = forall {k} {l} (t :: (k -> *) -> l -> *) m (f :: k -> *).
(TraversableFC t, Monoid m) =>
(forall (x :: k). f x -> m) -> forall (x :: l). t f x -> m
foldMapFCDefault

instance TraversableFC Assignment where
  traverseFC :: forall (f :: k -> *) (g :: k -> *) (m :: * -> *).
Applicative m =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: Ctx k). Assignment f x -> m (Assignment g x)
traverseFC forall (x :: k). f x -> m (g x)
f = forall k (f :: k -> *) (g :: k -> *) (m :: * -> *) (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> m (g tp))
-> Assignment f c -> m (Assignment g c)
traverseF forall (x :: k). f x -> m (g x)
f

instance FunctorFCWithIndex Assignment where
  imapFC :: forall (f :: k -> *) (g :: k -> *) (z :: Ctx k).
(forall (x :: k). IndexF (Assignment f z) x -> f x -> g x)
-> Assignment f z -> Assignment g z
imapFC = forall {k} {l} (t :: (k -> *) -> l -> *) (f :: k -> *)
       (g :: k -> *) (z :: l).
TraversableFCWithIndex t =>
(forall (x :: k). IndexF (t f z) x -> f x -> g x) -> t f z -> t g z
imapFCDefault

instance FoldableFCWithIndex Assignment where
  ifoldMapFC :: forall (f :: k -> *) m (z :: Ctx k).
Monoid m =>
(forall (x :: k). IndexF (Assignment f z) x -> f x -> m)
-> Assignment f z -> m
ifoldMapFC = forall {k} {l} (t :: (k -> *) -> l -> *) m (z :: l) (f :: k -> *).
(TraversableFCWithIndex t, Monoid m) =>
(forall (x :: k). IndexF (t f z) x -> f x -> m) -> t f z -> m
ifoldMapFCDefault

instance TraversableFCWithIndex Assignment where
  itraverseFC :: forall (m :: * -> *) (z :: Ctx k) (f :: k -> *) (g :: k -> *).
Applicative m =>
(forall (x :: k). IndexF (Assignment f z) x -> f x -> m (g x))
-> Assignment f z -> m (Assignment g z)
itraverseFC = 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

-- | Map assignment
map :: (forall tp . f tp -> g tp) -> Assignment f c -> Assignment g c
map :: forall {k} (f :: k -> *) (g :: k -> *) (c :: Ctx k).
(forall (tp :: k). f tp -> g tp)
-> Assignment f c -> Assignment g c
map forall (tp :: k). f tp -> g tp
f = 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 (tp :: k). f tp -> g tp
f

traverseF :: forall k (f:: k -> Type) (g::k -> Type) (m:: Type -> Type) (c::Ctx k)
           . Applicative m
          => (forall tp . f tp -> m (g tp))
          -> Assignment f c
          -> m (Assignment g c)
traverseF :: forall k (f :: k -> *) (g :: k -> *) (m :: * -> *) (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> m (g tp))
-> Assignment f c -> m (Assignment g c)
traverseF forall (tp :: k). f tp -> m (g tp)
_ Assignment f c
AssignmentEmpty = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (f :: k -> *). Assignment f EmptyCtx
AssignmentEmpty
traverseF forall (tp :: k). f tp -> m (g tp)
f (AssignmentExtend Assignment f ctx
asgn f tp
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k (f :: k -> *) (g :: k -> *) (m :: * -> *) (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> m (g tp))
-> Assignment f c -> m (Assignment g c)
traverseF forall (tp :: k). f tp -> m (g tp)
f Assignment f ctx
asgn forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (tp :: k). f tp -> m (g tp)
f f tp
x

-- | Convert assignment to list.
toList :: (forall tp . f tp -> a)
       -> Assignment f c
       -> [a]
toList :: forall {k} (f :: k -> *) a (c :: Ctx k).
(forall (tp :: k). f tp -> a) -> Assignment f c -> [a]
toList forall (tp :: k). f tp -> a
f = forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
toListFC forall (tp :: k). f tp -> a
f

zipWithM :: Applicative m
         => (forall tp . f tp -> g tp -> m (h tp))
         -> Assignment f c
         -> Assignment g c
         -> m (Assignment h c)
zipWithM :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> g tp -> m (h tp))
-> Assignment f c -> Assignment g c -> m (Assignment h c)
zipWithM forall (tp :: k). f tp -> g tp -> m (h tp)
f Assignment f c
x Assignment g c
y = Assignment f c -> Assignment g c -> m (Assignment h c)
go Assignment f c
x Assignment g c
y
 where go :: Assignment f c -> Assignment g c -> m (Assignment h c)
go Assignment f c
AssignmentEmpty Assignment g c
Assignment g 'EmptyCtx
AssignmentEmpty = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (f :: k -> *). Assignment f EmptyCtx
AssignmentEmpty
       go (AssignmentExtend Assignment f ctx
asgn1 f tp
x1) (AssignmentExtend Assignment g ctx
asgn2 g tp
x2) =
             forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> g tp -> m (h tp))
-> Assignment f c -> Assignment g c -> m (Assignment h c)
zipWithM forall (tp :: k). f tp -> g tp -> m (h tp)
f Assignment f ctx
asgn1 Assignment g ctx
asgn2) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (tp :: k). f tp -> g tp -> m (h tp)
f f tp
x1 g tp
x2)

zipWith :: (forall x . f x -> g x -> h x)
        -> Assignment f a
        -> Assignment g a
        -> Assignment h a
zipWith :: forall {k} (f :: k -> *) (g :: k -> *) (h :: k -> *) (a :: Ctx k).
(forall (x :: k). f x -> g x -> h x)
-> Assignment f a -> Assignment g a -> Assignment h a
zipWith forall (x :: k). f x -> g x -> h x
f = \Assignment f a
x Assignment g a
y -> forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> g tp -> m (h tp))
-> Assignment f c -> Assignment g c -> m (Assignment h c)
zipWithM (\f tp
u g tp
v -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (x :: k). f x -> g x -> h x
f f tp
u g tp
v)) Assignment f a
x Assignment g a
y
{-# INLINE zipWith #-}

-- | This is a specialization of 'itraverseFC'.
traverseWithIndex :: Applicative m
                  => (forall tp . Index ctx tp -> f tp -> m (g tp))
                  -> Assignment f ctx
                  -> m (Assignment g ctx)
traverseWithIndex :: 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 forall (tp :: k). Index ctx tp -> f tp -> m (g tp)
f Assignment f ctx
a = forall {k} (ctx :: Ctx k) (m :: * -> *) (f :: k -> *).
Applicative m =>
Size ctx
-> (forall (tp :: k). Index ctx tp -> m (f tp))
-> m (Assignment f ctx)
generateM (forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size Assignment f ctx
a) forall a b. (a -> b) -> a -> b
$ \Index ctx tp
i -> forall (tp :: k). Index ctx tp -> f tp -> m (g tp)
f Index ctx tp
i (Assignment f ctx
a forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Index ctx tp
i)

(<++>) :: Assignment f x -> Assignment f y -> Assignment f (x <+> y)
Assignment f x
x <++> :: forall {k} (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
Assignment f x -> Assignment f y -> Assignment f (x <+> y)
<++> Assignment f y
AssignmentEmpty = Assignment f x
x
Assignment f x
x <++> AssignmentExtend Assignment f ctx
y f tp
t = forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend (Assignment f x
x forall {k} (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
Assignment f x -> Assignment f y -> Assignment f (x <+> y)
<++> Assignment f ctx
y) f tp
t

------------------------------------------------------------------------
-- KnownRepr instances

instance (KnownRepr (Assignment f) ctx, KnownRepr f bt)
      => KnownRepr (Assignment f) (ctx ::> bt) where
  knownRepr :: Assignment f (ctx ::> bt)
knownRepr = forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
`extend` forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

instance KnownRepr (Assignment f) EmptyCtx where
  knownRepr :: Assignment f EmptyCtx
knownRepr = forall {k} (f :: k -> *). Assignment f EmptyCtx
empty

--------------------------------------------------------------------------------------
-- lookups and update for lenses

data MyNat where
  MyZ :: MyNat
  MyS :: MyNat -> MyNat

type MyZ = 'MyZ
type MyS = 'MyS

data MyNatRepr :: MyNat -> Type where
  MyZR :: MyNatRepr MyZ
  MySR :: MyNatRepr n -> MyNatRepr (MyS n)

type family StrongCtxUpdate (n::MyNat) (ctx::Ctx k) (z::k) :: Ctx k where
  StrongCtxUpdate n       EmptyCtx     z = EmptyCtx
  StrongCtxUpdate MyZ     (ctx::>x)    z = ctx ::> z
  StrongCtxUpdate (MyS n) (ctx::>x)    z = (StrongCtxUpdate n ctx z) ::> x

type family MyNatLookup (n::MyNat) (ctx::Ctx k) (f::k -> Type) :: Type where
  MyNatLookup n       EmptyCtx  f = ()
  MyNatLookup MyZ     (ctx::>x) f = f x
  MyNatLookup (MyS n) (ctx::>x) f = MyNatLookup n ctx f

mynat_lookup :: MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup :: forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr n
_   Assignment f ctx
AssignmentEmpty = ()
mynat_lookup MyNatRepr n
MyZR     (AssignmentExtend Assignment f ctx
_    f tp
x) = f tp
x
mynat_lookup (MySR MyNatRepr n
n) (AssignmentExtend Assignment f ctx
asgn f tp
_) = forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr n
n Assignment f ctx
asgn

strong_ctx_update :: MyNatRepr n -> Assignment f ctx -> f tp -> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update :: forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr n
_        Assignment f ctx
AssignmentEmpty           f tp
_ = forall {k} (f :: k -> *). Assignment f EmptyCtx
AssignmentEmpty
strong_ctx_update MyNatRepr n
MyZR     (AssignmentExtend Assignment f ctx
asgn f tp
_) f tp
z = forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend Assignment f ctx
asgn f tp
z
strong_ctx_update (MySR MyNatRepr n
n) (AssignmentExtend Assignment f ctx
asgn f tp
x) f tp
z = forall {k} (f :: k -> *) (n :: Ctx k) (tp :: k).
Assignment f n -> f tp -> Assignment f (n ::> tp)
AssignmentExtend (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr n
n Assignment f ctx
asgn f tp
z) f tp
x

------------------------------------------------------------------------
-- 1 field lens combinators

type Assignment1 f x1 = Assignment f ('EmptyCtx '::> x1)

instance Lens.Field1 (Assignment1 f t) (Assignment1 f u) (f t) (f u) where

  _1 :: Lens (Assignment1 f t) (Assignment1 f u) (f t) (f u)
_1 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
        where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR

------------------------------------------------------------------------
-- 2 field lens combinators

type Assignment2 f x1 x2
   = Assignment f ('EmptyCtx '::> x1 '::> x2)

instance Lens.Field1 (Assignment2 f t x2) (Assignment2 f u x2) (f t) (f u) where
  _1 :: Lens (Assignment2 f t x2) (Assignment2 f u x2) (f t) (f u)
_1 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS 'MyZ)
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS 'MyZ)
n)
        where n :: MyNatRepr (MyS 'MyZ)
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field2 (Assignment2 f x1 t) (Assignment2 f x1 u) (f t) (f u) where
  _2 :: Lens (Assignment2 f x1 t) (Assignment2 f x1 u) (f t) (f u)
_2 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
        where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR


------------------------------------------------------------------------
-- 3 field lens combinators

type Assignment3 f x1 x2 x3
   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3)

instance Lens.Field1 (Assignment3 f t x2 x3)
                     (Assignment3 f u x2 x3)
                     (f t)
                     (f u) where
  _1 :: Lens (Assignment3 f t x2 x3) (Assignment3 f u x2 x3) (f t) (f u)
_1 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
n)
        where n :: MyNatRepr (MyS (MyS 'MyZ))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field2 (Assignment3 f x1 t x3)
                     (Assignment3 f x1 u x3)
                     (f t)
                     (f u) where
  _2 :: Lens (Assignment3 f x1 t x3) (Assignment3 f x1 u x3) (f t) (f u)
_2 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS 'MyZ)
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS 'MyZ)
n)
        where n :: MyNatRepr (MyS 'MyZ)
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field3 (Assignment3 f x1 x2 t)
                     (Assignment3 f x1 x2 u)
                     (f t)
                     (f u) where
  _3 :: Lens (Assignment3 f x1 x2 t) (Assignment3 f x1 x2 u) (f t) (f u)
_3 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
        where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR

------------------------------------------------------------------------
-- 4 field lens combinators

type Assignment4 f x1 x2 x3 x4
   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4)

instance Lens.Field1 (Assignment4 f t x2 x3 x4)
                     (Assignment4 f u x2 x3 x4)
                     (f t)
                     (f u) where
  _1 :: Lens
  (Assignment4 f t x2 x3 x4) (Assignment4 f u x2 x3 x4) (f t) (f u)
_1 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
n)
        where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field2 (Assignment4 f x1 t x3 x4)
                     (Assignment4 f x1 u x3 x4)
                     (f t)
                     (f u) where
  _2 :: Lens
  (Assignment4 f x1 t x3 x4) (Assignment4 f x1 u x3 x4) (f t) (f u)
_2 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
n)
        where n :: MyNatRepr (MyS (MyS 'MyZ))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field3 (Assignment4 f x1 x2 t x4)
                     (Assignment4 f x1 x2 u x4)
                     (f t)
                     (f u) where
  _3 :: Lens
  (Assignment4 f x1 x2 t x4) (Assignment4 f x1 x2 u x4) (f t) (f u)
_3 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS 'MyZ)
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS 'MyZ)
n)
        where n :: MyNatRepr (MyS 'MyZ)
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field4 (Assignment4 f x1 x2 x3 t)
                     (Assignment4 f x1 x2 x3 u)
                     (f t)
                     (f u) where
  _4 :: Lens
  (Assignment4 f x1 x2 x3 t) (Assignment4 f x1 x2 x3 u) (f t) (f u)
_4 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
        where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR


------------------------------------------------------------------------
-- 5 field lens combinators

type Assignment5 f x1 x2 x3 x4 x5
   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5)

instance Lens.Field1 (Assignment5 f t x2 x3 x4 x5)
                     (Assignment5 f u x2 x3 x4 x5)
                     (f t)
                     (f u) where
  _1 :: Lens
  (Assignment5 f t x2 x3 x4 x5)
  (Assignment5 f u x2 x3 x4 x5)
  (f t)
  (f u)
_1 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n)
        where n :: MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field2 (Assignment5 f x1 t x3 x4 x5)
                     (Assignment5 f x1 u x3 x4 x5)
                     (f t)
                     (f u) where
  _2 :: Lens
  (Assignment5 f x1 t x3 x4 x5)
  (Assignment5 f x1 u x3 x4 x5)
  (f t)
  (f u)
_2 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
n)
        where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field3 (Assignment5 f x1 x2 t x4 x5)
                     (Assignment5 f x1 x2 u x4 x5)
                     (f t)
                     (f u) where
  _3 :: Lens
  (Assignment5 f x1 x2 t x4 x5)
  (Assignment5 f x1 x2 u x4 x5)
  (f t)
  (f u)
_3 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
n)
        where n :: MyNatRepr (MyS (MyS 'MyZ))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field4 (Assignment5 f x1 x2 x3 t x5)
                     (Assignment5 f x1 x2 x3 u x5)
                     (f t)
                     (f u) where
  _4 :: Lens
  (Assignment5 f x1 x2 x3 t x5)
  (Assignment5 f x1 x2 x3 u x5)
  (f t)
  (f u)
_4 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS 'MyZ)
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS 'MyZ)
n)
        where n :: MyNatRepr (MyS 'MyZ)
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field5 (Assignment5 f x1 x2 x3 x4 t)
                     (Assignment5 f x1 x2 x3 x4 u)
                     (f t)
                     (f u) where
  _5 :: Lens
  (Assignment5 f x1 x2 x3 x4 t)
  (Assignment5 f x1 x2 x3 x4 u)
  (f t)
  (f u)
_5 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
        where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR

------------------------------------------------------------------------
-- 6 field lens combinators

type Assignment6 f x1 x2 x3 x4 x5 x6
   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6)

instance Lens.Field1 (Assignment6 f t x2 x3 x4 x5 x6)
                     (Assignment6 f u x2 x3 x4 x5 x6)
                     (f t)
                     (f u) where
  _1 :: Lens
  (Assignment6 f t x2 x3 x4 x5 x6)
  (Assignment6 f u x2 x3 x4 x5 x6)
  (f t)
  (f u)
_1 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n)
        where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field2 (Assignment6 f x1 t x3 x4 x5 x6)
                     (Assignment6 f x1 u x3 x4 x5 x6)
                     (f t)
                     (f u) where
  _2 :: Lens
  (Assignment6 f x1 t x3 x4 x5 x6)
  (Assignment6 f x1 u x3 x4 x5 x6)
  (f t)
  (f u)
_2 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n)
        where n :: MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field3 (Assignment6 f x1 x2 t x4 x5 x6)
                     (Assignment6 f x1 x2 u x4 x5 x6)
                     (f t)
                     (f u) where
  _3 :: Lens
  (Assignment6 f x1 x2 t x4 x5 x6)
  (Assignment6 f x1 x2 u x4 x5 x6)
  (f t)
  (f u)
_3 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
n)
        where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field4 (Assignment6 f x1 x2 x3 t x5 x6)
                     (Assignment6 f x1 x2 x3 u x5 x6)
                     (f t)
                     (f u) where
  _4 :: Lens
  (Assignment6 f x1 x2 x3 t x5 x6)
  (Assignment6 f x1 x2 x3 u x5 x6)
  (f t)
  (f u)
_4 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
n)
        where n :: MyNatRepr (MyS (MyS 'MyZ))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field5 (Assignment6 f x1 x2 x3 x4 t x6)
                     (Assignment6 f x1 x2 x3 x4 u x6)
                     (f t)
                     (f u) where
  _5 :: Lens
  (Assignment6 f x1 x2 x3 x4 t x6)
  (Assignment6 f x1 x2 x3 x4 u x6)
  (f t)
  (f u)
_5 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS 'MyZ)
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS 'MyZ)
n)
        where n :: MyNatRepr (MyS 'MyZ)
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field6 (Assignment6 f x1 x2 x3 x4 x5 t)
                     (Assignment6 f x1 x2 x3 x4 x5 u)
                     (f t)
                     (f u) where
  _6 :: Lens
  (Assignment6 f x1 x2 x3 x4 x5 t)
  (Assignment6 f x1 x2 x3 x4 x5 u)
  (f t)
  (f u)
_6 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
        where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR

------------------------------------------------------------------------
-- 7 field lens combinators

type Assignment7 f x1 x2 x3 x4 x5 x6 x7
   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7)

instance Lens.Field1 (Assignment7 f t x2 x3 x4 x5 x6 x7)
                     (Assignment7 f u x2 x3 x4 x5 x6 x7)
                     (f t)
                     (f u) where
  _1 :: Lens
  (Assignment7 f t x2 x3 x4 x5 x6 x7)
  (Assignment7 f u x2 x3 x4 x5 x6 x7)
  (f t)
  (f u)
_1 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n)
        where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field2 (Assignment7 f x1 t x3 x4 x5 x6 x7)
                     (Assignment7 f x1 u x3 x4 x5 x6 x7)
                     (f t)
                     (f u) where
  _2 :: Lens
  (Assignment7 f x1 t x3 x4 x5 x6 x7)
  (Assignment7 f x1 u x3 x4 x5 x6 x7)
  (f t)
  (f u)
_2 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n)
        where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field3 (Assignment7 f x1 x2 t x4 x5 x6 x7)
                     (Assignment7 f x1 x2 u x4 x5 x6 x7)
                     (f t)
                     (f u) where
  _3 :: Lens
  (Assignment7 f x1 x2 t x4 x5 x6 x7)
  (Assignment7 f x1 x2 u x4 x5 x6 x7)
  (f t)
  (f u)
_3 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n)
        where n :: MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field4 (Assignment7 f x1 x2 x3 t x5 x6 x7)
                     (Assignment7 f x1 x2 x3 u x5 x6 x7)
                     (f t)
                     (f u) where
  _4 :: Lens
  (Assignment7 f x1 x2 x3 t x5 x6 x7)
  (Assignment7 f x1 x2 x3 u x5 x6 x7)
  (f t)
  (f u)
_4 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
n)
        where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field5 (Assignment7 f x1 x2 x3 x4 t x6 x7)
                     (Assignment7 f x1 x2 x3 x4 u x6 x7)
                     (f t)
                     (f u) where
  _5 :: Lens
  (Assignment7 f x1 x2 x3 x4 t x6 x7)
  (Assignment7 f x1 x2 x3 x4 u x6 x7)
  (f t)
  (f u)
_5 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
n)
        where n :: MyNatRepr (MyS (MyS 'MyZ))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field6 (Assignment7 f x1 x2 x3 x4 x5 t x7)
                     (Assignment7 f x1 x2 x3 x4 x5 u x7)
                     (f t)
                     (f u) where
  _6 :: Lens
  (Assignment7 f x1 x2 x3 x4 x5 t x7)
  (Assignment7 f x1 x2 x3 x4 x5 u x7)
  (f t)
  (f u)
_6 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS 'MyZ)
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS 'MyZ)
n)
        where n :: MyNatRepr (MyS 'MyZ)
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field7 (Assignment7 f x1 x2 x3 x4 x5 x6 t)
                     (Assignment7 f x1 x2 x3 x4 x5 x6 u)
                     (f t)
                     (f u) where
  _7 :: Lens
  (Assignment7 f x1 x2 x3 x4 x5 x6 t)
  (Assignment7 f x1 x2 x3 x4 x5 x6 u)
  (f t)
  (f u)
_7 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
        where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR

------------------------------------------------------------------------
-- 8 field lens combinators

type Assignment8 f x1 x2 x3 x4 x5 x6 x7 x8
   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7 '::> x8)

instance Lens.Field1 (Assignment8 f t x2 x3 x4 x5 x6 x7 x8)
                     (Assignment8 f u x2 x3 x4 x5 x6 x7 x8)
                     (f t)
                     (f u) where
  _1 :: Lens
  (Assignment8 f t x2 x3 x4 x5 x6 x7 x8)
  (Assignment8 f u x2 x3 x4 x5 x6 x7 x8)
  (f t)
  (f u)
_1 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
n)
        where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR


instance Lens.Field2 (Assignment8 f x1 t x3 x4 x5 x6 x7 x8)
                     (Assignment8 f x1 u x3 x4 x5 x6 x7 x8)
                     (f t)
                     (f u) where
  _2 :: Lens
  (Assignment8 f x1 t x3 x4 x5 x6 x7 x8)
  (Assignment8 f x1 u x3 x4 x5 x6 x7 x8)
  (f t)
  (f u)
_2 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n)
        where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field3 (Assignment8 f x1 x2 t x4 x5 x6 x7 x8)
                     (Assignment8 f x1 x2 u x4 x5 x6 x7 x8)
                     (f t)
                     (f u) where
  _3 :: Lens
  (Assignment8 f x1 x2 t x4 x5 x6 x7 x8)
  (Assignment8 f x1 x2 u x4 x5 x6 x7 x8)
  (f t)
  (f u)
_3 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n)
        where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field4 (Assignment8 f x1 x2 x3 t x5 x6 x7 x8)
                     (Assignment8 f x1 x2 x3 u x5 x6 x7 x8)
                     (f t)
                     (f u) where
  _4 :: Lens
  (Assignment8 f x1 x2 x3 t x5 x6 x7 x8)
  (Assignment8 f x1 x2 x3 u x5 x6 x7 x8)
  (f t)
  (f u)
_4 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n)
        where n :: MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field5 (Assignment8 f x1 x2 x3 x4 t x6 x7 x8)
                     (Assignment8 f x1 x2 x3 x4 u x6 x7 x8)
                     (f t)
                     (f u) where
  _5 :: Lens
  (Assignment8 f x1 x2 x3 x4 t x6 x7 x8)
  (Assignment8 f x1 x2 x3 x4 u x6 x7 x8)
  (f t)
  (f u)
_5 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
n)
        where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field6 (Assignment8 f x1 x2 x3 x4 x5 t x7 x8)
                     (Assignment8 f x1 x2 x3 x4 x5 u x7 x8)
                     (f t)
                     (f u) where
  _6 :: Lens
  (Assignment8 f x1 x2 x3 x4 x5 t x7 x8)
  (Assignment8 f x1 x2 x3 x4 x5 u x7 x8)
  (f t)
  (f u)
_6 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
n)
        where n :: MyNatRepr (MyS (MyS 'MyZ))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field7 (Assignment8 f x1 x2 x3 x4 x5 x6 t x8)
                     (Assignment8 f x1 x2 x3 x4 x5 x6 u x8)
                     (f t)
                     (f u) where
  _7 :: Lens
  (Assignment8 f x1 x2 x3 x4 x5 x6 t x8)
  (Assignment8 f x1 x2 x3 x4 x5 x6 u x8)
  (f t)
  (f u)
_7 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS 'MyZ)
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS 'MyZ)
n)
        where n :: MyNatRepr (MyS 'MyZ)
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field8 (Assignment8 f x1 x2 x3 x4 x5 x6 x7 t)
                     (Assignment8 f x1 x2 x3 x4 x5 x6 x7 u)
                     (f t)
                     (f u) where
  _8 :: Lens
  (Assignment8 f x1 x2 x3 x4 x5 x6 x7 t)
  (Assignment8 f x1 x2 x3 x4 x5 x6 x7 u)
  (f t)
  (f u)
_8 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
        where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR

------------------------------------------------------------------------
-- 9 field lens combinators

type Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 x9
   = Assignment f ('EmptyCtx '::> x1 '::> x2 '::> x3 '::> x4 '::> x5 '::> x6 '::> x7 '::> x8 '::> x9)


instance Lens.Field1 (Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9)
                     (Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9)
                     (f t)
                     (f u) where
  _1 :: Lens
  (Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9)
  (Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9)
  (f t)
  (f u)
_1 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
n)
        where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field2 (Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9)
                     (Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9)
                     (f t)
                     (f u) where
  _2 :: Lens
  (Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9)
  (Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9)
  (f t)
  (f u)
_2 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
n)
        where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ)))))))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field3 (Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9)
                     (Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9)
                     (f t)
                     (f u) where
  _3 :: Lens
  (Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9)
  (Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9)
  (f t)
  (f u)
_3 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n)
        where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS (MyS 'MyZ))))))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field4 (Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9)
                     (Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9)
                     (f t)
                     (f u) where
  _4 :: Lens
  (Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9)
  (Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9)
  (f t)
  (f u)
_4 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n)
        where n :: MyNatRepr (MyS (MyS (MyS (MyS (MyS 'MyZ)))))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field5 (Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9)
                     (Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9)
                     (f t)
                     (f u) where
  _5 :: Lens
  (Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9)
  (Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9)
  (f t)
  (f u)
_5 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n)
        where n :: MyNatRepr (MyS (MyS (MyS (MyS 'MyZ))))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field6 (Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9)
                     (Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9)
                     (f t)
                     (f u) where
  _6 :: Lens
  (Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9)
  (Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9)
  (f t)
  (f u)
_6 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS (MyS 'MyZ)))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS (MyS 'MyZ)))
n)
        where n :: MyNatRepr (MyS (MyS (MyS 'MyZ)))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field7 (Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9)
                     (Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9)
                     (f t)
                     (f u) where
  _7 :: Lens
  (Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9)
  (Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9)
  (f t)
  (f u)
_7 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS (MyS 'MyZ))
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS (MyS 'MyZ))
n)
        where n :: MyNatRepr (MyS (MyS 'MyZ))
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field8 (Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9)
                     (Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9)
                     (f t)
                     (f u) where
  _8 :: Lens
  (Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9)
  (Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9)
  (f t)
  (f u)
_8 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr (MyS 'MyZ)
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr (MyS 'MyZ)
n)
        where n :: MyNatRepr (MyS 'MyZ)
n = forall (n :: MyNat). MyNatRepr n -> MyNatRepr (MyS n)
MySR forall a b. (a -> b) -> a -> b
$ MyNatRepr 'MyZ
MyZR

instance Lens.Field9 (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t)
                     (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u)
                     (f t)
                     (f u) where
  _9 :: Lens
  (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t)
  (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u)
  (f t)
  (f u)
_9 = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k).
MyNatRepr n -> Assignment f ctx -> MyNatLookup n ctx f
mynat_lookup MyNatRepr 'MyZ
n) (forall {k} (n :: MyNat) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
MyNatRepr n
-> Assignment f ctx
-> f tp
-> Assignment f (StrongCtxUpdate n ctx tp)
strong_ctx_update MyNatRepr 'MyZ
n)
        where n :: MyNatRepr 'MyZ
n = MyNatRepr 'MyZ
MyZR