InsertionSortImp.ghc76.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 NatTyCtor = Nat
    type NatTyCtorSym0 = NatTyCtor
    type ZeroSym0 = Zero
    data SuccSym0 (k :: TyFun Nat Nat)
    type instance Apply SuccSym0 a = Succ a
    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 instance 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.[] = GHC.Types.[]
    insertionSort (h GHC.Types.: t) = insert h (insertionSort t)
    type family Leq (a :: Nat) (a :: Nat) :: Bool
    type instance Leq Zero z = TrueSym0
    type instance Leq (Succ z) Zero = FalseSym0
    type instance Leq (Succ a) (Succ b) = Apply (Apply LeqSym0 a) b
    data LeqSym1 (l :: Nat) (l :: TyFun Nat Bool)
    data LeqSym0 (k :: TyFun Nat (TyFun Nat Bool -> *))
    type instance Apply (LeqSym1 a) a = Leq a a
    type instance Apply LeqSym0 a = LeqSym1 a
    type family Insert (a :: Nat) (a :: [Nat]) :: [Nat]
    type instance Insert n GHC.Types.[] = '[n]
    type instance Insert n (GHC.Types.: h t) =
        If (Apply (Apply LeqSym0 n) h) (Apply (Apply :$ n) (Apply (Apply :$ h) t)) (Apply (Apply :$ h) (Apply (Apply InsertSym0 n) t))
    data InsertSym1 (l :: Nat) (l :: TyFun [Nat] [Nat])
    data InsertSym0 (k :: TyFun Nat (TyFun [Nat] [Nat] -> *))
    type instance Apply (InsertSym1 a) a = Insert a a
    type instance Apply InsertSym0 a = InsertSym1 a
    type family InsertionSort (a :: [Nat]) :: [Nat]
    type instance InsertionSort GHC.Types.[] = GHC.Types.[]
    type instance InsertionSort (GHC.Types.: h t) =
        Apply (Apply InsertSym0 h) (Apply InsertionSortSym0 t)
    data InsertionSortSym0 (k :: TyFun [Nat] [Nat])
    type instance Apply InsertionSortSym0 a = InsertionSort a
    sLeq ::
      forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Leq t t)
    sLeq SZero _ = STrue
    sLeq (SSucc _) SZero = SFalse
    sLeq (SSucc a) (SSucc b) = sLeq a b
    sInsert ::
      forall (t :: Nat) (t :: [Nat]).
      Sing t -> Sing t -> Sing (Insert t t)
    sInsert n SNil = SCons n SNil
    sInsert n (SCons h t)
      = sIf (sLeq n h) (SCons n (SCons h t)) (SCons h (sInsert n t))
    sInsertionSort ::
      forall (t :: [Nat]). Sing t -> Sing (InsertionSort t)
    sInsertionSort SNil = SNil
    sInsertionSort (SCons h t) = sInsert h (sInsertionSort t)