{-| Split tree for transforming pattern clauses into case trees.

The coverage checker generates a split tree from the clauses.
The clause compiler uses it to transform clauses to case trees.

The initial problem is a set of clauses.  The root node designates
on which argument to split and has subtrees for all the constructors.
Splitting continues until there is only a single clause left at
each leaf of the split tree.

-}
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 () --instance only
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

-- | Abstract case tree shape.
data SplitTree' a
  = -- | No more splits coming. We are at a single, all-variable
    -- clause.
    SplittingDone
    { forall a. SplitTree' a -> Int
splitBindings :: Int       -- ^  The number of variables bound in the clause
    }
  | -- | A split is necessary.
    SplitAt
    { forall a. SplitTree' a -> Arg Int
splitArg   :: Arg Int       -- ^ Arg. no to split at.
    , forall a. SplitTree' a -> LazySplit
splitLazy  :: LazySplit
    , forall a. SplitTree' a -> SplitTrees' a
splitTrees :: SplitTrees' a -- ^ Sub split trees.
    }
  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)

-- | Split tree branching.  A finite map from constructor names to splittrees
--   A list representation seems appropriate, since we are expecting not
--   so many constructors per data type, and there is no need for
--   random access.
type SplitTrees' a = [(a, SplitTree' a)]

-- | Tag for labeling branches of a split tree. Each branch is associated to
--   either a constructor or a literal, or is a catchall branch (currently
--   only used for splitting on a literal type).
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

-- * Printing a split tree

data SplitTreeLabel a = SplitTreeLabel
  { forall a. SplitTreeLabel a -> Maybe a
lblConstructorName :: Maybe a   -- ^ 'Nothing' for root of split tree
  , 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

-- | Convert a split tree into a 'Data.Tree' (for printing).
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