{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_HADDOCK hide #-}
module Data.Parameterized.Context.Unsafe
  ( module Data.Parameterized.Ctx
  , KnownContext(..)
    -- * Size
  , Size
  , sizeInt
  , zeroSize
  , incSize
  , decSize
  , extSize
  , addSize
  , SizeView(..)
  , viewSize
  , sizeToNatRepr
    -- * 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
    -- ** IndexRange
  , IndexRange
  , allRange
  , indexOfRange
  , dropHeadRange
  , dropTailRange
    -- * Assignments
  , Assignment
  , size
  , Data.Parameterized.Context.Unsafe.replicate
  , generate
  , generateM
  , empty
  , extend
  , adjust
  , update
  , adjustM
  , AssignView(..)
  , viewAssign
  , (!)
  , (!^)
  , Data.Parameterized.Context.Unsafe.zipWith
  , zipWithM
  , (<++>)
  , traverseWithIndex
  ) where

import qualified Control.Category as Cat
import           Control.DeepSeq
import           Control.Exception
import qualified Control.Lens as Lens
import           Control.Monad.Identity (Identity(..))
import           Data.Bits
import           Data.Coerce
import           Data.Hashable
import           Data.List (intercalate)
import           Data.Proxy
import           Unsafe.Coerce
import           Data.Kind(Type)

import           Data.Parameterized.Axiom
import           Data.Parameterized.Classes
import           Data.Parameterized.Ctx
import           Data.Parameterized.Ctx.Proofs
import           Data.Parameterized.NatRepr
import           Data.Parameterized.NatRepr.Internal (NatRepr(NatRepr))
import           Data.Parameterized.Some
import           Data.Parameterized.TraversableFC
import           Data.Parameterized.TraversableFC.WithIndex

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

-- | Represents the size of a context.
newtype Size (ctx :: Ctx k) = Size Int

type role Size nominal

-- | Convert a context size to an 'Int'.
sizeInt :: Size ctx -> Int
sizeInt :: forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt (Size Int
n) = Int
n

-- | The size of an empty context.
zeroSize :: Size 'EmptyCtx
zeroSize :: forall {k}. Size 'EmptyCtx
zeroSize = forall k (ctx :: Ctx k). Int -> Size ctx
Size Int
0

-- | 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 Int
n) = forall k (ctx :: Ctx k). Int -> Size ctx
Size (Int
nforall a. Num a => a -> a -> a
+Int
1)

decSize :: Size (ctx '::> tp) -> Size ctx
decSize :: forall {k} (ctx :: Ctx k) (tp :: k). Size (ctx '::> tp) -> Size ctx
decSize (Size Int
n) = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
n forall a. Ord a => a -> a -> Bool
> Int
0) (forall k (ctx :: Ctx k). Int -> Size ctx
Size (Int
nforall a. Num a => a -> a -> a
-Int
1))

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

-- | Project a size
viewSize :: Size ctx -> SizeView ctx
viewSize :: forall {k} (ctx :: Ctx k). Size ctx -> SizeView ctx
viewSize (Size Int
0) = forall a b. a -> b
unsafeCoerce forall {k}. SizeView 'EmptyCtx
ZeroSize
viewSize (Size Int
n) = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
n forall a. Ord a => a -> a -> Bool
> Int
0) (forall a b. a -> b
unsafeCoerce (forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> SizeView (ctx '::> tp)
IncSize (forall k (ctx :: Ctx k). Int -> Size ctx
Size (Int
nforall a. Num a => a -> a -> a
-Int
1))))

-- | 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 Int
n) = forall (n :: Natural). Natural -> NatRepr n
NatRepr (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n)

instance Show (Size ctx) where
  show :: Size ctx -> String
show (Size Int
i) = forall a. Show a => a -> String
show Int
i

instance ShowF 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.
newtype Diff (l :: Ctx k) (r :: Ctx k)
      = Diff { forall k (l :: Ctx k) (r :: Ctx k). Diff l r -> Int
_contextExtSize :: Int }

type role Diff nominal nominal

-- | 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) (r :: Ctx k). Int -> Diff l r
Diff Int
0
{-# INLINE noDiff #-}

-- | 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 Int
x) (Diff Int
y) = forall k (l :: Ctx k) (r :: Ctx k). Int -> Diff l r
Diff (Int
x forall a. Num a => a -> a -> a
+ Int
y)
{-# INLINE addDiff #-}

-- | Extend the difference to a sub-context of the right side.
extendRight :: Diff l r -> Diff l (r '::> tp)
extendRight :: forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Diff l r -> Diff l (r '::> tp)
extendRight (Diff Int
i) = forall k (l :: Ctx k) (r :: Ctx k). Int -> Diff l r
Diff (Int
iforall a. Num a => a -> a -> a
+Int
1)

appendDiff :: Size r -> Diff l (l <+> r)
appendDiff :: forall {k} (r :: Ctx k) (l :: Ctx k). Size r -> Diff l (l <+> r)
appendDiff (Size Int
r) = forall k (l :: Ctx k) (r :: Ctx k). Int -> Diff l r
Diff Int
r

-- | 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
noDiff
  Diff b c
j . :: forall (b :: Ctx k) (c :: Ctx k) (a :: Ctx k).
Diff b c -> Diff a b -> Diff a c
. Diff a b
i = forall {k} (a :: Ctx k) (b :: Ctx k) (c :: Ctx k).
Diff a b -> Diff b c -> Diff a c
addDiff Diff a b
i Diff b c
j

-- | 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 Int
i) (Diff Int
j) = forall k (ctx :: Ctx k). Int -> Size ctx
Size (Int
iforall a. Num a => a -> a -> a
+Int
j)

-- | 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 Int
x) (Size Int
y) = forall k (ctx :: Ctx k). Int -> Size ctx
Size (Int
x forall a. Num a => a -> a -> a
+ Int
y)


-- | 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 Int
i) = forall a b. a -> b
unsafeCoerce forall a b. (a -> b) -> a -> b
$ forall {k} (ctx :: Ctx k) (l :: Ctx k).
Size ctx -> IsAppend l (l <+> ctx)
IsAppend (forall k (ctx :: Ctx k). Int -> Size ctx
Size Int
i)

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 Int
i)
  | Int
i forall a. Eq a => a -> a -> Bool
== Int
0 = forall a b. a -> b
unsafeCoerce forall {k} (a :: Ctx k). DiffView a a
NoDiff
  | Bool
otherwise  = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
i forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce forall a b. (a -> b) -> a -> b
$ forall {k} (a :: Ctx k) (ctx :: Ctx k) (tp :: k).
Diff a ctx -> DiffView a (ctx ::> tp)
ExtendRightDiff (forall k (l :: Ctx k) (r :: Ctx k). Int -> Diff l r
Diff (Int
iforall a. Num a => a -> a -> a
-Int
1))

------------------------------------------------------------------------
-- 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 {-# INCOHERENT #-} KnownDiff l r => KnownDiff l (r '::> tp) where
  knownDiff :: Diff l (r '::> tp)
knownDiff = forall {k} (l :: Ctx k) (r :: Ctx k) (tp :: k).
Diff l r -> Diff l (r '::> 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.
newtype Index (ctx :: Ctx k) (tp :: k) = Index { forall k (ctx :: Ctx k) (tp :: k). Index ctx tp -> Int
indexVal :: Int }

type role Index nominal nominal

instance Eq (Index ctx tp) where
  Index Int
i == :: Index ctx tp -> Index ctx tp -> Bool
== Index Int
j = Int
i forall a. Eq a => a -> a -> Bool
== Int
j

instance TestEquality (Index ctx) where
  testEquality :: forall (a :: k) (b :: k).
Index ctx a -> Index ctx b -> Maybe (a :~: b)
testEquality (Index Int
i) (Index Int
j)
    | Int
i forall a. Eq a => a -> a -> Bool
== Int
j = forall a. a -> Maybe a
Just forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom
    | Bool
otherwise = forall a. Maybe a
Nothing

instance Ord (Index ctx tp) where
  Index Int
i compare :: Index ctx tp -> Index ctx tp -> Ordering
`compare` Index Int
j = forall a. Ord a => a -> a -> Ordering
compare Int
i Int
j

instance OrdF (Index ctx) where
  compareF :: forall (x :: k) (y :: k).
Index ctx x -> Index ctx y -> OrderingF x y
compareF (Index Int
i) (Index Int
j)
    | Int
i forall a. Ord a => a -> a -> Bool
< Int
j = forall {k} (x :: k) (y :: k). OrderingF x y
LTF
    | Int
i forall a. Eq a => a -> a -> Bool
== Int
j = forall a b. a -> b
unsafeCoerce forall {k} (x :: k). OrderingF x x
EQF
    | Bool
otherwise = forall {k} (x :: k) (y :: k). OrderingF x y
GTF

-- | Index for first element in context.
baseIndex :: Index ('EmptyCtx '::> tp) tp
baseIndex :: forall {k} (tp :: k). Index ('EmptyCtx '::> tp) tp
baseIndex = forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index Int
0

-- | 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 Int
i) = forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index Int
i

-- | Return the index of a element one past the size.
nextIndex :: Size ctx -> Index (ctx ::> tp) tp
nextIndex :: forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size ctx
n = forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index (forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt Size ctx
n)

-- | 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 Size (ctx ::> tp)
n = forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index (forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt Size (ctx ::> tp)
n forall a. Num a => a -> a -> a
- Int
1)

-- | 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
_ (Index Int
il) = forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index Int
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 Int
sl) Size r
_ (Index Int
ir) = forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index (Int
sl forall a. Num a => a -> a -> a
+ Int
ir)

{-# 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
_ = forall a b. a -> b
unsafeCoerce

{-# 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 Int
l) Size r
_ (Index Int
idx) = forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index (Int
idx forall a. Num a => a -> a -> a
+ Int
l)

-- | Given a size @n@, a function @f@, and an initial value @v0@, the
-- expression @forIndex n f v0@ is equivalent to @v0@ when @n@ is
-- zero, and @f (forIndex (n-1) f v0) n@ otherwise.  Unlike the safe
-- version, which starts from 'Index' @0@ and increments 'Index'
-- values, this version starts at 'Index' @(n-1)@ and decrements
-- 'Index' values to 'Index' @0@.
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
n forall (tp :: k). r -> Index ctx tp -> r
f r
r =
  case forall {k} (ctx :: Ctx k). Size ctx -> SizeView ctx
viewSize Size ctx
n of
    SizeView ctx
ZeroSize -> r
r
    IncSize Size ctx
p -> forall (tp :: k). r -> Index ctx tp -> r
f (forall {k} (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
forIndex Size ctx
p (coerce :: forall a b. Coercible a b => a -> b
coerce forall (tp :: k). r -> Index ctx tp -> r
f) r
r) (forall {k} (ctx :: Ctx k) (tp :: k).
Size ctx -> Index (ctx ::> tp) tp
nextIndex Size ctx
p)

-- | Given an index @i@, size @n@, a function @f@, and a value @v@,
-- the expression @forIndex i n f v@ is equivalent to
-- @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n f v)@
-- otherwise.
forIndexRange :: forall ctx r
               . 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 Int
n) forall (tp :: k). Index ctx tp -> r -> r
f r
r
  | Int
i forall a. Ord a => a -> a -> Bool
>= Int
n = r
r
  | Bool
otherwise = forall (tp :: k). Index ctx tp -> r -> r
f (forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index Int
i) (forall {k} (ctx :: Ctx k) r.
Int
-> Size ctx -> (forall (tp :: k). Index ctx tp -> r -> r) -> r -> r
forIndexRange (Int
iforall a. Num a => a -> a -> a
+Int
1) (forall k (ctx :: Ctx k). Int -> Size ctx
Size Int
n) forall (tp :: k). Index ctx tp -> r -> r
f r
r)

-- | 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
i Size ctx
n | Int
0 forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i forall a. Ord a => a -> a -> Bool
< forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt Size ctx
n = forall a. a -> Maybe a
Just (forall k (f :: k -> *) (x :: k). f x -> Some f
Some (forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index Int
i))
             | Bool
otherwise = forall a. Maybe a
Nothing

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

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

-- | 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 Int
sz) (Index Int
i)
  | Int
