{-| 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 (Typeable (SplitTree' a)
Typeable (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 (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (SplitTree' a))
-> (SplitTree' a -> Constr)
-> (SplitTree' a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (SplitTree' a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (SplitTree' a)))
-> ((forall b. Data b => b -> b) -> SplitTree' a -> SplitTree' a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SplitTree' a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SplitTree' a -> r)
-> (forall u. (forall d. Data d => d -> u) -> SplitTree' a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SplitTree' a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a))
-> Data (SplitTree' a)
SplitTree' a -> DataType
SplitTree' a -> Constr
(forall b. Data b => b -> b) -> SplitTree' a -> SplitTree' a
forall {a}. Data a => Typeable (SplitTree' a)
forall a. Data a => SplitTree' a -> DataType
forall a. Data a => SplitTree' a -> Constr
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 u. Int -> (forall d. Data d => d -> u) -> SplitTree' a -> u
forall u. (forall d. Data d => d -> u) -> SplitTree' a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SplitTree' a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SplitTree' a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SplitTree' a -> m (SplitTree' 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))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> 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
[SplitTree' a] -> ShowS
SplitTree' a -> String
(Int -> SplitTree' a -> ShowS)
-> (SplitTree' a -> String)
-> ([SplitTree' a] -> ShowS)
-> Show (SplitTree' a)
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 x. SplitTree' a -> Rep (SplitTree' a) x)
-> (forall x. Rep (SplitTree' a) x -> SplitTree' a)
-> Generic (SplitTree' a)
forall x. Rep (SplitTree' a) x -> SplitTree' a
forall x. SplitTree' a -> Rep (SplitTree' a) x
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
Typeable LazySplit
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LazySplit -> c LazySplit)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LazySplit)
-> (LazySplit -> Constr)
-> (LazySplit -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> LazySplit -> LazySplit)
-> (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 u. (forall d. Data d => d -> u) -> LazySplit -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> LazySplit -> u)
-> (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 (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LazySplit -> m LazySplit)
-> Data LazySplit
LazySplit -> DataType
LazySplit -> Constr
(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
(Int -> LazySplit -> ShowS)
-> (LazySplit -> String)
-> ([LazySplit] -> ShowS)
-> Show LazySplit
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
(LazySplit -> LazySplit -> Bool)
-> (LazySplit -> LazySplit -> Bool) -> Eq LazySplit
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
Eq LazySplit
-> (LazySplit -> LazySplit -> Ordering)
-> (LazySplit -> LazySplit -> Bool)
-> (LazySplit -> LazySplit -> Bool)
-> (LazySplit -> LazySplit -> Bool)
-> (LazySplit -> LazySplit -> Bool)
-> (LazySplit -> LazySplit -> LazySplit)
-> (LazySplit -> LazySplit -> LazySplit)
-> Ord 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. LazySplit -> Rep LazySplit x)
-> (forall x. Rep LazySplit x -> LazySplit) -> Generic LazySplit
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
(Int -> SplitTag -> ShowS)
-> (SplitTag -> String) -> ([SplitTag] -> ShowS) -> Show SplitTag
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
(SplitTag -> SplitTag -> Bool)
-> (SplitTag -> SplitTag -> Bool) -> Eq SplitTag
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
Eq SplitTag
-> (SplitTag -> SplitTag -> Ordering)
-> (SplitTag -> SplitTag -> Bool)
-> (SplitTag -> SplitTag -> Bool)
-> (SplitTag -> SplitTag -> Bool)
-> (SplitTag -> SplitTag -> Bool)
-> (SplitTag -> SplitTag -> SplitTag)
-> (SplitTag -> SplitTag -> SplitTag)
-> Ord 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
Typeable SplitTag
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> SplitTag -> c SplitTag)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SplitTag)
-> (SplitTag -> Constr)
-> (SplitTag -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> SplitTag -> SplitTag)
-> (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 u. (forall d. Data d => d -> u) -> SplitTag -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> SplitTag -> u)
-> (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 (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SplitTag -> m SplitTag)
-> Data SplitTag
SplitTag -> DataType
SplitTag -> Constr
(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. SplitTag -> Rep SplitTag x)
-> (forall x. Rep SplitTag x -> SplitTag) -> Generic SplitTag
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) = QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
c
  pretty (SplitLit Literal
l)  = Literal -> Doc
forall a. Pretty a => a -> Doc
pretty Literal
l
  pretty SplitTag
SplitCatchall = Doc
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 (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"done, " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Pretty a => a -> String
prettyShow Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" bindings"
    SplitTreeLabel Maybe a
Nothing (Just Arg Int
n)  LazySplit
lz Maybe Int
Nothing  -> LazySplit -> Doc
forall {a}. (IsString a, Null a) => LazySplit -> a
lzp LazySplit
lz Doc -> Doc -> Doc
<+> String -> Doc
text (String
"split at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Arg Int -> String
forall a. Pretty a => a -> String
prettyShow Arg Int
n)
    SplitTreeLabel (Just a
q) Maybe (Arg Int)
Nothing  LazySplit
_  (Just Int
n) -> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
q Doc -> Doc -> Doc
<+> String -> Doc
text (String
"-> done, " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Pretty a => a -> String
prettyShow Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" bindings")
    SplitTreeLabel (Just a
q) (Just Arg Int
n) LazySplit
lz Maybe Int
Nothing  -> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
q Doc -> Doc -> Doc
<+> String -> Doc
text String
"->" Doc -> Doc -> Doc
<+> LazySplit -> Doc
forall {a}. (IsString a, Null a) => LazySplit -> a
lzp LazySplit
lz Doc -> Doc -> Doc
<+> String -> Doc
text (String
"split at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Arg Int -> String
forall a. Pretty a => a -> String
prettyShow Arg Int
n)
    SplitTreeLabel a
_ -> Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
    where lzp :: LazySplit -> a
lzp LazySplit
lz | LazySplit
lz LazySplit -> LazySplit -> Bool
forall a. Eq a => a -> a -> Bool
== LazySplit
LazySplit = a
"lazy"
                 | Bool
otherwise       = a
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 -> SplitTreeLabel a
-> [Tree (SplitTreeLabel a)] -> Tree (SplitTreeLabel a)
forall a. a -> [Tree a] -> Tree a
Node (Maybe a
-> Maybe (Arg Int) -> LazySplit -> Maybe Int -> SplitTreeLabel a
forall a.
Maybe a
-> Maybe (Arg Int) -> LazySplit -> Maybe Int -> SplitTreeLabel a
SplitTreeLabel Maybe a
forall a. Maybe a
Nothing Maybe (Arg Int)
forall a. Maybe a
Nothing LazySplit
StrictSplit (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
n)) []
  SplitAt Arg Int
n LazySplit
lz SplitTrees' a
ts    -> SplitTreeLabel a
-> [Tree (SplitTreeLabel a)] -> Tree (SplitTreeLabel a)
forall a. a -> [Tree a] -> Tree a
Node (Maybe a
-> Maybe (Arg Int) -> LazySplit -> Maybe Int -> SplitTreeLabel a
forall a.
Maybe a
-> Maybe (Arg Int) -> LazySplit -> Maybe Int -> SplitTreeLabel a
SplitTreeLabel Maybe a
forall a. Maybe a
Nothing (Arg Int -> Maybe (Arg Int)
forall a. a -> Maybe a
Just Arg Int
n) LazySplit
lz Maybe Int
forall a. Maybe a
Nothing) ([Tree (SplitTreeLabel a)] -> Tree (SplitTreeLabel a))
-> [Tree (SplitTreeLabel a)] -> Tree (SplitTreeLabel a)
forall a b. (a -> b) -> a -> b
$ SplitTrees' a -> [Tree (SplitTreeLabel a)]
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 = ((a, SplitTree' a) -> Tree (SplitTreeLabel a))
-> [(a, SplitTree' a)] -> [Tree (SplitTreeLabel a)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a
c,SplitTree' a
t) -> a -> Tree (SplitTreeLabel a) -> Tree (SplitTreeLabel a)
forall a. a -> Tree (SplitTreeLabel a) -> Tree (SplitTreeLabel a)
setCons a
c (Tree (SplitTreeLabel a) -> Tree (SplitTreeLabel a))
-> Tree (SplitTreeLabel a) -> Tree (SplitTreeLabel a)
forall a b. (a -> b) -> a -> b
$ SplitTree' a -> Tree (SplitTreeLabel a)
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) = SplitTreeLabel a
-> [Tree (SplitTreeLabel a)] -> Tree (SplitTreeLabel a)
forall a. a -> [Tree a] -> Tree a
Node (SplitTreeLabel a
l { lblConstructorName :: Maybe a
lblConstructorName = a -> Maybe a
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 (String -> Doc) -> (SplitTree' a -> String) -> SplitTree' a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tree String -> String
drawTree (Tree String -> String)
-> (SplitTree' a -> Tree String) -> SplitTree' a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SplitTreeLabel a -> String)
-> Tree (SplitTreeLabel a) -> Tree String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SplitTreeLabel a -> String
forall a. Pretty a => a -> String
prettyShow (Tree (SplitTreeLabel a) -> Tree String)
-> (SplitTree' a -> Tree (SplitTreeLabel a))
-> SplitTree' a
-> Tree String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SplitTree' a -> Tree (SplitTreeLabel a)
forall a. SplitTree' a -> Tree (SplitTreeLabel a)
toTree

instance KillRange SplitTag where
  killRange :: SplitTag -> SplitTag
killRange = \case
    SplitCon QName
c -> (QName -> SplitTag) -> QName -> SplitTag
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 QName -> SplitTag
SplitCon QName
c
    SplitLit Literal
l -> (Literal -> SplitTag) -> Literal -> SplitTag
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 -> Int -> SplitTree' a
forall a. Int -> SplitTree' a
SplittingDone Int
n
    SplitAt Arg Int
i LazySplit
lz SplitTrees' a
ts -> (SplitTrees' a -> SplitTree' a) -> SplitTrees' a -> SplitTree' a
forall a b. KillRange a => (a -> b) -> a -> b
killRange1 (Arg Int -> LazySplit -> SplitTrees' a -> SplitTree' a
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