singletons-2.7: tests/compile-and-dump/Singletons/Nat.golden
Singletons/Nat.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| plus :: Nat -> Nat -> Nat
plus Zero m = m
plus (Succ n) m = Succ (plus n m)
pred :: Nat -> Nat
pred Zero = Zero
pred (Succ n) = n
data Nat
where
Zero :: Nat
Succ :: Nat -> Nat
deriving (Eq, Show, Read, Ord) |]
======>
data Nat
where
Zero :: Nat
Succ :: Nat -> Nat
deriving (Eq, Show, Read, Ord)
plus :: Nat -> Nat -> Nat
plus Zero m = m
plus (Succ n) m = Succ ((plus n) m)
pred :: Nat -> Nat
pred Zero = Zero
pred (Succ n) = n
type ZeroSym0 = Zero :: Nat
type SuccSym0 :: (~>) Nat Nat
data SuccSym0 a0123456789876543210
where
SuccSym0KindInference :: SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
SuccSym0 a0123456789876543210
type instance Apply SuccSym0 a0123456789876543210 = SuccSym1 a0123456789876543210
instance SuppressUnusedWarnings SuccSym0 where
suppressUnusedWarnings = snd (((,) SuccSym0KindInference) ())
type SuccSym1 (a0123456789876543210 :: Nat) =
Succ a0123456789876543210 :: Nat
type PredSym0 :: (~>) Nat Nat
data PredSym0 a0123456789876543210
where
PredSym0KindInference :: SameKind (Apply PredSym0 arg) (PredSym1 arg) =>
PredSym0 a0123456789876543210
type instance Apply PredSym0 a0123456789876543210 = PredSym1 a0123456789876543210
instance SuppressUnusedWarnings PredSym0 where
suppressUnusedWarnings = snd (((,) PredSym0KindInference) ())
type PredSym1 (a0123456789876543210 :: Nat) =
Pred a0123456789876543210 :: Nat
type PlusSym0 :: (~>) Nat ((~>) Nat Nat)
data PlusSym0 a0123456789876543210
where
PlusSym0KindInference :: SameKind (Apply PlusSym0 arg) (PlusSym1 arg) =>
PlusSym0 a0123456789876543210
type instance Apply PlusSym0 a0123456789876543210 = PlusSym1 a0123456789876543210
instance SuppressUnusedWarnings PlusSym0 where
suppressUnusedWarnings = snd (((,) PlusSym0KindInference) ())
type PlusSym1 :: Nat -> (~>) Nat Nat
data PlusSym1 a0123456789876543210 a0123456789876543210
where
PlusSym1KindInference :: SameKind (Apply (PlusSym1 a0123456789876543210) arg) (PlusSym2 a0123456789876543210 arg) =>
PlusSym1 a0123456789876543210 a0123456789876543210
type instance Apply (PlusSym1 a0123456789876543210) a0123456789876543210 = PlusSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (PlusSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) PlusSym1KindInference) ())
type PlusSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) =
Plus a0123456789876543210 a0123456789876543210 :: Nat
type Pred :: Nat -> Nat
type family Pred a where
Pred Zero = ZeroSym0
Pred (Succ n) = n
type Plus :: Nat -> Nat -> Nat
type family Plus a a where
Plus Zero m = m
Plus (Succ n) m = Apply SuccSym0 (Apply (Apply PlusSym0 n) m)
type ShowsPrec_0123456789876543210 :: GHC.Types.Nat
-> Nat -> GHC.Types.Symbol -> GHC.Types.Symbol
type family ShowsPrec_0123456789876543210 a a a where
ShowsPrec_0123456789876543210 _ Zero a_0123456789876543210 = Apply (Apply ShowStringSym0 "Zero") a_0123456789876543210
ShowsPrec_0123456789876543210 p_0123456789876543210 (Succ arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (Data.Singletons.Prelude.Num.FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Succ ")) (Apply (Apply ShowsPrecSym0 (Data.Singletons.Prelude.Num.FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210
type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Types.Nat ((~>) Nat ((~>) GHC.Types.Symbol GHC.Types.Symbol))
data ShowsPrec_0123456789876543210Sym0 a0123456789876543210
where
ShowsPrec_0123456789876543210Sym0KindInference :: SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
ShowsPrec_0123456789876543210Sym0 a0123456789876543210
type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210
instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) ShowsPrec_0123456789876543210Sym0KindInference) ())
type ShowsPrec_0123456789876543210Sym1 :: GHC.Types.Nat
-> (~>) Nat ((~>) GHC.Types.Symbol GHC.Types.Symbol)
data ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
where
ShowsPrec_0123456789876543210Sym1KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) =>
ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd (((,) ShowsPrec_0123456789876543210Sym1KindInference) ())
type ShowsPrec_0123456789876543210Sym2 :: GHC.Types.Nat
-> Nat -> (~>) GHC.Types.Symbol GHC.Types.Symbol
data ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
where
ShowsPrec_0123456789876543210Sym2KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) =>
ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings
= snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ())
type ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: Nat) (a0123456789876543210 :: GHC.Types.Symbol) =
ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 :: GHC.Types.Symbol
instance PShow Nat where
type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
type Compare_0123456789876543210 :: Nat -> Nat -> Ordering
type family Compare_0123456789876543210 a a where
Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) NilSym0
Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)
Compare_0123456789876543210 Zero (Succ _) = LTSym0
Compare_0123456789876543210 (Succ _) Zero = GTSym0
type Compare_0123456789876543210Sym0 :: (~>) Nat ((~>) Nat Ordering)
data Compare_0123456789876543210Sym0 a0123456789876543210
where
Compare_0123456789876543210Sym0KindInference :: SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
Compare_0123456789876543210Sym0 a0123456789876543210
type instance Apply Compare_0123456789876543210Sym0 a0123456789876543210 = Compare_0123456789876543210Sym1 a0123456789876543210
instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) Compare_0123456789876543210Sym0KindInference) ())
type Compare_0123456789876543210Sym1 :: Nat -> (~>) Nat Ordering
data Compare_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
where
Compare_0123456789876543210Sym1KindInference :: SameKind (Apply (Compare_0123456789876543210Sym1 a0123456789876543210) arg) (Compare_0123456789876543210Sym2 a0123456789876543210 arg) =>
Compare_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (Compare_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Compare_0123456789876543210Sym1KindInference) ())
type Compare_0123456789876543210Sym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) =
Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 :: Ordering
instance POrd Nat where
type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
type Equals_0123456789876543210 :: Nat -> Nat -> Bool
type family Equals_0123456789876543210 a b where
Equals_0123456789876543210 Zero Zero = TrueSym0
Equals_0123456789876543210 (Succ a) (Succ b) = (==) a b
Equals_0123456789876543210 (_ :: Nat) (_ :: Nat) = FalseSym0
instance PEq Nat where
type (==) a b = Equals_0123456789876543210 a b
sPred ::
forall (t :: Nat). Sing t -> Sing (Apply PredSym0 t :: Nat)
sPlus ::
forall (t :: Nat) (t :: Nat).
Sing t -> Sing t -> Sing (Apply (Apply PlusSym0 t) t :: Nat)
sPred SZero = SZero
sPred (SSucc (sN :: Sing n)) = sN
sPlus SZero (sM :: Sing m) = sM
sPlus (SSucc (sN :: Sing n)) (sM :: Sing m)
= (applySing ((singFun1 @SuccSym0) SSucc))
((applySing ((applySing ((singFun2 @PlusSym0) sPlus)) sN)) sM)
instance SingI (PredSym0 :: (~>) Nat Nat) where
sing = (singFun1 @PredSym0) sPred
instance SingI (PlusSym0 :: (~>) Nat ((~>) Nat Nat)) where
sing = (singFun2 @PlusSym0) sPlus
instance SingI d =>
SingI (PlusSym1 (d :: Nat) :: (~>) Nat Nat) where
sing = (singFun1 @(PlusSym1 (d :: Nat))) (sPlus (sing @d))
data SNat :: Nat -> GHC.Types.Type
where
SZero :: SNat (Zero :: Nat)
SSucc :: forall (n :: Nat). (Sing n) -> SNat (Succ n :: Nat)
type instance Sing @Nat = SNat
instance SingKind Nat where
type Demote Nat = Nat
fromSing SZero = Zero
fromSing (SSucc b) = Succ (fromSing b)
toSing Zero = SomeSing SZero
toSing (Succ (b :: Demote Nat))
= case toSing b :: SomeSing Nat of {
SomeSing c -> SomeSing (SSucc c) }
instance SShow Nat => SShow Nat where
sShowsPrec ::
forall (t1 :: GHC.Types.Nat) (t2 :: Nat) (t3 :: GHC.Types.Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat ((~>) Nat ((~>) GHC.Types.Symbol GHC.Types.Symbol))
-> GHC.Types.Type) t1) t2) t3)
sShowsPrec
_
SZero
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= (applySing
((applySing ((singFun2 @ShowStringSym0) sShowString))
(sing :: Sing "Zero")))
sA_0123456789876543210
sShowsPrec
(sP_0123456789876543210 :: Sing p_0123456789876543210)
(SSucc (sArg_0123456789876543210 :: Sing arg_0123456789876543210))
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= (applySing
((applySing
((applySing ((singFun3 @ShowParenSym0) sShowParen))
((applySing
((applySing ((singFun2 @(>@#@$)) (%>))) sP_0123456789876543210))
(Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 10)))))
((applySing
((applySing ((singFun3 @(.@#@$)) (%.)))
((applySing ((singFun2 @ShowStringSym0) sShowString))
(sing :: Sing "Succ "))))
((applySing
((applySing ((singFun3 @ShowsPrecSym0) sShowsPrec))
(Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 11))))
sArg_0123456789876543210))))
sA_0123456789876543210
instance SOrd Nat => SOrd Nat where
sCompare ::
forall (t1 :: Nat) (t2 :: Nat).
Sing t1
-> Sing t2
-> Sing (Apply (Apply (CompareSym0 :: TyFun Nat ((~>) Nat Ordering)
-> GHC.Types.Type) t1) t2)
sCompare SZero SZero
= (applySing
((applySing
((applySing ((singFun3 @FoldlSym0) sFoldl))
((singFun2 @ThenCmpSym0) sThenCmp)))
SEQ))
Data.Singletons.Prelude.Instances.SNil
sCompare
(SSucc (sA_0123456789876543210 :: Sing a_0123456789876543210))
(SSucc (sB_0123456789876543210 :: Sing b_0123456789876543210))
= (applySing
((applySing
((applySing ((singFun3 @FoldlSym0) sFoldl))
((singFun2 @ThenCmpSym0) sThenCmp)))
SEQ))
((applySing
((applySing
((singFun2 @(:@#@$))
Data.Singletons.Prelude.Instances.SCons))
((applySing
((applySing ((singFun2 @CompareSym0) sCompare))
sA_0123456789876543210))
sB_0123456789876543210)))
Data.Singletons.Prelude.Instances.SNil)
sCompare SZero (SSucc _) = SLT
sCompare (SSucc _) SZero = SGT
instance SEq Nat => SEq Nat where
(%==) SZero SZero = STrue
(%==) SZero (SSucc _) = SFalse
(%==) (SSucc _) SZero = SFalse
(%==) (SSucc a) (SSucc b) = ((%==) a) b
instance SDecide Nat => SDecide Nat where
(%~) SZero SZero = Proved Refl
(%~) SZero (SSucc _) = Disproved (\ x -> case x of)
(%~) (SSucc _) SZero = Disproved (\ x -> case x of)
(%~) (SSucc a) (SSucc b)
= case ((%~) a) b of
Proved Refl -> Proved Refl
Disproved contra
-> Disproved (\ refl -> case refl of { Refl -> contra Refl })
instance SDecide Nat =>
Data.Type.Equality.TestEquality (SNat :: Nat
-> GHC.Types.Type) where
Data.Type.Equality.testEquality
= Data.Singletons.Decide.decideEquality
instance SDecide Nat =>
Data.Type.Coercion.TestCoercion (SNat :: Nat
-> GHC.Types.Type) where
Data.Type.Coercion.testCoercion
= Data.Singletons.Decide.decideCoercion
instance Data.Singletons.ShowSing.ShowSing Nat =>
Show (SNat (z :: Nat)) where
showsPrec _ SZero = showString "SZero"
showsPrec
p_0123456789876543210
(SSucc (arg_0123456789876543210 :: Sing argTy_0123456789876543210))
= (showParen (((>) p_0123456789876543210) 10))
(((.) (showString "SSucc "))
((showsPrec 11) arg_0123456789876543210)) ::
Data.Singletons.ShowSing.ShowSing' argTy_0123456789876543210 =>
ShowS
instance SingI Zero where
sing = SZero
instance SingI n => SingI (Succ (n :: Nat)) where
sing = SSucc sing
instance SingI (SuccSym0 :: (~>) Nat Nat) where
sing = (singFun1 @SuccSym0) SSucc