sz' forall a. Eq a => a -> a -> Bool
== Int
i  = forall a b. a -> b
unsafeCoerce (forall {k} (ctx :: Ctx k) (t :: k).
Size ctx -> IndexView (ctx '::> t) t
IndexViewLast (forall k (ctx :: Ctx k). Int -> Size ctx
Size Int
sz'))
  | Bool
otherwise = forall a b. a -> b
unsafeCoerce (forall {k} (ctx :: Ctx k) (t :: k) (tp :: k).
Index ctx t -> IndexView (ctx '::> tp) t
IndexViewInit (forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index Int
i))
  where
    sz' :: Int
sz' = Int
szforall a. Num a => a -> a -> a
-Int
1

------------------------------------------------------------------------
-- IndexRange

-- | This represents a contiguous range of indices.
data IndexRange (ctx :: Ctx k) (sub :: Ctx k)
   = IndexRange {-# UNPACK #-} !Int
                {-# UNPACK #-} !Int

-- | Return a range containing all indices in the context.
allRange :: Size ctx -> IndexRange ctx ctx
allRange :: forall {k} (ctx :: Ctx k). Size ctx -> IndexRange ctx ctx
allRange (Size Int
n) = forall k (ctx :: Ctx k) (sub :: Ctx k).
Int -> Int -> IndexRange ctx sub
IndexRange Int
0 Int
n

-- | `indexOfRange` returns the only index in a range.
indexOfRange :: IndexRange ctx (EmptyCtx ::> e) -> Index ctx e
indexOfRange :: forall {k} (ctx :: Ctx k) (e :: k).
IndexRange ctx (EmptyCtx ::> e) -> Index ctx e
indexOfRange (IndexRange Int
i Int
n) = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
n forall a. Eq a => a -> a -> Bool
== Int
1) forall a b. (a -> b) -> a -> b
$ forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index Int
i

-- | @dropTailRange r n@ drops the last @n@ elements in @r@.
dropTailRange :: IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x
dropTailRange :: forall {k} (ctx :: Ctx k) (x :: Ctx k) (y :: Ctx k).
IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x
dropTailRange (IndexRange Int
i Int
n) (Size Int
j) = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
n forall a. Ord a => a -> a -> Bool
>= Int
j) forall a b. (a -> b) -> a -> b
$ forall k (ctx :: Ctx k) (sub :: Ctx k).
Int -> Int -> IndexRange ctx sub
IndexRange Int
i (Int
n forall a. Num a => a -> a -> a
- Int
j)

-- | @dropHeadRange r n@ drops the first @n@ elements in @r@.
dropHeadRange :: IndexRange ctx (x <+> y) -> Size x -> IndexRange ctx y
dropHeadRange :: forall {k} (ctx :: Ctx k) (x :: Ctx k) (y :: Ctx k).
IndexRange ctx (x <+> y) -> Size x -> IndexRange ctx y
dropHeadRange (IndexRange Int
i Int
n) (Size Int
j) = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
i' forall a. Ord a => a -> a -> Bool
>= Int
i Bool -> Bool -> Bool
&& Int
n forall a. Ord a => a -> a -> Bool
>= Int
j) forall a b. (a -> b) -> a -> b
$ forall k (ctx :: Ctx k) (sub :: Ctx k).
Int -> Int -> IndexRange ctx sub
IndexRange Int
i' (Int
n forall a. Num a => a -> a -> a
- Int
j)
  where i' :: Int
i' = Int
i forall a. Num a => a -> a -> a
+ Int
j

------------------------------------------------------------------------
-- Height

data Height = Zero | Succ Height

type family Pred (k :: Height) :: Height
type instance Pred ('Succ h) = h

------------------------------------------------------------------------
-- * BalancedTree

-- | A balanced tree where all leaves are at the same height.
--
-- The first parameter is the height of the tree.
-- The second is the parameterized value.
data BalancedTree h (f :: k -> Type) (p :: Ctx k) where
  BalLeaf :: !(f x) -> BalancedTree 'Zero f (SingleCtx x)
  BalPair :: !(BalancedTree h f x)
          -> !(BalancedTree h f y)
          -> BalancedTree ('Succ h) f (x <+> y)

bal_size :: BalancedTree h f p -> Int
bal_size :: forall {k} (h :: Height) (f :: k -> *) (p :: Ctx k).
BalancedTree h f p -> Int
bal_size (BalLeaf f x
_) = Int
1
bal_size (BalPair BalancedTree h f x
x BalancedTree h f y
y) = forall {k} (h :: Height) (f :: k -> *) (p :: Ctx k).
BalancedTree h f p -> Int
bal_size BalancedTree h f x
x forall a. Num a => a -> a -> a
+ forall {k} (h :: Height) (f :: k -> *) (p :: Ctx k).
BalancedTree h f p -> Int
bal_size BalancedTree h f y
y


instance TestEqualityFC (BalancedTree h) where
  testEqualityFC :: forall (f :: k -> *).
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> forall (x :: Ctx k) (y :: Ctx k).
   BalancedTree h f x -> BalancedTree h f y -> Maybe (x :~: y)
testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test (BalLeaf f x
x) (BalLeaf f x
y) = do
    x :~: x
Refl <- forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test f x
x f x
y
    forall (m :: * -> *) a. Monad m => a -> m a
return forall {k} (a :: k). a :~: a
Refl
  testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test (BalPair BalancedTree h f x
x1 BalancedTree h f y
x2) (BalPair BalancedTree h f x
y1 BalancedTree h f y
y2) = do
    x :~: x
Refl <- forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
TestEqualityFC t =>
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> forall (x :: l) (y :: l). t f x -> t f y -> Maybe (x :~: y)
testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test BalancedTree h f x
x1 BalancedTree h f x
y1
    y :~: y
Refl <- forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
TestEqualityFC t =>
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> forall (x :: l) (y :: l). t f x -> t f y -> Maybe (x :~: y)
testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test BalancedTree h f y
x2 BalancedTree h f y
y2
    forall (m :: * -> *) a. Monad m => a -> m a
return forall {k} (a :: k). a :~: a
Refl

instance OrdFC (BalancedTree h) where
  compareFC :: forall (f :: k -> *).
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> forall (x :: Ctx k) (y :: Ctx k).
   BalancedTree h f x -> BalancedTree h f y -> OrderingF x y
compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test (BalLeaf f x
x) (BalLeaf f x
y) =
    forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test f x
x f x
y) forall a b. (a -> b) -> a -> b
$ forall {k} (x :: k). OrderingF x x
EQF
  compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test (BalPair BalancedTree h f x
x1 BalancedTree h f y
x2) (BalPair BalancedTree h f x
y1 BalancedTree h f y
y2) =
    forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
OrdFC t =>
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF x y
compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test BalancedTree h f x
x1 BalancedTree h f x
y1) forall a b. (a -> b) -> a -> b
$
    forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
OrdFC t =>
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF x y
compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test BalancedTree h f y
x2 BalancedTree h f y
y2) forall a b. (a -> b) -> a -> b
$
    forall {k} (x :: k). OrderingF x x
EQF

instance HashableF f => HashableF (BalancedTree h f) where
  hashWithSaltF :: forall (tp :: Ctx k). Int -> BalancedTree h f tp -> Int
hashWithSaltF Int
s BalancedTree h f tp
t =
    case BalancedTree h f tp
t of
      BalLeaf f x
x -> Int
s forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
`hashWithSaltF` f x
x
      BalPair BalancedTree h f x
x BalancedTree h f y
y -> Int
s forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
`hashWithSaltF` BalancedTree h f x
x forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
`hashWithSaltF` BalancedTree h f y
y

fmap_bal :: (forall tp . f tp -> g tp)
         -> BalancedTree h f c
         -> BalancedTree h g c
fmap_bal :: forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
(forall (tp :: k). f tp -> g tp)
-> BalancedTree h f c -> BalancedTree h g c
fmap_bal = forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
(forall (tp :: k). f tp -> g tp)
-> BalancedTree h f c -> BalancedTree h g c
go
  where go :: (forall tp . f tp -> g tp)
              -> BalancedTree h f c
              -> BalancedTree h g c
        go :: forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
(forall (tp :: k). f tp -> g tp)
-> BalancedTree h f c -> BalancedTree h g c
go forall (tp :: k). f tp -> g tp
f (BalLeaf f x
x) = forall {k} (f :: k -> *) (ctx :: k).
f ctx -> BalancedTree 'Zero f (SingleCtx ctx)
BalLeaf (forall (tp :: k). f tp -> g tp
f f x
x)
        go forall (tp :: k). f tp -> g tp
f (BalPair BalancedTree h f x
x BalancedTree h f y
y) = forall {k} (ctx :: Height) (f :: k -> *) (tp :: Ctx k)
       (y :: Ctx k).
BalancedTree ctx f tp
-> BalancedTree ctx f y -> BalancedTree ('Succ ctx) f (tp <+> y)
BalPair (forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
(forall (tp :: k). f tp -> g tp)
-> BalancedTree h f c -> BalancedTree h g c
go forall (tp :: k). f tp -> g tp
f BalancedTree h f x
x) (forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
(forall (tp :: k). f tp -> g tp)
-> BalancedTree h f c -> BalancedTree h g c
go forall (tp :: k). f tp -> g tp
f BalancedTree h f y
y)
{-# INLINABLE fmap_bal #-}

traverse_bal :: Applicative m
             => (forall tp . f tp -> m (g tp))
             -> BalancedTree h f c
             -> m (BalancedTree h g c)
traverse_bal :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
       (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> m (g tp))
-> BalancedTree h f c -> m (BalancedTree h g c)
traverse_bal = forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
       (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> m (g tp))
-> BalancedTree h f c -> m (BalancedTree h g c)
go
  where go :: Applicative m
              => (forall tp . f tp -> m (g tp))
              -> BalancedTree h f c
              -> m (BalancedTree h g c)
        go :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
       (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> m (g tp))
-> BalancedTree h f c -> m (BalancedTree h g c)
go forall (tp :: k). f tp -> m (g tp)
f (BalLeaf f x
x) = forall {k} (f :: k -> *) (ctx :: k).
f ctx -> BalancedTree 'Zero f (SingleCtx ctx)
BalLeaf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tp :: k). f tp -> m (g tp)
f f x
x
        go forall (tp :: k). f tp -> m (g tp)
f (BalPair BalancedTree h f x
x BalancedTree h f y
y) = forall {k} (ctx :: Height) (f :: k -> *) (tp :: Ctx k)
       (y :: Ctx k).
BalancedTree ctx f tp
-> BalancedTree ctx f y -> BalancedTree ('Succ ctx) f (tp <+> y)
BalPair forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
       (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> m (g tp))
-> BalancedTree h f c -> m (BalancedTree h g c)
go forall (tp :: k). f tp -> m (g tp)
f BalancedTree h f x
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
       (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> m (g tp))
-> BalancedTree h f c -> m (BalancedTree h g c)
go forall (tp :: k). f tp -> m (g tp)
f BalancedTree h f y
y
{-# INLINABLE traverse_bal #-}

instance ShowF f => Show (BalancedTree h f tp) where
  show :: BalancedTree h f tp -> String
show (BalLeaf f x
x) = forall k (f :: k -> *) (tp :: k). ShowF f => f tp -> String
showF f x
x
  show (BalPair BalancedTree h f x
x BalancedTree h f y
y) = String
"BalPair " forall a. [a] -> [a] -> [a]
Prelude.++ forall a. Show a => a -> String
show BalancedTree h f x
x forall a. [a] -> [a] -> [a]
Prelude.++ String
" " forall a. [a] -> [a] -> [a]
Prelude.++ forall a. Show a => a -> String
show BalancedTree h f y
y

instance ShowF f => ShowF (BalancedTree h f)

unsafe_bal_generate :: forall ctx h f t
                     . Int -- ^ Height of tree to generate
                    -> Int -- ^ Starting offset for entries.
                    -> (forall tp . Index ctx tp -> f tp)
                    -> BalancedTree h f t
unsafe_bal_generate :: forall {k} (ctx :: Ctx k) (h :: Height) (f :: k -> *) (t :: Ctx k).
Int
-> Int
-> (forall (tp :: k). Index ctx tp -> f tp)
-> BalancedTree h f t
unsafe_bal_generate Int
h Int
o forall (tp :: k). Index ctx tp -> f tp
f
  | Int
h forall a. Ord a => a -> a -> Bool
<  Int
0 = forall a. (?callStack::CallStack) => String -> a
error String
"unsafe_bal_generate given negative height"
  | Int
h forall a. Eq a => a -> a -> Bool
== Int
0 = forall a b. a -> b
unsafeCoerce forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> *) (ctx :: k).
f ctx -> BalancedTree 'Zero f (SingleCtx ctx)
BalLeaf (forall (tp :: k). Index ctx tp -> f tp
f (forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index Int
o))
  | Bool
otherwise =
    let l :: BalancedTree Any f Any
l = forall {k} (ctx :: Ctx k) (h :: Height) (f :: k -> *) (t :: Ctx k).
Int
-> Int
-> (forall (tp :: k). Index ctx tp -> f tp)
-> BalancedTree h f t
unsafe_bal_generate (Int
hforall a. Num a => a -> a -> a
-Int
1) Int
o forall (tp :: k). Index ctx tp -> f tp
f
        o' :: Int
o' = Int
o forall a. Num a => a -> a -> a
+ Int
1 forall a. Bits a => a -> Int -> a
`shiftL` (Int
hforall a. Num a => a -> a -> a
-Int
1)
        u :: BalancedTree Any f Any
u = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
o forall a. Num a => a -> a -> a
+ forall {k} (h :: Height) (f :: k -> *) (p :: Ctx k).
BalancedTree h f p -> Int
bal_size BalancedTree Any f Any
l forall a. Eq a => a -> a -> Bool
== Int
o') forall a b. (a -> b) -> a -> b
$ forall {k} (ctx :: Ctx k) (h :: Height) (f :: k -> *) (t :: Ctx k).
Int
-> Int
-> (forall (tp :: k). Index ctx tp -> f tp)
-> BalancedTree h f t
unsafe_bal_generate (Int
hforall a. Num a => a -> a -> a
-Int
1) Int
o' forall (tp :: k). Index ctx tp -> f tp
f
     in forall a b. a -> b
unsafeCoerce forall a b. (a -> b) -> a -> b
$ forall {k} (ctx :: Height) (f :: k -> *) (tp :: Ctx k)
       (y :: Ctx k).
BalancedTree ctx f tp
-> BalancedTree ctx f y -> BalancedTree ('Succ ctx) f (tp <+> y)
BalPair BalancedTree Any f Any
l BalancedTree Any f Any
u

unsafe_bal_generateM :: forall m ctx h f t
                      . Applicative m
                     => Int -- ^ Height of tree to generate
                     -> Int -- ^ Starting offset for entries.
                     -> (forall x . Index ctx x -> m (f x))
                     -> m (BalancedTree h f t)
unsafe_bal_generateM :: forall {k} (m :: * -> *) (ctx :: Ctx k) (h :: Height) (f :: k -> *)
       (t :: Ctx k).
Applicative m =>
Int
-> Int
-> (forall (x :: k). Index ctx x -> m (f x))
-> m (BalancedTree h f t)
unsafe_bal_generateM Int
h Int
o forall (x :: k). Index ctx x -> m (f x)
f
  | Int
h forall a. Eq a => a -> a -> Bool
== Int
0 = forall a b. a -> b
unsafeCoerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (ctx :: k).
f ctx -> BalancedTree 'Zero f (SingleCtx ctx)
BalLeaf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (x :: k). Index ctx x -> m (f x)
f (forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index Int
o)
  | Bool
otherwise =
    let o' :: Int
o' = Int
o forall a. Num a => a -> a -> a
+ Int
1 forall a. Bits a => a -> Int -> a
`shiftL` (Int
hforall a. Num a => a -> a -> a
-Int
1)
        g :: BalancedTree Any f Any
-> BalancedTree Any f Any -> BalancedTree h f t
g BalancedTree Any f Any
lv BalancedTree Any f Any
uv = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
o' forall a. Eq a => a -> a -> Bool
== Int
o forall a. Num a => a -> a -> a
+ forall {k} (h :: Height) (f :: k -> *) (p :: Ctx k).
BalancedTree h f p -> Int
bal_size BalancedTree Any f Any
lv) forall a b. (a -> b) -> a -> b
$
           forall a b. a -> b
unsafeCoerce (forall {k} (ctx :: Height) (f :: k -> *) (tp :: Ctx k)
       (y :: Ctx k).
BalancedTree ctx f tp
-> BalancedTree ctx f y -> BalancedTree ('Succ ctx) f (tp <+> y)
BalPair BalancedTree Any f Any
lv BalancedTree Any f Any
uv)
      in BalancedTree Any f Any
-> BalancedTree Any f Any -> BalancedTree h f t
g forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (m :: * -> *) (ctx :: Ctx k) (h :: Height) (f :: k -> *)
       (t :: Ctx k).
Applicative m =>
Int
-> Int
-> (forall (x :: k). Index ctx x -> m (f x))
-> m (BalancedTree h f t)
unsafe_bal_generateM (Int
hforall a. Num a => a -> a -> a
-Int
1) Int
o  forall (x :: k). Index ctx x -> m (f x)
f
           forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {k} (m :: * -> *) (ctx :: Ctx k) (h :: Height) (f :: k -> *)
       (t :: Ctx k).
Applicative m =>
Int
-> Int
-> (forall (x :: k). Index ctx x -> m (f x))
-> m (BalancedTree h f t)
unsafe_bal_generateM (Int
hforall a. Num a => a -> a -> a
-Int
1) Int
o' forall (x :: k). Index ctx x -> m (f x)
f

-- | Lookup index in tree.
unsafe_bal_index :: BalancedTree h f a -- ^ Tree to lookup.
                 -> Int -- ^ Index to lookup.
                 -> Int  -- ^ Height of tree
                 -> f tp
unsafe_bal_index :: forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k) (tp :: k).
BalancedTree h f a -> Int -> Int -> f tp
unsafe_bal_index BalancedTree h f a
_ Int
j Int
i
  | seq :: forall a b. a -> b -> b
seq Int
j forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq Int
i forall a b. (a -> b) -> a -> b
$ Bool
False = forall a. (?callStack::CallStack) => String -> a
error String
"bad unsafe_bal_index"
unsafe_bal_index (BalLeaf f x
u) Int
_ Int
i = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
i forall a. Eq a => a -> a -> Bool
== Int
0) forall a b. (a -> b) -> a -> b
$ forall a b. a -> b
unsafeCoerce f x
u
unsafe_bal_index (BalPair BalancedTree h f x
x BalancedTree h f y
y) Int
j Int
i
  | Int
j forall a. Bits a => a -> Int -> Bool
`testBit` (Int
iforall a. Num a => a -> a -> a
-Int
1) = forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k) (tp :: k).
BalancedTree h f a -> Int -> Int -> f tp
unsafe_bal_index BalancedTree h f y
y Int
j forall a b. (a -> b) -> a -> b
$! (Int
iforall a. Num a => a -> a -> a
-Int
1)
  | Bool
otherwise         = forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k) (tp :: k).
BalancedTree h f a -> Int -> Int -> f tp
unsafe_bal_index BalancedTree h f x
x Int
j forall a b. (a -> b) -> a -> b
$! (Int
iforall a. Num a => a -> a -> a
-Int
1)

