singletons-2.3: tests/compile-and-dump/InsertionSort/InsertionSortImp.ghc82.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 (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
data instance Sing (z :: Nat)
= z ~ Zero => SZero |
forall (n :: Nat). z ~ Succ n => SSucc (Sing (n :: Nat))
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)
= 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
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 GHC.Types.[] = [n]
insert n (h GHC.Types.: t)
= if (leq n) h then
(n GHC.Types.: (h GHC.Types.: t))
else
(h GHC.Types.: ((insert n) t))
insertionSort :: [Nat] -> [Nat]
insertionSort GHC.Types.[] = []
insertionSort (h GHC.Types.: t) = (insert h) (insertionSort t)
type Let0123456789876543210Scrutinee_0123456789876543210Sym3 t t t =
Let0123456789876543210Scrutinee_0123456789876543210 t t t
instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym2 where
suppressUnusedWarnings _
= snd
((GHC.Tuple.(,)
Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference)
GHC.Tuple.())
data Let0123456789876543210Scrutinee_0123456789876543210Sym2 l l l
= forall arg. SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 l l) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym3 l l arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference
type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 l l) l = Let0123456789876543210Scrutinee_0123456789876543210 l l l
instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym1 where
suppressUnusedWarnings _
= snd
((GHC.Tuple.(,)
Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference)
GHC.Tuple.())
data Let0123456789876543210Scrutinee_0123456789876543210Sym1 l l
= forall arg. SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 l) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym2 l arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference
type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 l) l = Let0123456789876543210Scrutinee_0123456789876543210Sym2 l l
instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
suppressUnusedWarnings _
= snd
((GHC.Tuple.(,)
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference)
GHC.Tuple.())
data Let0123456789876543210Scrutinee_0123456789876543210Sym0 l
= forall arg. SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference
type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 l = Let0123456789876543210Scrutinee_0123456789876543210Sym1 l
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 LeqSym2 (t :: Nat) (t :: Nat) = Leq t t
instance SuppressUnusedWarnings LeqSym1 where
suppressUnusedWarnings _
= snd ((GHC.Tuple.(,) LeqSym1KindInference) GHC.Tuple.())
data LeqSym1 (l :: Nat) (l :: TyFun Nat Bool)
= forall arg. SameKind (Apply (LeqSym1 l) arg) (LeqSym2 l arg) =>
LeqSym1KindInference
type instance Apply (LeqSym1 l) l = Leq l l
instance SuppressUnusedWarnings LeqSym0 where
suppressUnusedWarnings _
= snd ((GHC.Tuple.(,) LeqSym0KindInference) GHC.Tuple.())
data LeqSym0 (l :: TyFun Nat (TyFun Nat Bool -> GHC.Types.Type))
= forall arg. SameKind (Apply LeqSym0 arg) (LeqSym1 arg) =>
LeqSym0KindInference
type instance Apply LeqSym0 l = LeqSym1 l
type InsertSym2 (t :: Nat) (t :: [Nat]) = Insert t t
instance SuppressUnusedWarnings InsertSym1 where
suppressUnusedWarnings _
= snd ((GHC.Tuple.(,) InsertSym1KindInference) GHC.Tuple.())
data InsertSym1 (l :: Nat) (l :: TyFun [Nat] [Nat])
= forall arg. SameKind (Apply (InsertSym1 l) arg) (InsertSym2 l arg) =>
InsertSym1KindInference
type instance Apply (InsertSym1 l) l = Insert l l
instance SuppressUnusedWarnings InsertSym0 where
suppressUnusedWarnings _
= snd ((GHC.Tuple.(,) InsertSym0KindInference) GHC.Tuple.())
data InsertSym0 (l :: TyFun Nat (TyFun [Nat] [Nat]
-> GHC.Types.Type))
= forall arg. SameKind (Apply InsertSym0 arg) (InsertSym1 arg) =>
InsertSym0KindInference
type instance Apply InsertSym0 l = InsertSym1 l
type InsertionSortSym1 (t :: [Nat]) = InsertionSort t
instance SuppressUnusedWarnings InsertionSortSym0 where
suppressUnusedWarnings _
= snd ((GHC.Tuple.(,) InsertionSortSym0KindInference) GHC.Tuple.())
data InsertionSortSym0 (l :: TyFun [Nat] [Nat])
= forall arg. SameKind (Apply InsertionSortSym0 arg) (InsertionSortSym1 arg) =>
InsertionSortSym0KindInference
type instance Apply InsertionSortSym0 l = InsertionSort l
type family Leq (a :: Nat) (a :: Nat) :: Bool where
Leq Zero _z_0123456789876543210 = TrueSym0
Leq (Succ _z_0123456789876543210) Zero = FalseSym0
Leq (Succ a) (Succ b) = Apply (Apply LeqSym0 a) b
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 InsertionSort (a :: [Nat]) :: [Nat] where
InsertionSort '[] = '[]
InsertionSort ((:) h t) = Apply (Apply InsertSym0 h) (Apply InsertionSortSym0 t)
sLeq ::
forall (t :: Nat) (t :: Nat).
Sing t -> Sing t -> Sing (Apply (Apply LeqSym0 t) t :: Bool)
sInsert ::
forall (t :: Nat) (t :: [Nat]).
Sing t -> Sing t -> Sing (Apply (Apply InsertSym0 t) t :: [Nat])
sInsertionSort ::
forall (t :: [Nat]).
Sing t -> Sing (Apply InsertionSortSym0 t :: [Nat])
sLeq SZero _ = STrue
sLeq (SSucc _) SZero = SFalse
sLeq (SSucc (sA :: Sing a)) (SSucc (sB :: Sing b))
= (applySing ((applySing ((singFun2 @LeqSym0) sLeq)) sA)) sB
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 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) ::
Sing (Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t) :: [Nat])
sInsertionSort SNil = SNil
sInsertionSort (SCons (sH :: Sing h) (sT :: Sing t))
= (applySing ((applySing ((singFun2 @InsertSym0) sInsert)) sH))
((applySing ((singFun1 @InsertionSortSym0) sInsertionSort)) sT)