{-# LANGUAGE CApiFFI #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-duplicate-exports #-}

#if defined(TH_AS_NATURAL) || defined(TH_AS_WORD64)
{-# LANGUAGE MagicHash #-}
#endif

#if defined(TH_AS_NATURAL)
#include "MachDeps.h"
#endif

module Data.DeBruijn.Thinning.Fast (
  -- * Thinnings
  (:<=) (KeepAll, KeepOne, DropOne),
  dropAll,
  toBools,
  fromTh,
  fromThRaw,

  -- * Existential Wrapper
  SomeTh (..),
  fromBools,
  toSomeTh,
  toSomeThRaw,
  fromSomeTh,
  fromSomeThRaw,

  -- * The action of thinnings on 'Nat'-indexed types
  Thin (..),

  -- * Fast
  ThRep,
  bitsToThRep,
  thRepToBits,
  (:<=) (UnsafeTh, thRep),
) where

import Control.DeepSeq (NFData (..))
import Data.Bifunctor (Bifunctor (..))
import Data.Bits (Bits (..))
import Data.DeBruijn.Index.Fast (Ix (..), isPos)
import Data.Kind (Constraint, Type)
import Data.Type.Equality (type (:~:) (Refl))
import Data.Type.Nat (Nat (..), Pos, Pred)
import Data.Type.Nat.Singleton.Fast (SNat (..), SNatRep, SomeSNat (..), decSNat, plus, toSomeSNat, toSomeSNatRaw)
import Unsafe.Coerce (unsafeCoerce)

#if defined(TH_AS_BITVEC)
import Data.Bit (Bit)
import Data.Vector.Unboxed (Vector)
#elif defined(TH_AS_INTEGER)
-- No import needed for Integer
#elif defined(TH_AS_NATURAL)

import GHC.Num.BigNat (BigNat#, bigNatFromWord#, bigNatIndex#, bigNatShiftL#, bigNatShiftR#, bigNatOrWord#, bigNatTestBit#, bigNatSize#)
import GHC.Num.Natural (Natural (..), naturalZero)
import GHC.Prim (and#, clz#, geWord#, leWord#, minusWord#, neWord#, popCnt#, uncheckedShiftL#, uncheckedShiftRL#)
import GHC.Types (isTrue#)
#elif defined(TH_AS_WORD64)
import Control.Exception (ArithException (Overflow), throw)
import Data.Bits (FiniteBits (..))
import GHC.Types (Word (W#))
#endif
-- Import for specialised thinning for Word
#if defined(TH_AS_WORD64) || defined(TH_AS_NATURAL)
import GHC.Prim (Word#, or#, not#, pdep#)
#endif

--------------------------------------------------------------------------------
-- Thinning Representation
--------------------------------------------------------------------------------

#if defined(TH_AS_BITVEC)
type ThRep = Vector Bit
#elif defined(TH_AS_INTEGER)
type ThRep = Integer
#elif defined(TH_AS_NATURAL)
type ThRep = Natural
#elif defined(TH_AS_WORD64)
type ThRep = Word
#elif !defined(__HLINT__)
#error "cpp: define one of [TH_AS_BITVEC, TH_AS_INTEGER, TH_AS_NATURAL, TH_AS_WORD64]"
#endif

--------------------------------------------------------------------------------
-- Thinning Representation: Natural
--
-- NOTE:
-- The implementation for Natural manually inlines the 'shift' and 'setBit'
-- operations, as these functions are marked with 'NOINLINE' in ghc-bignum.
#if defined(TH_AS_NATURAL)

mkKeepAllRep :: ThRep
mkKeepAllRep :: ThRep
mkKeepAllRep = ThRep
naturalZero
{-# INLINE mkKeepAllRep #-}

mkKeepOneRep :: ThRep -> ThRep
mkKeepOneRep :: ThRep -> ThRep
mkKeepOneRep v :: ThRep
v@(NS Word#
x)
   | Word#
0## <- Word#
x                       = ThRep
v
   | Int# -> Bool
isTrue# (Word# -> Word#
clz# Word#
x Word# -> Word# -> Int#
`geWord#` Word#
1##) = Word# -> ThRep
NS (Word#
x Word# -> Int# -> Word#
`uncheckedShiftL#` Int#
1#)
   | Bool
True                           = ByteArray# -> ThRep
NB (Word# -> ByteArray#
bigNatFromWord# Word#
x ByteArray# -> Word# -> ByteArray#
`bigNatShiftL#` Word#
1##)
mkKeepOneRep (NB ByteArray#
x)                 = ByteArray# -> ThRep
NB (ByteArray#
x ByteArray# -> Word# -> ByteArray#
`bigNatShiftL#` Word#
1##)
{-# INLINE mkKeepOneRep #-}

mkDropOneRep :: ThRep -> ThRep
mkDropOneRep :: ThRep -> ThRep
mkDropOneRep (NS Word#
x)
   | Word#
0## <- Word#
x                       = Word# -> ThRep
NS Word#
1##
   | Int# -> Bool
isTrue# (Word# -> Word#
clz# Word#
x Word# -> Word# -> Int#
`geWord#` Word#
1##) = Word# -> ThRep
NS ((Word#
x Word# -> Int# -> Word#
`uncheckedShiftL#` Int#
1#) Word# -> Word# -> Word#
`or#` Word#
1##)
   | Bool
True                           = ByteArray# -> ThRep
NB ((Word# -> ByteArray#
bigNatFromWord# Word#
x ByteArray# -> Word# -> ByteArray#
`bigNatShiftL#` Word#
1##) ByteArray# -> Word# -> ByteArray#
`bigNatOrWord#` Word#
1##)
mkDropOneRep (NB ByteArray#
x)                 = ByteArray# -> ThRep
NB ((ByteArray#
x ByteArray# -> Word# -> ByteArray#
`bigNatShiftL#` Word#
1##) ByteArray# -> Word# -> ByteArray#
`bigNatOrWord#` Word#
1##)
{-# INLINE mkDropOneRep #-}

elThRep :: a -> (ThRep -> a) -> (ThRep -> a) -> ThRep -> a
elThRep :: forall a. a -> (ThRep -> a) -> (ThRep -> a) -> ThRep -> a
elThRep a
ifKeepAll ThRep -> a
ifKeepOne ThRep -> a
ifDropOne = ThRep -> a
go
  where
    go :: ThRep -> a
go (NS Word#
w)
      | Word#
0## <- Word#
w = a
ifKeepAll
      | Int# -> Bool
isTrue# ((Word#
w Word# -> Word# -> Word#
`and#` Word#
1##) Word# -> Word# -> Int#
`neWord#` Word#
0##) = ThRep -> a
ifDropOne ThRep
thRepArg
      | Bool
otherwise = ThRep -> a
ifKeepOne ThRep
thRepArg
      where
        thRepArg :: ThRep
thRepArg = Word# -> ThRep
NS (Word#
w Word# -> Int# -> Word#
`uncheckedShiftRL#` Int#
1#)
    go (NB ByteArray#
bn)
      | Int# -> Bool
isTrue# (ByteArray# -> Word# -> Int#
bigNatTestBit# ByteArray#
bn Word#
0##) = ThRep -> a
ifDropOne ThRep
thRepArg
      | Bool
otherwise = ThRep -> a
ifKeepOne ThRep
thRepArg
      where
        thRepArg :: ThRep
thRepArg = ByteArray# -> ThRep
thRepFromBigNat# (ByteArray#
bn ByteArray# -> Word# -> ByteArray#
`bigNatShiftR#` Word#
1##)
{-# INLINE elThRep #-}

thRepFromBigNat# :: BigNat# -> ThRep
thRepFromBigNat# :: ByteArray# -> ThRep
thRepFromBigNat# ByteArray#
x = case ByteArray# -> Int#
bigNatSize# ByteArray#
x of
   Int#
0# -> ThRep
naturalZero
   Int#
1# -> Word# -> ThRep
NS (ByteArray# -> Int# -> Word#
bigNatIndex# ByteArray#
x Int#
0#)
   Int#
_  -> ByteArray# -> ThRep
NB ByteArray#
x

--------------------------------------------------------------------------------
-- Thinning Representation: Bits
#elif defined(TH_AS_BITVEC) || defined(TH_AS_INTEGER)

mkKeepAllRep :: ThRep
mkKeepAllRep = zeroBits
{-# INLINE mkKeepAllRep #-}

mkKeepOneRep :: ThRep -> ThRep
mkKeepOneRep = (`unsafeShiftL` 1)
{-# INLINE mkKeepOneRep #-}

mkDropOneRep :: ThRep -> ThRep
mkDropOneRep = (`setBit` 0) . (`unsafeShiftL` 1)
{-# INLINE mkDropOneRep #-}

elThRep :: a -> (ThRep -> a) -> (ThRep -> a) -> ThRep -> a
elThRep ifKeepAll ifKeepOne ifDropOne th
  | th == zeroBits = ifKeepAll
  | testBit th 0 = ifDropOne (unsafeShiftR th 1)
  | otherwise = ifKeepOne (unsafeShiftR th 1)
{-# INLINE elThRep #-}

--------------------------------------------------------------------------------
-- Thinning Representation: Finite Bits
#elif defined(TH_AS_WORD64)

mkKeepAllRep :: ThRep
mkKeepAllRep = zeroBits
{-# INLINE mkKeepAllRep #-}

mkKeepOneRep :: ThRep -> ThRep
mkKeepOneRep r
  | countLeadingZeros r < 1 = throw Overflow
  | otherwise = r `unsafeShiftL` 1
{-# INLINE mkKeepOneRep #-}

mkDropOneRep :: ThRep -> ThRep
mkDropOneRep r
  | countLeadingZeros r < 1 = throw Overflow
  | otherwise = r `unsafeShiftL` 1 .|. 1
{-# INLINE mkDropOneRep #-}

elThRep :: a -> (ThRep -> a) -> (ThRep -> a) -> ThRep -> a
elThRep ifKeepAll ifKeepOne ifDropOne r
  | r == zeroBits = ifKeepAll
  | testBit r 0 = ifDropOne (r `unsafeShiftR` 1)
  | otherwise = ifKeepOne (r `unsafeShiftR` 1)
{-# INLINE elThRep #-}
#endif

--------------------------------------------------------------------------------
-- Specialised Implementation of thin for Word
#if defined(TH_AS_NATURAL) || defined(TH_AS_WORD64)
{-
12<=29: 0b0000000000000000000000000000000000010101101010111010111110000110
04<=12: 0b0000000000000000000000000000000000000000000000000000111111110000
expect: 0b0000000000000000000000000000000000011111111111111111111111000110
not nm: 0b1111111111111111111111111111111111101010010101000101000001111001
dep ln: 0b0000000000000000000000000000000000001010010101000101000001000000
-}
thinWord# :: Word# -> Word# -> Word#
thinWord# :: Word# -> Word# -> Word#
thinWord# Word#
nm# Word#
ln# = Word#
nm# Word# -> Word# -> Word#
`or#` (Word# -> Word# -> Word#
pdep# Word#
ln# (Word# -> Word#
not# Word#
nm#))
{-# INLINE thinWord# #-}
#endif

--------------------------------------------------------------------------------
-- Thinnings
--------------------------------------------------------------------------------

type (:<=) :: Nat -> Nat -> Type
newtype (:<=) n m = UnsafeTh {forall (n :: Nat) (m :: Nat). (n :<= m) -> ThRep
thRep :: ThRep}

type role (:<=) nominal nominal

mkKeepAll :: n :<= n
mkKeepAll :: forall (n :: Nat). n :<= n
mkKeepAll = ThRep -> n :<= n
forall (n :: Nat) (m :: Nat). ThRep -> n :<= m
UnsafeTh ThRep
mkKeepAllRep
{-# INLINE mkKeepAll #-}

mkKeepOne :: n :<= m -> S n :<= S m
mkKeepOne :: forall (n :: Nat) (m :: Nat). (n :<= m) -> S n :<= S m
mkKeepOne = ThRep -> S n :<= S m
forall (n :: Nat) (m :: Nat). ThRep -> n :<= m
UnsafeTh (ThRep -> S n :<= S m)
-> ((n :<= m) -> ThRep) -> (n :<= m) -> S n :<= S m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThRep -> ThRep
mkKeepOneRep (ThRep -> ThRep) -> ((n :<= m) -> ThRep) -> (n :<= m) -> ThRep
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (.thRep)
{-# INLINE mkKeepOne #-}

mkDropOne :: n :<= m -> n :<= S m
mkDropOne :: forall (n :: Nat) (m :: Nat). (n :<= m) -> n :<= S m
mkDropOne = ThRep -> n :<= S m
forall (n :: Nat) (m :: Nat). ThRep -> n :<= m
UnsafeTh (ThRep -> n :<= S m)
-> ((n :<= m) -> ThRep) -> (n :<= m) -> n :<= S m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThRep -> ThRep
mkDropOneRep (ThRep -> ThRep) -> ((n :<= m) -> ThRep) -> (n :<= m) -> ThRep
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (.thRep)
{-# INLINE mkDropOne #-}

elTh :: a -> (Pred n :<= Pred m -> a) -> (n :<= Pred m -> a) -> n :<= m -> a
elTh :: forall a (n :: Nat) (m :: Nat).
a
-> ((Pred n :<= Pred m) -> a)
-> ((n :<= Pred m) -> a)
-> (n :<= m)
-> a
elTh a
ifKeepAll (Pred n :<= Pred m) -> a
ifKeepOne (n :<= Pred m) -> a
ifDropOne =
  a -> (ThRep -> a) -> (ThRep -> a) -> ThRep -> a
forall a. a -> (ThRep -> a) -> (ThRep -> a) -> ThRep -> a
elThRep a
ifKeepAll ((Pred n :<= Pred m) -> a
ifKeepOne ((Pred n :<= Pred m) -> a)
-> (ThRep -> Pred n :<= Pred m) -> ThRep -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThRep -> Pred n :<= Pred m
forall (n :: Nat) (m :: Nat). ThRep -> n :<= m
UnsafeTh) ((n :<= Pred m) -> a
ifDropOne ((n :<= Pred m) -> a) -> (ThRep -> n :<= Pred m) -> ThRep -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThRep -> n :<= Pred m
forall (n :: Nat) (m :: Nat). ThRep -> n :<= m
UnsafeTh) (ThRep -> a) -> ((n :<= m) -> ThRep) -> (n :<= m) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (.thRep)
{-# INLINE elTh #-}

data ThF (th :: Nat -> Nat -> Type) (n :: Nat) (m :: Nat) where
  KeepAllF :: ThF th n n
  KeepOneF :: !(th n m) -> ThF th (S n) (S m)
  DropOneF :: !(th n m) -> ThF th n (S m)

projectTh :: n :<= m -> ThF (:<=) n m
projectTh :: forall (n :: Nat) (m :: Nat). (n :<= m) -> ThF (:<=) n m
projectTh =
  ThF (:<=) n m
-> ((Pred n :<= Pred m) -> ThF (:<=) n m)
-> ((n :<= Pred m) -> ThF (:<=) n m)
-> (n :<= m)
-> ThF (:<=) n m
forall a (n :: Nat) (m :: Nat).
a
-> ((Pred n :<= Pred m) -> a)
-> ((n :<= Pred m) -> a)
-> (n :<= m)
-> a
elTh (ThF Any Any Any -> ThF (:<=) n m
forall a b. a -> b
unsafeCoerce ThF Any Any Any
forall (th :: Nat -> Nat -> *) (n :: Nat). ThF th n n
KeepAllF) (ThF (:<=) (S (Pred n)) (S (Pred m)) -> ThF (:<=) n m
forall a b. a -> b
unsafeCoerce (ThF (:<=) (S (Pred n)) (S (Pred m)) -> ThF (:<=) n m)
-> ((Pred n :<= Pred m) -> ThF (:<=) (S (Pred n)) (S (Pred m)))
-> (Pred n :<= Pred m)
-> ThF (:<=) n m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pred n :<= Pred m) -> ThF (:<=) (S (Pred n)) (S (Pred m))
forall (th :: Nat -> Nat -> *) (m :: Nat) (m :: Nat).
th m m -> ThF th (S m) (S m)
KeepOneF) (ThF (:<=) n (S (Pred m)) -> ThF (:<=) n m
forall a b. a -> b
unsafeCoerce (ThF (:<=) n (S (Pred m)) -> ThF (:<=) n m)
-> ((n :<= Pred m) -> ThF (:<=) n (S (Pred m)))
-> (n :<= Pred m)
-> ThF (:<=) n m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (n :<= Pred m) -> ThF (:<=) n (S (Pred m))
forall (th :: Nat -> Nat -> *) (n :: Nat) (m :: Nat).
th n m -> ThF th n (S m)
DropOneF)
{-# INLINE projectTh #-}

embedTh :: ThF (:<=) n m -> n :<= m
embedTh :: forall (n :: Nat) (m :: Nat). ThF (:<=) n m -> n :<= m
embedTh = \case
  ThF (:<=) n m
KeepAllF -> n :<= n
n :<= m
forall (n :: Nat). n :<= n
mkKeepAll
  KeepOneF n :<= m
n'm' -> (n :<= m) -> S n :<= S m
forall (n :: Nat) (m :: Nat). (n :<= m) -> S n :<= S m
mkKeepOne n :<= m
n'm'
  DropOneF n :<= m
nm' -> (n :<= m) -> n :<= S m
forall (n :: Nat) (m :: Nat). (n :<= m) -> n :<= S m
mkDropOne n :<= m
nm'
{-# INLINE embedTh #-}

pattern KeepAll :: () => (n ~ m) => n :<= m
pattern $mKeepAll :: forall {r} {n :: Nat} {m :: Nat}.
(n :<= m) -> ((n ~ m) => r) -> ((# #) -> r) -> r
$bKeepAll :: forall (n :: Nat) (m :: Nat). (n ~ m) => n :<= m
KeepAll <- (projectTh -> KeepAllF) where KeepAll = ThF (:<=) n m -> n :<= m
forall (n :: Nat) (m :: Nat). ThF (:<=) n m -> n :<= m
embedTh ThF (:<=) n n
ThF (:<=) n m
forall (th :: Nat -> Nat -> *) (n :: Nat). ThF th n n
KeepAllF
{-# INLINE KeepAll #-}

pattern KeepOne :: () => (Pos n, Pos m) => Pred n :<= Pred m -> n :<= m
pattern $mKeepOne :: forall {r} {n :: Nat} {m :: Nat}.
(n :<= m)
-> ((Pos n, Pos m) => (Pred n :<= Pred m) -> r)
-> ((# #) -> r)
-> r
$bKeepOne :: forall (n :: Nat) (m :: Nat).
(Pos n, Pos m) =>
(Pred n :<= Pred m) -> n :<= m
KeepOne nm <- (projectTh -> KeepOneF nm) where KeepOne Pred n :<= Pred m
nm = ThF (:<=) n m -> n :<= m
forall (n :: Nat) (m :: Nat). ThF (:<=) n m -> n :<= m
embedTh ((Pred n :<= Pred m) -> ThF (:<=) (S (Pred n)) (S (Pred m))
forall (th :: Nat -> Nat -> *) (m :: Nat) (m :: Nat).
th m m -> ThF th (S m) (S m)
KeepOneF Pred n :<= Pred m
nm)
{-# INLINE KeepOne #-}

pattern DropOne :: () => (Pos m) => n :<= Pred m -> n :<= m
pattern $mDropOne :: forall {r} {m :: Nat} {n :: Nat}.
(n :<= m) -> (Pos m => (n :<= Pred m) -> r) -> ((# #) -> r) -> r
$bDropOne :: forall (m :: Nat) (n :: Nat). Pos m => (n :<= Pred m) -> n :<= m
DropOne nm <- (projectTh -> DropOneF nm) where DropOne n :<= Pred m
nm = ThF (:<=) n m -> n :<= m
forall (n :: Nat) (m :: Nat). ThF (:<=) n m -> n :<= m
embedTh ((n :<= Pred m) -> ThF (:<=) n (S (Pred m))
forall (th :: Nat -> Nat -> *) (n :: Nat) (m :: Nat).
th n m -> ThF th n (S m)
DropOneF n :<= Pred m
nm)
{-# INLINE DropOne #-}

{-# COMPLETE KeepAll, KeepOne, DropOne #-}

deriving newtype instance Eq (n :<= m)

instance Show (n :<= m) where
  showsPrec :: Int -> n :<= m -> ShowS
  showsPrec :: Int -> (n :<= m) -> ShowS
showsPrec Int
p =
    Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ((n :<= m) -> ShowS) -> (n :<= m) -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
      n :<= m
KeepAll -> String -> ShowS
showString String
"KeepAll"
      KeepOne Pred n :<= Pred m
n'm' -> String -> ShowS
showString String
"KeepOne " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (Pred n :<= Pred m) -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Pred n :<= Pred m
n'm'
      DropOne n :<= Pred m
nm' -> String -> ShowS
showString String
"DropOne " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (n :<= Pred m) -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 n :<= Pred m
nm'

deriving newtype instance NFData (n :<= m)

-- | Drop all entries.
dropAll :: SNat m -> Z :<= m
dropAll :: forall (m :: Nat). SNat m -> Z :<= m
dropAll SNat m
Z = Z :<= m
forall (n :: Nat) (m :: Nat). (n ~ m) => n :<= m
KeepAll
dropAll (S SNat (Pred m)
m') = (Z :<= Pred m) -> Z :<= m
forall (m :: Nat) (n :: Nat). Pos m => (n :<= Pred m) -> n :<= m
DropOne (SNat (Pred m) -> Z :<= Pred m
forall (m :: Nat). SNat m -> Z :<= m
dropAll SNat (Pred m)
m')

-- | Convert a thinning into a list of booleans.
toBools :: n :<= m -> [Bool]
toBools :: forall (n :: Nat) (m :: Nat). (n :<= m) -> [Bool]
toBools = \case
  n :<= m
KeepAll -> []
  KeepOne Pred n :<= Pred m
n'm' -> Bool
False Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: (Pred n :<= Pred m) -> [Bool]
forall (n :: Nat) (m :: Nat). (n :<= m) -> [Bool]
toBools Pred n :<= Pred m
n'm'
  DropOne n :<= Pred m
nm' -> Bool
True Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
: (n :<= Pred m) -> [Bool]
forall (n :: Nat) (m :: Nat). (n :<= m) -> [Bool]
toBools n :<= Pred m
nm'

-- | Convert a thinning into a bit sequence.
fromTh :: (Bits bs) => n :<= m -> bs
fromTh :: forall bs (n :: Nat) (m :: Nat). Bits bs => (n :<= m) -> bs
fromTh = \case
  n :<= m
KeepAll -> bs
forall a. Bits a => a
zeroBits
  KeepOne Pred n :<= Pred m
n'm' -> (bs -> Int -> bs
forall a. Bits a => a -> Int -> a
`unsafeShiftL` Int
1) (bs -> bs)
-> ((Pred n :<= Pred m) -> bs) -> (Pred n :<= Pred m) -> bs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pred n :<= Pred m) -> bs
forall bs (n :: Nat) (m :: Nat). Bits bs => (n :<= m) -> bs
fromTh ((Pred n :<= Pred m) -> bs) -> (Pred n :<= Pred m) -> bs
forall a b. (a -> b) -> a -> b
$ Pred n :<= Pred m
n'm'
  DropOne n :<= Pred m
nm' -> (bs -> Int -> bs
forall a. Bits a => a -> Int -> a
`setBit` Int
0) (bs -> bs) -> ((n :<= Pred m) -> bs) -> (n :<= Pred m) -> bs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (bs -> Int -> bs
forall a. Bits a => a -> Int -> a
`unsafeShiftL` Int
1) (bs -> bs) -> ((n :<= Pred m) -> bs) -> (n :<= Pred m) -> bs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (n :<= Pred m) -> bs
forall bs (n :: Nat) (m :: Nat). Bits bs => (n :<= m) -> bs
fromTh ((n :<= Pred m) -> bs) -> (n :<= Pred m) -> bs
forall a b. (a -> b) -> a -> b
$ n :<= Pred m
nm'
{-# SPECIALIZE fromTh :: n :<= m -> ThRep #-}

fromThRaw :: n :<= m -> ThRep
fromThRaw :: forall (n :: Nat) (m :: Nat). (n :<= m) -> ThRep
fromThRaw = (.thRep)
{-# INLINE fromThRaw #-}

--------------------------------------------------------------------------------
-- Existential Wrapper
--------------------------------------------------------------------------------

data SomeTh
  = forall n m.
  SomeTh
  { ()
lower :: SNat n
  , ()
upper :: SNat m
  , ()
value :: n :<= m
  }

instance Eq SomeTh where
  (==) :: SomeTh -> SomeTh -> Bool
  SomeTh SNat n
n1 SNat m
m1 n :<= m
n1m1 == :: SomeTh -> SomeTh -> Bool
== SomeTh SNat n
n2 SNat m
m2 n :<= m
n2m2
    | Just n :~: n
Refl <- SNat n -> SNat n -> Maybe (n :~: n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Maybe (n :~: m)
decSNat SNat n
n1 SNat n
n2
    , Just m :~: m
Refl <- SNat m -> SNat m -> Maybe (m :~: m)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> Maybe (n :~: m)
decSNat SNat m
m1 SNat m
m2 =
        n :<= m
n1m1 (n :<= m) -> (n :<= m) -> Bool
forall a. Eq a => a -> a -> Bool
== n :<= m
n :<= m
n2m2
    | Bool
otherwise = Bool
False

deriving stock instance Show SomeTh

instance NFData SomeTh where
  rnf :: SomeTh -> ()
  rnf :: SomeTh -> ()
rnf SomeTh{SNat n
SNat m
n :<= m
lower :: ()
upper :: ()
value :: ()
lower :: SNat n
upper :: SNat m
value :: n :<= m
..} = SNat n -> ()
forall a. NFData a => a -> ()
rnf SNat n
lower () -> () -> ()
forall a b. a -> b -> b
`seq` SNat m -> ()
forall a. NFData a => a -> ()
rnf SNat m
upper () -> () -> ()
forall a b. a -> b -> b
`seq` (n :<= m) -> ()
forall a. NFData a => a -> ()
rnf n :<= m
value

someKeepAll :: SomeSNat -> SomeTh
someKeepAll :: SomeSNat -> SomeTh
someKeepAll (SomeSNat SNat n
bound) =
  SomeTh
    { lower :: SNat n
lower = SNat n
bound
    , upper :: SNat n
upper = SNat n
bound
    , value :: n :<= n
value = n :<= n
forall (n :: Nat) (m :: Nat). (n ~ m) => n :<= m
KeepAll
    }
{-# INLINE someKeepAll #-}

someKeepOne :: SomeTh -> SomeTh
someKeepOne :: SomeTh -> SomeTh
someKeepOne SomeTh{SNat n
SNat m
n :<= m
lower :: ()
upper :: ()
value :: ()
lower :: SNat n
upper :: SNat m
value :: n :<= m
..} =
  SomeTh
    { lower :: SNat (S n)
lower = SNat (Pred (S n)) -> SNat (S n)
forall (n :: Nat). Pos n => SNat (Pred n) -> SNat n
S SNat n
SNat (Pred (S n))
lower
    , upper :: SNat (S m)
upper = SNat (Pred (S m)) -> SNat (S m)
forall (n :: Nat). Pos n => SNat (Pred n) -> SNat n
S SNat m
SNat (Pred (S m))
upper
    , value :: S n :<= S m
value = (Pred (S n) :<= Pred (S m)) -> S n :<= S m
forall (n :: Nat) (m :: Nat).
(Pos n, Pos m) =>
(Pred n :<= Pred m) -> n :<= m
KeepOne n :<= m
Pred (S n) :<= Pred (S m)
value
    }
{-# INLINE someKeepOne #-}

someDropOne :: SomeTh -> SomeTh
someDropOne :: SomeTh -> SomeTh
someDropOne SomeTh{SNat n
SNat m
n :<= m
lower :: ()
upper :: ()
value :: ()
lower :: SNat n
upper :: SNat m
value :: n :<= m
..} =
  SomeTh
    { lower :: SNat n
lower = SNat n
lower
    , upper :: SNat (S m)
upper = SNat (Pred (S m)) -> SNat (S m)
forall (n :: Nat). Pos n => SNat (Pred n) -> SNat n
S SNat m
SNat (Pred (S m))
upper
    , value :: n :<= S m
value = (n :<= Pred (S m)) -> n :<= S m
forall (m :: Nat) (n :: Nat). Pos m => (n :<= Pred m) -> n :<= m
DropOne n :<= m
n :<= Pred (S m)
value
    }
{-# INLINE someDropOne #-}

fromBools :: (Integral i) => i -> [Bool] -> SomeTh
fromBools :: forall i. Integral i => i -> [Bool] -> SomeTh
fromBools i
bound = [Bool] -> SomeTh
go
 where
  go :: [Bool] -> SomeTh
go [] = SomeSNat -> SomeTh
someKeepAll (i -> SomeSNat
forall i. Integral i => i -> SomeSNat
toSomeSNat i
bound)
  go (Bool
False : [Bool]
bools) = SomeTh -> SomeTh
someKeepOne ([Bool] -> SomeTh
go [Bool]
bools)
  go (Bool
True : [Bool]
bools) = SomeTh -> SomeTh
someDropOne ([Bool] -> SomeTh
go [Bool]
bools)
{-# SPECIALIZE fromBools :: SNatRep -> [Bool] -> SomeTh #-}

toSomeTh :: (Integral i, Bits bs) => (i, bs) -> SomeTh
toSomeTh :: forall i bs. (Integral i, Bits bs) => (i, bs) -> SomeTh
toSomeTh (i
nRep, bs
nmRep) = (Int, ThRep) -> SomeTh
toSomeThRaw (i -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral i
nRep, bs -> ThRep
forall bs1 bs2. (Bits bs1, Bits bs2) => bs1 -> bs2
copyBits bs
nmRep)
{-# SPECIALIZE toSomeTh :: (SNatRep, ThRep) -> SomeTh #-}

toSomeThRaw :: (SNatRep, ThRep) -> SomeTh
toSomeThRaw :: (Int, ThRep) -> SomeTh
toSomeThRaw (Int
nRep, ThRep
nmRep)
  | SomeSNat SNat n
n <- Int -> SomeSNat
toSomeSNatRaw Int
nRep
  , let dRep :: Int
dRep = ThRep -> Int
forall a. Bits a => a -> Int
popCount ThRep
nmRep
  , SomeSNat SNat n
d <- Int -> SomeSNat
forall i. Integral i => i -> SomeSNat
toSomeSNat Int
dRep
  , let m :: SNat (n + n)
m = SNat n
n SNat n -> SNat n -> SNat (n + n)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
`plus` SNat n
d
  , let nm :: n :<= (n + n)
nm = ThRep -> n :<= (n + n)
forall (n :: Nat) (m :: Nat). ThRep -> n :<= m
UnsafeTh ThRep
nmRep =
      SNat n -> SNat (n + n) -> (n :<= (n + n)) -> SomeTh
forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> (n :<= m) -> SomeTh
SomeTh SNat n
n SNat (n + n)
m n :<= (n + n)
nm
{-# INLINE toSomeThRaw #-}

withSomeTh :: (forall n m. SNat n -> SNat m -> n :<= m -> r) -> SomeTh -> r
withSomeTh :: forall r.
(forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n :<= m) -> r)
-> SomeTh -> r
withSomeTh forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n :<= m) -> r
action (SomeTh SNat n
n SNat m
m n :<= m
nm) = SNat n -> SNat m -> (n :<= m) -> r
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n :<= m) -> r
action SNat n
n SNat m
m n :<= m
nm
{-# INLINE withSomeTh #-}

-- | Convert a thinning into a bit sequence.
fromSomeTh :: (Integral i, Bits bs) => SomeTh -> (i, bs)
fromSomeTh :: forall i bs. (Integral i, Bits bs) => SomeTh -> (i, bs)
fromSomeTh = (Int -> i) -> (ThRep -> bs) -> (Int, ThRep) -> (i, bs)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Int -> i
forall a b. (Integral a, Num b) => a -> b
fromIntegral ThRep -> bs
forall bs. Bits bs => ThRep -> bs
thRepToBits ((Int, ThRep) -> (i, bs))
-> (SomeTh -> (Int, ThRep)) -> SomeTh -> (i, bs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeTh -> (Int, ThRep)
fromSomeThRaw
{-# INLINE fromSomeTh #-}

fromSomeThRaw :: SomeTh -> (SNatRep, ThRep)
fromSomeThRaw :: SomeTh -> (Int, ThRep)
fromSomeThRaw = (forall (n :: Nat) (m :: Nat).
 SNat n -> SNat m -> (n :<= m) -> (Int, ThRep))
-> SomeTh -> (Int, ThRep)
forall r.
(forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> (n :<= m) -> r)
-> SomeTh -> r
withSomeTh (\SNat n
n SNat m
_m n :<= m
nm -> (SNat n
n.snatRep, n :<= m
nm.thRep))
{-# INLINE fromSomeThRaw #-}

bitsToThRep :: (Bits bs) => bs -> ThRep
bitsToThRep :: forall bs. Bits bs => bs -> ThRep
bitsToThRep = bs -> ThRep
forall bs1 bs2. (Bits bs1, Bits bs2) => bs1 -> bs2
copyBits
{-# INLINE bitsToThRep #-}

thRepToBits :: (Bits bs) => ThRep -> bs
thRepToBits :: forall bs. Bits bs => ThRep -> bs
thRepToBits = ThRep -> bs
forall bs1 bs2. (Bits bs1, Bits bs2) => bs1 -> bs2
copyBits
{-# INLINE thRepToBits #-}

-- TODO(optimise):
copyBits :: forall bs1 bs2. (Bits bs1, Bits bs2) => bs1 -> bs2
copyBits :: forall bs1 bs2. (Bits bs1, Bits bs2) => bs1 -> bs2
copyBits bs1
bs = Int -> bs2 -> bs1 -> bs2
go Int
0 (bs2 -> Int -> bs2
forall a. Bits a => a -> Int -> a
unsafeShiftL bs2
forall a. Bits a => a
zeroBits (bs1 -> Int
forall a. Bits a => a -> Int
bitCount bs1
bs)) bs1
bs
 where
  go :: Int -> bs2 -> bs1 -> bs2
  go :: Int -> bs2 -> bs1 -> bs2
go Int
i bs2
bs2 bs1
bs1
    | bs1
bs1 bs1 -> bs1 -> Bool
forall a. Eq a => a -> a -> Bool
== bs1
forall a. Bits a => a
zeroBits = bs2
bs2
    | bs1 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit bs1
bs1 Int
0 = Int -> bs2 -> bs1 -> bs2
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (bs2 -> Int -> bs2
forall a. Bits a => a -> Int -> a
setBit bs2
bs2 Int
i) (bs1 -> Int -> bs1
forall a. Bits a => a -> Int -> a
unsafeShiftR bs1
bs1 Int
1)
    | Bool
otherwise = Int -> bs2 -> bs1 -> bs2
go (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) bs2
bs2 (bs1 -> Int -> bs1
forall a. Bits a => a -> Int -> a
unsafeShiftR bs1
bs1 Int
1)

bitCount :: (Bits bs) => bs -> Int
bitCount :: forall a. Bits a => a -> Int
bitCount bs
bs
  | bs
bs bs -> bs -> Bool
forall a. Eq a => a -> a -> Bool
== bs
forall a. Bits a => a
zeroBits = Int
0
  | Bool
otherwise = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ bs -> Int
forall a. Bits a => a -> Int
bitCount (bs -> Int -> bs
forall a. Bits a => a -> Int -> a
unsafeShiftR bs
bs Int
1)

--------------------------------------------------------------------------------
-- Thinning Class
--------------------------------------------------------------------------------

-- | The actions of thinnings on natural-indexed data types.
type Thin :: (Nat -> Type) -> Constraint
class Thin f where
  thin :: n :<= m -> f n -> f m
  thick :: n :<= m -> f m -> Maybe (f n)

instance Thin Ix where
  thin :: n :<= m -> Ix n -> Ix m
  thin :: forall (n :: Nat) (m :: Nat). (n :<= m) -> Ix n -> Ix m
thin !n :<= m
t !Ix n
i = Ix n -> (Pos n => Ix m) -> Ix m
forall (n :: Nat) a. Ix n -> (Pos n => a) -> a
isPos Ix n
i ((Pos n => Ix m) -> Ix m) -> (Pos n => Ix m) -> Ix m
forall a b. (a -> b) -> a -> b
$
    -- TODO(optimise): this can be done in constant time by converting the
    -- index to a 1-thinning, applying constant-time thinning composition,
    -- and finally converting back to a number. the conversions should be
    -- `bit` and `log2`, both of which consist of one instruction.
    case n :<= m
t of
      n :<= m
KeepAll -> Ix n
Ix m
i
      KeepOne Pred n :<= Pred m
n'm' ->
        case Ix n
i of
          Ix n
FZ -> Ix m
forall (n :: Nat). Pos n => Ix n
FZ
          FS Ix (Pred n)
i' -> Ix (Pred m) -> Ix m
forall (n :: Nat). Pos n => Ix (Pred n) -> Ix n
FS ((Pred n :<= Pred m) -> Ix (Pred n) -> Ix (Pred m)
forall (n :: Nat) (m :: Nat). (n :<= m) -> Ix n -> Ix m
forall (f :: Nat -> *) (n :: Nat) (m :: Nat).
Thin f =>
(n :<= m) -> f n -> f m
thin Pred n :<= Pred m
n'm' Ix (Pred n)
i')
      DropOne n :<= Pred m
nm' -> Ix (Pred m) -> Ix m
forall (n :: Nat). Pos n => Ix (Pred n) -> Ix n
FS ((n :<= Pred m) -> Ix n -> Ix (Pred m)
forall (n :: Nat) (m :: Nat). (n :<= m) -> Ix n -> Ix m
forall (f :: Nat -> *) (n :: Nat) (m :: Nat).
Thin f =>
(n :<= m) -> f n -> f m
thin n :<= Pred m
nm' Ix n
i)

  -- TODO(optimise):
  thick :: n :<= m -> Ix m -> Maybe (Ix n)
  thick :: forall (n :: Nat) (m :: Nat). (n :<= m) -> Ix m -> Maybe (Ix n)
thick n :<= m
KeepAll Ix m
i = Ix n -> Maybe (Ix n)
forall a. a -> Maybe a
Just Ix n
Ix m
i
  thick (KeepOne Pred n :<= Pred m
_n'm') Ix m
FZ = Ix n -> Maybe (Ix n)
forall a. a -> Maybe a
Just Ix n
forall (n :: Nat). Pos n => Ix n
FZ
  thick (KeepOne Pred n :<= Pred m
n'm') (FS Ix (Pred m)
i') = Ix (Pred n) -> Ix n
forall (n :: Nat). Pos n => Ix (Pred n) -> Ix n
FS (Ix (Pred n) -> Ix n) -> Maybe (Ix (Pred n)) -> Maybe (Ix n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pred n :<= Pred m) -> Ix (Pred m) -> Maybe (Ix (Pred n))
forall (n :: Nat) (m :: Nat). (n :<= m) -> Ix m -> Maybe (Ix n)
forall (f :: Nat -> *) (n :: Nat) (m :: Nat).
Thin f =>
(n :<= m) -> f m -> Maybe (f n)
thick Pred n :<= Pred m
n'm' Ix (Pred m)
i'
  thick (DropOne n :<= Pred m
_nm') Ix m
FZ = Maybe (Ix n)
forall a. Maybe a
Nothing
  thick (DropOne n :<= Pred m
nm') (FS Ix (Pred m)
i') = (n :<= Pred m) -> Ix (Pred m) -> Maybe (Ix n)
forall (n :: Nat) (m :: Nat). (n :<= m) -> Ix m -> Maybe (Ix n)
forall (f :: Nat -> *) (n :: Nat) (m :: Nat).
Thin f =>
(n :<= m) -> f m -> Maybe (f n)
thick n :<= Pred m
nm' Ix (Pred m)
i'

instance Thin ((:<=) l) where
  thin :: n :<= m -> l :<= n -> l :<= m
#if defined(TH_AS_NATURAL)
  thin :: forall (n :: Nat) (m :: Nat). (n :<= m) -> (l :<= n) -> l :<= m
thin (UnsafeTh (NS Word#
nm#)) (UnsafeTh (NS Word#
ln#))
    | Int# -> Bool
isTrue# (WORD_SIZE_IN_BITS## `minusWord#` clz# ln# `leWord#` popCnt# (not# nm#))
    = ThRep -> l :<= m
forall (n :: Nat) (m :: Nat). ThRep -> n :<= m
UnsafeTh (Word# -> ThRep
NS (Word# -> Word# -> Word#
thinWord# Word#
nm# Word#
ln#))
  -- TODO(optimise): this can be done for the `NB` case by iterating the
  -- `thinWord#` over all components of the `BigNat`.
  thin n :<= m
nm l :<= n
KeepAll = l :<= m
n :<= m
nm
  thin n :<= m
KeepAll l :<= n
ln = l :<= n
l :<= m
ln
  thin (KeepOne Pred n :<= Pred m
n'm') (KeepOne Pred l :<= Pred n
l'n') = (Pred l :<= Pred m) -> l :<= m
forall (n :: Nat) (m :: Nat).
(Pos n, Pos m) =>
(Pred n :<= Pred m) -> n :<= m
KeepOne ((Pred n :<= Pred m) -> (Pred l :<= Pred n) -> Pred l :<= Pred m
forall (n :: Nat) (m :: Nat).
(n :<= m) -> (Pred l :<= n) -> Pred l :<= m
forall (f :: Nat -> *) (n :: Nat) (m :: Nat).
Thin f =>
(n :<= m) -> f n -> f m
thin Pred n :<= Pred m
n'm' Pred l :<= Pred n
l'n')
  thin (KeepOne Pred n :<= Pred m
n'm') (DropOne l :<= Pred n
ln') = (l :<= Pred m) -> l :<= m
forall (m :: Nat) (n :: Nat). Pos m => (n :<= Pred m) -> n :<= m
DropOne ((Pred n :<= Pred m) -> (l :<= Pred n) -> l :<= Pred m
forall (n :: Nat) (m :: Nat). (n :<= m) -> (l :<= n) -> l :<= m
forall (f :: Nat -> *) (n :: Nat) (m :: Nat).
Thin f =>
(n :<= m) -> f n -> f m
thin Pred n :<= Pred m
n'm' l :<= Pred n
ln')
  thin (DropOne n :<= Pred m
nm') l :<= n
ln = (l :<= Pred m) -> l :<= m
forall (m :: Nat) (n :: Nat). Pos m => (n :<= Pred m) -> n :<= m
DropOne ((n :<= Pred m) -> (l :<= n) -> l :<= Pred m
forall (n :: Nat) (m :: Nat). (n :<= m) -> (l :<= n) -> l :<= m
forall (f :: Nat -> *) (n :: Nat) (m :: Nat).
Thin f =>
(n :<= m) -> f n -> f m
thin n :<= Pred m
nm' l :<= n
ln)
#elif defined(TH_AS_WORD64)
  thin (UnsafeTh (W# nm#)) (UnsafeTh (W# ln#)) = UnsafeTh (W# (thinWord# nm# ln#))
#else
  thin nm KeepAll = nm
  thin KeepAll ln = ln
  thin (KeepOne n'm') (KeepOne l'n') = KeepOne (thin n'm' l'n')
  thin (KeepOne n'm') (DropOne ln') = DropOne (thin n'm' ln')
  thin (DropOne nm') ln = DropOne (thin nm' ln)
#endif

{- ORMOLU_DISABLE -}
  -- TODO(optimise):
  thick :: n :<= m -> l :<= m -> Maybe (l :<= n)
  thick :: forall (n :: Nat) (m :: Nat).
(n :<= m) -> (l :<= m) -> Maybe (l :<= n)
thick n :<= m
KeepAll l :<= m
lm = (l :<= n) -> Maybe (l :<= n)
forall a. a -> Maybe a
Just l :<= n
l :<= m
lm
  thick (KeepOne Pred n :<= Pred m
n'm') l :<= m
KeepAll = (Pred l :<= Pred n) -> l :<= n
(Pred m :<= Pred n) -> l :<= n
forall (n :: Nat) (m :: Nat).
(Pos n, Pos m) =>
(Pred n :<= Pred m) -> n :<= m
KeepOne ((Pred m :<= Pred n) -> l :<= n)
-> Maybe (Pred m :<= Pred n) -> Maybe (l :<= n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pred n :<= Pred m)
-> (Pred m :<= Pred m) -> Maybe (Pred m :<= Pred n)
forall (n :: Nat) (m :: Nat).
(n :<= m) -> (Pred m :<= m) -> Maybe (Pred m :<= n)
forall (f :: Nat -> *) (n :: Nat) (m :: Nat).
Thin f =>
(n :<= m) -> f m -> Maybe (f n)
thick Pred n :<= Pred m
n'm' Pred m :<= Pred m
forall (n :: Nat) (m :: Nat). (n ~ m) => n :<= m
KeepAll
  thick (KeepOne Pred n :<= Pred m
n'm') (KeepOne Pred l :<= Pred m
l'n') = (Pred l :<= Pred n) -> l :<= n
forall (n :: Nat) (m :: Nat).
(Pos n, Pos m) =>
(Pred n :<= Pred m) -> n :<= m
KeepOne ((Pred l :<= Pred n) -> l :<= n)
-> Maybe (Pred l :<= Pred n) -> Maybe (l :<= n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pred n :<= Pred m)
-> (Pred l :<= Pred m) -> Maybe (Pred l :<= Pred n)
forall (n :: Nat) (m :: Nat).
(n :<= m) -> (Pred l :<= m) -> Maybe (Pred l :<= n)
forall (f :: Nat -> *) (n :: Nat) (m :: Nat).
Thin f =>
(n :<= m) -> f m -> Maybe (f n)
thick Pred n :<= Pred m
n'm' Pred l :<= Pred m
l'n'
  thick (KeepOne Pred n :<= Pred m
n'm') (DropOne l :<= Pred m
ln') = (l :<= Pred n) -> l :<= n
forall (m :: Nat) (n :: Nat). Pos m => (n :<= Pred m) -> n :<= m
DropOne ((l :<= Pred n) -> l :<= n)
-> Maybe (l :<= Pred n) -> Maybe (l :<= n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pred n :<= Pred m) -> (l :<= Pred m) -> Maybe (l :<= Pred n)
forall (n :: Nat) (m :: Nat).
(n :<= m) -> (l :<= m) -> Maybe (l :<= n)
forall (f :: Nat -> *) (n :: Nat) (m :: Nat).
Thin f =>
(n :<= m) -> f m -> Maybe (f n)
thick Pred n :<= Pred m
n'm' l :<= Pred m
ln'
  thick (DropOne n :<= Pred m
_nm') l :<= m
KeepAll = Maybe (l :<= n)
forall a. Maybe a
Nothing
  thick (DropOne n :<= Pred m
_nm') (KeepOne Pred l :<= Pred m
_l'n') = Maybe (l :<= n)
forall a. Maybe a
Nothing
  thick (DropOne n :<= Pred m
nm') (DropOne l :<= Pred m
ln') = (n :<= Pred m) -> (l :<= Pred m) -> Maybe (l :<= n)
forall (n :: Nat) (m :: Nat).
(n :<= m) -> (l :<= m) -> Maybe (l :<= n)
forall (f :: Nat -> *) (n :: Nat) (m :: Nat).
Thin f =>
(n :<= m) -> f m -> Maybe (f n)
thick n :<= Pred m
nm' l :<= Pred m
ln'
{- ORMOLU_ENABLE -}