-- | Update value at index in tree.
unsafe_bal_adjust :: Functor m
                  => (f x -> m (f y))
                  -> BalancedTree h f a -- ^ Tree to update
                  -> Int -- ^ Index to lookup.
                  -> Int  -- ^ Height of tree
                  -> m (BalancedTree h f b)
unsafe_bal_adjust :: forall {k} (m :: * -> *) (f :: k -> *) (x :: k) (y :: k)
       (h :: Height) (a :: Ctx k) (b :: Ctx k).
Functor m =>
(f x -> m (f y))
-> BalancedTree h f a -> Int -> Int -> m (BalancedTree h f b)
unsafe_bal_adjust f x -> m (f y)
f (BalLeaf f x
u) Int
_ Int
i = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
i forall a. Eq a => a -> a -> Bool
== Int
0) forall a b. (a -> b) -> a -> b
$
  (forall a b. a -> b
unsafeCoerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (ctx :: k).
f ctx -> BalancedTree 'Zero f (SingleCtx ctx)
BalLeaf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (f x -> m (f y)
f (forall a b. a -> b
unsafeCoerce f x
u)))
unsafe_bal_adjust f x -> m (f y)
f (BalPair BalancedTree h f x
x BalancedTree h f y
y) Int
j Int
i
  | Int
