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