singletons-1.1: tests/compile-and-dump/InsertionSort/InsertionSortImp.ghc78.template
InsertionSort/InsertionSortImp.hs:0:0: Splicing declarations
singletons [d| data Nat = Zero | Succ Nat |]
======>
InsertionSort/InsertionSortImp.hs:(0,0)-(0,0)
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. KindOf (Apply SuccSym0 arg) ~ KindOf (SuccSym1 arg) =>
SuccSym0KindInference
type instance Apply SuccSym0 l = SuccSym1 l
data instance Sing (z :: Nat)
= z ~ Zero => SZero |
forall (n :: Nat). z ~ Succ n => SSucc (Sing n)
type SNat (z :: Nat) = Sing z
instance SingKind (KProxy :: KProxy Nat) where
type DemoteRep (KProxy :: KProxy Nat) = Nat
fromSing SZero = Zero
fromSing (SSucc b) = Succ (fromSing b)
toSing Zero = SomeSing SZero
toSing (Succ b)
= case toSing b :: SomeSing (KProxy :: KProxy 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: 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) |]
======>
InsertionSort/InsertionSortImp.hs:(0,0)-(0,0)
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 Let_0123456789Scrutinee_0123456789Sym3 t t t =
Let_0123456789Scrutinee_0123456789 t t t
instance SuppressUnusedWarnings Let_0123456789Scrutinee_0123456789Sym2 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,)
Let_0123456789Scrutinee_0123456789Sym2KindInference GHC.Tuple.())
data Let_0123456789Scrutinee_0123456789Sym2 l l l
= forall arg. KindOf (Apply (Let_0123456789Scrutinee_0123456789Sym2 l l) arg) ~ KindOf (Let_0123456789Scrutinee_0123456789Sym3 l l arg) =>
Let_0123456789Scrutinee_0123456789Sym2KindInference
type instance Apply (Let_0123456789Scrutinee_0123456789Sym2 l l) l = Let_0123456789Scrutinee_0123456789Sym3 l l l
instance SuppressUnusedWarnings Let_0123456789Scrutinee_0123456789Sym1 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,)
Let_0123456789Scrutinee_0123456789Sym1KindInference GHC.Tuple.())
data Let_0123456789Scrutinee_0123456789Sym1 l l
= forall arg. KindOf (Apply (Let_0123456789Scrutinee_0123456789Sym1 l) arg) ~ KindOf (Let_0123456789Scrutinee_0123456789Sym2 l arg) =>
Let_0123456789Scrutinee_0123456789Sym1KindInference
type instance Apply (Let_0123456789Scrutinee_0123456789Sym1 l) l = Let_0123456789Scrutinee_0123456789Sym2 l l
instance SuppressUnusedWarnings Let_0123456789Scrutinee_0123456789Sym0 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,)
Let_0123456789Scrutinee_0123456789Sym0KindInference GHC.Tuple.())
data Let_0123456789Scrutinee_0123456789Sym0 l
= forall arg. KindOf (Apply Let_0123456789Scrutinee_0123456789Sym0 arg) ~ KindOf (Let_0123456789Scrutinee_0123456789Sym1 arg) =>
Let_0123456789Scrutinee_0123456789Sym0KindInference
type instance Apply Let_0123456789Scrutinee_0123456789Sym0 l = Let_0123456789Scrutinee_0123456789Sym1 l
type Let_0123456789Scrutinee_0123456789 n h t =
Apply (Apply LeqSym0 n) h
type family Case_0123456789 n h t t where
Case_0123456789 n h t True = Apply (Apply (:$) n) (Apply (Apply (:$) h) t)
Case_0123456789 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. KindOf (Apply (LeqSym1 l) arg) ~ KindOf (LeqSym2 l arg) =>
LeqSym1KindInference
type instance Apply (LeqSym1 l) l = LeqSym2 l l
instance SuppressUnusedWarnings LeqSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) LeqSym0KindInference GHC.Tuple.())
data LeqSym0 (l :: TyFun Nat (TyFun Nat Bool -> *))
= forall arg. KindOf (Apply LeqSym0 arg) ~ KindOf (LeqSym1 arg) =>
LeqSym0KindInference
type instance Apply LeqSym0 l = LeqSym1 l
type InsertSym2 (t :: Nat) (t :: GHC.Types.[] Nat) = Insert t t
instance SuppressUnusedWarnings InsertSym1 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) InsertSym1KindInference GHC.Tuple.())
data InsertSym1 (l :: Nat)
(l :: TyFun (GHC.Types.[] Nat) (GHC.Types.[] Nat))
= forall arg. KindOf (Apply (InsertSym1 l) arg) ~ KindOf (InsertSym2 l arg) =>
InsertSym1KindInference
type instance Apply (InsertSym1 l) l = InsertSym2 l l
instance SuppressUnusedWarnings InsertSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) InsertSym0KindInference GHC.Tuple.())
data InsertSym0 (l :: TyFun Nat (TyFun (GHC.Types.[] Nat) (GHC.Types.[] Nat)
-> *))
= forall arg. KindOf (Apply InsertSym0 arg) ~ KindOf (InsertSym1 arg) =>
InsertSym0KindInference
type instance Apply InsertSym0 l = InsertSym1 l
type InsertionSortSym1 (t :: GHC.Types.[] Nat) = InsertionSort t
instance SuppressUnusedWarnings InsertionSortSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) InsertionSortSym0KindInference GHC.Tuple.())
data InsertionSortSym0 (l :: TyFun (GHC.Types.[] Nat) (GHC.Types.[] Nat))
= forall arg. KindOf (Apply InsertionSortSym0 arg) ~ KindOf (InsertionSortSym1 arg) =>
InsertionSortSym0KindInference
type instance Apply InsertionSortSym0 l = InsertionSortSym1 l
type family Leq (a :: Nat) (a :: Nat) :: Bool where
Leq Zero z = TrueSym0
Leq (Succ z) Zero = FalseSym0
Leq (Succ a) (Succ b) = Apply (Apply LeqSym0 a) b
type family Insert (a :: Nat)
(a :: GHC.Types.[] Nat) :: GHC.Types.[] Nat where
Insert n GHC.Types.[] = Apply (Apply (:$) n) GHC.Types.[]
Insert n ((GHC.Types.:) h t) = Case_0123456789 n h t (Let_0123456789Scrutinee_0123456789Sym3 n h t)
type family InsertionSort (a :: GHC.Types.[] Nat) :: GHC.Types.[] Nat where
InsertionSort GHC.Types.[] = GHC.Types.[]
InsertionSort ((GHC.Types.:) 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)
sInsert ::
forall (t :: Nat) (t :: GHC.Types.[] Nat).
Sing t -> Sing t -> Sing (Apply (Apply InsertSym0 t) t)
sInsertionSort ::
forall (t :: GHC.Types.[] Nat).
Sing t -> Sing (Apply InsertionSortSym0 t)
sLeq SZero _
= let
lambda ::
forall wild. (t ~ ZeroSym0, t ~ wild) =>
Sing (Apply (Apply LeqSym0 ZeroSym0) wild)
lambda = STrue
in lambda
sLeq (SSucc _) SZero
= let
lambda ::
forall wild. (t ~ Apply SuccSym0 wild, t ~ ZeroSym0) =>
Sing (Apply (Apply LeqSym0 (Apply SuccSym0 wild)) ZeroSym0)
lambda = SFalse
in lambda
sLeq (SSucc sA) (SSucc sB)
= let
lambda ::
forall a b. (t ~ Apply SuccSym0 a, t ~ Apply SuccSym0 b) =>
Sing a
-> Sing b
-> Sing (Apply (Apply LeqSym0 (Apply SuccSym0 a)) (Apply SuccSym0 b))
lambda a b
= applySing
(applySing (singFun2 (Proxy :: Proxy LeqSym0) sLeq) a) b
in lambda sA sB
sInsert sN SNil
= let
lambda ::
forall n. (t ~ n, t ~ GHC.Types.[]) =>
Sing n -> Sing (Apply (Apply InsertSym0 n) GHC.Types.[])
lambda n
= applySing
(applySing (singFun2 (Proxy :: Proxy (:$)) SCons) n) SNil
in lambda sN
sInsert sN (SCons sH sT)
= let
lambda ::
forall n h t. (t ~ n, t ~ Apply (Apply (:$) h) t) =>
Sing n
-> Sing h
-> Sing t
-> Sing (Apply (Apply InsertSym0 n) (Apply (Apply (:$) h) t))
lambda n h t
= let
sScrutinee_0123456789 ::
Sing (Let_0123456789Scrutinee_0123456789Sym3 n h t)
sScrutinee_0123456789
= applySing
(applySing (singFun2 (Proxy :: Proxy LeqSym0) sLeq) n) h
in
case sScrutinee_0123456789 of {
STrue
-> let
lambda :: Sing (Case_0123456789 n h t TrueSym0)
lambda
= applySing
(applySing (singFun2 (Proxy :: Proxy (:$)) SCons) n)
(applySing (applySing (singFun2 (Proxy :: Proxy (:$)) SCons) h) t)
in lambda
SFalse
-> let
lambda :: Sing (Case_0123456789 n h t FalseSym0)
lambda
= applySing
(applySing (singFun2 (Proxy :: Proxy (:$)) SCons) h)
(applySing
(applySing (singFun2 (Proxy :: Proxy InsertSym0) sInsert) n) t)
in lambda }
in lambda sN sH sT
sInsertionSort SNil
= let
lambda ::
t ~ GHC.Types.[] => Sing (Apply InsertionSortSym0 GHC.Types.[])
lambda = SNil
in lambda
sInsertionSort (SCons sH sT)
= let
lambda ::
forall h t. t ~ Apply (Apply (:$) h) t =>
Sing h
-> Sing t
-> Sing (Apply InsertionSortSym0 (Apply (Apply (:$) h) t))
lambda h t
= applySing
(applySing (singFun2 (Proxy :: Proxy InsertSym0) sInsert) h)
(applySing
(singFun1 (Proxy :: Proxy InsertionSortSym0) sInsertionSort) t)
in lambda sH sT