singletons-2.6: tests/compile-and-dump/InsertionSort/InsertionSortImp.ghc88.template
InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
singletons [d| data Nat = Zero | Succ Nat |]
======>
data Nat = Zero | Succ Nat
type ZeroSym0 = Zero
type SuccSym1 (t0123456789876543210 :: Nat) =
Succ t0123456789876543210
instance SuppressUnusedWarnings SuccSym0 where
suppressUnusedWarnings = snd (((,) SuccSym0KindInference) ())
data SuccSym0 :: (~>) Nat Nat
where
SuccSym0KindInference :: forall t0123456789876543210
arg. SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
SuccSym0 t0123456789876543210
type instance Apply SuccSym0 t0123456789876543210 = Succ t0123456789876543210
data SNat :: Nat -> Type
where
SZero :: SNat Zero
SSucc :: forall (n :: Nat). (Sing (n :: Nat)) -> SNat (Succ n)
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 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
InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| leq :: Nat -> Nat -> Bool
leq Zero _ = True
leq (Succ _) Zero = False
leq (Succ a) (Succ b) = leq a b
insert :: Nat -> [Nat] -> [Nat]
insert n [] = [n]
insert n (h : t)
= if leq n h then (n : h : t) else h : (insert n t)
insertionSort :: [Nat] -> [Nat]
insertionSort [] = []
insertionSort (h : t) = insert h (insertionSort t) |]
======>
leq :: Nat -> Nat -> Bool
leq Zero _ = True
leq (Succ _) Zero = False
leq (Succ a) (Succ b) = (leq a) b
insert :: Nat -> [Nat] -> [Nat]
insert n [] = [n]
insert n (h : t)
= if (leq n) h then (n : (h : t)) else (h : (insert n) t)
insertionSort :: [Nat] -> [Nat]
insertionSort [] = []
insertionSort (h : t) = (insert h) (insertionSort t)
type Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210 =
Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym2 h0123456789876543210 n0123456789876543210) where
suppressUnusedWarnings
= snd
(((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference)
())
data Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210 t0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference :: forall n0123456789876543210
h0123456789876543210
t0123456789876543210
arg. SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210 t0123456789876543210
type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 h0123456789876543210 n0123456789876543210) t0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 h0123456789876543210 n0123456789876543210 t0123456789876543210
instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210) where
suppressUnusedWarnings
= snd
(((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference)
())
data Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference :: forall n0123456789876543210
h0123456789876543210
arg. SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210
type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210) h0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210
instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd
(((,)
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference)
())
data Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210
where
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: forall n0123456789876543210
arg. SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210
type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210
type family Let0123456789876543210Scrutinee_0123456789876543210 n h t where
Let0123456789876543210Scrutinee_0123456789876543210 n h t = Apply (Apply LeqSym0 n) h
type family Case_0123456789876543210 n h t t where
Case_0123456789876543210 n h t 'True = Apply (Apply (:@#@$) n) (Apply (Apply (:@#@$) h) t)
Case_0123456789876543210 n h t 'False = Apply (Apply (:@#@$) h) (Apply (Apply InsertSym0 n) t)
type InsertionSortSym1 (a0123456789876543210 :: [Nat]) =
InsertionSort a0123456789876543210
instance SuppressUnusedWarnings InsertionSortSym0 where
suppressUnusedWarnings
= snd (((,) InsertionSortSym0KindInference) ())
data InsertionSortSym0 :: (~>) [Nat] [Nat]
where
InsertionSortSym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply InsertionSortSym0 arg) (InsertionSortSym1 arg) =>
InsertionSortSym0 a0123456789876543210
type instance Apply InsertionSortSym0 a0123456789876543210 = InsertionSort a0123456789876543210
type InsertSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: [Nat]) =
Insert a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (InsertSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) InsertSym1KindInference) ())
data InsertSym1 (a0123456789876543210 :: Nat) :: (~>) [Nat] [Nat]
where
InsertSym1KindInference :: forall a0123456789876543210
a0123456789876543210
arg. SameKind (Apply (InsertSym1 a0123456789876543210) arg) (InsertSym2 a0123456789876543210 arg) =>
InsertSym1 a0123456789876543210 a0123456789876543210
type instance Apply (InsertSym1 a0123456789876543210) a0123456789876543210 = Insert a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings InsertSym0 where
suppressUnusedWarnings = snd (((,) InsertSym0KindInference) ())
data InsertSym0 :: (~>) Nat ((~>) [Nat] [Nat])
where
InsertSym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply InsertSym0 arg) (InsertSym1 arg) =>
InsertSym0 a0123456789876543210
type instance Apply InsertSym0 a0123456789876543210 = InsertSym1 a0123456789876543210
type LeqSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) =
Leq a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (LeqSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) LeqSym1KindInference) ())
data LeqSym1 (a0123456789876543210 :: Nat) :: (~>) Nat Bool
where
LeqSym1KindInference :: forall a0123456789876543210
a0123456789876543210
arg. SameKind (Apply (LeqSym1 a0123456789876543210) arg) (LeqSym2 a0123456789876543210 arg) =>
LeqSym1 a0123456789876543210 a0123456789876543210
type instance Apply (LeqSym1 a0123456789876543210) a0123456789876543210 = Leq a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings LeqSym0 where
suppressUnusedWarnings = snd (((,) LeqSym0KindInference) ())
data LeqSym0 :: (~>) Nat ((~>) Nat Bool)
where
LeqSym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply LeqSym0 arg) (LeqSym1 arg) =>
LeqSym0 a0123456789876543210
type instance Apply LeqSym0 a0123456789876543210 = LeqSym1 a0123456789876543210
type family InsertionSort (a :: [Nat]) :: [Nat] where
InsertionSort '[] = '[]
InsertionSort ('(:) h t) = Apply (Apply InsertSym0 h) (Apply InsertionSortSym0 t)
type family Insert (a :: Nat) (a :: [Nat]) :: [Nat] where
Insert n '[] = Apply (Apply (:@#@$) n) '[]
Insert n ('(:) h t) = Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t)
type family Leq (a :: Nat) (a :: Nat) :: Bool where
Leq 'Zero _ = TrueSym0
Leq ('Succ _) 'Zero = FalseSym0
Leq ('Succ a) ('Succ b) = Apply (Apply LeqSym0 a) b
sInsertionSort ::
forall (t :: [Nat]).
Sing t -> Sing (Apply InsertionSortSym0 t :: [Nat])
sInsert ::
forall (t :: Nat) (t :: [Nat]).
Sing t -> Sing t -> Sing (Apply (Apply InsertSym0 t) t :: [Nat])
sLeq ::
forall (t :: Nat) (t :: Nat).
Sing t -> Sing t -> Sing (Apply (Apply LeqSym0 t) t :: Bool)
sInsertionSort SNil = SNil
sInsertionSort (SCons (sH :: Sing h) (sT :: Sing t))
= (applySing ((applySing ((singFun2 @InsertSym0) sInsert)) sH))
((applySing ((singFun1 @InsertionSortSym0) sInsertionSort)) sT)
sInsert (sN :: Sing n) SNil
= (applySing ((applySing ((singFun2 @(:@#@$)) SCons)) sN)) SNil
sInsert (sN :: Sing n) (SCons (sH :: Sing h) (sT :: Sing t))
= let
sScrutinee_0123456789876543210 ::
Sing (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t)
sScrutinee_0123456789876543210
= (applySing ((applySing ((singFun2 @LeqSym0) sLeq)) sN)) sH
in
(id
@(Sing (Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t) :: [Nat])))
(case sScrutinee_0123456789876543210 of
STrue
-> (applySing ((applySing ((singFun2 @(:@#@$)) SCons)) sN))
((applySing ((applySing ((singFun2 @(:@#@$)) SCons)) sH)) sT)
SFalse
-> (applySing ((applySing ((singFun2 @(:@#@$)) SCons)) sH))
((applySing ((applySing ((singFun2 @InsertSym0) sInsert)) sN)) sT))
sLeq SZero _ = STrue
sLeq (SSucc _) SZero = SFalse
sLeq (SSucc (sA :: Sing a)) (SSucc (sB :: Sing b))
= (applySing ((applySing ((singFun2 @LeqSym0) sLeq)) sA)) sB
instance SingI (InsertionSortSym0 :: (~>) [Nat] [Nat]) where
sing = (singFun1 @InsertionSortSym0) sInsertionSort
instance SingI (InsertSym0 :: (~>) Nat ((~>) [Nat] [Nat])) where
sing = (singFun2 @InsertSym0) sInsert
instance SingI d =>
SingI (InsertSym1 (d :: Nat) :: (~>) [Nat] [Nat]) where
sing = (singFun1 @(InsertSym1 (d :: Nat))) (sInsert (sing @d))
instance SingI (LeqSym0 :: (~>) Nat ((~>) Nat Bool)) where
sing = (singFun2 @LeqSym0) sLeq
instance SingI d =>
SingI (LeqSym1 (d :: Nat) :: (~>) Nat Bool) where
sing = (singFun1 @(LeqSym1 (d :: Nat))) (sLeq (sing @d))