{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# 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
    -- * 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.Classes
import           Data.Parameterized.Ctx
import           Data.Parameterized.Ctx.Proofs
import           Data.Parameterized.Some
import           Data.Parameterized.TraversableFC

------------------------------------------------------------------------
-- 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 :: Size ctx -> Int
sizeInt (Size Int
n) = Int
n

-- | The size of an empty context.
zeroSize :: Size 'EmptyCtx
zeroSize :: Size 'EmptyCtx
zeroSize = Int -> Size 'EmptyCtx
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 :: Size ctx -> Size (ctx '::> tp)
incSize (Size Int
n) = Int -> Size (ctx '::> tp)
forall k (ctx :: Ctx k). Int -> Size ctx
Size (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)

decSize :: Size (ctx '::> tp) -> Size ctx
decSize :: Size (ctx '::> tp) -> Size ctx
decSize (Size Int
n) = Bool -> Size ctx -> Size ctx
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Int -> Size ctx
forall k (ctx :: Ctx k). Int -> Size ctx
Size (Int
nInt -> Int -> Int
forall 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 :: Size ctx -> SizeView ctx
viewSize (Size Int
0) = SizeView 'EmptyCtx -> SizeView ctx
forall a b. a -> b
unsafeCoerce SizeView 'EmptyCtx
forall k. SizeView 'EmptyCtx
ZeroSize
viewSize (Size Int
n) = Bool -> SizeView ctx -> SizeView ctx
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (SizeView (Any '::> Any) -> SizeView ctx
forall a b. a -> b
unsafeCoerce (Size Any -> SizeView (Any '::> Any)
forall k (ctx :: Ctx k) (tp :: k).
Size ctx -> SizeView (ctx '::> tp)
IncSize (Int -> Size Any
forall k (ctx :: Ctx k). Int -> Size ctx
Size (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))))

instance Show (Size ctx) where
  show :: Size ctx -> String
show (Size Int
i) = Int -> String
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 = Size 'EmptyCtx
forall k. Size 'EmptyCtx
zeroSize

instance KnownContext ctx => KnownContext (ctx '::> tp) where
  knownSize :: Size (ctx '::> tp)
knownSize = Size ctx -> Size (ctx '::> tp)
forall k (ctx :: Ctx k) (tp :: k). Size ctx -> Size (ctx '::> tp)
incSize Size ctx
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 { Diff l r -> Int
_contextExtSize :: Int }

type role Diff nominal nominal

-- | The identity difference. Identity element of 'Category' instance.
noDiff :: Diff l l
noDiff :: Diff l l
noDiff = Int -> Diff l l
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 :: Diff a b -> Diff b c -> Diff a c
addDiff (Diff Int
x) (Diff Int
y) = Int -> Diff a c
forall k (l :: Ctx k) (r :: Ctx k). Int -> Diff l r
Diff (Int
x Int -> Int -> Int
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 :: Diff l r -> Diff l (r '::> tp)
extendRight (Diff Int
i) = Int -> Diff l (r '::> tp)
forall k (l :: Ctx k) (r :: Ctx k). Int -> Diff l r
Diff (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)

appendDiff :: Size r -> Diff l (l <+> r)
appendDiff :: Size r -> Diff l (l <+> r)
appendDiff (Size Int
r) = Int -> Diff l (l <+> 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 :: Diff a a
id = Diff a a
forall k (a :: Ctx k). Diff a a
noDiff
  Diff b c
j . :: Diff b c -> Diff a b -> Diff a c
. Diff a b
i = Diff a b -> Diff b c -> Diff a c
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 :: Size l -> Diff l r -> Size r
extSize (Size Int
i) (Diff Int
j) = Int -> Size r
forall k (ctx :: Ctx k). Int -> Size ctx
Size (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
j)

-- | The total size of two concatenated contexts.
addSize :: Size x -> Size y -> Size (x <+> y)
addSize :: Size x -> Size y -> Size (x <+> y)
addSize (Size Int
x) (Size Int
y) = Int -> Size (x <+> y)
forall k (ctx :: Ctx k). Int -> Size ctx
Size (Int
x Int -> Int -> Int
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 :: Diff l r -> IsAppend l r
diffIsAppend (Diff Int
i) = IsAppend Any (Any <+> Any) -> IsAppend l r
forall a b. a -> b
unsafeCoerce (IsAppend Any (Any <+> Any) -> IsAppend l r)
-> IsAppend Any (Any <+> Any) -> IsAppend l r
forall a b. (a -> b) -> a -> b
$ Size Any -> IsAppend Any (Any <+> Any)
forall k (app :: Ctx k) (l :: Ctx k).
Size app -> IsAppend l (l <+> app)
IsAppend (Int -> Size Any
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 :: Diff a b -> DiffView a b
viewDiff (Diff Int
i)
  | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = DiffView Any Any -> DiffView a b
forall a b. a -> b
unsafeCoerce DiffView Any Any
forall k (a :: Ctx k). DiffView a a
NoDiff
  | Bool
otherwise  = Bool -> DiffView a b -> DiffView a b
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (DiffView a b -> DiffView a b) -> DiffView a b -> DiffView a b
forall a b. (a -> b) -> a -> b
$ DiffView Any (Any '::> Any) -> DiffView a b
forall a b. a -> b
unsafeCoerce (DiffView Any (Any '::> Any) -> DiffView a b)
-> DiffView Any (Any '::> Any) -> DiffView a b
forall a b. (a -> b) -> a -> b
$ Diff Any Any -> DiffView Any (Any '::> Any)
forall k (a :: Ctx k) (b :: Ctx k) (r :: k).
Diff a b -> DiffView a (b ::> r)
ExtendRightDiff (Int -> Diff Any Any
forall k (l :: Ctx k) (r :: Ctx k). Int -> Diff l r
Diff (Int
iInt -> Int -> Int
forall 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 = Diff l l
forall k (a :: Ctx k). Diff a a
noDiff

instance {-# INCOHERENT #-} KnownDiff l r => KnownDiff l (r '::> tp) where
  knownDiff :: Diff l (r '::> tp)
knownDiff = Diff l r -> Diff l (r '::> tp)
forall k (l :: Ctx k) (r :: Ctx k) (tp :: k).
Diff l r -> Diff l (r '::> tp)
extendRight Diff l r
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 { 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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j

instance TestEquality (Index ctx) where
  testEquality :: Index ctx a -> Index ctx b -> Maybe (a :~: b)
testEquality (Index Int
i) (Index Int
j)
    | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just ((Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall k (a :: k). a :~: a
Refl)
    | Bool
otherwise = Maybe (a :~: b)
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 = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
i Int
j

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

-- | Index for first element in context.
baseIndex :: Index ('EmptyCtx '::> tp) tp
baseIndex :: Index ('EmptyCtx '::> tp) tp
baseIndex = Int -> Index ('EmptyCtx '::> tp) tp
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 :: Index ctx x -> Index (ctx '::> y) x
skipIndex (Index Int
i) = Int -> Index (ctx '::> y) x
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 :: Size ctx -> Index (ctx ::> tp) tp
nextIndex Size ctx
n = Int -> Index (ctx ::> tp) tp
forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index (Size ctx -> Int
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 :: Size (ctx ::> tp) -> Index (ctx ::> tp) tp
lastIndex Size (ctx ::> tp)
n = Int -> Index (ctx ::> tp) tp
forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index (Size (ctx ::> tp) -> Int
forall k (ctx :: Ctx k). Size ctx -> Int
sizeInt Size (ctx ::> tp)
n Int -> Int -> Int
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 :: Size r -> Index l tp -> Index (l <+> r) tp
leftIndex Size r
_ (Index Int
il) = Int -> Index (l <+> r) tp
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 :: Size l -> Size r -> Index r tp -> Index (l <+> r) tp
rightIndex (Size Int
sl) Size r
_ (Index Int
ir) = Int -> Index (l <+> r) tp
forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index (Int
sl Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
ir)

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

-- | Given a size @n@, an initial value @v0@, and a function @f@, the
-- expression @forIndex n v0 f@ is equivalent to @v0@ when @n@ is
-- zero, and @f (forIndex (n-1) 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 :: 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 Size ctx -> SizeView ctx
forall k (ctx :: Ctx k). Size ctx -> SizeView ctx
viewSize Size ctx
n of
    SizeView ctx
ZeroSize -> r
r
    IncSize Size ctx
p -> r -> Index ctx tp -> r
forall (tp :: k). r -> Index ctx tp -> r
f (Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
forall k (ctx :: Ctx k) r.
Size ctx -> (forall (tp :: k). r -> Index ctx tp -> r) -> r -> r
forIndex Size ctx
p ((r -> Index ctx Any -> r) -> r -> Index ctx tp -> r
coerce r -> Index ctx Any -> r
forall (tp :: k). r -> Index ctx tp -> r
f) r
r) (Size ctx -> Index (ctx ::> tp) tp
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@, value @v@, and a
-- function @f@, the expression @forIndex i n f v@ is equivalent to
-- @v@ when @i >= sizeInt n@, and @f i (forIndexRange (i+1) n v)@
-- otherwise.
forIndexRange :: forall ctx r
               . Int
              -> Size ctx
              -> (forall tp . Index ctx tp -> r -> r)
              -> r
              -> r
forIndexRange :: 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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = r
r
  | Bool
otherwise = Index ctx Any -> r -> r
forall (tp :: k). Index ctx tp -> r -> r
f (Int -> Index ctx Any
forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index Int
i) (Int
-> Size ctx -> (forall (tp :: k). Index ctx tp -> r -> r) -> r -> r
forall k (ctx :: Ctx k) r.
Int
-> Size ctx -> (forall (tp :: k). Index ctx tp -> r -> r) -> r -> r
forIndexRange (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Int -> Size ctx
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 :: Int -> Size ctx -> Maybe (Some (Index ctx))
intIndex Int
i Size ctx
n | Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Size ctx -> Int
forall k (ctx :: Ctx k). Size ctx -> Int
sizeInt Size ctx
n = Some (Index ctx) -> Maybe (Some (Index ctx))
forall a. a -> Maybe a
Just (Index ctx Any -> Some (Index ctx)
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (Int -> Index ctx Any
forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index Int
i))
             | Bool
otherwise = Maybe (Some (Index ctx))
forall a. Maybe a
Nothing

instance Show (Index ctx tp) where
   show :: Index ctx tp -> String
show = Int -> String
forall a. Show a => a -> String
show (Int -> String) -> (Index ctx tp -> Int) -> Index ctx tp -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index ctx tp -> Int
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 :: Size ctx -> Index ctx tp -> IndexView ctx tp
viewIndex (Size Int
sz) (Index Int
i)
  | Int
sz' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i  = IndexView (Any '::> Any) Any -> IndexView ctx tp
forall a b. a -> b
unsafeCoerce (Size Any -> IndexView (Any '::> Any) Any
forall k (ctx :: Ctx k) (t :: k).
Size ctx -> IndexView (ctx '::> t) t
IndexViewLast (Int -> Size Any
forall k (ctx :: Ctx k). Int -> Size ctx
Size Int
sz'))
  | Bool
otherwise = IndexView (Any '::> Any) Any -> IndexView ctx tp
forall a b. a -> b
unsafeCoerce (Index Any Any -> IndexView (Any '::> Any) Any
forall k (ctx :: Ctx k) (t :: k) (u :: k).
Index ctx t -> IndexView (ctx '::> u) t
IndexViewInit (Int -> Index Any Any
forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index Int
i))
  where
    sz' :: Int
sz' = Int
szInt -> Int -> Int
forall 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 :: Size ctx -> IndexRange ctx ctx
allRange (Size Int
n) = Int -> Int -> IndexRange ctx ctx
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 :: IndexRange ctx (EmptyCtx ::> e) -> Index ctx e
indexOfRange (IndexRange Int
i Int
n) = Bool -> Index ctx e -> Index ctx e
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) (Index ctx e -> Index ctx e) -> Index ctx e -> Index ctx e
forall a b. (a -> b) -> a -> b
$ Int -> Index ctx e
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 :: IndexRange ctx (x <+> y) -> Size y -> IndexRange ctx x
dropTailRange (IndexRange Int
i Int
n) (Size Int
j) = Bool -> IndexRange ctx x -> IndexRange ctx x
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
j) (IndexRange ctx x -> IndexRange ctx x)
-> IndexRange ctx x -> IndexRange ctx x
forall a b. (a -> b) -> a -> b
$ Int -> Int -> IndexRange ctx x
forall k (ctx :: Ctx k) (sub :: Ctx k).
Int -> Int -> IndexRange ctx sub
IndexRange Int
i (Int
n Int -> Int -> Int
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 :: IndexRange ctx (x <+> y) -> Size x -> IndexRange ctx y
dropHeadRange (IndexRange Int
i Int
n) (Size Int
j) = Bool -> IndexRange ctx y -> IndexRange ctx y
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
i' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
i Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
j) (IndexRange ctx y -> IndexRange ctx y)
-> IndexRange ctx y -> IndexRange ctx y
forall a b. (a -> b) -> a -> b
$ Int -> Int -> IndexRange ctx y
forall k (ctx :: Ctx k) (sub :: Ctx k).
Int -> Int -> IndexRange ctx sub
IndexRange Int
i' (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
j)
  where i' :: Int
i' = Int
i Int -> Int -> Int
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 :: 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) = BalancedTree h f x -> Int
forall k (h :: Height) (f :: k -> *) (p :: Ctx k).
BalancedTree h f p -> Int
bal_size BalancedTree h f x
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ BalancedTree h f y -> Int
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 (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 <- f x -> f x -> Maybe (x :~: x)
forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y)
test f x
x f x
y
    (x :~: x) -> Maybe (x :~: x)
forall (m :: * -> *) a. Monad m => a -> m a
return x :~: x
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 (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> BalancedTree h f x -> BalancedTree h f x -> Maybe (x :~: x)
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
BalancedTree h f x
y1
    y :~: y
Refl <- (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> BalancedTree h f y -> BalancedTree h f y -> Maybe (y :~: y)
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
BalancedTree h f y
y2
    (x :~: x) -> Maybe (x :~: x)
forall (m :: * -> *) a. Monad m => a -> m a
return x :~: x
forall k (a :: k). a :~: a
Refl

instance OrdFC (BalancedTree h) where
  compareFC :: (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) =
    OrderingF x x -> ((x ~ x) => OrderingF x y) -> OrderingF 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 (f x -> f x -> OrderingF x x
forall (x :: k) (y :: k). f x -> f y -> OrderingF x y
test f x
x f x
y) (((x ~ x) => OrderingF x y) -> OrderingF x y)
-> ((x ~ x) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$ (x ~ x) => OrderingF x y
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) =
    OrderingF x x -> ((x ~ x) => OrderingF x y) -> OrderingF 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)
-> BalancedTree h f x -> BalancedTree h f x -> OrderingF x x
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
BalancedTree h f x
y1) (((x ~ x) => OrderingF x y) -> OrderingF x y)
-> ((x ~ x) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$
    OrderingF y y -> ((y ~ y) => OrderingF x y) -> OrderingF 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)
-> BalancedTree h f y -> BalancedTree h f y -> OrderingF y y
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
BalancedTree h f y
y2) (((y ~ y) => OrderingF x y) -> OrderingF x y)
-> ((y ~ y) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$
    (y ~ y) => OrderingF x y
forall k (x :: k). OrderingF x x
EQF

instance HashableF f => HashableF (BalancedTree h f) where
  hashWithSaltF :: 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 Int -> f x -> Int
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 Int -> BalancedTree h f x -> Int
forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
`hashWithSaltF` BalancedTree h f x
x Int -> BalancedTree h f y -> Int
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 (tp :: k). f tp -> g tp)
-> BalancedTree h f c -> BalancedTree h g c
fmap_bal = (forall (tp :: k). f tp -> g tp)
-> BalancedTree h f c -> BalancedTree h g c
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 (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) = g x -> BalancedTree 'Zero g (SingleCtx x)
forall k (f :: k -> *) (x :: k).
f x -> BalancedTree 'Zero f (SingleCtx x)
BalLeaf (f x -> g x
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) = BalancedTree h g x
-> BalancedTree h g y -> BalancedTree ('Succ h) g (x <+> y)
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
BalancedTree h f x
-> BalancedTree h f y -> BalancedTree ('Succ h) f (x <+> y)
BalPair ((forall (tp :: k). f tp -> g tp)
-> BalancedTree h f x -> BalancedTree h g 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 x
x) ((forall (tp :: k). f tp -> g tp)
-> BalancedTree h f y -> BalancedTree h g y
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 (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))
-> BalancedTree h f c -> m (BalancedTree h g c)
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 (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) = g x -> BalancedTree 'Zero g (SingleCtx x)
forall k (f :: k -> *) (x :: k).
f x -> BalancedTree 'Zero f (SingleCtx x)
BalLeaf (g x -> BalancedTree 'Zero g (SingleCtx x))
-> m (g x) -> m (BalancedTree 'Zero g (SingleCtx x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> m (g x)
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) = BalancedTree h g x -> BalancedTree h g y -> BalancedTree h g c
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
BalancedTree h f x
-> BalancedTree h f y -> BalancedTree ('Succ h) f (x <+> y)
BalPair (BalancedTree h g x -> BalancedTree h g y -> BalancedTree h g c)
-> m (BalancedTree h g x)
-> m (BalancedTree h g y -> BalancedTree h g c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (tp :: k). f tp -> m (g tp))
-> BalancedTree h f x -> m (BalancedTree h g x)
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 m (BalancedTree h g y -> BalancedTree h g c)
-> m (BalancedTree h g y) -> m (BalancedTree h g c)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (tp :: k). f tp -> m (g tp))
-> BalancedTree h f y -> m (BalancedTree h g y)
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) = f x -> String
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 " String -> ShowS
forall a. [a] -> [a] -> [a]
Prelude.++ BalancedTree h f x -> String
forall a. Show a => a -> String
show BalancedTree h f x
x String -> ShowS
forall a. [a] -> [a] -> [a]
Prelude.++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
Prelude.++ BalancedTree h f y -> String
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 :: 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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<  Int
0 = String -> BalancedTree h f t
forall a. (?callStack::CallStack) => String -> a
error String
"unsafe_bal_generate given negative height"
  | Int
h Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = BalancedTree 'Zero f (SingleCtx Any) -> BalancedTree h f t
forall a b. a -> b
unsafeCoerce (BalancedTree 'Zero f (SingleCtx Any) -> BalancedTree h f t)
-> BalancedTree 'Zero f (SingleCtx Any) -> BalancedTree h f t
forall a b. (a -> b) -> a -> b
$ f Any -> BalancedTree 'Zero f (SingleCtx Any)
forall k (f :: k -> *) (x :: k).
f x -> BalancedTree 'Zero f (SingleCtx x)
BalLeaf (Index ctx Any -> f Any
forall (tp :: k). Index ctx tp -> f tp
f (Int -> Index ctx Any
forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index Int
o))
  | Bool
otherwise =
    let l :: BalancedTree Any f Any
l = Int
-> Int
-> (forall (tp :: k). Index ctx tp -> f tp)
-> BalancedTree Any f Any
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
hInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
o forall (tp :: k). Index ctx tp -> f tp
f
        o' :: Int
o' = Int
o Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftL` (Int
hInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
        u :: BalancedTree Any f Any
u = Bool -> BalancedTree Any f Any -> BalancedTree Any f Any
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
o Int -> Int -> Int
forall a. Num a => a -> a -> a
+ BalancedTree Any f Any -> Int
forall k (h :: Height) (f :: k -> *) (p :: Ctx k).
BalancedTree h f p -> Int
bal_size BalancedTree Any f Any
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
o') (BalancedTree Any f Any -> BalancedTree Any f Any)
-> BalancedTree Any f Any -> BalancedTree Any f Any
forall a b. (a -> b) -> a -> b
$ Int
-> Int
-> (forall (tp :: k). Index ctx tp -> f tp)
-> BalancedTree Any f Any
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
hInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
o' forall (tp :: k). Index ctx tp -> f tp
f
     in BalancedTree ('Succ Any) f (Any <+> Any) -> BalancedTree h f t
forall a b. a -> b
unsafeCoerce (BalancedTree ('Succ Any) f (Any <+> Any) -> BalancedTree h f t)
-> BalancedTree ('Succ Any) f (Any <+> Any) -> BalancedTree h f t
forall a b. (a -> b) -> a -> b
$ BalancedTree Any f Any
-> BalancedTree Any f Any
-> BalancedTree ('Succ Any) f (Any <+> Any)
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
BalancedTree h f x
-> BalancedTree h f y -> BalancedTree ('Succ h) f (x <+> 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 :: 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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = BalancedTree 'Zero f (SingleCtx Any) -> BalancedTree h f t
forall a b. a -> b
unsafeCoerce (BalancedTree 'Zero f (SingleCtx Any) -> BalancedTree h f t)
-> (f Any -> BalancedTree 'Zero f (SingleCtx Any))
-> f Any
-> BalancedTree h f t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Any -> BalancedTree 'Zero f (SingleCtx Any)
forall k (f :: k -> *) (x :: k).
f x -> BalancedTree 'Zero f (SingleCtx x)
BalLeaf (f Any -> BalancedTree h f t)
-> m (f Any) -> m (BalancedTree h f t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Index ctx Any -> m (f Any)
forall (x :: k). Index ctx x -> m (f x)
f (Int -> Index ctx Any
forall k (ctx :: Ctx k) (tp :: k). Int -> Index ctx tp
Index Int
o)
  | Bool
otherwise =
    let o' :: Int
o' = Int
o Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftL` (Int
hInt -> Int -> Int
forall 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 = Bool -> BalancedTree h f t -> BalancedTree h f t
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
o' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
o Int -> Int -> Int
forall a. Num a => a -> a -> a
+ BalancedTree Any f Any -> Int
forall k (h :: Height) (f :: k -> *) (p :: Ctx k).
BalancedTree h f p -> Int
bal_size BalancedTree Any f Any
lv) (BalancedTree h f t -> BalancedTree h f t)
-> BalancedTree h f t -> BalancedTree h f t
forall a b. (a -> b) -> a -> b
$
           BalancedTree ('Succ Any) f (Any <+> Any) -> BalancedTree h f t
forall a b. a -> b
unsafeCoerce (BalancedTree Any f Any
-> BalancedTree Any f Any
-> BalancedTree ('Succ Any) f (Any <+> Any)
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
BalancedTree h f x
-> BalancedTree h f y -> BalancedTree ('Succ h) f (x <+> 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 (BalancedTree Any f Any
 -> BalancedTree Any f Any -> BalancedTree h f t)
-> m (BalancedTree Any f Any)
-> m (BalancedTree Any f Any -> BalancedTree h f t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> Int
-> (forall (x :: k). Index ctx x -> m (f x))
-> m (BalancedTree Any f Any)
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
hInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
o  forall (x :: k). Index ctx x -> m (f x)
f
           m (BalancedTree Any f Any -> BalancedTree h f t)
-> m (BalancedTree Any f Any) -> m (BalancedTree h f t)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int
-> Int
-> (forall (x :: k). Index ctx x -> m (f x))
-> m (BalancedTree Any f Any)
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
hInt -> Int -> Int
forall 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 :: BalancedTree h f a -> Int -> Int -> f tp
unsafe_bal_index BalancedTree h f a
_ Int
j Int
i
  | Int -> Bool -> Bool
seq Int
j (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> Bool -> Bool
seq Int
i (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool
False = String -> f tp
forall a. (?callStack::CallStack) => String -> a
error String
"bad unsafe_bal_index"
unsafe_bal_index (BalLeaf f x
u) Int
_ Int
i = Bool -> f tp -> f tp
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) (f tp -> f tp) -> f tp -> f tp
forall a b. (a -> b) -> a -> b
$ f x -> f tp
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 Int -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) = BalancedTree h f y -> Int -> Int -> f tp
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 (Int -> f tp) -> Int -> f tp
forall a b. (a -> b) -> a -> b
$! (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
  | Bool
otherwise         = BalancedTree h f x -> Int -> Int -> f tp
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 (Int -> f tp) -> Int -> f tp
forall a b. (a -> b) -> a -> b
$! (Int
iInt -> Int -> Int
forall 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 :: (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 = Bool -> m (BalancedTree h f b) -> m (BalancedTree h f b)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) (m (BalancedTree h f b) -> m (BalancedTree h f b))
-> m (BalancedTree h f b) -> m (BalancedTree h f b)
forall a b. (a -> b) -> a -> b
$
  (BalancedTree 'Zero f (SingleCtx y) -> BalancedTree h f b
forall a b. a -> b
unsafeCoerce (BalancedTree 'Zero f (SingleCtx y) -> BalancedTree h f b)
-> (f y -> BalancedTree 'Zero f (SingleCtx y))
-> f y
-> BalancedTree h f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f y -> BalancedTree 'Zero f (SingleCtx y)
forall k (f :: k -> *) (x :: k).
f x -> BalancedTree 'Zero f (SingleCtx x)
BalLeaf (f y -> BalancedTree h f b) -> m (f y) -> m (BalancedTree h f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (f x -> m (f y)
f (f x -> f x
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 Int -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) = (BalancedTree ('Succ h) f (x <+> Any) -> BalancedTree h f b
forall a b. a -> b
unsafeCoerce (BalancedTree ('Succ h) f (x <+> Any) -> BalancedTree h f b)
-> (BalancedTree h f Any -> BalancedTree ('Succ h) f (x <+> Any))
-> BalancedTree h f Any
-> BalancedTree h f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BalancedTree h f x
-> BalancedTree h f Any -> BalancedTree ('Succ h) f (x <+> Any)
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
BalancedTree h f x
-> BalancedTree h f y -> BalancedTree ('Succ h) f (x <+> y)
BalPair BalancedTree h f x
x      (BalancedTree h f Any -> BalancedTree h f b)
-> m (BalancedTree h f Any) -> m (BalancedTree h f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((f x -> m (f y))
-> BalancedTree h f y -> Int -> Int -> m (BalancedTree h f Any)
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
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)))
  | Bool
otherwise         = (BalancedTree ('Succ h) f (Any <+> y) -> BalancedTree h f b
forall a b. a -> b
unsafeCoerce (BalancedTree ('Succ h) f (Any <+> y) -> BalancedTree h f b)
-> (BalancedTree h f Any -> BalancedTree ('Succ h) f (Any <+> y))
-> BalancedTree h f Any
-> BalancedTree h f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BalancedTree h f Any
 -> BalancedTree h f y -> BalancedTree ('Succ h) f (Any <+> y))
-> BalancedTree h f y
-> BalancedTree h f Any
-> BalancedTree ('Succ h) f (Any <+> y)
forall a b c. (a -> b -> c) -> b -> a -> c
flip BalancedTree h f Any
-> BalancedTree h f y -> BalancedTree ('Succ h) f (Any <+> y)
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
BalancedTree h f x
-> BalancedTree h f y -> BalancedTree ('Succ h) f (x <+> y)
BalPair BalancedTree h f y
y (BalancedTree h f Any -> BalancedTree h f b)
-> m (BalancedTree h f Any) -> m (BalancedTree h f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((f x -> m (f y))
-> BalancedTree h f x -> Int -> Int -> m (BalancedTree h f Any)
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
iInt -> Int -> Int
forall 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 (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) = h x -> BalancedTree 'Zero h (SingleCtx x)
forall k (f :: k -> *) (x :: k).
f x -> BalancedTree 'Zero f (SingleCtx x)
BalLeaf (h x -> BalancedTree 'Zero h (SingleCtx x))
-> m (h x) -> m (BalancedTree 'Zero h (SingleCtx x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> g x -> m (h x)
forall (x :: k). f x -> g x -> m (h x)
f f x
x g 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) =
  BalancedTree h h x -> BalancedTree h h y -> BalancedTree u h a
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
BalancedTree h f x
-> BalancedTree h f y -> BalancedTree ('Succ h) f (x <+> y)
BalPair (BalancedTree h h x -> BalancedTree h h y -> BalancedTree u h a)
-> m (BalancedTree h h x)
-> m (BalancedTree h h y -> BalancedTree u h a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: k). f x -> g x -> m (h x))
-> BalancedTree h f x
-> BalancedTree h g x
-> m (BalancedTree h h x)
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 (BalancedTree h g x -> BalancedTree h g x
forall a b. a -> b
unsafeCoerce BalancedTree h g x
y1)
          m (BalancedTree h h y -> BalancedTree u h a)
-> m (BalancedTree h h y) -> m (BalancedTree u h a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (x :: k). f x -> g x -> m (h x))
-> BalancedTree h f y
-> BalancedTree h g y
-> m (BalancedTree h h y)
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 (BalancedTree h g y -> BalancedTree h g y
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 :: 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
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
sInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1
tsize (PlusZero  Int
s BinomialTree ('Succ h) f a
_) = Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
s

t_cnt_size :: BinomialTree h f a -> Int
t_cnt_size :: 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) = BinomialTree ('Succ h) f x -> Int
forall k (h :: Height) (f :: k -> *) (a :: Ctx k).
BinomialTree h f a -> Int
t_cnt_size BinomialTree ('Succ h) f x
l Int -> Int -> Int
forall a. Num a => a -> a -> a
+ BalancedTree h f y -> Int
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) = BinomialTree ('Succ h) f a -> Int
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 :: BinomialTree h f x
-> BalancedTree h f y -> BinomialTree h f (x <+> y)
append BinomialTree h f x
Empty BalancedTree h f y
y = Int
-> BinomialTree ('Succ h) f EmptyCtx
-> BalancedTree h f y
-> BinomialTree h f (EmptyCtx <+> y)
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
Int
-> BinomialTree ('Succ h) f x
-> BalancedTree h f y
-> BinomialTree h f (x <+> y)
PlusOne Int
0 BinomialTree ('Succ h) f EmptyCtx
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 BinomialTree ('Succ h) f x
-> BalancedTree h f y
-> BalancedTree h f y
-> (x <+> (y <+> y)) :~: ((x <+> y) <+> y)
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' = BinomialTree ('Succ h) f x
-> BalancedTree ('Succ h) f (y <+> y)
-> BinomialTree ('Succ h) f (x <+> (y <+> y))
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 (BalancedTree h f y
-> BalancedTree h f y -> BalancedTree ('Succ h) f (y <+> y)
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
BalancedTree h f x
-> BalancedTree h f y -> BalancedTree ('Succ h) f (x <+> y)
BalPair BalancedTree h f y
x BalancedTree h f y
y)
       in Int
-> BinomialTree ('Succ h) f (x <+> (y <+> y))
-> BinomialTree h f (x <+> (y <+> y))
forall k (h :: Height) (f :: k -> *) (x :: Ctx k).
Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
PlusZero (BinomialTree ('Succ h) f (x <+> (y <+> y)) -> Int
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 = Int
-> BinomialTree ('Succ h) f x
-> BalancedTree h f y
-> BinomialTree h f (x <+> y)
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
Int
-> BinomialTree ('Succ h) f x
-> BalancedTree h f y
-> BinomialTree h f (x <+> y)
PlusOne Int
s BinomialTree ('Succ h) f x
t BalancedTree h f y
x

instance TestEqualityFC (BinomialTree h) where
  testEqualityFC :: (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 = (x :~: x) -> Maybe (x :~: x)
forall (m :: * -> *) a. Monad m => a -> m a
return x :~: x
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 (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> BinomialTree ('Succ h) f x
-> BinomialTree ('Succ h) f y
-> Maybe (x :~: y)
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
    (x :~: x) -> Maybe (x :~: x)
forall (m :: * -> *) a. Monad m => a -> m a
return x :~: x
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 (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> BinomialTree ('Succ h) f x
-> BinomialTree ('Succ h) f x
-> Maybe (x :~: x)
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 (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> BalancedTree h f y -> BalancedTree h f y -> Maybe (y :~: y)
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
    (x :~: x) -> Maybe (x :~: x)
forall (m :: * -> *) a. Monad m => a -> m a
return x :~: x
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
_ = Maybe (x :~: y)
forall a. Maybe a
Nothing

instance OrdFC (BinomialTree h) where
  compareFC :: (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 = OrderingF x y
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
_ = OrderingF x 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 = OrderingF x y
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) =
    OrderingF x y -> ((x ~ y) => OrderingF x y) -> OrderingF 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)
-> BinomialTree ('Succ h) f x
-> BinomialTree ('Succ h) f y
-> OrderingF x y
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) (((x ~ y) => OrderingF x y) -> OrderingF x y)
-> ((x ~ y) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$ (x ~ y) => OrderingF x y
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
_ = OrderingF x 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{} = OrderingF x y
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) =
    OrderingF x x -> ((x ~ x) => OrderingF x y) -> OrderingF 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)
-> BinomialTree ('Succ h) f x
-> BinomialTree ('Succ h) f x
-> OrderingF x x
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) (((x ~ x) => OrderingF x y) -> OrderingF x y)
-> ((x ~ x) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$
    OrderingF y y -> ((y ~ y) => OrderingF x y) -> OrderingF 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)
-> BalancedTree h f y -> BalancedTree h f y -> OrderingF y y
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) (((y ~ y) => OrderingF x y) -> OrderingF x y)
-> ((y ~ y) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$
    (y ~ y) => OrderingF x y
forall k (x :: k). OrderingF x x
EQF

instance HashableF f => HashableF (BinomialTree h f) where
  hashWithSaltF :: 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 Int -> BinomialTree ('Succ h) f tp -> Int
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 Int -> BinomialTree ('Succ h) f x -> Int
forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
`hashWithSaltF` BinomialTree ('Succ h) f x
x Int -> BalancedTree h f y -> Int
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 (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 = BinomialTree h g c
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) = Int
-> BinomialTree ('Succ h) g x
-> BalancedTree h g y
-> BinomialTree h g (x <+> y)
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
Int
-> BinomialTree ('Succ h) f x
-> BalancedTree h f y
-> BinomialTree h f (x <+> y)
PlusOne Int
s ((forall (tp :: k). f tp -> g tp)
-> BinomialTree ('Succ h) f x -> BinomialTree ('Succ h) g x
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 (tp :: k). f tp -> g tp)
-> BalancedTree h f y -> BalancedTree h g y
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)  = Int -> BinomialTree ('Succ h) g c -> BinomialTree h g c
forall k (h :: Height) (f :: k -> *) (x :: Ctx k).
Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
PlusZero Int
s ((forall (tp :: k). f tp -> g tp)
-> BinomialTree ('Succ h) f c -> BinomialTree ('Succ h) g c
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 (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 = BinomialTree h g EmptyCtx -> m (BinomialTree h g EmptyCtx)
forall (f :: * -> *) a. Applicative f => a -> f a
pure BinomialTree h g EmptyCtx
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) = Int
-> BinomialTree ('Succ h) g x
-> BalancedTree h g y
-> BinomialTree h g (x <+> y)
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
Int
-> BinomialTree ('Succ h) f x
-> BalancedTree h f y
-> BinomialTree h f (x <+> y)
PlusOne Int
s  (BinomialTree ('Succ h) g x
 -> BalancedTree h g y -> BinomialTree h g c)
-> m (BinomialTree ('Succ h) g x)
-> m (BalancedTree h g y -> BinomialTree h g c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (tp :: k). f tp -> m (g tp))
-> BinomialTree ('Succ h) f x -> m (BinomialTree ('Succ h) g x)
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 m (BalancedTree h g y -> BinomialTree h g c)
-> m (BalancedTree h g y) -> m (BinomialTree h g c)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (tp :: k). f tp -> m (g tp))
-> BalancedTree h f y -> m (BalancedTree h g y)
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)  = Int -> BinomialTree ('Succ h) g c -> BinomialTree h g c
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) g c -> BinomialTree h g c)
-> m (BinomialTree ('Succ h) g c) -> m (BinomialTree h g c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (tp :: k). f tp -> m (g tp))
-> BinomialTree ('Succ h) f c -> m (BinomialTree ('Succ h) g c)
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 :: 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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = BinomialTree Any Any 'EmptyCtx -> BinomialTree h f t
forall a b. a -> b
unsafeCoerce BinomialTree Any Any 'EmptyCtx
forall k (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
Empty
  | Int
sz Int -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
0 =
    let s :: Int
s = Int
sz Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftR` Int
1
        t :: BinomialTree ('Succ Any) f Any
t = Int
-> Int
-> (forall (x :: k). Index ctx x -> f x)
-> BinomialTree ('Succ Any) f Any
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
hInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) forall (x :: k). Index ctx x -> f x
f
        o :: Int
o = Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
2Int -> Int -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
hInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
        u :: BalancedTree Any f Any
u = Bool -> BalancedTree Any f Any -> BalancedTree Any f Any
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
o Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== BinomialTree ('Succ Any) f Any -> Int
forall k (h :: Height) (f :: k -> *) (a :: Ctx k).
BinomialTree h f a -> Int
t_cnt_size BinomialTree ('Succ Any) f Any
t) (BalancedTree Any f Any -> BalancedTree Any f Any)
-> BalancedTree Any f Any -> BalancedTree Any f Any
forall a b. (a -> b) -> a -> b
$ Int
-> Int
-> (forall (x :: k). Index ctx x -> f x)
-> BalancedTree Any f Any
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 BinomialTree Any f (Any <+> Any) -> BinomialTree h f t
forall a b. a -> b
unsafeCoerce (Int
-> BinomialTree ('Succ Any) f Any
-> BalancedTree Any f Any
-> BinomialTree Any f (Any <+> Any)
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
Int
-> BinomialTree ('Succ h) f x
-> BalancedTree h f y
-> BinomialTree h f (x <+> y)
PlusOne Int
s BinomialTree ('Succ Any) f Any
t BalancedTree Any f Any
u)
  | Bool
otherwise =
    let s :: Int
s = Int
sz Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftR` Int
1
        t :: BinomialTree ('Succ h) f t
t = Int
-> Int
-> (forall (x :: k). Index ctx x -> f x)
-> BinomialTree ('Succ h) f 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 Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftR` Int
1) (Int
hInt -> Int -> Int
forall 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 = Int -> BinomialTree ('Succ h) f t -> BinomialTree h f t
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 :: 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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = BinomialTree h f t -> m (BinomialTree h f t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BinomialTree Any Any 'EmptyCtx -> BinomialTree h f t
forall a b. a -> b
unsafeCoerce BinomialTree Any Any 'EmptyCtx
forall k (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
Empty)
  | Int
sz Int -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
0 =
    let s :: Int
s = Int
sz Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftR` Int
1
        t :: m (BinomialTree Any f Any)
t = Int
-> Int
-> (forall (x :: k). Index ctx x -> m (f x))
-> m (BinomialTree Any f Any)
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
hInt -> Int -> Int
forall 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 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
2Int -> Int -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^(Int
hInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
        u :: m (BalancedTree Any f Any)
u = Int
-> Int
-> (forall (x :: k). Index ctx x -> m (f x))
-> m (BalancedTree Any f Any)
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 = (BinomialTree ('Succ Any) Any Any
 -> BalancedTree Any Any Any -> BinomialTree Any Any (Any <+> Any))
-> BinomialTree Any f Any
-> BalancedTree Any f Any
-> BinomialTree h f t
forall a b. a -> b
unsafeCoerce (Int
-> BinomialTree ('Succ Any) Any Any
-> BalancedTree Any Any Any
-> BinomialTree Any Any (Any <+> Any)
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
Int
-> BinomialTree ('Succ h) f x
-> BalancedTree h f y
-> BinomialTree h f (x <+> y)
PlusOne Int
s) (BinomialTree Any f Any
 -> BalancedTree Any f Any -> BinomialTree h f t)
-> m (BinomialTree Any f Any)
-> m (BalancedTree Any f Any -> BinomialTree h f t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (BinomialTree Any f Any)
t m (BalancedTree Any f Any -> BinomialTree h f t)
-> m (BalancedTree Any f Any) -> m (BinomialTree h f 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 Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftR` Int
1
        t :: m (BinomialTree ('Succ h) f t)
t = Int
-> Int
-> (forall (x :: k). Index ctx x -> m (f x))
-> m (BinomialTree ('Succ h) f 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
hInt -> Int -> Int
forall 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 = Int -> BinomialTree ('Succ h) f t -> BinomialTree h f t
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 -> BinomialTree h f t)
-> m (BinomialTree ('Succ h) f t) -> m (BinomialTree h f t)
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 :: BinomialTree h f x -> BalancedTree h f y -> DropResult f (x <+> y)
bal_drop BinomialTree h f x
t (BalLeaf f x
e) = BinomialTree 'Zero f x -> f x -> DropResult f (x ::> x)
forall k (f :: k -> *) (x :: Ctx k) (y :: k).
BinomialTree 'Zero f x -> f y -> DropResult f (x ::> y)
DropExt BinomialTree h f x
BinomialTree 'Zero f x
t f x
e
bal_drop BinomialTree h f x
t (BalPair BalancedTree h f x
x BalancedTree h f y
y) =
  DropResult f ((Any <+> x) <+> y) -> DropResult f (x <+> y)
forall a b. a -> b
unsafeCoerce (BinomialTree h f (Any <+> x)
-> BalancedTree h f y -> DropResult f ((Any <+> x) <+> y)
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 (Int
-> BinomialTree ('Succ h) f Any
-> BalancedTree h f x
-> BinomialTree h f (Any <+> x)
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
Int
-> BinomialTree ('Succ h) f x
-> BalancedTree h f y
-> BinomialTree h f (x <+> y)
PlusOne (BinomialTree h f x -> Int
forall k (h :: Height) (f :: k -> *) (a :: Ctx k).
BinomialTree h f a -> Int
tsize BinomialTree h f x
t) (BinomialTree h f x -> BinomialTree ('Succ h) f Any
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 :: BinomialTree h f ctx -> DropResult f ctx
bin_drop BinomialTree h f ctx
Empty = DropResult f ctx
forall k (f :: k -> *). DropResult f EmptyCtx
DropEmpty
bin_drop (PlusZero Int
_ BinomialTree ('Succ h) f ctx
u) = BinomialTree ('Succ h) f ctx -> DropResult f ctx
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 -> BinomialTree h f x
forall k (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
Empty
            BinomialTree ('Succ h) f x
_ -> Int -> BinomialTree ('Succ h) f x -> BinomialTree 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 BinomialTree h f x -> BalancedTree h f y -> DropResult f (x <+> y)
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 :: BinomialTree h f a -> Int -> Int -> f u
unsafe_bin_index BinomialTree h f a
_ Int
_ Int
i
  | Int -> Bool -> Bool
seq Int
i Bool
False = String -> f u
forall a. (?callStack::CallStack) => String -> a
error String
"bad unsafe_bin_index"
unsafe_bin_index BinomialTree h f a
Empty Int
_ Int
_ = String -> f u
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftR` (Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
i) = BalancedTree h f y -> Int -> Int -> f u
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 = BinomialTree ('Succ h) f x -> Int -> Int -> f u
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 (Int -> f u) -> Int -> f u
forall a b. (a -> b) -> a -> b
$! (Int
1Int -> Int -> Int
forall 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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftR` (Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
i) = String -> f u
forall a. (?callStack::CallStack) => String -> a
error String
"unsafe_bin_index stopped at PlusZero"
  | Bool
otherwise = BinomialTree ('Succ h) f a -> Int -> Int -> f u
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 (Int -> f u) -> Int -> f u
forall a b. (a -> b) -> a -> b
$! (Int
1Int -> Int -> Int
forall 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 :: (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
_ = String -> m (BinomialTree h f b)
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftR` (Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
i) =
    BinomialTree h f (x <+> Any) -> BinomialTree h f b
forall a b. a -> b
unsafeCoerce (BinomialTree h f (x <+> Any) -> BinomialTree h f b)
-> (BalancedTree h f Any -> BinomialTree h f (x <+> Any))
-> BalancedTree h f Any
-> BinomialTree h f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int
-> BinomialTree ('Succ h) f x
-> BalancedTree h f Any
-> BinomialTree h f (x <+> Any)
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
Int
-> BinomialTree ('Succ h) f x
-> BalancedTree h f y
-> BinomialTree h f (x <+> y)
PlusOne Int
sz BinomialTree ('Succ h) f x
t        (BalancedTree h f Any -> BinomialTree h f b)
-> m (BalancedTree h f Any) -> m (BinomialTree h f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((f x -> m (f y))
-> BalancedTree h f y -> Int -> Int -> m (BalancedTree h f Any)
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 =
    BinomialTree h f (Any <+> y) -> BinomialTree h f b
forall a b. a -> b
unsafeCoerce (BinomialTree h f (Any <+> y) -> BinomialTree h f b)
-> (BinomialTree ('Succ h) f Any -> BinomialTree h f (Any <+> y))
-> BinomialTree ('Succ h) f Any
-> BinomialTree h f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BinomialTree ('Succ h) f Any
 -> BalancedTree h f y -> BinomialTree h f (Any <+> y))
-> BalancedTree h f y
-> BinomialTree ('Succ h) f Any
-> BinomialTree h f (Any <+> y)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Int
-> BinomialTree ('Succ h) f Any
-> BalancedTree h f y
-> BinomialTree h f (Any <+> y)
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
Int
-> BinomialTree ('Succ h) f x
-> BalancedTree h f y
-> BinomialTree h f (x <+> y)
PlusOne Int
sz) BalancedTree h f y
u (BinomialTree ('Succ h) f Any -> BinomialTree h f b)
-> m (BinomialTree ('Succ h) f Any) -> m (BinomialTree h f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((f x -> m (f y))
-> BinomialTree ('Succ h) f x
-> Int
-> Int
-> m (BinomialTree ('Succ h) f Any)
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
iInt -> Int -> Int
forall 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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j Int -> Int -> Int
forall a. Bits a => a -> Int -> a
`shiftR` (Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
i) = String -> m (BinomialTree h f b)
forall a. (?callStack::CallStack) => String -> a
error String
"unsafe_bin_adjust stopped at PlusZero"
  | Bool
otherwise = Int -> BinomialTree ('Succ h) f b -> BinomialTree h f b
forall k (h :: Height) (f :: k -> *) (x :: Ctx k).
Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
PlusZero Int
sz (BinomialTree ('Succ h) f b -> BinomialTree h f b)
-> m (BinomialTree ('Succ h) f b) -> m (BinomialTree h f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((f x -> m (f y))
-> BinomialTree ('Succ h) f a
-> Int
-> Int
-> m (BinomialTree ('Succ h) 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
iInt -> Int -> Int
forall 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 (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 = BinomialTree u h EmptyCtx -> m (BinomialTree u h EmptyCtx)
forall (f :: * -> *) a. Applicative f => a -> f a
pure BinomialTree u h EmptyCtx
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) =
  Int
-> BinomialTree ('Succ u) h x
-> BalancedTree u h y
-> BinomialTree u h (x <+> y)
forall k (h :: Height) (f :: k -> *) (x :: Ctx k) (y :: Ctx k).
Int
-> BinomialTree ('Succ h) f x
-> BalancedTree h f y
-> BinomialTree h f (x <+> y)
PlusOne Int
s (BinomialTree ('Succ u) h x
 -> BalancedTree u h y -> BinomialTree u h a)
-> m (BinomialTree ('Succ u) h x)
-> m (BalancedTree u h y -> BinomialTree u h a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: k). f x -> g x -> m (h x))
-> BinomialTree ('Succ u) f x
-> BinomialTree ('Succ u) g x
-> m (BinomialTree ('Succ u) h x)
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 (BinomialTree ('Succ u) g x -> BinomialTree ('Succ u) g x
forall a b. a -> b
unsafeCoerce BinomialTree ('Succ u) g x
y1)
            m (BalancedTree u h y -> BinomialTree u h a)
-> m (BalancedTree u h y) -> m (BinomialTree u h a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (x :: k). f x -> g x -> m (h x))
-> BalancedTree u f y
-> BalancedTree u g y
-> m (BalancedTree u h y)
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 (BalancedTree u g y -> BalancedTree u g y
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) =
  Int -> BinomialTree ('Succ u) h a -> BinomialTree u h a
forall k (h :: Height) (f :: k -> *) (x :: Ctx k).
Int -> BinomialTree ('Succ h) f x -> BinomialTree h f x
PlusZero Int
s (BinomialTree ('Succ u) h a -> BinomialTree u h a)
-> m (BinomialTree ('Succ u) h a) -> m (BinomialTree u h a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: k). f x -> g x -> m (h x))
-> BinomialTree ('Succ u) f a
-> BinomialTree ('Succ u) g a
-> m (BinomialTree ('Succ u) h a)
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
_ = String -> m (BinomialTree u h 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 = Assignment f ctx -> () -> ()
seq Assignment f ctx
a ()

-- | Return number of elements in assignment.
size :: Assignment f ctx -> Size ctx
size :: Assignment f ctx -> Size ctx
size (Assignment BinomialTree 'Zero f ctx
t) = Int -> Size ctx
forall k (ctx :: Ctx k). Int -> Size ctx
Size (BinomialTree 'Zero f ctx -> Int
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 :: Size ctx -> (forall (tp :: k). f tp) -> Assignment f ctx
replicate Size ctx
n forall (tp :: k). f tp
c = Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
forall k (ctx :: Ctx k) (f :: k -> *).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
generate Size ctx
n (\Index ctx tp
_ -> f tp
forall (tp :: k). f tp
c)

-- | Generate an assignment
generate :: Size ctx
         -> (forall tp . Index ctx tp -> f tp)
         -> Assignment f ctx
generate :: 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  = BinomialTree 'Zero f ctx -> Assignment f ctx
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 = Int
-> Int
-> (forall (tp :: k). Index ctx tp -> f tp)
-> BinomialTree 'Zero f ctx
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 (Size ctx -> Int
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 :: 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 = BinomialTree 'Zero f ctx -> Assignment f ctx
forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment (BinomialTree 'Zero f ctx -> Assignment f ctx)
-> m (BinomialTree 'Zero f ctx) -> m (Assignment f ctx)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> Int
-> (forall (tp :: k). Index ctx tp -> m (f tp))
-> m (BinomialTree 'Zero f ctx)
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 (Size ctx -> Int
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 :: Assignment f EmptyCtx
empty = BinomialTree 'Zero f EmptyCtx -> Assignment f EmptyCtx
forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment BinomialTree 'Zero f EmptyCtx
forall k (h :: Height) (f :: k -> *). BinomialTree h f EmptyCtx
Empty

extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x)
extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x)
extend (Assignment BinomialTree 'Zero f ctx
x) f x
y = BinomialTree 'Zero f (ctx ::> x) -> Assignment f (ctx ::> x)
forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment (BinomialTree 'Zero f (ctx ::> x) -> Assignment f (ctx ::> x))
-> BinomialTree 'Zero f (ctx ::> x) -> Assignment f (ctx ::> x)
forall a b. (a -> b) -> a -> b
$ BinomialTree 'Zero f ctx
-> BalancedTree 'Zero f (SingleCtx x)
-> BinomialTree 'Zero f (ctx <+> SingleCtx x)
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 (f x -> BalancedTree 'Zero f (SingleCtx x)
forall k (f :: k -> *) (x :: k).
f x -> BalancedTree 'Zero f (SingleCtx x)
BalLeaf f x
y)

-- | Unexported index that returns an arbitrary type of expression.
unsafeIndex :: proxy u -> Int -> Assignment f ctx -> f u
unsafeIndex :: proxy u -> Int -> Assignment f ctx -> f u
unsafeIndex proxy u
_ Int
idx (Assignment BinomialTree 'Zero f ctx
t) = BinomialTree 'Zero f ctx -> f u -> f u
seq BinomialTree 'Zero f ctx
t (f u -> f u) -> f u -> f u
forall a b. (a -> b) -> a -> b
$ BinomialTree 'Zero f ctx -> Int -> Int -> f u
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 ! :: Assignment f ctx -> Index ctx tp -> f tp
! Index Int
i = Bool -> f tp -> f tp
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Size ctx -> Int
forall k (ctx :: Ctx k). Size ctx -> Int
sizeInt (Assignment f ctx -> Size ctx
forall k (f :: k -> *) (ctx :: Ctx k). Assignment f ctx -> Size ctx
size Assignment f ctx
a)) (f tp -> f tp) -> f tp -> f tp
forall a b. (a -> b) -> a -> b
$
              Proxy tp -> Int -> Assignment f ctx -> f tp
forall k (proxy :: k -> *) (u :: k) (f :: k -> *) (ctx :: Ctx k).
proxy u -> Int -> Assignment f ctx -> f u
unsafeIndex Proxy tp
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 !^ :: Assignment f r -> Index l tp -> f tp
!^ Index l tp
i = Assignment f r
a Assignment f r -> Index r tp -> f tp
forall k (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Index l tp -> Index r 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 (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 (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> BinomialTree 'Zero f x
-> BinomialTree 'Zero f y
-> Maybe (x :~: y)
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
     (x :~: x) -> Maybe (x :~: x)
forall (m :: * -> *) a. Monad m => a -> m a
return x :~: x
forall k (a :: k). a :~: a
Refl

instance TestEquality f => TestEquality (Assignment f) where
  testEquality :: Assignment f a -> Assignment f b -> Maybe (a :~: b)
testEquality = (forall (x :: k) (y :: k). f x -> f y -> Maybe (x :~: y))
-> forall (a :: Ctx k) (b :: Ctx k).
   Assignment f a -> Assignment f b -> Maybe (a :~: b)
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)
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 = Maybe (ctx :~: ctx) -> Bool
forall a. Maybe a -> Bool
isJust (Assignment f ctx -> Assignment f ctx -> Maybe (ctx :~: ctx)
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 (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) =
     OrderingF x y -> ((x ~ y) => OrderingF x y) -> OrderingF 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)
-> BinomialTree 'Zero f x
-> BinomialTree 'Zero f y
-> OrderingF x y
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) (((x ~ y) => OrderingF x y) -> OrderingF x y)
-> ((x ~ y) => OrderingF x y) -> OrderingF x y
forall a b. (a -> b) -> a -> b
$ (x ~ y) => OrderingF x y
forall k (x :: k). OrderingF x x
EQF

instance OrdF f => OrdF (Assignment f) where
  compareF :: Assignment f x -> Assignment f y -> OrderingF x y
compareF = (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
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
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 = OrderingF ctx ctx -> Ordering
forall k (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (Assignment f ctx -> Assignment f ctx -> OrderingF ctx ctx
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 :: Int -> Index ctx tp -> Int
hashWithSaltF Int
s Index ctx tp
i = Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (Index ctx tp -> Int
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 = Int -> Index ctx tp -> Int
forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
hashWithSaltF

instance HashableF f => Hashable (Assignment f ctx) where
  hashWithSalt :: Int -> Assignment f ctx -> Int
hashWithSalt Int
s (Assignment BinomialTree 'Zero f ctx
a) = Int -> BinomialTree 'Zero f ctx -> Int
forall k (f :: k -> *) (tp :: k). HashableF f => Int -> f tp -> Int
hashWithSaltF Int
s BinomialTree 'Zero f ctx
a

instance HashableF f => HashableF (Assignment f) where
  hashWithSaltF :: Int -> Assignment f tp -> Int
hashWithSaltF = Int -> Assignment f tp -> Int
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
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
Prelude.++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((forall (x :: k). f x -> String) -> Assignment f ctx -> [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 (x :: k). f x -> String
forall k (f :: k -> *) (tp :: k). ShowF f => f tp -> String
showF Assignment f ctx
a) String -> ShowS
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 :: (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 = Identity (Assignment f ctx) -> Assignment f ctx
forall a. Identity a -> a
runIdentity ((f tp -> Identity (f tp))
-> Index ctx tp -> Assignment f ctx -> Identity (Assignment f ctx)
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 -> Identity (f tp)
forall a. a -> Identity a
Identity (f tp -> Identity (f tp))
-> (f tp -> f tp) -> f tp -> Identity (f tp)
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 :: Index ctx tp -> f tp -> Assignment f ctx -> Assignment f ctx
update Index ctx tp
i f tp
v Assignment f ctx
a = (f tp -> f tp)
-> Index ctx tp -> Assignment f ctx -> Assignment f ctx
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 :: (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) = BinomialTree 'Zero f ctx -> Assignment f ctx
forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment (BinomialTree 'Zero f ctx -> Assignment f ctx)
-> m (BinomialTree 'Zero f ctx) -> m (Assignment f ctx)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((f tp -> m (f tp))
-> BinomialTree 'Zero f ctx
-> Int
-> Int
-> m (BinomialTree 'Zero f ctx)
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' :: Index ctx x -> Lens' (Assignment f ctx) (f x)
ixF' Index ctx x
idx f x -> f (f x)
f = (f x -> f (f x))
-> Index ctx x -> Assignment f ctx -> f (Assignment f ctx)
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 :: IndexF (Assignment f ctx) x
-> Traversal' (Assignment f ctx) (IxValueF (Assignment f ctx) x)
ixF = IndexF (Assignment f ctx) x
-> (IxValueF (Assignment f ctx) x
    -> f (IxValueF (Assignment f ctx) x))
-> Assignment f ctx
-> f (Assignment f ctx)
forall k m (x :: k).
IxedF' k m =>
IndexF m x -> Lens' m (IxValueF m x)
ixF'

-- 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 :: Int -> Assignment f ctx -> f u -> Assignment f ctx'
unsafeUpdate Int
i (Assignment BinomialTree 'Zero f ctx
a) f u
e = BinomialTree 'Zero f ctx' -> Assignment f ctx'
forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment (Identity (BinomialTree 'Zero f ctx') -> BinomialTree 'Zero f ctx'
forall a. Identity a -> a
runIdentity ((f Any -> Identity (f u))
-> BinomialTree 'Zero f ctx
-> Int
-> Int
-> Identity (BinomialTree 'Zero f ctx')
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
_ -> f u -> Identity (f u)
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 :: Assignment f ctx -> AssignView f ctx
viewAssign (Assignment BinomialTree 'Zero f ctx
x) =
  case BinomialTree 'Zero f ctx -> DropResult f ctx
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 -> AssignView f ctx
forall k (f :: k -> *). AssignView f EmptyCtx
AssignEmpty
    DropExt BinomialTree 'Zero f x
t f y
v -> Assignment f x -> f y -> AssignView f (x ::> y)
forall k (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> f tp -> AssignView f (ctx ::> tp)
AssignExtend (BinomialTree 'Zero f x -> Assignment f x
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 (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 -> Identity (Assignment h a) -> Assignment h a
forall a. Identity a -> a
runIdentity (Identity (Assignment h a) -> Assignment h a)
-> Identity (Assignment h a) -> Assignment h a
forall a b. (a -> b) -> a -> b
$ (forall (x :: k). f x -> g x -> Identity (h x))
-> Assignment f a -> Assignment g a -> Identity (Assignment h a)
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 -> h x -> Identity (h x)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (f x -> g x -> h x
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 (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) = BinomialTree 'Zero h a -> Assignment h a
forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment (BinomialTree 'Zero h a -> Assignment h a)
-> m (BinomialTree 'Zero h a) -> m (Assignment h a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: k). f x -> g x -> m (h x))
-> BinomialTree 'Zero f a
-> BinomialTree 'Zero g a
-> m (BinomialTree 'Zero h a)
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 (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) -> BinomialTree 'Zero g x -> Assignment g x
forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment ((forall (x :: k). f x -> g x)
-> BinomialTree 'Zero f x -> BinomialTree 'Zero g x
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 (x :: k). f x -> m)
-> forall (x :: Ctx k). Assignment f x -> m
foldMapFC = (forall (x :: k). f x -> m) -> Assignment f x -> m
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 (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) -> BinomialTree 'Zero g x -> Assignment g x
forall k (f :: k -> *) (ctx :: Ctx k).
BinomialTree 'Zero f ctx -> Assignment f ctx
Assignment (BinomialTree 'Zero g x -> Assignment g x)
-> m (BinomialTree 'Zero g x) -> m (Assignment g x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: k). f x -> m (g x))
-> BinomialTree 'Zero f x -> m (BinomialTree 'Zero g x)
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 #-}

traverseWithIndex :: Applicative m
                  => (forall tp . 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))
-> Assignment f ctx -> m (Assignment g ctx)
traverseWithIndex forall (tp :: k). Index ctx tp -> f tp -> m (g tp)
f Assignment f ctx
a = Size ctx
-> (forall (tp :: k). Index ctx tp -> m (g tp))
-> m (Assignment g ctx)
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 (Assignment f ctx -> Size ctx
forall k (f :: k -> *) (ctx :: Ctx k). Assignment f ctx -> Size ctx
size Assignment f ctx
a) ((forall (tp :: k). Index ctx tp -> m (g tp))
 -> m (Assignment g ctx))
-> (forall (tp :: k). Index ctx tp -> m (g tp))
-> m (Assignment g ctx)
forall a b. (a -> b) -> a -> b
$ \Index ctx tp
i -> Index ctx tp -> f tp -> m (g tp)
forall (tp :: k). Index ctx tp -> f tp -> m (g tp)
f Index ctx tp
i (Assignment f ctx
a Assignment f ctx -> Index ctx tp -> f tp
forall k (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
! Index ctx tp
i)

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

appendBal :: Assignment f x -> BalancedTree h f y -> Assignment f (x <+> y)
appendBal :: Assignment f x -> BalancedTree h f y -> Assignment f (x <+> y)
appendBal Assignment f x
x (BalLeaf f x
a) = Assignment f x
x Assignment f x -> f x -> Assignment f (x ::> x)
forall k (f :: k -> *) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
`extend` f x
a
appendBal Assignment f x
x (BalPair BalancedTree h f x
y BalancedTree h f y
z) =
  case Assignment f x
-> BalancedTree h f x
-> BalancedTree h f y
-> (x <+> (x <+> y)) :~: ((x <+> x) <+> y)
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 Assignment f x -> BalancedTree h f x -> 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 Assignment f (x <+> x)
-> BalancedTree h f y -> Assignment f ((x <+> 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 :: Assignment f x -> BinomialTree h f y -> Assignment f (x <+> y)
appendBin Assignment f x
x BinomialTree h f y
Empty = Assignment f x
Assignment f (x <+> y)
x
appendBin Assignment f x
x (PlusOne Int
_ BinomialTree ('Succ h) f x
y BalancedTree h f y
z) =
  case Assignment f x
-> BinomialTree ('Succ h) f x
-> BalancedTree h f y
-> (x <+> (x <+> y)) :~: ((x <+> x) <+> y)
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 Assignment f x
-> BinomialTree ('Succ h) f x -> 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 Assignment f (x <+> x)
-> BalancedTree h f y -> Assignment f ((x <+> 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 Assignment f x
-> BinomialTree ('Succ h) f y -> Assignment f (x <+> y)
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 <++> :: Assignment f x -> Assignment f y -> Assignment f (x <+> y)
<++> Assignment BinomialTree 'Zero f y
y = Assignment f x
x Assignment f x -> BinomialTree 'Zero f y -> Assignment f (x <+> y)
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 = Assignment f ctx
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr Assignment f ctx -> f bt -> Assignment f (ctx ::> bt)
forall k (f :: k -> *) (ctx :: Ctx k) (x :: k).
Assignment f ctx -> f x -> Assignment f (ctx ::> x)
`extend` f bt
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

instance KnownRepr (Assignment f) EmptyCtx where
  knownRepr :: Assignment f EmptyCtx
knownRepr = Assignment f EmptyCtx
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 :: Int -> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
unsafeLens Int
idx =
  (Assignment f ctx -> f tp)
-> (Assignment f ctx -> f u -> Assignment f ctx')
-> Lens (Assignment f ctx) (Assignment f ctx') (f tp) (f u)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Lens.lens (Proxy tp -> Int -> Assignment f ctx -> f tp
forall k (proxy :: k -> *) (u :: k) (f :: k -> *) (ctx :: Ctx k).
proxy u -> Int -> Assignment f ctx -> f u
unsafeIndex Proxy tp
forall k (t :: k). Proxy t
Proxy Int
idx) (Int -> Assignment f ctx -> f u -> Assignment f ctx'
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 :: (f t -> f (f u)) -> Assignment1 f t -> f (Assignment1 f u)
_1 = Int -> Lens (Assignment1 f t) (Assignment1 f u) (f t) (f u)
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 :: (f t -> f (f u)) -> Assignment2 f t x2 -> f (Assignment2 f u x2)
_1 = Int -> Lens (Assignment2 f t x2) (Assignment2 f u x2) (f t) (f u)
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 :: (f t -> f (f u)) -> Assignment2 f x1 t -> f (Assignment2 f x1 u)
_2 = Int -> Lens (Assignment2 f x1 t) (Assignment2 f x1 u) (f t) (f u)
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 :: (f t -> f (f u))
-> Assignment3 f t x2 x3 -> f (Assignment3 f u x2 x3)
_1 = Int
-> Lens (Assignment3 f t x2 x3) (Assignment3 f u x2 x3) (f t) (f u)
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 :: (f t -> f (f u))
-> Assignment3 f x1 t x3 -> f (Assignment3 f x1 u x3)
_2 = Int
-> Lens (Assignment3 f x1 t x3) (Assignment3 f x1 u x3) (f t) (f u)
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 :: (f t -> f (f u))
-> Assignment3 f x1 x2 t -> f (Assignment3 f x1 x2 u)
_3 = Int
-> Lens (Assignment3 f x1 x2 t) (Assignment3 f x1 x2 u) (f t) (f u)
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 :: (f t -> f (f u))
-> Assignment4 f t x2 x3 x4 -> f (Assignment4 f u x2 x3 x4)
_1 = Int
-> Lens
     (Assignment4 f t x2 x3 x4) (Assignment4 f u x2 x3 x4) (f t) (f u)
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 :: (f t -> f (f u))
-> Assignment4 f x1 t x3 x4 -> f (Assignment4 f x1 u x3 x4)
_2 = Int
-> Lens
     (Assignment4 f x1 t x3 x4) (Assignment4 f x1 u x3 x4) (f t) (f u)
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 :: (f t -> f (f u))
-> Assignment4 f x1 x2 t x4 -> f (Assignment4 f x1 x2 u x4)
_3 = Int
-> Lens
     (Assignment4 f x1 x2 t x4) (Assignment4 f x1 x2 u x4) (f t) (f u)
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 :: (f t -> f (f u))
-> Assignment4 f x1 x2 x3 t -> f (Assignment4 f x1 x2 x3 u)
_4 = Int
-> Lens
     (Assignment4 f x1 x2 x3 t) (Assignment4 f x1 x2 x3 u) (f t) (f u)
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 :: (f t -> f (f u))
-> Assignment5 f t x2 x3 x4 x5 -> f (Assignment5 f u x2 x3 x4 x5)
_1 = Int
-> Lens
     (Assignment5 f t x2 x3 x4 x5)
     (Assignment5 f u x2 x3 x4 x5)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment5 f x1 t x3 x4 x5 -> f (Assignment5 f x1 u x3 x4 x5)
_2 = Int
-> Lens
     (Assignment5 f x1 t x3 x4 x5)
     (Assignment5 f x1 u x3 x4 x5)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment5 f x1 x2 t x4 x5 -> f (Assignment5 f x1 x2 u x4 x5)
_3 = Int
-> Lens
     (Assignment5 f x1 x2 t x4 x5)
     (Assignment5 f x1 x2 u x4 x5)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment5 f x1 x2 x3 t x5 -> f (Assignment5 f x1 x2 x3 u x5)
_4 = Int
-> Lens
     (Assignment5 f x1 x2 x3 t x5)
     (Assignment5 f x1 x2 x3 u x5)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment5 f x1 x2 x3 x4 t -> f (Assignment5 f x1 x2 x3 x4 u)
_5 = Int
-> Lens
     (Assignment5 f x1 x2 x3 x4 t)
     (Assignment5 f x1 x2 x3 x4 u)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment6 f t x2 x3 x4 x5 x6
-> f (Assignment6 f u x2 x3 x4 x5 x6)
_1 = Int
-> Lens
     (Assignment6 f t x2 x3 x4 x5 x6)
     (Assignment6 f u x2 x3 x4 x5 x6)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment6 f x1 t x3 x4 x5 x6
-> f (Assignment6 f x1 u x3 x4 x5 x6)
_2 = Int
-> Lens
     (Assignment6 f x1 t x3 x4 x5 x6)
     (Assignment6 f x1 u x3 x4 x5 x6)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment6 f x1 x2 t x4 x5 x6
-> f (Assignment6 f x1 x2 u x4 x5 x6)
_3 = Int
-> Lens
     (Assignment6 f x1 x2 t x4 x5 x6)
     (Assignment6 f x1 x2 u x4 x5 x6)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment6 f x1 x2 x3 t x5 x6
-> f (Assignment6 f x1 x2 x3 u x5 x6)
_4 = Int
-> Lens
     (Assignment6 f x1 x2 x3 t x5 x6)
     (Assignment6 f x1 x2 x3 u x5 x6)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment6 f x1 x2 x3 x4 t x6
-> f (Assignment6 f x1 x2 x3 x4 u x6)
_5 = Int
-> Lens
     (Assignment6 f x1 x2 x3 x4 t x6)
     (Assignment6 f x1 x2 x3 x4 u x6)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment6 f x1 x2 x3 x4 x5 t
-> f (Assignment6 f x1 x2 x3 x4 x5 u)
_6 = Int
-> Lens
     (Assignment6 f x1 x2 x3 x4 x5 t)
     (Assignment6 f x1 x2 x3 x4 x5 u)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment7 f t x2 x3 x4 x5 x6 x7
-> f (Assignment7 f u x2 x3 x4 x5 x6 x7)
_1 = Int
-> Lens
     (Assignment7 f t x2 x3 x4 x5 x6 x7)
     (Assignment7 f u x2 x3 x4 x5 x6 x7)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment7 f x1 t x3 x4 x5 x6 x7
-> f (Assignment7 f x1 u x3 x4 x5 x6 x7)
_2 = Int
-> Lens
     (Assignment7 f x1 t x3 x4 x5 x6 x7)
     (Assignment7 f x1 u x3 x4 x5 x6 x7)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment7 f x1 x2 t x4 x5 x6 x7
-> f (Assignment7 f x1 x2 u x4 x5 x6 x7)
_3 = Int
-> Lens
     (Assignment7 f x1 x2 t x4 x5 x6 x7)
     (Assignment7 f x1 x2 u x4 x5 x6 x7)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment7 f x1 x2 x3 t x5 x6 x7
-> f (Assignment7 f x1 x2 x3 u x5 x6 x7)
_4 = Int
-> Lens
     (Assignment7 f x1 x2 x3 t x5 x6 x7)
     (Assignment7 f x1 x2 x3 u x5 x6 x7)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment7 f x1 x2 x3 x4 t x6 x7
-> f (Assignment7 f x1 x2 x3 x4 u x6 x7)
_5 = Int
-> Lens
     (Assignment7 f x1 x2 x3 x4 t x6 x7)
     (Assignment7 f x1 x2 x3 x4 u x6 x7)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment7 f x1 x2 x3 x4 x5 t x7
-> f (Assignment7 f x1 x2 x3 x4 x5 u x7)
_6 = Int
-> Lens
     (Assignment7 f x1 x2 x3 x4 x5 t x7)
     (Assignment7 f x1 x2 x3 x4 x5 u x7)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment7 f x1 x2 x3 x4 x5 x6 t
-> f (Assignment7 f x1 x2 x3 x4 x5 x6 u)
_7 = Int
-> Lens
     (Assignment7 f x1 x2 x3 x4 x5 x6 t)
     (Assignment7 f x1 x2 x3 x4 x5 x6 u)
     (f t)
     (f u)
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 :: (f t -> f (f u))
-> Assignment8 f t x2 x3 x4 x5 x6 x7 x8
-> f (Assignment8 f u x2 x3 x4 x5 x6 x7 x8)
_1 = Int
-> 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)
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 :: (f t -> f (f u))
-> Assignment8 f x1 t x3 x4 x5 x6 x7 x8
-> f (Assignment8 f x1 u x3 x4 x5 x6 x7 x8)
_2 = Int
-> 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)
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 :: (f t -> f (f u))
-> Assignment8 f x1 x2 t x4 x5 x6 x7 x8
-> f (Assignment8 f x1 x2 u x4 x5 x6 x7 x8)
_3 = Int
-> 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)
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 :: (f t -> f (f u))
-> Assignment8 f x1 x2 x3 t x5 x6 x7 x8
-> f (Assignment8 f x1 x2 x3 u x5 x6 x7 x8)
_4 = Int
-> 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)
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 :: (f t -> f (f u))
-> Assignment8 f x1 x2 x3 x4 t x6 x7 x8
-> f (Assignment8 f x1 x2 x3 x4 u x6 x7 x8)
_5 = Int
-> 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)
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 :: (f t -> f (f u))
-> Assignment8 f x1 x2 x3 x4 x5 t x7 x8
-> f (Assignment8 f x1 x2 x3 x4 x5 u x7 x8)
_6 = Int
-> 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)
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 :: (f t -> f (f u))
-> Assignment8 f x1 x2 x3 x4 x5 x6 t x8
-> f (Assignment8 f x1 x2 x3 x4 x5 x6 u x8)
_7 = Int
-> 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)
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 :: (f t -> f (f u))
-> Assignment8 f x1 x2 x3 x4 x5 x6 x7 t
-> f (Assignment8 f x1 x2 x3 x4 x5 x6 x7 u)
_8 = Int
-> 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)
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 :: (f t -> f (f u))
-> Assignment9 f t x2 x3 x4 x5 x6 x7 x8 x9
-> f (Assignment9 f u x2 x3 x4 x5 x6 x7 x8 x9)
_1 = Int
-> 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)
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 :: (f t -> f (f u))
-> Assignment9 f x1 t x3 x4 x5 x6 x7 x8 x9
-> f (Assignment9 f x1 u x3 x4 x5 x6 x7 x8 x9)
_2 = Int
-> 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)
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 :: (f t -> f (f u))
-> Assignment9 f x1 x2 t x4 x5 x6 x7 x8 x9
-> f (Assignment9 f x1 x2 u x4 x5 x6 x7 x8 x9)
_3 = Int
-> 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)
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 :: (f t -> f (f u))
-> Assignment9 f x1 x2 x3 t x5 x6 x7 x8 x9
-> f (Assignment9 f x1 x2 x3 u x5 x6 x7 x8 x9)
_4 = Int
-> 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)
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 :: (f t -> f (f u))
-> Assignment9 f x1 x2 x3 x4 t x6 x7 x8 x9
-> f (Assignment9 f x1 x2 x3 x4 u x6 x7 x8 x9)
_5 = Int
-> 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)
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 :: (f t -> f (f u))
-> Assignment9 f x1 x2 x3 x4 x5 t x7 x8 x9
-> f (Assignment9 f x1 x2 x3 x4 x5 u x7 x8 x9)
_6 = Int
-> 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)
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 :: (f t -> f (f u))
-> Assignment9 f x1 x2 x3 x4 x5 x6 t x8 x9
-> f (Assignment9 f x1 x2 x3 x4 x5 x6 u x8 x9)
_7 = Int
-> 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)
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 :: (f t -> f (f u))
-> Assignment9 f x1 x2 x3 x4 x5 x6 x7 t x9
-> f (Assignment9 f x1 x2 x3 x4 x5 x6 x7 u x9)
_8 = Int
-> 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)
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 :: (f t -> f (f u))
-> Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 t
-> f (Assignment9 f x1 x2 x3 x4 x5 x6 x7 x8 u)
_9 = Int
-> 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)
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