module Data.Type.Witness.Specific.PeanoNat where import Data.PeanoNat import Data.Type.Witness.General.Order import Data.Type.Witness.General.Representative import Data.Type.Witness.General.WitnessValue import Import type PeanoNatType :: PeanoNat -> Type data PeanoNatType t where ZeroType :: PeanoNatType 'Zero SuccType :: PeanoNatType t -> PeanoNatType ('Succ t) instance TestEquality PeanoNatType where testEquality :: forall (a :: PeanoNat) (b :: PeanoNat). PeanoNatType a -> PeanoNatType b -> Maybe (a :~: b) testEquality PeanoNatType a ZeroType PeanoNatType b ZeroType = forall (m :: Type -> Type) a. Monad m => a -> m a return forall {k} (a :: k). a :~: a Refl testEquality (SuccType PeanoNatType t a) (SuccType PeanoNatType t b) = do t :~: t Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b) testEquality PeanoNatType t a PeanoNatType t b forall (m :: Type -> Type) a. Monad m => a -> m a return forall {k} (a :: k). a :~: a Refl testEquality PeanoNatType a _ PeanoNatType b _ = forall a. Maybe a Nothing instance TestOrder PeanoNatType where testCompare :: forall (a :: PeanoNat) (b :: PeanoNat). PeanoNatType a -> PeanoNatType b -> WOrdering a b testCompare PeanoNatType a ZeroType PeanoNatType b ZeroType = forall k (a :: k). WOrdering a a WEQ testCompare (SuccType PeanoNatType t a) (SuccType PeanoNatType t b) = case forall k (w :: k -> Type) (a :: k) (b :: k). TestOrder w => w a -> w b -> WOrdering a b testCompare PeanoNatType t a PeanoNatType t b of WOrdering t t WLT -> forall k (a :: k) (b :: k). WOrdering a b WLT WOrdering t t WGT -> forall k (a :: k) (b :: k). WOrdering a b WGT WOrdering t t WEQ -> forall k (a :: k). WOrdering a a WEQ testCompare (SuccType PeanoNatType t _) PeanoNatType b ZeroType = forall k (a :: k) (b :: k). WOrdering a b WGT testCompare PeanoNatType a ZeroType (SuccType PeanoNatType t _) = forall k (a :: k) (b :: k). WOrdering a b WLT instance Representative PeanoNatType where getRepWitness :: Subrepresentative PeanoNatType PeanoNatType getRepWitness PeanoNatType a ZeroType = forall (a :: Constraint). a => Dict a Dict getRepWitness (SuccType PeanoNatType t n) = case forall k (rep :: k -> Type). Representative rep => Subrepresentative rep rep getRepWitness PeanoNatType t n of Dict (Is PeanoNatType t) Dict -> forall (a :: Constraint). a => Dict a Dict instance Is PeanoNatType 'Zero where representative :: PeanoNatType 'Zero representative = PeanoNatType 'Zero ZeroType instance Is PeanoNatType n => Is PeanoNatType ('Succ n) where representative :: PeanoNatType ('Succ n) representative = forall (a :: PeanoNat). PeanoNatType a -> PeanoNatType ('Succ a) SuccType forall k (rep :: k -> Type) (a :: k). Is rep a => rep a representative instance WitnessValue PeanoNatType where type WitnessValueType PeanoNatType = PeanoNat witnessToValue :: forall t. PeanoNatType t -> PeanoNat witnessToValue :: forall (t :: PeanoNat). PeanoNatType t -> PeanoNat witnessToValue PeanoNatType t ZeroType = PeanoNat Zero witnessToValue (SuccType PeanoNatType t n) = PeanoNat -> PeanoNat Succ forall a b. (a -> b) -> a -> b $ forall k (w :: k -> Type) (t :: k). WitnessValue w => w t -> WitnessValueType w witnessToValue PeanoNatType t n valueToWitness :: forall r. WitnessValueType PeanoNatType -> (forall (t :: PeanoNat). PeanoNatType t -> r) -> r valueToWitness WitnessValueType PeanoNatType PeanoNat Zero forall (t :: PeanoNat). PeanoNatType t -> r cont = forall (t :: PeanoNat). PeanoNatType t -> r cont PeanoNatType 'Zero ZeroType valueToWitness (Succ PeanoNat n) forall (t :: PeanoNat). PeanoNatType t -> r cont = forall k (w :: k -> Type) r. WitnessValue w => WitnessValueType w -> (forall (t :: k). w t -> r) -> r valueToWitness PeanoNat n forall a b. (a -> b) -> a -> b $ \PeanoNatType t t -> forall (t :: PeanoNat). PeanoNatType t -> r cont forall a b. (a -> b) -> a -> b $ forall (a :: PeanoNat). PeanoNatType a -> PeanoNatType ('Succ a) SuccType PeanoNatType t t type GreaterEqual :: PeanoNat -> PeanoNat -> Type data GreaterEqual a b where ZeroGreaterEqual :: GreaterEqual a 'Zero SuccGreaterEqual :: GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b) greaterEqualIndex :: GreaterEqual a b -> PeanoNatType b greaterEqualIndex :: forall (a :: PeanoNat) (b :: PeanoNat). GreaterEqual a b -> PeanoNatType b greaterEqualIndex GreaterEqual a b ZeroGreaterEqual = PeanoNatType 'Zero ZeroType greaterEqualIndex (SuccGreaterEqual GreaterEqual a b n) = forall (a :: PeanoNat). PeanoNatType a -> PeanoNatType ('Succ a) SuccType forall a b. (a -> b) -> a -> b $ forall (a :: PeanoNat) (b :: PeanoNat). GreaterEqual a b -> PeanoNatType b greaterEqualIndex GreaterEqual a b n samePeanoGreaterEqual :: PeanoNatType a -> GreaterEqual a a samePeanoGreaterEqual :: forall (a :: PeanoNat). PeanoNatType a -> GreaterEqual a a samePeanoGreaterEqual PeanoNatType a ZeroType = forall (a :: PeanoNat). GreaterEqual a 'Zero ZeroGreaterEqual samePeanoGreaterEqual (SuccType PeanoNatType t a) = forall (a :: PeanoNat) (b :: PeanoNat). GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b) SuccGreaterEqual forall a b. (a -> b) -> a -> b $ forall (a :: PeanoNat). PeanoNatType a -> GreaterEqual a a samePeanoGreaterEqual PeanoNatType t a diff1GreaterEqual :: GreaterEqual a b -> GreaterEqual ('Succ a) b diff1GreaterEqual :: forall (a :: PeanoNat) (b :: PeanoNat). GreaterEqual a b -> GreaterEqual ('Succ a) b diff1GreaterEqual GreaterEqual a b ZeroGreaterEqual = forall (a :: PeanoNat). GreaterEqual a 'Zero ZeroGreaterEqual diff1GreaterEqual (SuccGreaterEqual GreaterEqual a b ge) = forall (a :: PeanoNat) (b :: PeanoNat). GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b) SuccGreaterEqual forall a b. (a -> b) -> a -> b $ forall (a :: PeanoNat) (b :: PeanoNat). GreaterEqual a b -> GreaterEqual ('Succ a) b diff1GreaterEqual GreaterEqual a b ge peanoGreaterEqual :: PeanoNatType a -> PeanoNatType b -> Maybe (GreaterEqual a b) peanoGreaterEqual :: forall (a :: PeanoNat) (b :: PeanoNat). PeanoNatType a -> PeanoNatType b -> Maybe (GreaterEqual a b) peanoGreaterEqual PeanoNatType a _ PeanoNatType b ZeroType = forall (m :: Type -> Type) a. Monad m => a -> m a return forall (a :: PeanoNat). GreaterEqual a 'Zero ZeroGreaterEqual peanoGreaterEqual PeanoNatType a ZeroType PeanoNatType b _ = forall a. Maybe a Nothing peanoGreaterEqual (SuccType PeanoNatType t a) (SuccType PeanoNatType t b) = do GreaterEqual t t al <- forall (a :: PeanoNat) (b :: PeanoNat). PeanoNatType a -> PeanoNatType b -> Maybe (GreaterEqual a b) peanoGreaterEqual PeanoNatType t a PeanoNatType t b forall (m :: Type -> Type) a. Monad m => a -> m a return forall a b. (a -> b) -> a -> b $ forall (a :: PeanoNat) (b :: PeanoNat). GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b) SuccGreaterEqual GreaterEqual t t al addPeanoNatType :: PeanoNatType a -> PeanoNatType b -> PeanoNatType (Add a b) addPeanoNatType :: forall (a :: PeanoNat) (b :: PeanoNat). PeanoNatType a -> PeanoNatType b -> PeanoNatType (Add a b) addPeanoNatType PeanoNatType a ZeroType PeanoNatType b b = PeanoNatType b b addPeanoNatType (SuccType PeanoNatType t a) PeanoNatType b b = forall (a :: PeanoNat). PeanoNatType a -> PeanoNatType ('Succ a) SuccType forall a b. (a -> b) -> a -> b $ forall (a :: PeanoNat) (b :: PeanoNat). PeanoNatType a -> PeanoNatType b -> PeanoNatType (Add a b) addPeanoNatType PeanoNatType t a PeanoNatType b b addZeroPeanoNatTypeEqual :: PeanoNatType a -> Add a 'Zero :~: a addZeroPeanoNatTypeEqual :: forall (a :: PeanoNat). PeanoNatType a -> Add a 'Zero :~: a addZeroPeanoNatTypeEqual PeanoNatType a ZeroType = forall {k} (a :: k). a :~: a Refl addZeroPeanoNatTypeEqual (SuccType PeanoNatType t a) = case forall (a :: PeanoNat). PeanoNatType a -> Add a 'Zero :~: a addZeroPeanoNatTypeEqual PeanoNatType t a of Add t 'Zero :~: t Refl -> forall {k} (a :: k). a :~: a Refl succAddPeanoNatTypeEqual' :: forall a b. PeanoNatType a -> 'Succ (Add a b) :~: Add a ('Succ b) succAddPeanoNatTypeEqual' :: forall (a :: PeanoNat) (b :: PeanoNat). PeanoNatType a -> 'Succ (Add a b) :~: Add a ('Succ b) succAddPeanoNatTypeEqual' PeanoNatType a ZeroType = forall {k} (a :: k). a :~: a Refl succAddPeanoNatTypeEqual' (SuccType PeanoNatType t a) = case forall (a :: PeanoNat) (b :: PeanoNat). PeanoNatType a -> 'Succ (Add a b) :~: Add a ('Succ b) succAddPeanoNatTypeEqual' @_ @b PeanoNatType t a of 'Succ (Add t b) :~: Add t ('Succ b) Refl -> forall {k} (a :: k). a :~: a Refl succAddPeanoNatTypeEqual :: forall a b. PeanoNatType a -> PeanoNatType b -> 'Succ (Add a b) :~: Add a ('Succ b) succAddPeanoNatTypeEqual :: forall (a :: PeanoNat) (b :: PeanoNat). PeanoNatType a -> PeanoNatType b -> 'Succ (Add a b) :~: Add a ('Succ b) succAddPeanoNatTypeEqual PeanoNatType a a PeanoNatType b _ = forall (a :: PeanoNat) (b :: PeanoNat). PeanoNatType a -> 'Succ (Add a b) :~: Add a ('Succ b) succAddPeanoNatTypeEqual' @a @b PeanoNatType a a addPeanoNatTypeGE :: PeanoNatType a -> PeanoNatType b -> GreaterEqual (Add a b) a addPeanoNatTypeGE :: forall (a :: PeanoNat) (b :: PeanoNat). PeanoNatType a -> PeanoNatType b -> GreaterEqual (Add a b) a addPeanoNatTypeGE PeanoNatType a a PeanoNatType b ZeroType = case forall (a :: PeanoNat). PeanoNatType a -> Add a 'Zero :~: a addZeroPeanoNatTypeEqual PeanoNatType a a of Add a 'Zero :~: a Refl -> forall (a :: PeanoNat). PeanoNatType a -> GreaterEqual a a samePeanoGreaterEqual PeanoNatType a a addPeanoNatTypeGE PeanoNatType a a (SuccType PeanoNatType t b) = case forall (a :: PeanoNat) (b :: PeanoNat). PeanoNatType a -> PeanoNatType b -> 'Succ (Add a b) :~: Add a ('Succ b) succAddPeanoNatTypeEqual PeanoNatType a a PeanoNatType t b of 'Succ (Add a t) :~: Add a ('Succ t) Refl -> forall (a :: PeanoNat) (b :: PeanoNat). GreaterEqual a b -> GreaterEqual ('Succ a) b diff1GreaterEqual forall a b. (a -> b) -> a -> b $ forall (a :: PeanoNat) (b :: PeanoNat). PeanoNatType a -> PeanoNatType b -> GreaterEqual (Add a b) a addPeanoNatTypeGE PeanoNatType a a PeanoNatType t b type Greater :: PeanoNat -> PeanoNat -> Type data Greater a b where MkGreater :: GreaterEqual a b -> Greater ('Succ a) b greaterIndex :: Greater a b -> PeanoNatType b greaterIndex :: forall (a :: PeanoNat) (b :: PeanoNat). Greater a b -> PeanoNatType b greaterIndex (MkGreater GreaterEqual a b n) = forall (a :: PeanoNat) (b :: PeanoNat). GreaterEqual a b -> PeanoNatType b greaterEqualIndex GreaterEqual a b n peanoGreater :: PeanoNatType a -> PeanoNatType b -> Maybe (Greater a b) peanoGreater :: forall (a :: PeanoNat) (b :: PeanoNat). PeanoNatType a -> PeanoNatType b -> Maybe (Greater a b) peanoGreater (SuccType PeanoNatType t a) PeanoNatType b b = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b fmap forall (a :: PeanoNat) (b :: PeanoNat). GreaterEqual a b -> Greater ('Succ a) b MkGreater forall a b. (a -> b) -> a -> b $ forall (a :: PeanoNat) (b :: PeanoNat). PeanoNatType a -> PeanoNatType b -> Maybe (GreaterEqual a b) peanoGreaterEqual PeanoNatType t a PeanoNatType b b peanoGreater PeanoNatType a ZeroType PeanoNatType b _ = forall a. Maybe a Nothing instance Eq (Greater 'Zero b) where == :: Greater 'Zero b -> Greater 'Zero b -> Bool (==) = forall n a. Empty n => n -> a never instance Searchable (Greater 'Zero b) where search :: forall b. (Greater 'Zero b -> Maybe b) -> Maybe b search = forall a b. Finite a => (a -> Maybe b) -> Maybe b finiteSearch instance Countable (Greater 'Zero b) where countPrevious :: Greater 'Zero b -> Maybe (Greater 'Zero b) countPrevious = forall n a. Empty n => n -> a never countMaybeNext :: Maybe (Greater 'Zero b) -> Maybe (Greater 'Zero b) countMaybeNext Maybe (Greater 'Zero b) Nothing = forall a. Maybe a Nothing countMaybeNext (Just Greater 'Zero b n) = forall n a. Empty n => n -> a never Greater 'Zero b n instance Finite (Greater 'Zero b) where allValues :: [Greater 'Zero b] allValues = [] assemble :: forall b (f :: Type -> Type). Applicative f => (Greater 'Zero b -> f b) -> f (Greater 'Zero b -> b) assemble Greater 'Zero b -> f b _ = forall (f :: Type -> Type) a. Applicative f => a -> f a pure forall n a. Empty n => n -> a never instance Empty (Greater 'Zero b) where never :: forall a. Greater 'Zero b -> a never Greater 'Zero b n = case Greater 'Zero b n of {}