j forall a. Bits a => a -> Int -> Bool
`testBit` (Int
iforall a. Num a => a -> a -> a
-Int
1) = (forall a b. a -> b
unsafeCoerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (ctx :: Height) (f :: k -> *) (tp :: Ctx k)
       (y :: Ctx k).
BalancedTree ctx f tp
-> BalancedTree ctx f y -> BalancedTree ('Succ ctx) f (tp <+> y)
BalPair BalancedTree h f x
x      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall {k} (m :: * -> *) (f :: k -> *) (x :: k) (y :: k)
       (h :: Height) (a :: Ctx k) (b :: Ctx k).
Functor m =>
(f x -> m (f y))
-> BalancedTree h f a -> Int -> Int -> m (BalancedTree h f b)
unsafe_bal_adjust f x -> m (f y)
f BalancedTree h f y
y Int
j (Int
iforall a. Num a => a -> a -> a
-Int
1)))
  | Bool
otherwise         = (forall a b. a -> b
unsafeCoerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall {k} (ctx :: Height) (f :: k -> *) (tp :: Ctx k)
       (y :: Ctx k).
BalancedTree ctx f tp
-> BalancedTree ctx f y -> BalancedTree ('Succ ctx) f (tp <+> y)
BalPair BalancedTree h f y
y forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall {k} (m :: * -> *) (f :: k -> *) (x :: k) (y :: k)
       (h :: Height) (a :: Ctx k) (b :: Ctx k).
Functor m =>
(f x -> m (f y))
-> BalancedTree h f a -> Int -> Int -> m (BalancedTree h f b)
unsafe_bal_adjust f x -> m (f y)
f BalancedTree h f x
x Int
j (Int
iforall a. Num a => a -> a -> a
-Int
1)))

