fixed-length 0.1.1 → 0.2

raw patch · 3 files changed

+199/−418 lines, 3 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• fixed-length.cabal +3/−10
• src/Data/FixedLength.hs +196/−159
• src/Data/FixedLength/Unary.hs +0/−249

@@ -1,5 +1,5 @@ Name:             fixed-length-Version:          0.1.1+Version:          0.2 License:          BSD3 License-File:     LICENSE Author:           Henning Thielemann <haskell@henning-thielemann.de>@@ -25,7 +25,7 @@ Build-Type:       Simple  Source-Repository this-  Tag:         0.1.1+  Tag:         0.2   Type:        darcs   Location:    http://hub.darcs.net/thielema/fixed-length/ @@ -33,12 +33,9 @@   Type:        darcs   Location:    http://hub.darcs.net/thielema/fixed-length/ -Flag tfp-  Description: use type-level unary numbers from tfp package-  Default: False- Library   Build-Depends:+    tfp >=1.0 && <1.1,     non-empty >=0.2 && <0.4,     utility-ht >=0.0.1 && <0.1,     base >=4 && <5@@ -47,7 +44,3 @@   Hs-Source-Dirs:   src   Exposed-Modules:     Data.FixedLength--  If flag(tfp)-    Other-Modules: Data.FixedLength.Unary-    Build-Depends: tfp >=1.0 && <1.1

