    {-|
    Description: Representations of a type-level natural at runtime.
    Copyright        : (c) Galois, Inc 2019

    This defines a type 'Peano' and 'PeanoRepr' for representing a
    type-level natural at runtime. These type-level numbers are defined
    inductively instead of using GHC.TypeLits.

    As a result, type-level computation defined recursively over these
    numbers works more smoothly. (For example, see the type-level
    function 'Repeat' below.)

    Note: as in "NatRepr", in UNSAFE mode, the runtime representation of
    these type-level natural numbers is 'Word64'.

    -}
    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE EmptyCase #-}
    {-# LANGUAGE ExplicitNamespaces #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE RoleAnnotations #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE UndecidableInstances #-}

    {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
    #if __GLASGOW_HASKELL__ >= 805
    {-# LANGUAGE NoStarIsType #-}
    #endif
    module Data.Parameterized.Peano
       ( -- * Peano
         Peano
         , Z , S

         -- * Basic arithmetic
         , Plus, Minus, Mul,  Max, Min
         , plusP, minusP, mulP, maxP, minP
         , zeroP, succP, predP

         -- * Counting
         , Repeat, CtxSizeP
         , repeatP, ctxSizeP
         -- * Comparisons
         , Le, Lt, Gt, Ge
         , leP, ltP, gtP, geP

         -- * Runtime representation
         , KnownPeano
         , PeanoRepr
         , PeanoView(..), peanoView, viewRepr

         -- * 'Some Peano'
         , mkPeanoRepr, peanoValue
         , somePeano
         , maxPeano
         , minPeano
         , peanoLength

         -- * Properties
         , plusCtxSizeAxiom
         , minusPlusAxiom
         , ltMinusPlusAxiom

         -- * Re-exports
         , TestEquality(..)
         , (:~:)(..)
         , Data.Parameterized.Some.Some

         ) where

    import           Data.Parameterized.BoolRepr
    import           Data.Parameterized.Classes
    import           Data.Parameterized.DecidableEq
    import           Data.Parameterized.Some
    import           Data.Parameterized.Context

    import           Data.Word

    #ifdef UNSAFE_OPS
    import           Data.Parameterized.Axiom
    import           Unsafe.Coerce(unsafeCoerce)
    #endif

    ------------------------------------------------------------------------
    -- * Peano arithmetic

    -- | Unary representation for natural numbers
    data Peano = Z | S Peano
    -- | Peano zero
    type Z = 'Z
    -- | Peano successor
    type S = 'S

    -- Peano numbers are more about *counting* than arithmetic.
    -- They are most useful as iteration arguments and list indices
    -- However, for completeness, we define a few standard
    -- operations.

    -- | Addition
    type family Plus (a :: Peano) (b :: Peano) :: Peano where
      Plus Z     b = b
      Plus (S a) b = S (Plus a b)

    -- | Subtraction
    type family Minus (a :: Peano) (b :: Peano) :: Peano where
      Minus Z     b     = Z
      Minus (S a) (S b) = Minus a b
      Minus a    Z      = a

    -- | Multiplication
    type family Mul (a :: Peano) (b :: Peano) :: Peano where
      Mul Z     b = Z
      Mul (S a) b = Plus a (Mul a b)

    -- | Less-than-or-equal
    type family Le  (a :: Peano) (b :: Peano) :: Bool where
      Le  Z  b        = 'True
      Le  a  Z        = 'False
      Le  (S a) (S b) = Le a b

    -- | Less-than
    type family Lt  (a :: Peano) (b :: Peano) :: Bool where
      Lt a b = Le (S a) b

    -- | Greater-than
    type family Gt  (a :: Peano) (b :: Peano) :: Bool where
      Gt a b = Le b a

    -- | Greater-than-or-equal
    type family Ge  (a :: Peano) (b :: Peano) :: Bool where
      Ge a b = Lt b a

    -- | Maximum
    type family Max (a :: Peano) (b :: Peano) :: Peano where
      Max Z b = b
      Max a Z = a
      Max (S a) (S b) = S (Max a b)

    -- | Minimum
    type family Min (a :: Peano) (b :: Peano) :: Peano where
      Min Z b = Z
      Min a Z = Z
      Min (S a) (S b) = S (Min a b)

    -- | Apply a constructor 'f' n-times to an argument 's'
    type family Repeat (m :: Peano) (f :: k -> k) (s :: k) :: k where
      Repeat Z f s     = s
      Repeat (S m) f s = f (Repeat m f s)

    -- | Calculate the size of a context
    type family CtxSizeP (ctx :: Ctx k) :: Peano where
      CtxSizeP 'EmptyCtx   = Z
      CtxSizeP (xs '::> x) = S (CtxSizeP xs)

    ------------------------------------------------------------------------
    -- * Run time representation of Peano numbers

    #ifdef UNSAFE_OPS
    -- | The run time value, stored as an Word64
    -- As these are unary numbers, we don't worry about overflow.
    newtype PeanoRepr (n :: Peano) =
      PeanoRepr { forall (n :: Peano). PeanoRepr n -> Word64
    peanoValue :: Word64 }
    -- n is Phantom in the definition, but we don't want to allow coerce
    type role PeanoRepr nominal
    #else
    -- | Runtime value
    type PeanoRepr = PeanoView
    -- | Conversion
    peanoValue :: PeanoRepr n -> Word64
    peanoValue ZRepr     = 0
    peanoValue (SRepr m) = 1 + peanoValue m
    #endif

    -- | When we have optimized the runtime representation,
    -- we need to have a "view" that decomposes the representation
    -- into the standard form.
    data PeanoView (n :: Peano) where
      ZRepr :: PeanoView Z
      SRepr :: PeanoRepr n -> PeanoView (S n)

    -- | Test whether a number is Zero or Successor
    peanoView :: PeanoRepr n -> PeanoView n
    #ifdef UNSAFE_OPS
    peanoView :: forall (n :: Peano). PeanoRepr n -> PeanoView n
    peanoView (PeanoRepr Word64
    i) =
      if Word64
    i Word64 -> Word64 -> Bool
    forall a. Eq a => a -> a -> Bool
    == Word64
    0
      then PeanoView Z -> PeanoView n
    forall a b. a -> b
    unsafeCoerce PeanoView Z
    ZRepr
      else PeanoView (S (ZonkAny 1)) -> PeanoView n
    forall a b. a -> b
    unsafeCoerce (PeanoRepr (ZonkAny 1) -> PeanoView (S (ZonkAny 1))
    forall (n :: Peano). PeanoRepr n -> PeanoView (S n)
    SRepr (Word64 -> PeanoRepr (ZonkAny 1)
    forall (n :: Peano). Word64 -> PeanoRepr n
    PeanoRepr (Word64
    iWord64 -> Word64 -> Word64
    forall a. Num a => a -> a -> a
    -Word64
    1)))
    #else
    peanoView = id
    #endif

    -- | convert the view back to the runtime representation
    viewRepr :: PeanoView n -> PeanoRepr n
    #ifdef UNSAFE_OPS
    viewRepr :: forall (n :: Peano). PeanoView n -> PeanoRepr n
    viewRepr PeanoView n
    ZRepr     = Word64 -> PeanoRepr n
    forall (n :: Peano). Word64 -> PeanoRepr n
    PeanoRepr Word64
    0
    viewRepr (SRepr PeanoRepr n
    n) = Word64 -> PeanoRepr n
    forall (n :: Peano). Word64 -> PeanoRepr n
    PeanoRepr (PeanoRepr n -> Word64
    forall (n :: Peano). PeanoRepr n -> Word64
    peanoValue PeanoRepr n
    n Word64 -> Word64 -> Word64
    forall a. Num a => a -> a -> a
    + Word64
    1)
    #else
    viewRepr = id
    #endif

    ----------------------------------------------------------
    -- * Class instances

    instance Hashable (PeanoRepr n) where
      hashWithSalt :: Int -> PeanoRepr n -> Int
    hashWithSalt Int
    i PeanoRepr n
    x = Int -> Word64 -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt Int
    i (PeanoRepr n -> Word64
    forall (n :: Peano). PeanoRepr n -> Word64
    peanoValue PeanoRepr n
    x)

    instance Eq (PeanoRepr m) where
      PeanoRepr m
    _ == :: PeanoRepr m -> PeanoRepr m -> Bool
    == PeanoRepr m
    _ = Bool
    True

    instance EqF PeanoRepr where
      eqF :: forall (m :: Peano). PeanoRepr m -> PeanoRepr m -> Bool
    eqF PeanoRepr a
    _ PeanoRepr a
    _ = Bool
    True

    instance TestEquality PeanoRepr where
    #ifdef UNSAFE_OPS
      testEquality :: forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> Maybe (a :~: b)
    testEquality (PeanoRepr Word64
    m) (PeanoRepr Word64
    n)
        | Word64
    m Word64 -> Word64 -> Bool
    forall a. Eq a => a -> a -> Bool
    == Word64
    n = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: b
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom
        | Bool
    otherwise = Maybe (a :~: b)
    forall a. Maybe a
    Nothing
    #else
      testEquality ZRepr ZRepr = Just Refl
      testEquality (SRepr m1) (SRepr m2)
        | Just Refl <- testEquality m1 m2
        = Just Refl
      testEquality _ _ = Nothing

    #endif

    instance DecidableEq PeanoRepr where
    #ifdef UNSAFE_OPS
      decEq :: forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> Either (a :~: b) ((a :~: b) -> Void)
    decEq (PeanoRepr Word64
    m) (PeanoRepr Word64
    n)
        | Word64
    m Word64 -> Word64 -> Bool
    forall a. Eq a => a -> a -> Bool
    == Word64
    n    = (a :~: b) -> Either (a :~: b) ((a :~: b) -> Void)
    forall a b. a -> Either a b
    Left a :~: b
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom
        | Bool
    otherwise = ((a :~: b) -> Void) -> Either (a :~: b) ((a :~: b) -> Void)
    forall a b. b -> Either a b
    Right (((a :~: b) -> Void) -> Either (a :~: b) ((a :~: b) -> Void))
    -> ((a :~: b) -> Void) -> Either (a :~: b) ((a :~: b) -> Void)
    forall a b. (a -> b) -> a -> b
    $
            \a :~: b
    x -> (a :~: b) -> Void -> Void
    forall a b. a -> b -> b
    seq a :~: b
    x (Void -> Void) -> Void -> Void
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Void
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "Impossible [DecidableEq on PeanoRepr]"
    #else
      decEq ZRepr ZRepr = Left Refl
      decEq (SRepr m1) (SRepr m2) =
        case decEq m1 m2 of
          Left Refl -> Left Refl
          Right f   -> Right $ \case Refl -> f Refl
      decEq ZRepr (SRepr _) =
          Right $ \case {}
      decEq (SRepr _) ZRepr =
          Right $ \case {}
    #endif

    instance OrdF PeanoRepr where
    #ifdef UNSAFE_OPS
      compareF :: forall (x :: Peano) (y :: Peano).
    PeanoRepr x -> PeanoRepr y -> OrderingF x y
    compareF (PeanoRepr Word64
    m) (PeanoRepr Word64
    n)
        | Word64
    m Word64 -> Word64 -> Bool
    forall a. Ord a => a -> a -> Bool
    < Word64
    n     = OrderingF (ZonkAny 3) (ZonkAny 4) -> OrderingF x y
    forall a b. a -> b
    unsafeCoerce OrderingF (ZonkAny 3) (ZonkAny 4)
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
        | Word64
    m Word64 -> Word64 -> Bool
    forall a. Eq a => a -> a -> Bool
    == Word64
    n    = OrderingF (ZonkAny 6) (ZonkAny 6) -> OrderingF x y
    forall a b. a -> b
    unsafeCoerce OrderingF (ZonkAny 6) (ZonkAny 6)
    forall {k} (x :: k). OrderingF x x
    EQF
        | Bool
    otherwise = OrderingF (ZonkAny 8) (ZonkAny 9) -> OrderingF x y
    forall a b. a -> b
    unsafeCoerce OrderingF (ZonkAny 8) (ZonkAny 9)
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF
    #else
      compareF ZRepr      ZRepr      = EQF
      compareF ZRepr      (SRepr _)  = LTF
      compareF (SRepr _)  ZRepr      = GTF
      compareF (SRepr m1) (SRepr m2) =
        case compareF m1 m2 of
           EQF -> EQF
           LTF -> LTF
           GTF -> GTF
    #endif

    instance PolyEq (PeanoRepr m) (PeanoRepr n) where
      polyEqF :: PeanoRepr m -> PeanoRepr n -> Maybe (PeanoRepr m :~: PeanoRepr n)
    polyEqF PeanoRepr m
    x PeanoRepr n
    y = (\m :~: n
    Refl -> PeanoRepr m :~: PeanoRepr m
    PeanoRepr m :~: PeanoRepr n
    forall {k} (a :: k). a :~: a
    Refl) ((m :~: n) -> PeanoRepr m :~: PeanoRepr n)
    -> Maybe (m :~: n) -> Maybe (PeanoRepr m :~: PeanoRepr n)
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> PeanoRepr m -> PeanoRepr n -> Maybe (m :~: n)
    forall {k} (f :: k -> Type) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> Maybe (a :~: b)
    testEquality PeanoRepr m
    x PeanoRepr n
    y

    -- Display as digits, not in unary
    instance Show (PeanoRepr p) where
      show :: PeanoRepr p -> [Char]
    show PeanoRepr p
    p = Word64 -> [Char]
    forall a. Show a => a -> [Char]
    show (PeanoRepr p -> Word64
    forall (n :: Peano). PeanoRepr n -> Word64
    peanoValue PeanoRepr p
    p)

    instance ShowF PeanoRepr

    instance HashableF PeanoRepr where
      hashWithSaltF :: forall (n :: Peano). Int -> PeanoRepr n -> Int
    hashWithSaltF = Int -> PeanoRepr tp -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt

    ----------------------------------------------------------
    -- * Implicit runtime Peano numbers

    -- | Implicit runtime representation
    type KnownPeano = KnownRepr PeanoRepr

    instance KnownRepr PeanoRepr Z where
      knownRepr :: PeanoRepr Z
    knownRepr = PeanoView Z -> PeanoRepr Z
    forall (n :: Peano). PeanoView n -> PeanoRepr n
    viewRepr PeanoView Z
    ZRepr
    instance (KnownRepr PeanoRepr n) => KnownRepr PeanoRepr (S n) where
      knownRepr :: PeanoRepr (S n)
    knownRepr = PeanoView (S n) -> PeanoRepr (S n)
    forall (n :: Peano). PeanoView n -> PeanoRepr n
    viewRepr (PeanoRepr n -> PeanoView (S n)
    forall (n :: Peano). PeanoRepr n -> PeanoView (S n)
    SRepr PeanoRepr n
    forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
    knownRepr)

    ----------------------------------------------------------
    -- * Operations on runtime numbers

    -- | Zero
    zeroP :: PeanoRepr Z
    #ifdef UNSAFE_OPS
    zeroP :: PeanoRepr Z
    zeroP = Word64 -> PeanoRepr Z
    forall (n :: Peano). Word64 -> PeanoRepr n
    PeanoRepr Word64
    0
    #else
    zeroP = ZRepr
    #endif

    -- | Successor, Increment
    succP :: PeanoRepr n -> PeanoRepr (S n)
    #ifdef UNSAFE_OPS
    succP :: forall (n :: Peano). PeanoRepr n -> PeanoRepr (S n)
    succP (PeanoRepr Word64
    i) = Word64 -> PeanoRepr (S n)
    forall (n :: Peano). Word64 -> PeanoRepr n
    PeanoRepr (Word64
    iWord64 -> Word64 -> Word64
    forall a. Num a => a -> a -> a
    +Word64
    1)
    #else
    succP = SRepr
    #endif

    -- | Get the predecessor (decrement)
    predP :: PeanoRepr (S n) -> PeanoRepr n
    #ifdef UNSAFE_OPS
    predP :: forall (n :: Peano). PeanoRepr (S n) -> PeanoRepr n
    predP (PeanoRepr Word64
    i) = Word64 -> PeanoRepr n
    forall (n :: Peano). Word64 -> PeanoRepr n
    PeanoRepr (Word64
    iWord64 -> Word64 -> Word64
    forall a. Num a => a -> a -> a
    -Word64
    1)
    #else
    predP (SRepr i) = i
    #endif

    -- | Addition
    plusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Plus a b)
    #ifdef UNSAFE_OPS
    plusP :: forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> PeanoRepr (Plus a b)
    plusP (PeanoRepr Word64
    a) (PeanoRepr Word64
    b) = Word64 -> PeanoRepr (Plus a b)
    forall (n :: Peano). Word64 -> PeanoRepr n
    PeanoRepr (Word64
    a Word64 -> Word64 -> Word64
    forall a. Num a => a -> a -> a
    + Word64
    b)
    #else
    plusP (SRepr a) b = SRepr (plusP a b)
    #endif

    -- | Subtraction
    minusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Minus a b)
    #ifdef UNSAFE_OPS
    minusP :: forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> PeanoRepr (Minus a b)
    minusP (PeanoRepr Word64
    a) (PeanoRepr Word64
    b) = Word64 -> PeanoRepr (Minus a b)
    forall (n :: Peano). Word64 -> PeanoRepr n
    PeanoRepr (Word64
    a Word64 -> Word64 -> Word64
    forall a. Num a => a -> a -> a
    - Word64
    b)
    #else
    minusP ZRepr     _b        = ZRepr
    minusP (SRepr a) (SRepr b) = minusP a b
    minusP a ZRepr             = a
    #endif

    -- | Multiplication
    mulP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Mul a b)
    #ifdef UNSAFE_OPS
    mulP :: forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> PeanoRepr (Mul a b)
    mulP (PeanoRepr Word64
    a) (PeanoRepr Word64
    b) = Word64 -> PeanoRepr (Mul a b)
    forall (n :: Peano). Word64 -> PeanoRepr n
    PeanoRepr (Word64
    a Word64 -> Word64 -> Word64
    forall a. Num a => a -> a -> a
    * Word64
    b)
    #else
    mulP ZRepr     _b = ZRepr
    mulP (SRepr a) b  = plusP a (mulP a b)
    #endif

    -- | Maximum
    maxP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Max a b)
    #ifdef UNSAFE_OPS
    maxP :: forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> PeanoRepr (Max a b)
    maxP (PeanoRepr Word64
    a) (PeanoRepr Word64
    b) = Word64 -> PeanoRepr (Max a b)
    forall (n :: Peano). Word64 -> PeanoRepr n
    PeanoRepr (Word64 -> Word64 -> Word64
    forall a. Ord a => a -> a -> a
    max Word64
    a Word64
    b)
    #else
    maxP ZRepr     b         = b
    maxP a         ZRepr     = a
    maxP (SRepr a) (SRepr b) = SRepr (maxP a b)
    #endif

    -- | Minimum
    minP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Min a b)
    #ifdef UNSAFE_OPS
    minP :: forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> PeanoRepr (Min a b)
    minP (PeanoRepr Word64
    a) (PeanoRepr Word64
    b) = Word64 -> PeanoRepr (Min a b)
    forall (n :: Peano). Word64 -> PeanoRepr n
    PeanoRepr (Word64 -> Word64 -> Word64
    forall a. Ord a => a -> a -> a
    min Word64
    a Word64
    b)
    #else
    minP ZRepr     _b        = ZRepr
    minP _a        ZRepr     = ZRepr
    minP (SRepr a) (SRepr b) = SRepr (minP a b)
    #endif

    -- | Less-than-or-equal-to
    leP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Le a b)
    #ifdef UNSAFE_OPS
    leP :: forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> BoolRepr (Le a b)
    leP  (PeanoRepr Word64
    a) (PeanoRepr Word64
    b) =
      if Word64
    a Word64 -> Word64 -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Word64
    b then BoolRepr 'True -> BoolRepr (Le a b)
    forall a b. a -> b
    unsafeCoerce (BoolRepr 'True
    TrueRepr)
                else BoolRepr 'False -> BoolRepr (Le a b)
    forall a b. a -> b
    unsafeCoerce(BoolRepr 'False
    FalseRepr)
    #else
    leP ZRepr      ZRepr    = TrueRepr
    leP ZRepr     (SRepr _) = TrueRepr
    leP (SRepr _) ZRepr     = FalseRepr
    leP (SRepr a) (SRepr b) = leP a b
    #endif

    -- | Less-than
    ltP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Lt a b)
    ltP :: forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> BoolRepr (Lt a b)
    ltP PeanoRepr a
    a PeanoRepr b
    b = PeanoRepr (S a) -> PeanoRepr b -> BoolRepr (Le (S a) b)
    forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> BoolRepr (Le a b)
    leP (PeanoRepr a -> PeanoRepr (S a)
    forall (n :: Peano). PeanoRepr n -> PeanoRepr (S n)
    succP PeanoRepr a
    a) PeanoRepr b
    b

    -- | Greater-than-or-equal-to
    geP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Ge a b)
    geP :: forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> BoolRepr (Ge a b)
    geP PeanoRepr a
    a PeanoRepr b
    b = PeanoRepr b -> PeanoRepr a -> BoolRepr (Lt b a)
    forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> BoolRepr (Lt a b)
    ltP PeanoRepr b
    b PeanoRepr a
    a

    -- | Greater-than
    gtP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Gt a b)
    gtP :: forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> BoolRepr (Gt a b)
    gtP PeanoRepr a
    a PeanoRepr b
    b = PeanoRepr b -> PeanoRepr a -> BoolRepr (Le b a)
    forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> BoolRepr (Le a b)
    leP PeanoRepr b
    b PeanoRepr a
    a

    -- | Apply a constructor 'f' n-times to an argument 's'
    repeatP :: PeanoRepr m -> (forall a. repr a -> repr (f a)) -> repr s -> repr (Repeat m f s)
    repeatP :: forall {k} (m :: Peano) (repr :: k -> Type) (f :: k -> k) (s :: k).
    PeanoRepr m
    -> (forall (a :: k). repr a -> repr (f a))
    -> repr s
    -> repr (Repeat m f s)
    repeatP PeanoRepr m
    n forall (a :: k). repr a -> repr (f a)
    f repr s
    s = case PeanoRepr m -> PeanoView m
    forall (n :: Peano). PeanoRepr n -> PeanoView n
    peanoView PeanoRepr m
    n of
      PeanoView m
    ZRepr   -> repr s
    repr (Repeat m f s)
    s
      SRepr PeanoRepr n
    m -> repr (Repeat n f s) -> repr (f (Repeat n f s))
    forall (a :: k). repr a -> repr (f a)
    f (PeanoRepr n
    -> (forall (a :: k). repr a -> repr (f a))
    -> repr s
    -> repr (Repeat n f s)
    forall {k} (m :: Peano) (repr :: k -> Type) (f :: k -> k) (s :: k).
    PeanoRepr m
    -> (forall (a :: k). repr a -> repr (f a))
    -> repr s
    -> repr (Repeat m f s)
    repeatP PeanoRepr n
    m repr a -> repr (f a)
    forall (a :: k). repr a -> repr (f a)
    f repr s
    s)

    -- | Calculate the size of a context
    ctxSizeP :: Assignment f ctx -> PeanoRepr (CtxSizeP ctx)
    ctxSizeP :: forall {k} (f :: k -> Type) (ctx :: Ctx k).
    Assignment f ctx -> PeanoRepr (CtxSizeP ctx)
    ctxSizeP Assignment f ctx
    r = case Assignment f ctx -> AssignView f ctx
    forall {k} (f :: k -> Type) (ctx :: Ctx k).
    Assignment f ctx -> AssignView f ctx
    viewAssign Assignment f ctx
    r of
      AssignView f ctx
    AssignEmpty -> PeanoRepr (CtxSizeP ctx)
    PeanoRepr Z
    zeroP
      AssignExtend Assignment f ctx1
    a f tp
    _ -> PeanoRepr (CtxSizeP ctx1) -> PeanoRepr (S (CtxSizeP ctx1))
    forall (n :: Peano). PeanoRepr n -> PeanoRepr (S n)
    succP (Assignment f ctx1 -> PeanoRepr (CtxSizeP ctx1)
    forall {k} (f :: k -> Type) (ctx :: Ctx k).
    Assignment f ctx -> PeanoRepr (CtxSizeP ctx)
    ctxSizeP Assignment f ctx1
    a)

    ------------------------------------------------------------------------
    -- * Some PeanoRepr

    -- | Convert a 'Word64' to a 'PeanoRepr'
    mkPeanoRepr :: Word64 -> Some PeanoRepr
    #ifdef UNSAFE_OPS
    mkPeanoRepr :: Word64 -> Some PeanoRepr
    mkPeanoRepr Word64
    n = PeanoRepr (ZonkAny 0) -> Some PeanoRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (Word64 -> PeanoRepr (ZonkAny 0)
    forall (n :: Peano). Word64 -> PeanoRepr n
    PeanoRepr Word64
    n)
    #else
    mkPeanoRepr 0 = Some ZRepr
    mkPeanoRepr n = case mkPeanoRepr (n - 1) of
                     Some mr -> Some (SRepr mr)
    #endif

    -- | Turn an @Integral@ value into a 'PeanoRepr'.  Returns @Nothing@
    --   if the given value is negative.
    somePeano :: Integral a => a -> Maybe (Some PeanoRepr)
    somePeano :: forall a. Integral a => a -> Maybe (Some PeanoRepr)
    somePeano a
    x | a
    x a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    >= a
    0 = Some PeanoRepr -> Maybe (Some PeanoRepr)
    forall a. a -> Maybe a
    Just (Some PeanoRepr -> Maybe (Some PeanoRepr))
    -> (Word64 -> Some PeanoRepr) -> Word64 -> Maybe (Some PeanoRepr)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word64 -> Some PeanoRepr
    mkPeanoRepr (Word64 -> Maybe (Some PeanoRepr))
    -> Word64 -> Maybe (Some PeanoRepr)
    forall a b. (a -> b) -> a -> b
    $! a -> Word64
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral a
    x
    somePeano a
    _ = Maybe (Some PeanoRepr)
    forall a. Maybe a
    Nothing

    -- | Return the maximum of two representations.
    maxPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr
    maxPeano :: forall (m :: Peano) (n :: Peano).
    PeanoRepr m -> PeanoRepr n -> Some PeanoRepr
    maxPeano PeanoRepr m
    x PeanoRepr n
    y = PeanoRepr (Max m n) -> Some PeanoRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (PeanoRepr m -> PeanoRepr n -> PeanoRepr (Max m n)
    forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> PeanoRepr (Max a b)
    maxP PeanoRepr m
    x PeanoRepr n
    y)

    -- | Return the minimum of two representations.
    minPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr
    minPeano :: forall (m :: Peano) (n :: Peano).
    PeanoRepr m -> PeanoRepr n -> Some PeanoRepr
    minPeano PeanoRepr m
    x PeanoRepr n
    y = PeanoRepr (Min m n) -> Some PeanoRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (PeanoRepr m -> PeanoRepr n -> PeanoRepr (Min m n)
    forall (a :: Peano) (b :: Peano).
    PeanoRepr a -> PeanoRepr b -> PeanoRepr (Min a b)
    minP PeanoRepr m
    x PeanoRepr n
    y)

    -- | List length as a Peano number
    peanoLength :: [a] -> Some PeanoRepr
    peanoLength :: forall a. [a] -> Some PeanoRepr
    peanoLength [] = PeanoRepr Z -> Some PeanoRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some PeanoRepr Z
    zeroP
    peanoLength (a
    _:[a]
    xs) = case [a] -> Some PeanoRepr
    forall a. [a] -> Some PeanoRepr
    peanoLength [a]
    xs of
      Some PeanoRepr x
    n -> PeanoRepr (S x) -> Some PeanoRepr
    forall k (f :: k -> Type) (x :: k). f x -> Some f
    Some (PeanoRepr x -> PeanoRepr (S x)
    forall (n :: Peano). PeanoRepr n -> PeanoRepr (S n)
    succP PeanoRepr x
    n)

    ------------------------------------------------------------------------
    -- * Properties about Peano numbers
    --
    -- The safe version of these properties includes a runtime proof of
    -- the equality. The unsafe version has no run-time
    -- computation. Therefore, in the unsafe version, the "Repr" arguments
    -- can be used as proxies (i.e. called using 'undefined') but must be
    -- supplied to the safe versions.

    -- | Context size commutes with context append
    plusCtxSizeAxiom :: forall t1 t2 f.
      Assignment f t1 -> Assignment f t2 ->
      CtxSizeP (t1 <+> t2) :~: Plus (CtxSizeP t2) (CtxSizeP t1)
    #ifdef UNSAFE_OPS
    plusCtxSizeAxiom :: forall {k} (t1 :: Ctx k) (t2 :: Ctx k) (f :: k -> Type).
    Assignment f t1
    -> Assignment f t2
    -> CtxSizeP (t1 <+> t2) :~: Plus (CtxSizeP t2) (CtxSizeP t1)
    plusCtxSizeAxiom Assignment f t1
    _t1 Assignment f t2
    _t2 = CtxSizeP (t1 <+> t2) :~: Plus (CtxSizeP t2) (CtxSizeP t1)
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom
    #else
    plusCtxSizeAxiom t1 t2 =
      case viewAssign t2 of
        AssignEmpty -> Refl
        AssignExtend t2' _
          | Refl <- plusCtxSizeAxiom t1 t2' -> Refl
    #endif

    -- | Minus distributes over plus
    --
    minusPlusAxiom :: forall n t t'.
      PeanoRepr n -> PeanoRepr t -> PeanoRepr t' ->
      Minus n (Plus t' t) :~: Minus (Minus n t') t
    #ifdef UNSAFE_OPS
    minusPlusAxiom :: forall (n :: Peano) (t :: Peano) (t' :: Peano).
    PeanoRepr n
    -> PeanoRepr t
    -> PeanoRepr t'
    -> Minus n (Plus t' t) :~: Minus (Minus n t') t
    minusPlusAxiom PeanoRepr n
    _n PeanoRepr t
    _t PeanoRepr t'
    _t' = Minus n (Plus t' t) :~: Minus (Minus n t') t
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom
    #else
    minusPlusAxiom n t t' = case peanoView t' of
      ZRepr -> Refl
      SRepr t1' -> case peanoView n of
          ZRepr -> Refl
          SRepr n1 -> case minusPlusAxiom n1 t t1' of
            Refl -> Refl
    #endif

    -- | We can reshuffle minus with less than
    --
    ltMinusPlusAxiom :: forall n t t'.
      (Lt t (Minus n t') ~ 'True) =>
      PeanoRepr n -> PeanoRepr t -> PeanoRepr t' ->
      Lt (Plus t' t) n :~: 'True
    #ifdef UNSAFE_OPS
    ltMinusPlusAxiom :: forall (n :: Peano) (t :: Peano) (t' :: Peano).
    (Lt t (Minus n t') ~ 'True) =>
    PeanoRepr n
    -> PeanoRepr t -> PeanoRepr t' -> Lt (Plus t' t) n :~: 'True
    ltMinusPlusAxiom PeanoRepr n
    _n PeanoRepr t
    _t PeanoRepr t'
    _t' = Lt (Plus t' t) n :~: 'True
    Le (S (Plus t' t)) n :~: 'True
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom
    #else
    ltMinusPlusAxiom n t t' = case peanoView n of
      SRepr m -> case peanoView t' of
         ZRepr -> Refl
         SRepr t1' -> case ltMinusPlusAxiom m t t1' of
            Refl -> Refl
    #endif

    ------------------------------------------------------------------------
    --  LocalWords:  PeanoRepr runtime Peano unary