{-# SPECIALIZE unsafe_bal_adjust
     :: (f x -> Identity (f y))
     -> BalancedTree h f a
     -> Int
     -> Int
     -> Identity (BalancedTree h f b)
  #-}

-- | Zip two balanced trees together.
bal_zipWithM :: Applicative m
             => (forall x . f x -> g x -> m (h x))
             -> BalancedTree u f a
             -> BalancedTree u g a
             -> m (BalancedTree u h a)
bal_zipWithM :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (u :: Height) (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> BalancedTree u f a
-> BalancedTree u g a
-> m (BalancedTree u h a)
bal_zipWithM forall (x :: k). f x -> g x -> m (h x)
f (BalLeaf f x
x) (BalLeaf g x
y) = forall {k} (f :: k -> *) (ctx :: k).
f ctx -> BalancedTree 'Zero f (SingleCtx ctx)
BalLeaf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (x :: k). f x -> g x -> m (h x)
f f x
x g x
y
bal_zipWithM forall (x :: k). f x -> g x -> m (h x)
f (BalPair BalancedTree h f x
x1 BalancedTree h f y
x2) (BalPair BalancedTree h g x
y1 BalancedTree h g y
y2) =
  forall {k} (ctx :: Height) (f :: k -> *) (tp :: Ctx k)
       (y :: Ctx k).
BalancedTree ctx f tp
-> BalancedTree ctx f y -> BalancedTree ('Succ ctx) f (tp <+> y)
BalPair forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (u :: Height) (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> BalancedTree u f a
-> BalancedTree u g a
-> m (BalancedTree u h a)
bal_zipWithM forall (x :: k). f x -> g x -> m (h x)
f BalancedTree h f x
x1 (forall a b. a -> b
unsafeCoerce BalancedTree h g x
y1)
          forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (u :: Height) (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> BalancedTree u f a
-> BalancedTree u g a
-> m (BalancedTree u h a)
bal_zipWithM forall (x :: k). f x -> g x -> m (h x)
f BalancedTree h f y
x2 (forall a b. a -> b
unsafeCoerce BalancedTree h g y
y2)
{-# INLINABLE bal_zipWithM #-}

------------------------------------------------------------------------
-- * BinomialTree

data BinomialTree (h::Height) (f :: k -> Type) :: Ctx k -> Type where
  Empty :: BinomialTree h f EmptyCtx

  -- Contains size of the subtree, subtree, then element.
  PlusOne  :: !Int
           -> !(BinomialTree ('Succ h) f x)
           -> !(BalancedTree h f y)
           -> BinomialTree h f (x <+> y)

  -- Contains size of the subtree, subtree, then element.
  PlusZero  :: !Int
            -> !(BinomialTree ('Succ h) f x)
            -> BinomialTree h f x

tsize :: BinomialTree h f a -> Int
tsize :: forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k).
BinomialTree h f a -> Int
tsize BinomialTree h f a
Empty = Int
0
tsize (PlusOne Int
s BinomialTree ('Succ h) f x
_ BalancedTree h f y
_) = Int
2forall a. Num a => a -> a -> a
*Int
sforall a. Num a => a -> a -> a
+Int
1
tsize (PlusZero  Int
s BinomialTree ('Succ h) f a
_) = Int
2forall a. Num a => a -> a -> a
*Int
s

t_cnt_size :: BinomialTree h f a -> Int
t_cnt_size :: forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k).
BinomialTree h f a -> Int
t_cnt_size BinomialTree h f a
Empty = Int
0
t_cnt_size (PlusOne Int
_ BinomialTree ('Succ h) f x
l BalancedTree h f y
r) = forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k).
BinomialTree h f a -> Int
t_cnt_size BinomialTree ('Succ h) f x
l forall a. Num a => a -> a -> a
+ forall {k} (h :: Height) (f :: k -> *) (p :: Ctx k).
BalancedTree h f p -> Int
bal_size BalancedTree h f y
r
t_cnt_size (PlusZero  Int
_ BinomialTree ('Succ h) f a
l) = forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k).
BinomialTree h f a -> Int
t_cnt_size BinomialTree ('Succ h) f a
l

-- | Concatenate a binomial tree and a balanced tree.
append :: BinomialTree h f x
       -> BalancedTree h f y
       -> BinomialTree h f (x <+> y)
append :: forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
BinomialTree h f x
-> BalancedTree h f y -> BinomialTree h f (x <+> y)
append BinomialTree h f x
Empty BalancedTree h f y
y = forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
       (tp :: Ctx k).
Int
-> BinomialTree ('Succ h) f ctx
-> BalancedTree h f tp
-> BinomialTree h f (ctx <+> tp)
PlusOne Int
0 forall {k} (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
Empty BalancedTree h f y
y
append (PlusOne Int
_ BinomialTree ('Succ h) f x
t BalancedTree h f y
x) BalancedTree h f y
y =
  case forall {k} (p :: Ctx k -> *) (x :: Ctx k) (q :: Ctx k -> *)
       (y :: Ctx k) (r :: Ctx k -> *) (z :: Ctx k).
p x -> q y -> r z -> (x <+> (y <+> z)) :~: ((x <+> y) <+> z)
assoc BinomialTree ('Succ h) f x
t BalancedTree h f y
x BalancedTree h f y
y of
    (x <+> (y <+> y)) :~: ((x <+> y) <+> y)
Refl ->
      let t' :: BinomialTree ('Succ h) f (x <+> (y <+> y))
t' = forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
BinomialTree h f x
-> BalancedTree h f y -> BinomialTree h f (x <+> y)
append BinomialTree ('Succ h) f x
t (forall {k} (ctx :: Height) (f :: k -> *) (tp :: Ctx k)
       (y :: Ctx k).
BalancedTree ctx f tp
-> BalancedTree ctx f y -> BalancedTree ('Succ ctx) f (tp <+> y)
BalPair BalancedTree h f y
x BalancedTree h f y
y)
       in forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k).
Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
PlusZero (forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k).
BinomialTree h f a -> Int
tsize BinomialTree ('Succ h) f (x <+> (y <+> y))
t') BinomialTree ('Succ h) f (x <+> (y <+> y))
t'
append (PlusZero Int
s BinomialTree ('Succ h) f x
t) BalancedTree h f y
x = forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
       (tp :: Ctx k).
Int
-> BinomialTree ('Succ h) f ctx
-> BalancedTree h f tp
-> BinomialTree h f (ctx <+> tp)
PlusOne Int
s BinomialTree ('Succ h) f x
t BalancedTree h f y
x

instance TestEqualityFC (BinomialTree h) where
  testEqualityFC :: forall (f :: k -> *).
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> forall (x :: Ctx k) (y :: Ctx k).
   BinomialTree h f x -> BinomialTree h f y -> Maybe (x :~: y)
testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
_ BinomialTree h f x
Empty BinomialTree h f y
Empty = forall (m :: * -> *) a. Monad m => a -> m a
return forall {k} (a :: k). a :~: a
Refl
  testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test (PlusZero Int
_ BinomialTree ('Succ h) f x
x1) (PlusZero Int
_ BinomialTree ('Succ h) f y
y1) = do
    x :~: y
Refl <- forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
TestEqualityFC t =>
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> forall (x :: l) (y :: l). t f x -> t f y -> Maybe (x :~: y)
testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test BinomialTree ('Succ h) f x
x1 BinomialTree ('Succ h) f y
y1
    forall (m :: * -> *) a. Monad m => a -> m a
return forall {k} (a :: k). a :~: a
Refl
  testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test (PlusOne Int
_ BinomialTree ('Succ h) f x
x1 BalancedTree h f y
x2) (PlusOne Int
_ BinomialTree ('Succ h) f x
y1 BalancedTree h f y
y2) = do
    x :~: x
Refl <- forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
TestEqualityFC t =>
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> forall (x :: l) (y :: l). t f x -> t f y -> Maybe (x :~: y)
testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test BinomialTree ('Succ h) f x
x1 BinomialTree ('Succ h) f x
y1
    y :~: y
Refl <- forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
TestEqualityFC t =>
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> forall (x :: l) (y :: l). t f x -> t f y -> Maybe (x :~: y)
testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test BalancedTree h f y
x2 BalancedTree h f y
y2
    forall (m :: * -> *) a. Monad m => a -> m a
return forall {k} (a :: k). a :~: a
Refl
  testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
_ BinomialTree h f x
_ BinomialTree h f y
_ = forall a. Maybe a
Nothing

instance OrdFC (BinomialTree h) where
  compareFC :: forall (f :: k -> *).
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> forall (x :: Ctx k) (y :: Ctx k).
   BinomialTree h f x -> BinomialTree h f y -> OrderingF x y
compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
_ BinomialTree h f x
Empty BinomialTree h f y
Empty = forall {k} (x :: k). OrderingF x x
EQF
  compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
_ BinomialTree h f x
Empty BinomialTree h f y
_ = forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
_ BinomialTree h f x
_ BinomialTree h f y
Empty = forall {k} (x :: k) (y :: k). OrderingF x y
GTF

  compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test (PlusZero Int
_ BinomialTree ('Succ h) f x
x1) (PlusZero Int
_ BinomialTree ('Succ h) f y
y1) =
    forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
OrdFC t =>
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF x y
compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test BinomialTree ('Succ h) f x
x1 BinomialTree ('Succ h) f y
y1) forall a b. (a -> b) -> a -> b
$ forall {k} (x :: k). OrderingF x x
EQF
  compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
_ PlusZero{} BinomialTree h f y
_ = forall {k} (x :: k) (y :: k). OrderingF x y
LTF
  compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
_ BinomialTree h f x
_ PlusZero{} = forall {k} (x :: k) (y :: k). OrderingF x y
GTF

  compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test (PlusOne Int
_ BinomialTree ('Succ h) f x
x1 BalancedTree h f y
x2) (PlusOne Int
_ BinomialTree ('Succ h) f x
y1 BalancedTree h f y
y2) =
    forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
OrdFC t =>
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF x y
compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test BinomialTree ('Succ h) f x
x1 BinomialTree ('Succ h) f x
y1) forall a b. (a -> b) -> a -> b
$
    forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
OrdFC t =>
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF x y
compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test BalancedTree h f y
x2 BalancedTree h f y
y2) forall a b. (a -> b) -> a -> b
$
    forall {k} (x :: k). OrderingF x x
EQF

instance HashableF f => HashableF (BinomialTree h f) where
  hashWithSaltF :: forall (tp :: Ctx k). Int -> BinomialTree h f tp -> Int
hashWithSaltF Int
s BinomialTree h f tp
t =
    case BinomialTree h f tp
t of
      BinomialTree h f tp
Empty -> Int
s
      PlusZero Int
_ BinomialTree ('Succ h) f tp
x   -> Int
s forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
`hashWithSaltF` BinomialTree ('Succ h) f tp
x
      PlusOne  Int
_ BinomialTree ('Succ h) f x
x BalancedTree h f y
y -> Int
s forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
`hashWithSaltF` BinomialTree ('Succ h) f x
x forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
`hashWithSaltF` BalancedTree h f y
y

-- | Map over a binary tree.
fmap_bin :: (forall tp . f tp -> g tp)
         -> BinomialTree h f c
         -> BinomialTree h g c
fmap_bin :: forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
(forall (tp :: k). f tp -> g tp)
-> BinomialTree h f c -> BinomialTree h g c
fmap_bin forall (tp :: k). f tp -> g tp
_ BinomialTree h f c
Empty = forall {k} (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
Empty
fmap_bin forall (tp :: k). f tp -> g tp
f (PlusOne Int
s BinomialTree ('Succ h) f x
t BalancedTree h f y
x) = forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
       (tp :: Ctx k).
Int
-> BinomialTree ('Succ h) f ctx
-> BalancedTree h f tp
-> BinomialTree h f (ctx <+> tp)
PlusOne Int
s (forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
(forall (tp :: k). f tp -> g tp)
-> BinomialTree h f c -> BinomialTree h g c
fmap_bin forall (tp :: k). f tp -> g tp
f BinomialTree ('Succ h) f x
t) (forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
(forall (tp :: k). f tp -> g tp)
-> BalancedTree h f c -> BalancedTree h g c
fmap_bal forall (tp :: k). f tp -> g tp
f BalancedTree h f y
x)
fmap_bin forall (tp :: k). f tp -> g tp
f (PlusZero Int
s BinomialTree ('Succ h) f c
t)  = forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k).
Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
PlusZero Int
s (forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
(forall (tp :: k). f tp -> g tp)
-> BinomialTree h f c -> BinomialTree h g c
fmap_bin forall (tp :: k). f tp -> g tp
f BinomialTree ('Succ h) f c
t)
{-# INLINABLE fmap_bin #-}

traverse_bin :: Applicative m
             => (forall tp . f tp -> m (g tp))
             -> BinomialTree h f c
             -> m (BinomialTree h g c)
traverse_bin :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
       (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> m (g tp))
-> BinomialTree h f c -> m (BinomialTree h g c)
traverse_bin forall (tp :: k). f tp -> m (g tp)
_ BinomialTree h f c
Empty = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
Empty
traverse_bin forall (tp :: k). f tp -> m (g tp)
f (PlusOne Int
s BinomialTree ('Succ h) f x
t BalancedTree h f y
x) = forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
       (tp :: Ctx k).
Int
-> BinomialTree ('Succ h) f ctx
-> BalancedTree h f tp
-> BinomialTree h f (ctx <+> tp)
PlusOne Int
s  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
       (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> m (g tp))
-> BinomialTree h f c -> m (BinomialTree h g c)
traverse_bin forall (tp :: k). f tp -> m (g tp)
f BinomialTree ('Succ h) f x
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
       (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> m (g tp))
-> BalancedTree h f c -> m (BalancedTree h g c)
traverse_bal forall (tp :: k). f tp -> m (g tp)
f BalancedTree h f y
x
traverse_bin forall (tp :: k). f tp -> m (g tp)
f (PlusZero Int
s BinomialTree ('Succ h) f c
t)  = forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k).
Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
PlusZero Int
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
       (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> m (g tp))
-> BinomialTree h f c -> m (BinomialTree h g c)
traverse_bin forall (tp :: k). f tp -> m (g tp)
f BinomialTree ('Succ h) f c
t
{-# INLINABLE traverse_bin #-}

unsafe_bin_generate :: forall h f ctx t
                     . Int -- ^ Size of tree to generate
                    -> Int -- ^ Height of each element.
                    -> (forall x . Index ctx x -> f x)
                    -> BinomialTree h f t
unsafe_bin_generate :: forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k) (t :: Ctx k).
Int
-> Int
-> (forall (x :: k). Index ctx x -> f x)
-> BinomialTree h f t
unsafe_bin_generate Int
sz Int
h forall (x :: k). Index ctx x -> f x
f
  | Int
sz forall a. Eq a => a -> a -> Bool
== Int
0 = forall a b. a -> b
unsafeCoerce forall {k} (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
Empty
  | Int
sz forall a. Bits a => a -> Int -> Bool
`testBit` Int
0 =
    let s :: Int
s = Int
sz forall a. Bits a => a -> Int -> a
`shiftR` Int
1
        t :: BinomialTree ('Succ Any) f Any
t = forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k) (t :: Ctx k).
Int
-> Int
-> (forall (x :: k). Index ctx x -> f x)
-> BinomialTree h f t
unsafe_bin_generate Int
s (Int
hforall a. Num a => a -> a -> a
+Int
1) forall (x :: k). Index ctx x -> f x
f
        o :: Int
o = Int
s forall a. Num a => a -> a -> a
* Int
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
hforall a. Num a => a -> a -> a
+Int
1)
        u :: BalancedTree Any f Any
u = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
o forall a. Eq a => a -> a -> Bool
== forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k).
BinomialTree h f a -> Int
t_cnt_size BinomialTree ('Succ Any) f Any
t) forall a b. (a -> b) -> a -> b
$ forall {k} (ctx :: Ctx k) (h :: Height) (f :: k -> *) (t :: Ctx k).
Int
-> Int
-> (forall (tp :: k). Index ctx tp -> f tp)
-> BalancedTree h f t
unsafe_bal_generate Int
h Int
o forall (x :: k). Index ctx x -> f x
f
     in forall a b. a -> b
unsafeCoerce (forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
       (tp :: Ctx k).
Int
-> BinomialTree ('Succ h) f ctx
-> BalancedTree h f tp
-> BinomialTree h f (ctx <+> tp)
PlusOne Int
s BinomialTree ('Succ Any) f Any
t BalancedTree Any f Any
u)
  | Bool
otherwise =
    let s :: Int
s = Int
sz forall a. Bits a => a -> Int -> a
`shiftR` Int
1
        t :: BinomialTree ('Succ h) f t
t = forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k) (t :: Ctx k).
Int
-> Int
-> (forall (x :: k). Index ctx x -> f x)
-> BinomialTree h f t
unsafe_bin_generate (Int
sz forall a. Bits a => a -> Int -> a
`shiftR` Int
1) (Int
hforall a. Num a => a -> a -> a
+Int
1) forall (x :: k). Index ctx x -> f x
f
        r :: BinomialTree h f t
        r :: BinomialTree h f t
r = forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k).
Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
PlusZero Int
s BinomialTree ('Succ h) f t
t
    in BinomialTree h f t
r

unsafe_bin_generateM :: forall m h f ctx t
                      . Applicative m
                     => Int -- ^ Size of tree to generate
                     -> Int -- ^ Height of each element.
                     -> (forall x . Index ctx x -> m (f x))
                     -> m (BinomialTree h f t)
unsafe_bin_generateM :: forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (ctx :: Ctx k)
       (t :: Ctx k).
Applicative m =>
Int
-> Int
-> (forall (x :: k). Index ctx x -> m (f x))
-> m (BinomialTree h f t)
unsafe_bin_generateM Int
sz Int
h forall (x :: k). Index ctx x -> m (f x)
f
  | Int
sz forall a. Eq a => a -> a -> Bool
== Int
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> b
unsafeCoerce forall {k} (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
Empty)
  | Int
sz forall a. Bits a => a -> Int -> Bool
`testBit` Int
0 =
    let s :: Int
s = Int
sz forall a. Bits a => a -> Int -> a
`shiftR` Int
1
        t :: m (BinomialTree Any f Any)
t = forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (ctx :: Ctx k)
       (t :: Ctx k).
Applicative m =>
Int
-> Int
-> (forall (x :: k). Index ctx x -> m (f x))
-> m (BinomialTree h f t)
unsafe_bin_generateM Int
s (Int
hforall a. Num a => a -> a -> a
+Int
1) forall (x :: k). Index ctx x -> m (f x)
f
        -- Next offset
        o :: Int
o = Int
s forall a. Num a => a -> a -> a
* Int
2forall a b. (Num a, Integral b) => a -> b -> a
^(Int
hforall a. Num a => a -> a -> a
+Int
1)
        u :: m (BalancedTree Any f Any)
u = forall {k} (m :: * -> *) (ctx :: Ctx k) (h :: Height) (f :: k -> *)
       (t :: Ctx k).
Applicative m =>
Int
-> Int
-> (forall (x :: k). Index ctx x -> m (f x))
-> m (BalancedTree h f t)
unsafe_bal_generateM Int
h Int
o forall (x :: k). Index ctx x -> m (f x)
f
        r :: m (BinomialTree h f t)
r = forall a b. a -> b
unsafeCoerce (forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
       (tp :: Ctx k).
Int
-> BinomialTree ('Succ h) f ctx
-> BalancedTree h f tp
-> BinomialTree h f (ctx <+> tp)
PlusOne Int
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (BinomialTree Any f Any)
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (BalancedTree Any f Any)
u
     in m (BinomialTree h f t)
r
  | Bool
otherwise =
    let s :: Int
s = Int
sz forall a. Bits a => a -> Int -> a
`shiftR` Int
1
        t :: m (BinomialTree ('Succ h) f t)
t = forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (ctx :: Ctx k)
       (t :: Ctx k).
Applicative m =>
Int
-> Int
-> (forall (x :: k). Index ctx x -> m (f x))
-> m (BinomialTree h f t)
unsafe_bin_generateM Int
s (Int
hforall a. Num a => a -> a -> a
+Int
1) forall (x :: k). Index ctx x -> m (f x)
f
        r :: m (BinomialTree h f t)
        r :: m (BinomialTree h f t)
r = forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k).
Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
PlusZero Int
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (BinomialTree ('Succ h) f t)
t
     in m (BinomialTree h f t)
r

------------------------------------------------------------------------
-- Dropping

data DropResult f (ctx :: Ctx k) where
  DropEmpty :: DropResult f EmptyCtx
  DropExt   :: BinomialTree 'Zero f x
            -> f y
            -> DropResult f (x ::> y)

-- | @bal_drop x y@ returns the tree formed @append x (init y)@
bal_drop :: forall h f x y
          . BinomialTree h f x
            -- ^ Bina
         -> BalancedTree h f y
         -> DropResult f (x <+> y)
bal_drop :: forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
BinomialTree h f x -> BalancedTree h f y -> DropResult f (x <+> y)
bal_drop BinomialTree h f x
t (BalLeaf f x
e) = forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
BinomialTree 'Zero f ctx -> f tp -> DropResult f (ctx ::> tp)
DropExt BinomialTree h f x
t f x
e
bal_drop BinomialTree h f x
t (BalPair BalancedTree h f x
x BalancedTree h f y
y) =
  forall a b. a -> b
unsafeCoerce (forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
BinomialTree h f x -> BalancedTree h f y -> DropResult f (x <+> y)
bal_drop (forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
       (tp :: Ctx k).
Int
-> BinomialTree ('Succ h) f ctx
-> BalancedTree h f tp
-> BinomialTree h f (ctx <+> tp)
PlusOne (forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k).
BinomialTree h f a -> Int
tsize BinomialTree h f x
t) (forall a b. a -> b
unsafeCoerce BinomialTree h f x
t) BalancedTree h f x
x) BalancedTree h f y
y)

bin_drop :: forall h f ctx
          . BinomialTree h f ctx
         -> DropResult f ctx
bin_drop :: forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k).
BinomialTree h f ctx -> DropResult f ctx
bin_drop BinomialTree h f ctx
Empty = forall {k} (f :: k -> *). DropResult f EmptyCtx
DropEmpty
bin_drop (PlusZero Int
_ BinomialTree ('Succ h) f ctx
u) = forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k).
BinomialTree h f ctx -> DropResult f ctx
bin_drop BinomialTree ('Succ h) f ctx
u
bin_drop (PlusOne Int
s BinomialTree ('Succ h) f x
t BalancedTree h f y
u) =
  let m :: BinomialTree h f x
m = case BinomialTree ('Succ h) f x
t of
            BinomialTree ('Succ h) f x
Empty -> forall {k} (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
Empty
            BinomialTree ('Succ h) f x
_ -> forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k).
Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
PlusZero Int
s BinomialTree ('Succ h) f x
t
   in forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
BinomialTree h f x -> BalancedTree h f y -> DropResult f (x <+> y)
bal_drop BinomialTree h f x
m BalancedTree h f y
u

------------------------------------------------------------------------
-- Indexing

-- | Lookup value in tree.
unsafe_bin_index :: BinomialTree h f a -- ^ Tree to lookup in.
                 -> Int
                 -> Int -- ^ Size of tree
                 -> f u
unsafe_bin_index :: forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k) (u :: k).
BinomialTree h f a -> Int -> Int -> f u
unsafe_bin_index BinomialTree h f a
_ Int
_ Int
i
  | seq :: forall a b. a -> b -> b
seq Int
i Bool
False = forall a. (?callStack::CallStack) => String -> a
error String
"bad unsafe_bin_index"
unsafe_bin_index BinomialTree h f a
Empty Int
_ Int
_ = forall a. (?callStack::CallStack) => String -> a
error String
"unsafe_bin_index reached end of list"
unsafe_bin_index (PlusOne Int
sz BinomialTree ('Succ h) f x
t BalancedTree h f y
u) Int
j Int
i
  | Int
sz forall a. Eq a => a -> a -> Bool
== Int
j forall a. Bits a => a -> Int -> a
`shiftR` (Int
1forall a. Num a => a -> a -> a
+Int
i) = forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k) (tp :: k).
BalancedTree h f a -> Int -> Int -> f tp
unsafe_bal_index BalancedTree h f y
u Int
j Int
i
  | Bool
otherwise = forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k) (u :: k).
BinomialTree h f a -> Int -> Int -> f u
unsafe_bin_index BinomialTree ('Succ h) f x
t Int
j forall a b. (a -> b) -> a -> b
$! (Int
1forall a. Num a => a -> a -> a
+Int
i)
unsafe_bin_index (PlusZero Int
sz BinomialTree ('Succ h) f a
t) Int
j Int
i
  | Int
sz forall a. Eq a => a -> a -> Bool
== Int
j forall a. Bits a => a -> Int -> a
`shiftR` (Int
1forall a. Num a => a -> a -> a
+Int
i) = forall a. (?callStack::CallStack) => String -> a
error String
"unsafe_bin_index stopped at PlusZero"
  | Bool
otherwise = forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k) (u :: k).
BinomialTree h f a -> Int -> Int -> f u
unsafe_bin_index BinomialTree ('Succ h) f a
t Int
j forall a b. (a -> b) -> a -> b
$! (Int
1forall a. Num a => a -> a -> a
+Int
i)

-- | Lookup value in tree.
unsafe_bin_adjust :: forall m h f x y a b
                   . Functor m
                  => (f x -> m (f y))
                  -> BinomialTree h f a -- ^ Tree to lookup in.
                  -> Int
                  -> Int -- ^ Size of tree
                  -> m (BinomialTree h f b)
unsafe_bin_adjust :: forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (x :: k)
       (y :: k) (a :: Ctx k) (b :: Ctx k).
Functor m =>
(f x -> m (f y))
-> BinomialTree h f a -> Int -> Int -> m (BinomialTree h f b)
unsafe_bin_adjust f x -> m (f y)
_ BinomialTree h f a
Empty Int
_ Int
_ = forall a. (?callStack::CallStack) => String -> a
error String
"unsafe_bin_adjust reached end of list"
unsafe_bin_adjust f x -> m (f y)
f (PlusOne Int
sz BinomialTree ('Succ h) f x
t BalancedTree h f y
u) Int
j Int
i
  | Int
sz forall a. Eq a => a -> a -> Bool
== Int
j forall a. Bits a => a -> Int -> a
`shiftR` (Int
1forall a. Num a => a -> a -> a
+Int
i) =
    forall a b. a -> b
unsafeCoerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
       (tp :: Ctx k).
Int
-> BinomialTree ('Succ h) f ctx
-> BalancedTree h f tp
-> BinomialTree h f (ctx <+> tp)
PlusOne Int
sz BinomialTree ('Succ h) f x
t        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall {k} (m :: * -> *) (f :: k -> *) (x :: k) (y :: k)
       (h :: Height) (a :: Ctx k) (b :: Ctx k).
Functor m =>
(f x -> m (f y))
-> BalancedTree h f a -> Int -> Int -> m (BalancedTree h f b)
unsafe_bal_adjust f x -> m (f y)
f BalancedTree h f y
u Int
j Int
i)
  | Bool
otherwise =
    forall a b. a -> b
unsafeCoerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
       (tp :: Ctx k).
Int
-> BinomialTree ('Succ h) f ctx
-> BalancedTree h f tp
-> BinomialTree h f (ctx <+> tp)
PlusOne Int
sz) BalancedTree h f y
u forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (x :: k)
       (y :: k) (a :: Ctx k) (b :: Ctx k).
Functor m =>
(f x -> m (f y))
-> BinomialTree h f a -> Int -> Int -> m (BinomialTree h f b)
unsafe_bin_adjust f x -> m (f y)
f BinomialTree ('Succ h) f x
t Int
j (Int
iforall a. Num a => a -> a -> a
+Int
1))
unsafe_bin_adjust f x -> m (f y)
f (PlusZero Int
sz BinomialTree ('Succ h) f a
t) Int
j Int
i
  | Int
sz forall a. Eq a => a -> a -> Bool
== Int
j forall a. Bits a => a -> Int -> a
`shiftR` (Int
1forall a. Num a => a -> a -> a
+Int
i) = forall a. (?callStack::CallStack) => String -> a
error String
"unsafe_bin_adjust stopped at PlusZero"
  | Bool
otherwise = forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k).
Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
PlusZero Int
sz forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (x :: k)
       (y :: k) (a :: Ctx k) (b :: Ctx k).
Functor m =>
(f x -> m (f y))
-> BinomialTree h f a -> Int -> Int -> m (BinomialTree h f b)
unsafe_bin_adjust f x -> m (f y)
f BinomialTree ('Succ h) f a
t Int
j (Int
iforall a. Num a => a -> a -> a
+Int
1))


{-# SPECIALIZE unsafe_bin_adjust
     :: (f x -> Identity (f y))
     -> BinomialTree h f a
     -> Int
     -> Int
     -> Identity (BinomialTree h f b)
  #-}

tree_zipWithM :: Applicative m
             => (forall x . f x -> g x -> m (h x))
             -> BinomialTree u f a
             -> BinomialTree u g a
             -> m (BinomialTree u h a)
tree_zipWithM :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (u :: Height) (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> BinomialTree u f a
-> BinomialTree u g a
-> m (BinomialTree u h a)
tree_zipWithM forall (x :: k). f x -> g x -> m (h x)
_ BinomialTree u f a
Empty BinomialTree u g a
Empty = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {k} (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
Empty
tree_zipWithM forall (x :: k). f x -> g x -> m (h x)
f (PlusOne Int
s BinomialTree ('Succ u) f x
x1 BalancedTree u f y
x2) (PlusOne Int
_ BinomialTree ('Succ u) g x
y1 BalancedTree u g y
y2) =
  forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k)
       (tp :: Ctx k).
Int
-> BinomialTree ('Succ h) f ctx
-> BalancedTree h f tp
-> BinomialTree h f (ctx <+> tp)
PlusOne Int
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (u :: Height) (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> BinomialTree u f a
-> BinomialTree u g a
-> m (BinomialTree u h a)
tree_zipWithM forall (x :: k). f x -> g x -> m (h x)
f BinomialTree ('Succ u) f x
x1 (forall a b. a -> b
unsafeCoerce BinomialTree ('Succ u) g x
y1)
            forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (u :: Height) (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> BalancedTree u f a
-> BalancedTree u g a
-> m (BalancedTree u h a)
bal_zipWithM  forall (x :: k). f x -> g x -> m (h x)
f BalancedTree u f y
x2 (forall a b. a -> b
unsafeCoerce BalancedTree u g y
y2)
tree_zipWithM forall (x :: k). f x -> g x -> m (h x)
f (PlusZero Int
s BinomialTree ('Succ u) f a
x1) (PlusZero Int
_ BinomialTree ('Succ u) g a
y1) =
  forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k).
Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
PlusZero Int
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (u :: Height) (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> BinomialTree u f a
-> BinomialTree u g a
-> m (BinomialTree u h a)
tree_zipWithM forall (x :: k). f x -> g x -> m (h x)
f BinomialTree ('Succ u) f a
x1 BinomialTree ('Succ u) g a
y1
tree_zipWithM forall (x :: k). f x -> g x -> m (h x)
_ BinomialTree u f a
_ BinomialTree u g a
_ = forall a. (?callStack::CallStack) => String -> a
error String
"ilegal args to tree_zipWithM"
{-# INLINABLE tree_zipWithM #-}

------------------------------------------------------------------------
-- * Assignment

-- | An assignment is a sequence that maps each index with type @tp@ to
-- a value of type @f tp@.
--
-- This assignment implementation uses a binomial tree implementation
-- that offers lookups and updates in time and space logarithmic with
-- respect to the number of elements in the context.
newtype Assignment (f :: k -> Type) (ctx :: Ctx k)
      = Assignment (BinomialTree 'Zero f ctx)

type role Assignment nominal nominal

instance NFData (Assignment f ctx) where
  rnf :: Assignment f ctx -> ()
rnf Assignment f ctx
a = seq :: forall a b. a -> b -> b
seq Assignment f ctx
a ()

-- | 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 BinomialTree 'Zero f ctx
t) = forall k (ctx :: Ctx k). Int -> Size ctx
Size (forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k).
BinomialTree h f a -> Int
tsize BinomialTree 'Zero f ctx
t)

-- | @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)

-- | Generate an assignment
generate :: 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
n forall (tp :: k). Index ctx tp -> f tp
f  = forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment BinomialTree 'Zero f ctx
r
  where r :: BinomialTree 'Zero f ctx
r = forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k) (t :: Ctx k).
Int
-> Int
-> (forall (x :: k). Index ctx x -> f x)
-> BinomialTree h f t
unsafe_bin_generate (forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt Size ctx
n) Int
0 forall (tp :: k). Index ctx tp -> f tp
f
{-# NOINLINE generate #-}

-- | Generate an assignment in an 'Applicative' context
generateM :: Applicative m
          => Size ctx
          -> (forall tp . Index ctx tp -> m (f tp))
          -> m (Assignment f ctx)
generateM :: forall {k} (m :: * -> *) (ctx :: Ctx k) (f :: k -> *).
Applicative m =>
Size ctx
-> (forall (tp :: k). Index ctx tp -> m (f tp))
-> m (Assignment f ctx)
generateM Size ctx
n forall (tp :: k). Index ctx tp -> m (f tp)
f = forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (ctx :: Ctx k)
       (t :: Ctx k).
Applicative m =>
Int
-> Int
-> (forall (x :: k). Index ctx x -> m (f x))
-> m (BinomialTree h f t)
unsafe_bin_generateM (forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt Size ctx
n) Int
0 forall (tp :: k). Index ctx tp -> m (f tp)
f
{-# NOINLINE generateM #-}

-- | Return empty assignment
empty :: Assignment f EmptyCtx
empty :: forall {k} (f :: k -> *). Assignment f EmptyCtx
empty = forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment forall {k} (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
Empty

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

-- | Extend an indexed vector with a new entry.
extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x)
extend :: forall {k} (f :: k -> *) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
extend (Assignment BinomialTree 'Zero f ctx
x) f x
y = forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment forall a b. (a -> b) -> a -> b
$ forall {k} (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
BinomialTree h f x
-> BalancedTree h f y -> BinomialTree h f (x <+> y)
append BinomialTree 'Zero f ctx
x (forall {k} (f :: k -> *) (ctx :: k).
f ctx -> BalancedTree 'Zero f (SingleCtx ctx)
BalLeaf f x
y)

-- | Unexported index that returns an arbitrary type of expression.
unsafeIndex :: proxy u -> Int -> Assignment f ctx -> f u
unsafeIndex :: forall {k} (proxy :: k -> *) (u :: k) (f :: k -> *) (ctx :: Ctx k).
proxy u -> Int -> Assignment f ctx -> f u
unsafeIndex proxy u
_ Int
idx (Assignment BinomialTree 'Zero f ctx
t) = seq :: forall a b. a -> b -> b
seq BinomialTree 'Zero f ctx
t forall a b. (a -> b) -> a -> b
$ forall {k} (h :: Height) (f :: k -> *) (a :: Ctx k) (u :: k).
BinomialTree h f a -> Int -> Int -> f u
unsafe_bin_index BinomialTree 'Zero f ctx
t Int
idx Int
0

-- | Return value of assignment.
(!) :: Assignment f ctx -> Index ctx tp -> f tp
Assignment f ctx
a ! :: forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Index Int
i = forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
0 forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i forall a. Ord a => a -> a -> Bool
< forall {k} (ctx :: Ctx k). Size ctx -> Int
sizeInt (forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size Assignment f ctx
a)) forall a b. (a -> b) -> a -> b
$
              forall {k} (proxy :: k -> *) (u :: k) (f :: k -> *) (ctx :: Ctx k).
proxy u -> Int -> Assignment f ctx -> f u
unsafeIndex forall {k} (t :: k). Proxy t
Proxy Int
i Assignment f ctx
a

-- | 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 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)
test (Assignment BinomialTree 'Zero f x
x) (Assignment BinomialTree 'Zero f y
y) = do
     x :~: y
Refl <- forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
TestEqualityFC t =>
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> forall (x :: l) (y :: l). t f x -> t f y -> Maybe (x :~: y)
testEqualityFC forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test BinomialTree 'Zero f x
x BinomialTree 'Zero f y
y
     forall (m :: * -> *) a. Monad m => a -> m a
return forall {k} (a :: k). a :~: a
Refl

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 = forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
TestEqualityFC t =>
(forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> forall (x :: l) (y :: l). t f x -> t f y -> Maybe (x :~: y)
testEqualityFC forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality

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)

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
test (Assignment BinomialTree 'Zero f x
x) (Assignment BinomialTree 'Zero f y
y) =
     forall j k (a :: j) (b :: j) (c :: k) (d :: k).
OrderingF a b -> ((a ~ b) => OrderingF c d) -> OrderingF c d
joinOrderingF (forall k l (t :: (k -> *) -> l -> *) (f :: k -> *).
OrdFC t =>
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF x y
compareFC forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test BinomialTree 'Zero f x
x BinomialTree 'Zero f y
y) forall a b. (a -> b) -> a -> b
$ forall {k} (x :: k). OrderingF x x
EQF

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 l (t :: (k -> *) -> l -> *) (f :: k -> *).
OrdFC t =>
(forall (x :: k) (y :: k). f x -> f y -> OrderingF x y)
-> forall (x :: l) (y :: l). t f x -> t f y -> OrderingF x y
compareFC 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 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 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 f, TestEquality f) => Hashable (Assignment f ctx) where
  hashWithSalt :: Int -> Assignment f ctx -> Int
hashWithSalt Int
s (Assignment BinomialTree 'Zero f ctx
a) = forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
hashWithSaltF Int
s BinomialTree 'Zero f ctx
a

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 ShowF f => Show (Assignment f ctx) where
  show :: Assignment f ctx -> String
show Assignment f ctx
a = String
"[" forall a. [a] -> [a] -> [a]
Prelude.++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (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 k (f :: k -> *) (tp :: k). ShowF f => f tp -> String
showF Assignment f ctx
a) forall a. [a] -> [a] -> [a]
Prelude.++ String
"]"

instance ShowF f => ShowF (Assignment f)

{-# DEPRECATED adjust "Replace 'adjust f i asgn' with 'Lens.over (ixF i) f asgn' instead." #-}
adjust :: (f tp -> f tp) -> Index ctx tp -> Assignment f ctx -> Assignment f ctx
adjust :: forall {k} (f :: k -> *) (tp :: k) (ctx :: Ctx 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 -> *) (tp :: k) (ctx :: Ctx 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 :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx
update :: forall {k} (ctx :: Ctx k) (tp :: k) (f :: 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 -> *) (tp :: k) (ctx :: Ctx 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

-- | Modify the value of an assignment at a particular index.
adjustM :: Functor m => (f tp -> m (f tp)) -> Index ctx tp -> Assignment f ctx -> m (Assignment f ctx)
adjustM :: forall {k} (m :: * -> *) (f :: k -> *) (tp :: k) (ctx :: Ctx 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 (Index Int
i) (Assignment BinomialTree 'Zero f ctx
a) = forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (x :: k)
       (y :: k) (a :: Ctx k) (b :: Ctx k).
Functor m =>
(f x -> m (f y))
-> BinomialTree h f a -> Int -> Int -> m (BinomialTree h f b)
unsafe_bin_adjust f tp -> m (f tp)
f BinomialTree 'Zero f ctx
a Int
i Int
0)
{-# SPECIALIZE adjustM :: (f tp -> Identity (f tp)) -> Index ctx tp -> Assignment f ctx -> Identity (Assignment f ctx) #-}

type instance IndexF       (Assignment f ctx) = Index ctx
type instance IxValueF     (Assignment f ctx) = f

instance forall k (f :: k -> Type) ctx. IxedF' k (Assignment (f :: k -> Type) 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 -> *) (tp :: k) (ctx :: Ctx 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 :: forall (x :: k).
IndexF (Assignment f ctx) x
-> Traversal' (Assignment f ctx) (IxValueF (Assignment f ctx) x)
ixF IndexF (Assignment f ctx) x
idx = forall k m (x :: k).
IxedF' k m =>
IndexF m x -> Lens' m (IxValueF m x)
ixF' IndexF (Assignment f ctx) x
idx

-- This is an unsafe version of update that changes the type of the expression.
unsafeUpdate :: Int -> Assignment f ctx -> f u -> Assignment f ctx'
unsafeUpdate :: forall {k} (f :: k -> *) (ctx :: Ctx k) (u :: k) (ctx' :: Ctx k).
Int -> Assignment f ctx -> f u -> Assignment f ctx'
unsafeUpdate Int
i (Assignment BinomialTree 'Zero f ctx
a) f u
e = forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment (forall a. Identity a -> a
runIdentity (forall {k} (m :: * -> *) (h :: Height) (f :: k -> *) (x :: k)
       (y :: k) (a :: Ctx k) (b :: Ctx k).
Functor m =>
(f x -> m (f y))
-> BinomialTree h f a -> Int -> Int -> m (BinomialTree h f b)
unsafe_bin_adjust (\f Any
_ -> forall a. a -> Identity a
Identity f u
e) BinomialTree 'Zero f ctx
a Int
i Int
0))

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

-- | View an assignment as either empty or an assignment with one appended.
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 BinomialTree 'Zero f ctx
x) =
  case forall {k} (h :: Height) (f :: k -> *) (ctx :: Ctx k).
BinomialTree h f ctx -> DropResult f ctx
bin_drop BinomialTree 'Zero f ctx
x of
    DropResult f ctx
DropEmpty -> forall {k} (f :: k -> *). AssignView f EmptyCtx
AssignEmpty
    DropExt BinomialTree 'Zero f x
t f y
v -> forall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> f tp -> AssignView f (ctx ::> tp)
AssignExtend (forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment BinomialTree 'Zero f x
t) f y
v

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 -> *)
       (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> Assignment f a -> Assignment g a -> m (Assignment h a)
zipWithM (\f x
u g x
v -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (x :: k). f x -> g x -> h x
f f x
u g x
v)) Assignment f a
x Assignment g a
y
{-# INLINE zipWith #-}

zipWithM :: Applicative m
         => (forall x . f x -> g x -> m (h x))
         -> Assignment f a
         -> Assignment g a
         -> m (Assignment h a)
zipWithM :: forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> Assignment f a -> Assignment g a -> m (Assignment h a)
zipWithM forall (x :: k). f x -> g x -> m (h x)
f (Assignment BinomialTree 'Zero f a
x) (Assignment BinomialTree 'Zero g a
y) = forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *)
       (u :: Height) (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> BinomialTree u f a
-> BinomialTree u g a
-> m (BinomialTree u h a)
tree_zipWithM forall (x :: k). f x -> g x -> m (h x)
f BinomialTree 'Zero f a
x BinomialTree 'Zero g a
y
{-# INLINABLE zipWithM #-}

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 (x :: k). f x -> g x
f (Assignment BinomialTree 'Zero f x
x) -> forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment (forall {k} (f :: k -> *) (g :: k -> *) (h :: Height) (c :: Ctx k).
(forall (tp :: k). f tp -> g tp)
-> BinomialTree h f c -> BinomialTree h g c
fmap_bin forall (x :: k). f x -> g x
f BinomialTree 'Zero f x
x)
  {-# INLINE fmapFC #-}

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
  {-# INLINE foldMapFC #-}

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 (Assignment BinomialTree 'Zero f x
x) -> forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: Height)
       (c :: Ctx k).
Applicative m =>
(forall (tp :: k). f tp -> m (g tp))
-> BinomialTree h f c -> m (BinomialTree h g c)
traverse_bin forall (x :: k). f x -> m (g x)
f BinomialTree 'Zero f x
x
  {-# INLINE traverseFC #-}

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


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} (m :: * -> *) (ctx :: Ctx k) (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)

------------------------------------------------------------------------
-- Appending

appendBal :: Assignment f x -> BalancedTree h f y -> Assignment f (x <+> y)
appendBal :: forall {k} (f :: k -> *) (x :: Ctx k) (h :: Height) (y :: Ctx k).
Assignment f x -> BalancedTree h f y -> Assignment f (x <+> y)
appendBal Assignment f x
x (BalLeaf f x
a) = Assignment f x
x forall {k} (f :: k -> *) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
`extend` f x
a
appendBal Assignment f x
x (BalPair BalancedTree h f x
y BalancedTree h f y
z) =
  case forall {k} (p :: Ctx k -> *) (x :: Ctx k) (q :: Ctx k -> *)
       (y :: Ctx k) (r :: Ctx k -> *) (z :: Ctx k).
p x -> q y -> r z -> (x <+> (y <+> z)) :~: ((x <+> y) <+> z)
assoc Assignment f x
x BalancedTree h f x
y BalancedTree h f y
z of
    (x <+> (x <+> y)) :~: ((x <+> x) <+> y)
Refl -> Assignment f x
x forall {k} (f :: k -> *) (x :: Ctx k) (h :: Height) (y :: Ctx k).
Assignment f x -> BalancedTree h f y -> Assignment f (x <+> y)
`appendBal` BalancedTree h f x
y forall {k} (f :: k -> *) (x :: Ctx k) (h :: Height) (y :: Ctx k).
Assignment f x -> BalancedTree h f y -> Assignment f (x <+> y)
`appendBal` BalancedTree h f y
z

appendBin :: Assignment f x -> BinomialTree h f y -> Assignment f (x <+> y)
appendBin :: forall {k} (f :: k -> *) (x :: Ctx k) (h :: Height) (y :: Ctx k).
Assignment f x -> BinomialTree h f y -> Assignment f (x <+> y)
appendBin Assignment f x
x BinomialTree h f y
Empty = Assignment f x
x
appendBin Assignment f x
x (PlusOne Int
_ BinomialTree ('Succ h) f x
y BalancedTree h f y
z) =
  case forall {k} (p :: Ctx k -> *) (x :: Ctx k) (q :: Ctx k -> *)
       (y :: Ctx k) (r :: Ctx k -> *) (z :: Ctx k).
p x -> q y -> r z -> (x <+> (y <+> z)) :~: ((x <+> y) <+> z)
assoc Assignment f x
x BinomialTree ('Succ h) f x
y BalancedTree h f y
z of
    (x <+> (x <+> y)) :~: ((x <+> x) <+> y)
Refl -> Assignment f x
x forall {k} (f :: k -> *) (x :: Ctx k) (h :: Height) (y :: Ctx k).
Assignment f x -> BinomialTree h f y -> Assignment f (x <+> y)
`appendBin` BinomialTree ('Succ h) f x
y forall {k} (f :: k -> *) (x :: Ctx k) (h :: Height) (y :: Ctx k).
Assignment f x -> BalancedTree h f y -> Assignment f (x <+> y)
`appendBal` BalancedTree h f y
z
appendBin Assignment f x
x (PlusZero Int
_ BinomialTree ('Succ h) f y
y) = Assignment f x
x forall {k} (f :: k -> *) (x :: Ctx k) (h :: Height) (y :: Ctx k).
Assignment f x -> BinomialTree h f y -> Assignment f (x <+> y)
`appendBin` BinomialTree ('Succ h) f y
y

(<++>) :: 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 BinomialTree 'Zero f y
y = Assignment f x
x forall {k} (f :: k -> *) (x :: Ctx k) (h :: Height) (y :: Ctx k).
Assignment f x -> BinomialTree h f y -> Assignment f (x <+> y)
`appendBin` BinomialTree 'Zero f y
y

------------------------------------------------------------------------
-- 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 -> *) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
`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

------------------------------------------------------------------------
-- Lens combinators

unsafeLens :: Int -> Lens.Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens :: forall {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
idx =
  forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (forall {k} (proxy :: k -> *) (u :: k) (f :: k -> *) (ctx :: Ctx k).
proxy u -> Int -> Assignment f ctx -> f u
unsafeIndex forall {k} (t :: k). Proxy t
Proxy Int
idx) (forall {k} (f :: k -> *) (ctx :: Ctx k) (u :: k) (ctx' :: Ctx k).
Int -> Assignment f ctx -> f u -> Assignment f ctx'
unsafeUpdate Int
idx)

------------------------------------------------------------------------
-- 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
0

------------------------------------------------------------------------
-- 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
0

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
1

------------------------------------------------------------------------
-- 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
0


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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
1

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
2

------------------------------------------------------------------------
-- 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
0


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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
1

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
2

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
3

------------------------------------------------------------------------
-- 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
0

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
1

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
2

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
3

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
4

------------------------------------------------------------------------
-- 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
0


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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
1

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
2

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
3

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
4

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
5

------------------------------------------------------------------------
-- 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
0


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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
1

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
2

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
3

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
4

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
5

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
6

------------------------------------------------------------------------
-- 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
0


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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
1

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
2

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
3

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
4

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
5

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
6

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
7

------------------------------------------------------------------------
-- 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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
0

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
1

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
2

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
3

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
4

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
5

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
6

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
7

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 {k} (f :: k -> *) (ctx :: Ctx k) (ctx' :: Ctx k) (tp :: k)
       (u :: k).
Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
8