module Agda.TypeChecking.Coverage.SplitTree where
import Control.DeepSeq
import Data.Tree
import Data.Data (Data)
import GHC.Generics (Generic)
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Utils.Pretty
import Agda.Utils.Null
import Agda.Utils.Impossible
type SplitTree = SplitTree' SplitTag
type SplitTrees = SplitTrees' SplitTag
data SplitTree' a
=
SplittingDone
{ forall a. SplitTree' a -> Int
splitBindings :: Int
}
|
SplitAt
{ forall a. SplitTree' a -> Arg Int
splitArg :: Arg Int
, forall a. SplitTree' a -> LazySplit
splitLazy :: LazySplit
, forall a. SplitTree' a -> SplitTrees' a
splitTrees :: SplitTrees' a
}
deriving (SplitTree' a -> Constr
SplitTree' a -> DataType
forall {a}. Data a => Typeable (SplitTree' a)
forall a. Data a => SplitTree' a -> Constr
forall a. Data a => SplitTree' a -> DataType
forall a.
Data a =>
(forall b. Data b => b -> b) -> SplitTree' a -> SplitTree' a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> SplitTree' a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> SplitTree' a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SplitTree' a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SplitTree' a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SplitTree' a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SplitTree' a -> c (SplitTree' a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (SplitTree' a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (SplitTree' a))
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SplitTree' a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SplitTree' a -> c (SplitTree' a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (SplitTree' a))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SplitTree' a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> SplitTree' a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> SplitTree' a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> SplitTree' a -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SplitTree' a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SplitTree' a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SplitTree' a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SplitTree' a -> r
gmapT :: (forall b. Data b => b -> b) -> SplitTree' a -> SplitTree' a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> SplitTree' a -> SplitTree' a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (SplitTree' a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (SplitTree' a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (SplitTree' a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (SplitTree' a))
dataTypeOf :: SplitTree' a -> DataType
$cdataTypeOf :: forall a. Data a => SplitTree' a -> DataType
toConstr :: SplitTree' a -> Constr
$ctoConstr :: forall a. Data a => SplitTree' a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SplitTree' a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SplitTree' a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SplitTree' a -> c (SplitTree' a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SplitTree' a -> c (SplitTree' a)
Data, Int -> SplitTree' a -> ShowS
forall a. Show a => Int -> SplitTree' a -> ShowS
forall a. Show a => [SplitTree' a] -> ShowS
forall a. Show a => SplitTree' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SplitTree' a] -> ShowS
$cshowList :: forall a. Show a => [SplitTree' a] -> ShowS
show :: SplitTree' a -> String
$cshow :: forall a. Show a => SplitTree' a -> String
showsPrec :: Int -> SplitTree' a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> SplitTree' a -> ShowS
Show, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (SplitTree' a) x -> SplitTree' a
forall a x. SplitTree' a -> Rep (SplitTree' a) x
$cto :: forall a x. Rep (SplitTree' a) x -> SplitTree' a
$cfrom :: forall a x. SplitTree' a -> Rep (SplitTree' a) x
Generic)
data LazySplit = LazySplit | StrictSplit
deriving (Typeable LazySplit
LazySplit -> Constr
LazySplit -> DataType
(forall b. Data b => b -> b) -> LazySplit -> LazySplit
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> LazySplit -> u
forall u. (forall d. Data d => d -> u) -> LazySplit -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LazySplit -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LazySplit -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LazySplit -> m LazySplit
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LazySplit -> m LazySplit
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LazySplit
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LazySplit -> c LazySplit
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LazySplit)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LazySplit)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LazySplit -> m LazySplit
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LazySplit -> m LazySplit
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LazySplit -> m LazySplit
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LazySplit -> m LazySplit
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LazySplit -> m LazySplit
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LazySplit -> m LazySplit
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LazySplit -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LazySplit -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> LazySplit -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LazySplit -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LazySplit -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LazySplit -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LazySplit -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LazySplit -> r
gmapT :: (forall b. Data b => b -> b) -> LazySplit -> LazySplit
$cgmapT :: (forall b. Data b => b -> b) -> LazySplit -> LazySplit
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LazySplit)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LazySplit)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LazySplit)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LazySplit)
dataTypeOf :: LazySplit -> DataType
$cdataTypeOf :: LazySplit -> DataType
toConstr :: LazySplit -> Constr
$ctoConstr :: LazySplit -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LazySplit
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LazySplit
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LazySplit -> c LazySplit
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LazySplit -> c LazySplit
Data, Int -> LazySplit -> ShowS
[LazySplit] -> ShowS
LazySplit -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LazySplit] -> ShowS
$cshowList :: [LazySplit] -> ShowS
show :: LazySplit -> String
$cshow :: LazySplit -> String
showsPrec :: Int -> LazySplit -> ShowS
$cshowsPrec :: Int -> LazySplit -> ShowS
Show, LazySplit -> LazySplit -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LazySplit -> LazySplit -> Bool
$c/= :: LazySplit -> LazySplit -> Bool
== :: LazySplit -> LazySplit -> Bool
$c== :: LazySplit -> LazySplit -> Bool
Eq, Eq LazySplit
LazySplit -> LazySplit -> Bool
LazySplit -> LazySplit -> Ordering
LazySplit -> LazySplit -> LazySplit
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: LazySplit -> LazySplit -> LazySplit
$cmin :: LazySplit -> LazySplit -> LazySplit
max :: LazySplit -> LazySplit -> LazySplit
$cmax :: LazySplit -> LazySplit -> LazySplit
>= :: LazySplit -> LazySplit -> Bool
$c>= :: LazySplit -> LazySplit -> Bool
> :: LazySplit -> LazySplit -> Bool
$c> :: LazySplit -> LazySplit -> Bool
<= :: LazySplit -> LazySplit -> Bool
$c<= :: LazySplit -> LazySplit -> Bool
< :: LazySplit -> LazySplit -> Bool
$c< :: LazySplit -> LazySplit -> Bool
compare :: LazySplit -> LazySplit -> Ordering
$ccompare :: LazySplit -> LazySplit -> Ordering
Ord, forall x. Rep LazySplit x -> LazySplit
forall x. LazySplit -> Rep LazySplit x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep LazySplit x -> LazySplit
$cfrom :: forall x. LazySplit -> Rep LazySplit x
Generic)
type SplitTrees' a = [(a, SplitTree' a)]
data SplitTag
= SplitCon QName
| SplitLit Literal
| SplitCatchall
deriving (Int -> SplitTag -> ShowS
[SplitTag] -> ShowS
SplitTag -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SplitTag] -> ShowS
$cshowList :: [SplitTag] -> ShowS
show :: SplitTag -> String
$cshow :: SplitTag -> String
showsPrec :: Int -> SplitTag -> ShowS
$cshowsPrec :: Int -> SplitTag -> ShowS
Show, SplitTag -> SplitTag -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SplitTag -> SplitTag -> Bool
$c/= :: SplitTag -> SplitTag -> Bool
== :: SplitTag -> SplitTag -> Bool
$c== :: SplitTag -> SplitTag -> Bool
Eq, Eq SplitTag
SplitTag -> SplitTag -> Bool
SplitTag -> SplitTag -> Ordering
SplitTag -> SplitTag -> SplitTag
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SplitTag -> SplitTag -> SplitTag
$cmin :: SplitTag -> SplitTag -> SplitTag
max :: SplitTag -> SplitTag -> SplitTag
$cmax :: SplitTag -> SplitTag -> SplitTag
>= :: SplitTag -> SplitTag -> Bool
$c>= :: SplitTag -> SplitTag -> Bool
> :: SplitTag -> SplitTag -> Bool
$c> :: SplitTag -> SplitTag -> Bool
<= :: SplitTag -> SplitTag -> Bool
$c<= :: SplitTag -> SplitTag -> Bool
< :: SplitTag -> SplitTag -> Bool
$c< :: SplitTag -> SplitTag -> Bool
compare :: SplitTag -> SplitTag -> Ordering
$ccompare :: SplitTag -> SplitTag -> Ordering
Ord, Typeable SplitTag
SplitTag -> Constr
SplitTag -> DataType
(forall b. Data b => b -> b) -> SplitTag -> SplitTag
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SplitTag -> u
forall u. (forall d. Data d => d -> u) -> SplitTag -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SplitTag -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SplitTag -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SplitTag -> m SplitTag
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SplitTag -> m SplitTag
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SplitTag
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SplitTag -> c SplitTag
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SplitTag)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SplitTag)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SplitTag -> m SplitTag
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SplitTag -> m SplitTag
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SplitTag -> m SplitTag
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SplitTag -> m SplitTag
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SplitTag -> m SplitTag
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SplitTag -> m SplitTag
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SplitTag -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SplitTag -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> SplitTag -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SplitTag -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SplitTag -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SplitTag -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SplitTag -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SplitTag -> r
gmapT :: (forall b. Data b => b -> b) -> SplitTag -> SplitTag
$cgmapT :: (forall b. Data b => b -> b) -> SplitTag -> SplitTag
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SplitTag)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SplitTag)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SplitTag)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SplitTag)
dataTypeOf :: SplitTag -> DataType
$cdataTypeOf :: SplitTag -> DataType
toConstr :: SplitTag -> Constr
$ctoConstr :: SplitTag -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SplitTag
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SplitTag
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SplitTag -> c SplitTag
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SplitTag -> c SplitTag
Data, forall x. Rep SplitTag x -> SplitTag
forall x. SplitTag -> Rep SplitTag x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SplitTag x -> SplitTag
$cfrom :: forall x. SplitTag -> Rep SplitTag x
Generic)
instance Pretty SplitTag where
pretty :: SplitTag -> Doc
pretty (SplitCon QName
c) = forall a. Pretty a => a -> Doc
pretty QName
c
pretty (SplitLit Literal
l) = forall a. Pretty a => a -> Doc
pretty Literal
l
pretty SplitTag
SplitCatchall = forall a. Underscore a => a
underscore
data SplitTreeLabel a = SplitTreeLabel
{ forall a. SplitTreeLabel a -> Maybe a
lblConstructorName :: Maybe a
, forall a. SplitTreeLabel a -> Maybe (Arg Int)
lblSplitArg :: Maybe (Arg Int)
, forall a. SplitTreeLabel a -> LazySplit
lblLazy :: LazySplit
, forall a. SplitTreeLabel a -> Maybe Int
lblBindings :: Maybe Int
}
instance Pretty a => Pretty (SplitTreeLabel a) where
pretty :: SplitTreeLabel a -> Doc
pretty = \case
SplitTreeLabel Maybe a
Nothing Maybe (Arg Int)
Nothing LazySplit
_ (Just Int
n) -> String -> Doc
text forall a b. (a -> b) -> a -> b
$ String
"done, " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow Int
n forall a. [a] -> [a] -> [a]
++ String
" bindings"
SplitTreeLabel Maybe a
Nothing (Just Arg Int
n) LazySplit
lz Maybe Int
Nothing -> forall {a}. (IsString a, Null a) => LazySplit -> a
lzp LazySplit
lz Doc -> Doc -> Doc
<+> String -> Doc
text (String
"split at " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow Arg Int
n)
SplitTreeLabel (Just a
q) Maybe (Arg Int)
Nothing LazySplit
_ (Just Int
n) -> forall a. Pretty a => a -> Doc
pretty a
q Doc -> Doc -> Doc
<+> String -> Doc
text (String
"-> done, " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow Int
n forall a. [a] -> [a] -> [a]
++ String
" bindings")
SplitTreeLabel (Just a
q) (Just Arg Int
n) LazySplit
lz Maybe Int
Nothing -> forall a. Pretty a => a -> Doc
pretty a
q Doc -> Doc -> Doc
<+> String -> Doc
text String
"->" Doc -> Doc -> Doc
<+> forall {a}. (IsString a, Null a) => LazySplit -> a
lzp LazySplit
lz Doc -> Doc -> Doc
<+> String -> Doc
text (String
"split at " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow Arg Int
n)
SplitTreeLabel a
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
where lzp :: LazySplit -> a
lzp LazySplit
lz | LazySplit
lz forall a. Eq a => a -> a -> Bool
== LazySplit
LazySplit = a
"lazy"
| Bool
otherwise = forall a. Null a => a
empty
toTree :: SplitTree' a -> Tree (SplitTreeLabel a)
toTree :: forall a. SplitTree' a -> Tree (SplitTreeLabel a)
toTree = \case
SplittingDone Int
n -> forall a. a -> [Tree a] -> Tree a
Node (forall a.
Maybe a
-> Maybe (Arg Int) -> LazySplit -> Maybe Int -> SplitTreeLabel a
SplitTreeLabel forall a. Maybe a
Nothing forall a. Maybe a
Nothing LazySplit
StrictSplit (forall a. a -> Maybe a
Just Int
n)) []
SplitAt Arg Int
n LazySplit
lz SplitTrees' a
ts -> forall a. a -> [Tree a] -> Tree a
Node (forall a.
Maybe a
-> Maybe (Arg Int) -> LazySplit -> Maybe Int -> SplitTreeLabel a
SplitTreeLabel forall a. Maybe a
Nothing (forall a. a -> Maybe a
Just Arg Int
n) LazySplit
lz forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ forall a. SplitTrees' a -> Forest (SplitTreeLabel a)
toTrees SplitTrees' a
ts
toTrees :: SplitTrees' a -> Forest (SplitTreeLabel a)
toTrees :: forall a. SplitTrees' a -> Forest (SplitTreeLabel a)
toTrees = forall a b. (a -> b) -> [a] -> [b]
map (\ (a
c,SplitTree' a
t) -> forall a. a -> Tree (SplitTreeLabel a) -> Tree (SplitTreeLabel a)
setCons a
c forall a b. (a -> b) -> a -> b
$ forall a. SplitTree' a -> Tree (SplitTreeLabel a)
toTree SplitTree' a
t)
where
setCons :: a -> Tree (SplitTreeLabel a) -> Tree (SplitTreeLabel a)
setCons :: forall a. a -> Tree (SplitTreeLabel a) -> Tree (SplitTreeLabel a)
setCons a
c (Node SplitTreeLabel a
l [Tree (SplitTreeLabel a)]
ts) = forall a. a -> [Tree a] -> Tree a
Node (SplitTreeLabel a
l { lblConstructorName :: Maybe a
lblConstructorName = forall a. a -> Maybe a
Just a
c }) [Tree (SplitTreeLabel a)]
ts
instance Pretty a => Pretty (SplitTree' a) where
pretty :: SplitTree' a -> Doc
pretty = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tree String -> String
drawTree forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Pretty a => a -> String
prettyShow forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SplitTree' a -> Tree (SplitTreeLabel a)
toTree
instance KillRange SplitTag where
killRange :: SplitTag -> SplitTag
killRange = \case
SplitCon QName
c -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 QName -> SplitTag
SplitCon QName
c
SplitLit Literal
l -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 Literal -> SplitTag
SplitLit Literal
l
SplitTag
SplitCatchall -> SplitTag
SplitCatchall
instance KillRange a => KillRange (SplitTree' a) where
killRange :: KillRangeT (SplitTree' a)
killRange = \case
SplittingDone Int
n -> forall a. Int -> SplitTree' a
SplittingDone Int
n
SplitAt Arg Int
i LazySplit
lz SplitTrees' a
ts -> forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (forall a. Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
SplitAt Arg Int
i LazySplit
lz) SplitTrees' a
ts
instance NFData a => NFData (SplitTree' a)
instance NFData LazySplit
instance NFData SplitTag