{-|
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 forall a. Eq a => a -> a -> Bool
== Word64
0
  then forall a b. a -> b
unsafeCoerce PeanoView Z
ZRepr
  else forall a b. a -> b
unsafeCoerce (forall (n :: Peano). PeanoRepr n -> PeanoView (S n)
SRepr (forall (n :: Peano). Word64 -> PeanoRepr n
PeanoRepr (Word64
iforall 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     = forall (n :: Peano). Word64 -> PeanoRepr n
PeanoRepr Word64
0
viewRepr (SRepr PeanoRepr n
n) = forall (n :: Peano). Word64 -> PeanoRepr n
PeanoRepr (forall (n :: Peano). PeanoRepr n -> Word64
peanoValue PeanoRepr n
n 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 = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
i (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 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 forall a. Eq a => a -> a -> Bool
== Word64
n = forall a. a -> Maybe a
Just forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom
    | Bool
otherwise = 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 forall a. Eq a => a -> a -> Bool
== Word64
n    = forall a b. a -> Either a b
Left forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom
    | Bool
otherwise = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$
        \a :~: b
x -> seq :: forall a b. a -> b -> b
seq a :~: b
x forall a b. (a -> b) -> a -> b
$ 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 forall a. Ord a => a -> a -> Bool
< Word64
n     = forall a b. a -> b
unsafeCoerce forall {k} (x :: k) (y :: k). OrderingF x y
LTF
    | Word64
m forall a. Eq a => a -> a -> Bool
== Word64
n    = forall a b. a -> b
unsafeCoerce forall {k} (x :: k). OrderingF x x
EQF
    | Bool
otherwise = forall a b. a -> b
unsafeCoerce 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 -> forall {k} (a :: k). a :~: a
Refl) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f 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 = forall a. Show a => a -> [Char]
show (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 = 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 = 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 = forall (n :: Peano). PeanoView n -> PeanoRepr n
viewRepr (forall (n :: Peano). PeanoRepr n -> PeanoView (S n)
SRepr 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 = 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) = forall (n :: Peano). Word64 -> PeanoRepr n
PeanoRepr (Word64
iforall 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) = forall (n :: Peano). Word64 -> PeanoRepr n
PeanoRepr (Word64
iforall 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) = forall (n :: Peano). Word64 -> PeanoRepr n
PeanoRepr (Word64
a 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) = forall (n :: Peano). Word64 -> PeanoRepr n
PeanoRepr (Word64
a 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) = forall (n :: Peano). Word64 -> PeanoRepr n
PeanoRepr (Word64
a 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) = forall (n :: Peano). Word64 -> PeanoRepr n
PeanoRepr (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) = forall (n :: Peano). Word64 -> PeanoRepr n
PeanoRepr (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 forall a. Ord a => a -> a -> Bool
<= Word64
b then forall a b. a -> b
unsafeCoerce (BoolRepr 'True
TrueRepr)
            else 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 = forall (a :: Peano) (b :: Peano).
PeanoRepr a -> PeanoRepr b -> BoolRepr (Le a b)
leP (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 = 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 = 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 forall (n :: Peano). PeanoRepr n -> PeanoView n
peanoView PeanoRepr m
n of
  PeanoView m
ZRepr   -> repr s
s
  SRepr PeanoRepr n
m -> forall (a :: k). repr a -> repr (f a)
f (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 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 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 Z
zeroP
  AssignExtend Assignment f ctx
a f tp
_ -> forall (n :: Peano). PeanoRepr n -> PeanoRepr (S n)
succP (forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> PeanoRepr (CtxSizeP ctx)
ctxSizeP Assignment f ctx
a)

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

-- | Convert a 'Word64' to a 'PeanoRepr'
mkPeanoRepr :: Word64 -> Some PeanoRepr
#ifdef UNSAFE_OPS
mkPeanoRepr :: Word64 -> Some PeanoRepr
mkPeanoRepr Word64
n = forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (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 forall a. Ord a => a -> a -> Bool
>= a
0 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Some PeanoRepr
mkPeanoRepr forall a b. (a -> b) -> a -> b
$! forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x
somePeano a
_ = 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 = forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (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 = forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (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 [] = forall k (f :: k -> Type) (x :: k). f x -> Some f
Some PeanoRepr Z
zeroP
peanoLength (a
_:[a]
xs) = case forall a. [a] -> Some PeanoRepr
peanoLength [a]
xs of
  Some PeanoRepr x
n -> forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (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 = 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' = 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' = 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