    {-# OPTIONS_GHC -Wall #-}

    {-| 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 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.Syntax.Common.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 (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
    $cshowsPrec :: forall a. Show a => Int -> SplitTree' a -> ShowS
    showsPrec :: Int -> SplitTree' a -> ShowS
    $cshow :: forall a. Show a => SplitTree' a -> String
    show :: SplitTree' a -> String
    $cshowList :: forall a. Show a => [SplitTree' a] -> ShowS
    showList :: [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
    $cfrom :: forall a x. SplitTree' a -> Rep (SplitTree' a) x
    from :: forall x. SplitTree' a -> Rep (SplitTree' a) x
    $cto :: forall a x. Rep (SplitTree' a) x -> SplitTree' a
    to :: forall x. Rep (SplitTree' a) x -> SplitTree' a
    Generic)

    data LazySplit = LazySplit | StrictSplit
      deriving (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
    $cshowsPrec :: Int -> LazySplit -> ShowS
    showsPrec :: Int -> LazySplit -> ShowS
    $cshow :: LazySplit -> String
    show :: LazySplit -> String
    $cshowList :: [LazySplit] -> ShowS
    showList :: [LazySplit] -> ShowS
    Show, LazySplit -> LazySplit -> Bool
    (LazySplit -> LazySplit -> Bool)
    -> (LazySplit -> LazySplit -> Bool) -> Eq LazySplit
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: LazySplit -> LazySplit -> Bool
    == :: LazySplit -> LazySplit -> Bool
    $c/= :: LazySplit -> LazySplit -> Bool
    /= :: 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
    $ccompare :: LazySplit -> LazySplit -> Ordering
    compare :: LazySplit -> LazySplit -> Ordering
    $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
    >= :: LazySplit -> LazySplit -> Bool
    $cmax :: LazySplit -> LazySplit -> LazySplit
    max :: LazySplit -> LazySplit -> LazySplit
    $cmin :: LazySplit -> LazySplit -> LazySplit
    min :: LazySplit -> LazySplit -> LazySplit
    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
    $cfrom :: forall x. LazySplit -> Rep LazySplit x
    from :: forall x. LazySplit -> Rep LazySplit x
    $cto :: forall x. Rep LazySplit x -> LazySplit
    to :: forall x. Rep LazySplit x -> LazySplit
    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
    $cshowsPrec :: Int -> SplitTag -> ShowS
    showsPrec :: Int -> SplitTag -> ShowS
    $cshow :: SplitTag -> String
    show :: SplitTag -> String
    $cshowList :: [SplitTag] -> ShowS
    showList :: [SplitTag] -> ShowS
    Show, SplitTag -> SplitTag -> Bool
    (SplitTag -> SplitTag -> Bool)
    -> (SplitTag -> SplitTag -> Bool) -> Eq SplitTag
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: SplitTag -> SplitTag -> Bool
    == :: SplitTag -> SplitTag -> Bool
    $c/= :: SplitTag -> SplitTag -> Bool
    /= :: 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
    $ccompare :: SplitTag -> SplitTag -> Ordering
    compare :: SplitTag -> SplitTag -> Ordering
    $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
    >= :: SplitTag -> SplitTag -> Bool
    $cmax :: SplitTag -> SplitTag -> SplitTag
    max :: SplitTag -> SplitTag -> SplitTag
    $cmin :: SplitTag -> SplitTag -> SplitTag
    min :: SplitTag -> SplitTag -> SplitTag
    Ord, (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
    $cfrom :: forall x. SplitTag -> Rep SplitTag x
    from :: forall x. SplitTag -> Rep SplitTag x
    $cto :: forall x. Rep SplitTag x -> SplitTag
    to :: forall x. Rep SplitTag x -> SplitTag
    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
    forall a. String -> Doc a
    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
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc
    forall a. String -> Doc a
    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
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc
    forall a. String -> Doc a
    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
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc
    forall a. String -> Doc a
    text String
    "->" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> LazySplit -> Doc
    forall {a}. (IsString a, Null a) => LazySplit -> a
    lzp LazySplit
    lz Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc
    forall a. String -> Doc a
    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 = Just c }) [Tree (SplitTreeLabel a)]
    ts

    instance Pretty a => Pretty (SplitTree' a) where
      pretty :: SplitTree' a -> Doc
    pretty = String -> Doc
    forall a. String -> Doc a
    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 a b. (a -> b) -> Tree a -> Tree b
    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 t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN QName -> SplitTag
    SplitCon QName
    c
        SplitLit Literal
    l -> (Literal -> SplitTag) -> Literal -> SplitTag
    forall t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN 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 t (b :: Bool).
    (KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
    t -> t
    killRangeN (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