singletons-2.4: tests/compile-and-dump/Singletons/Nat.ghc84.template
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
type SuccSym1 (t :: Nat) = Succ t
instance SuppressUnusedWarnings SuccSym0 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) SuccSym0KindInference) GHC.Tuple.())
data SuccSym0 (l :: TyFun Nat Nat)
= forall arg. SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
SuccSym0KindInference
type instance Apply SuccSym0 l = Succ l
type PredSym1 (t :: Nat) = Pred t
instance SuppressUnusedWarnings PredSym0 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) PredSym0KindInference) GHC.Tuple.())
data PredSym0 (l :: TyFun Nat Nat)
= forall arg. SameKind (Apply PredSym0 arg) (PredSym1 arg) =>
PredSym0KindInference
type instance Apply PredSym0 l = Pred l
type PlusSym2 (t :: Nat) (t :: Nat) = Plus t t
instance SuppressUnusedWarnings PlusSym1 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) PlusSym1KindInference) GHC.Tuple.())
data PlusSym1 (l :: Nat) (l :: TyFun Nat Nat)
= forall arg. SameKind (Apply (PlusSym1 l) arg) (PlusSym2 l arg) =>
PlusSym1KindInference
type instance Apply (PlusSym1 l) l = Plus l l
instance SuppressUnusedWarnings PlusSym0 where
suppressUnusedWarnings
= snd ((GHC.Tuple.(,) PlusSym0KindInference) GHC.Tuple.())
data PlusSym0 (l :: TyFun Nat (TyFun Nat Nat -> GHC.Types.Type))
= forall arg. SameKind (Apply PlusSym0 arg) (PlusSym1 arg) =>
PlusSym0KindInference
type instance Apply PlusSym0 l = PlusSym1 l
type family Pred (a :: Nat) :: Nat where
Pred Zero = ZeroSym0
Pred (Succ n) = n
type family Plus (a :: Nat) (a :: Nat) :: Nat where
Plus Zero m = m
Plus (Succ n) m = Apply SuccSym0 (Apply (Apply PlusSym0 n) m)
type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (a :: Nat) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol 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_0123456789876543210Sym3 (t :: GHC.Types.Nat) (t :: Nat) (t :: GHC.Types.Symbol) =
ShowsPrec_0123456789876543210 t t t
instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym2 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) ShowsPrec_0123456789876543210Sym2KindInference)
GHC.Tuple.())
data ShowsPrec_0123456789876543210Sym2 (l :: GHC.Types.Nat) (l :: Nat) (l :: TyFun GHC.Types.Symbol GHC.Types.Symbol)
= forall arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym2 l l) arg) (ShowsPrec_0123456789876543210Sym3 l l arg) =>
ShowsPrec_0123456789876543210Sym2KindInference
type instance Apply (ShowsPrec_0123456789876543210Sym2 l l) l = ShowsPrec_0123456789876543210 l l l
instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym1 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) ShowsPrec_0123456789876543210Sym1KindInference)
GHC.Tuple.())
data ShowsPrec_0123456789876543210Sym1 (l :: GHC.Types.Nat) (l :: TyFun Nat (TyFun GHC.Types.Symbol GHC.Types.Symbol
-> GHC.Types.Type))
= forall arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym1 l) arg) (ShowsPrec_0123456789876543210Sym2 l arg) =>
ShowsPrec_0123456789876543210Sym1KindInference
type instance Apply (ShowsPrec_0123456789876543210Sym1 l) l = ShowsPrec_0123456789876543210Sym2 l l
instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) ShowsPrec_0123456789876543210Sym0KindInference)
GHC.Tuple.())
data ShowsPrec_0123456789876543210Sym0 (l :: TyFun GHC.Types.Nat (TyFun Nat (TyFun GHC.Types.Symbol GHC.Types.Symbol
-> GHC.Types.Type)
-> GHC.Types.Type))
= forall arg. SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
ShowsPrec_0123456789876543210Sym0KindInference
type instance Apply ShowsPrec_0123456789876543210Sym0 l = ShowsPrec_0123456789876543210Sym1 l
instance PShow Nat where
type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
type family Compare_0123456789876543210 (a :: Nat) (a :: Nat) :: Ordering where
Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) '[])
Compare_0123456789876543210 Zero (Succ _) = LTSym0
Compare_0123456789876543210 (Succ _) Zero = GTSym0
type Compare_0123456789876543210Sym2 (t :: Nat) (t :: Nat) =
Compare_0123456789876543210 t t
instance SuppressUnusedWarnings Compare_0123456789876543210Sym1 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) Compare_0123456789876543210Sym1KindInference)
GHC.Tuple.())
data Compare_0123456789876543210Sym1 (l :: Nat) (l :: TyFun Nat Ordering)
= forall arg. SameKind (Apply (Compare_0123456789876543210Sym1 l) arg) (Compare_0123456789876543210Sym2 l arg) =>
Compare_0123456789876543210Sym1KindInference
type instance Apply (Compare_0123456789876543210Sym1 l) l = Compare_0123456789876543210 l l
instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd
((GHC.Tuple.(,) Compare_0123456789876543210Sym0KindInference)
GHC.Tuple.())
data Compare_0123456789876543210Sym0 (l :: TyFun Nat (TyFun Nat Ordering
-> GHC.Types.Type))
= forall arg. SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
Compare_0123456789876543210Sym0KindInference
type instance Apply Compare_0123456789876543210Sym0 l = Compare_0123456789876543210Sym1 l
instance POrd Nat where
type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
type family Equals_0123456789876543210 (a :: Nat) (b :: Nat) :: Bool 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)
data instance Sing (z :: Nat)
where
SZero :: Sing Zero
SSucc :: forall (n :: Nat). (Sing (n :: Nat)) -> Sing (Succ n)
type SNat = (Sing :: Nat -> GHC.Types.Type)
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 (TyFun Nat (TyFun GHC.Types.Symbol GHC.Types.Symbol
-> GHC.Types.Type)
-> GHC.Types.Type)
-> 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 (TyFun Nat Ordering
-> GHC.Types.Type)
-> 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 Data.Singletons.ShowSing.ShowSing Nat =>
Data.Singletons.ShowSing.ShowSing Nat where
Data.Singletons.ShowSing.showsSingPrec _ SZero = showString "SZero"
Data.Singletons.ShowSing.showsSingPrec
p_0123456789876543210
(SSucc arg_0123456789876543210)
= (showParen (((>) p_0123456789876543210) 10))
(((.) (showString "SSucc "))
((Data.Singletons.ShowSing.showsSingPrec 11)
arg_0123456789876543210))
instance Data.Singletons.ShowSing.ShowSing Nat =>
Show (Sing (z :: Nat)) where
showsPrec = Data.Singletons.ShowSing.showsSingPrec
instance SingI Zero where
sing = SZero
instance SingI n => SingI (Succ (n :: Nat)) where
sing = SSucc sing