-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-unused-top-binds #-}
-- This is needed because `singletons-th` generates redundant constraints.
-- GHC may not throw the warning always, see #791.
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE DeriveLift #-}

-- | Type-nat utilities.
--
-- We take Peano numbers as base for operations because they make it
-- much easer to prove things to compiler. Their performance does not
-- seem to introduce a problem, because we use nats primarily along with
-- stack which is a linked list with similar performance characteristics.
--
-- Many of things we introduce here are covered in @type-natural@ package,
-- but unfortunatelly it does not work with GHC 8.6 at the moment of writing
-- this module. We use "Data.Vinyl" as source of Peano @Nat@ for now.
module Morley.Util.Peano
  ( -- * General
    Peano
  , pattern S
  , pattern Z
  , ToPeano
  , FromPeano
  , SingNat (SZ, SS)

  , peanoSing
  , peanoSing'
  , withPeanoSingI
  , withSomePeano

  -- * Utility type synonyms
  , IsoNatPeano
  , SingIPeano

  -- * Peano Arithmetic
  , type (>)
  , type (>=)
  , peanoSingDecrement
  , peanoSingAdd
  , Decrement
  , AddPeano
  , SubPeano
  , MinPeano
  , MaxPeano

  -- * Lists
  , Length
  , At
  , Drop
  , Take

    -- * Morley-specific utils
  , IsLongerThan
  , LongerThan
  , RequireLongerThan
  , IsLongerOrSameLength
  , LongerOrSameLength
  , RequireLongerOrSameLength

  -- * Length constraints 'Dict'ionaries
  , requireLongerThan
  , requireLongerOrSameLength

  -- * Length constraints 'Dict'ionaries
  , isGreaterThan
  , isGreaterEqualThan

  -- * Inductive proofs
  , additivity
  , associativity
  , minIdempotency
  , commutativity
  , transitivity
  , (|-)

  -- * Helpers
  , toNatural
  , someSingNat
  ) where

import Data.Constraint (Dict(..), (\\))
import Data.Singletons (Sing, SingI(..), SomeSing(..))
import Data.Type.Equality (gcastWith, type (:~:)(..))
import Data.Vinyl (Rec(..))
import Data.Vinyl.TypeLevel (Nat(..), RLength)
import GHC.TypeLits (ErrorMessage(..), TypeError)
import GHC.TypeNats (type (+), type (-))
import GHC.TypeNats qualified as GHC
import Language.Haskell.TH.Syntax (Lift)
import Unsafe.Coerce (unsafeCoerce)

import Morley.Util.Sing (genSingletonsType)
import Morley.Util.Type (FailUnless, MockableConstraint(..))

