{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data.Eliminator (
elimBool
, elimEither
, elimList
, elimMaybe
, elimNat
, elimNonEmpty
, elimOrdering
, elimTuple0
, elimTuple2
, elimTuple3
, elimTuple4
, elimTuple5
, elimTuple6
, elimTuple7
, elimVoid
) where
import Control.Monad.Extra
import Data.Eliminator.TH
import Data.List.NonEmpty (NonEmpty(..))
import Data.Nat
import Data.Singletons.Prelude
import Data.Singletons.Prelude.List.NonEmpty (Sing(..))
import Data.Void (Void)
import Language.Haskell.TH.Desugar (tupleNameDegree_maybe)
$(concatMapM deriveElim [''Bool, ''Either, ''Maybe, ''Nat, ''NonEmpty, ''Ordering, ''Void])
$(deriveElimNamed "elimList" ''[])
$(concatMapM (\n -> let Just deg = tupleNameDegree_maybe n
in deriveElimNamed ("elimTuple" ++ show deg) n)
[''(), ''(,), ''(,,), ''(,,,), ''(,,,,), ''(,,,,,), ''(,,,,,,)])