packages feed

ral 0.1 → 0.2

raw patch · 13 files changed

+973/−48 lines, 13 filesdep +indexed-traversabledep ~QuickCheckdep ~basedep ~fin

Dependencies added: indexed-traversable

Dependency ranges changed: QuickCheck, base, fin, semigroupoids, semigroups

Files

ChangeLog.md view
@@ -1,5 +1,16 @@ # Version history for ral +## 0.2++- `fin-0.2` support+- Add `indexed-traversable` instances+- Explicitly mark all modules as Safe or Trustworthy.++## 0.1.1++- Add `reverse` and `itraverse_` to `Data.RAVec.Tree`+- Add `Data.RAVec.Tree.DF`+ ## 0.1  - First version. Released on an unsuspecting world.
ral.cabal view
@@ -1,6 +1,6 @@ cabal-version:      2.2 name:               ral-version:            0.1+version:            0.2 synopsis:           Random access lists category:           Data, Dependent Types, Singletons description:@@ -25,7 +25,7 @@ license-file:       LICENSE author:             Oleg Grenrus <oleg.grenrus@iki.fi> maintainer:         Oleg.Grenrus <oleg.grenrus@iki.fi>-copyright:          (c) 2019 Oleg Grenrus+copyright:          (c) 2019-2021 Oleg Grenrus build-type:         Simple extra-source-files: ChangeLog.md tested-with:@@ -35,7 +35,9 @@    || ==8.2.2    || ==8.4.4    || ==8.6.5-   || ==8.8.1+   || ==8.8.4+   || ==8.10.4+   || ==9.0.1  source-repository head   type:     git@@ -72,29 +74,32 @@     Data.RAVec     Data.RAVec.NonEmpty     Data.RAVec.Tree+    Data.RAVec.Tree.DF    other-modules:     Data.RAList.Internal     Data.RAList.NonEmpty.Internal     Data.RAList.Tree.Internal+    TrustworthyCompat    -- GHC boot libs   build-depends:-    , base     >=4.7     && <4.14+    , base     >=4.7     && <4.16     , deepseq  >=1.3.0.1 && <1.5    if !impl(ghc >=8.0)-    build-depends: semigroups >=0.18.4 && <0.20+    build-depends: semigroups >=0.18.5 && <0.20    -- siblings   build-depends:     , bin  ^>=0.1-    , fin  ^>=0.1.1+    , fin  ^>=0.2    -- other dependencies   build-depends:-    , hashable    >=1.2.7.0 && <1.4-    , QuickCheck  ^>=2.13.2+    , hashable             >=1.2.7.0 && <1.4+    , indexed-traversable  ^>=0.1.1+    , QuickCheck           ^>=2.14.2    if flag(distributive)     build-depends: distributive >=0.5.3 && <0.7@@ -103,7 +108,12 @@       build-depends: adjunctions ^>=4.4    if flag(semigroupoids)-    build-depends: semigroupoids >=5.2.2 && <5.4+    build-depends: semigroupoids ^>=5.3.5++  if impl(ghc >=9.0)+    -- these flags may abort compilation with GHC-8.10+    -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3295+    ghc-options: -Winferred-safe-imports -Wmissing-safe-haskell-mode  -- dump-core -- if impl(ghc >= 8.0)
src/Data/RAList.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE Safe #-} -- | Random access list. -- -- This module is designed to imported qualifed.@@ -29,8 +30,8 @@     itraverse,     ) where -import Prelude (Maybe (..)) import Data.RAList.Internal+import Prelude              (Maybe (..))  import qualified Data.RAList.NonEmpty as NE
src/Data/RAList/Internal.hs view
@@ -1,11 +1,13 @@-{-# LANGUAGE CPP                 #-}-{-# LANGUAGE DeriveFoldable      #-}-{-# LANGUAGE DeriveFunctor       #-}-{-# LANGUAGE DeriveTraversable   #-}-{-# LANGUAGE FlexibleContexts    #-}-{-# LANGUAGE InstanceSigs        #-}-{-# LANGUAGE KindSignatures      #-}-{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE CPP                   #-}+{-# LANGUAGE DeriveFoldable        #-}+{-# LANGUAGE DeriveFunctor         #-}+{-# LANGUAGE DeriveTraversable     #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE InstanceSigs          #-}+{-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Safe                  #-}+{-# LANGUAGE ScopedTypeVariables   #-} module Data.RAList.Internal (     RAList (..),     -- * Showing@@ -48,6 +50,10 @@ import qualified Data.Traversable as I (Traversable (..)) import qualified Test.QuickCheck  as QC +import qualified Data.Foldable.WithIndex    as WI (FoldableWithIndex (..))+import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))+import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))+ import qualified Data.RAList.NonEmpty.Internal as NE  -- $setup@@ -109,6 +115,19 @@ #ifdef MIN_VERSION_semigroupoids -- Apply, Bind #endif++-- | @since 0.2+instance WI.FunctorWithIndex Int RAList where+    imap = imap++-- | @since 0.2+instance WI.FoldableWithIndex Int RAList where+    ifoldMap = ifoldMap+    -- ifoldr   = ifoldr -- TODO, PR welcome!++-- | @since 0.2+instance WI.TraversableWithIndex Int RAList where+    itraverse = itraverse  ------------------------------------------------------------------------------- -- Showing
src/Data/RAList/NonEmpty.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE CPP #-}+{-# LANGUAGE CPP  #-}+{-# LANGUAGE Safe #-} -- | Non-empty random access list. -- -- This module is designed to imported qualifed.@@ -40,11 +41,11 @@ #endif     ) where -import Prelude (snd) import Data.RAList.NonEmpty.Internal+import Prelude                       (snd) -import Data.RAList.Tree (Leaf (..), Node (..)) import Data.RAList.Internal (RAList (..))+import Data.RAList.Tree     (Leaf (..), Node (..))  -- $setup -- >>> import Prelude (($))@@ -62,17 +63,17 @@ tail :: NERAList a -> RAList a tail r = snd (uncons r) --- | +-- | -- >>> uncons $ fromNonEmpty $ 'a' :| "bcdef" -- ('a',fromList "bcdef") uncons :: NERAList a -> (a, RAList a) uncons (NE (Last  (Lf x)))   = (x, Empty) uncons (NE (Cons1 (Lf x) r)) = (x, NonEmpty (NE (Cons0 r)))-uncons (NE (Cons0        r)) = +uncons (NE (Cons0        r)) =     let (Lf x, r') = unconsTree r in (x, NonEmpty (NE r'))  unconsTree :: NERAList' (Node t) a -> (t a, NERAList' t a) unconsTree (Last  (Nd x y))   = (x, Last y) unconsTree (Cons1 (Nd x y) r) = (x, Cons1 y (Cons0 r))-unconsTree (Cons0          r) = +unconsTree (Cons0          r) =     let (Nd x y, r') = unconsTree r in (x, Cons1 y r')
src/Data/RAList/NonEmpty/Internal.hs view
@@ -1,12 +1,14 @@-{-# LANGUAGE BangPatterns        #-}-{-# LANGUAGE CPP                 #-}-{-# LANGUAGE DeriveFoldable      #-}-{-# LANGUAGE DeriveFunctor       #-}-{-# LANGUAGE DeriveTraversable   #-}-{-# LANGUAGE FlexibleContexts    #-}-{-# LANGUAGE InstanceSigs        #-}-{-# LANGUAGE KindSignatures      #-}-{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE BangPatterns          #-}+{-# LANGUAGE CPP                   #-}+{-# LANGUAGE DeriveFoldable        #-}+{-# LANGUAGE DeriveFunctor         #-}+{-# LANGUAGE DeriveTraversable     #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE InstanceSigs          #-}+{-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Safe                  #-}+{-# LANGUAGE ScopedTypeVariables   #-} module Data.RAList.NonEmpty.Internal (     NERAList (..),     NERAList' (..),@@ -61,6 +63,10 @@ import qualified Data.Traversable   as I (Traversable (..)) import qualified Test.QuickCheck    as QC +import qualified Data.Foldable.WithIndex    as WI (FoldableWithIndex (..))+import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))+import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))+ #ifdef MIN_VERSION_semigroupoids import Data.Functor.Apply (Apply (..)) @@ -165,6 +171,19 @@ #ifdef MIN_VERSION_semigroupoids -- Apply, Bind #endif++-- | @since 0.2+instance WI.FunctorWithIndex Int NERAList where+    imap = imap++-- | @since 0.2+instance WI.FoldableWithIndex Int NERAList where+    ifoldMap = ifoldMap+    -- ifoldr   = ifoldr -- TODO, PR welcome!++-- | @since 0.2+instance WI.TraversableWithIndex Int NERAList where+    itraverse = itraverse  ------------------------------------------------------------------------------- -- Showing
src/Data/RAList/Tree.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE Safe #-} module Data.RAList.Tree (     Leaf (..),     Node (..),
src/Data/RAList/Tree/Internal.hs view
@@ -4,6 +4,7 @@ {-# LANGUAGE DeriveFunctor     #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleContexts  #-}+{-# LANGUAGE Safe              #-} {-# LANGUAGE TypeFamilies      #-} module Data.RAList.Tree.Internal (     Leaf (..),
src/Data/RAVec.hs view
@@ -7,6 +7,7 @@ {-# LANGUAGE GADTs                 #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE Safe                  #-} {-# LANGUAGE ScopedTypeVariables   #-} {-# LANGUAGE StandaloneDeriving    #-} {-# LANGUAGE TypeFamilies          #-}@@ -30,6 +31,7 @@     toList,     toNonEmpty,     fromList,+    reifyList,     reifyNonEmpty,      -- * Indexing@@ -44,6 +46,9 @@     foldr,     ifoldr, +    -- * Special folds+    null,+     -- * Mapping     map,     imap,@@ -68,7 +73,8 @@     )  where  import Prelude-       (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Ord (..), Show, ($), (.))+       (Bool (..), Eq (..), Functor (..), Int, Maybe (..), Ord (..), Show, ($),+       (.))  import Control.Applicative (Applicative (..), (<$>)) import Control.DeepSeq     (NFData (..))@@ -79,7 +85,6 @@ import Data.Monoid         (Monoid (..)) import Data.Semigroup      (Semigroup (..)) import Data.Type.Bin       (SBin (..), SBinI (..), SBinPI (..))-import Data.Type.Equality  ((:~:) (..)) import Data.Typeable       (Typeable)  import qualified Data.RAVec.NonEmpty as NE@@ -89,6 +94,10 @@ import qualified Data.Traversable as I (Traversable (..)) import qualified Test.QuickCheck  as QC +import qualified Data.Foldable.WithIndex    as WI (FoldableWithIndex (..))+import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))+import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))+ #ifdef MIN_VERSION_distributive import qualified Data.Distributive as I (Distributive (..)) @@ -105,15 +114,18 @@ #endif  import Data.RAVec.NonEmpty (NERAVec (..))+import TrustworthyCompat  -- $setup -- >>> :set -XScopedTypeVariables -XDataKinds--- >>> import Prelude (print, Char, Bounded (..))+-- >>> import Prelude (print, Char, Bounded (..), Maybe (..), (.), ($), Eq (..)) -- >>> import Data.List (sort) -- >>> import Data.Wrd (Wrd (..))--- >>> import Data.Bin.Pos (top, pop)+-- >>> import Data.Bin.Pos (Pos (..), top, pop) -- >>> import Data.BinP.PosP (PosP (..), PosP' (..))+-- >>> import Data.List.NonEmpty (NonEmpty (..)) -- >>> import qualified Data.Bin.Pos as P+-- >>> import qualified Data.Type.Bin as B  ------------------------------------------------------------------------------- -- Random access vec@@ -149,6 +161,19 @@ instance I.Traversable (RAVec b) where     traverse = traverse +-- | @since 0.2+instance WI.FunctorWithIndex (Pos n) (RAVec n) where+    imap = imap++-- | @since 0.2+instance WI.FoldableWithIndex (Pos n) (RAVec n) where+    ifoldMap = ifoldMap+    ifoldr   = ifoldr++-- | @since 0.2+instance WI.TraversableWithIndex (Pos n) (RAVec n) where+    itraverse = itraverse+ #ifdef MIN_VERSION_semigroupoids instance b ~ 'BP n => I.Foldable1 (RAVec b) where     foldMap1   = foldMap1@@ -457,5 +482,5 @@  instance (B.SBinI b, QC.Function a) => QC.Function (RAVec b a) where     function = case B.sbin :: B.SBin b of-        SBZ -> QC.functionMap (\Empty -> ())       (\() -> Empty) +        SBZ -> QC.functionMap (\Empty -> ())       (\() -> Empty)         SBP -> QC.functionMap (\(NonEmpty r) -> r) NonEmpty
src/Data/RAVec/NonEmpty.hs view
@@ -6,6 +6,7 @@ {-# LANGUAGE GADTs                 #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE Safe                  #-} {-# LANGUAGE ScopedTypeVariables   #-} {-# LANGUAGE StandaloneDeriving    #-} {-# LANGUAGE TypeFamilies          #-}@@ -67,13 +68,14 @@     liftShrink, liftShrink',     ) where -import Prelude (Bool (..), uncurry, Int, Eq (..), Functor (..), Ord (..), Show, seq, ($), (.))+import Prelude+       (Bool (..), Eq (..), Functor (..), Int, Ord (..), Show, seq, uncurry,+       ($), (.))  import Control.Applicative (Applicative (..), (<$>)) import Control.DeepSeq     (NFData (..)) import Data.Bin            (BinP (..)) import Data.BinP.PosP      (PosP (..), PosP' (..))-import Data.Coerce         (coerce) import Data.Hashable       (Hashable (..)) import Data.List.NonEmpty  (NonEmpty (..)) import Data.Monoid         (Monoid (..))@@ -91,6 +93,10 @@ import qualified Data.Traversable as I (Traversable (..)) import qualified Test.QuickCheck  as QC +import qualified Data.Foldable.WithIndex    as WI (FoldableWithIndex (..))+import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))+import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))+ #ifdef MIN_VERSION_distributive import qualified Data.Distributive as I (Distributive (..)) @@ -106,7 +112,8 @@ import qualified Data.Semigroup.Traversable as I (Traversable1 (..)) #endif -import Data.RAVec.Tree (Tree (..))+import Data.RAVec.Tree   (Tree (..))+import TrustworthyCompat  -- $setup -- >>> :set -XScopedTypeVariables -XDataKinds@@ -168,6 +175,32 @@  instance I.Traversable (NERAVec' n b) where     traverse = traverse'++-- | @since 0.2+instance WI.FunctorWithIndex (PosP n) (NERAVec n) where+    imap = imap++-- | @since 0.2+instance WI.FoldableWithIndex (PosP n) (NERAVec n) where+    ifoldMap = ifoldMap+    ifoldr   = ifoldr++-- | @since 0.2+instance WI.TraversableWithIndex (PosP n) (NERAVec n) where+    itraverse = itraverse++-- | @since 0.2+instance WI.FunctorWithIndex (PosP' n m) (NERAVec' n m) where+    imap = imap'++-- | @since 0.2+instance WI.FoldableWithIndex (PosP' n m) (NERAVec' n m) where+    ifoldMap = ifoldMap'+    ifoldr   = ifoldr'++-- | @since 0.2+instance WI.TraversableWithIndex (PosP' n m) (NERAVec' n m) where+    itraverse = itraverse'  #ifdef MIN_VERSION_semigroupoids instance I.Foldable1 (NERAVec b) where
src/Data/RAVec/Tree.hs view
@@ -6,6 +6,7 @@ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs                  #-} {-# LANGUAGE RankNTypes             #-}+{-# LANGUAGE Safe                   #-} {-# LANGUAGE ScopedTypeVariables    #-} {-# LANGUAGE StandaloneDeriving     #-} {-# LANGUAGE TypeFamilies           #-}@@ -18,6 +19,7 @@      -- * Conversions     toList,+    reverse,      -- * Indexing     (!),@@ -36,7 +38,12 @@     ifoldr1Map,     foldl,     ifoldl,++    -- * Special folds     length,+    null,+    sum,+    product,      -- * Mapping     map,@@ -47,7 +54,7 @@     traverse1,     itraverse1, #endif-    -- TODO: itraverse_,+    itraverse_,      -- * Zipping     zipWith,@@ -60,15 +67,15 @@     -- * QuickCheck     liftArbitrary,     liftShrink,-     ) where  import Prelude-       (Bool (..), Eq (..), Functor (..), Int, Ord (..), Show, id, seq,-       uncurry, ($), (*), (.))+       (Bool (..), Eq (..), Functor (..), Int, Num, Ord (..), Show, id, seq,+       uncurry, ($), (*), (+), (.))  import Control.Applicative (Applicative (..), (<$>)) import Control.DeepSeq     (NFData (..))+import Control.Monad       (void) import Data.Hashable       (Hashable (..)) import Data.Monoid         (Monoid (..)) import Data.Nat            (Nat (..))@@ -83,6 +90,10 @@ import qualified Data.Traversable as I (Traversable (..)) import qualified Test.QuickCheck  as QC +import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))+import qualified Data.Foldable.WithIndex    as WI (FoldableWithIndex (..))+import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))+ #ifdef MIN_VERSION_distributive import qualified Data.Distributive as I (Distributive (..)) @@ -101,7 +112,9 @@ -- $setup -- >>> :set -XScopedTypeVariables -- >>> import Data.Proxy (Proxy (..))--- >>> import Prelude (Char, not, uncurry, flip)+-- >>> import Prelude (Char, not, uncurry, flip, ($), Bool (..))+-- >>> import Data.Wrd (Wrd (..))+-- >>> import qualified Data.Type.Nat as N  ------------------------------------------------------------------------------- -- Data@@ -139,7 +152,7 @@     foldr   = foldr     foldl   = foldl #if MIN_VERSION_base(4,8,0)-    null _ = False+    null   = null     toList = toList     length = length #endif@@ -147,6 +160,19 @@ instance I.Traversable (Tree n) where     traverse = traverse +-- | @since 0.2+instance WI.FunctorWithIndex (Wrd n) (Tree n) where+    imap = imap++-- | @since 0.2+instance WI.FoldableWithIndex (Wrd n) (Tree n) where+    ifoldMap = ifoldMap+    ifoldr   = ifoldr++-- | @since 0.2+instance WI.TraversableWithIndex (Wrd n) (Tree n) where+    itraverse = itraverse+ #ifdef MIN_VERSION_semigroupoids instance I.Foldable1 (Tree n) where     foldMap1 = foldMap1@@ -175,6 +201,8 @@     liftA2 = zipWith #endif +-- TODO: Monad+ #ifdef MIN_VERSION_distributive instance N.SNatI n => I.Distributive (Tree n) where     distribute f = tabulate (\k -> fmap (! k) f)@@ -249,6 +277,21 @@ rightmost (Node _ y) = rightmost y  -------------------------------------------------------------------------------+-- Reverse+-------------------------------------------------------------------------------++-- | Reverse 'Tree'.+--+-- >>> let t = Node (Node (Leaf 'a') (Leaf 'b')) (Node (Leaf 'c') (Leaf 'd'))+-- >>> reverse t+-- Node (Node (Leaf 'd') (Leaf 'c')) (Node (Leaf 'b') (Leaf 'a'))+--+-- @since 0.1.1+reverse :: Tree n a -> Tree n a+reverse t@(Leaf _) = t+reverse (Node x y) = Node (reverse y) (reverse x)++------------------------------------------------------------------------------- -- Folds ------------------------------------------------------------------------------- @@ -296,8 +339,14 @@ ifoldl f z (Leaf x)   = f WE z x ifoldl f z (Node x y) = ifoldl (goLeft f) (ifoldl (goRight f) z x) y --- TODO: foldl+-------------------------------------------------------------------------------+-- Special folds+------------------------------------------------------------------------------- +-- | @since 0.1.1+null :: Tree n a -> Bool+null _ = False+ -- | >>> length (universe :: Tree N.Nat3 (Wrd N.Nat3)) -- 8 --@@ -307,6 +356,20 @@     go !acc (Leaf _)   = acc     go  acc (Node x _) = go (2 * acc) x +-- | Non-strict 'sum'.+--+-- @since 0.1.1+sum :: Num a => Tree n a -> a+sum (Leaf a)   = a+sum (Node x y) = sum x + sum y++-- | Non-strict 'product'.+--+-- @since 0.1.1+product :: Num a => Tree n a -> a+product (Leaf a)   = a+product (Node x y) = product x * product y+ ------------------------------------------------------------------------------- -- Mapping -------------------------------------------------------------------------------@@ -340,6 +403,12 @@ itraverse1 f (Leaf x)   = Leaf <$> f WE x itraverse1 f (Node x y) = Node <$> itraverse1 (goLeft f) x <.> itraverse1 (goRight f) y #endif++-- |+-- @since 0.1.1+itraverse_ :: forall n f a b. Applicative f => (Wrd n -> a -> f b) -> Tree n a -> f ()+itraverse_ f (Leaf x)   = void (f WE x)+itraverse_ f (Node x y) = itraverse_ (f . W0) x *> itraverse_ (f . W1) y  ------------------------------------------------------------------------------- -- Zipping
+ src/Data/RAVec/Tree/DF.hs view
@@ -0,0 +1,726 @@+{-# LANGUAGE CPP                    #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE DeriveDataTypeable     #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs                  #-}+{-# LANGUAGE RankNTypes             #-}+{-# LANGUAGE Safe                   #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeFamilies           #-}+-- | Depth indexed perfect tree as data family.+module Data.RAVec.Tree.DF (+    Tree (..),++    -- * Construction+    singleton,++    -- * Conversions+    toList,+    reverse,++    -- * Indexing+    (!),+    tabulate,+    leftmost,+    rightmost,++    -- * Folds+    foldMap,+    foldMap1,+    ifoldMap,+    ifoldMap1,+    foldr,+    ifoldr,+    foldr1Map,+    ifoldr1Map,+    foldl,+    ifoldl,++    -- * Special folds+    length,+    null,+    sum,+    product,++    -- * Mapping+    map,+    imap,+    traverse,+    itraverse,+#ifdef MIN_VERSION_semigroupoids+    traverse1,+    itraverse1,+#endif+    itraverse_,++    -- * Zipping+    zipWith,+    izipWith,+    repeat,++    -- * Universe+    universe,++    -- * QuickCheck+    liftArbitrary,+    liftShrink,++    -- * Ensure spine+    ensureSpine,+) where++import Prelude+       (Bool (..), Eq (..), Functor (..), Int, Num, Ord (..), Ordering (..),+       Show (..), ShowS, flip, id, seq, showChar, showParen, showString,+       uncurry, ($), (&&), (*), (+), (.))++import Control.Applicative (Applicative (..), liftA2, (<$>))+import Control.DeepSeq     (NFData (..))+import Control.Monad       (void)+import Data.Hashable       (Hashable (..))+import Data.Monoid         (Monoid (..))+import Data.Nat            (Nat (..))+import Data.Semigroup      (Semigroup (..))+import Data.Wrd            (Wrd (..))++import qualified Data.Type.Nat as N++-- instances+import qualified Data.Foldable    as I (Foldable (..))+import qualified Data.Traversable as I (Traversable (..))+import qualified Test.QuickCheck  as QC++import qualified Data.Foldable.WithIndex    as WI (FoldableWithIndex (..))+import qualified Data.Functor.WithIndex     as WI (FunctorWithIndex (..))+import qualified Data.Traversable.WithIndex as WI (TraversableWithIndex (..))++#ifdef MIN_VERSION_distributive+import qualified Data.Distributive as I (Distributive (..))++#ifdef MIN_VERSION_adjunctions+import qualified Data.Functor.Rep as I (Representable (..))+#endif+#endif++#ifdef MIN_VERSION_semigroupoids+import Data.Functor.Apply (Apply (..))++import qualified Data.Semigroup.Foldable    as I (Foldable1 (..))+import qualified Data.Semigroup.Traversable as I (Traversable1 (..))+#endif++-- $setup+-- >>> :set -XScopedTypeVariables+-- >>> import Data.Proxy (Proxy (..))+-- >>> import Prelude (Char, not, uncurry, flip, error, ($), Bool (..), id)+-- >>> import Data.Wrd (Wrd (..))+-- >>> import qualified Data.Type.Nat as N++-------------------------------------------------------------------------------+-- Types+-------------------------------------------------------------------------------++data family Tree (n :: Nat) a++newtype instance Tree 'Z     a = Leaf a+data instance    Tree ('S n) a = Node (Tree n a) (Tree n a)++-------------------------------------------------------------------------------+-- Instances+-------------------------------------------------------------------------------++instance (Eq a, N.SNatI n) => Eq (Tree n a) where+    (==) = getEqual (N.induction1 start step) where+        start :: Equal 'Z a+        start = Equal $ \(Leaf x) (Leaf y) -> x == y++        step :: Equal m a -> Equal ('S m) a+        step (Equal go) = Equal $ \(Node x1 y1) (Node x2 y2) ->+            go x1 x2 && go y1 y2++newtype Equal n a = Equal { getEqual :: Tree n a -> Tree n a -> Bool }++instance (Ord a, N.SNatI n) => Ord (Tree n a) where+    compare = getCompare (N.induction1 start step) where+        start :: Compare 'Z a+        start = Compare $ \(Leaf x) (Leaf y) -> compare x y++        step :: Compare m a -> Compare ('S m) a+        step (Compare go) = Compare $ \(Node x1 y1) (Node x2 y2) ->+            go x1 x2 <> go y1 y2++newtype Compare n a = Compare { getCompare :: Tree n a -> Tree n a -> Ordering }++instance (Show a, N.SNatI n) => Show (Tree n a) where+    showsPrec = getShowsPrec (N.induction1 start step) where+        start :: ShowsPrec 'Z a+        start = ShowsPrec $ \d (Leaf x) -> showParen (d > 10)+            $ showString "Leaf "+            . showsPrec 11 x++        step :: ShowsPrec m a -> ShowsPrec ('S m) a+        step (ShowsPrec go) = ShowsPrec $ \d (Node x y) -> showParen (d > 10)+            $ showString "Node "+            . go 11 x+            . showChar ' '+            . go 11 y++newtype ShowsPrec n a = ShowsPrec { getShowsPrec :: Int -> Tree n a -> ShowS }++instance N.SNatI n => Functor (Tree n) where+    fmap = map++instance N.SNatI n => I.Foldable (Tree n) where+    foldMap = foldMap++    foldr  = foldr+    -- foldl' = foldl'++#if MIN_VERSION_base(4,8,0)+    null    = null+    length  = length+    sum     = sum+    product = product+#endif++#ifdef MIN_VERSION_semigroupoids+instance (N.SNatI n) => I.Foldable1 (Tree n) where+    foldMap1 = foldMap1++instance (N.SNatI n) => I.Traversable1 (Tree n) where+    traverse1 = traverse1+#endif++instance N.SNatI n => I.Traversable (Tree n) where+    traverse = traverse++-- | @since 0.2+instance N.SNatI n => WI.FunctorWithIndex (Wrd n) (Tree n) where+    imap = imap++-- | @since 0.2+instance N.SNatI n => WI.FoldableWithIndex (Wrd n) (Tree n) where+    ifoldMap = ifoldMap+    ifoldr   = ifoldr++-- | @since 0.2+instance N.SNatI n => WI.TraversableWithIndex (Wrd n) (Tree n) where+    itraverse = itraverse++instance (NFData a, N.SNatI n) => NFData (Tree n a) where+    rnf = getRnf (N.induction1 z s) where+        z           = Rnf $ \(Leaf x)   -> rnf x+        s (Rnf rec) = Rnf $ \(Node x y) -> rec x `seq` rec y++newtype Rnf n a = Rnf { getRnf :: Tree n a -> () }++instance (Hashable a, N.SNatI n) => Hashable (Tree n a) where+    hashWithSalt = getHashWithSalt (N.induction1 z s) where+        z = HashWithSalt $ \salt (Leaf x) -> salt `hashWithSalt` x+        s (HashWithSalt rec) = HashWithSalt $ \salt (Node x y) -> rec (rec salt x) y++newtype HashWithSalt n a = HashWithSalt { getHashWithSalt :: Int -> Tree n a -> Int }++instance N.SNatI n => Applicative (Tree n) where+    pure = repeat+    (<*>)  = zipWith ($)+    _ *> x = x+    x <* _ = x+#if MIN_VERSION_base(4,10,0)+    liftA2 = zipWith+#endif++-- TODO: Monad++#ifdef MIN_VERSION_distributive+instance N.SNatI n => I.Distributive (Tree n) where+    distribute f = tabulate (\k -> fmap (! k) f)++#ifdef MIN_VERSION_adjunctions+instance N.SNatI n => I.Representable (Tree n) where+    type Rep (Tree n) = Wrd n+    tabulate = tabulate+    index    = (!)+#endif+#endif++instance (Semigroup a, N.SNatI n) => Semigroup (Tree n a) where+    (<>) = zipWith (<>)++instance (Monoid a, N.SNatI n) => Monoid (Tree n a) where+    mempty = pure mempty+    mappend = zipWith mappend++#ifdef MIN_VERSION_semigroupoids+instance N.SNatI n => Apply (Tree n) where+    (<.>) = zipWith ($)+    _ .> x = x+    x <. _ = x+    liftF2 = zipWith++-- TODO: Bind+#endif++-------------------------------------------------------------------------------+-- Construction+-------------------------------------------------------------------------------++-- | 'Tree' with exactly one element.+--+-- >>> singleton True+-- Leaf True+--+singleton :: a -> Tree 'Z a+singleton = Leaf++-------------------------------------------------------------------------------+-- Conversions+-------------------------------------------------------------------------------++-- | Convert 'Tree' to list.+--+-- >>> toList $ Node (Node (Leaf 'f') (Leaf 'o')) (Node (Leaf 'o') (Leaf 'd'))+-- "food"+toList :: forall n a. N.SNatI n => Tree n a -> [a]+toList xs = getToList (N.induction1 start step) xs [] where+    start :: ToList 'Z a+    start = ToList (\(Leaf x) -> (x :))++    step :: ToList m a -> ToList ('S m) a+    step (ToList f) = ToList $ \(Node x y) -> f x . f y++newtype ToList n a = ToList { getToList :: Tree n a -> [a] -> [a] }++-------------------------------------------------------------------------------+-- Indexing+-------------------------------------------------------------------------------++flipIndex :: N.SNatI n => Wrd n -> Tree n a -> a+flipIndex = getIndex (N.induction1 start step) where+    start :: Index 'Z a+    start = Index $ \_ (Leaf x) -> x++    step :: Index m a-> Index ('N.S m) a+    step (Index go) = Index $ \i (Node x y) -> case i of+        W0 j -> go j x+        W1 j -> go j y++newtype Index n a = Index { getIndex :: Wrd n -> Tree n a -> a }++-- | Indexing.+--+-- >>> let t = Node (Node (Leaf 'a') (Leaf 'b')) (Node (Leaf 'c') (Leaf 'd'))+-- >>> t ! W1 (W0 WE)+-- 'c'+--+(!) :: N.SNatI n => Tree n a -> Wrd n -> a+(!) = flip flipIndex++-- | Tabulating, inverse of '!'.+--+-- >>> tabulate id :: Tree N.Nat2 (Wrd N.Nat2)+-- Node (Node (Leaf 0b00) (Leaf 0b01)) (Node (Leaf 0b10) (Leaf 0b11))+tabulate :: N.SNatI n => (Wrd n -> a) -> Tree n a+tabulate = getTabulate (N.induction1 start step) where+    start :: Tabulate 'Z a+    start = Tabulate $ \f -> Leaf (f WE)++    step :: Tabulate m a -> Tabulate ('S m) a+    step (Tabulate go) = Tabulate $ \f -> Node (go (f . W0)) (go (f . W1))++newtype Tabulate n a = Tabulate { getTabulate :: (Wrd n -> a) -> Tree n a }++leftmost :: N.SNatI n => Tree n a -> a+leftmost = getTheMost (N.induction1 start step) where+    start :: TheMost 'Z a+    start = TheMost $ \(Leaf x) -> x++    step :: TheMost m a -> TheMost ('S m) a+    step (TheMost go) = TheMost $ \(Node x _) -> go x++rightmost :: N.SNatI n => Tree n a -> a+rightmost = getTheMost (N.induction1 start step) where+    start :: TheMost 'Z a+    start = TheMost $ \(Leaf x) -> x++    step :: TheMost m a -> TheMost ('S m) a+    step (TheMost go) = TheMost $ \(Node _ y) -> go y++newtype TheMost n a = TheMost { getTheMost :: Tree n a -> a }++-------------------------------------------------------------------------------+-- Reverse+-------------------------------------------------------------------------------++-- | Reverse 'Tree'.+--+-- >>> let t = Node (Node (Leaf 'a') (Leaf 'b')) (Node (Leaf 'c') (Leaf 'd'))+-- >>> reverse t+-- Node (Node (Leaf 'd') (Leaf 'c')) (Node (Leaf 'b') (Leaf 'a'))+--+reverse :: forall n a. N.SNatI n => Tree n a -> Tree n a+reverse = getReverse (N.induction1 start step) where+    start :: Reverse 'Z a+    start = Reverse id++    step :: N.SNatI m => Reverse m a -> Reverse ('S m) a+    step (Reverse go) = Reverse $ \(Node x y) -> Node (go y) (go x)++newtype Reverse n a = Reverse { getReverse :: Tree n a -> Tree n a }++-------------------------------------------------------------------------------+-- Mapping+-------------------------------------------------------------------------------++-- | >>> map not $ Node (Leaf True) (Leaf False)+-- Node (Leaf False) (Leaf True)+--+map :: forall a b n. N.SNatI n => (a -> b) -> Tree n a -> Tree n b+map f = getMap $ N.induction1 start step where+    start :: Map a 'Z b+    start = Map $ \(Leaf x) -> Leaf (f x)++    step :: Map a m b -> Map a ('S m) b+    step (Map go) = Map $ \(Node x y) -> Node (go x) (go y)++newtype Map a n b = Map { getMap :: Tree n a -> Tree n b }++-- |+-- >>> let t = Node (Node (Leaf 'a') (Leaf 'b')) (Node (Leaf 'c') (Leaf 'd'))+-- >>> imap (,) t+-- Node (Node (Leaf (0b00,'a')) (Leaf (0b01,'b'))) (Node (Leaf (0b10,'c')) (Leaf (0b11,'d')))+--+imap :: N.SNatI n => (Wrd n -> a -> b) -> Tree n a -> Tree n b+imap = getIMap $ N.induction1 start step where+    start :: IMap a 'Z b+    start = IMap $ \f (Leaf x) -> Leaf (f WE x)++    step :: IMap a m b -> IMap a ('S m) b+    step (IMap go) = IMap $ \f (Node x y) ->+        Node (go (f . W0) x) (go (f . W1) y)++newtype IMap a n b = IMap { getIMap :: (Wrd n -> a -> b) -> Tree n a -> Tree n b }++-- | Apply an action to every element of a 'Tree', yielding a 'Tree' of results.+traverse :: forall n f a b. (Applicative f, N.SNatI n) => (a -> f b) -> Tree n a -> f (Tree n b)+traverse f =  getTraverse $ N.induction1 start step where+    start :: Traverse f a 'Z b+    start = Traverse $ \(Leaf x) -> Leaf <$> f x++    step :: Traverse f a m b -> Traverse f a ('S m) b+    step (Traverse go) = Traverse $ \(Node x y) -> liftA2 Node (go x) (go y)+{-# INLINE traverse #-}++newtype Traverse f a n b = Traverse { getTraverse :: Tree n a -> f (Tree n b) }++-- | Apply an action to every element of a 'Tree' and its index, yielding a 'Tree' of results.+itraverse :: forall n f a b. (Applicative f, N.SNatI n) => (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)+itraverse = getITraverse $ N.induction1 start step where+    start :: ITraverse f a 'Z b+    start = ITraverse $ \f (Leaf x) -> Leaf <$> f WE x++    step :: ITraverse f a m b -> ITraverse f a ('S m) b+    step (ITraverse go) = ITraverse $ \f (Node x y) -> liftA2 Node (go (f . W0) x) (go (f . W1) y)+{-# INLINE itraverse #-}++newtype ITraverse f a n b = ITraverse { getITraverse :: (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b) }++#ifdef MIN_VERSION_semigroupoids+-- | Apply an action to non-empty 'Tree', yielding a 'Tree' of results.+traverse1 :: forall n f a b. (Apply f, N.SNatI n) => (a -> f b) -> Tree n a -> f (Tree n b)+traverse1 f = getTraverse $ N.induction1 start step where+    start :: Traverse f a 'Z b+    start = Traverse $ \(Leaf x) -> Leaf <$> f x++    step :: Traverse f a m b -> Traverse f a ('S m) b+    step (Traverse go) = Traverse $ \(Node x y) -> liftF2 Node (go x) (go y)+{-# INLINE traverse1 #-}++itraverse1 :: forall n f a b. (Apply f, N.SNatI n) => (Wrd n -> a -> f b) -> Tree n a -> f (Tree n b)+itraverse1 = getITraverse $ N.induction1 start step where+    start :: ITraverse f a 'Z b+    start = ITraverse $ \f (Leaf x) -> Leaf <$> f WE x++    step :: ITraverse f a m b -> ITraverse f a ('S m) b+    step (ITraverse go) = ITraverse $ \f (Node x y) -> liftF2 Node (go (f . W0) x) (go (f . W1) y)+{-# INLINE itraverse1 #-}+#endif++-- | Apply an action to every element of a 'Tree' and its index, ignoring the results.+itraverse_ :: forall n f a b. (Applicative f, N.SNatI n) => (Wrd n -> a -> f b) -> Tree n a -> f ()+itraverse_ = getITraverse_ $ N.induction1 start step where+    start :: ITraverse_ f a 'Z b+    start = ITraverse_ $ \f (Leaf x) -> void (f WE x)++    step :: ITraverse_ f a m b -> ITraverse_ f a ('S m) b+    step (ITraverse_ go) = ITraverse_ $ \f (Node x y) -> go (f . W0) x *> go (f . W1) y++newtype ITraverse_ f a n b = ITraverse_ { getITraverse_ :: (Wrd n -> a -> f b) -> Tree n a -> f () }++-------------------------------------------------------------------------------+-- Folding+-------------------------------------------------------------------------------++-- | See 'I.Foldable'.+foldMap :: forall a n m. (Monoid m, N.SNatI n) => (a -> m) -> Tree n a -> m+foldMap f = getFold (N.induction1 start step) where+    start :: Fold a 'Z m+    start = Fold $ \(Leaf x) -> f x++    step :: Fold a p m -> Fold a ('S p) m+    step (Fold g) = Fold $ \(Node x y) -> g x `mappend` g y++newtype Fold a n b = Fold  { getFold  :: Tree n a -> b }++-- | See 'I.Foldable1'.+foldMap1 :: forall s a n. (Semigroup s, N.SNatI n) => (a -> s) -> Tree n a -> s+foldMap1 f = getFold $ N.induction1 start step where+    start :: Fold a 'Z s+    start = Fold $ \(Leaf x) -> f x++    step :: Fold a m s -> Fold a ('S m) s+    step (Fold g) = Fold $ \(Node x y) -> g x <> g y++-- | See 'I.FoldableWithIndex'.+ifoldMap :: forall a n m. (Monoid m, N.SNatI n) => (Wrd n -> a -> m) -> Tree n a -> m+ifoldMap = getIFoldMap $ N.induction1 start step where+    start :: IFoldMap a 'Z m+    start = IFoldMap $ \f (Leaf x) -> f WE x++    step :: IFoldMap a p m -> IFoldMap a ('S p) m+    step (IFoldMap go) = IFoldMap $ \f (Node x y) -> go (f . W0) x `mappend` go (f . W1) y++newtype IFoldMap a n m = IFoldMap { getIFoldMap :: (Wrd n -> a -> m) -> Tree n a -> m }++-- | There is no type-class for this :(+ifoldMap1 :: forall a n s. (Semigroup s, N.SNatI n) => (Wrd ('S n) -> a -> s) -> Tree ('S n) a -> s+ifoldMap1 = getIFoldMap $ N.induction1 start step where+    start :: IFoldMap a 'Z m+    start = IFoldMap $ \f (Leaf x) -> f WE x++    step :: IFoldMap a p s -> IFoldMap a ('S p) s+    step (IFoldMap go) = IFoldMap $ \f (Node x y) -> go (f . W0) x <> go (f . W1) y+++++-- | Right fold.+foldr :: forall a b n. N.SNatI n => (a -> b -> b) -> b -> Tree n a -> b+foldr f = getFoldr (N.induction1 start step) where+    start :: Foldr a 'Z b+    start = Foldr $ \z (Leaf x) -> f x z++    step :: Foldr a m b -> Foldr a ('S m) b+    step (Foldr go) = Foldr $ \z (Node x y) -> go (go z y) x++newtype Foldr a n b = Foldr { getFoldr :: b -> Tree n a -> b }++-- | Right fold with an index.+ifoldr :: forall a b n. N.SNatI n => (Wrd n -> a -> b -> b) -> b -> Tree n a -> b+ifoldr = getIFoldr $ N.induction1 start step where+    start :: IFoldr a 'Z b+    start = IFoldr $ \f z (Leaf x) -> f WE x z++    step :: IFoldr a m b -> IFoldr a ('S m) b+    step (IFoldr go) = IFoldr $ \f z (Node x y) -> go (f . W0) (go (f . W1) z y) x++newtype IFoldr a n b = IFoldr { getIFoldr :: (Wrd n -> a -> b -> b) -> b -> Tree n a -> b }++foldr1Map :: forall a b n. N.SNatI n => (a -> b -> b) -> (a -> b) -> Tree n a -> b+foldr1Map f = getFoldr1 (N.induction1 start step) where+    start :: Foldr1 a 'Z b+    start = Foldr1 $ \z (Leaf x) -> z x++    step :: Foldr1 a m b -> Foldr1 a ('S m) b+    step (Foldr1 go) = Foldr1 $ \z (Node x y) -> go (\z0 -> f z0 (go z y)) x++newtype Foldr1 a n b = Foldr1 { getFoldr1 :: (a -> b) -> Tree n a -> b }++ifoldr1Map :: (Wrd n -> a -> b -> b) -> (Wrd n -> a -> b) -> Tree n a -> b+ifoldr1Map = ifoldr1Map++-- | Left fold.+foldl :: forall a b n. N.SNatI n => (b -> a -> b) -> b -> Tree n a -> b+foldl f = getFoldl (N.induction1 start step) where+    start :: Foldl a 'Z b+    start = Foldl $ \z (Leaf x) -> f z x++    step :: Foldl a m b -> Foldl a ('S m) b+    step (Foldl go) = Foldl $ \z (Node x y) -> go (go z x) y++newtype Foldl a n b = Foldl { getFoldl :: b -> Tree n a -> b }++-- | Left fold with an index.+ifoldl :: forall a b n. N.SNatI n => (Wrd n -> b -> a -> b) -> b -> Tree n a -> b+ifoldl = getIFoldl $ N.induction1 start step where+    start :: IFoldl a 'Z b+    start = IFoldl $ \f z (Leaf x) -> f WE z x++    step :: IFoldl a m b -> IFoldl a ('S m) b+    step (IFoldl go) = IFoldl $ \f z (Node x y) -> go (f . W0) (go (f . W1) z x) y++newtype IFoldl a n b = IFoldl { getIFoldl :: (Wrd n -> b -> a -> b) -> b -> Tree n a -> b }++-- | Yield the length of a 'Tree'. /O(n)/+length :: forall n a. N.SNatI n => Tree n a -> Int+length _ = getLength l where+    l :: Length n+    l = N.induction (Length 1) $ \(Length n) -> Length (2 * n)++newtype Length (n :: Nat) = Length { getLength :: Int }++-- | Test whether a 'Tree' is empty. It never is. /O(1)/+null :: Tree n a -> Bool+null _ = False++-------------------------------------------------------------------------------+-- Special folds+-------------------------------------------------------------------------------++-- | Non-strict 'sum'.+sum :: (Num a, N.SNatI n) => Tree n a -> a+sum = getFold $ N.induction1 start step where+    start :: Num a => Fold a 'Z a+    start = Fold $ \(Leaf x) -> x++    step :: Num a => Fold a m a -> Fold a ('S m) a+    step (Fold f) = Fold $ \(Node x y) -> f x + f y++-- | Non-strict 'product'.+product :: (Num a, N.SNatI n) => Tree n a -> a+product = getFold $ N.induction1 start step where+    start :: Num a => Fold a 'Z a+    start = Fold $ \(Leaf x) -> x++    step :: Num a => Fold a m a -> Fold a ('S m) a+    step (Fold f) = Fold $ \(Node x y) -> f x * f y++-------------------------------------------------------------------------------+-- Zipping+-------------------------------------------------------------------------------++-- | Zip two 'Tree's with a function.+zipWith :: forall a b c n. N.SNatI n => (a -> b -> c) -> Tree n a -> Tree n b -> Tree n c+zipWith f = getZipWith $ N.induction start step where+    start :: ZipWith a b c 'Z+    start = ZipWith $ \(Leaf x) (Leaf y) -> Leaf (f x y)++    step :: ZipWith a b c m -> ZipWith a b c ('S m)+    step (ZipWith go) = ZipWith $ \(Node x y) (Node u v) -> Node (go x u) (go y v)++newtype ZipWith a b c n = ZipWith { getZipWith :: Tree n a -> Tree n b -> Tree n c }++-- | Zip two 'Tree's. with a function that also takes the elements' indices.+izipWith :: N.SNatI n => (Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c+izipWith = getIZipWith $ N.induction start step where+    start :: IZipWith a b c 'Z+    start = IZipWith $ \f (Leaf x) (Leaf y) -> Leaf (f WE x y)++    step :: IZipWith a b c m -> IZipWith a b c ('S m)+    step (IZipWith go) = IZipWith $ \f (Node x y) (Node u v) -> Node (go (f . W0) x u) (go (f . W1) y v)++newtype IZipWith a b c n = IZipWith { getIZipWith :: (Wrd n -> a -> b -> c) -> Tree n a -> Tree n b -> Tree n c }++-- | Repeat value+--+-- >>> repeat 'x' :: Tree N.Nat2 Char+-- Node (Node (Leaf 'x') (Leaf 'x')) (Node (Leaf 'x') (Leaf 'x'))+--+repeat :: N.SNatI n => x -> Tree n x+repeat x = N.induction1 (Leaf x) $ \t -> Node t t++-------------------------------------------------------------------------------+-- Monadic+-------------------------------------------------------------------------------++-- TODO++-------------------------------------------------------------------------------+-- universe+-------------------------------------------------------------------------------++-- | Get all @'Wrd' n@ in a @'Tree' n@.+--+-- >>> universe :: Tree N.Nat2 (Wrd N.Nat2)+-- Node (Node (Leaf 0b00) (Leaf 0b01)) (Node (Leaf 0b10) (Leaf 0b11))+universe :: N.SNatI n => Tree n (Wrd n)+universe = tabulate id++-------------------------------------------------------------------------------+-- EnsureSpine+-------------------------------------------------------------------------------++-- | Ensure spine.+--+-- If we have an undefined 'Tree',+--+-- >>> let v = error "err" :: Tree N.Nat2 Char+--+-- And insert data into it later:+--+-- >>> let setHead :: a -> Tree N.Nat2 a -> Tree N.Nat2 a; setHead x (Node (Node _ u) v) = Node (Node (Leaf x) u) v+--+-- Then without a spine, it will fail:+--+-- >>> leftmost $ setHead 'x' v+-- *** Exception: err+-- ...+--+-- But with the spine, it won't:+--+-- >>> leftmost $ setHead 'x' $ ensureSpine v+-- 'x'+--+ensureSpine :: N.SNatI n => Tree n a -> Tree n a+ensureSpine = getEnsureSpine (N.induction1 first step) where+    first :: EnsureSpine 'Z a+    first = EnsureSpine $ \ ~(Leaf x) -> Leaf x++    step :: EnsureSpine m a -> EnsureSpine ('S m) a+    step (EnsureSpine go) = EnsureSpine $ \ ~(Node x y) -> Node (go x) (go y)++newtype EnsureSpine n a = EnsureSpine { getEnsureSpine :: Tree n a -> Tree n a }++-------------------------------------------------------------------------------+-- QuickCheck+-------------------------------------------------------------------------------++instance N.SNatI n => QC.Arbitrary1 (Tree n) where+    liftArbitrary = liftArbitrary+    liftShrink    = liftShrink++liftArbitrary :: forall n a. N.SNatI n => QC.Gen a -> QC.Gen (Tree n a)+liftArbitrary arb = getArb $ N.induction1 start step where+    start :: Arb 'Z a+    start = Arb $ Leaf <$> arb++    step :: Arb m a -> Arb ('S m) a+    step (Arb rec) = Arb $ liftA2 Node rec rec++newtype Arb n a = Arb { getArb :: QC.Gen (Tree n a) }++liftShrink :: forall n a. N.SNatI n => (a -> [a]) -> Tree n a -> [Tree n a]+liftShrink shr = getShr $ N.induction1 start step where+    start :: Shr 'Z a+    start = Shr $ \(Leaf x) ->Leaf <$> shr x++    step :: Shr m a -> Shr ('S m) a+    step (Shr rec) = Shr $ \(Node x y) ->+        uncurry Node <$> QC.liftShrink2 rec rec (x, y)++newtype Shr n a = Shr { getShr :: Tree n a -> [Tree n a] }++instance (N.SNatI n, QC.Arbitrary a) => QC.Arbitrary (Tree n a) where+    arbitrary = QC.arbitrary1+    shrink    = QC.shrink1++instance (N.SNatI n, QC.CoArbitrary a) => QC.CoArbitrary (Tree n a) where+    coarbitrary v = case N.snat :: N.SNat n of+        N.SZ -> QC.variant (0 :: Int) . (case v of (Leaf x) -> QC.coarbitrary x)+        N.SS -> QC.variant (1 :: Int) . (case v of (Node x y) -> QC.coarbitrary (x, y))++instance (N.SNatI n, QC.Function a) => QC.Function (Tree n a) where+    function = case N.snat :: N.SNat n of+        N.SZ -> QC.functionMap (\(Leaf x) -> x) Leaf+        N.SS -> QC.functionMap (\(Node x y) -> (x, y)) (\(x,y) -> Node x y)
+ src/TrustworthyCompat.hs view
@@ -0,0 +1,9 @@+{-# LANGUAGE Trustworthy #-}+module TrustworthyCompat (+    (:~:) (..),+    TestEquality (..),+    coerce,+) where++import Data.Coerce        (coerce)+import Data.Type.Equality (TestEquality (..), (:~:) (..))