-- This is very obviously a false positive.
{-# ANN module ("HLint: ignore Use 'natVal' from Universum" :: Text) #-}
{-# ANN module ("HLint: ignore Use 'someNatVal' from Universum" :: Text) #-}

----------------------------------------------------------------------------
-- General
----------------------------------------------------------------------------

-- | A convenient alias.
--
-- We are going to use 'Peano' numbers for type-dependent logic and
-- normal 'Nat's in user API, need to distinguish them somehow.
type Peano = Nat

deriving stock instance Eq Nat
deriving stock instance Show Nat
deriving stock instance Generic Nat
deriving anyclass instance NFData Nat

$(genSingletonsType ''Nat)

deriving stock instance Show (SingNat (n :: Nat))
deriving stock instance Eq (SingNat (n :: Nat))
deriving stock instance Lift (SingNat (n :: Nat))
instance NFData (SingNat (n :: Nat)) where
  rnf :: SingNat n -> ()
rnf SingNat n
SZ = ()
  rnf (SS Sing n
n) = SingNat n -> ()
forall a. NFData a => a -> ()
rnf Sing n
SingNat n
n


-- | A constraint asserting that GHC's @Nat@ @n@ and @Peano@ @p@ are the same (up to an
-- isomorphism)
type IsoNatPeano (n :: GHC.Nat) (p :: Peano) = (n ~ FromPeano p, ToPeano n ~ p)

-- | A synonym for @SingI (ToPeano n)@. Essentially requires that we can construct a 'Peano'
-- singleton for a given 'Nat'
type SingIPeano (n :: GHC.Nat) = SingI (ToPeano n)

type family ToPeano (n :: GHC.Nat) :: Peano where
  ToPeano 0 = 'Z
  ToPeano a = 'S (ToPeano (a - 1))

type family FromPeano (n :: Peano) :: GHC.Nat where
  FromPeano 'Z = 0
  FromPeano ('S a) = 1 + FromPeano a

-- | Get the peano singleton for a given type-level nat literal.
--
-- >>> peanoSing @2
-- SS (SS SZ)
peanoSing :: forall (n :: GHC.Nat). SingIPeano n => SingNat (ToPeano n)
peanoSing :: forall (n :: Nat). SingIPeano n => SingNat (ToPeano n)
peanoSing = forall {k} (a :: k). SingI a => Sing a
forall (a :: Nat). SingI a => Sing a
sing @(ToPeano n)

-- | Same as 'peanoSing', but only requires 'KnownNat' instance.
--
-- Witnesses half the equivalence between @KnownNat n@ and @SingI (ToPeano n)@
peanoSing' :: forall (n :: GHC.Nat). KnownNat n => SingNat (ToPeano n)
peanoSing' :: forall (n :: Nat). KnownNat n => SingNat (ToPeano n)
peanoSing' = Natural -> SingNat (ToPeano n)
forall (m :: Nat). Natural -> SingNat m
go (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal @n Proxy n
forall {k} (t :: k). Proxy t
Proxy)
  where
  go :: forall m. Natural -> SingNat m
  go :: forall (m :: Nat). Natural -> SingNat m
go = \case
    Natural
0 -> ((Any :~: Any) -> m :~: 'Z
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: m :~: 'Z) (m :~: 'Z) -> ((m ~ 'Z) => SingNat m) -> SingNat m
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- SingNat 'Z
(m ~ 'Z) => SingNat m
SZ
    Natural
n -> ((Any :~: Any) -> m :~: 'S (Decrement m)
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: m :~: 'S (Decrement m)) (m :~: 'S (Decrement m))
-> ((m ~ 'S (Decrement m)) => SingNat (Decrement m) -> SingNat m)
-> SingNat (Decrement m)
-> SingNat m
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|-
      (m ~ 'S (Decrement m)) => SingNat (Decrement m) -> SingNat m
forall (n :: Nat). Sing n -> SingNat ('S n)
SS (SingNat (Decrement m) -> SingNat m)
-> SingNat (Decrement m) -> SingNat m
forall a b. (a -> b) -> a -> b
$ forall (m :: Nat). Natural -> SingNat m
go @(Decrement m) (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1)

-- | Run a computation requiring @SingI (ToPeano n)@ in a context which only has
-- @KnownNat n@. Mostly useful when used with 'SomeNat'
withPeanoSingI :: forall (n :: GHC.Nat) r. KnownNat n => (SingIPeano n => r) -> r
withPeanoSingI :: forall (n :: Nat) r. KnownNat n => (SingIPeano n => r) -> r
withPeanoSingI SingI (ToPeano n) => r
act = SingI (ToPeano n) => r
act (SingI (ToPeano n) => r) -> Dict (SingI (ToPeano n)) -> r
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: Nat). Natural -> Dict (SingI m)
go @(ToPeano n) (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal @n Proxy n
forall {k} (t :: k). Proxy t
Proxy)
  where
  go :: forall (m :: Peano). Natural -> Dict (SingI m)
  go :: forall (m :: Nat). Natural -> Dict (SingI m)
go = \case
    Natural
0 -> ((Any :~: Any) -> m :~: 'Z
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: m :~: 'Z) (m :~: 'Z) -> ((m ~ 'Z) => Dict (SingI m)) -> Dict (SingI m)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- (m ~ 'Z) => Dict (SingI m)
forall (a :: Constraint). a => Dict a
Dict
    Natural
n -> ((Any :~: Any) -> m :~: 'S (Decrement m)
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: m :~: 'S (Decrement m)) (m :~: 'S (Decrement m))
-> ((m ~ 'S (Decrement m)) => Dict (SingI m)) -> Dict (SingI m)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- (SingI (Decrement m) => Dict (SingI m)
forall (a :: Constraint). a => Dict a
Dict (SingI (Decrement m) => Dict (SingI m))
-> Dict (SingI (Decrement m)) -> Dict (SingI m)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: Nat). Natural -> Dict (SingI m)
go @(Decrement m) (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1))

-- | Lift a given term-level 'Natural' to the type level for a given computation. The computation is
-- expected to accept a 'Proxy' for the sake of convenience: it's easier to get at the type-level
-- natural with @ScopedTypeVariables@ when pattern-matching on the proxy, e.g.
--
-- > (x :: Natural) `withSomePeano` \(_ :: Proxy n) -> doSomeNatComputation @n
withSomePeano :: Natural -> (forall n. (KnownNat n, SingIPeano n) => Proxy n -> r) -> r
withSomePeano :: forall r.
Natural
-> (forall (n :: Nat). (KnownNat n, SingIPeano n) => Proxy n -> r)
-> r
withSomePeano Natural
n forall (n :: Nat). (KnownNat n, SingIPeano n) => Proxy n -> r
f = case Natural -> SomeNat
someNatVal Natural
n of
  SomeNat (Proxy n
pn :: Proxy n) -> forall (n :: Nat) r. KnownNat n => (SingIPeano n => r) -> r
withPeanoSingI @n ((SingIPeano n => r) -> r) -> (SingIPeano n => r) -> r
forall a b. (a -> b) -> a -> b
$ Proxy n -> r
forall (n :: Nat). (KnownNat n, SingIPeano n) => Proxy n -> r
f Proxy n
pn


----------------------------------------------------------------------------
-- Peano Arithmetic
----------------------------------------------------------------------------

type family Decrement (a :: Peano) :: Peano where
  Decrement 'Z = TypeError ('Text "Expected n > 0")
  Decrement ('S n) = n

-- | Utility to 'Decrement' a Peano 'Sing'leton.
--
-- Useful when dealing with the constraint
peanoSingDecrement :: Sing n -> Maybe (Sing (Decrement n))
peanoSingDecrement :: forall (n :: Nat). Sing n -> Maybe (Sing (Decrement n))
peanoSingDecrement = \case
  Sing n
SingNat n
SZ -> Maybe (Sing (Decrement n))
forall a. Maybe a
Nothing
  SS Sing n
n -> SingNat n -> Maybe (SingNat n)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sing n
SingNat n
n

-- | 'Peano' naturals comparisson
type family (>) (x :: Peano) (y :: Peano) :: Bool where
  'Z   > _    = 'False
  'S _ > 'Z   = 'True
  'S x > 'S y = x > y

-- | 'Peano' naturals comparisson
type family (>=) (x :: Peano) (y :: Peano) :: Bool where
  _      >= 'Z     = 'True
  'Z     >= _      = 'False
  ('S x) >= ('S y) = x >= y

-- | 'Peano' naturals addition
type family AddPeano (n :: Peano) (m :: Peano) :: Peano where
  AddPeano 'Z x = x
  AddPeano ('S x) y = 'S (AddPeano x y)

-- | 'Peano' naturals subtraction
type family SubPeano (n :: Peano) (m :: Peano) :: Peano where
  SubPeano 'Z ('S m) = TypeError ('Text "Subtracting " ':<>: 'ShowType (FromPeano ('S m))
    ':<>: 'Text " from zero")
  SubPeano n 'Z = n
  SubPeano ('S n) ('S m) = SubPeano n m

-- | Out of two 'Peano' naturals, return the smaller one
type family MinPeano (n :: Peano) (m :: Peano) :: Peano where
  MinPeano _ 'Z = 'Z
  MinPeano 'Z _ = 'Z
  MinPeano ('S n) ('S m) = 'S (MinPeano n m)

-- | Out of two 'Peano' naturals, return the larger one
type family MaxPeano (n :: Peano) (m :: Peano) :: Peano where
  MaxPeano n 'Z = n
  MaxPeano 'Z m = m
  MaxPeano ('S n) ('S m) = 'S (MaxPeano n m)

-- | Singleton addition
peanoSingAdd :: SingNat n -> SingNat m -> SingNat (AddPeano n m)
peanoSingAdd :: forall (n :: Nat) (m :: Nat).
SingNat n -> SingNat m -> SingNat (AddPeano n m)
peanoSingAdd (SS Sing n
n) (SS Sing n
m) = SingNat n -> SingNat n -> AddPeano n ('S n) :~: 'S (AddPeano n n)
forall (x :: Nat) (y :: Nat).
SingNat x -> SingNat y -> AddPeano x ('S y) :~: 'S (AddPeano x y)
associativity Sing n
SingNat n
n Sing n
SingNat n
m (AddPeano n ('S n) :~: 'S (AddPeano n n))
-> ((AddPeano n ('S n) ~ 'S (AddPeano n n)) =>
    SingNat ('S (AddPeano n n)) -> SingNat ('S (AddPeano n ('S n))))
-> SingNat ('S (AddPeano n n))
-> SingNat ('S (AddPeano n ('S n)))
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- (AddPeano n ('S n) ~ 'S (AddPeano n n)) =>
SingNat ('S (AddPeano n n)) -> SingNat ('S (AddPeano n ('S n)))
forall (n :: Nat). Sing n -> SingNat ('S n)
SS (SingNat ('S (AddPeano n n)) -> SingNat ('S (AddPeano n ('S n))))
-> SingNat ('S (AddPeano n n)) -> SingNat ('S (AddPeano n ('S n)))
forall a b. (a -> b) -> a -> b
$ Sing (AddPeano n n) -> SingNat ('S (AddPeano n n))
forall (n :: Nat). Sing n -> SingNat ('S n)
SS (Sing (AddPeano n n) -> SingNat ('S (AddPeano n n)))
-> Sing (AddPeano n n) -> SingNat ('S (AddPeano n n))
forall a b. (a -> b) -> a -> b
$ SingNat n -> SingNat n -> SingNat (AddPeano n n)
forall (n :: Nat) (m :: Nat).
SingNat n -> SingNat m -> SingNat (AddPeano n m)
peanoSingAdd Sing n
SingNat n
n Sing n
SingNat n
m
peanoSingAdd SingNat n
SZ SingNat m
m = SingNat m
SingNat (AddPeano n m)
m
peanoSingAdd SingNat n
n SingNat m
SZ = SingNat n -> SingNat 'Z -> AddPeano n 'Z :~: AddPeano 'Z n
forall (x :: Nat) (y :: Nat).
SingNat x -> SingNat y -> AddPeano x y :~: AddPeano y x
commutativity SingNat n
n SingNat 'Z
SZ (AddPeano n 'Z :~: n)
-> ((AddPeano n 'Z ~ n) => SingNat (AddPeano n 'Z))
-> SingNat (AddPeano n 'Z)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- SingNat n
(AddPeano n 'Z ~ n) => SingNat (AddPeano n 'Z)
n

----------------------------------------------------------------------------
-- Lists
----------------------------------------------------------------------------

type family Length l :: Peano where
  Length l = RLength l

type family At (n :: Peano) s where
  At 'Z (x ': _) = x
  At ('S n) (_ ': xs) = At n xs
  At a '[] =
    TypeError
      ('Text "You tried to access a non-existing element of the stack, n = " ':<>:
         'ShowType (FromPeano a))

type family Drop (n :: Peano) (s :: [k]) :: [k] where
  Drop  'Z s = s
  Drop ('S _) '[] = '[]
  Drop ('S n) (_ ': s) = Drop n s

type family Take (n :: Peano) (s :: [k]) :: [k] where
  Take  'Z _ = '[]
  Take _ '[] = '[]
  Take ('S n) (a ': s) = a ': Take n s

----------------------------------------------------------------------------
-- Morley-specific utils
----------------------------------------------------------------------------

-- Note that we could define type families to return 'Constraint' instead
-- of defining standalone constraint in form `c ~ 'True`, but apparently
-- such constraint would be weaker, e. g. there is an example when with
-- current approach there is no warning, but if we change the approach
-- to return 'Constraint' from type family then GHC complains about
-- non-exhaustive patterns (@gromak).
-- Also we use these `Bool` type families in more than one place, we generate
-- two constraints: one gives more information to GHC and another one produces
-- better error messages on failure.

-- | Comparison of type-level naturals, as a function.
--
-- It is as lazy on the list argument as possible - there is no
-- need to know the whole list if the natural argument is small enough.
-- This property is important if we want to be able to extract reusable
-- parts of code which are aware only of relevant part of stack.
type family IsLongerThan (l :: [k]) (a :: Peano) :: Bool where
  IsLongerThan (_ ': _) 'Z = 'True
  IsLongerThan (_ ': xs) ('S a) = IsLongerThan xs a
  IsLongerThan '[] _ = 'False

-- | Comparison of type-level naturals, as a constraint.
type LongerThan l a = IsLongerThan l a ~ 'True

-- | Similar to 'IsLongerThan', but returns 'True' when list length
-- equals to the passed number.
type family IsLongerOrSameLength (l :: [k]) (a :: Peano) :: Bool where
  IsLongerOrSameLength _ 'Z = 'True
  IsLongerOrSameLength (_ ': xs) ('S a) = IsLongerOrSameLength xs a
  IsLongerOrSameLength '[] ('S _) = 'False

-- | 'IsLongerOrSameLength' in form of constraint that gives most
-- information to GHC.
type LongerOrSameLength l a = IsLongerOrSameLength l a ~ 'True

{- | Evaluates list length.

This type family is a best-effort attempt to display neat error messages
when list is known only partially.

For instance, when called on @Int ': Int ': s@, the result will be
@OfLengthWithTail 2 s@ - compare with result of simple 'Length' -
@1 + 1 + Length s@.

For concrete types this will be identical to calling @FromPeano (Length l)@.
-}
type family OfLengthWithTail (acc :: GHC.Nat) (l :: [k]) :: GHC.Nat where
  OfLengthWithTail a '[] = a
  OfLengthWithTail a (_ ': xs) = OfLengthWithTail (a + 1) xs

type LengthWithTail l = OfLengthWithTail 0 l

-- | Comparison of type-level naturals, raises human-readable compile error
-- when does not hold.
--
-- Here we use the same approach as for 'RequireLongerOrSameLength', this
-- type family is internal.
type family RequireLongerThan' (l :: [k]) (a :: Nat) :: Constraint where
  RequireLongerThan' l a =
    FailUnless
      (IsLongerThan l a)
      ('Text "Stack element #" ':<>: 'ShowType (FromPeano a) ':<>:
       'Text " is not accessible" ':$$:
       'Text "Current stack has size of only " ':<>:
       'ShowType (LengthWithTail l) ':<>:
       'Text ":" ':$$: 'ShowType l
       )

class (RequireLongerThan' l a, LongerThan l a) =>
  RequireLongerThan (l :: [k]) (a :: Peano)
instance (RequireLongerThan' l a, LongerThan l a) =>
  RequireLongerThan l a

-- | 'IsLongerOrSameLength' in form of constraint that produces
-- good error message. Should be used together with 'LongerThan'
-- because 'LongerThan' gives GHC more information.
-- We use it in combination, so that it gives enough information to
-- GHC and also producess good error messages.
type family RequireLongerOrSameLength' (l :: [k]) (a :: Peano) :: Constraint where
  RequireLongerOrSameLength' l a =
    FailUnless
      (IsLongerOrSameLength l a)
      ('Text "Expected stack with length >= " ':<>: 'ShowType (FromPeano a) ':$$:
       'Text "Current stack has size of only " ':<>:
       'ShowType (LengthWithTail l) ':<>:
       'Text ":" ':$$: 'ShowType l
       )

-- | We can have
-- `RequireLongerOrSameLength = (RequireLongerOrSameLength' l a, LongerOrSameLength l a)`,
-- but apparently the printed error message can be caused by `LongerOrSameLength`
-- rather than `RequireLongerOrSameLength'`.
-- We do not know for sure how it all works, but we think that if we require constraint X before
-- Y (using multiple `=>`s) then X will always be evaluated first.
class (RequireLongerOrSameLength' l a, LongerOrSameLength l a) =>
  RequireLongerOrSameLength (l :: [k]) (a :: Peano)
instance (RequireLongerOrSameLength' l a, LongerOrSameLength l a) =>
  RequireLongerOrSameLength l a

instance MockableConstraint (RequireLongerOrSameLength l a) where
  unsafeProvideConstraint :: Dict (RequireLongerOrSameLength l a)
unsafeProvideConstraint = Dict (RequireLongerOrSameLength '[] 'Z)
-> Dict (RequireLongerOrSameLength l a)
forall a b. a -> b
unsafeCoerce (Dict (RequireLongerOrSameLength '[] 'Z)
 -> Dict (RequireLongerOrSameLength l a))
-> Dict (RequireLongerOrSameLength '[] 'Z)
-> Dict (RequireLongerOrSameLength l a)
forall a b. (a -> b) -> a -> b
$ forall (a :: Constraint). a => Dict a
Dict @(RequireLongerOrSameLength '[] 'Z)

instance MockableConstraint (RequireLongerThan l a) where
  unsafeProvideConstraint :: Dict (RequireLongerThan l a)
unsafeProvideConstraint = Dict (RequireLongerThan '[()] 'Z) -> Dict (RequireLongerThan l a)
forall a b. a -> b
unsafeCoerce (Dict (RequireLongerThan '[()] 'Z) -> Dict (RequireLongerThan l a))
-> Dict (RequireLongerThan '[()] 'Z)
-> Dict (RequireLongerThan l a)
forall a b. (a -> b) -> a -> b
$ forall (a :: Constraint). a => Dict a
Dict @(RequireLongerThan '[()] 'Z)

----------------------------------------------------------------------------
-- Length constraints 'Dict'ionaries
----------------------------------------------------------------------------

requireLongerThan
  :: Rec any stk
  -> Sing n
  -> Maybe (Dict (RequireLongerThan stk n))
requireLongerThan :: forall {k} (any :: k -> *) (stk :: [k]) (n :: Nat).
Rec any stk -> Sing n -> Maybe (Dict (RequireLongerThan stk n))
requireLongerThan Rec any stk
RNil Sing n
_           = Maybe (Dict (RequireLongerThan stk n))
forall a. Maybe a
Nothing
requireLongerThan (any r
_ :& Rec any rs
_xs) Sing n
SingNat n
SZ    = Dict (RequireLongerThan stk n)
-> Maybe (Dict (RequireLongerThan stk n))
forall a. a -> Maybe a
Just Dict (RequireLongerThan stk n)
forall (a :: Constraint). a => Dict a
Dict
requireLongerThan (any r
_ :& Rec any rs
xs) (SS Sing n
n) = do
  Dict (RequireLongerThan rs n)
Dict <- Rec any rs -> Sing n -> Maybe (Dict (RequireLongerThan rs n))
forall {k} (any :: k -> *) (stk :: [k]) (n :: Nat).
Rec any stk -> Sing n -> Maybe (Dict (RequireLongerThan stk n))
requireLongerThan Rec any rs
xs Sing n
n
  Dict (RequireLongerThan stk n)
-> Maybe (Dict (RequireLongerThan stk n))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (RequireLongerThan stk n)
forall (a :: Constraint). a => Dict a
Dict

requireLongerOrSameLength
  :: Rec any stk
  -> Sing n
  -> Maybe (Dict (RequireLongerOrSameLength stk n))
requireLongerOrSameLength :: forall {k} (any :: k -> *) (stk :: [k]) (n :: Nat).
Rec any stk
-> Sing n -> Maybe (Dict (RequireLongerOrSameLength stk n))
requireLongerOrSameLength Rec any stk
_ Sing n
SingNat n
SZ             = Dict (RequireLongerOrSameLength stk n)
-> Maybe (Dict (RequireLongerOrSameLength stk n))
forall a. a -> Maybe a
Just Dict (RequireLongerOrSameLength stk n)
forall (a :: Constraint). a => Dict a
Dict
requireLongerOrSameLength Rec any stk
RNil (SS Sing n
_)      = Maybe (Dict (RequireLongerOrSameLength stk n))
forall a. Maybe a
Nothing
requireLongerOrSameLength (any r
_ :& Rec any rs
xs) (SS Sing n
n) = do
  Dict (RequireLongerOrSameLength rs n)
Dict <- Rec any rs
-> Sing n -> Maybe (Dict (RequireLongerOrSameLength rs n))
forall {k} (any :: k -> *) (stk :: [k]) (n :: Nat).
Rec any stk
-> Sing n -> Maybe (Dict (RequireLongerOrSameLength stk n))
requireLongerOrSameLength Rec any rs
xs Sing n
n
  Dict (RequireLongerOrSameLength stk n)
-> Maybe (Dict (RequireLongerOrSameLength stk n))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (RequireLongerOrSameLength stk n)
forall (a :: Constraint). a => Dict a
Dict

----------------------------------------------------------------------------
-- Arith constraints 'Dict'ionaries
----------------------------------------------------------------------------

isGreaterThan
  :: Sing a -> Sing b
  -> Maybe (Dict ((a > b) ~ 'True))
isGreaterThan :: forall (a :: Nat) (b :: Nat).
Sing a -> Sing b -> Maybe (Dict ((a > b) ~ 'True))
isGreaterThan Sing a
SingNat a
SZ Sing b
_          = Maybe (Dict ((a > b) ~ 'True))
forall a. Maybe a
Nothing
isGreaterThan (SS Sing n
_) Sing b
SingNat b
SZ     = Dict ('True ~ 'True) -> Maybe (Dict ('True ~ 'True))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict ('True ~ 'True)
forall (a :: Constraint). a => Dict a
Dict
isGreaterThan (SS Sing n
a) (SS Sing n
b) = Sing n -> Sing n -> Maybe (Dict ((n > n) ~ 'True))
forall (a :: Nat) (b :: Nat).
Sing a -> Sing b -> Maybe (Dict ((a > b) ~ 'True))
isGreaterThan Sing n
a Sing n
b

isGreaterEqualThan
  :: Sing a -> Sing b
  -> Maybe (Dict ((a >= b) ~ 'True))
isGreaterEqualThan :: forall (a :: Nat) (b :: Nat).
Sing a -> Sing b -> Maybe (Dict ((a >= b) ~ 'True))
isGreaterEqualThan Sing a
_ Sing b
SingNat b
SZ          = Dict ('True ~ 'True) -> Maybe (Dict ('True ~ 'True))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Dict ('True ~ 'True)
forall (a :: Constraint). a => Dict a
Dict
isGreaterEqualThan Sing a
SingNat a
SZ Sing b
_          = Maybe (Dict ((a >= b) ~ 'True))
forall a. Maybe a
Nothing
isGreaterEqualThan (SS Sing n
a) (SS Sing n
b) = Sing n -> Sing n -> Maybe (Dict ((n >= n) ~ 'True))
forall (a :: Nat) (b :: Nat).
Sing a -> Sing b -> Maybe (Dict ((a >= b) ~ 'True))
isGreaterEqualThan Sing n
a Sing n
b

----------------------------------------------------------------------------
-- Inductive proofs
----------------------------------------------------------------------------

-- | Convenience synonym for 'gcastWith'
(|-) :: forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- :: forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
(|-) = (a :~: b) -> ((a ~ b) => r) -> r
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith
infixr 1 |-

-- | Proof that for naturals, @k + (m + 1) = n@ entails @n > k@
{-# RULES "additivity" forall k m n. additivity k m n = unsafeCoerce Refl #-}
{-# INLINE[1] additivity #-}
additivity :: forall k m n. AddPeano k ('S m) ~ n
           => SingNat m -> SingNat n -> SingNat k -> n > k :~: 'True
additivity :: forall (k :: Nat) (m :: Nat) (n :: Nat).
(AddPeano k ('S m) ~ n) =>
SingNat m -> SingNat n -> SingNat k -> (n > k) :~: 'True
additivity SingNat m
_ (SS Sing n
_) SingNat k
SZ = (n > k) :~: 'True
forall {k} (a :: k). a :~: a
Refl
additivity SingNat m
m (SS Sing n
_) SingNat k
k = SingNat k -> SingNat m -> AddPeano k ('S m) :~: 'S (AddPeano k m)
forall (x :: Nat) (y :: Nat).
SingNat x -> SingNat y -> AddPeano x ('S y) :~: 'S (AddPeano x y)
associativity SingNat k
k SingNat m
m ('S n :~: 'S (AddPeano k m))
-> (('S n ~ 'S (AddPeano k m)) => ('S n > k) :~: 'True)
-> ('S n > k) :~: 'True
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- forall (k' :: Nat) (m' :: Nat).
SingNat k' -> ('S (AddPeano k' m') > k') :~: 'True
lemma2 @_ @m SingNat k
k (('S n > k) :~: 'True)
-> ((('S n > k) ~ 'True) => ('S n > k) :~: 'True)
-> ('S n > k) :~: 'True
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- SingNat k -> ('S k > k) :~: 'True
forall (k' :: Nat). SingNat k' -> ('S k' > k') :~: 'True
lemma SingNat k
k (('S k > k) :~: 'True)
-> ((('S k > k) ~ 'True) => ('S n > k) :~: 'True)
-> ('S n > k) :~: 'True
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- (('S k > k) ~ 'True) => ('S n > k) :~: 'True
forall {k} (a :: k). a :~: a
Refl
  where

  lemma2 :: forall k' m'. SingNat k' -> 'S (AddPeano k' m') > k' :~: 'True
  lemma2 :: forall (k' :: Nat) (m' :: Nat).
SingNat k' -> ('S (AddPeano k' m') > k') :~: 'True
lemma2 SingNat k'
SZ = ('S (AddPeano k' m') > k') :~: 'True
forall {k} (a :: k). a :~: a
Refl
  lemma2 (SS Sing n
k') = forall (k' :: Nat) (m' :: Nat).
SingNat k' -> ('S (AddPeano k' m') > k') :~: 'True
lemma2 @_ @m' Sing n
SingNat n
k' (('S (AddPeano n m') > n) :~: 'True)
-> ((('S (AddPeano n m') > n) ~ 'True) =>
    ('S (AddPeano n m') > n) :~: 'True)
-> ('S (AddPeano n m') > n) :~: 'True
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- (('S (AddPeano n m') > n) ~ 'True) =>
('S (AddPeano n m') > n) :~: 'True
forall {k} (a :: k). a :~: a
Refl

  lemma :: SingNat k' -> 'S k' > k' :~: 'True
  lemma :: forall (k' :: Nat). SingNat k' -> ('S k' > k') :~: 'True
lemma SingNat k'
SZ = ('S k' > k') :~: 'True
forall {k} (a :: k). a :~: a
Refl
  lemma (SS Sing n
n) = SingNat n -> ('S n > n) :~: 'True
forall (k' :: Nat). SingNat k' -> ('S k' > k') :~: 'True
lemma Sing n
SingNat n
n (('S n > n) :~: 'True)
-> ((('S n > n) ~ 'True) => ('S n > n) :~: 'True)
-> ('S n > n) :~: 'True
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- (('S n > n) ~ 'True) => ('S n > n) :~: 'True
forall {k} (a :: k). a :~: a
Refl

-- | Proof that for naturals, @x + (y + 1) = (x + y) + 1@
{-# RULES "associativity" forall x y. associativity x y = unsafeCoerce Refl #-}
{-# INLINE[1] associativity #-}
associativity :: SingNat x -> SingNat y -> AddPeano x ('S y) :~: 'S (AddPeano x y)
associativity :: forall (x :: Nat) (y :: Nat).
SingNat x -> SingNat y -> AddPeano x ('S y) :~: 'S (AddPeano x y)
associativity SingNat x
SZ SingNat y
_ = AddPeano x ('S y) :~: 'S (AddPeano x y)
forall {k} (a :: k). a :~: a
Refl
associativity (SS Sing n
x) SingNat y
y = SingNat n -> SingNat y -> AddPeano n ('S y) :~: 'S (AddPeano n y)
forall (x :: Nat) (y :: Nat).
SingNat x -> SingNat y -> AddPeano x ('S y) :~: 'S (AddPeano x y)
associativity Sing n
SingNat n
x SingNat y
y (AddPeano n ('S y) :~: 'S (AddPeano n y))
-> ((AddPeano n ('S y) ~ 'S (AddPeano n y)) =>
    'S (AddPeano n ('S y)) :~: 'S ('S (AddPeano n y)))
-> 'S (AddPeano n ('S y)) :~: 'S ('S (AddPeano n y))
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- (AddPeano n ('S y) ~ 'S (AddPeano n y)) =>
'S (AddPeano n ('S y)) :~: 'S ('S (AddPeano n y))
forall {k} (a :: k). a :~: a
Refl

-- | Proof that @x + y = y + x@
{-# RULES "commutativity" forall x y. commutativity x y = unsafeCoerce Refl #-}
{-# INLINE[1] commutativity #-}
commutativity :: SingNat x -> SingNat y -> AddPeano x y :~: AddPeano y x
commutativity :: forall (x :: Nat) (y :: Nat).
SingNat x -> SingNat y -> AddPeano x y :~: AddPeano y x
commutativity SingNat x
SZ SingNat y
SZ = AddPeano x y :~: AddPeano y x
forall {k} (a :: k). a :~: a
Refl
commutativity SingNat x
SZ (SS Sing n
y) = SingNat 'Z -> SingNat n -> AddPeano 'Z n :~: AddPeano n 'Z
forall (x :: Nat) (y :: Nat).
SingNat x -> SingNat y -> AddPeano x y :~: AddPeano y x
commutativity SingNat 'Z
SZ Sing n
SingNat n
y (n :~: AddPeano n 'Z)
-> ((n ~ AddPeano n 'Z) => 'S n :~: 'S (AddPeano n 'Z))
-> 'S n :~: 'S (AddPeano n 'Z)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- (n ~ AddPeano n 'Z) => 'S n :~: 'S (AddPeano n 'Z)
forall {k} (a :: k). a :~: a
Refl
commutativity (SS Sing n
x) SingNat y
y = SingNat n -> SingNat y -> AddPeano n y :~: AddPeano y n
forall (x :: Nat) (y :: Nat).
SingNat x -> SingNat y -> AddPeano x y :~: AddPeano y x
commutativity Sing n
SingNat n
x SingNat y
y (AddPeano n y :~: AddPeano y n)
-> ((AddPeano n y ~ AddPeano y n) =>
    'S (AddPeano n y) :~: AddPeano y ('S n))
-> 'S (AddPeano n y) :~: AddPeano y ('S n)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- SingNat y -> SingNat n -> AddPeano y ('S n) :~: 'S (AddPeano y n)
forall (x :: Nat) (y :: Nat).
SingNat x -> SingNat y -> AddPeano x ('S y) :~: 'S (AddPeano x y)
associativity SingNat y
y Sing n
SingNat n
x (AddPeano y ('S n) :~: 'S (AddPeano y n))
-> ((AddPeano y ('S n) ~ 'S (AddPeano y n)) =>
    'S (AddPeano n y) :~: AddPeano y ('S n))
-> 'S (AddPeano n y) :~: AddPeano y ('S n)
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- (AddPeano y ('S n) ~ 'S (AddPeano y n)) =>
'S (AddPeano n y) :~: AddPeano y ('S n)
forall {k} (a :: k). a :~: a
Refl

-- | Proof that for naturals, @min(n, n) = n@
{-# RULES "minIdempotency" forall x. minIdempotency x = unsafeCoerce Refl #-}
{-# INLINE[1] minIdempotency #-}
minIdempotency :: SingNat n -> MinPeano n n :~: n
minIdempotency :: forall (n :: Nat). SingNat n -> MinPeano n n :~: n
minIdempotency SingNat n
SZ = MinPeano n n :~: n
forall {k} (a :: k). a :~: a
Refl
minIdempotency (SS Sing n
n) = SingNat n -> MinPeano n n :~: n
forall (n :: Nat). SingNat n -> MinPeano n n :~: n
minIdempotency Sing n
SingNat n
n (MinPeano n n :~: n)
-> ((MinPeano n n ~ n) => 'S (MinPeano n n) :~: 'S n)
-> 'S (MinPeano n n) :~: 'S n
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- (MinPeano n n ~ n) => 'S (MinPeano n n) :~: 'S n
forall {k} (a :: k). a :~: a
Refl

-- | Proof that for naturals, @x >= y > z@ implies @x > z@
{-# RULES "transitivity" forall x y z. transitivity x y z = unsafeCoerce Refl #-}
{-# INLINE[1] transitivity #-}
transitivity :: (x >= y ~ 'True, y > z ~ 'True)
             => SingNat x -> SingNat y -> SingNat z -> x > z :~: 'True
transitivity :: forall (x :: Nat) (y :: Nat) (z :: Nat).
((x >= y) ~ 'True, (y > z) ~ 'True) =>
SingNat x -> SingNat y -> SingNat z -> (x > z) :~: 'True
transitivity (SS Sing n
_) (SS Sing n
_) SingNat z
SZ = (x > z) :~: 'True
forall {k} (a :: k). a :~: a
Refl
transitivity (SS Sing n
x) (SS Sing n
y) (SS Sing n
z) = SingNat n -> SingNat n -> SingNat n -> (n > n) :~: 'True
forall (x :: Nat) (y :: Nat) (z :: Nat).
((x >= y) ~ 'True, (y > z) ~ 'True) =>
SingNat x -> SingNat y -> SingNat z -> (x > z) :~: 'True
transitivity Sing n
SingNat n
x Sing n
SingNat n
y Sing n
SingNat n
z ((n > n) :~: 'True)
-> (((n > n) ~ 'True) => (n > n) :~: 'True) -> (n > n) :~: 'True
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
|- ((n > n) ~ 'True) => (n > n) :~: 'True
forall {k} (a :: k). a :~: a
Refl

----------------------------------------------------------------------------
-- Helpers
----------------------------------------------------------------------------

toNatural :: Peano -> Natural
toNatural :: Nat -> Natural
toNatural Nat
Z = Natural
0
toNatural (S Nat
x) = Natural
1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Nat -> Natural
toNatural Nat
x

someSingNat :: Natural -> SomeSing Peano
someSingNat :: Natural -> SomeSing Nat
someSingNat Natural
0 = Sing 'Z -> SomeSing Nat
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing 'Z
SingNat 'Z
SZ
someSingNat Natural
n = case Natural -> SomeSing Nat
someSingNat (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1) of
  SomeSing Sing a
sn -> Sing ('S a) -> SomeSing Nat
forall k (a :: k). Sing a -> SomeSing k
SomeSing (Sing a -> SingNat ('S a)
forall (n :: Nat). Sing n -> SingNat ('S n)
SS Sing a
sn)