Safe Haskell	None
Language	GHC2021

Data.DeBruijn.Index.Fast

Contents

DeBruijn Indexes
Existential Wrapper
Fast

Synopsis

data Ix (n :: Nat) where
- pattern FZ :: () => Pos n => Ix n
- pattern FS :: () => Pos n => Ix (Pred n) -> Ix n
eqIx :: forall (n :: Nat) (m :: Nat). Ix n -> Ix m -> Bool
fromIx :: forall i (n :: Nat). Integral i => Ix n -> i
fromIxRaw :: forall (n :: Nat). Ix n -> IxRep
isPos :: forall (n :: Nat) a. Ix n -> (Pos n => a) -> a
thin :: forall (n :: Nat). Ix ('S n) -> Ix n -> Ix ('S n)
thick :: forall (n :: Nat). Ix ('S n) -> Ix ('S n) -> Maybe (Ix n)
inject :: forall (n :: Nat) (m :: Nat). Ix n -> SNat m -> Ix (n + m)
raise :: forall (n :: Nat) (m :: Nat). SNat n -> Ix m -> Ix (n + m)
data SomeIx = SomeIx {
- bound :: !(SNat n)
- index :: !(Ix n)
}
withSomeIx :: (forall (n :: Nat). SNat n -> Ix n -> a) -> SomeIx -> a
toSomeIx :: (Integral n, Integral i) => (n, i) -> SomeIx
toSomeIxRaw :: (SNatRep, IxRep) -> SomeIx
fromSomeIx :: (Integral n, Integral i) => SomeIx -> (n, i)
fromSomeIxRaw :: SomeIx -> (SNatRep, IxRep)
type IxRep = Int
intToIxRep :: Int -> IxRep
ixRepToInt :: IxRep -> Int
snatRepToIxRep :: SNatRep -> IxRep
ixRepToSNatRep :: IxRep -> SNatRep
newtype Ix (n :: Nat) = UnsafeIx {
- ixRep :: IxRep
}

DeBruijn Indexes

data Ix (n :: Nat) where Source #

Ix n is the type of DeBruijn indices less than n.

Bundled Patterns

pattern FZ :: () => Pos n => Ix n
pattern FS :: () => Pos n => Ix (Pred n) -> Ix n

Instances

Instances details

Thin Ix Source #
Instance details Defined in Data.DeBruijn.Thinning.Fast Methods thin :: forall (n :: Nat) (m :: Nat). (n :<= m) -> Ix n -> Ix m Source # thick :: forall (n :: Nat) (m :: Nat). (n :<= m) -> Ix m -> Maybe (Ix n) Source #
Show (Ix n) Source #
Instance details Defined in Data.DeBruijn.Index.Fast Methods showsPrec :: Int -> Ix n -> ShowS # show :: Ix n -> String # showList :: [Ix n] -> ShowS #
NFData (Ix n) Source #
Instance details Defined in Data.DeBruijn.Index.Fast Methods rnf :: Ix n -> () #
Eq (Ix n) Source #
Instance details Defined in Data.DeBruijn.Index.Fast Methods (==) :: Ix n -> Ix n -> Bool # (/=) :: Ix n -> Ix n -> Bool #

eqIx :: forall (n :: Nat) (m :: Nat). Ix n -> Ix m -> Bool Source #

fromIx :: forall i (n :: Nat). Integral i => Ix n -> i Source #

fromSNat n returns the numeric representation of 'SNat n'.

fromIxRaw :: forall (n :: Nat). Ix n -> IxRep Source #

fromIxRaw n returns the raw numeric representation of 'SNat n'.

isPos :: forall (n :: Nat) a. Ix n -> (Pos n => a) -> a Source #

If any value of type Ix n exists, n must have a predecessor.

thin :: forall (n :: Nat). Ix ('S n) -> Ix n -> Ix ('S n) Source #

Thinning.

thick :: forall (n :: Nat). Ix ('S n) -> Ix ('S n) -> Maybe (Ix n) Source #

Thickening.

inject :: forall (n :: Nat) (m :: Nat). Ix n -> SNat m -> Ix (n + m) Source #

Inject.

raise :: forall (n :: Nat) (m :: Nat). SNat n -> Ix m -> Ix (n + m) Source #

Raise.

Existential Wrapper

data SomeIx Source #

An existential wrapper around indexes.

Constructors

SomeIx
Fields bound :: !(SNat n) index :: !(Ix n)

Instances

Instances details

Show SomeIx Source #
Instance details Defined in Data.DeBruijn.Index.Fast Methods showsPrec :: Int -> SomeIx -> ShowS # show :: SomeIx -> String # showList :: [SomeIx] -> ShowS #
NFData SomeIx Source #
Instance details Defined in Data.DeBruijn.Index.Fast Methods rnf :: SomeIx -> () #
Eq SomeIx Source #
Instance details Defined in Data.DeBruijn.Index.Fast Methods (==) :: SomeIx -> SomeIx -> Bool # (/=) :: SomeIx -> SomeIx -> Bool #

withSomeIx :: (forall (n :: Nat). SNat n -> Ix n -> a) -> SomeIx -> a Source #

toSomeIx :: (Integral n, Integral i) => (n, i) -> SomeIx Source #

toSomeIx n constructs the index n at type Ix n from the number n.

toSomeIx (fromSomeIx i) == i

toSomeIxRaw :: (SNatRep, IxRep) -> SomeIx Source #

toSomeIxRaw n constructs the index n at type Ix n from the Int n.

toSomeIxRaw (fromSomeIxRaw i) == i

fromSomeIx :: (Integral n, Integral i) => SomeIx -> (n, i) Source #

fromSomeSNat n returns the numeric representation of the wrapped index.

fromSomeIxRaw :: SomeIx -> (SNatRep, IxRep) Source #

fromSomeSNat n returns the Int representation of the wrapped index.

Fast

type IxRep = Int Source #

intToIxRep :: Int -> IxRep Source #

Convert an IxRep to an Int.

ixRepToInt :: IxRep -> Int Source #

Convert an IxRep to an Int.

snatRepToIxRep :: SNatRep -> IxRep Source #

Convert an SNatRep to an IxRep.

ixRepToSNatRep :: IxRep -> SNatRep Source #

Convert an IxRep to an SNatRep.

newtype Ix (n :: Nat) Source #

Ix n is the type of DeBruijn indices less than n.

Constructors

UnsafeIx
Fields ixRep :: IxRep

Instances

Instances details

Thin Ix Source #
Instance details Defined in Data.DeBruijn.Thinning.Fast Methods thin :: forall (n :: Nat) (m :: Nat). (n :<= m) -> Ix n -> Ix m Source # thick :: forall (n :: Nat) (m :: Nat). (n :<= m) -> Ix m -> Maybe (Ix n) Source #
Show (Ix n) Source #
Instance details Defined in Data.DeBruijn.Index.Fast Methods showsPrec :: Int -> Ix n -> ShowS # show :: Ix n -> String # showList :: [Ix n] -> ShowS #
NFData (Ix n) Source #
Instance details Defined in Data.DeBruijn.Index.Fast Methods rnf :: Ix n -> () #
Eq (Ix n) Source #
Instance details Defined in Data.DeBruijn.Index.Fast Methods (==) :: Ix n -> Ix n -> Bool # (/=) :: Ix n -> Ix n -> Bool #