@@ -2,19 +2,24 @@ {-# LANGUAGE Rank2Types #-} {-# LANGUAGE EmptyDataDecls #-} module Data.FixedLength (-   C, Position, List, switch,-   Wrap(Wrap, unwrap),-   WrapPos(WrapPos, unwrapPos),-   Zero, Succ(Stop, Succ),-   toList, equal, showsPrec,+   T, Position, List, Length,+   Index, Zero, Succ(Stop, Succ),+   toList, showsPrec,    map, zipWith, sequenceA, repeat,-   index, update, indices, indicesInt, numFromPos,-   N0, N1, N2, N3, N4, N5, N6, N7, N8,+   index, update, indices, indicesInt, numFromIndex,    GE1, GE2, GE3, GE4, GE5, GE6, GE7, GE8,    i0, i1, i2, i3, i4, i5, i6, i7,-   (NonEmpty.!:), end,+   fromFixedList, toFixedList,+   (!:), end, singleton,+   viewL, switchL, head, tail, switchEnd,+   Curried, uncurry,+   minimum, maximum,    ) where +import qualified Type.Data.Num.Unary as Unary+import Type.Data.Num.Unary.Literal (U1)+import Type.Data.Num.Unary (Positive, Natural, switchNat)+ import qualified Data.NonEmpty as NonEmpty import qualified Data.Empty as Empty @@ -39,119 +44,142 @@ import Prelude (Functor, fmap, Show, ShowS, Int, (+), error)  -type family List position :: * -> *+type family List n :: * -> *+type instance List Unary.Zero = Empty.T+type instance List (Unary.Succ n) = NonEmpty.T (List n) -class (list ~ List (Position list)) => C list where-   type Position list :: *-   switch ::-      f Empty.T ->-      (forall list0. C list0 => f (NonEmpty.T list0)) ->-      f list+type family Length (f :: * -> *)+type instance Length Empty.T = Unary.Zero+type instance Length (NonEmpty.T f) = Unary.Succ (Length f)  -type instance List Zero = Empty.T+newtype T n a = Cons (List n a) -instance C Empty.T where-   type Position Empty.T = Zero-   switch x _ = x+fromFixedList :: List n a -> T n a+fromFixedList = Cons +toFixedList :: T n a -> List n a+toFixedList (Cons xs) = xs -type instance List (Succ position) = NonEmpty.T (List position) -instance C list => C (NonEmpty.T list) where-   type Position (NonEmpty.T list) = Succ (Position list)-   switch _ x = x+end :: T Unary.Zero a+end = Cons Empty.Cons +infixr 5 !: -newtype-   SwitchPos f list =-      SwitchPos {runSwitchPos :: f list (Position list)}+(!:) :: a -> T n a -> T (Unary.Succ n) a+x !: Cons xs = Cons $ NonEmpty.Cons x xs -switchPos ::-   (C list, Position list ~ pos) =>-   f Empty.T Zero ->-   (forall list0 pos0. (C list0, Position list0 ~ pos0) =>-    f (NonEmpty.T list0) (Succ pos0)) ->-   f list pos-switchPos empty nonEmpty =-   runSwitchPos $ switch (SwitchPos empty) (SwitchPos nonEmpty)+viewL :: T (Unary.Succ n) a -> (a, T n a)+viewL (Cons (NonEmpty.Cons x xs)) = (x, Cons xs) +switchL :: (a -> T n a -> b) -> (T (Unary.Succ n) a -> b)+switchL f = P.uncurry f . viewL -end :: Empty.T a-end = Empty.Cons+switchEnd :: b -> T Unary.Zero a -> b+switchEnd x (Cons Empty.Cons) = x  -equal :: (C list, Eq a) => list a -> list a -> Bool-equal xs ys = Fold.and $ Wrap $ zipWith (==) xs ys+newtype WithPos a b n = WithPos {runWithPos :: T n a -> b} -showsPrec :: (C list, Show a) => Int -> list a -> ShowS+withPos ::+   (Positive n) =>+   (forall m. Natural m => T (Unary.Succ m) a -> b) -> T n a -> b+withPos f = runWithPos $ Unary.switchPos (WithPos f)++head :: (Positive n) => T n a -> a+head = withPos (P.fst . viewL)++tail :: T (Unary.Succ n) a -> T n a+tail = P.snd . viewL++singleton :: a -> T U1 a+singleton x = x!:end++minimum :: (Positive n, Ord a) => T n a -> a+minimum = withPos (NonEmpty.minimum . switchL NonEmpty.cons)++maximum :: (Positive n, Ord a) => T n a -> a+maximum = withPos (NonEmpty.maximum . switchL NonEmpty.cons)++++instance (Natural n, Eq a) => Eq (T n a) where+   xs == ys  =  Fold.and $ zipWith (==) xs ys++showsPrec :: (Natural n, Show a) => Int -> T n a -> ShowS showsPrec p =    P.showParen (p>5) . concatS .    List.intersperse (P.showString "!:") .    (++ [P.showString "end"]) .    List.map (P.showsPrec 6) . toList -toList :: (C list) => list a -> [a]-toList = Fold.toList . Wrap+instance (Natural n, Show a) => Show (T n a) where+   showsPrec = showsPrec -newtype Wrap list a = Wrap {unwrap :: list a} +toList :: (Natural n) => T n a -> [a]+toList = Fold.toList -newtype Map a b list = Map {runMap :: list a -> list b} -map :: C list => (a -> b) -> list a -> list b+newtype Map a b n = Map {runMap :: T n a -> T n b}++map :: Natural n => (a -> b) -> T n a -> T n b map f =    runMap $-   switch-      (Map $ \Empty.Cons -> Empty.Cons)-      (Map $ \(NonEmpty.Cons x xs) -> NonEmpty.Cons (f x) $ map f xs)+   switchNat+      (Map $ switchEnd end)+      (Map $ switchL $ \x xs -> f x !: map f xs)  -newtype Sequence f a list = Sequence {runSequence :: list (f a) -> f (list a)}+newtype Sequence f a n = Sequence {runSequence :: T n (f a) -> f (T n a)} -sequenceA :: (Applicative f, C list) => list (f a) -> f (list a)+sequenceA :: (Applicative f, Natural n) => T n (f a) -> f (T n a) sequenceA =    runSequence $-   switch-      (Sequence $ \Empty.Cons -> App.pure Empty.Cons)-      (Sequence $ \(NonEmpty.Cons x xs) -> liftA2 NonEmpty.Cons x $ sequenceA xs)+   switchNat+      (Sequence $ switchEnd $ App.pure end)+      (Sequence $ switchL $ \x xs -> liftA2 (!:) x $ sequenceA xs)  -newtype Repeat a list = Repeat {runRepeat :: list a}+newtype Repeat a n = Repeat {runRepeat :: T n a} -repeat :: C list => a -> list a+repeat :: Natural n => a -> T n a repeat a =    runRepeat $-   switch-      (Repeat $ Empty.Cons)-      (Repeat $ NonEmpty.Cons a $ repeat a)+   switchNat+      (Repeat end)+      (Repeat $ a !: repeat a)  -newtype Zip a b c list = Zip {runZip :: list a -> list b -> list c}+newtype Zip a b c n = Zip {runZip :: T n a -> T n b -> T n c} -zipWith :: C list => (a -> b -> c) -> list a -> list b -> list c+zipWith :: Natural n => (a -> b -> c) -> T n a -> T n b -> T n c zipWith f =    runZip $-   switch-      (Zip $ \Empty.Cons Empty.Cons -> Empty.Cons)-      (Zip $ \(NonEmpty.Cons a as) (NonEmpty.Cons b bs) ->-         NonEmpty.Cons (f a b) $ zipWith f as bs)+   switchNat+      (Zip $ switchEnd $ switchEnd end)+      (Zip $ switchL $ \a as -> switchL $ \b bs -> f a b !: zipWith f as bs)  -instance C list => Functor (Wrap list) where-   fmap f = Wrap . map f . unwrap+instance Natural n => Functor (T n) where+   fmap = map -instance C list => Foldable (Wrap list) where+instance Natural n => Foldable (T n) where    foldMap = foldMapDefault -instance C list => Traversable (Wrap list) where-   sequenceA = fmap Wrap . sequenceA . unwrap+instance Natural n => Traversable (T n) where+   sequenceA = sequenceA -instance C list => Applicative (Wrap list) where-   pure = Wrap . repeat-   Wrap f <*> Wrap x = Wrap $ zipWith ($) f x+instance Natural n => Applicative (T n) where+   pure = repeat+   f <*> x = zipWith ($) f x  +type family Position n :: *+type instance Position Unary.Zero = Zero+type instance Position (Unary.Succ n) = Succ (Position n)+ data Zero data Succ pos = Stop | Succ pos deriving (Eq, Ord, Show) @@ -159,120 +187,129 @@ instance Ord Zero where compare _ _ = EQ  -newtype Update a list pos = Update {runUpdate :: pos -> list a -> list a}+newtype Index n = Index (Position n) -updatePos :: C list => (a -> a) -> Position list -> list a -> list a-updatePos f =-   runUpdate $-   switchPos-      (Update $ \ _ Empty.Cons -> Empty.Cons)-      (Update $ \pos0 (NonEmpty.Cons x xs) ->-          case pos0 of-             Stop -> NonEmpty.Cons (f x) xs-             Succ pos1 -> NonEmpty.Cons x $ updatePos f pos1 xs)+unpackSucc :: Index (Unary.Succ n) -> Succ (Index n)+unpackSucc (Index n1) =+   case n1 of+      Stop -> Stop+      Succ n0 -> Succ $ Index n0 -update :: C list => (a -> a) -> WrapPos list -> list a -> list a-update f (WrapPos k) = updatePos f k +newtype Update a n = Update {runUpdate :: Index n -> T n a -> T n a} -newtype Index a list pos = Index {runIndex :: pos -> list a -> a}+update :: Natural n => (a -> a) -> Index n -> T n a -> T n a+update f =+   runUpdate $+   switchNat+      (Update $ \ _ xs -> xs)+      (Update $ \pos0 -> switchL $ \x xs ->+         case unpackSucc pos0 of+            Stop -> f x !: xs+            Succ pos1 -> x !: update f pos1 xs) -indexPos :: C list => Position list -> list a -> a-indexPos =+newtype PeekIndex a n = PeekIndex {runIndex :: Index n -> T n a -> a}++index :: Natural n => Index n -> T n a -> a+index =    runIndex $-   switchPos-      (Index $ \ _ {- Zero -} Empty.Cons -> error "impossible index")-      (Index $ \pos0 (NonEmpty.Cons x xs) ->-          case pos0 of+   switchNat+      (PeekIndex $ \ _ {- Zero -} -> switchEnd $ error "impossible index")+      (PeekIndex $ \pos0 -> switchL $ \x xs ->+          case unpackSucc pos0 of              Stop -> x-             Succ pos1 -> indexPos pos1 xs)--index :: C list => WrapPos list -> list a -> a-index (WrapPos k) = indexPos k+             Succ pos1 -> index pos1 xs) -newtype Indices list pos = Indices {runIndices :: list pos}+newtype Indices n = Indices {runIndices :: T n (Index n)} -indicesPos :: C list => list (Position list)-indicesPos =+indices :: Natural n => T n (Index n)+indices =    runIndices $-   switchPos-      (Indices $ Empty.Cons)-      (Indices $ NonEmpty.Cons Stop $ map Succ indicesPos)--indices :: C list => list (WrapPos list)-indices = map WrapPos indicesPos+   switchNat+      (Indices end)+      (Indices $ i0 !: map succ indices) -indicesInt :: C list => list Int+indicesInt :: Natural n => T n Int indicesInt =-   unwrap $ NonEmpty.init $ NonEmpty.scanl (+) 0 $ App.pure 1---newtype WrapPos list = WrapPos {unwrapPos :: Position list}--swapWrapPosSucc :: WrapPos (NonEmpty.T list) -> Succ (WrapPos list)-swapWrapPosSucc (WrapPos n) =-   case n of-      Stop -> Stop-      Succ m -> Succ (WrapPos m)+   NonEmpty.init $ NonEmpty.scanl (+) 0 $ App.pure 1  -newtype NumFromPos list = NumFromPos {runNumFromPos :: WrapPos list -> Word}+newtype NumFromIndex n = NumFromIndex {runNumFromIndex :: Index n -> Word} -numFromPos :: C list => WrapPos list -> Word-numFromPos =-   runNumFromPos $-   switch-      (NumFromPos $ \_ -> error "numFromPos")-      (NumFromPos $ \n ->-         case swapWrapPosSucc n of+numFromIndex :: Natural n => Index n -> Word+numFromIndex =+   runNumFromIndex $+   switchNat+      (NumFromIndex $ \_ -> error "numFromIndex")+      (NumFromIndex $ \n ->+         case unpackSucc n of             Stop -> 0-            Succ m -> 1 + numFromPos m)+            Succ m -> 1 + numFromIndex m) -newtype Compare a list =-           Compare {runCompare :: WrapPos list -> WrapPos list -> a} -instance (C list) => Eq (WrapPos list) where+newtype Compare a n =+           Compare {runCompare :: Index n -> Index n -> a}++instance (Natural n) => Eq (Index n) where    (==) =       runCompare $-      switch-         (Compare $ \_ _ -> error "equalPos")+      switchNat+         (Compare $ \_ _ -> error "equalIndex")          (Compare $ \i j ->-             case (swapWrapPosSucc i, swapWrapPosSucc j) of-                (Succ k, Succ l) -> k == l-                (Stop, Stop) -> True-                _ -> False)+            case (unpackSucc i, unpackSucc j) of+               (Succ k, Succ l) -> k == l+               (Stop, Stop) -> True+               _ -> False) -instance (C list) => Ord (WrapPos list) where+instance (Natural n) => Ord (Index n) where    compare =       runCompare $-      switch-         (Compare $ \_ _ -> error "equalPos")+      switchNat+         (Compare $ \_ _ -> error "compareIndex")          (Compare $ \i j ->-             case (swapWrapPosSucc i, swapWrapPosSucc j) of-                (Succ k, Succ l) -> compare k l-                (Stop, Stop) -> EQ-                (Stop, Succ _) -> LT-                (Succ _, Stop) -> GT)+            case (unpackSucc i, unpackSucc j) of+               (Succ k, Succ l) -> compare k l+               (Stop, Stop) -> EQ+               (Stop, Succ _) -> LT+               (Succ _, Stop) -> GT)  -type N0 = Empty.T-type N1 = GE1 Empty.T; type GE1 list = NonEmpty.T list-type N2 = GE2 Empty.T; type GE2 list = NonEmpty.T (GE1 list)-type N3 = GE3 Empty.T; type GE3 list = NonEmpty.T (GE2 list)-type N4 = GE4 Empty.T; type GE4 list = NonEmpty.T (GE3 list)-type N5 = GE5 Empty.T; type GE5 list = NonEmpty.T (GE4 list)-type N6 = GE6 Empty.T; type GE6 list = NonEmpty.T (GE5 list)-type N7 = GE7 Empty.T; type GE7 list = NonEmpty.T (GE6 list)-type N8 = GE8 Empty.T; type GE8 list = NonEmpty.T (GE7 list)+type GE1 n = Unary.Succ n+type GE2 n = Unary.Succ (GE1 n)+type GE3 n = Unary.Succ (GE2 n)+type GE4 n = Unary.Succ (GE3 n)+type GE5 n = Unary.Succ (GE4 n)+type GE6 n = Unary.Succ (GE5 n)+type GE7 n = Unary.Succ (GE6 n)+type GE8 n = Unary.Succ (GE7 n) -succ :: WrapPos list -> WrapPos (NonEmpty.T list)-succ (WrapPos n) = WrapPos (Succ n)+succ :: Index n -> Index (Unary.Succ n)+succ (Index n) = Index (Succ n) -i0 :: WrapPos (GE1 list); i0 = WrapPos Stop-i1 :: WrapPos (GE2 list); i1 = succ i0-i2 :: WrapPos (GE3 list); i2 = succ i1-i3 :: WrapPos (GE4 list); i3 = succ i2-i4 :: WrapPos (GE5 list); i4 = succ i3-i5 :: WrapPos (GE6 list); i5 = succ i4-i6 :: WrapPos (GE7 list); i6 = succ i5-i7 :: WrapPos (GE8 list); i7 = succ i6+i0 :: Index (GE1 n); i0 = Index Stop+i1 :: Index (GE2 n); i1 = succ i0+i2 :: Index (GE3 n); i2 = succ i1+i3 :: Index (GE4 n); i3 = succ i2+i4 :: Index (GE5 n); i4 = succ i3+i5 :: Index (GE6 n); i5 = succ i4+i6 :: Index (GE7 n); i6 = succ i5+i7 :: Index (GE8 n); i7 = succ i6++++newtype+   Uncurry a b n =+      Uncurry {+         runUncurry :: Curried n a b -> T n a -> b+      }++type family Curried n a b+type instance Curried Unary.Zero a b = b+type instance Curried (Unary.Succ n) a b = a -> Curried n a b++uncurry :: (Unary.Natural n) => Curried n a b -> T n a -> b+uncurry =+   runUncurry $+   Unary.switchNat+      (Uncurry switchEnd)+      (Uncurry $ \f -> switchL (\x -> uncurry (f x)))

@@ -1,249 +0,0 @@-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE EmptyDataDecls #-}-module Data.FixedLength.Unary (-   T, Position, List,-   Zero, Succ(Stop, Succ),-   toList, showsPrec,-   map, zipWith, sequenceA, repeat,-   index, update, indices, indicesInt, numFromIndex,-   GE1, GE2, GE3, GE4, GE5, GE6, GE7, GE8,-   i0, i1, i2, i3, i4, i5, i6, i7,-   (!:), end, viewL, switchL,-   ) where--import qualified Type.Data.Num.Unary as Unary-import Type.Data.Num.Unary (Natural, switchNat)--import qualified Data.NonEmpty as NonEmpty-import qualified Data.Empty as Empty--import qualified Control.Applicative as App-import qualified Data.Traversable as Trav-import qualified Data.Foldable as Fold-import qualified Data.List as List-import Control.Applicative (Applicative, liftA2)-import Data.Traversable (Traversable, foldMapDefault)-import Data.Foldable (Foldable, foldMap)-import Data.List ((++))-import Data.Word (Word)--import Data.Function (($), (.))-import Data.Tuple (uncurry)-import Data.Bool (Bool(False, True))-import Data.Ord (Ord, Ordering(LT,EQ,GT), compare, (>))-import Data.Eq (Eq, (==))--import Text.Show.HT (concatS)--import qualified Prelude as P-import Prelude (Functor, fmap, Show, ShowS, Int, (+), error)---type family List n :: * -> *-type instance List Unary.Zero = Empty.T-type instance List (Unary.Succ n) = NonEmpty.T (List n)--newtype T n a = Cons (List n a)---end :: T Unary.Zero a-end = Cons Empty.Cons--infixr 5 !:--(!:) :: a -> T n a -> T (Unary.Succ n) a-x !: Cons xs = Cons $ NonEmpty.Cons x xs--viewL :: T (Unary.Succ n) a -> (a, T n a)-viewL (Cons (NonEmpty.Cons x xs)) = (x, Cons xs)--switchL :: (a -> T n a -> b) -> (T (Unary.Succ n) a -> b)-switchL f = uncurry f . viewL---instance (Natural n, Eq a) => Eq (T n a) where-   xs == ys  =  Fold.and $ zipWith (==) xs ys--showsPrec :: (Natural n, Show a) => Int -> T n a -> ShowS-showsPrec p =-   P.showParen (p>5) . concatS .-   List.intersperse (P.showString "!:") .-   (++ [P.showString "end"]) .-   List.map (P.showsPrec 6) . toList--toList :: (Natural n) => T n a -> [a]-toList = Fold.toList---newtype Map a b n = Map {runMap :: T n a -> T n b}--map :: Natural n => (a -> b) -> T n a -> T n b-map f =-   runMap $-   switchNat-      (Map $ \(Cons Empty.Cons) -> end)-      (Map $ switchL $ \x xs -> f x !: map f xs)---newtype Sequence f a n = Sequence {runSequence :: T n (f a) -> f (T n a)}--sequenceA :: (Applicative f, Natural n) => T n (f a) -> f (T n a)-sequenceA =-   runSequence $-   switchNat-      (Sequence $ \(Cons Empty.Cons) -> App.pure end)-      (Sequence $ switchL $ \x xs -> liftA2 (!:) x $ sequenceA xs)---newtype Repeat a n = Repeat {runRepeat :: T n a}--repeat :: Natural n => a -> T n a-repeat a =-   runRepeat $-   switchNat-      (Repeat end)-      (Repeat $ a !: repeat a)---newtype Zip a b c n = Zip {runZip :: T n a -> T n b -> T n c}--zipWith :: Natural n => (a -> b -> c) -> T n a -> T n b -> T n c-zipWith f =-   runZip $-   switchNat-      (Zip $ \(Cons Empty.Cons) (Cons Empty.Cons) -> end)-      (Zip $ switchL $ \a as -> switchL $ \b bs -> f a b !: zipWith f as bs)---instance Natural n => Functor (T n) where-   fmap = map--instance Natural n => Foldable (T n) where-   foldMap = foldMapDefault--instance Natural n => Traversable (T n) where-   sequenceA = sequenceA--instance Natural n => Applicative (T n) where-   pure = repeat-   f <*> x = zipWith ($) f x---type family Position n :: *-type instance Position Unary.Zero = Zero-type instance Position (Unary.Succ n) = Succ (Position n)--data Zero-data Succ pos = Stop | Succ pos deriving (Eq, Ord, Show)--instance Eq Zero where _==_ = True-instance Ord Zero where compare _ _ = EQ---newtype Index n = Index (Position n)--unpackSucc :: Index (Unary.Succ n) -> Succ (Index n)-unpackSucc (Index n1) =-   case n1 of-      Stop -> Stop-      Succ n0 -> Succ $ Index n0---newtype Update a n = Update {runUpdate :: Index n -> T n a -> T n a}--update :: Natural n => (a -> a) -> Index n -> T n a -> T n a-update f =-   runUpdate $-   switchNat-      (Update $ \ _ xs -> xs)-      (Update $ \pos0 -> switchL $ \x xs ->-         case unpackSucc pos0 of-            Stop -> f x !: xs-            Succ pos1 -> x !: update f pos1 xs)--newtype PeekIndex a n = PeekIndex {runIndex :: Index n -> T n a -> a}--index :: Natural n => Index n -> T n a -> a-index =-   runIndex $-   switchNat-      (PeekIndex $ \ _ {- Zero -} (Cons Empty.Cons) -> error "impossible index")-      (PeekIndex $ \pos0 -> switchL $ \x xs ->-          case unpackSucc pos0 of-             Stop -> x-             Succ pos1 -> index pos1 xs)--newtype Indices n = Indices {runIndices :: T n (Index n)}--indices :: Natural n => T n (Index n)-indices =-   runIndices $-   switchNat-      (Indices end)-      (Indices $ i0 !: map succ indices)--indicesInt :: Natural n => T n Int-indicesInt =-   NonEmpty.init $ NonEmpty.scanl (+) 0 $ App.pure 1---newtype NumFromIndex n = NumFromIndex {runNumFromIndex :: Index n -> Word}--numFromIndex :: Natural n => Index n -> Word-numFromIndex =-   runNumFromIndex $-   switchNat-      (NumFromIndex $ \_ -> error "numFromIndex")-      (NumFromIndex $ \n ->-         case unpackSucc n of-            Stop -> 0-            Succ m -> 1 + numFromIndex m)---newtype Compare a n =-           Compare {runCompare :: Index n -> Index n -> a}--instance (Natural n) => Eq (Index n) where-   (==) =-      runCompare $-      switchNat-         (Compare $ \_ _ -> error "equalIndex")-         (Compare $ \i j ->-            case (unpackSucc i, unpackSucc j) of-               (Succ k, Succ l) -> k == l-               (Stop, Stop) -> True-               _ -> False)--instance (Natural n) => Ord (Index n) where-   compare =-      runCompare $-      switchNat-         (Compare $ \_ _ -> error "compareIndex")-         (Compare $ \i j ->-            case (unpackSucc i, unpackSucc j) of-               (Succ k, Succ l) -> compare k l-               (Stop, Stop) -> EQ-               (Stop, Succ _) -> LT-               (Succ _, Stop) -> GT)---type GE1 n = Unary.Succ n-type GE2 n = Unary.Succ (GE1 n)-type GE3 n = Unary.Succ (GE2 n)-type GE4 n = Unary.Succ (GE3 n)-type GE5 n = Unary.Succ (GE4 n)-type GE6 n = Unary.Succ (GE5 n)-type GE7 n = Unary.Succ (GE6 n)-type GE8 n = Unary.Succ (GE7 n)--succ :: Index n -> Index (Unary.Succ n)-succ (Index n) = Index (Succ n)--i0 :: Index (GE1 n); i0 = Index Stop-i1 :: Index (GE2 n); i1 = succ i0-i2 :: Index (GE3 n); i2 = succ i1-i3 :: Index (GE4 n); i3 = succ i2-i4 :: Index (GE5 n); i4 = succ i3-i5 :: Index (GE6 n); i5 = succ i4-i6 :: Index (GE7 n); i6 = succ i5-i7 :: Index (GE8 n); i7 = succ i6