{-| 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.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 (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
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 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 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