module Prelude.Type (
module Prelude,
module Prelude.Type,
module GHC.Prim,
module GHC.TypeLits,
module Prelude.Type.Match,
module Prelude.Type.Integer,
module Prelude.Type.Value
) where
import Prelude.Type.Match
import Prelude.Type.Integer
import Prelude.Type.Value
import qualified Prelude.Type.Families as F
import Prelude(
Bool(False, True),
Maybe(Nothing, Just),
Either(Left, Right),
Ordering(LT, GT, EQ)
)
import GHC.TypeLits (Symbol, Nat)
import GHC.Prim (Constraint)
class Lambda1 (a :: k) (c :: Constraint) (a' :: k) | a' c -> a
instance c => Lambda1 a c a
class Lambda2 (a :: k1) (b :: k2) (c :: Constraint) (a' :: k1) (b' :: k2) | a' b' c -> a b
instance c => Lambda2 a b c a b
class Lambda3 (a :: k1) (b :: k2) (d :: k3) (c :: Constraint) (a' :: k1) (b' :: k2) (d' :: k3) | a' b' d' c -> a b d
instance c => Lambda3 a b d c a b d
class Lambda4 (a :: k1) (b :: k2) (d :: k3) (e :: k4) (c :: Constraint) (a' :: k1) (b' :: k2) (d' :: k3) (e' :: k4) | a' b' d' e' c -> a b d e
instance c => Lambda4 a b d e c a b d e
type family Lambda :: k
type instance Lambda = Lambda1
type instance Lambda = Lambda2
type instance Lambda = Lambda3
type instance Lambda = Lambda4
class If (p :: Bool -> Constraint) (a :: Constraint) (b :: Constraint)
instance (p x, F.If x a b) => If p a b
class Case (a :: k) (c :: [Alternative k Constraint])
instance Error '("Case: No matching alternative for", a) => Case a '[]
instance b => Case a ('[Otherwise b])
instance (Match a x p, Case' p b a cs) => Case a ((x --> b) ': cs)
class Case' (p :: Bool) (b :: Constraint) (a :: k) (cs :: [Alternative k Constraint])
instance b => Case' True b a cs
instance Case a cs => Case' False b a cs
data Alternative a b = (-->) a b | Otherwise b
class Show (a :: k) (b :: [Symbol]) | a -> b
instance Shows a '[] b => Show a b
class Shows (a :: k) (b :: [Symbol]) (c :: [Symbol]) | a b -> c
class Kind (a :: k) (k' :: *) | k -> k', k' -> k
class ((a :: k) == (b :: k)) (p :: Bool) | a b -> p
class ((a :: k) /= (b :: k)) (p :: Bool) | a b -> p
instance ((a == b) p, Not p q) => (a /= b) q
class Compare (a :: k) (b :: k) (o :: Ordering) | a b -> o
class ((a :: k) < (b :: k)) (p :: Bool) | a b -> p
instance (Compare a b o,
Case o [LT --> True ~ p,
Otherwise (False ~ p)])
=> (a < b) p
class ((a :: k) <= (b :: k)) (p :: Bool) | a b -> p
instance (Compare a b o,
Case o [GT --> False ~ p,
Otherwise (True ~ p)])
=> (a <= b) p
class ((a :: k) >= (b :: k)) (p :: Bool) | a b -> p
instance (Compare a b o,
Case o [LT --> False ~ p,
Otherwise (True ~ p)])
=> (a >= b) p
class ((a :: k) > (b :: k)) (p :: Bool) | a b -> p
instance (Compare a b o,
Case o [GT --> True ~ p,
Otherwise (False ~ p)])
=> (a > b) p
class Max (a :: k) (b :: k) (max :: k)
instance (Compare a b o,
Case o [
LT --> (max ~ b),
Otherwise (max ~ a)])
=> Max a b max
class Min (a :: k) (b :: k) (min :: k)
instance (Compare a b o,
Case o [
GT --> (min ~ b),
Otherwise (min ~ a)])
=> Min a b min
class ToEnum (i :: Integer) (a :: k) | k i -> a
class FromEnum (a :: k) (i :: Integer) | a -> i
class Succ (a :: k) (b :: k) | a -> b
instance (FromEnum a i, (i + I 1) j, ToEnum j b) => Succ a b
class Pred (a :: k) (b :: k) | a -> b
instance (FromEnum a i, (i `Minus` I 1) j, ToEnum j b) => Pred a b
class EnumFromTo (a :: k) (b :: k) (l :: [k]) | a b -> l
instance (FromEnum a i,
FromEnum b j,
EnumFromTo i j k,
Map ToEnum k l)
=> EnumFromTo a b l
instance If (b < a) (l ~ '[])
(((I 1) + a) c, EnumFromTo c b k, l ~ (a ': k))
=> EnumFromTo (a :: Integer) b l
class EnumFromThenTo (a :: k) (c :: k) (b :: k) (l :: [k]) | a c b -> l
instance (FromEnum a i,
FromEnum c h,
FromEnum b j,
EnumFromThenTo i h j k,
Map ToEnum k l)
=> EnumFromThenTo a c b l
instance ((c `Minus` a) x, EnumFromToBy a b x l)
=> EnumFromThenTo (a :: Integer) c b l
class EnumFromToBy (a :: k) (b :: k) (c :: k) (l :: [k]) | a b c -> l
instance If (b < a) (l ~ '[])
((c + a) d, EnumFromToBy d b c k, l ~ (a ': k))
=> EnumFromToBy a b c l
class MinBound (a :: k) | k -> a
instance F.MinBound ~ a => MinBound a
class MaxBound (a :: k) | k -> a
instance F.MaxBound ~ a => MaxBound a
instance Shows '() x ("()" ': x)
instance ToEnum Zeros '()
instance FromEnum '() Zeros
instance Kind '() ()
instance ((a :: ()) == b) True
instance Compare '() '() EQ
instance Shows Nothing x ("Nothing" ': x)
instance Shows a x y => Shows (Just a) x ("Just" ': y)
instance FromEnum Nothing Zeros
instance (FromEnum a i, (i + I 1) j) => FromEnum (Just a) j
instance ToEnum Zeros Nothing
instance ((j `Minus` I 1) i, ToEnum i a, e ~ Just a) => ToEnum j e
instance Compare Nothing Nothing EQ
instance Compare Nothing (Just a) LT
instance Compare (Just a) Nothing GT
instance Compare a b o => Compare (Just a) (Just b) o
instance Kind a k => Kind (Just a) (Maybe k)
instance Kind Nothing (Maybe k)
instance (Nothing == Nothing) True
instance (a == b) p => (Just a == Just b) p
instance (Nothing == Just b) False
instance (Just a == Nothing) False
instance Shows True x ("True" ': x)
instance Shows False x ("False" ': x)
instance FromEnum False Zeros
instance FromEnum True (One Zeros)
instance ToEnum Zeros False
instance ToEnum (One Zeros) True
instance o ~ (F.Compare a b) => Compare (a :: Bool) b o
instance Kind (a :: Bool) Bool
instance p ~ (a F.== b) => ((a :: Bool) == b) p
class Not (a :: Bool) (b :: Bool) | a -> b
instance Not True False
instance Not False True
class ((a :: Bool) || (b :: Bool)) (c :: Bool) | a b -> c
instance (False || False) False
instance True ~ p => (a || b) p
class ((a :: Bool) && (b :: Bool)) (c :: Bool) | a b -> c
instance (True && True) True
instance False ~ p => (a && b) p
instance y ~ F.Shows o x => Shows (o :: Ordering) x y
instance i ~ F.FromEnum o => FromEnum (o :: Ordering) i
instance o ~ F.ToEnum i => ToEnum i o
instance o ~ F.Compare a b => Compare (a :: Ordering) b o
instance Kind (a :: Ordering) Ordering
instance TypeEq a b p => ((a :: Ordering) == b) p
instance Shows a x y => Shows (Left a) x ("Left" ': y)
instance Shows a x y => Shows (Right a) x ("Right" ': y)
instance Compare (Left a) (Right b) LT
instance Compare (Right a) (Left b) GT
instance Compare a b o => Compare (Right a) (Right b) o
instance Compare a b o => Compare (Left a) (Left b) o
instance Kind a k => Kind (Left a) (Either k l)
instance Kind a k => Kind (Right a) (Either l k)
instance (a == b) p => (Left a == Left b) p
instance (a == b) p => (Right a == Right b) p
instance (Left a == Right b) False
instance (Right a == Left b) False
instance (Shows a ("," ': y) z, Shows b (")" ': x) y) => Shows '(a, b) x ("(" ': z)
instance (Shows a ("," ': y) z, Shows b ("," ': x) y, Shows c (")" ': w) x) => Shows '(a, b, c) w ("(" ': z)
instance (Shows a ("," ': y) z, Shows b ("," ': x) y, Shows c ("," ': w) x, Shows d (")" ': v) w) => Shows '(a, b, c, d) v ("(" ': z)
instance
(Compare a e o,
Case o [
EQ --> Compare b f r,
o --> o ~ r
])
=> Compare '(a, b) '(e, f) r
instance
(Compare a e o,
Case o [
EQ --> Compare '(b, c) '(f, g) r,
o --> o ~ r
])
=> Compare '(a, b, c) '(e, f, g) r
instance
(Compare a e o,
Case o [
EQ --> Compare '(b, c, d) '(f, g, h) r,
o --> o ~ r
])
=> Compare '(a, b, c, d) '(e, f, g, h) r
instance (Kind a k, Kind b l) => Kind '(a, b) (k, l)
instance (Kind a k, Kind b l, Kind c m) => Kind '(a, b, c) (k, l, m)
instance (Kind a k, Kind b l, Kind c m, Kind d n) => Kind '(a, b, c, d) (k, l, m, n)
instance ((a == w) p, (b == x) q, (p && q) o) =>
('(a, b) == '(w, x)) o
instance ((a == w) p, (b == x) q, (c == y) r, (p && q) n, (n && r) p) =>
('(a, b, c) == '(w, x, y)) o
instance ((a == w) p, (b == x) q, (c == y) r, (d == z) s,
(p && q) m, (r && s) n, (m && n) o) =>
('(a, b, c, d) == '(w, x, y, z)) o
class Fst (p :: (a, b)) (x :: a) | p -> x
instance Fst '(a, b) a
class Snd (p :: (a, b)) (x :: b) | p -> x
instance Snd '(a, b) b
instance Shows (a :: Symbol) x (a ': x)
instance Kind (a :: Nat) Nat
instance Kind (a :: Symbol) Symbol
instance TypeEq a b p => ((a :: Nat) == b) p
instance TypeEq a b p => ((a :: Symbol) == b) p
data StarKind
instance Kind (a :: *) StarKind
instance TypeEq a b p => ((a :: *) == b) p
class Compose1 (f :: k -> l -> Constraint) (g :: j -> k -> Constraint) (x :: j) (z :: l) | f g -> x z
instance (g x y, f y z) => Compose1 f g x z
class Compose2 (f :: k -> l -> m -> Constraint) (g :: j -> k -> Constraint) (x :: j) (z :: l) (a :: m) | f g -> x z
instance (g x y, f y z a) => Compose2 f g x z a
class Compose3 (f :: k -> l -> m -> n -> Constraint) (g :: j -> k -> Constraint) (x :: j) (z :: l) (a :: m) (b :: n) | f g -> x z
instance (g x y, f y z a b) => Compose3 f g x z a b
class Compose4 (f :: k -> l -> m -> n -> o -> Constraint) (g :: j -> k -> Constraint) (x :: j) (z :: l) (a :: m) (b :: n) (c :: o) | f g -> x z
instance (g x y, f y z a b c) => Compose4 f g x z a b c
type O = Compose
type family Compose :: k
type instance Compose = Compose1
type instance Compose = Compose2
type instance Compose = Compose3
type instance Compose = Compose4
class Partial1 (f :: a -> k) (x :: a) (y :: k) | f x -> y
instance Partial1 f x (f x)
class Partial2 (f :: a -> b -> k) (x :: a) (m :: b) (y :: k) | f x m -> y
instance Partial2 f x y (f x y)
class Partial3 (f :: a -> b -> c -> k) (x :: a) (m :: b) (n :: c) (y :: k) | f x m n -> y
instance Partial3 f x y z (f x y z)
class Partial4 (f :: a -> b -> c -> d -> k) (x :: a) (m :: b) (n :: c) (o :: d) (y :: k) | f x m n o -> y
instance Partial4 f x y z a (f x y z a)
type family Partial :: k
type instance Partial = Partial1
type instance Partial = Partial2
type instance Partial = Partial3
type instance Partial = Partial4
class Apply1 (f :: a -> Constraint) (x :: a -> Constraint)
instance (x y, f y) => Apply1 f x
class Apply2 (f :: a -> b -> Constraint) (x :: a -> Constraint) (e :: b)
instance (x y, f y e) => Apply2 f x e
class Apply3 (f :: a -> b -> c -> Constraint) (x :: a -> Constraint) (e :: b) (g :: c)
instance (x y, f y e g) => Apply3 f x e g
class Apply4 (f :: a -> b -> c -> d -> Constraint) (x :: a -> Constraint) (e :: b) (h :: c) (g :: d)
instance (x y, f y e g h) => Apply4 f x e g h
type family (a :: x) $ (b :: y) :: k
type instance a $ b = a b
type instance a $ b = Apply1 a b
type instance a $ b = Apply2 a b
type instance a $ b = Apply3 a b
type instance a $ b = Apply4 a b
class Id (a :: k) (b :: k) | a -> b, b -> a
instance Id a a
class Flip1 (f :: a -> b -> Constraint) (x :: b) (y :: a)
instance f y x => Flip1 f x y
class Flip2 (f :: a -> b -> c -> Constraint) (x :: b) (y :: a) (m :: c)
instance f y x m => Flip2 f x y m
class Flip3 (f :: a -> b -> c -> d -> Constraint) (x :: b) (y :: a) (m :: c) (n :: d)
instance f y x m n => Flip3 f x y m n
class Flip4 (f :: a -> b -> c -> d -> e -> Constraint) (x :: b) (y :: a) (m :: c) (n :: d) (o :: e)
instance f y x m n o => Flip4 f x y m n o
type family Flip :: (x -> y -> k) -> y -> x-> k
type instance Flip = Flip1
type instance Flip = Flip2
type instance Flip = Flip3
type instance Flip = Flip4
class Const1 (a :: k) b (c :: k) | a -> c, c -> a
instance Const1 a b a
class Const2 (a :: k) b c (d :: k) | a -> d, d -> a
instance Const2 a b c a
class Const3 (a :: k) b c d (e :: k) | a -> e, e -> a
instance Const3 a b c d a
class Const4 (a :: k) b c d e (f :: k) | a -> f, f -> a
instance Const4 a b c d e a
type family Const :: k
type instance Const = Const1
type instance Const = Const2
type instance Const = Const3
type instance Const = Const4
class Until (p :: a -> Bool -> Constraint)
(f :: a -> a -> Constraint)
(x :: a)
(y :: a)
instance If (p x) (x ~ y) (f x x', Until p f x' y)
=> Until p f x y
instance Shows '[] x ("[]" ': x)
instance (Shows a y z, ShowsTail l ("]" ': x) y) => Shows (a ': l) x ("[" ': z)
class ShowsTail (a :: [k]) (x :: [Symbol]) (y :: [Symbol]) | a x -> y
instance ShowsTail '[] x ("]" ': x)
instance (Shows a y z, ShowsTail l x y) => ShowsTail (a ': l) x ("," ': z)
instance Compare '[] '[] EQ
instance Compare '[] (x ': xs) LT
instance Compare (x ': xs) '[] GT
instance
(Compare x y o,
Case o [
EQ --> Compare xs ys r,
o --> o ~ r
])
=> Compare (x ': xs) (y ': ys) r
instance (Kind x k) => Kind (x ': xs) [k]
instance Kind '[] [k]
instance ('[] == '[]) True
instance ((x == y) p, (xs == zs) q, (p && q) o) =>
((x ': xs) == (y ': ys)) o
class Map (f :: a -> c -> Constraint) (l :: [a]) (j :: [c]) | f l -> j
instance Map f '[] '[]
instance (f x y, Map f xs ys)
=> Map f (x ': xs) (y ': ys)
class FoldR (f :: a -> b -> b -> Constraint)
(nil :: b) (list :: [a]) (ret :: b) | f nil list -> ret
instance Id nil ret => FoldR f nil '[] ret
instance (FoldR f nil xs tail, f x tail ret)
=> FoldR f nil (x ': xs) ret
class FoldL (f :: b -> a -> b -> Constraint)
(accum :: b) (list :: [a]) (ret :: b) | f accum list -> ret
instance FoldL f accum '[] accum
instance (f accum x accum',
FoldL f accum' xs ret)
=> FoldL f accum (x ': xs) ret
class Head (l :: [a]) (x :: a) | l -> x
instance Error "Head: empty list" => Head '[] a
instance Head (x ': xs) x
class Tail (l :: [a]) (x :: [a]) | l -> x
instance Error "Tail: empty list" => Tail '[] a
instance Tail (x ': xs) xs
class Last (l :: [a]) (x :: a) | l -> x
instance Error "Last: empty list" => Last '[] a
instance a ~ b => Last '[a] b
instance Last (y ': xs) a => Last (x ': y ': xs) a
class Init (l :: [a]) (x :: [a]) | l -> x
instance Error "Init: empty list" => Init '[] a
instance Init '[a] '[]
instance Init (y ': xs) a => Init (x ': y ': xs) (x ': a)
class Null (l :: [a]) (p :: Bool) | l -> p
instance Null '[] True
instance Null (x ': xs) False
class Length (l :: [a]) (i :: Integer) | l -> i
instance Length '[] Zeros
instance (Length xs n, (I 1 + n) i) => Length (x ': xs) i
class ((l :: [a]) !! (n :: Integer)) (x :: a) | l n -> x
instance Error "(!!): index too large" => ('[] !! n) x
instance y ~ x => ((x ': xs) !! Zeros) y
instance (xs !! i) y
=> ((x ': xs) !! One i) y
instance (Drop i xs ys, (ys !! i) y)
=> ((x ': xs) !! Zero i) y
class Drop (i :: Integer) (l :: [a]) (k :: [a]) | i l -> k
instance a ~ b => Drop Zeros a b
instance Error "Drop: negative count" => Drop Ones a b
instance Drop i '[] '[]
instance (Drop i xs ys, Drop i ys zs) => Drop (One i) (x ': xs) zs
instance (Drop i xs ys, Drop i ys zs) => Drop (Zero i) xs zs
class ((a :: [k]) ++ (b :: [k])) (c :: [k]) | a b -> c
instance ('[] ++ b) b
instance (a ++ b) c => ((x ': a) ++ b) (x ': c)
type Concat = FoldR (++) '[]
class ConcatMap (f :: k -> [x] -> Constraint) (a :: [k]) (b :: [x]) | f a -> b
instance (Map f l k, Concat k j) => ConcatMap f l j
class ScanL (f :: a -> b -> a -> Constraint) (x :: a) (l :: [b]) (k :: [a]) | f x l -> k
instance ScanL f x '[] '[x]
instance (f x y z, ScanL f z ys zs) => ScanL f x (y ': ys) (x ': zs)
class ScanR (f :: a -> b -> b -> Constraint) (x :: b) (l :: [a]) (k :: [b]) | f x l -> k
instance ScanR f q '[] '[q]
instance (f x z y, ScanR f q xs (z ': ys)) => ScanR f q (x ': xs) (y ': z ': ys)
class ScanFold1 (c :: a -> b -> [b] -> c -> Constraint) (x :: a) (y :: [b]) (z :: c) | c x y -> z
instance c x y ys z => ScanFold1 c x (y ': ys) z
type ScanL1 = ScanFold1 ScanL
type ScanR1 = ScanFold1 ScanR
type FoldL1 = ScanFold1 FoldL
type FoldR1 = ScanFold1 FoldR
class Replicate (i :: Integer) (a :: k) (l :: [k]) | i a -> l
instance Replicate Zeros a '[]
instance (Replicate (i `F.Minus` I 1) a as, l ~ (a ': as)) => Replicate i a l
class Take (i :: Integer) (a :: [k]) (b :: [k]) | i a -> b
instance Take i '[] '[]
instance (F.If (F.IsZero i) (b ~ '[]) (Take (i `F.Minus` I 1) xs t, b ~ (x ': t))) => Take i (x ': xs) b
class SplitAt (i :: Integer) (a :: [k]) (b :: ([k], [k]))
instance (Take i a x, Drop i a y) => SplitAt i a '(x, y)
class TakeWhile (f :: a -> Bool -> Constraint) (x :: [a]) (y :: [a])
instance TakeWhile f '[] '[]
instance If (f x) (TakeWhile f xs zs, ys ~ (x ': zs)) (ys ~ '[]) => TakeWhile f (x ': xs) ys
class DropWhile (f :: a -> Bool -> Constraint) (x :: [a]) (y :: [a])
instance DropWhile f '[] '[]
instance If (f x) (DropWhile f xs ys) (ys ~ (x ': xs)) => DropWhile f (x ': xs) ys
class Span (f :: a -> Bool -> Constraint) (x :: [a]) (y :: ([a], [a]))
instance (TakeWhile f a b, DropWhile f a c) => Span f a '(b, c)
class Break (f :: a -> Bool -> Constraint) (x :: [a]) (y :: ([a], [a]))
instance Break f '[] '( '[], '[])
instance If (f x)
(y ~ '( '[], x ': xs))
(Break f xs '(a, b), y ~ '(x ': a, b))
=> Break f (x ': xs) y
type And = FoldR (&&) True
type Or = FoldR (||) False
type Any = (Compose1 Or) `Compose2` Partial1 Map
type All = (Compose1 And) `Compose2` Partial1 Map
class Elem (a :: k) (b :: [k]) (p :: Bool) | a b -> p
instance Elem a '[] False
instance If (a == x) (p ~ True) (Elem a xs p) => Elem a (x ': xs) p
type NotElem = (Compose1 Not) `Compose2` Partial1 Elem
type Maximum = FoldL1 Max
instance Shows Zeros x ("0" ': x)
instance If (i > I 0)
(ShowsInteger i x y)
(Negate i j, ShowsInteger j x y', y ~ ("-" ': y'))
=> Shows (i :: Integer) x y
class ShowsInteger (i :: Integer) (x :: [Symbol]) (y :: [Symbol]) | i x -> y
instance ShowsInteger Zeros x x
instance (QuotRem' i (I 10) q r,
ShowsInteger q (F.Digit r ': x) y)
=> ShowsInteger i x y
instance (Ones == Ones) True
instance (Zeros == Zeros) True
instance (i == j) p => (One i == One j) p
instance (i == j) p => (Zero i == Zero j) p
instance p ~ False => ((i :: Integer) == j) p
instance FromEnum i (i :: Integer)
instance ToEnum i (i :: Integer)
instance Kind (a :: Integer) Integer
class ((a :: k) + (b :: k)) (sum :: k) | a b -> sum
instance AddWithCarry False a b sum => (a + b) sum
class AddWithCarry (carry :: Bool) (a :: Integer) (b :: Integer)
(sum :: Integer) | carry a b -> sum
instance AddWithCarry False Zeros a a
instance AddWithCarry False Ones Zeros Ones
instance AddWithCarry True Ones a a
instance AddWithCarry True Zeros Ones Zeros
instance (F.Add3 carry (IntegerHead a) (IntegerHead b) ~ '(head, carry'),
IntegerTail a ~ a',
IntegerTail b ~ b',
AddWithCarry carry' a' b' tail,
sum ~ IntegerCons head tail)
=> AddWithCarry carry a b sum
class Minus (a :: k) (b :: k) (dif :: k) | a b -> dif
instance (Complement b cb, AddWithCarry True a cb dif)
=> Minus a b (dif :: Integer)
class Negate (a :: k) (b :: k) | a -> b
instance (Complement a b,
(b + (I 1)) c)
=> Negate a (c :: Integer)
class ((a :: k) * (b :: k)) (prod :: k) | a b -> prod
instance (Zeros * a) Zeros
instance Negate a prod => (Ones * a) prod
instance (One Zeros * a) a
instance ((i * a) b, prod ~ IntegerCons False b) => (Zero i * a) prod
instance ((i * a) b,
b' ~ IntegerCons False b,
(a + b') prod)
=> (One i * a) prod
class Signum (a :: k) (b :: k) | a -> b
instance Signum Zeros Zeros
instance Signum i s => Signum (Zero i) s
instance Signum' i s => Signum i s
class Signum' (a :: k) (b :: k) | a -> b
instance Signum' Zeros (One Zeros)
instance Signum' Ones Ones
instance Signum' i s => Signum' (Zero i) s
instance Signum' i s => Signum' (One i) s
class Abs (a :: k) (b :: k) | a -> b
instance (Signum a s,
Case s [Ones --> Negate a b,
Otherwise (a ~ b)])
=> Abs a b
class Subtract (a :: k) (b :: k) (dif :: k) | a b -> dif
instance Minus b a dif => Subtract a b dif
class Even (a :: k) (p :: Bool) | a -> p
instance (p ~ (IntegerHead i)) => Even i p
class Odd (a :: k) (p :: Bool) | a -> p
instance Odd Ones True
instance Odd Zeros False
instance Odd (One i) True
instance Odd (Zero i) False
class Gcd (a :: k) (b :: k) (c :: k) | a b -> c
instance Error "Gcd 0 0 is undefined" => Gcd Zeros Zeros c
instance (Abs x x',
Abs y y',
Gcd' x' y' z)
=> Gcd x y z
class Gcd' (x :: Integer) (y :: Integer) (z :: Integer) | x y -> z
instance Gcd' x Zeros x
instance (Rem x y r,
Gcd' y r z)
=> Gcd' x y z
instance (Minus a b d,
Signum d s,
Case s [Ones --> p ~ LT,
Zeros --> p ~ EQ,
One Zeros --> p ~ GT,
Otherwise (Error '("Signum returned", s))])
=> Compare (a :: Integer) b p
class Error a
instance ERROR a => Error a
class ERROR a
class AsKindOf (a :: k) (b :: k) | a -> b, b -> a
instance AsKindOf a b
class Xor (a :: k) (b :: k) (c :: k) | a b -> c, b c -> c, a c -> b
instance c ~ F.Xor a b => Xor (a :: Bool) b c
instance Xor Zeros a a
instance Complement a b => Xor Ones a b
instance (Xor (IntegerHead a) (IntegerHead b) c,
Xor (IntegerTail a) (IntegerTail b) d,
e ~ IntegerCons c d)
=> Xor (a :: Integer) b e
class ((a :: k) .&. (b :: k)) (c :: k) | a b -> c
instance c ~ (a F..&. b) => (a .&. b) c
instance (Zeros .&. a) Zeros
instance (Ones .&. a) a
instance ((True .&. (IntegerHead b)) c,
(a .&. (IntegerTail b)) d,
e ~ IntegerCons c d)
=> ((One a) .&. b) (e :: Integer)
instance ((False .&. (IntegerHead b)) c,
(a .&. (IntegerTail b)) d,
e ~ IntegerCons c d)
=> ((Zero a) .&. b) (e :: Integer)
class Complement (a :: k) (b :: k) | a -> b, b -> a
instance Complement True False
instance Complement False True
instance Complement Zeros Ones
instance Complement Ones Zeros
instance (Complement (IntegerHead a) head,
Complement (IntegerTail a) tail,
b ~ IntegerCons head tail)
=> Complement a (b :: Integer)
class QuotRem (a :: k) (b :: k) (c :: (k, k)) | a b -> c
instance Error "Division by zero" => QuotRem (a :: Integer) Zeros b
instance (Abs a a', Abs b b',
QuotRem' a' b' q r,
Signum a sa, Signum b sb,
(sa * r) rem,
(sa * q) q',
(sb * q') quot)
=> QuotRem (a :: Integer) b '(quot, rem)
class QuotRem' (a :: Integer) (b :: Integer) (q :: Integer) (r :: Integer)
instance (If (a < b)
('(q, r) ~ '(I 0, a))
((I 2 * b) b2,
QuotRem' a b2 q' r',
(q' * I 2) q'',
If (r' >= b)
((I 1 + q'') q,
(r' `Minus` b) r)
(q ~ q'', r' ~ r)))
=> QuotRem' a b q r
class Rem (a :: k) (b :: k) (c :: k) | a b -> c
instance (QuotRem a b '(q, r)) => Rem a b (r :: Integer)
class Quot (a :: k) (b :: k) (c :: k) | a b -> c
instance (QuotRem a b '(q, r)) => Quot a b (q :: Integer)
class TypeEq' '() x y b => TypeEq (x :: k) (y :: k) (b :: Bool) | x y -> b
class TypeEq' (q :: ()) (x :: k) (y :: k) (b :: Bool) | q x y -> b
class TypeEq'' (q :: ()) (x :: k) (y :: k) (b :: Bool) | q x y -> b
instance TypeEq' '() x y b => TypeEq x y b
instance b ~ True => TypeEq' '() x x b
instance TypeEq'' q x y b => TypeEq' q x y b
instance TypeEq'' '() x y False