singletons-2.2: tests/compile-and-dump/InsertionSort/InsertionSortImp.ghc80.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. 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 :: Nat))
type SNat = (Sing :: Nat -> GHC.Types.Type)
instance SingKind Nat where
type DemoteRep 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 Let0123456789Scrutinee_0123456789Sym3 t t t =
Let0123456789Scrutinee_0123456789 t t t
instance SuppressUnusedWarnings Let0123456789Scrutinee_0123456789Sym2 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,)
Let0123456789Scrutinee_0123456789Sym2KindInference GHC.Tuple.())
data Let0123456789Scrutinee_0123456789Sym2 l l l
= forall arg. KindOf (Apply (Let0123456789Scrutinee_0123456789Sym2 l l) arg) ~ KindOf (Let0123456789Scrutinee_0123456789Sym3 l l arg) =>
Let0123456789Scrutinee_0123456789Sym2KindInference
type instance Apply (Let0123456789Scrutinee_0123456789Sym2 l l) l = Let0123456789Scrutinee_0123456789Sym3 l l l
instance SuppressUnusedWarnings Let0123456789Scrutinee_0123456789Sym1 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,)
Let0123456789Scrutinee_0123456789Sym1KindInference GHC.Tuple.())
data Let0123456789Scrutinee_0123456789Sym1 l l
= forall arg. KindOf (Apply (Let0123456789Scrutinee_0123456789Sym1 l) arg) ~ KindOf (Let0123456789Scrutinee_0123456789Sym2 l arg) =>
Let0123456789Scrutinee_0123456789Sym1KindInference
type instance Apply (Let0123456789Scrutinee_0123456789Sym1 l) l = Let0123456789Scrutinee_0123456789Sym2 l l
instance SuppressUnusedWarnings Let0123456789Scrutinee_0123456789Sym0 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,)
Let0123456789Scrutinee_0123456789Sym0KindInference GHC.Tuple.())
data Let0123456789Scrutinee_0123456789Sym0 l
= forall arg. KindOf (Apply Let0123456789Scrutinee_0123456789Sym0 arg) ~ KindOf (Let0123456789Scrutinee_0123456789Sym1 arg) =>
Let0123456789Scrutinee_0123456789Sym0KindInference
type instance Apply Let0123456789Scrutinee_0123456789Sym0 l = Let0123456789Scrutinee_0123456789Sym1 l
type family Let0123456789Scrutinee_0123456789 n h t where
Let0123456789Scrutinee_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 -> GHC.Types.Type))
= forall arg. KindOf (Apply LeqSym0 arg) ~ KindOf (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. 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 [Nat] [Nat]
-> GHC.Types.Type))
= forall arg. KindOf (Apply InsertSym0 arg) ~ KindOf (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. 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_0123456789 = TrueSym0
Leq (Succ _z_0123456789) 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_0123456789 n h t (Let0123456789Scrutinee_0123456789Sym3 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 _s_z_0123456789
= let
lambda ::
forall _z_0123456789.
(t ~ ZeroSym0, t ~ _z_0123456789) =>
Sing _z_0123456789 -> Sing (Apply (Apply LeqSym0 t) t :: Bool)
lambda _z_0123456789 = STrue
in lambda _s_z_0123456789
sLeq (SSucc _s_z_0123456789) SZero
= let
lambda ::
forall _z_0123456789.
(t ~ Apply SuccSym0 _z_0123456789, t ~ ZeroSym0) =>
Sing _z_0123456789 -> Sing (Apply (Apply LeqSym0 t) t :: Bool)
lambda _z_0123456789 = SFalse
in lambda _s_z_0123456789
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 t) t :: Bool)
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 ~ '[]) =>
Sing n -> Sing (Apply (Apply InsertSym0 t) t :: [Nat])
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 t) t :: [Nat])
lambda n h t
= let
sScrutinee_0123456789 ::
Sing (Let0123456789Scrutinee_0123456789Sym3 n h t)
sScrutinee_0123456789
= applySing
(applySing (singFun2 (Proxy :: Proxy LeqSym0) sLeq) n) h
in case sScrutinee_0123456789 of {
STrue
-> let
lambda ::
TrueSym0 ~ Let0123456789Scrutinee_0123456789Sym3 n h t =>
Sing (Case_0123456789 n h t TrueSym0 :: [Nat])
lambda
= applySing
(applySing (singFun2 (Proxy :: Proxy (:$)) SCons) n)
(applySing (applySing (singFun2 (Proxy :: Proxy (:$)) SCons) h) t)
in lambda
SFalse
-> let
lambda ::
FalseSym0 ~ Let0123456789Scrutinee_0123456789Sym3 n h t =>
Sing (Case_0123456789 n h t FalseSym0 :: [Nat])
lambda
= applySing
(applySing (singFun2 (Proxy :: Proxy (:$)) SCons) h)
(applySing
(applySing (singFun2 (Proxy :: Proxy InsertSym0) sInsert) n) t)
in lambda } ::
Sing (Case_0123456789 n h t (Let0123456789Scrutinee_0123456789Sym3 n h t) :: [Nat])
in lambda sN sH sT
sInsertionSort SNil
= let
lambda :: t ~ '[] => Sing (Apply InsertionSortSym0 t :: [Nat])
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 t :: [Nat])
lambda h t
= applySing
(applySing (singFun2 (Proxy :: Proxy InsertSym0) sInsert) h)
(applySing
(singFun1 (Proxy :: Proxy InsertionSortSym0) sInsertionSort) t)
in lambda sH sT