-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Dependently typed elimination functions using singletons
--   
--   This library provides eliminators for inductive data types, leveraging
--   the power of the <tt>singletons</tt> library to allow dependently
--   typed elimination.
@package eliminators
@version 0.3


-- | Generate dependently typed elimination functions using Template
--   Haskell.
module Data.Eliminator.TH

-- | <tt><a>deriveElim</a> dataName</tt> generates a top-level elimination
--   function for the datatype <tt>dataName</tt>. The eliminator will
--   follow these naming conventions: The naming conventions are:
--   
--   <ul>
--   <li>If the datatype has an alphanumeric name, its eliminator will have
--   that name with <tt>elim</tt> prepended.</li>
--   <li>If the datatype has a symbolic name, its eliminator will have that
--   name with <tt>~&gt;</tt> prepended.</li>
--   </ul>
deriveElim :: Name -> Q [Dec]

-- | <tt><a>deriveElimNamed</a> funName dataName</tt> generates a top-level
--   elimination function named <tt>funName</tt> for the datatype
--   <tt>dataName</tt>.
deriveElimNamed :: String -> Name -> Q [Dec]


-- | Dependently typed elimination functions using <tt>singletons</tt>.
module Data.Eliminator
elimBool :: forall (p_aqLQ :: (~>) Bool Type) (s_aqLR :: Bool). Sing s_aqLR -> (@@) p_aqLQ False -> (@@) p_aqLQ True -> (@@) p_aqLQ s_aqLR
elimEither :: forall (a_apTW :: Type) (b_apTX :: Type) (p_aqLW :: (~>) (Either a_apTW b_apTX) Type) (s_aqLX :: Either a_apTW b_apTX). Sing s_aqLX -> (forall (f0_aqLY :: a_apTW). Sing f0_aqLY -> (@@) p_aqLW (Left f0_aqLY)) -> (forall (f0_aqLZ :: b_apTX). Sing f0_aqLZ -> (@@) p_aqLW (Right f0_aqLZ)) -> (@@) p_aqLW s_aqLX
elimList :: forall (a_11 :: Type) (p_arcl :: (~>) ([] a_11) Type) (s_arcm :: [] a_11). Sing s_arcm -> (@@) p_arcl [] -> (forall (f0_arcn :: a_11). Sing f0_arcn -> forall (f1_arco :: [a_11]). Sing f1_arco -> (@@) p_arcl f1_arco -> (@@) p_arcl ((:) f0_arcn f1_arco)) -> (@@) p_arcl s_arcm
elimMaybe :: forall (a_11 :: Type) (p_aqM8 :: (~>) (Maybe a_11) Type) (s_aqM9 :: Maybe a_11). Sing s_aqM9 -> (@@) p_aqM8 Nothing -> (forall (f0_aqMa :: a_11). Sing f0_aqMa -> (@@) p_aqM8 (Just f0_aqMa)) -> (@@) p_aqM8 s_aqM9
elimNat :: forall (p_aqMh :: (~>) Nat Type) (s_aqMi :: Nat). Sing s_aqMi -> (@@) p_aqMh Z -> (forall (f0_aqMj :: Nat). Sing f0_aqMj -> (@@) p_aqMh f0_aqMj -> (@@) p_aqMh (S f0_aqMj)) -> (@@) p_aqMh s_aqMi
elimNonEmpty :: forall (a_akvq :: Type) (p_aqMq :: (~>) (NonEmpty a_akvq) Type) (s_aqMr :: NonEmpty a_akvq). Sing s_aqMr -> (forall (f0_aqMs :: a_akvq). Sing f0_aqMs -> forall (f1_aqMt :: [a_akvq]). Sing f1_aqMt -> (@@) p_aqMq ((:|) f0_aqMs f1_aqMt)) -> (@@) p_aqMq s_aqMr
elimOrdering :: forall (p_aqMz :: (~>) Ordering Type) (s_aqMA :: Ordering). Sing s_aqMA -> (@@) p_aqMz LT -> (@@) p_aqMz EQ -> (@@) p_aqMz GT -> (@@) p_aqMz s_aqMA
elimTuple0 :: forall (p_arjz :: (~>) () Type) (s_arjA :: ()). Sing s_arjA -> (@@) p_arjz () -> (@@) p_arjz s_arjA
elimTuple2 :: forall (a_11 :: Type) (b_12 :: Type) (p_arjC :: (~>) ((,) a_11 b_12) Type) (s_arjD :: (,) a_11 b_12). Sing s_arjD -> (forall (f0_arjE :: a_11). Sing f0_arjE -> forall (f1_arjF :: b_12). Sing f1_arjF -> (@@) p_arjC ((,) f0_arjE f1_arjF)) -> (@@) p_arjC s_arjD
elimTuple3 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (p_arjL :: (~>) ((,,) a_11 b_12 c_13) Type) (s_arjM :: (,,) a_11 b_12 c_13). Sing s_arjM -> (forall (f0_arjN :: a_11). Sing f0_arjN -> forall (f1_arjO :: b_12). Sing f1_arjO -> forall (f2_arjP :: c_13). Sing f2_arjP -> (@@) p_arjL ((,,) f0_arjN f1_arjO f2_arjP)) -> (@@) p_arjL s_arjM
elimTuple4 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (p_arjX :: (~>) ((,,,) a_11 b_12 c_13 d_14) Type) (s_arjY :: (,,,) a_11 b_12 c_13 d_14). Sing s_arjY -> (forall (f0_arjZ :: a_11). Sing f0_arjZ -> forall (f1_ark0 :: b_12). Sing f1_ark0 -> forall (f2_ark1 :: c_13). Sing f2_ark1 -> forall (f3_ark2 :: d_14). Sing f3_ark2 -> (@@) p_arjX ((,,,) f0_arjZ f1_ark0 f2_ark1 f3_ark2)) -> (@@) p_arjX s_arjY
elimTuple5 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (e_15 :: Type) (p_arkc :: (~>) ((,,,,) a_11 b_12 c_13 d_14 e_15) Type) (s_arkd :: (,,,,) a_11 b_12 c_13 d_14 e_15). Sing s_arkd -> (forall (f0_arke :: a_11). Sing f0_arke -> forall (f1_arkf :: b_12). Sing f1_arkf -> forall (f2_arkg :: c_13). Sing f2_arkg -> forall (f3_arkh :: d_14). Sing f3_arkh -> forall (f4_arki :: e_15). Sing f4_arki -> (@@) p_arkc ((,,,,) f0_arke f1_arkf f2_arkg f3_arkh f4_arki)) -> (@@) p_arkc s_arkd
elimTuple6 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (e_15 :: Type) (f_16 :: Type) (p_arku :: (~>) ((,,,,,) a_11 b_12 c_13 d_14 e_15 f_16) Type) (s_arkv :: (,,,,,) a_11 b_12 c_13 d_14 e_15 f_16). Sing s_arkv -> (forall (f0_arkw :: a_11). Sing f0_arkw -> forall (f1_arkx :: b_12). Sing f1_arkx -> forall (f2_arky :: c_13). Sing f2_arky -> forall (f3_arkz :: d_14). Sing f3_arkz -> forall (f4_arkA :: e_15). Sing f4_arkA -> forall (f5_arkB :: f_16). Sing f5_arkB -> (@@) p_arku ((,,,,,) f0_arkw f1_arkx f2_arky f3_arkz f4_arkA f5_arkB)) -> (@@) p_arku s_arkv
elimTuple7 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (e_15 :: Type) (f_16 :: Type) (g_17 :: Type) (p_arkP :: (~>) ((,,,,,,) a_11 b_12 c_13 d_14 e_15 f_16 g_17) Type) (s_arkQ :: (,,,,,,) a_11 b_12 c_13 d_14 e_15 f_16 g_17). Sing s_arkQ -> (forall (f0_arkR :: a_11). Sing f0_arkR -> forall (f1_arkS :: b_12). Sing f1_arkS -> forall (f2_arkT :: c_13). Sing f2_arkT -> forall (f3_arkU :: d_14). Sing f3_arkU -> forall (f4_arkV :: e_15). Sing f4_arkV -> forall (f5_arkW :: f_16). Sing f5_arkW -> forall (f6_arkX :: g_17). Sing f6_arkX -> (@@) p_arkP ((,,,,,,) f0_arkR f1_arkS f2_arkT f3_arkU f4_arkV f5_arkW f6_arkX)) -> (@@) p_arkP s_arkQ


-- | A crude imitation of an eliminator function for <a>Nat</a>.
module Data.Eliminator.TypeNats

-- | Although <a>Nat</a> is not actually an inductive data type in GHC, we
--   can (crudely) pretend that it is using this eliminator.
elimNat :: forall (p :: Nat ~> Type) (n :: Nat). Sing n -> p @@ 0 -> (forall (k :: Nat). Sing k -> p @@ k -> p @@ (k + 1)) -> p @@ n
